Emacs HOL mode fix, need subr-x for string-remove-suffix

Fix HOL mode emacs snippets not being loaded correctly, if the HOLDIR environment variable is not set

fix hol-mode "hol-db-find" after 797ee1e

hol-mode: Fix location pragma when trimming leading connectives.

hol-mode: Fix cleanup of leading connectives in "Apply tactic"

The bug was caused by a location pragma being prepended before
cleaning up the tactic string. Reversing the order of those operations seems to fix it.

Add some new snippets and make the emacs mode use company mode if present to easier expand snippets

Add new yasnippets folder to tools, edit emacs mode to load snippets if yasnippet package is installed

Fix emacs mode in light of c3f12a32ec

fixed wrong number of arguments when calling copy-region-as-hol-definition-quietly

hol-mode: fix copy-region-as-hol-definition-quietly

In commit d3c3a92e60b29c5c32a23c9080a7315ae347c0fd the prefix argument
of copy-region-as-hol-definition-quietly. This is very sensible, but
afterwards copy-region-as-hol-definition-quietly could not be used
interactively any more, since the interactive code was not adapted. This
commit fixes it.

Correct bug in hol-with-region's completing-read

Work on #421

Remove elisp doc string mentioning nicenice argument to hol

Remove niceness argument to hol starter functions

I have not used this option since about 2000, and I don't imagine
anyone else has ever used it at all. It was never admitted to outside
of the elisp documentation strings and the hol-horizontal and
hol-vertical commands did not set it or use it either.

Implement "start HOL with region/buffer" functionality in emacs mode

Function is bound to M-h H.

Also correct spelling mistake: "quitely" --> "quietly", in various
elisp function names.

Closes #421

hol-mode: add menu entries for showing tags and axioms

Fix Emacs HOL mode to work with new by

Progress with issue #407

hol-mode: add hol-print-info

I recently have the problem on various machines, that have multiple
copies of HOL installed, to figure out which version is started by hol-
mode. I did this by looking at the value of HOLDIR, the current load
paths etc in ML and the used hol and holmake executables in Lisp. To
simplify this process of looking up these values, this commit adds this
functionality to hol-mode.

emacs mode: provide support for de-Unicode-ify

There is a new command `hol-remove-unicode` now that replaces commonly
used unicode symbols with their ASCII counterpart. It can be found in
the menu as "HOL / Misc / Replace common HOL unicode symbols". If a
region is selected, it operates only on this region, otherwise on the
whole buffer.

Currently the most common unicode symbols are replaced. Probably a few
more need adding in time. This should be straightforward by updating the
list "hol-unicode-replacements".

hol-mode: toggle pretty printing of cases extended for pmatch cases

Now the menu item "HOL/Printing Switches/Toggle pretty-printing of
cases" toggles the pretty printing of PMATCH case expression in addition
to the already existing behavior of toggling the printing of decision
tree case expressions.

holmode: add support for hol.bare

I got tired of having to set the HOL executable to hol.bare manually in
the emacs HOL mode when working on theories that are build before
bossLib. This commit changes holmode to add an option for appending
".bare" to the hol-executable to the HOL-process menu.

Improve handling of Unicode quotes in emacs mode

Make Emacs hol-mode handle “..” as well as ‘..’

Closes #370

address issue #370

I hope this commit addresses issue #370. Now HOL-mode should support
unicode quotation marks.

Add "termination goal" to g/stack menu in hol-mode

Improve tactic selection/movement in emacs mode

Also add new "execute the next tactic" binding on M-h M-e, which
"automagically" selects the next tactic from the source buffer, and
applies it. If the next tactic is, say, a parenthesised argument to
>-/THEN1, it will select all of it. To step into such a tactic, the
user has to manually move the cursor into the sexp.

Revert "Tidy up emacs code for filtering HOL output"

This reverts commit a593c230f3327e1c1eee92a9e63ef6166ec936b4.

Also add a comment explaining why the solution in a593c23 (with
with-temp-buffer) can't work.

Tidy up emacs code for filtering HOL output

It's hard to test this code systematically

Pretty-printer now annotates consts with their real names and types.

