Custom Query (361 matches)

Init order in proof-shell-start is tricky, because the shell mode sets some configuration variables at the same time as the process is being fired up (and the proof-shell-config-done sends startup commands to the prover!).

This could be made cleaner by (1) creating the shell buffer and setting its mode first (including filter functions), then (2) firing up the comint process inside it, then finally (3) sending initialisation messages. It looks like the current comint interface would allow this to work correctly for derived modes, which may have been a problem in earlier versions.

Several places, e.g.:

• Compatibility with the standard Coq Windows distribution (currently there are path problems, as well as much use of shell-command-to-string in coq.el).

• The unthinkable: easy Isabelle on Windows? Easy X-Symbol there?

• Remove use of so many window-system strings in proof-face-specs; just default to simple and standard defface settings (also improves behaviour in custom where lisp is sometimes seen). Are settings really needed for light/dark/terminal, doesn't everyone use light nowadays? The dark ones may customise themselves...

X-Symbol in Emacs 23 is disabled in PG 3.7 because of breakage due to API changes in fontset.el.

This may be relatively easy to fix: I've committed a partial attempt which now works for X Symbol font but not the ordinary symbol font for some reason. Looks pretty awful next to antialised Xft rendered characters, of course.

NB: although the X-Symbol menu option is disabled in Emacs 23, you can still issue M-x proof-x-symbol-toggle to turn it on in the normal way.