Shell session transcript for reporting Proof General issue

ProofGeneral-isar-markup-ml-issue.txt

Peter-LeFanu-Lumsdaines-MacBook:ProofGeneral-4.2 peterlefanulumsdaine$ make clean; make compile EMACS=/Applications/Aquamacs.app/Contents/MacOS/Aquamacs
rm -f acl2/acl2.elc ccc/ccc.elc coq/coq-abbrev.elc coq/coq-autotest.elc coq/coq-db.elc coq/coq-indent.elc coq/coq-local-vars.elc coq/coq-mmm.elc coq/coq-smie-lexer.elc coq/coq-syntax.elc coq/coq-unicode-tokens.elc coq/coq.elc hol98/hol98.elc isar/interface-setup.elc isar/isabelle-system.elc isar/isar-autotest.elc isar/isar-find-theorems.elc isar/isar-keywords.elc isar/isar-mmm.elc isar/isar-profiling.elc isar/isar-syntax.elc isar/isar-unicode-tokens.elc isar/isar.elc lego/lego-syntax.elc lego/lego.elc hol-light/hol-light-autotest.elc hol-light/hol-light-unicode-tokens.elc hol-light/hol-light.elc phox/phox-extraction.elc phox/phox-font.elc phox/phox-fun.elc phox/phox-lang.elc phox/phox-outline.elc phox/phox-pbrpm.elc phox/phox-sym-lock.elc phox/phox-tags.elc phox/phox.elc pgshell/pgshell.elc pgocaml/pgocaml.elc pghaskell/pghashell.elc pghaskell/pghaskell.elc generic/pg-assoc.elc generic/pg-autotest.elc generic/pg-custom.elc generic/pg-goals.elc generic/pg-movie.elc generic/pg-pamacs.elc generic/pg-pbrpm.elc generic/pg-pgip.elc generic/pg-response.elc generic/pg-user.elc generic/pg-vars.elc generic/pg-xml.elc generic/proof-autoloads.elc generic/proof-auxmodes.elc generic/proof-config.elc generic/proof-depends.elc generic/proof-easy-config.elc generic/proof-faces.elc generic/proof-indent.elc generic/proof-maths-menu.elc generic/proof-menu.elc generic/proof-mmm.elc generic/proof-script.elc generic/proof-shell.elc generic/proof-site.elc generic/proof-splash.elc generic/proof-syntax.elc generic/proof-toolbar.elc generic/proof-tree.elc generic/proof-unicode-tokens.elc generic/proof-useropts.elc generic/proof-utils.elc generic/proof.elc lib/bufhist.elc lib/holes.elc lib/local-vars-list.elc lib/maths-menu.elc lib/pg-dev.elc lib/pg-fontsets.elc lib/proof-compat.elc lib/scomint.elc lib/span.elc lib/texi-docstring-magic.elc lib/unicode-chars.elc lib/unicode-tokens.elc contrib/mmm/mmm-auto.elc contrib/mmm/mmm-class.elc contrib/mmm/mmm-cmds.elc contrib/mmm/mmm-compat.elc contrib/mmm/mmm-cweb.elc contrib/mmm/mmm-mason.elc contrib/mmm/mmm-mode.elc contrib/mmm/mmm-region.elc contrib/mmm/mmm-rpm.elc contrib/mmm/mmm-sample.elc contrib/mmm/mmm-univ.elc contrib/mmm/mmm-utils.elc contrib/mmm/mmm-vars.elc *~ */*~ .\#* */.\#* */.autotest.log */.profile.log
(cd doc; /Applications/Xcode.app/Contents/Developer/usr/bin/make clean)
/Applications/Xcode.app/Contents/Developer/usr/bin/make -f Makefile.doc DOCNAME=PG-adapting MAKE="/Applications/Xcode.app/Contents/Developer/usr/bin/make -f Makefile.doc" clean
rm -f PG-adapting.cp PG-adapting.fn PG-adapting.vr PG-adapting.tp PG-adapting.ky PG-adapting.kys PG-adapting.pg PG-adapting.fns PG-adapting.vrs PG-adapting.cps PG-adapting.aux PG-adapting.log PG-adapting.cp PG-adapting.cp0 PG-adapting.toc
rm -f *~
/Applications/Xcode.app/Contents/Developer/usr/bin/make -f Makefile.doc DOCNAME=ProofGeneral MAKE="/Applications/Xcode.app/Contents/Developer/usr/bin/make -f Makefile.doc" clean 
rm -f ProofGeneral.cp ProofGeneral.fn ProofGeneral.vr ProofGeneral.tp ProofGeneral.ky ProofGeneral.kys ProofGeneral.pg ProofGeneral.fns ProofGeneral.vrs ProofGeneral.cps ProofGeneral.aux ProofGeneral.log ProofGeneral.cp ProofGeneral.cp0 ProofGeneral.toc
rm -f *~
****************************************************************
 Byte compiling... 
****************************************************************
/Applications/Xcode.app/Contents/Developer/usr/bin/make elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile acl2/acl2.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/acl2/acl2.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile ccc/ccc.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/ccc/ccc.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-abbrev.el
Warning: Eager macro-expansion skipped due to cycle:
  … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el")
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-abbrev.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-autotest.el
Warning: Eager macro-expansion skipped due to cycle:
  … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el")
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-autotest.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-db.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-db.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-indent.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-indent.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-local-vars.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-local-vars.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-mmm.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-mmm.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-smie-lexer.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-smie-lexer.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-syntax.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-syntax.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq-unicode-tokens.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq-unicode-tokens.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile coq/coq.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/coq/coq.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile hol98/hol98.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/hol98/hol98.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/interface-setup.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/isar/interface-setup.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isabelle-system.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/isar/isabelle-system.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isar-autotest.el
Warning: Eager macro-expansion skipped due to cycle:
  … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el")
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/isar/isar-autotest.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isar-find-theorems.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/isar/isar-find-theorems.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isar-keywords.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/isar/isar-keywords.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isar-mmm.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/isar/isar-mmm.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isar-profiling.el
Warning: Eager macro-expansion skipped due to cycle:
  … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el")
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/isar/isar-profiling.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isar-syntax.el
Wrote /Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/isar/isar-syntax.elc
/Applications/Aquamacs.app/Contents/MacOS/Aquamacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/Users/peterlefanulumsdaine/Library/Application Support/Aquamacs Emacs/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile isar/isar-unicode-tokens.el

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
Peter-LeFanu-Lumsdaines-MacBook:ProofGeneral-4.2 peterlefanulumsdaine$ make clean; make compile EMACS=/Applications/Aquamacs.app/Contents/MacOS/Aquamacs