In "complicated" overload situations, such as the overloads for NOTIN
and <>, the annotation can't point to a "real" underlying constant,
but does still provide the type for the emacs tool-tips.

In passing, also create a new annotation form, the SymConst as well as
the Const. This is done for the TeX backend's benefit, so that it can
avoid treating things like + the same as normal identifiers. This
works well for math-mode munging where you want "+" to map to $+$, but
want "INSERT" to map to \textsf{INSERT}.

Closes #39

Make subgoal function in emacs mode Raise exceptions

Bug-fix for change to hol-subgoal-tactic.

Now behaviour is correct (had to test "raw" prefix argument for nil).

Emacs hol-subgoal-tactic now emulates "suffices_by" as well as "by"

Get the suffices_by effect by using a prefix argument, i.e., by
pressing C-u before invoking it. Thus, C-u M-h M-s will give you
"suffices_by", and M-h M-s will give you "by" (as before).

hol-mode now strips \\ instead of //

Change the template introduced by the emacs-mode for Datatype declarations.

This makes the mode use the syntax introduced in b4161465b.

Add // as an lcsymtacs alias for THEN; fix hol-mode bug in handling of THEN1

Fix bug in emacs mode's handling of open thyname.

Problem arose if the thyname included the string "_fun_".
Thanks to Magnus for the bug report.

You will need to do a fresh ML < tools/smart-configure.sml
to get the new version of the Emacs mode created.

Stop emacs-mode causing an extra Raise when applying a tactic.

The e and expandf functions in the proof manager already do a Raise as
it is.

New goalstack pretty-printing trace & rationalise goalstack trace names

New trace prints a count of the sub-goals at the end of the stack.
This saves the user from having to scroll back over the several
hundred goals they've just generated to find out the number.

Remove hol-begin-theory (from 0a0b0b0) as same functionality already exists.

See hol-template-new-script-file or the Templates sub-menu of the HOL
menu.

Remove existing template’s leading blank lines.

Thanks to Magnus for pointing out the duplication.

Write a hol-mode function to insert standard HOL theory template.

Make it easier to start a function termination proof from emacs

added pp_cases to emacs-mode

Add function to hol-mode for printing a region and preserving its Unicode

Thanks to Dan Synek for the suggestion and most of the code.

Fix for hol-mode's use of temporary files under Windows.

Bug reported by Joseph Chan.

Adjust hol-subgoal-tactic so that it handles chained equalities better.

In particular, it is legitimate to do

`_ = newrhs` by foo

to get chained equality reasoning (the rhs of the top assumption gets
inserted into the _ position, and the top assumption is chained with
the result to give oldlhs = newrhs as the new top assumption).

This didn't use to work with the HOL-mode properly though because it
didn't apply "by" to the text, but rather Q.SUBGOAL_THEN.

Slight tweak to tactic-connective regexp in hol-mode.

Template fixed.

Add THEN-stripping feature suggested by Magnus Myreen (inspired by vim-mode).

