Custom Query (361 matches)

I’m on Mac OS 10.10.2 (Yosemite), trying to build Proof General 4.2, for Aquamacs 3.2 (based on Emacs 24.4). Running make clean; make compile EMACS=/Applications/Aquamacs.app/Contents/MacOS/Aquamacs fails with the error cascade

In toplevel form:
isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined.
make[1]: *** [isar/isar-unicode-tokens.elc] Error 1
make: *** [compile] Error 2

Full make output at ​https://gist.github.com/peterlefanulumsdaine/92c49ce941018b594891

I have a problem in a byte compilation of 'Proof General 3.7.1' with emacs-22.1.50 on Mac OS X 10.5.5.

'make compile' failed with an error:

In toplevel form: generic/pg-user.el:24:13:Error: Invalid read syntax: "#" make[2]: * [generic/pg-user.elc] Error 1 make[1]: * [.byte-compile] Error 2 make: * [compile] Error 2

when my completion file (~/.completion) has commented-out lines starting with "#". The compilation was successfully completed after removing the comments in the file.

When I use proof general with Isabelle, the "Isabelle/Show? me .../Facts" menu says "C-c C-a <h> <f>" next to it, but after typing just "ctrl-c ctrl-a h" emacs says "C-c C-a h is undefined".

I have 3.7.1.1.