This will cause tactic-sending in the emacs mode to ignore leading or trailing
instances of things like THEN, THENL as well as parentheses typically
associated with these. For example, all of the line
SRW_TAC [][] THEN1 (
could be highlighted, and only the SRW_TAC [][] would be sent.

added support for setting the maximum number of shown subgoals when printing a goalstack

added support for Sanity

incorporate the renaming of BBackup to restore and save_proof to save in proofManagerLib

Support for the new user-backup system added.

adaption to renaming of trace "emacs terminal show types" into "PPBackEnd show types"

Apply bits of Thomas's last Emacs mode update (7597) that are OK.

Revert "Added support for calling Holmake to hol-mode. Moreover, ..."

This undows commit 7597, which (unintentionally) undid changes of mine
in 7498. I will re-apply those parts of 7597 that are not broken in a
follow-up.

Added support for calling Holmake to hol-mode. Moreover, some more key-combinations were added.

Allow the Emacs mode command hol-recentre to also raise the HOL frame.

An automatic call to raise-frame used to be the default. However, the
default now is still not to raise the frame, but this can be
changed by adjusting the customisable variable hol-raise-on-recentre.

Added missing functions "hol-toggle-pp-styles" and "hol-toggle-pp-annotations".

Moreover, there is a problem with output filtering, if a pretty-printer opens
a style with begin_style and never closes it in hol-mode. In this case, emacs waits forever
for the closing and stops printing. A menu option was added to reset the
hol-mode printing in this case.

hol-mode that can handle the new pretty-printing styles

Support for turning tool-tips off was added to the emacs-mode. This reflects recent changes to pretty-printing and PPBackEnd.

A "Clean up" command was added (HOL - Misc - Clean up). This command replaces tabs with spaces. Thereby it pays attantion to the current tab-width and the column the tab occurs. As a result, the optical appearence of the file should not change. Moreover whitespaces at the end of lines and empty lines at the end of the buffer are removed.

Changed hol-mode.src so that in Emacs the color for types is slightly darker than before (cyan3 instead of cyan). This makes type information more visible on a light background, so that it does not become hard to read compared with term information. The vt100 windows color for types is still cyan, as the vt100's palette is more restricted, but this is OK because for some reason in terminal windows the cyan is more visible in practice.

Changed hol-mode.src and src/parse/PPBackEnd.sml so that type variables are displayed in purple.

"Everybody's cute... Everybody's cute, even me. But in purple, I'm STUNNING!"
(Centauri Ambassador Londo Molari, Babylon 5, The Parliament of Dreams)

Changed hol-mode.src again, so that in Emacs the colors for types are the same (cyan) as in the terminal windows. Had left out that this only works for color displays.

Changed hol-mode.src so that in Emacs the colors for types are the same (cyan) as in the terminal windows.

Link the type pretty-printer to the PPBackEnd infrastructure. In
Emacs, types are printed in italics, with tooltips indicating the real
nature of the underlying thing (type abbreviations supported).

Make some minor changes to the HOL/emacs link in response to issues
identified by Thomas (who is using an older version of emacs than I
am). Along the way, allow people not using the hol-mode, but still
using hol within emacs, to continue doing so straightforwardly.

Get rid of some unneeded stuff that also makes the customize interface
for the hol faces get grungy.

Emacs HOL mode: now has a customisation group. If you do M-x
customize, and then select External/Hol, you will get the standard
emacs interface for changing some bits and pieces. Also add the
ppbackend toggle to the HOL menu. (This HOL menu should really only
appear above relevant buffers, not all the time.)

Some fixes and a new feature for the Emacs pp backend: variables now
display their types when you hover your mouse over them. Adding this
information can make calls to open rather slow. In those situations,
I recommend not having any output at all (C-u M-h o, or C-u C-u M-h
M-r), or putting the terminal into "raw" mode (M-h C-p).

There are still some "minor problems" with this, but it mainly looks
reasonable. It now also loads correctly when you start emacs. In
order to get your system to do the right thing, you will need to
reconfigure HOL in order to get a fresh hol-mode.el file, and then you
will also have to restart your emacs.

Preliminary check-in to get colouring of variables in emacs. You
will have to start your emacs with the hol-mode command in order to
avoid seeing lots of horrible gibberish in your output.
Alternatively, start it in a *shell* as you are used to, and then do
current_backend := PPBackEnd.raw_terminal

Magnus and I removed the output filter from the emacs HOL-mode. The output filter was making printing slow.

Also, we added some ML code that will make the auto-load feature not attempt to load standard structures that are already by default loaded, e.g. String, TextIO etc.

Magnus and I added the possibility to throw away all HOL-output (including errors and warnings) inside emacs. This may sound dangerous and useless, since quitedec/interactive turns off all output except warnings and errors. However, it is useful internally sometimes. For example we hide the installation of some auxiliary ml-functions at startup using this method.

Nevertheless, a menu-entry was added to send a region to HOL and ignore all output. For completeness, a command was added as well, that toggles quitedec, sends the region and the toggles it back. Both commands might be useful when opening theories or libraries. The second one usually sends the region and just shows warnings and errors. Depending on the library / theory one is loading there might be a lot of warnings (incomplete pattern matching, free type variables etc). The first command ignores these warnings/errors as well.

Removed an occurence of (raise-frame) which made
emacs constantly pop up when minimized.

A function was added to easily get information about the type of a term. Now by pressing M-h i one gets typing information about a marked term
- without context
- in the context of the surrounding term and
- in the context of the current goal.

Magnus and I added some functions to show and modify the current load-path. Also, hopefully Michael's problem is fixed now.

If there is a type-checking error inside a tactic that the HOL mode is
sending to HOL, then ensure it only gets reported once. (The default
state is for the parser to use Raise, but the hol-mode also calls
Raise at the top-level, so we set a flag to turn the inner Raise off.)

I fixed a bug in the output filter. Sometimes, output was thrown away without being printed.

Minor fix to the emacs HOL mode: now the new recentre option
also works in the Mac version of emacs (Carbon emacs).

For constructs like "val name1 = store_thm ("name2", ...)" it is important that name1 and name2 are equal. However, at least I have frequently typos in one of them, especially name2. I added some functionality to search and fix those mismatches.

Moreover I added the possibility to have feedback from HOL to the current buffer. Now, one can
- insert a list of ALL_TAC corresponding to the number of current subgoals
- insert the current goal or
- insert an assumption.

We added a flag that allows to turn off the automatic loading of libraries. Moreover, a menu entry for changing the HOL-executable and one for echoing commands were added.

Magnus and I added a new mode to recentering the HOL-buffer. Now it can be centered on top of the last result sent by HOL as well as the bottom. This might be useful when working with goalstack. Moreover some simplifications for starting HOL were added. Now the window can automatically be split horizontally or vertically when starting HOL. Moreover, there are some changes in the styles of the comments and some other very minor changes.

Added keyboard shortcut for DB.find: M-h f

Magnus and I have added a "HOL" menu to the emacs HOL mode. This new menu, which is at the top of emacs windows, lists all of the HOL mode commands. Thus, people don't need to memorise the key combinations, instead the mouse can be used to select commands from the drop down menu.

We also added a few new commands to the HOL mode: Kill HOL and templates for creating a new theory file, definition, data-type definition, and various styles of comments.

Added support for the traces "goalstack print goal at top" (M-h C-o) and "goalstack number of assums" (M-h M-a) that have recently been added to control how goals are displayed.

Make the Emacs mode quietness feature also toggle Globals.interactive.

Fix a bug by putting the equivalent of a null-exception handler around
the call to delete the previous temporary file. Without it, emacs
would get its knickers in a twist if it thought there was a file but
there wasn't. When the call to delete-file failed, the whole function
would exit with an error, and the variable recording the previous
file's name would stay unchanged.

Couple of parse message fixes:
* when doing a parse-in-context, don't automatically "say" errors.
Now only do it if the "report type errors" trace allows.
* The set_goal command in the emacs mode doesn't need to Raise any
exceptions (doing so causes type error messages to be printed
twice).

Add a command to the Emacs mode (M-h C-u) to toggle "Unicode mode".

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Final bit of fussing with quiet declarations.

Realised that putting the quietdec thing into Systeml wouldn't work in
Moscow ML because this code needs compiling and you can't compile
references to the Meta structure. So, I just put it into the
respective prelude files.

Put a toggle_quietdec function into the Systeml structure, allowing a
common interface to be relied on by the emacs mode.

Added proofManagerLib. This adds a type of "goal trees"
as an alternative to goalstacks. Relevant entrypoints:

gt ` .... ` -- start a goaltree proof,
analogous to g
eq ` ... ` -- expand a tactic,
analogous to e (except that
the text of the tactic is
delimited by quotes).

A goaltree manages the construction of the final
tactic, so should ease some of the script maintenance
that the goalstack requires.

Backup and restart are just as for goalstacks.

All the entrypoints for goalstacks are just as they
were before; there shouldn't be any difference.

Remove the race condition between 'use'-ing the temporary file and
deleting it by having the name of the temporary stored in a variable
and deleted the next time the send-region-to-hol function is called.

Aditi Barthwal pointed out that using temp files and not deleting them
can fill up small root partitions.

Remove one of the last remaining vestiges of "hol98"; in the Emacs mode.