Many compatibility updates, bug fixes, rearrangements for compilation.

32 files changed, 2272 insertions, 2411 deletions

diff --git a/Makefile b/Makefile
index f2f6beda..f6637625 100644
--- a/Makefile
+++ b/Makefile
@@ -38,7 +38,7 @@ DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README.* REGISTER d
 DOC_EXAMPLES=acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
 DOC_SUBDIRS=${DOC_EXAMPLES} */README.* */CHANGES */BUGS 
 
-BATCHEMACS=${EMACS} -batch -q -no-site-file
+BATCHEMACS=${EMACS} --batch --no-site-file -q 
 
 # Scripts to edit paths to shells
 BASH_SCRIPTS = isar/interface bin/proofgeneral
@@ -64,39 +64,39 @@ default: all
 FORCE:
 
 ## 
-## compile : byte compile files in working directory:
-##           Clearout old .elc's and re-compile in a
-##           single Emacs process.  This is faster than "make elc",
-##	     but can have artefacts because of context between
-##	     compiles.
+## compile : byte compile all lisp files
+##           If EMACS variable has changed since last call, clearout 
+##	     old .elc's and re-compile.
 ##
-compile: .byte-compile
-	lastemacs=`cat .byte-compile`; if [ "$$lastemacs" != "$(EMACS)" ]; then rm -f .byte-compile; make .byte-compile; fi
+compile: $(EL) x-symbol/lisp/*.el
+	lastemacs=`cat .byte-compile 2>/dev/null || echo `; if [ "$$lastemacs" != "" ] && [ "$$lastemacs" != "$(EMACS)" ]; then rm -f .byte-compile $(ELC) x-symbol/lisp/*.elc; fi
+	make .byte-compile
 
 ## Compiling can show up errors in the code, but be wary of fixing obsoletion
-## warnings unless they're valid for both Emacsen.
+## or argument call warnings unless they're valid for both Emacsen.
 
 .byte-compile: $(EL) x-symbol/lisp/*.el
 	@echo "****************************************************************"
-	@echo " Byte compiling... IGNORING ERRORS FOR NOW; COMPILATION IS CURRENTLY BROKEN"
+	@echo " Byte compiling... "
 	@echo "****************************************************************"
-	rm -f $(ELC)
-#	$(BYTECOMP) $(EL)
 	make elc
 	@echo " Byte compiling X-Symbol..."
-	(cd x-symbol/lisp; rm -f *.elc; $(MAKE) EMACS="$(EMACS) -q -no-site-file")
+	(cd x-symbol/lisp; $(MAKE) EMACS="$(EMACS) -q -no-site-file")
 	echo $(EMACS) > $(@)
-	@echo "*************************************************"
+	@echo "****************************************************************"
 	@echo " Finished."
-	@echo "*************************************************"
+	@echo "****************************************************************"
 
 
 ##
-## Make individual .elc.  Building separately means we need to be careful
-## to add proper requires in source files.
+## Make an individual .elc.  Building separately means we need to be
+## careful to add proper requires in source files and prevent
+## evaluating/optimising top-level forms too early.  Using a separate
+## emacs process for each file is slower but avoids any chance of
+## accidently polluting the compilation environment.
 ##
 .el.elc:
-	-$(BYTECOMP) $*.el
+	$(BYTECOMP) $*.el
 
 elc:	$(ELC)
 
diff --git a/Makefile.devel b/Makefile.devel
index a6474798..f4f90766 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -167,7 +167,7 @@ ZIP=zip
 
 # Files not to include the distribution area or tarball 
 # FIXME: really this should be an opt-in list!
-UNFINISHED_ELISP=generic/pg-metadata.el generic/pg-xhhtml.el generic/_pkg.el
+UNFINISHED_ELISP=generic/pg-metadata.el generic/pg-xhhtml.el 
 ETC_FILES=etc/lego etc/coq etc/demoisa etc/isa etc/isar etc/lego etc/patches etc/pgkit etc/*.txt pgkit etc/Mailman
 NONDISTFILES=.cvsignore */.cvsignore Makefile.devel Makefile.xemacs doc/notes.txt doc/ProofGeneral.dvi doc/PG-adapting.dvi doc/ProofGeneral.jpg $(UNFINISHED_ELISP) $(ETC_FILES)
 
diff --git a/TAGS b/TAGS
index 33d89fda..a812c989 100644
--- a/TAGS
+++ b/TAGS
@@ -1,188 +1,190 @@
 
-coq/coq-abbrev.el,468
+coq/coq-abbrev.el,504
 (defun holes-show-doc 10,310
 (defun coq-local-vars-list-show-doc 14,387
 (defconst coq-tactics-menu 19,487
-(defconst coq-tactics-abbrev-table 24,636
-(defconst coq-tacticals-menu 27,724
-(defconst coq-tacticals-abbrev-table 32,879
-(defconst coq-commands-menu 36,972
-(defconst coq-commands-abbrev-table 42,1189
-(defconst coq-terms-menu 45,1279
-(defconst coq-terms-abbrev-table 50,1419
-(defpgdefault menu-entries 72,2197
-(defpgdefault help-menu-entries153,5618
+(defconst coq-tactics-abbrev-table 24,666
+(defconst coq-tacticals-menu 27,784
+(defconst coq-tacticals-abbrev-table 31,894
+(defconst coq-commands-menu 35,987
+(defconst coq-commands-abbrev-table 41,1204
+(defconst coq-terms-menu 44,1294
+(defconst coq-terms-abbrev-table 49,1434
+(defun coq-install-abbrevs 56,1629
+(defpgdefault menu-entries 75,2310
+(defpgdefault help-menu-entries156,5731
 
 coq/coq-db.el,559
-(defconst coq-syntax-db 22,519
-(defvar coq-user-tactics-db58,1892
-(defun coq-insert-from-db 68,2241
-(defun coq-build-regexp-list-from-db 86,3022
-(defun max-length-db 108,4075
-(defun coq-build-menu-from-db-internal 120,4350
-(defun coq-build-title-menu 155,5974
-(defun coq-sort-menu-entries 164,6342
-(defun coq-build-menu-from-db 167,6462
-(defun coq-build-abbrev-table-from-db 187,7233
-(defun filter-state-preserving 203,7787
-(defun filter-state-changing 208,7941
-(defface coq-solve-tactics-face 215,8162
-(defconst coq-solve-tactics-face 223,8424
-
-coq/coq.el,6050
-(defcustom coq-translate-to-v8 34,982
-(defcustom coq-compile-file-command 49,1471
-(defcustom coq-default-undo-limit 59,1840
-(defconst coq-shell-init-cmd 64,1968
-(defvar coq-utf-safe 73,2184
-(defcustom coq-prog-env 82,2600
-(defconst coq-shell-restart-cmd 90,2852
-(defvar coq-shell-prompt-pattern 97,3112
-(defvar coq-shell-cd 105,3441
-(defvar coq-shell-abort-goal-regexp 109,3596
-(defvar coq-shell-proof-completed-regexp 112,3722
-(defvar coq-goal-regexp115,3853
-(defun coq-library-directory 124,4042
-(defcustom coq-tags 131,4222
-(defconst coq-interrupt-regexp 136,4372
-(defcustom coq-www-home-page 141,4493
-(defvar coq-outline-regexp151,4664
-(defvar coq-outline-heading-end-regexp 158,4878
-(defvar coq-shell-outline-regexp 160,4932
-(defvar coq-shell-outline-heading-end-regexp 161,4982
-(defconst coq-kill-goal-command 166,5092
-(defconst coq-forget-id-command 167,5135
-(defconst coq-back-n-command 168,5182
-(defconst coq-state-preserving-tactics-regexp 172,5326
-(defconst coq-state-changing-commands-regexp174,5427
-(defconst coq-state-preserving-commands-regexp 176,5534
-(defconst coq-commands-regexp 178,5646
-(defvar coq-retractable-instruct-regexp 180,5724
-(defvar coq-non-retractable-instruct-regexp 182,5815
-(defvar coq-keywords-section186,5955
-(defvar coq-section-regexp 189,6049
-(defun coq-set-undo-limit 223,7149
-(defconst coq-keywords-decl-defn-regexp234,7588
-(defun coq-proof-mode-p 238,7738
-(defun coq-is-comment-or-proverprocp 249,8148
-(defun coq-is-goalsave-p 251,8252
-(defun coq-is-module-equal-p 252,8327
-(defun coq-is-def-p 255,8523
-(defun coq-is-decl-defn-p 257,8631
-(defun coq-state-preserving-command-p 262,8798
-(defun coq-command-p 265,8932
-(defun coq-state-preserving-tactic-p 268,9032
-(defun coq-state-changing-tactic-p 273,9180
-(defun coq-state-changing-command-p 280,9414
-(defun coq-section-or-module-start-p 287,9760
-(defun build-list-id-from-string 296,10001
-(defun coq-last-prompt-info 309,10531
-(defun coq-last-prompt-info-safe 321,11072
-(defvar coq-last-but-one-statenum 331,11587
-(defvar coq-last-but-one-proofnum 333,11654
-(defvar coq-last-but-one-proofstack 335,11717
-(defun coq-get-span-statenum 337,11759
-(defun coq-get-span-proofnum 342,11874
-(defun coq-get-span-proofstack 347,11989
-(defun coq-set-span-statenum 352,12133
-(defun coq-get-span-goalcmd 357,12264
-(defun coq-set-span-goalcmd 362,12378
-(defun coq-set-span-proofnum 367,12508
-(defun coq-set-span-proofstack 372,12639
-(defun proof-last-locked-span 377,12799
-(defun coq-set-state-infos 392,13403
-(defun count-not-intersection 432,15482
-(defun  coq-find-and-forget-v81 463,16736
-(defun coq-find-and-forget-v80 491,17868
-(defun coq-find-and-forget 586,22567
-(defvar coq-current-goal 599,23107
-(defun coq-goal-hyp 602,23172
-(defun coq-state-preserving-p 615,23605
-(defconst notation-print-kinds-table 630,24111
-(defun coq-PrintScope 634,24279
-(defun coq-guess-or-ask-for-string 653,24835
-(defun coq-ask-do 664,25220
-(defun coq-SearchIsos 673,25608
-(defun coq-SearchConstant 679,25841
-(defun coq-SearchRewrite 683,25934
-(defun coq-SearchAbout 687,26032
-(defun coq-Print 691,26124
-(defun coq-About 695,26246
-(defun coq-LocateConstant 699,26363
-(defun coq-LocateLibrary 705,26498
-(defun coq-addquotes 711,26648
-(defun coq-LocateNotation 713,26696
-(defun coq-Pwd 720,26895
-(defun coq-Inspect 726,27027
-(defun coq-PrintSection(730,27127
-(defun coq-Print-implicit 734,27221
-(defun coq-Check 739,27373
-(defun coq-Show 744,27483
-(defun coq-Compile 758,27928
-(defun coq-guess-command-line 772,28248
-(defun coq-pre-shell-start 794,29096
-(defun coq-mode-config 804,29545
-(defun coq-hybrid-ouput-goals-response-p 920,33755
-(defun coq-hybrid-ouput-goals-response 926,34013
-(defun coq-shell-mode-config 948,34925
-(defun coq-goals-mode-config 992,36996
-(defun coq-response-config 999,37228
-(defun coq-maybe-compile-buffer 1019,37934
-(defun coq-ancestors-of 1056,39468
-(defun coq-all-ancestors-of 1079,40435
-(defconst coq-require-command-regexp 1091,40828
-(defun coq-process-require-command 1096,41037
-(defun coq-included-children 1101,41164
-(defun coq-process-file 1122,42003
-(defpacustom print-fully-explicit 1147,42918
-(defpacustom print-implicit 1152,43067
-(defpacustom print-coercions 1157,43234
-(defpacustom print-match-wildcards 1162,43379
-(defpacustom print-elim-types 1167,43560
-(defpacustom printing-depth 1172,43727
-(defpacustom time-commands 1177,43889
-(defpacustom auto-compile-vos 1181,44000
-(defun coq-preprocessing 1201,44670
-(defun coq-fake-constant-markup 1216,45089
-(defun coq-create-span-menu 1238,45896
-(defconst module-kinds-table 1265,46698
-(defconst modtype-kinds-table1269,46848
-(defun coq-insert-section-or-module 1273,46977
-(defconst reqkinds-kinds-table1296,47837
-(defun coq-insert-requires 1301,47982
-(defun coq-end-Section 1317,48488
-(defun coq-insert-intros 1335,49072
-(defun coq-insert-match 1347,49596
-(defun coq-insert-tactic 1379,50774
-(defun coq-insert-tactical 1385,51013
-(defun coq-insert-command 1391,51262
-(defun coq-insert-term 1397,51506
-(define-key coq-keymap 1404,51704
-(define-key coq-keymap 1405,51762
-(define-key coq-keymap 1406,51819
-(define-key coq-keymap 1407,51888
-(define-key coq-keymap 1408,51944
-(define-key coq-keymap 1409,51993
-(define-key coq-keymap 1410,52051
-(define-key coq-keymap 1412,52112
-(define-key coq-keymap 1413,52171
-(define-key coq-keymap 1415,52235
-(define-key coq-keymap 1416,52295
-(define-key coq-keymap 1418,52351
-(define-key coq-keymap 1419,52401
-(define-key coq-keymap 1420,52451
-(define-key coq-keymap 1421,52501
-(define-key coq-keymap 1422,52555
-(define-key coq-keymap 1423,52614
-(defvar last-coq-error-location 1433,52797
-(defun coq-get-last-error-location 1442,53196
-(defun coq-highlight-error 1475,54593
-(defun coq-decide-highlight-error 1544,57278
-(defun coq-highlight-error-hook 1549,57440
-(defun first-word-of-buffer 1560,57833
-(defun coq-show-first-goal 1569,58064
-(defun is-not-split-vertic 1594,58953
-(defun optim-resp-windows 1603,59392
+(defconst coq-syntax-db 22,533
+(defvar coq-user-tactics-db58,1906
+(defun coq-insert-from-db 68,2255
+(defun coq-build-regexp-list-from-db 86,3036
+(defun max-length-db 108,4089
+(defun coq-build-menu-from-db-internal 120,4364
+(defun coq-build-title-menu 155,5988
+(defun coq-sort-menu-entries 164,6356
+(defun coq-build-menu-from-db 170,6486
+(defun coq-build-abbrev-table-from-db 192,7247
+(defun filter-state-preserving 209,7805
+(defun filter-state-changing 214,7959
+(defface coq-solve-tactics-face 221,8180
+(defconst coq-solve-tactics-face 229,8442
+
+coq/coq.el,6096
+(defcustom coq-translate-to-v8 37,1089
+(defun coq-build-prog-args 43,1269
+(defcustom coq-compile-file-command 56,1651
+(defcustom coq-default-undo-limit 66,2020
+(defconst coq-shell-init-cmd 71,2148
+(defvar coq-utf-safe 80,2364
+(defcustom coq-prog-env 89,2780
+(defconst coq-shell-restart-cmd 97,3032
+(defvar coq-shell-prompt-pattern 104,3292
+(defvar coq-shell-cd 112,3621
+(defvar coq-shell-abort-goal-regexp 116,3776
+(defvar coq-shell-proof-completed-regexp 119,3902
+(defvar coq-goal-regexp122,4054
+(defun coq-library-directory 131,4243
+(defcustom coq-tags 138,4423
+(defconst coq-interrupt-regexp 143,4573
+(defcustom coq-www-home-page 148,4694
+(defvar coq-outline-regexp158,4865
+(defvar coq-outline-heading-end-regexp 165,5079
+(defvar coq-shell-outline-regexp 167,5133
+(defvar coq-shell-outline-heading-end-regexp 168,5183
+(defconst coq-kill-goal-command 173,5293
+(defconst coq-forget-id-command 174,5336
+(defconst coq-back-n-command 175,5383
+(defconst coq-state-preserving-tactics-regexp 179,5527
+(defconst coq-state-changing-commands-regexp181,5628
+(defconst coq-state-preserving-commands-regexp 183,5735
+(defconst coq-commands-regexp 185,5847
+(defvar coq-retractable-instruct-regexp 187,5925
+(defvar coq-non-retractable-instruct-regexp 189,6016
+(defvar coq-keywords-section193,6156
+(defvar coq-section-regexp 196,6250
+(defun coq-set-undo-limit 230,7350
+(defconst coq-keywords-decl-defn-regexp241,7789
+(defun coq-proof-mode-p 245,7939
+(defun coq-is-comment-or-proverprocp 256,8347
+(defun coq-is-goalsave-p 258,8451
+(defun coq-is-module-equal-p 259,8526
+(defun coq-is-def-p 262,8722
+(defun coq-is-decl-defn-p 264,8830
+(defun coq-state-preserving-command-p 269,8997
+(defun coq-command-p 272,9131
+(defun coq-state-preserving-tactic-p 275,9231
+(defun coq-state-changing-tactic-p 280,9379
+(defun coq-state-changing-command-p 287,9613
+(defun coq-section-or-module-start-p 294,9959
+(defun build-list-id-from-string 303,10200
+(defun coq-last-prompt-info 316,10730
+(defun coq-last-prompt-info-safe 328,11271
+(defvar coq-last-but-one-statenum 338,11786
+(defvar coq-last-but-one-proofnum 340,11853
+(defvar coq-last-but-one-proofstack 342,11916
+(defun coq-get-span-statenum 344,11958
+(defun coq-get-span-proofnum 349,12073
+(defun coq-get-span-proofstack 354,12188
+(defun coq-set-span-statenum 359,12332
+(defun coq-get-span-goalcmd 364,12463
+(defun coq-set-span-goalcmd 369,12577
+(defun coq-set-span-proofnum 374,12707
+(defun coq-set-span-proofstack 379,12838
+(defun proof-last-locked-span 384,12998
+(defun coq-set-state-infos 399,13602
+(defun count-not-intersection 439,15681
+(defun  coq-find-and-forget-v81 470,16935
+(defun coq-find-and-forget-v80 498,18067
+(defun coq-find-and-forget 593,22766
+(defvar coq-current-goal 606,23306
+(defun coq-goal-hyp 609,23371
+(defun coq-state-preserving-p 622,23804
+(defconst notation-print-kinds-table 637,24310
+(defun coq-PrintScope 641,24478
+(defun coq-guess-or-ask-for-string 660,25034
+(defun coq-ask-do 671,25419
+(defun coq-SearchIsos 680,25807
+(defun coq-SearchConstant 686,26040
+(defun coq-SearchRewrite 690,26133
+(defun coq-SearchAbout 694,26231
+(defun coq-Print 698,26323
+(defun coq-About 702,26445
+(defun coq-LocateConstant 706,26562
+(defun coq-LocateLibrary 712,26697
+(defun coq-addquotes 718,26847
+(defun coq-LocateNotation 720,26895
+(defun coq-Pwd 727,27094
+(defun coq-Inspect 733,27226
+(defun coq-PrintSection(737,27326
+(defun coq-Print-implicit 741,27419
+(defun coq-Check 746,27570
+(defun coq-Show 751,27678
+(defun coq-Compile 765,28121
+(defun coq-guess-command-line 779,28441
+(defun coq-mode-config 800,29294
+(defun coq-hybrid-ouput-goals-response-p 913,33418
+(defun coq-hybrid-ouput-goals-response 919,33676
+(defun coq-shell-mode-config 941,34588
+(defun coq-goals-mode-config 985,36659
+(defun coq-response-config 992,36891
+(defun coq-maybe-compile-buffer 1012,37597
+(defun coq-ancestors-of 1049,39131
+(defun coq-all-ancestors-of 1072,40098
+(defconst coq-require-command-regexp 1084,40491
+(defun coq-process-require-command 1089,40700
+(defun coq-included-children 1094,40827
+(defun coq-process-file 1115,41666
+(defpacustom print-fully-explicit 1140,42581
+(defpacustom print-implicit 1145,42730
+(defpacustom print-coercions 1150,42897
+(defpacustom print-match-wildcards 1155,43042
+(defpacustom print-elim-types 1160,43223
+(defpacustom printing-depth 1165,43390
+(defpacustom time-commands 1170,43552
+(defpacustom auto-compile-vos 1174,43663
+(defun coq-preprocessing 1195,44405
+(defun coq-fake-constant-markup 1210,44824
+(defun coq-create-span-menu 1232,45631
+(defconst module-kinds-table 1259,46433
+(defconst modtype-kinds-table1263,46583
+(defun coq-insert-section-or-module 1267,46712
+(defconst reqkinds-kinds-table1290,47572
+(defun coq-insert-requires 1295,47717
+(defun coq-end-Section 1311,48223
+(defun coq-insert-intros 1329,48807
+(defun coq-insert-match 1341,49331
+(defun coq-insert-tactic 1373,50509
+(defun coq-insert-tactical 1379,50748
+(defun coq-insert-command 1385,50997
+(defun coq-insert-term 1391,51241
+(define-key coq-keymap 1398,51439
+(define-key coq-keymap 1399,51497
+(define-key coq-keymap 1400,51554
+(define-key coq-keymap 1401,51623
+(define-key coq-keymap 1402,51679
+(define-key coq-keymap 1403,51728
+(define-key coq-keymap 1404,51786
+(define-key coq-keymap 1406,51847
+(define-key coq-keymap 1407,51906
+(define-key coq-keymap 1409,51970
+(define-key coq-keymap 1410,52030
+(define-key coq-keymap 1412,52086
+(define-key coq-keymap 1413,52136
+(define-key coq-keymap 1414,52186
+(define-key coq-keymap 1415,52236
+(define-key coq-keymap 1416,52290
+(define-key coq-keymap 1417,52349
+(defvar last-coq-error-location 1427,52532
+(defun coq-get-last-error-location 1436,52931
+(defun coq-highlight-error 1469,54328
+(defvar coq-allow-highlight-error 1534,56883
+(defun coq-decide-highlight-error 1540,57149
+(defun coq-highlight-error-hook 1545,57311
+(defun first-word-of-buffer 1556,57704
+(defun coq-show-first-goal 1565,57935
+(defun is-not-split-vertic 1590,58824
+(defun optim-resp-windows 1599,59263
 
 coq/coq-indent.el,2241
 (defconst coq-any-command-regexp11,262
@@ -247,8 +249,72 @@ coq/coq-local-vars.el,279
 (defun coq-ask-prog-name 133,5426
 (defun coq-ask-insert-coq-prog-name 148,6067
 
-coq/coq-syntax.el,33
-(defcustom coq-prog-name 12,355
+coq/coq-syntax.el,2572
+(defcustom coq-prog-name 12,357
+(defvar coq-version-is-V8 33,1303
+(defvar coq-version-is-V8-0 35,1382
+(defvar coq-version-is-V8-1 42,1760
+(defun coq-determine-version 51,2193
+(defcustom coq-user-tactics-db 96,4053
+(defcustom coq-user-commands-db 113,4566
+(defcustom coq-user-tacticals-db 129,5085
+(defcustom coq-user-solve-tactics-db 145,5606
+(defcustom coq-user-reserved-db 163,6127
+(defvar coq-tactics-db181,6658
+(defvar coq-solve-tactics-db336,14726
+(defvar coq-tacticals-db359,15524
+(defvar coq-decl-db384,16460
+(defvar coq-defn-db406,17678
+(defvar coq-goal-starters-db459,21664
+(defvar coq-commands-db485,23155
+(defvar coq-terms-db611,32442
+(defun coq-count-match 675,35094
+(defun coq-goal-command-str-v80-p 694,35957
+(defun coq-module-opening-p 717,36830
+(defun coq-section-command-p 728,37246
+(defun coq-goal-command-str-v81-p 732,37343
+(defun coq-goal-command-p-v81 747,38012
+(defun coq-goal-command-str-p 757,38352
+(defun coq-goal-command-p 767,38718
+(defvar coq-keywords-save-strict775,39030
+(defvar coq-keywords-save784,39143
+(defun coq-save-command-p 788,39221
+(defvar coq-keywords-kill-goal 797,39515
+(defvar coq-keywords-state-changing-misc-commands801,39606
+(defvar coq-keywords-goal804,39731
+(defvar coq-keywords-decl807,39814
+(defvar coq-keywords-defn810,39888
+(defvar coq-keywords-state-changing-commands814,39963
+(defvar coq-keywords-state-preserving-commands823,40224
+(defvar coq-keywords-commands828,40440
+(defvar coq-solve-tactics833,40589
+(defvar coq-tacticals837,40710
+(defvar coq-reserved843,40887
+(defvar coq-state-changing-tactics854,41216
+(defvar coq-state-preserving-tactics857,41325
+(defvar coq-tactics861,41439
+(defvar coq-retractable-instruct864,41528
+(defvar coq-non-retractable-instruct867,41638
+(defvar coq-keywords871,41766
+(defvar coq-symbols878,41934
+(defvar coq-error-regexp 897,42147
+(defvar coq-id 900,42375
+(defvar coq-id-shy 901,42400
+(defvar coq-ids 903,42454
+(defun coq-first-abstr-regexp 905,42495
+(defvar coq-font-lock-terms908,42591
+(defconst coq-save-command-regexp-strict926,43552
+(defconst coq-save-command-regexp930,43719
+(defconst coq-save-with-hole-regexp934,43872
+(defconst coq-goal-command-regexp938,44031
+(defconst coq-goal-with-hole-regexp941,44131
+(defconst coq-decl-with-hole-regexp945,44264
+(defconst coq-defn-with-hole-regexp949,44397
+(defconst coq-with-with-hole-regexp959,44686
+(defvar coq-font-lock-keywords-1965,44979
+(defvar coq-font-lock-keywords 989,46243
+(defun coq-init-syntax-table 991,46301
+(defconst coq-generic-expression1020,47200
 
 coq/x-symbol-coq.el,1746
 (defvar x-symbol-coq-required-fonts 16,384
@@ -289,85 +355,82 @@ coq/x-symbol-coq.el,1746
 (defvar x-symbol-coq-table468,14023
 (defcustom x-symbol-coq-auto-style475,14184
 
-demoisa/demoisa.el,390
+demoisa/demoisa.el,349
 (defcustom isabelledemo-prog-name 54,1809
 (defcustom isabelledemo-web-page59,1931
 (defun demoisa-config 70,2161
-(defun demoisa-shell-config 90,2910
-(define-derived-mode demoisa-mode 119,3994
-(define-derived-mode demoisa-shell-mode 124,4117
-(define-derived-mode demoisa-response-mode 129,4260
-(define-derived-mode demoisa-goals-mode 133,4387
-(defun demoisa-pre-shell-start 152,5169
-
-isar/isabelle-system.el,1446
-(defgroup isabelle 19,596
-(defcustom isabelle-web-page23,724
-(defcustom isa-isatool-command34,1019
-(defvar isatool-not-found 61,1964
-(defun isa-set-isatool-command 64,2077
-(defun isa-shell-command-to-string 84,2938
-(defun isa-getenv 90,3162
-(defcustom isabelle-program-name 109,3819
-(defvar isabelle-prog-name 135,4767
-(defun isabelle-command-line 138,4894
-(defun isabelle-choose-logic 162,5851
-(defun isa-tool-list-logics 184,6823
-(defun isa-view-doc 191,7061
-(defun isa-tool-list-docs 199,7286
-(defconst isabelle-verbatim-regexp 226,8319
-(defun isabelle-verbatim 229,8460
-(defcustom isabelle-refresh-logics 236,8616
-(defcustom isabelle-logics-available 244,8943
-(defcustom isabelle-chosen-logic 252,9243
-(defconst isabelle-docs-menu 265,9711
-(defun isabelle-logics-menu-calculate 275,10104
-(defvar isabelle-time-to-refresh-logics 291,10613
-(defun isabelle-logics-menu-refresh 294,10706
-(defun isabelle-logics-menu-filter 311,11405
-(defun isabelle-menu-bar-update-logics 317,11615
-(defvar isabelle-logics-menu-entries 328,11971
-(defvar isabelle-logics-menu 330,12043
-(defun isabelle-load-isar-keywords 343,12661
-(defpgdefault menu-entries364,13402
-(defpgdefault help-menu-entries 367,13454
-(defpgdefault x-symbol-language 375,13648
-(defun isabelle-convert-idmarkup-to-subterm 398,14263
-(defun isabelle-create-span-menu 422,15275
-(defun isabelle-xml-sml-escapes 438,15720
-(defun isabelle-process-pgip 441,15821
-
-isar/isar.el,1243
-(defcustom isar-keywords-name 28,580
-(defpgdefault completion-table 45,1104
-(defcustom isar-web-page47,1157
-(defun isar-strip-terminators 61,1494
-(defun isar-markup-ml 74,1871
-(defun isar-mode-config-set-variables 79,2006
-(defun isar-shell-mode-config-set-variables 144,5021
-(defun isar-remove-file 242,9190
-(defun isar-shell-compute-new-files-list 252,9553
-(defun isar-activate-scripting 263,10019
-(define-derived-mode isar-shell-mode 272,10189
-(define-derived-mode isar-response-mode 277,10312
-(define-derived-mode isar-goals-mode 282,10494
-(define-derived-mode isar-mode 287,10669
-(defpgdefault menu-entries341,12646
-(defun isar-count-undos 371,13885
-(defun isar-find-and-forget 398,15010
-(defun isar-goal-command-p 439,16593
-(defun isar-global-save-command-p 444,16765
-(defvar isar-current-goal 465,17610
-(defun isar-state-preserving-p 468,17676
-(defvar isar-shell-current-line-width 493,18835
-(defun isar-shell-adjust-line-width 499,19053
-(defun isar-pre-shell-start 519,19938
-(defun isar-preprocessing 531,20281
-(defun isar-mode-config 554,21547
-(defun isar-shell-mode-config 566,22117
-(defun isar-response-mode-config 577,22487
-(defun isar-goals-mode-config 586,22744
-(defun isar-goalhyplit-test 597,23090
+(defun demoisa-shell-config 91,2953
+(define-derived-mode demoisa-mode 117,3930
+(define-derived-mode demoisa-shell-mode 122,4053
+(define-derived-mode demoisa-response-mode 127,4196
+(define-derived-mode demoisa-goals-mode 131,4323
+
+isar/isabelle-system.el,1400
+(defgroup isabelle 24,731
+(defcustom isabelle-web-page28,859
+(defcustom isa-isatool-command39,1154
+(defvar isatool-not-found 66,2097
+(defun isa-set-isatool-command 69,2210
+(defun isa-shell-command-to-string 89,3071
+(defun isa-getenv 95,3295
+(defcustom isabelle-program-name114,3956
+(defvar isabelle-prog-name 140,4886
+(defun isabelle-command-line 143,5013
+(defun isabelle-choose-logic 167,5971
+(defun isa-tool-list-logics 189,6937
+(defun isa-view-doc 196,7174
+(defun isa-tool-list-docs 204,7399
+(defconst isabelle-verbatim-regexp 231,8431
+(defun isabelle-verbatim 234,8573
+(defcustom isabelle-refresh-logics 241,8734
+(defcustom isabelle-logics-available 249,9061
+(defcustom isabelle-chosen-logic 257,9361
+(defconst isabelle-docs-menu270,9829
+(defun isabelle-logics-menu-calculate 280,10221
+(defvar isabelle-time-to-refresh-logics 296,10728
+(defun isabelle-logics-menu-refresh 299,10822
+(defun isabelle-logics-menu-filter 316,11519
+(defun isabelle-menu-bar-update-logics 322,11729
+(defvar isabelle-logics-menu-entries 333,12068
+(defvar isabelle-logics-menu335,12140
+(defun isabelle-load-isar-keywords 348,12752
+(defpgdefault menu-entries369,13493
+(defpgdefault help-menu-entries 372,13545
+(defun isabelle-convert-idmarkup-to-subterm 400,14297
+(defun isabelle-create-span-menu 424,15308
+(defun isabelle-xml-sml-escapes 440,15750
+(defun isabelle-process-pgip 443,15851
+
+isar/isar.el,1204
+(defcustom isar-keywords-name 30,707
+(defpgdefault completion-table 47,1230
+(defcustom isar-web-page49,1283
+(defun isar-strip-terminators 63,1615
+(defun isar-markup-ml 76,1992
+(defun isar-mode-config-set-variables 81,2127
+(defun isar-shell-mode-config-set-variables 146,5142
+(defun isar-remove-file 244,9291
+(defun isar-shell-compute-new-files-list 254,9654
+(defun isar-activate-scripting 265,10120
+(define-derived-mode isar-shell-mode 274,10290
+(define-derived-mode isar-response-mode 279,10413
+(define-derived-mode isar-goals-mode 284,10595
+(define-derived-mode isar-mode 289,10770
+(defpgdefault menu-entries343,12742
+(defun isar-count-undos 373,13981
+(defun isar-find-and-forget 400,15095
+(defun isar-goal-command-p 439,16675
+(defun isar-global-save-command-p 444,16852
+(defvar isar-current-goal 465,17713
+(defun isar-state-preserving-p 468,17779
+(defvar isar-shell-current-line-width 492,18916
+(defun isar-shell-adjust-line-width 497,19108
+(defun isar-preprocessing 520,19999
+(defun isar-mode-config 543,21266
+(defun isar-shell-mode-config 554,21767
+(defun isar-response-mode-config 565,22126
+(defun isar-goals-mode-config 574,22376
+(defun isar-goalhyplit-test 585,22715
 
 isar/isar-find-theorems.el,778
 (defun isar-find-theorems-minibuffer 18,715
@@ -417,148 +480,147 @@ isar/isar-mmm.el,83
 (defconst isar-start-latex-regexp 23,697
 (defconst isar-start-sml-regexp 35,1130
 
-isar/isar-syntax.el,3471
+isar/isar-syntax.el,3470
 (defconst isar-script-syntax-table-entries18,433
-(defconst isar-script-syntax-table-alist59,1469
-(defun isar-init-syntax-table 68,1759
-(defun isar-init-output-syntax-table 76,2006
-(defconst isar-keyword-begin 92,2453
-(defconst isar-keyword-end 93,2491
-(defconst isar-keywords-theory-enclose95,2526
-(defconst isar-keywords-theory100,2671
-(defconst isar-keywords-save105,2816
-(defconst isar-keywords-proof-enclose110,2945
-(defconst isar-keywords-proof116,3127
-(defconst isar-keywords-proof-context123,3332
-(defconst isar-keywords-local-goal127,3446
-(defconst isar-keywords-proper131,3558
-(defconst isar-keywords-improper136,3691
-(defconst isar-keywords-outline141,3837
-(defconst isar-keywords-fume144,3902
-(defconst isar-keywords-indent-open151,4120
-(defconst isar-keywords-indent-close157,4304
-(defconst isar-keywords-indent-enclose161,4409
-(defun isar-regexp-simple-alt 170,4624
-(defun isar-ids-to-regexp 190,5384
-(defconst isar-ext-first 224,6790
-(defconst isar-ext-rest 225,6857
-(defconst isar-long-id-stuff 227,6929
-(defconst isar-id 228,7003
-(defconst isar-idx 229,7073
-(defconst isar-string 231,7132
-(defconst isar-any-command-regexp233,7192
-(defconst isar-name-regexp237,7326
-(defconst isar-improper-regexp243,7621
-(defconst isar-save-command-regexp247,7769
-(defconst isar-global-save-command-regexp250,7870
-(defconst isar-goal-command-regexp253,7984
-(defconst isar-local-goal-command-regexp256,8092
-(defconst isar-comment-start 259,8205
-(defconst isar-comment-end 260,8240
-(defconst isar-comment-start-regexp 261,8273
-(defconst isar-comment-end-regexp 262,8344
-(defconst isar-string-start-regexp 264,8412
-(defconst isar-string-end-regexp 265,8464
-(defconst isar-antiq-regexp274,8717
-(defconst isar-nesting-regexp281,8878
-(defun isar-nesting 284,8976
-(defun isar-match-nesting 296,9397
-(defface isabelle-class-name-face308,9728
-(defface isabelle-tfree-name-face318,10003
-(defface isabelle-tvar-name-face328,10284
-(defface isabelle-free-name-face338,10564
-(defface isabelle-bound-name-face348,10840
-(defface isabelle-var-name-face358,11119
-(defconst isabelle-class-name-face 368,11398
-(defconst isabelle-tfree-name-face 369,11460
-(defconst isabelle-tvar-name-face 370,11522
-(defconst isabelle-free-name-face 371,11583
-(defconst isabelle-bound-name-face 372,11644
-(defconst isabelle-var-name-face 373,11706
-(defconst isar-font-lock-local376,11768
-(defvar isar-font-lock-keywords-1381,11934
-(defvar isar-output-font-lock-keywords-1395,12800
-(defvar isar-goals-font-lock-keywords422,14424
-(defconst isar-undo 456,15103
-(defun isar-remove 458,15165
-(defun isar-undos 461,15240
-(defun isar-cannot-undo 465,15346
-(defconst isar-theory-start-regexp468,15416
-(defconst isar-end-regexp474,15581
-(defconst isar-undo-fail-regexp478,15682
-(defconst isar-undo-skip-regexp482,15786
-(defconst isar-undo-ignore-regexp485,15907
-(defconst isar-undo-remove-regexp488,15972
-(defconst isar-any-entity-regexp496,16147
-(defconst isar-named-entity-regexp501,16334
-(defconst isar-unnamed-entity-regexp506,16511
-(defconst isar-next-entity-regexps509,16613
-(defconst isar-generic-expression517,16924
-(defconst isar-indent-any-regexp528,17241
-(defconst isar-indent-inner-regexp530,17334
-(defconst isar-indent-enclose-regexp532,17400
-(defconst isar-indent-open-regexp534,17516
-(defconst isar-indent-close-regexp536,17626
-(defconst isar-outline-regexp542,17763
-(defconst isar-outline-heading-end-regexp 546,17916
-
-isar/x-symbol-isabelle.el,1922
-(defvar x-symbol-isabelle-required-fonts 20,624
-(defvar x-symbol-isabelle-name 28,1028
-(defvar x-symbol-isabelle-modeline-name 29,1078
-(defcustom x-symbol-isabelle-header-groups-alist 31,1126
-(defcustom x-symbol-isabelle-electric-ignore 38,1354
-(defvar x-symbol-isabelle-required-fonts 46,1610
-(defvar x-symbol-isabelle-extra-menu-items 49,1719
-(defvar x-symbol-isabelle-token-grammar53,1817
-(defun x-symbol-isabelle-token-list 60,2023
-(defvar x-symbol-isabelle-user-table 63,2112
-(defvar x-symbol-isabelle-generated-data 66,2233
-(defvar x-symbol-isabelle-master-directory 74,2476
-(defvar x-symbol-isabelle-image-searchpath 75,2529
-(defvar x-symbol-isabelle-image-cached-dirs 76,2581
-(defvar x-symbol-isabelle-image-file-truename-alist 77,2651
-(defvar x-symbol-isabelle-image-keywords 78,2708
-(defcustom x-symbol-isabelle-subscript-matcher 88,3052
-(defcustom x-symbol-isabelle-font-lock-regexp 94,3299
-(defcustom x-symbol-isabelle-font-lock-limit-regexp 99,3483
-(defcustom x-symbol-isabelle-font-lock-contents-regexp 105,3715
-(defcustom x-symbol-isabelle-single-char-regexp 115,4107
-(defun x-symbol-isabelle-subscript-matcher 121,4385
-(defun isabelle-match-subscript 163,6057
-(defvar x-symbol-isabelle-font-lock-keywords172,6452
-(defvar x-symbol-isabelle-font-lock-allowed-faces 179,6720
-(defcustom x-symbol-isabelle-class-alist186,6952
-(defcustom x-symbol-isabelle-class-face-alist 197,7377
-(defvar x-symbol-isabelle-case-insensitive 212,7905
-(defvar x-symbol-isabelle-token-shape 213,7953
-(defvar x-symbol-isabelle-input-token-ignore 214,7996
-(defvar x-symbol-isabelle-token-list 215,8046
-(defvar x-symbol-isabelle-symbol-table 217,8095
-(defvar x-symbol-isabelle-xsymbol-table 317,10831
-(defun x-symbol-isabelle-prepare-table 463,15265
-(defvar x-symbol-isabelle-table471,15465
-(defcustom x-symbol-isabelle-auto-style485,15818
-(defcustom x-symbol-isabelle-auto-coding-alist 499,16328
-
-lclam/lclam.el,563
+(defconst isar-script-syntax-table-alist59,1464
+(defun isar-init-syntax-table 68,1754
+(defun isar-init-output-syntax-table 76,2001
+(defconst isar-keyword-begin 92,2448
+(defconst isar-keyword-end 93,2486
+(defconst isar-keywords-theory-enclose95,2521
+(defconst isar-keywords-theory100,2666
+(defconst isar-keywords-save105,2811
+(defconst isar-keywords-proof-enclose110,2940
+(defconst isar-keywords-proof116,3122
+(defconst isar-keywords-proof-context123,3327
+(defconst isar-keywords-local-goal127,3441
+(defconst isar-keywords-proper131,3553
+(defconst isar-keywords-improper136,3686
+(defconst isar-keywords-outline141,3832
+(defconst isar-keywords-fume144,3897
+(defconst isar-keywords-indent-open151,4115
+(defconst isar-keywords-indent-close157,4299
+(defconst isar-keywords-indent-enclose161,4404
+(defun isar-regexp-simple-alt 170,4619
+(defun isar-ids-to-regexp 190,5379
+(defconst isar-ext-first 224,6785
+(defconst isar-ext-rest 225,6852
+(defconst isar-long-id-stuff 227,6924
+(defconst isar-id 228,6998
+(defconst isar-idx 229,7068
+(defconst isar-string 231,7127
+(defconst isar-any-command-regexp233,7187
+(defconst isar-name-regexp237,7321
+(defconst isar-improper-regexp243,7616
+(defconst isar-save-command-regexp247,7764
+(defconst isar-global-save-command-regexp250,7865
+(defconst isar-goal-command-regexp253,7979
+(defconst isar-local-goal-command-regexp256,8087
+(defconst isar-comment-start 259,8200
+(defconst isar-comment-end 260,8235
+(defconst isar-comment-start-regexp 261,8268
+(defconst isar-comment-end-regexp 262,8339
+(defconst isar-string-start-regexp 264,8407
+(defconst isar-string-end-regexp 265,8459
+(defconst isar-antiq-regexp274,8712
+(defconst isar-nesting-regexp281,8873
+(defun isar-nesting 284,8971
+(defun isar-match-nesting 296,9392
+(defface isabelle-class-name-face308,9723
+(defface isabelle-tfree-name-face318,9998
+(defface isabelle-tvar-name-face328,10279
+(defface isabelle-free-name-face338,10559
+(defface isabelle-bound-name-face348,10835
+(defface isabelle-var-name-face358,11114
+(defconst isabelle-class-name-face 368,11393
+(defconst isabelle-tfree-name-face 369,11455
+(defconst isabelle-tvar-name-face 370,11517
+(defconst isabelle-free-name-face 371,11578
+(defconst isabelle-bound-name-face 372,11639
+(defconst isabelle-var-name-face 373,11701
+(defconst isar-font-lock-local376,11763
+(defvar isar-font-lock-keywords-1381,11931
+(defvar isar-output-font-lock-keywords-1395,12797
+(defvar isar-goals-font-lock-keywords422,14421
+(defconst isar-undo 456,15100
+(defun isar-remove 458,15162
+(defun isar-undos 461,15237
+(defun isar-cannot-undo 465,15343
+(defconst isar-theory-start-regexp468,15413
+(defconst isar-end-regexp474,15578
+(defconst isar-undo-fail-regexp478,15679
+(defconst isar-undo-skip-regexp482,15783
+(defconst isar-undo-ignore-regexp485,15904
+(defconst isar-undo-remove-regexp488,15969
+(defconst isar-any-entity-regexp496,16144
+(defconst isar-named-entity-regexp501,16331
+(defconst isar-unnamed-entity-regexp506,16508
+(defconst isar-next-entity-regexps509,16610
+(defconst isar-generic-expression517,16921
+(defconst isar-indent-any-regexp528,17238
+(defconst isar-indent-inner-regexp530,17331
+(defconst isar-indent-enclose-regexp532,17397
+(defconst isar-indent-open-regexp534,17513
+(defconst isar-indent-close-regexp536,17623
+(defconst isar-outline-regexp542,17760
+(defconst isar-outline-heading-end-regexp 546,17913
+
+isar/x-symbol-isar.el,1774
+(defvar x-symbol-isar-required-fonts 12,429
+(defvar x-symbol-isar-name 20,829
+(defvar x-symbol-isar-modeline-name 21,875
+(defcustom x-symbol-isar-header-groups-alist 23,919
+(defcustom x-symbol-isar-electric-ignore 30,1139
+(defvar x-symbol-isar-required-fonts 38,1387
+(defvar x-symbol-isar-extra-menu-items 41,1492
+(defvar x-symbol-isar-token-grammar45,1586
+(defun x-symbol-isar-token-list 52,1784
+(defvar x-symbol-isar-user-table 55,1869
+(defvar x-symbol-isar-generated-data 58,1982
+(defvar x-symbol-isar-master-directory 66,2221
+(defvar x-symbol-isar-image-searchpath 67,2270
+(defvar x-symbol-isar-image-cached-dirs 68,2318
+(defvar x-symbol-isar-image-file-truename-alist 69,2384
+(defvar x-symbol-isar-image-keywords 70,2437
+(defcustom x-symbol-isar-subscript-matcher 80,2777
+(defcustom x-symbol-isar-font-lock-regexp 86,3012
+(defcustom x-symbol-isar-font-lock-limit-regexp 91,3188
+(defcustom x-symbol-isar-font-lock-contents-regexp 97,3412
+(defcustom x-symbol-isar-single-char-regexp 107,3796
+(defun x-symbol-isar-subscript-matcher 113,4066
+(defun isabelle-match-subscript 155,5718
+(defvar x-symbol-isar-font-lock-keywords164,6101
+(defvar x-symbol-isar-font-lock-allowed-faces 171,6361
+(defcustom x-symbol-isar-class-alist178,6589
+(defcustom x-symbol-isar-class-face-alist 189,7010
+(defvar x-symbol-isar-case-insensitive 204,7530
+(defvar x-symbol-isar-token-shape 205,7574
+(defvar x-symbol-isar-input-token-ignore 206,7613
+(defvar x-symbol-isar-token-list 207,7659
+(defvar x-symbol-isar-symbol-table 209,7704
+(defvar x-symbol-isar-xsymbol-table 309,10436
+(defun x-symbol-isar-prepare-table 455,14866
+(defvar x-symbol-isar-table463,15062
+(defcustom x-symbol-isar-auto-style477,15395
+(defcustom x-symbol-isar-auto-coding-alist 491,15897
+
+lclam/lclam.el,524
 (defcustom lclam-prog-name 15,385
 (defcustom lclam-web-page21,533
 (defun lclam-config 32,763
-(defun lclam-shell-config 52,1477
-(define-derived-mode lclam-proofscript-mode 72,2136
-(define-derived-mode lclam-shell-mode 77,2259
-(define-derived-mode lclam-response-mode 82,2393
-(define-derived-mode lclam-goals-mode 86,2516
-(defun lclam-mode 94,2744
-(defun lclam-pre-shell-start 107,3027
-(define-derived-mode thy-mode 141,3970
-(defvar thy-mode-map 144,4068
-(defun thy-add-menus 146,4095
-(defun process-thy-file 186,6009
-(defun update-thy-only 192,6210
-
-lego/lego.el,1766
+(defun lclam-shell-config 54,1557
+(define-derived-mode lclam-proofscript-mode 74,2216
+(define-derived-mode lclam-shell-mode 79,2339
+(define-derived-mode lclam-response-mode 84,2473
+(define-derived-mode lclam-goals-mode 88,2596
+(defun lclam-mode 96,2824
+(define-derived-mode thy-mode 133,3635
+(defvar thy-mode-map 136,3733
+(defun thy-add-menus 138,3760
+(defun process-thy-file 178,5674
+(defun update-thy-only 184,5875
+
+lego/lego.el,1727
 (defcustom lego-tags 19,493
 (defcustom lego-test-all-name 24,629
 (defpgdefault help-menu-entries30,787
@@ -591,17 +653,16 @@ lego/lego.el,1766
 (define-derived-mode lego-goals-mode 167,5271
 (defun lego-count-undos 178,5697
 (defun lego-goal-command-p 198,6516
-(defun lego-find-and-forget 203,6686
-(defun lego-goal-hyp 245,8522
-(defun lego-state-preserving-p 254,8720
-(defvar lego-shell-current-line-width 270,9423
-(defun lego-shell-adjust-line-width 278,9730
-(defun lego-pre-shell-start 297,10469
-(defun lego-mode-config 304,10666
-(defun lego-equal-module-filename 373,12764
-(defun lego-shell-compute-new-files-list 379,13039
-(defun lego-shell-mode-config 393,13565
-(defun lego-goals-mode-config 442,15501
+(defun lego-find-and-forget 203,6687
+(defun lego-goal-hyp 245,8523
+(defun lego-state-preserving-p 254,8721
+(defvar lego-shell-current-line-width 270,9424
+(defun lego-shell-adjust-line-width 278,9731
+(defun lego-mode-config 297,10470
+(defun lego-equal-module-filename 365,12497
+(defun lego-shell-compute-new-files-list 371,12772
+(defun lego-shell-mode-config 385,13298
+(defun lego-goals-mode-config 434,15234
 
 lego/lego-syntax.el,600
 (defconst lego-keywords-goal 15,358
@@ -621,25 +682,24 @@ lego/lego-syntax.el,600
 (defvar lego-font-lock-keywords-199,3667
 (defun lego-init-syntax-table 110,4134
 
-phox/phox.el,682
-(defcustom phox-prog-name 31,931
-(defcustom phox-sym-lock-enabled 36,1033
-(defcustom phox-web-page42,1140
-(defcustom phox-doc-dir 48,1290
-(defcustom phox-lib-dir 54,1438
-(defcustom phox-tags-program 60,1582
-(defcustom phox-tags-doc 66,1762
-(defcustom phox-etags 72,1900
-(defpgdefault menu-entries93,2352
-(defun phox-config 107,2545
-(defun phox-shell-config 153,4582
-(define-derived-mode phox-mode 178,5511
-(define-derived-mode phox-shell-mode 198,6123
-(define-derived-mode phox-response-mode 203,6251
-(define-derived-mode phox-goals-mode 215,6678
-(defun phox-pre-shell-start 243,7750
-(defpgdefault completion-table257,8264
-(defpgdefault x-symbol-language 265,8369
+phox/phox.el,644
+(defcustom phox-prog-name 31,907
+(defcustom phox-sym-lock-enabled 36,1009
+(defcustom phox-web-page42,1116
+(defcustom phox-doc-dir 48,1266
+(defcustom phox-lib-dir 54,1414
+(defcustom phox-tags-program 60,1558
+(defcustom phox-tags-doc 66,1738
+(defcustom phox-etags 72,1876
+(defpgdefault menu-entries93,2328
+(defun phox-config 107,2521
+(defun phox-shell-config 153,4558
+(define-derived-mode phox-mode 178,5487
+(define-derived-mode phox-shell-mode 198,6099
+(define-derived-mode phox-response-mode 203,6227
+(define-derived-mode phox-goals-mode 215,6654
+(defpgdefault completion-table240,7522
+(defpgdefault x-symbol-language 248,7627
 
 phox/phox-extraction.el,382
 (defvar phox-prog-orig 11,480
@@ -655,8 +715,8 @@ phox/phox-extraction.el,382
 
 phox/phox-font.el,123
 (defconst phox-font-lock-keywords6,282
-(defconst phox-sym-lock-keywords-table65,2406
-(defun phox-sym-lock-start 88,2980
+(defconst phox-sym-lock-keywords-table65,2401
+(defun phox-sym-lock-start 88,2975
 
 phox/phox-fun.el,679
 (defun phox-init-syntax-table 67,2392
@@ -706,153 +766,152 @@ phox/phox-pbrpm.el,512
 (defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
289,10739
 
 phox/phox-sym-lock.el,1353
-(defvar phox-sym-lock-sym-count 35,1696
-(defvar phox-sym-lock-ext-start 38,1766
-(defvar phox-sym-lock-ext-end 40,1888
-(defvar phox-sym-lock-font-size 43,2007
-(defvar phox-sym-lock-keywords 48,2197
-(defvar phox-sym-lock-enabled 53,2373
-(defvar phox-sym-lock-color 58,2535
-(defvar phox-sym-lock-mouse-face 63,2753
-(defvar phox-sym-lock-mouse-face-enabled 68,2943
-(defconst phox-sym-lock-with-mule 73,3133
-(defun phox-sym-lock-gen-symbol 76,3217
-(defun phox-sym-lock-make-symbols-atomic 84,3520
-(defun phox-sym-lock-compute-font-size 111,4462
-(defvar phox-sym-lock-font-name149,5882
-(defun phox-sym-lock-set-foreground 187,7167
-(defun phox-sym-lock-translate-char 201,7776
-(defun phox-sym-lock-translate-char-or-string 209,8044
-(defun phox-sym-lock-remap-face 216,8271
-(defvar phox-sym-lock-clear-face236,9261
-(defun phox-sym-lock 248,9683
-(defun phox-sym-lock-rec 257,10087
-(defun phox-sym-lock-atom-face 263,10240
-(defun phox-sym-lock-pre-idle-hook-first 268,10536
-(defun phox-sym-lock-pre-idle-hook-last 276,10894
-(defun phox-sym-lock-enable 285,11269
-(defun phox-sym-lock-disable 298,11682
-(defun phox-sym-lock-mouse-face-enable 311,12100
-(defun phox-sym-lock-mouse-face-disable 318,12315
-(defun phox-sym-lock-font-lock-hook 325,12534
-(defun font-lock-set-defaults 340,13227
-(defun phox-sym-lock-patch-keywords 351,13605
+(defvar phox-sym-lock-sym-count 34,1618
+(defvar phox-sym-lock-ext-start 37,1688
+(defvar phox-sym-lock-ext-end 39,1810
+(defvar phox-sym-lock-font-size 42,1929
+(defvar phox-sym-lock-keywords 47,2119
+(defvar phox-sym-lock-enabled 52,2295
+(defvar phox-sym-lock-color 57,2457
+(defvar phox-sym-lock-mouse-face 62,2675
+(defvar phox-sym-lock-mouse-face-enabled 67,2865
+(defconst phox-sym-lock-with-mule 72,3055
+(defun phox-sym-lock-gen-symbol 75,3139
+(defun phox-sym-lock-make-symbols-atomic 83,3442
+(defun phox-sym-lock-compute-font-size 110,4384
+(defvar phox-sym-lock-font-name148,5804
+(defun phox-sym-lock-set-foreground 186,7089
+(defun phox-sym-lock-translate-char 200,7698
+(defun phox-sym-lock-translate-char-or-string 208,7966
+(defun phox-sym-lock-remap-face 215,8193
+(defvar phox-sym-lock-clear-face235,9183
+(defun phox-sym-lock 247,9605
+(defun phox-sym-lock-rec 256,10009
+(defun phox-sym-lock-atom-face 262,10162
+(defun phox-sym-lock-pre-idle-hook-first 267,10458
+(defun phox-sym-lock-pre-idle-hook-last 275,10816
+(defun phox-sym-lock-enable 284,11191
+(defun phox-sym-lock-disable 297,11604
+(defun phox-sym-lock-mouse-face-enable 310,12022
+(defun phox-sym-lock-mouse-face-disable 317,12237
+(defun phox-sym-lock-font-lock-hook 324,12456
+(defun font-lock-set-defaults 339,13149
+(defun phox-sym-lock-patch-keywords 350,13527
 
 phox/phox-tags.el,305
 (defun phox-tags-add-table(21,766
-(defun phox-tags-reset-table(38,1359
-(defun phox-tags-add-doc-table(48,1629
-(defun phox-tags-add-lib-table(54,1778
-(defun phox-tags-add-local-table(60,1914
-(defun phox-tags-create-local-table(66,2097
-(defun phox-complete-tag(77,2349
-(defvar phox-tags-menu96,2904
+(defun phox-tags-reset-table(38,1354
+(defun phox-tags-add-doc-table(48,1619
+(defun phox-tags-add-lib-table(54,1768
+(defun phox-tags-add-local-table(60,1904
+(defun phox-tags-create-local-table(66,2087
+(defun phox-complete-tag(77,2339
+(defvar phox-tags-menu96,2889
 
 phox/x-symbol-phox.el,1609
-(defvar x-symbol-phox-required-fonts 14,449
-(defcustom x-symbol-phox-header-groups-alist 29,1056
-(defcustom x-symbol-phox-electric-ignore 36,1276
-(defvar x-symbol-phox-required-fonts 43,1492
-(defvar x-symbol-phox-extra-menu-items 46,1593
-(defvar x-symbol-phox-token-grammar49,1682
-(defvar x-symbol-phox-input-token-grammar63,2473
-(defun x-symbol-phox-default-token-list 69,2728
-(defvar x-symbol-phox-user-table 81,3046
-(defvar x-symbol-phox-generated-data 84,3155
-(defvar x-symbol-phox-master-directory 92,3394
-(defvar x-symbol-phox-image-searchpath 93,3443
-(defvar x-symbol-phox-image-cached-dirs 94,3491
-(defvar x-symbol-phox-image-file-truename-alist 95,3557
-(defvar x-symbol-phox-image-keywords 96,3610
-(defcustom x-symbol-phox-class-alist103,3831
-(defcustom x-symbol-phox-class-face-alist 114,4213
-(defvar x-symbol-phox-font-lock-keywords 124,4526
-(defvar x-symbol-phox-font-lock-allowed-faces 126,4573
-(defvar x-symbol-phox-case-insensitive 132,4798
-(defvar x-symbol-phox-token-shape 133,4842
-(defvar x-symbol-phox-input-token-ignore 134,4881
-(defvar x-symbol-phox-token-list 141,5120
-(defvar x-symbol-phox-xsymb0-table 143,5165
-(defun x-symbol-phox-prepare-table 164,5624
-(defvar x-symbol-phox-table172,5800
-(defcustom x-symbol-phox-auto-style183,6118
-(defvar x-symbol-phox-menu-alist 209,7068
-(defvar x-symbol-phox-grid-alist 211,7158
-(defvar x-symbol-phox-decode-atree 214,7249
-(defvar x-symbol-phox-decode-alist 216,7342
-(defvar x-symbol-phox-encode-alist 218,7439
-(defvar x-symbol-phox-nomule-decode-exec 222,7596
-(defvar x-symbol-phox-nomule-encode-exec 224,7696
-
-plastic/plastic.el,2907
-(defcustom plastic-tags 28,805
-(defcustom plastic-test-all-name 33,937
-(defvar plastic-lit-string 39,1110
-(defcustom plastic-help-menu-list43,1223
-(defvar plastic-shell-process-output57,1717
-(defconst plastic-process-config 65,2043
-(defconst plastic-pretty-set-width 72,2293
-(defconst plastic-interrupt-regexp 76,2442
-(defcustom plastic-www-home-page 82,2563
-(defcustom plastic-www-latest-release87,2700
-(defcustom plastic-www-refcard93,2873
-(defcustom plastic-library-www-page99,3004
-(defcustom plastic-base 109,3219
-(defvar plastic-prog-name 117,3391
-(defun plastic-set-default-env-vars 121,3499
-(defvar plastic-shell-prompt-pattern 129,3737
-(defvar plastic-shell-cd 132,3862
-(defvar plastic-shell-abort-goal-regexp 136,4004
-(defvar plastic-shell-proof-completed-regexp 140,4172
-(defvar plastic-save-command-regexp143,4315
-(defvar plastic-goal-command-regexp145,4411
-(defvar plastic-kill-goal-command 148,4508
-(defvar plastic-forget-id-command 150,4609
-(defvar plastic-undoable-commands-regexp153,4690
-(defvar plastic-goal-regexp 165,5137
-(defvar plastic-outline-regexp167,5185
-(defvar plastic-outline-heading-end-regexp 173,5364
-(defvar plastic-shell-outline-regexp 175,5420
-(defvar plastic-shell-outline-heading-end-regexp 176,5478
-(defvar plastic-error-occurred 178,5549
-(define-derived-mode plastic-shell-mode 187,5881
-(define-derived-mode plastic-mode 193,6063
-(define-derived-mode plastic-goals-mode 207,6516
-(defun plastic-count-undos 216,6861
-(defun plastic-goal-command-p 236,7737
-(defun plastic-find-and-forget 241,7930
-(defun plastic-goal-hyp 276,9278
-(defun plastic-state-preserving-p 287,9528
-(defvar plastic-shell-current-line-width 309,10456
-(defun plastic-shell-adjust-line-width 317,10772
-(defun plastic-pre-shell-start 338,11653
-(defun plastic-mode-config 353,12219
-(defun plastic-show-shell-buffer 450,15864
-(defun plastic-equal-module-filename 456,15967
-(defun plastic-shell-compute-new-files-list 462,16245
-(defun plastic-shell-mode-config 478,16782
-(defun plastic-goals-mode-config 529,18975
-(defun plastic-small-bar 541,19257
-(defun plastic-large-bar 543,19346
-(defun plastic-preprocessing 545,19484
-(defun plastic-all-ctxt 596,21312
-(defun plastic-send-one-undo 603,21490
-(defun plastic-minibuf-cmd 613,21818
-(defun plastic-minibuf 625,22297
-(defun plastic-synchro 632,22503
-(defun plastic-send-minibuf 637,22644
-(defun plastic-had-error 645,22973
-(defun plastic-reset-error 649,23148
-(defun plastic-call-if-no-error 652,23287
-(defun plastic-show-shell 657,23491
-(define-key plastic-keymap 666,23753
-(define-key plastic-keymap 667,23814
-(define-key plastic-keymap 668,23875
-(define-key plastic-keymap 669,23935
-(define-key plastic-keymap 670,23994
-(define-key plastic-keymap 671,24053
-(defalias 'proof-toolbar-command proof-toolbar-command
681,24303
-(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
682,24354
+(defvar x-symbol-phox-required-fonts 16,473
+(defcustom x-symbol-phox-header-groups-alist 31,1080
+(defcustom x-symbol-phox-electric-ignore 38,1300
+(defvar x-symbol-phox-required-fonts 45,1516
+(defvar x-symbol-phox-extra-menu-items 48,1617
+(defvar x-symbol-phox-token-grammar51,1706
+(defvar x-symbol-phox-input-token-grammar65,2497
+(defun x-symbol-phox-default-token-list 71,2752
+(defvar x-symbol-phox-user-table 83,3070
+(defvar x-symbol-phox-generated-data 86,3179
+(defvar x-symbol-phox-master-directory 94,3418
+(defvar x-symbol-phox-image-searchpath 95,3467
+(defvar x-symbol-phox-image-cached-dirs 96,3515
+(defvar x-symbol-phox-image-file-truename-alist 97,3581
+(defvar x-symbol-phox-image-keywords 98,3634
+(defcustom x-symbol-phox-class-alist105,3855
+(defcustom x-symbol-phox-class-face-alist 116,4237
+(defvar x-symbol-phox-font-lock-keywords 126,4550
+(defvar x-symbol-phox-font-lock-allowed-faces 128,4597
+(defvar x-symbol-phox-case-insensitive 134,4822
+(defvar x-symbol-phox-token-shape 135,4866
+(defvar x-symbol-phox-input-token-ignore 136,4905
+(defvar x-symbol-phox-token-list 143,5144
+(defvar x-symbol-phox-xsymb0-table 145,5189
+(defun x-symbol-phox-prepare-table 166,5648
+(defvar x-symbol-phox-table174,5824
+(defcustom x-symbol-phox-auto-style185,6142
+(defvar x-symbol-phox-menu-alist 211,7092
+(defvar x-symbol-phox-grid-alist 213,7182
+(defvar x-symbol-phox-decode-atree 216,7273
+(defvar x-symbol-phox-decode-alist 218,7366
+(defvar x-symbol-phox-encode-alist 220,7463
+(defvar x-symbol-phox-nomule-decode-exec 224,7620
+(defvar x-symbol-phox-nomule-encode-exec 226,7720
+
+plastic/plastic.el,2866
+(defcustom plastic-tags 29,821
+(defcustom plastic-test-all-name 34,953
+(defvar plastic-lit-string 41,1144
+(defcustom plastic-help-menu-list45,1258
+(defvar plastic-shell-process-output59,1752
+(defconst plastic-process-config 67,2078
+(defconst plastic-pretty-set-width 74,2328
+(defconst plastic-interrupt-regexp 78,2477
+(defcustom plastic-www-home-page 84,2598
+(defcustom plastic-www-latest-release89,2735
+(defcustom plastic-www-refcard95,2908
+(defcustom plastic-library-www-page101,3039
+(defcustom plastic-base 111,3254
+(defvar plastic-prog-name 119,3426
+(defun plastic-set-default-env-vars 123,3534
+(defvar plastic-shell-prompt-pattern 131,3772
+(defvar plastic-shell-cd 134,3897
+(defvar plastic-shell-abort-goal-regexp 138,4039
+(defvar plastic-shell-proof-completed-regexp 142,4207
+(defvar plastic-save-command-regexp145,4350
+(defvar plastic-goal-command-regexp147,4446
+(defvar plastic-kill-goal-command 150,4543
+(defvar plastic-forget-id-command 152,4644
+(defvar plastic-undoable-commands-regexp155,4725
+(defvar plastic-goal-regexp 167,5172
+(defvar plastic-outline-regexp169,5220
+(defvar plastic-outline-heading-end-regexp 175,5399
+(defvar plastic-shell-outline-regexp 177,5455
+(defvar plastic-shell-outline-heading-end-regexp 178,5513
+(defvar plastic-error-occurred 180,5584
+(define-derived-mode plastic-shell-mode 189,5916
+(define-derived-mode plastic-mode 195,6098
+(define-derived-mode plastic-goals-mode 209,6551
+(defun plastic-count-undos 218,6896
+(defun plastic-goal-command-p 238,7772
+(defun plastic-find-and-forget 243,7965
+(defun plastic-goal-hyp 278,9313
+(defun plastic-state-preserving-p 289,9563
+(defvar plastic-shell-current-line-width 312,10456
+(defun plastic-shell-adjust-line-width 320,10772
+(defun plastic-mode-config 347,11867
+(defun plastic-show-shell-buffer 436,15108
+(defun plastic-equal-module-filename 442,15211
+(defun plastic-shell-compute-new-files-list 448,15489
+(defun plastic-shell-mode-config 464,16026
+(defun plastic-goals-mode-config 515,18219
+(defun plastic-small-bar 527,18501
+(defun plastic-large-bar 529,18590
+(defun plastic-preprocessing 531,18728
+(defun plastic-all-ctxt 582,20556
+(defun plastic-send-one-undo 589,20734
+(defun plastic-minibuf-cmd 599,21062
+(defun plastic-minibuf 611,21541
+(defun plastic-synchro 618,21747
+(defun plastic-send-minibuf 623,21888
+(defun plastic-had-error 631,22217
+(defun plastic-reset-error 635,22392
+(defun plastic-call-if-no-error 638,22531
+(defun plastic-show-shell 643,22735
+(define-key plastic-keymap 652,22997
+(define-key plastic-keymap 653,23058
+(define-key plastic-keymap 654,23119
+(define-key plastic-keymap 655,23179
+(define-key plastic-keymap 656,23238
+(define-key plastic-keymap 657,23297
+(defalias 'proof-toolbar-command proof-toolbar-command
667,23547
+(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
668,23598
 
 plastic/plastic-syntax.el,648
 (defconst plastic-keywords-goal 18,537
@@ -1092,163 +1151,168 @@ twelf/twelf-old.el,6958
 (defun twelf-server-remove-menu 2651,107274
 (defun twelf-server-reset-menu 2655,107386
 
-generic/pg-assoc.el,329
-(define-derived-mode proof-universal-keys-only-mode 20,563
-(defun proof-associated-buffers 32,987
-(defun proof-associated-windows 41,1184
-(defun pg-assoc-strip-subterm-markup 58,1665
-(defvar pg-assoc-ann-regexp 84,2598
-(defun pg-assoc-strip-subterm-markup-buf 87,2693
-(defun pg-assoc-strip-subterm-markup-buf-old 110,3412
-
-generic/pg-autotest.el,442
-(defvar pg-autotest-success 21,538
-(defun pg-autotest-find-file 25,622
-(defun pg-autotest-find-file-restart 32,893
-(defmacro pg-autotest 45,1341
-(defun pg-autotest-script-wholefile 59,1689
-(defun pg-autotest-retract-file 76,2302
-(defun pg-autotest-assert-processed 82,2438
-(defun pg-autotest-assert-unprocessed 89,2684
-(defun pg-autotest-message 96,2931
-(defun pg-autotest-quit-prover 103,3124
-(defun pg-autotest-finished 109,3306
-
-generic/pg-goals.el,704
-(define-derived-mode proof-goals-mode 29,669
-(define-key proof-goals-mode-map 50,1432
-(define-key proof-goals-mode-map 53,1515
-(define-key proof-goals-mode-map 54,1585
-(define-key proof-goals-mode-map 62,2175
-(define-key proof-goals-mode-map 64,2248
-(define-key proof-goals-mode-map 65,2316
-(define-key proof-goals-mode-map 71,2750
-(defun proof-goals-config-done 86,3014
-(defun pg-goals-display 96,3302
-(defun pg-goals-analyse-structure 152,5455
-(defun pg-goals-make-top-span 279,10502
-(defun pg-goals-yank-subterm 319,12006
-(defun pg-goals-button-action 346,12906
-(defun proof-expand-path 367,13879
-(defun pg-goals-construct-command 376,14123
-(defun pg-goals-get-subterm-help 405,15148
-
-generic/pg-metadata.el,128
-(defcustom pg-metadata-default-directory 23,628
-(defface proof-preparsed-span 28,802
-(defun pg-metadata-filename-for 39,1065
-
-generic/pg-pbrpm.el,1781
-(defvar pg-pbrpm-use-buffer-menu 13,309
-(defvar pg-pbrpm-buffer-menu 15,428
-(defvar pg-pbrpm-spans 16,462
-(defvar pg-pbrpm-goal-description 17,490
-(defvar pg-pbrpm-windows-dialog-bug 18,529
-(defun pg-pbrpm-erase-buffer-menu 20,571
-(defun pg-pbrpm-menu-change-hook 27,755
-(defun pg-pbrpm-create-reset-buffer-menu 45,1332
-(defun pg-pbrpm-analyse-goal-buffer 59,1946
-(defun pg-pbrpm-button-action 120,4366
-(defun pg-pbrpm-exists 127,4592
-(defun pg-pbrpm-eliminate-id 131,4704
-(defun pg-pbrpm-build-menu 139,4952
-(defun pg-pbrpm-setup-span 199,7269
-(defun pg-pbrpm-run-command 259,9600
-(defun pg-pbrpm-get-pos-info 288,10911
-(defun pg-pbrpm-get-region-info 324,12053
-(defun auto-select-arround-pos 334,12378
-(defun pg-pbrpm-translate-position 346,12822
-(defun pg-pbrpm-process-click 352,13046
-(defvar pg-pbrpm-remember-region-selected-region 372,14053
-(defvar pg-pbrpm-regions-list 373,14107
-(defun pg-pbrpm-erase-regions-list 375,14143
-(defun pg-pbrpm-filter-regions-list 384,14452
-(defface pg-pbrpm-multiple-selection-face391,14715
-(defface pg-pbrpm-menu-input-face399,14920
-(defun pg-pbrpm-do-remember-region 407,15113
-(defun pg-pbrpm-remember-region-drag-up-hook 428,15964
-(defun pg-pbrpm-remember-region-click-hook 432,16135
-(defun pg-pbrpm-remember-region 437,16320
-(defun pg-pbrpm-process-region 451,17035
-(defun pg-pbrpm-process-regions-list 468,17761
-(defun pg-pbrpm-region-expression 472,17944
-(define-key proof-goals-mode-map 497,18906
-(define-key proof-goals-mode-map 498,18976
-(define-key proof-goals-mode-map 499,19053
-(define-key pg-span-context-menu-keymap 500,19133
-(define-key pg-span-context-menu-keymap 501,19210
-(define-key proof-mode-map 502,19293
-(define-key proof-mode-map 503,19357
-(define-key proof-mode-map 504,19428
-
-generic/pg-pgip.el,2889
-(defalias 'pg-pgip-debug pg-pgip-debug
29,883
-(defalias 'pg-pgip-error pg-pgip-error
30,924
-(defalias 'pg-pgip-warning pg-pgip-warning
31,959
-(defconst pg-pgip-version-supported 33,1009
-(defun pg-pgip-process-packet 37,1115
-(defvar pg-pgip-last-seen-id 47,1688
-(defvar pg-pgip-last-seen-seq 48,1722
-(defun pg-pgip-process-pgip 50,1758
-(defun pg-pgip-process-msg 69,2689
-(defvar pg-pgip-post-process-functions83,3259
-(defun pg-pgip-post-process 93,3746
-(defun pg-pgip-process-askpgip 109,4357
-(defun pg-pgip-process-usespgip 114,4516
-(defun pg-pgip-process-usespgml 118,4680
-(defun pg-pgip-process-pgmlconfig 122,4844
-(defun pg-pgip-process-proverinfo 138,5463
-(defun pg-pgip-process-hasprefs 155,6128
-(defun pg-pgip-haspref 169,6760
-(defun pg-pgip-process-prefval 188,7539
-(defun pg-pgip-process-guiconfig 215,8248
-(defvar proof-assistant-idtables 222,8365
-(defun pg-pgip-process-ids 225,8482
-(defun pg-complete-idtable-symbol 251,9561
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids
256,9653
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids
257,9709
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids
258,9765
-(defun pg-pgip-process-idvalue 261,9823
-(defun pg-pgip-process-menuadd 273,10160
-(defun pg-pgip-process-menudel 276,10203
-(defun pg-pgip-process-ready 285,10436
-(defun pg-pgip-process-cleardisplay 288,10477
-(defun pg-pgip-process-proofstate 302,10954
-(defun pg-pgip-process-normalresponse 306,11031
-(defun pg-pgip-process-errorresponse 310,11155
-(defun pg-pgip-process-scriptinsert 314,11278
-(defun pg-pgip-process-metainforesponse 319,11412
-(defun pg-pgip-process-informfileloaded 328,11653
-(defun pg-pgip-process-informfileretracted 334,11920
-(defun pg-pgip-process-brokerstatus 347,12397
-(defun pg-pgip-process-proveravailmsg 350,12445
-(defun pg-pgip-process-newprovermsg 353,12495
-(defun pg-pgip-process-proverstatusmsg 356,12543
-(defvar pg-pgip-srcids 365,12790
-(defun pg-pgip-process-newfile 369,12897
-(defun pg-pgip-process-filestatus 385,13485
-(defun pg-pgip-process-newobj 405,14140
-(defun pg-pgip-process-delobj 408,14182
-(defun pg-pgip-process-objectstatus 411,14224
-(defun pg-pgip-process-parsescript 425,14580
-(defun pg-pgip-get-pgiptype 448,15455
-(defun pg-pgip-default-for 468,16252
-(defun pg-pgip-subst-for 481,16647
-(defun pg-pgip-interpret-value 493,16990
-(defun pg-pgip-interpret-choice 511,17676
-(defun pg-pgip-string-of-command 542,18696
-(defconst pg-pgip-id559,19457
-(defvar pg-pgip-refseq 565,19737
-(defvar pg-pgip-refid 567,19835
-(defvar pg-pgip-seq 570,19929
-(defun pg-pgip-assemble-packet 572,19993
-(defun pg-pgip-issue 590,20808
-(defun pg-pgip-maybe-askpgip 607,21421
-(defun pg-pgip-askprefs 613,21612
-(defun pg-pgip-askids 617,21726
-(defun pg-pgip-reset 630,22017
-(defconst pg-pgip-start-element-regexp 661,22715
-(defconst pg-pgip-end-element-regexp 662,22767
+generic/pg-assoc.el,354
+(defun proof-associated-buffers 35,1072
+(defun proof-associated-windows 44,1269
+(defun pg-assoc-strip-subterm-markup 61,1750
+(defvar pg-assoc-ann-regexp 87,2683
+(defun pg-assoc-strip-subterm-markup-buf 90,2778
+(defun pg-assoc-strip-subterm-markup-buf-old 113,3497
+(defun pg-assoc-make-top-span 142,4352
+(defun pg-assoc-analyse-structure 171,5571
+
+generic/pg-autotest.el,443
+(defvar pg-autotest-success 26,573
+(defun pg-autotest-find-file 30,657
+(defun pg-autotest-find-file-restart 37,937
+(defmacro pg-autotest 50,1385
+(defun pg-autotest-script-wholefile 64,1732
+(defun pg-autotest-retract-file 81,2345
+(defun pg-autotest-assert-processed 87,2481
+(defun pg-autotest-assert-unprocessed 94,2735
+(defun pg-autotest-message 101,2995
+(defun pg-autotest-quit-prover 108,3188
+(defun pg-autotest-finished 114,3369
+
+generic/pg-custom.el,673
+(defpgcustom x-symbol-enable 32,1033
+(defpgcustom x-symbol-language 41,1383
+(defpgcustom maths-menu-enable 46,1605
+(defpgcustom mmm-enable 52,1785
+(defpgcustom script-indent 61,2139
+(defpgcustom toolbar-entries 66,2276
+(defpgcustom prog-args 84,2996
+(defpgcustom prog-env 97,3571
+(defpgcustom favourites 106,3997
+(defpgcustom menu-entries 111,4186
+(defpgcustom help-menu-entries 118,4422
+(defpgcustom keymap 125,4685
+(defpgcustom completion-table 130,4857
+(defpgcustom tags-program 141,5231
+(defconst proof-mode-for-shell 151,5403
+(defconst proof-mode-for-response 155,5533
+(defconst proof-mode-for-goals 159,5701
+(defconst proof-mode-for-script 163,5829
+
+generic/pg-goals.el,363
+(define-derived-mode proof-goals-mode 33,663
+(define-key proof-goals-mode-map 63,1542
+(defun proof-goals-config-done 93,3010
+(defun pg-goals-display 103,3298
+(defun pg-goals-yank-subterm 169,5735
+(defun pg-goals-button-action 196,6635
+(defun proof-expand-path 217,7607
+(defun pg-goals-construct-command 226,7849
+(defun pg-goals-get-subterm-help 255,8870
+
+generic/pg-metadata.el,127
+(defcustom pg-metadata-default-directory 26,647
+(defface proof-preparsed-span31,821
+(defun pg-metadata-filename-for 42,1083
+
+generic/pg-pbrpm.el,1433
+(defvar pg-pbrpm-use-buffer-menu 10,270
+(defvar pg-pbrpm-buffer-menu 12,391
+(defvar pg-pbrpm-spans 13,425
+(defvar pg-pbrpm-goal-description 14,453
+(defvar pg-pbrpm-windows-dialog-bug 15,492
+(defun pg-pbrpm-erase-buffer-menu 17,534
+(defun pg-pbrpm-menu-change-hook 24,718
+(defun pg-pbrpm-create-reset-buffer-menu 42,1294
+(defun pg-pbrpm-analyse-goal-buffer 57,1923
+(defun pg-pbrpm-button-action 117,4333
+(defun pg-pbrpm-exists 124,4559
+(defun pg-pbrpm-eliminate-id 128,4671
+(defun pg-pbrpm-build-menu 136,4917
+(defun pg-pbrpm-setup-span 196,7229
+(defun pg-pbrpm-run-command 256,9546
+(defun pg-pbrpm-get-pos-info 285,10856
+(defun pg-pbrpm-get-region-info 321,11993
+(defun auto-select-arround-pos 331,12318
+(defun pg-pbrpm-translate-position 343,12762
+(defun pg-pbrpm-process-click 349,12985
+(defvar pg-pbrpm-remember-region-selected-region 369,13990
+(defvar pg-pbrpm-regions-list 370,14044
+(defun pg-pbrpm-erase-regions-list 372,14080
+(defun pg-pbrpm-filter-regions-list 381,14388
+(defface pg-pbrpm-multiple-selection-face388,14651
+(defface pg-pbrpm-menu-input-face396,14853
+(defun pg-pbrpm-do-remember-region 404,15043
+(defun pg-pbrpm-remember-region-drag-up-hook 425,15891
+(defun pg-pbrpm-remember-region-click-hook 429,16062
+(defun pg-pbrpm-remember-region 434,16247
+(defun pg-pbrpm-process-region 448,16962
+(defun pg-pbrpm-process-regions-list 465,17687
+(defun pg-pbrpm-region-expression 469,17870
+
+generic/pg-pgip.el,2890
+(defalias 'pg-pgip-debug pg-pgip-debug
35,939
+(defalias 'pg-pgip-error pg-pgip-error
36,980
+(defalias 'pg-pgip-warning pg-pgip-warning
37,1015
+(defconst pg-pgip-version-supported 39,1065
+(defun pg-pgip-process-packet 43,1171
+(defvar pg-pgip-last-seen-id 53,1743
+(defvar pg-pgip-last-seen-seq 54,1777
+(defun pg-pgip-process-pgip 56,1813
+(defun pg-pgip-process-msg 75,2744
+(defvar pg-pgip-post-process-functions89,3311
+(defun pg-pgip-post-process 99,3799
+(defun pg-pgip-process-askpgip 115,4410
+(defun pg-pgip-process-usespgip 120,4569
+(defun pg-pgip-process-usespgml 124,4733
+(defun pg-pgip-process-pgmlconfig 128,4897
+(defun pg-pgip-process-proverinfo 144,5514
+(defun pg-pgip-process-hasprefs 161,6179
+(defun pg-pgip-haspref 175,6811
+(defun pg-pgip-process-prefval 194,7587
+(defun pg-pgip-process-guiconfig 221,8296
+(defvar proof-assistant-idtables 228,8413
+(defun pg-pgip-process-ids 231,8530
+(defun pg-complete-idtable-symbol 257,9606
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids
262,9698
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids
263,9754
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids
264,9810
+(defun pg-pgip-process-idvalue 267,9868
+(defun pg-pgip-process-menuadd 279,10204
+(defun pg-pgip-process-menudel 282,10247
+(defun pg-pgip-process-ready 291,10480
+(defun pg-pgip-process-cleardisplay 294,10521
+(defun pg-pgip-process-proofstate 308,10978
+(defun pg-pgip-process-normalresponse 312,11055
+(defun pg-pgip-process-errorresponse 316,11179
+(defun pg-pgip-process-scriptinsert 320,11302
+(defun pg-pgip-process-metainforesponse 325,11436
+(defun pg-pgip-process-informfileloaded 334,11677
+(defun pg-pgip-process-informfileretracted 340,11943
+(defun pg-pgip-process-brokerstatus 353,12420
+(defun pg-pgip-process-proveravailmsg 356,12468
+(defun pg-pgip-process-newprovermsg 359,12518
+(defun pg-pgip-process-proverstatusmsg 362,12566
+(defvar pg-pgip-srcids 371,12813
+(defun pg-pgip-process-newfile 375,12920
+(defun pg-pgip-process-filestatus 391,13508
+(defun pg-pgip-process-newobj 411,14163
+(defun pg-pgip-process-delobj 414,14205
+(defun pg-pgip-process-objectstatus 417,14247
+(defun pg-pgip-process-parsescript 431,14602
+(defun pg-pgip-get-pgiptype 454,15477
+(defun pg-pgip-default-for 474,16270
+(defun pg-pgip-subst-for 487,16665
+(defun pg-pgip-interpret-value 499,17008
+(defun pg-pgip-interpret-choice 517,17693
+(defun pg-pgip-string-of-command 548,18710
+(defconst pg-pgip-id565,19471
+(defvar pg-pgip-refseq 571,19751
+(defvar pg-pgip-refid 573,19848
+(defvar pg-pgip-seq 576,19940
+(defun pg-pgip-assemble-packet 578,20004
+(defun pg-pgip-issue 596,20816
+(defun pg-pgip-maybe-askpgip 613,21428
+(defun pg-pgip-askprefs 619,21619
+(defun pg-pgip-askids 623,21733
+(defun pg-pgip-reset 636,22021
+(defconst pg-pgip-start-element-regexp 667,22719
+(defconst pg-pgip-end-element-regexp 668,22771
 
 generic/pg-pgip-old.el,456
 (defun pg-pgip-process-oldhaspref 18,633
@@ -1263,373 +1327,352 @@ generic/pg-pgip-old.el,456
 (defun pg-pgip-old-get-type 131,4423
 (defun pg-pgip-old-pgiptype 138,4639
 
-generic/pg-response.el,1188
-(define-derived-mode proof-response-mode 25,617
-(defun proof-response-config-done 50,1658
-(defvar proof-shell-special-display-regexp 71,2433
-(defconst proof-multiframe-specifiers 79,2838
-(defun proof-map-multiple-frame-specifiers 88,3202
-(defconst proof-multiframe-parameters98,3664
-(defun proof-multiple-frames-enable 107,3963
-(defun proof-three-window-enable 129,4683
-(defun proof-select-three-b 133,4747
-(defun proof-display-three-b 148,5216
-(defvar pg-frame-configuration 162,5710
-(defun pg-cache-frame-configuration 166,5857
-(defun proof-layout-windows 170,6028
-(defun proof-delete-other-frames 211,7841
-(defvar pg-response-erase-flag 242,8936
-(defun proof-shell-maybe-erase-response245,9051
-(defun pg-response-display 276,10253
-(defun pg-response-display-with-face 294,11107
-(defun pg-response-clear-displays 332,12464
-(defvar pg-response-next-error 350,13043
-(defun proof-next-error 354,13165
-(defun pg-response-has-error-location 434,16105
-(defvar proof-trace-last-fontify-pos 457,16938
-(defun proof-trace-fontify-pos 459,16981
-(defun proof-trace-buffer-display 467,17295
-(defun proof-trace-buffer-finish 491,18268
-(defun pg-thms-buffer-clear 512,18847
+generic/pg-response.el,1222
+(defvar pg-response-next-error 31,694
+(deflocal pg-response-eagerly-raise 34,801
+(define-derived-mode proof-response-mode 44,1026
+(defun proof-response-config-done 68,2027
+(defvar pg-response-special-display-regexp 89,2802
+(defconst proof-multiframe-specifiers97,3208
+(defun proof-map-multiple-frame-specifiers 106,3565
+(defconst proof-multiframe-parameters117,4087
+(defun proof-multiple-frames-enable 126,4386
+(defun proof-three-window-enable 144,5030
+(defun proof-select-three-b 148,5094
+(defun proof-display-three-b 163,5563
+(defvar pg-frame-configuration 177,6055
+(defun pg-cache-frame-configuration 181,6202
+(defun proof-layout-windows 185,6373
+(defun proof-delete-other-frames 226,8196
+(defvar pg-response-erase-flag 257,9286
+(defun pg-response-maybe-erase261,9415
+(defun pg-response-display 292,10600
+(defun pg-response-display-with-face 310,11433
+(defun pg-response-clear-displays 347,12731
+(defun proof-next-error 366,13318
+(defun pg-response-has-error-location 447,16234
+(defvar proof-trace-last-fontify-pos 470,17067
+(defun proof-trace-fontify-pos 472,17110
+(defun proof-trace-buffer-display 480,17423
+(defun proof-trace-buffer-finish 504,18423
+(defun pg-thms-buffer-clear 525,19003
 
 generic/pg-thymodes.el,152
-(defmacro pg-defthymode 19,466
-(defmacro pg-do-unless-null 67,2277
-(defun pg-symval 72,2364
-(defun pg-modesym 78,2520
-(defun pg-modesymval 82,2634
-
-generic/pg-user.el,2335
-(defmacro proof-maybe-save-point 21,410
-(defun proof-maybe-follow-locked-end 29,612
-(defun proof-assert-next-command-interactive 43,977
-(defun proof-process-buffer 53,1348
-(defun proof-undo-last-successful-command 67,1665
-(defun proof-undo-and-delete-last-successful-command 72,1827
-(defun proof-undo-last-successful-command-1 94,2799
-(defun proof-retract-buffer 110,3364
-(defun proof-retract-current-goal 119,3644
-(defun proof-interrupt-process 137,4135
-(defun proof-goto-command-start 164,5120
-(defun proof-goto-command-end 187,6062
-(defun proof-mouse-goto-point 212,6842
-(defun proof-mouse-track-insert 227,7416
-(defvar proof-minibuffer-history 262,8526
-(defun proof-minibuffer-cmd 265,8620
-(defun proof-frob-locked-end 313,10426
-(defmacro proof-if-setting-configured 406,13340
-(defmacro proof-define-assistant-command 414,13610
-(defmacro proof-define-assistant-command-witharg 427,14076
-(defun proof-issue-new-command 447,14901
-(defun proof-cd-sync 492,16400
-(deflocal proof-electric-terminator 543,17869
-(defun proof-electric-terminator-enable 553,18216
-(defun proof-electric-term-incomment-fn 564,18703
-(defun proof-process-electric-terminator 584,19459
-(defun proof-electric-terminator 611,20610
-(defun proof-add-completions 633,21248
-(defun proof-script-complete 653,22005
-(defun pg-insert-last-output-as-comment 681,22596
-(defun pg-copy-span-contents 712,23824
-(defun pg-numth-span-higher-or-lower 729,24384
-(defun pg-control-span-of 755,25131
-(defun pg-move-span-contents 761,25335
-(defun pg-fixup-children-span 815,27559
-(defun pg-move-region-down 822,27762
-(defun pg-move-region-up 831,28056
-(defun proof-forward-command 861,28896
-(defun proof-backward-command 882,29618
-(defvar pg-span-context-menu-keymap898,29862
-(defun pg-span-for-event 914,30289
-(defun pg-span-context-menu 925,30673
-(defun pg-toggle-visibility 940,31133
-(defun pg-create-in-span-context-menu 950,31455
-(defun pg-span-undo 983,32807
-(defun pg-goals-buffers-hint 1029,34217
-(defun pg-slow-fontify-tracing-hint 1032,34384
-(defun pg-response-buffers-hint 1035,34540
-(defun pg-jump-to-end-hint 1044,34889
-(defun pg-processing-complete-hint 1047,35005
-(defun pg-next-error-hint 1063,35691
-(defun pg-hint 1067,35828
-(defun pg-identifier-under-mouse-query 1086,36504
-(defun proof-imenu-enable 1131,38131
-
-generic/pg-xhtml.el,392
-(defvar pg-xhtml-dir 17,423
-(defun pg-xhtml-dir 20,489
-(defvar pg-xhtml-file-count 32,856
-(defun pg-xhtml-next-file 35,928
-(defvar pg-xhtml-header 47,1159
-(defmacro pg-xhtml-write-tempfile 53,1400
-(defun pg-xhtml-cleanup-tempdir 71,1996
-(defvar pg-mozilla-prog-name 75,2127
-(defun pg-xhtml-display-file-mozilla 79,2235
-(defalias 'pg-xhtml-display-file pg-xhtml-display-file
84,2408
-
-generic/pg-xml.el,1096
-(defun pg-xml-parse-string 40,1169
-(defun pg-xml-parse-buffer 51,1503
-(defun pg-xml-get-attr 73,2236
-(defun pg-xml-child-elts 81,2540
-(defun pg-xml-child-elt 86,2745
-(defun pg-xml-get-child 94,3028
-(defun pg-xml-get-text-content 104,3400
-(defmacro pg-xml-attr 115,3750
-(defmacro pg-xml-node 117,3812
-(defconst pg-xml-header 120,3905
-(defun pg-xml-string-of 124,3982
-(defun pg-xml-output-internal 135,4354
-(defun pg-xml-cdata 169,5504
-(defun pg-pgip-get-icon 177,5697
-(defsubst pg-pgip-get-name 181,5845
-(defsubst pg-pgip-get-version 184,5962
-(defsubst pg-pgip-get-descr 187,6085
-(defsubst pg-pgip-get-thmname 190,6204
-(defsubst pg-pgip-get-thyname 193,6327
-(defsubst pg-pgip-get-url 196,6450
-(defsubst pg-pgip-get-srcid 199,6565
-(defsubst pg-pgip-get-proverid 202,6684
-(defsubst pg-pgip-get-symname 205,6809
-(defsubst pg-pgip-get-prefcat 208,6929
-(defsubst pg-pgip-get-default 211,7057
-(defsubst pg-pgip-get-objtype 214,7180
-(defsubst pg-pgip-get-value 217,7303
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7373
-(defun pg-pgip-get-pgmltext 222,7432
+(defmacro pg-defthymode 23,499
+(defmacro pg-do-unless-null 71,2307
+(defun pg-symval 76,2394
+(defun pg-modesym 82,2549
+(defun pg-modesymval 86,2663
+
+generic/pg-user.el,2336
+(defmacro proof-maybe-save-point 22,441
+(defun proof-maybe-follow-locked-end 30,643
+(defun proof-assert-next-command-interactive 44,1008
+(defun proof-process-buffer 54,1379
+(defun proof-undo-last-successful-command 68,1696
+(defun proof-undo-and-delete-last-successful-command 73,1858
+(defun proof-undo-last-successful-command-1 95,2829
+(defun proof-retract-buffer 111,3394
+(defun proof-retract-current-goal 120,3674
+(defun proof-interrupt-process 138,4165
+(defun proof-goto-command-start 165,5146
+(defun proof-goto-command-end 188,6086
+(defun proof-mouse-goto-point 213,6864
+(defun proof-mouse-track-insert 228,7435
+(defvar proof-minibuffer-history 263,8543
+(defun proof-minibuffer-cmd 266,8638
+(defun proof-frob-locked-end 314,10436
+(defmacro proof-if-setting-configured 407,13352
+(defmacro proof-define-assistant-command 415,13621
+(defmacro proof-define-assistant-command-witharg 428,14084
+(defun proof-issue-new-command 448,14907
+(defun proof-cd-sync 493,16402
+(deflocal proof-electric-terminator 544,17867
+(defun proof-electric-terminator-enable 554,18214
+(defun proof-electric-term-incomment-fn 565,18700
+(defun proof-process-electric-terminator 585,19451
+(defun proof-electric-terminator 612,20599
+(defun proof-add-completions 634,21234
+(defun proof-script-complete 654,21988
+(defun pg-insert-last-output-as-comment 682,22579
+(defun pg-copy-span-contents 713,23805
+(defun pg-numth-span-higher-or-lower 730,24363
+(defun pg-control-span-of 756,25109
+(defun pg-move-span-contents 762,25313
+(defun pg-fixup-children-span 816,27536
+(defun pg-move-region-down 823,27739
+(defun pg-move-region-up 832,28032
+(defun proof-forward-command 862,28870
+(defun proof-backward-command 883,29591
+(defvar pg-span-context-menu-keymap899,29835
+(defun pg-span-for-event 915,30257
+(defun pg-span-context-menu 926,30635
+(defun pg-toggle-visibility 941,31090
+(defun pg-create-in-span-context-menu 951,31412
+(defun pg-span-undo 984,32756
+(defun pg-goals-buffers-hint 1030,34166
+(defun pg-slow-fontify-tracing-hint 1033,34333
+(defun pg-response-buffers-hint 1036,34489
+(defun pg-jump-to-end-hint 1045,34836
+(defun pg-processing-complete-hint 1048,34952
+(defun pg-next-error-hint 1064,35636
+(defun pg-hint 1068,35773
+(defun pg-identifier-under-mouse-query 1087,36443
+(defun proof-imenu-enable 1132,38065
+
+generic/pg-xhtml.el,390
+(defvar pg-xhtml-dir 24,472
+(defun pg-xhtml-dir 27,538
+(defvar pg-xhtml-file-count 39,905
+(defun pg-xhtml-next-file 42,977
+(defvar pg-xhtml-header54,1207
+(defmacro pg-xhtml-write-tempfile 60,1447
+(defun pg-xhtml-cleanup-tempdir 78,2042
+(defvar pg-mozilla-prog-name82,2173
+(defun pg-xhtml-display-file-mozilla 86,2280
+(defalias 'pg-xhtml-display-file pg-xhtml-display-file
91,2449
+
+generic/pg-xml.el,1095
+(defun pg-xml-parse-string 40,1165
+(defun pg-xml-parse-buffer 51,1498
+(defun pg-xml-get-attr 73,2231
+(defun pg-xml-child-elts 81,2534
+(defun pg-xml-child-elt 86,2739
+(defun pg-xml-get-child 94,3021
+(defun pg-xml-get-text-content 104,3393
+(defmacro pg-xml-attr 115,3743
+(defmacro pg-xml-node 117,3805
+(defconst pg-xml-header120,3897
+(defun pg-xml-string-of 124,3973
+(defun pg-xml-output-internal 135,4344
+(defun pg-xml-cdata 169,5494
+(defun pg-pgip-get-icon 177,5687
+(defsubst pg-pgip-get-name 181,5835
+(defsubst pg-pgip-get-version 184,5952
+(defsubst pg-pgip-get-descr 187,6075
+(defsubst pg-pgip-get-thmname 190,6194
+(defsubst pg-pgip-get-thyname 193,6317
+(defsubst pg-pgip-get-url 196,6440
+(defsubst pg-pgip-get-srcid 199,6555
+(defsubst pg-pgip-get-proverid 202,6674
+(defsubst pg-pgip-get-symname 205,6799
+(defsubst pg-pgip-get-prefcat 208,6919
+(defsubst pg-pgip-get-default 211,7047
+(defsubst pg-pgip-get-objtype 214,7170
+(defsubst pg-pgip-get-value 217,7293
+(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7363
+(defun pg-pgip-get-pgmltext 222,7422
 
 generic/proof-autoloads.el,57
-(defalias (quote proof-x-symbol-decode-region)421,14247
-
-generic/proof-config.el,11099
-(defgroup proof-user-options 84,3173
-(defcustom proof-electric-terminator-enable 89,3287
-(defcustom proof-toolbar-enable 101,3821
-(defcustom proof-imenu-enable 107,3994
-(defpgcustom x-symbol-enable 113,4165
-(defpgcustom maths-menu-enable 122,4515
-(defpgcustom mmm-enable 128,4695
-(defcustom pg-show-hints 137,5049
-(defcustom proof-output-fontify-enable 142,5184
-(defcustom proof-trace-output-slow-catchup 152,5566
-(defcustom proof-strict-state-preserving 162,6064
-(defcustom proof-strict-read-only 175,6673
-(defcustom proof-three-window-enable 185,7023
-(defcustom proof-multiple-frames-enable 204,7778
-(defcustom proof-delete-empty-windows 213,8114
-(defcustom proof-shrink-windows-tofit 224,8645
-(defcustom proof-toolbar-use-button-enablers 231,8917
-(defcustom proof-query-file-save-when-activating-scripting 254,9789
-(defpgcustom script-indent 270,10512
-(defcustom proof-one-command-per-line 276,10700
-(defcustom proof-prog-name-ask 284,10920
-(defcustom proof-prog-name-guess 290,11081
-(defcustom proof-tidy-response298,11341
-(defcustom proof-keep-response-history312,11808
-(defcustom proof-general-debug 322,12195
-(defcustom proof-experimental-features 331,12568
-(defcustom proof-follow-mode 349,13330
-(defcustom proof-auto-action-when-deactivating-scripting 375,14525
-(defcustom proof-script-command-separator 398,15476
-(defcustom proof-rsh-command 406,15769
-(defcustom proof-disappearing-proofs 422,16320
-(defgroup proof-faces 449,16970
-(defface proof-queue-face 454,17076
-(defface proof-locked-face462,17356
-(defface proof-declaration-name-face475,17859
-(defconst proof-declaration-name-face 487,18252
-(defface proof-tacticals-name-face492,18488
-(defconst proof-tacticals-name-face 501,18750
-(defface proof-tactics-name-face506,18980
-(defconst proof-tactics-name-face 515,19245
-(defface proof-error-face 520,19469
-(defface proof-warning-face528,19676
-(defconst proof-warning-face 537,19933
-(defface proof-eager-annotation-face539,19984
-(defface proof-debug-message-face547,20202
-(defface proof-boring-face555,20401
-(defface proof-mouse-highlight-face563,20593
-(defface proof-highlight-dependent-face571,20789
-(defface proof-highlight-dependency-face579,20998
-(defface proof-active-area-face 587,21195
-(defgroup prover-config 604,21471
-(defcustom proof-mode-for-shell 638,22590
-(defcustom proof-mode-for-response 645,22837
-(defcustom proof-mode-for-goals 652,23120
-(defcustom proof-mode-for-script 659,23375
-(defcustom proof-guess-command-line 670,23809
-(defcustom proof-assistant-home-page 685,24306
-(defcustom proof-context-command 691,24476
-(defcustom proof-info-command 696,24610
-(defcustom proof-showproof-command 703,24882
-(defcustom proof-goal-command 708,25018
-(defcustom proof-save-command 716,25316
-(defcustom proof-find-theorems-command 724,25626
-(defconst proof-toolbar-entries-default731,25935
-(defpgcustom toolbar-entries 765,27853
-(defcustom proof-assistant-true-value 783,28574
-(defcustom proof-assistant-false-value 789,28764
-(defcustom proof-assistant-format-int-fn 795,28958
-(defcustom proof-assistant-format-string-fn 802,29207
-(defcustom proof-assistant-setting-format 809,29474
-(defgroup proof-script 831,30169
-(defcustom proof-terminal-char 836,30299
-(defcustom proof-script-sexp-commands 846,30703
-(defcustom proof-script-command-end-regexp 857,31173
-(defcustom proof-script-command-start-regexp 875,31992
-(defcustom proof-script-use-old-parser 886,32454
-(defcustom proof-script-integral-proofs 898,32943
-(defcustom proof-script-fly-past-comments 913,33599
-(defcustom proof-script-parse-function 920,33916
-(defcustom proof-script-comment-start 938,34562
-(defcustom proof-script-comment-start-regexp 949,34997
-(defcustom proof-script-comment-end 957,35314
-(defcustom proof-script-comment-end-regexp 969,35732
-(defcustom pg-insert-output-as-comment-fn 977,36043
-(defcustom proof-string-start-regexp 983,36295
-(defcustom proof-string-end-regexp 988,36460
-(defcustom proof-case-fold-search 993,36621
-(defcustom proof-save-command-regexp 1002,37037
-(defcustom proof-save-with-hole-regexp 1007,37148
-(defcustom proof-save-with-hole-result 1019,37600
-(defcustom proof-goal-command-regexp 1030,38064
-(defcustom proof-goal-with-hole-regexp 1039,38456
-(defcustom proof-goal-with-hole-result 1051,38900
-(defcustom proof-non-undoables-regexp 1061,39299
-(defcustom proof-nested-undo-regexp 1072,39755
-(defcustom proof-ignore-for-undo-count 1088,40467
-(defcustom proof-script-next-entity-regexps 1096,40770
-(defcustom proof-script-find-next-entity-fn1140,42504
-(defcustom proof-script-imenu-generic-expression 1160,43334
-(defcustom proof-goal-command-p 1178,44189
-(defcustom proof-really-save-command-p 1205,45630
-(defcustom proof-completed-proof-behaviour 1217,46091
-(defcustom proof-count-undos-fn 1245,47451
-(defconst proof-no-command 1280,49052
-(defcustom proof-find-and-forget-fn 1285,49256
-(defcustom proof-forget-id-command 1302,49967
-(defcustom pg-topterm-goalhyplit-fn 1312,50325
-(defcustom proof-kill-goal-command 1324,50881
-(defcustom proof-undo-n-times-cmd 1338,51391
-(defcustom proof-nested-goals-history-p 1352,51940
-(defcustom proof-state-preserving-p 1361,52278
-(defcustom proof-activate-scripting-hook 1371,52748
-(defcustom proof-deactivate-scripting-hook 1390,53526
-(defcustom proof-indent 1403,53891
-(defcustom proof-indent-hang 1408,53998
-(defcustom proof-indent-enclose-offset 1413,54124
-(defcustom proof-indent-open-offset 1418,54266
-(defcustom proof-indent-close-offset 1423,54403
-(defcustom proof-indent-any-regexp 1428,54541
-(defcustom proof-indent-inner-regexp 1433,54701
-(defcustom proof-indent-enclose-regexp 1438,54855
-(defcustom proof-indent-open-regexp 1443,55009
-(defcustom proof-indent-close-regexp 1448,55161
-(defcustom proof-script-font-lock-keywords 1454,55315
-(defcustom proof-script-syntax-table-entries 1462,55638
-(defcustom proof-script-span-context-menu-extensions 1480,56035
-(defgroup proof-shell 1506,56824
-(defcustom proof-prog-name 1516,56995
-(defpgcustom prog-args 1529,57630
-(defpgcustom prog-env 1542,58205
-(defcustom proof-shell-auto-terminate-commands 1551,58631
-(defcustom proof-shell-pre-sync-init-cmd 1560,59028
-(defcustom proof-shell-init-cmd 1574,59587
-(defcustom proof-shell-restart-cmd 1585,60057
-(defcustom proof-shell-quit-cmd 1590,60212
-(defcustom proof-shell-quit-timeout 1595,60379
-(defcustom proof-shell-cd-cmd 1605,60827
-(defcustom proof-shell-start-silent-cmd 1622,61494
-(defcustom proof-shell-stop-silent-cmd 1631,61870
-(defcustom proof-shell-silent-threshold 1640,62207
-(defcustom  proof-shell-inform-file-processed-cmd 1648,62541
-(defcustom  proof-shell-inform-file-retracted-cmd 1669,63464
-(defcustom proof-auto-multiple-files 1697,64735
-(defcustom proof-cannot-reopen-processed-files 1712,65456
-(defcustom proof-shell-require-command-regexp 1726,66123
-(defcustom proof-done-advancing-require-function 1737,66585
-(defcustom proof-shell-quiet-errors 1743,66825
-(defcustom proof-shell-prompt-pattern 1756,67159
-(defcustom proof-shell-wakeup-char 1766,67581
-(defcustom proof-shell-annotated-prompt-regexp 1772,67812
-(defcustom proof-shell-abort-goal-regexp 1788,68452
-(defcustom proof-shell-error-regexp 1793,68587
-(defcustom proof-shell-truncate-before-error 1813,69381
-(defcustom pg-next-error-regexp 1827,69924
-(defcustom pg-next-error-filename-regexp 1842,70534
-(defcustom pg-next-error-extract-filename 1866,71572
-(defcustom proof-shell-interrupt-regexp 1873,71815
-(defcustom proof-shell-proof-completed-regexp 1887,72407
-(defcustom proof-shell-clear-response-regexp 1900,72915
-(defcustom proof-shell-clear-goals-regexp 1907,73214
-(defcustom proof-shell-start-goals-regexp 1914,73507
-(defcustom proof-shell-end-goals-regexp 1922,73874
-(defcustom proof-shell-eager-annotation-start 1928,74116
-(defcustom proof-shell-eager-annotation-start-length 1946,74854
-(defcustom proof-shell-eager-annotation-end 1957,75281
-(defcustom proof-shell-assumption-regexp 1973,75957
-(defcustom proof-shell-process-file 1983,76372
-(defcustom proof-shell-retract-files-regexp 2005,77324
-(defcustom proof-shell-compute-new-files-list 2014,77660
-(defcustom pg-use-specials-for-fontify 2026,78205
-(defcustom pg-special-char-regexp 2034,78553
-(defcustom proof-shell-set-elisp-variable-regexp 2040,78698
-(defcustom proof-shell-match-pgip-cmd 2073,80212
-(defcustom proof-shell-issue-pgip-cmd 2082,80542
-(defcustom proof-shell-query-dependencies-cmd 2091,80898
-(defcustom proof-shell-theorem-dependency-list-regexp 2098,81158
-(defcustom proof-shell-theorem-dependency-list-split 2114,81818
-(defcustom proof-shell-show-dependency-cmd 2123,82243
-(defcustom proof-shell-identifier-under-mouse-cmd 2130,82512
-(defcustom proof-shell-trace-output-regexp 2153,83593
-(defcustom proof-shell-thms-output-regexp 2169,84137
-(defcustom proof-shell-unicode 2182,84523
-(defcustom proof-shell-filename-escapes 2190,84851
-(defcustom proof-shell-process-connection-type 2207,85531
-(defcustom proof-shell-strip-crs-from-input 2230,86578
-(defcustom proof-shell-strip-crs-from-output 2242,87067
-(defcustom proof-shell-insert-hook 2250,87435
-(defcustom proof-pre-shell-start-hook 2290,89399
-(defcustom proof-shell-handle-delayed-output-hook2306,89871
-(defcustom proof-shell-handle-error-or-interrupt-hook2312,90086
-(defcustom proof-shell-pre-interrupt-hook2330,90835
-(defcustom proof-shell-process-output-system-specific 2338,91107
-(defcustom proof-state-change-hook 2357,91972
-(defcustom proof-shell-font-lock-keywords 2368,92354
-(defcustom proof-shell-syntax-table-entries 2376,92682
-(defgroup proof-goals 2394,93054
-(defcustom pg-subterm-first-special-char 2399,93175
-(defcustom pg-subterm-anns-use-stack 2407,93487
-(defcustom pg-goals-change-goal 2416,93791
-(defcustom pbp-goal-command 2421,93906
-(defcustom pbp-hyp-command 2426,94062
-(defcustom pg-subterm-help-cmd 2431,94224
-(defcustom pg-goals-error-regexp 2438,94460
-(defcustom proof-shell-result-start 2443,94620
-(defcustom proof-shell-result-end 2449,94854
-(defcustom pg-subterm-start-char 2455,95067
-(defcustom pg-subterm-sep-char 2469,95649
-(defcustom pg-subterm-end-char 2475,95828
-(defcustom pg-topterm-regexp 2481,95985
-(defcustom proof-goals-font-lock-keywords 2498,96588
-(defcustom proof-resp-font-lock-keywords 2512,97267
-(defcustom pg-before-fontify-output-hook 2524,97845
-(defcustom pg-after-fontify-output-hook 2532,98205
-(defgroup proof-x-symbol 2544,98459
-(defcustom proof-xsym-extra-modes 2549,98587
-(defcustom proof-xsym-font-lock-keywords 2562,99216
-(defcustom proof-xsym-activate-command 2570,99593
-(defcustom proof-xsym-deactivate-command 2577,99829
-(defpgcustom favourites 2594,100296
-(defpgcustom menu-entries 2599,100486
-(defpgcustom help-menu-entries 2606,100723
-(defpgcustom keymap 2613,100986
-(defpgcustom completion-table 2618,101157
-(defpgcustom tags-program 2628,101522
-(defcustom proof-general-name 2640,101695
-(defcustom proof-general-home-page2645,101852
-(defcustom proof-unnamed-theorem-name2651,102011
-(defcustom proof-universal-keys2657,102195
+(defalias (quote proof-x-symbol-decode-region)452,14953
+
+generic/proof-config.el,10171
+(defgroup proof-user-options 88,3165
+(defcustom proof-electric-terminator-enable 93,3279
+(defcustom proof-toolbar-enable 105,3811
+(defcustom proof-imenu-enable 111,3984
+(defcustom pg-show-hints 117,4155
+(defcustom proof-output-fontify-enable 122,4290
+(defcustom proof-trace-output-slow-catchup 132,4673
+(defcustom proof-strict-state-preserving 142,5170
+(defcustom proof-strict-read-only 155,5779
+(defcustom proof-three-window-enable 165,6129
+(defcustom proof-multiple-frames-enable 184,6879
+(defcustom proof-delete-empty-windows 193,7212
+(defcustom proof-shrink-windows-tofit 204,7743
+(defcustom proof-toolbar-use-button-enablers211,8015
+(defcustom proof-query-file-save-when-activating-scripting234,8883
+(defcustom proof-one-command-per-line253,9656
+(defcustom proof-prog-name-ask261,9875
+(defcustom proof-prog-name-guess267,10035
+(defcustom proof-tidy-response275,10294
+(defcustom proof-keep-response-history289,10757
+(defcustom proof-general-debug 299,11145
+(defcustom proof-experimental-features308,11516
+(defcustom proof-follow-mode 326,12275
+(defcustom proof-auto-action-when-deactivating-scripting 350,13455
+(defcustom proof-script-command-separator 373,14404
+(defcustom proof-rsh-command 381,14696
+(defcustom proof-disappearing-proofs 397,15246
+(defgroup proof-faces 424,15892
+(defface proof-queue-face429,15998
+(defface proof-locked-face437,16276
+(defface proof-declaration-name-face450,16779
+(defface proof-tacticals-name-face459,17065
+(defface proof-tactics-name-face468,17327
+(defface proof-error-face477,17592
+(defface proof-warning-face485,17798
+(defface proof-eager-annotation-face494,18055
+(defface proof-debug-message-face502,18273
+(defface proof-boring-face510,18472
+(defface proof-mouse-highlight-face518,18664
+(defface proof-highlight-dependent-face526,18860
+(defface proof-highlight-dependency-face534,19069
+(defface proof-active-area-face542,19266
+(defgroup prover-config 559,19541
+(defcustom proof-guess-command-line 601,20852
+(defcustom proof-assistant-home-page 616,21347
+(defcustom proof-context-command 622,21517
+(defcustom proof-info-command 627,21651
+(defcustom proof-showproof-command 634,21922
+(defcustom proof-goal-command 639,22058
+(defcustom proof-save-command 647,22355
+(defcustom proof-find-theorems-command 655,22664
+(defconst proof-toolbar-entries-default662,22974
+(defcustom proof-assistant-true-value 696,24887
+(defcustom proof-assistant-false-value 702,25077
+(defcustom proof-assistant-format-int-fn 708,25271
+(defcustom proof-assistant-format-string-fn 715,25520
+(defcustom proof-assistant-setting-format 722,25787
+(defgroup proof-script 744,26482
+(defcustom proof-terminal-char 749,26612
+(defcustom proof-script-sexp-commands 759,26999
+(defcustom proof-script-command-end-regexp 770,27456
+(defcustom proof-script-command-start-regexp 788,28275
+(defcustom proof-script-use-old-parser 799,28736
+(defcustom proof-script-integral-proofs 811,29222
+(defcustom proof-script-fly-past-comments 826,29878
+(defcustom proof-script-parse-function 831,30049
+(defcustom proof-script-comment-start 849,30692
+(defcustom proof-script-comment-start-regexp 860,31129
+(defcustom proof-script-comment-end 868,31446
+(defcustom proof-script-comment-end-regexp 880,31868
+(defcustom pg-insert-output-as-comment-fn 888,32179
+(defcustom proof-string-start-regexp 894,32431
+(defcustom proof-string-end-regexp 899,32596
+(defcustom proof-case-fold-search 904,32757
+(defcustom proof-save-command-regexp 913,33167
+(defcustom proof-save-with-hole-regexp 918,33277
+(defcustom proof-save-with-hole-result 930,33731
+(defcustom proof-goal-command-regexp 940,34182
+(defcustom proof-goal-with-hole-regexp 949,34570
+(defcustom proof-goal-with-hole-result 961,35011
+(defcustom proof-non-undoables-regexp 970,35398
+(defcustom proof-nested-undo-regexp 981,35853
+(defcustom proof-ignore-for-undo-count 997,36565
+(defcustom proof-script-next-entity-regexps 1005,36868
+(defcustom proof-script-find-next-entity-fn1049,38603
+(defcustom proof-script-imenu-generic-expression 1069,39441
+(defcustom proof-goal-command-p 1087,40294
+(defcustom proof-really-save-command-p 1114,41731
+(defcustom proof-completed-proof-behaviour 1126,42193
+(defcustom proof-count-undos-fn 1154,43549
+(defconst proof-no-command 1166,44098
+(defcustom proof-find-and-forget-fn 1171,44303
+(defcustom proof-forget-id-command 1188,45015
+(defcustom pg-topterm-goalhyplit-fn 1198,45373
+(defcustom proof-kill-goal-command 1210,45908
+(defcustom proof-undo-n-times-cmd 1224,46409
+(defcustom proof-nested-goals-history-p 1238,46957
+(defcustom proof-state-preserving-p 1247,47294
+(defcustom proof-activate-scripting-hook 1257,47764
+(defcustom proof-deactivate-scripting-hook 1276,48543
+(defcustom proof-indent 1289,48908
+(defcustom proof-indent-hang 1294,49015
+(defcustom proof-indent-enclose-offset 1299,49141
+(defcustom proof-indent-open-offset 1304,49283
+(defcustom proof-indent-close-offset 1309,49420
+(defcustom proof-indent-any-regexp 1314,49558
+(defcustom proof-indent-inner-regexp 1319,49718
+(defcustom proof-indent-enclose-regexp 1324,49872
+(defcustom proof-indent-open-regexp 1329,50026
+(defcustom proof-indent-close-regexp 1334,50178
+(defcustom proof-script-font-lock-keywords 1340,50332
+(defcustom proof-script-syntax-table-entries 1348,50661
+(defcustom proof-script-span-context-menu-extensions 1366,51058
+(defgroup proof-shell 1392,51818
+(defcustom proof-prog-name 1402,51989
+(defcustom proof-shell-auto-terminate-commands 1413,52407
+(defcustom proof-shell-pre-sync-init-cmd 1422,52804
+(defcustom proof-shell-init-cmd 1436,53362
+(defcustom proof-shell-restart-cmd 1447,53831
+(defcustom proof-shell-quit-cmd 1452,53986
+(defcustom proof-shell-quit-timeout 1457,54153
+(defcustom proof-shell-cd-cmd 1467,54601
+(defcustom proof-shell-start-silent-cmd 1484,55266
+(defcustom proof-shell-stop-silent-cmd 1493,55640
+(defcustom proof-shell-silent-threshold 1502,55973
+(defcustom  proof-shell-inform-file-processed-cmd 1510,56307
+(defcustom  proof-shell-inform-file-retracted-cmd 1531,57229
+(defcustom proof-auto-multiple-files 1559,58495
+(defcustom proof-cannot-reopen-processed-files 1574,59216
+(defcustom proof-shell-require-command-regexp 1588,59882
+(defcustom proof-done-advancing-require-function 1599,60344
+(defcustom proof-shell-quiet-errors 1605,60579
+(defcustom proof-shell-prompt-pattern 1618,60913
+(defcustom proof-shell-wakeup-char 1628,61334
+(defcustom proof-shell-annotated-prompt-regexp 1634,61565
+(defcustom proof-shell-abort-goal-regexp 1650,62199
+(defcustom proof-shell-error-regexp 1655,62334
+(defcustom proof-shell-truncate-before-error 1675,63128
+(defcustom pg-next-error-regexp 1689,63671
+(defcustom pg-next-error-filename-regexp 1704,64280
+(defcustom pg-next-error-extract-filename 1728,65313
+(defcustom proof-shell-interrupt-regexp 1735,65556
+(defcustom proof-shell-proof-completed-regexp 1749,66147
+(defcustom proof-shell-clear-response-regexp 1762,66655
+(defcustom proof-shell-clear-goals-regexp 1769,66954
+(defcustom proof-shell-start-goals-regexp 1776,67247
+(defcustom proof-shell-end-goals-regexp 1784,67614
+(defcustom proof-shell-eager-annotation-start 1790,67856
+(defcustom proof-shell-eager-annotation-start-length 1808,68591
+(defcustom proof-shell-eager-annotation-end 1819,69017
+(defcustom proof-shell-assumption-regexp 1835,69692
+(defcustom proof-shell-process-file 1845,70095
+(defcustom proof-shell-retract-files-regexp 1867,71051
+(defcustom proof-shell-compute-new-files-list 1876,71387
+(defcustom pg-use-specials-for-fontify 1888,71935
+(defcustom pg-special-char-regexp 1896,72283
+(defcustom proof-shell-set-elisp-variable-regexp 1902,72428
+(defcustom proof-shell-match-pgip-cmd 1935,73939
+(defcustom proof-shell-issue-pgip-cmd 1944,74268
+(defcustom proof-shell-query-dependencies-cmd 1953,74624
+(defcustom proof-shell-theorem-dependency-list-regexp 1960,74884
+(defcustom proof-shell-theorem-dependency-list-split 1976,75544
+(defcustom proof-shell-show-dependency-cmd 1985,75967
+(defcustom proof-shell-identifier-under-mouse-cmd 1992,76236
+(defcustom proof-shell-trace-output-regexp 2015,77317
+(defcustom proof-shell-thms-output-regexp 2029,77775
+(defcustom proof-shell-unicode 2042,78161
+(defcustom proof-shell-filename-escapes 2050,78481
+(defcustom proof-shell-process-connection-type2067,79161
+(defcustom proof-shell-strip-crs-from-input 2090,80207
+(defcustom proof-shell-strip-crs-from-output 2102,80692
+(defcustom proof-shell-insert-hook 2110,81060
+(defcustom proof-shell-handle-delayed-output-hook2150,83017
+(defcustom proof-shell-handle-error-or-interrupt-hook2156,83232
+(defcustom proof-shell-pre-interrupt-hook2174,83981
+(defcustom proof-shell-process-output-system-specific 2182,84253
+(defcustom proof-state-change-hook 2201,85117
+(defcustom proof-shell-font-lock-keywords 2212,85499
+(defcustom proof-shell-syntax-table-entries 2220,85831
+(defgroup proof-goals 2238,86203
+(defcustom pg-subterm-first-special-char 2243,86324
+(defcustom pg-subterm-anns-use-stack 2251,86636
+(defcustom pg-goals-change-goal 2260,86935
+(defcustom pbp-goal-command 2265,87051
+(defcustom pbp-hyp-command 2270,87207
+(defcustom pg-subterm-help-cmd 2275,87369
+(defcustom pg-goals-error-regexp 2282,87605
+(defcustom proof-shell-result-start 2287,87765
+(defcustom proof-shell-result-end 2293,87999
+(defcustom pg-subterm-start-char 2299,88212
+(defcustom pg-subterm-sep-char 2313,88792
+(defcustom pg-subterm-end-char 2319,88971
+(defcustom pg-topterm-regexp 2325,89128
+(defcustom proof-goals-font-lock-keywords 2342,89730
+(defcustom proof-resp-font-lock-keywords 2356,90415
+(defcustom pg-before-fontify-output-hook 2368,90995
+(defcustom pg-after-fontify-output-hook 2376,91355
+(defgroup proof-x-symbol 2388,91635
+(defcustom proof-xsym-extra-modes 2393,91763
+(defcustom proof-xsym-font-lock-keywords 2406,92391
+(defcustom proof-xsym-activate-command 2414,92768
+(defcustom proof-xsym-deactivate-command 2421,93003
+(defcustom proof-general-name 2438,93288
+(defcustom proof-general-home-page2443,93445
+(defcustom proof-unnamed-theorem-name2449,93605
+(defcustom proof-universal-keys2455,93789
 
 generic/proof-depends.el,824
 (defvar proof-thm-names-of-files 19,540
@@ -1638,520 +1681,505 @@ generic/proof-depends.el,824
 (defun proof-depends-module-of 44,1570
 (defun proof-depends-names-in-same-file 52,1864
 (defun proof-depends-process-dependencies 71,2484
-(defun proof-dependency-in-span-context-menu 124,4226
-(defun proof-dep-alldeps-menu 147,5129
-(defun proof-dep-make-alldeps-menu 153,5356
-(defun proof-dep-split-deps 171,5852
-(defun proof-dep-make-submenu 192,6551
-(defun proof-make-highlight-depts-menu 202,6904
-(defun proof-goto-dependency 212,7208
-(defun proof-show-dependency 218,7431
-(defconst pg-dep-span-priority 225,7721
-(defconst pg-ordinary-span-priority 226,7757
-(defun proof-highlight-depcs 228,7799
-(defun proof-highlight-depts 238,8229
-(defun proof-dep-unhighlight 249,8703
+(defun proof-dependency-in-span-context-menu 124,4231
+(defun proof-dep-alldeps-menu 147,5134
+(defun proof-dep-make-alldeps-menu 153,5361
+(defun proof-dep-split-deps 171,5857
+(defun proof-dep-make-submenu 192,6556
+(defun proof-make-highlight-depts-menu 202,6909
+(defun proof-goto-dependency 212,7213
+(defun proof-show-dependency 218,7436
+(defconst pg-dep-span-priority 225,7726
+(defconst pg-ordinary-span-priority 226,7762
+(defun proof-highlight-depcs 228,7804
+(defun proof-highlight-depts 238,8234
+(defun proof-dep-unhighlight 249,8708
 
 generic/proof-easy-config.el,192
-(defconst proof-easy-config-derived-modes-table15,492
-(defun proof-easy-config-define-derived-modes 22,898
-(defun proof-easy-config-check-setup 59,2510
-(defmacro proof-easy-config 91,3835
-
-generic/proof.el,543
-(deflocal proof-buffer-type 35,900
-(defvar proof-shell-busy 38,1013
-(defvar proof-included-files-list 43,1169
-(defvar proof-script-buffer 66,2185
-(defvar proof-previous-script-buffer 70,2325
-(defvar proof-shell-buffer 75,2579
-(defvar proof-goals-buffer 78,2665
-(defvar proof-response-buffer 81,2720
-(defvar proof-trace-buffer 84,2781
-(defvar proof-thms-buffer 88,2935
-(defvar proof-shell-error-or-interrupt-seen 92,3090
-(defvar proof-shell-proof-completed 97,3315
-(defvar proof-terminal-string 109,3860
-(defun unload-pg 123,4064
-
-generic/proof-indent.el,219
-(defun proof-indent-indent 13,353
-(defun proof-indent-offset 22,619
-(defun proof-indent-inner-p 39,1219
-(defun proof-indent-goto-prev 48,1526
-(defun proof-indent-calculate 55,1859
-(defun proof-indent-line 74,2575
+(defconst proof-easy-config-derived-modes-table14,475
+(defun proof-easy-config-define-derived-modes 21,881
+(defun proof-easy-config-check-setup 54,2291
+(defmacro proof-easy-config 86,3616
+
+generic/proof.el,516
+(deflocal proof-buffer-type 35,973
+(defvar proof-shell-busy 38,1086
+(defvar proof-included-files-list 43,1242
+(defvar proof-script-buffer 66,2256
+(defvar proof-previous-script-buffer 70,2396
+(defvar proof-shell-buffer 75,2650
+(defvar proof-goals-buffer 78,2736
+(defvar proof-response-buffer 81,2791
+(defvar proof-trace-buffer 84,2852
+(defvar proof-thms-buffer 88,3006
+(defvar proof-shell-error-or-interrupt-seen 92,3161
+(defvar proof-shell-proof-completed 97,3385
+(defvar proof-terminal-string 109,3930
+
+generic/proof-indent.el,218
+(defun proof-indent-indent 9,226
+(defun proof-indent-offset 18,492
+(defun proof-indent-inner-p 35,1092
+(defun proof-indent-goto-prev 44,1399
+(defun proof-indent-calculate 51,1732
+(defun proof-indent-line 70,2448
 
 generic/proof-maths-menu.el,134
-(defun proof-maths-menu-support-available 24,782
-(defun proof-maths-menu-set-global 37,1275
-(defun proof-maths-menu-enable 51,1731
-
-generic/proof-menu.el,2787
-(defvar proof-display-some-buffers-count 21,543
-(defun proof-display-some-buffers 23,588
-(defun proof-menu-define-keys 82,2790
-(define-key map 85,2938
-(define-key map 86,2990
-(define-key map 87,3041
-(define-key map 88,3094
-(define-key map 89,3148
-(define-key map 90,3210
-(define-key map 91,3270
-(define-key map 92,3332
-(define-key map 95,3505
-(define-key map 99,3742
-(define-key map 100,3796
-(define-key map 101,3861
-(define-key map 102,3935
-(define-key map 105,4116
-(define-key map 106,4182
-(define-key map 109,4388
-(define-key map 110,4454
-(define-key map 112,4569
-(define-key map 113,4632
-(define-key map 115,4717
-(define-key map 122,5043
-(define-key map 123,5102
-(defun proof-menu-define-main 143,5692
-(defun proof-menu-define-specific 153,5893
-(defun proof-assistant-menu-update 188,6911
-(defvar proof-help-menu205,7519
-(defvar proof-show-hide-menu213,7797
-(defvar proof-buffer-menu222,8110
-(defun proof-keep-response-history 277,10207
-(defconst proof-quick-opts-menu285,10517
-(defun proof-quick-opts-vars 412,15579
-(defun proof-quick-opts-changed-from-defaults-p 437,16330
-(defun proof-quick-opts-changed-from-saved-p 441,16435
-(defun proof-quick-opts-save 452,16787
-(defun proof-quick-opts-reset 457,16955
-(defconst proof-config-menu469,17223
-(defconst proof-advanced-menu476,17402
-(defvar proof-menu 489,17837
-(defvar proof-main-menu498,18121
-(defvar proof-aux-menu508,18347
-(defvar proof-menu-favourites 524,18669
-(defun proof-menu-define-favourites-menu 527,18776
-(defmacro proof-defshortcut 548,19447
-(defmacro proof-definvisible 564,20102
-(defun proof-def-favourite 585,20927
-(defvar proof-make-favourite-cmd-history 608,21902
-(defvar proof-make-favourite-menu-history 611,21987
-(defun proof-save-favourites 614,22073
-(defun proof-del-favourite 619,22221
-(defun proof-read-favourite 636,22782
-(defun proof-add-favourite 661,23585
-(defvar proof-assistant-settings 688,24636
-(defvar proof-menu-settings 695,24999
-(defun proof-menu-define-settings-menu 698,25073
-(defun proof-menu-entry-name 718,25817
-(defun proof-menu-entry-for-setting 730,26289
-(defun proof-settings-vars 748,26779
-(defun proof-settings-changed-from-defaults-p 753,26956
-(defun proof-settings-changed-from-saved-p 757,27062
-(defun proof-settings-save 761,27165
-(defun proof-settings-reset 766,27332
-(defun proof-defpacustom-fn 774,27578
-(defmacro defpacustom 850,30462
-(defun proof-assistant-invisible-command-ifposs 861,31103
-(defun proof-maybe-askprefs 883,32078
-(defun proof-assistant-settings-cmd 890,32282
-(defun proof-assistant-format 907,32942
-(defvar proof-assistant-format-table 931,34001
-(defun proof-assistant-format-bool 939,34370
-(defun proof-assistant-format-int 942,34483
-(defun proof-assistant-format-string 945,34575
+(defun proof-maths-menu-support-available 25,858
+(defun proof-maths-menu-set-global 36,1287
+(defun proof-maths-menu-enable 50,1743
+
+generic/proof-menu.el,2146
+(defvar proof-display-some-buffers-count 21,508
+(defun proof-display-some-buffers 23,553
+(defun proof-menu-define-keys 82,2755
+(defun proof-menu-define-main 144,5730
+(defun proof-menu-define-specific 154,5933
+(defun proof-assistant-menu-update 192,6959
+(defvar proof-help-menu208,7542
+(defvar proof-show-hide-menu216,7820
+(defvar proof-buffer-menu225,8133
+(defun proof-keep-response-history 280,10230
+(defconst proof-quick-opts-menu288,10540
+(defun proof-quick-opts-vars 415,15605
+(defun proof-quick-opts-changed-from-defaults-p 440,16356
+(defun proof-quick-opts-changed-from-saved-p 444,16461
+(defun proof-quick-opts-save 455,16813
+(defun proof-quick-opts-reset 460,16981
+(defconst proof-config-menu472,17249
+(defconst proof-advanced-menu479,17428
+(defvar proof-menu 492,17863
+(defun proof-main-menu 501,18147
+(defun proof-aux-menu 512,18413
+(defvar proof-menu-favourites 529,18791
+(defun proof-menu-define-favourites-menu 532,18898
+(defun proof-def-favourite 552,19554
+(defvar proof-make-favourite-cmd-history 575,20529
+(defvar proof-make-favourite-menu-history 578,20614
+(defun proof-save-favourites 581,20700
+(defun proof-del-favourite 586,20848
+(defun proof-read-favourite 603,21409
+(defun proof-add-favourite 628,22212
+(defvar proof-assistant-settings 655,23263
+(defvar proof-menu-settings 662,23626
+(defun proof-menu-define-settings-menu 665,23700
+(defun proof-menu-entry-name 685,24444
+(defun proof-menu-entry-for-setting 697,24916
+(defun proof-settings-vars 715,25406
+(defun proof-settings-changed-from-defaults-p 720,25583
+(defun proof-settings-changed-from-saved-p 724,25689
+(defun proof-settings-save 728,25792
+(defun proof-settings-reset 733,25959
+(defun proof-defpacustom-fn 741,26205
+(defmacro defpacustom 817,29089
+(defun proof-assistant-invisible-command-ifposs 828,29730
+(defun proof-maybe-askprefs 850,30705
+(defun proof-assistant-settings-cmd 857,30909
+(defun proof-assistant-format 874,31569
+(defvar proof-assistant-format-table 898,32628
+(defun proof-assistant-format-bool 906,32997
+(defun proof-assistant-format-int 909,33110
+(defun proof-assistant-format-string 912,33202
 
 generic/proof-mmm.el,113
-(defun proof-mmm-support-available 27,933
-(defun proof-mmm-set-global 53,1833
-(defun proof-mmm-enable 68,2374
-
-generic/proof-script.el,5105
-(defvar proof-last-theorem-dependencies 41,1047
-(defvar proof-nesting-depth 45,1209
-(defvar proof-element-counters 52,1440
-(deflocal proof-active-buffer-fake-minor-mode 58,1580
-(deflocal proof-script-buffer-file-name 61,1706
-(defun proof-next-element-count 75,2230
-(defun proof-element-id 84,2557
-(defun proof-next-element-id 88,2726
-(deflocal proof-script-last-entity 102,3042
-(defun proof-script-find-next-entity 109,3322
-(deflocal proof-locked-span 185,6064
-(deflocal proof-queue-span 192,6330
-(defun proof-span-read-only 204,6844
-(defun proof-strict-read-only 211,7101
-(defsubst proof-set-queue-endpoints 226,7771
-(defsubst proof-set-locked-endpoints 230,7912
-(defsubst proof-detach-queue 234,8056
-(defsubst proof-detach-locked 238,8188
-(defsubst proof-set-queue-start 242,8324
-(defsubst proof-set-locked-end 246,8450
-(defsubst proof-set-queue-end 261,9029
-(defun proof-init-segmentation 271,9285
-(defun proof-restart-buffers 303,10656
-(defun proof-script-buffers-with-spans 325,11578
-(defun proof-script-remove-all-spans-and-deactivate 335,11934
-(defun proof-script-clear-queue-spans 339,12122
-(defun proof-unprocessed-begin 357,12663
-(defun proof-script-end 365,12917
-(defun proof-queue-or-locked-end 374,13218
-(defun proof-locked-end 388,13881
-(defun proof-locked-region-full-p 404,14251
-(defun proof-locked-region-empty-p 412,14508
-(defun proof-only-whitespace-to-locked-region-p 416,14658
-(defun proof-in-locked-region-p 429,15294
-(defun proof-goto-end-of-locked 441,15557
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 458,16316
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 469,16797
-(defun proof-end-of-locked-visible-p 483,17450
-(defun proof-goto-end-of-queue-or-locked-if-not-visible 492,17901
-(defvar pg-idioms 511,18551
-(defvar pg-visibility-specs 514,18647
-(deflocal pg-script-portions 519,18854
-(defun pg-clear-script-portions 522,18976
-(defun pg-add-script-element 536,19505
-(defun pg-remove-script-element 539,19581
-(defsubst pg-visname 547,19859
-(defun pg-add-element 551,20004
-(defun pg-open-invisible-span 585,21633
-(defun pg-remove-element 596,21996
-(defun pg-make-element-invisible 603,22266
-(defun pg-make-element-visible 609,22523
-(defun pg-toggle-element-visibility 614,22702
-(defun pg-redisplay-for-gnuemacs 622,23032
-(defun pg-show-all-portions 629,23303
-(defun pg-show-all-proofs 647,23974
-(defun pg-hide-all-proofs 652,24102
-(defun pg-add-proof-element 657,24233
-(defun pg-span-name 671,24853
-(defun pg-set-span-helphighlights 692,25560
-(defun proof-complete-buffer-atomic 717,26384
-(defun proof-register-possibly-new-processed-file 758,28299
-(defun proof-inform-prover-file-retracted 809,30427
-(defun proof-auto-retract-dependencies 828,31213
-(defun proof-unregister-buffer-file-name 882,33753
-(defun proof-protected-process-or-retract 928,35576
-(defun proof-deactivate-scripting-auto 955,36746
-(defun proof-deactivate-scripting 964,37104
-(defun proof-activate-scripting 1101,42509
-(defun proof-toggle-active-scripting 1229,48263
-(defun proof-done-advancing 1270,49624
-(defun proof-done-advancing-comment 1356,52991
-(defun proof-done-advancing-save 1375,53733
-(defun proof-make-goalsave 1468,57348
-(defun proof-get-name-from-goal 1483,58091
-(defun proof-done-advancing-autosave 1502,59117
-(defun proof-done-advancing-other 1567,61663
-(defun proof-segment-up-to-parser 1595,62622
-(defun proof-script-generic-parse-find-comment-end 1658,64698
-(defun proof-script-generic-parse-cmdend 1667,65114
-(defun proof-script-generic-parse-cmdstart 1692,66009
-(defun proof-script-generic-parse-sexp 1755,68717
-(defun proof-cmdstart-add-segment-for-cmd 1779,69653
-(defun proof-segment-up-to-cmdstart 1831,71852
-(defun proof-segment-up-to-cmdend 1892,74212
-(defun proof-semis-to-vanillas 1963,76859
-(defun proof-script-new-command-advance 2002,78185
-(defun proof-script-next-command-advance 2044,79926
-(defun proof-assert-until-point-interactive 2056,80367
-(defun proof-assert-until-point 2082,81489
-(defun proof-assert-next-command2135,83921
-(defun proof-goto-point 2183,86184
-(defun proof-insert-pbp-command 2200,86710
-(defun proof-done-retracting 2233,87823
-(defun proof-setup-retract-action 2260,88934
-(defun proof-last-goal-or-goalsave 2270,89417
-(defun proof-retract-target 2293,90257
-(defun proof-retract-until-point-interactive 2378,93898
-(defun proof-retract-until-point 2386,94283
-(define-derived-mode proof-mode 2431,96144
-(defun proof-script-set-visited-file-name 2480,98111
-(defun proof-script-set-buffer-hooks 2504,99113
-(defun proof-script-kill-buffer-fn 2514,99609
-(defun proof-config-done-related 2558,101431
-(defun proof-generic-goal-command-p 2630,103999
-(defun proof-generic-state-preserving-p 2635,104211
-(defun proof-generic-count-undos 2644,104728
-(defun proof-generic-find-and-forget 2673,105758
-(defconst proof-script-important-settings2724,107583
-(defun proof-config-done 2737,108120
-(defun proof-setup-parsing-mechanism 2834,111668
-(defun proof-setup-imenu 2878,113521
-(defun proof-setup-func-menu 2895,114126
-
-generic/proof-shell.el,3390
-(defvar proof-shell-last-output 19,457
-(defvar proof-marker 63,1713
-(defvar proof-action-list 66,1810
-(defvar proof-shell-silent 74,1986
-(defvar proof-shell-last-prompt 88,2469
-(defvar proof-shell-last-output-kind 93,2699
-(defvar proof-shell-delayed-output 114,3521
-(defvar proof-shell-delayed-output-kind 117,3642
-(defcustom proof-shell-active-scripting-indicator126,3845
-(defun proof-shell-ready-prover 179,5321
-(defun proof-shell-live-buffer 193,5861
-(defun proof-shell-available-p 200,6096
-(defun proof-grab-lock 206,6319
-(defun proof-release-lock 223,7036
-(defcustom proof-shell-fiddle-frames 243,7592
-(deflocal proof-eagerly-raise 250,7833
-(defun proof-shell-set-text-representation 253,7939
-(defun proof-shell-start 266,8494
-(defvar proof-shell-kill-function-hooks 485,16486
-(defun proof-shell-kill-function 488,16584
-(defun proof-shell-clear-state 577,20387
-(defun proof-shell-exit 592,20830
-(defun proof-shell-bail-out 604,21275
-(defun proof-shell-restart 613,21752
-(defvar proof-shell-no-response-display 655,23136
-(defvar proof-shell-urgent-message-marker 658,23240
-(defvar proof-shell-urgent-message-scanner 661,23361
-(defun proof-shell-handle-output 665,23488
-(defun proof-shell-handle-delayed-output 730,26341
-(defvar proof-shell-no-error-display 765,27763
-(defun proof-shell-handle-error 771,27969
-(defun proof-shell-handle-interrupt 789,28805
-(defun proof-shell-error-or-interrupt-action 803,29427
-(defun proof-goals-pos 830,30632
-(defun proof-pbp-focus-on-first-goal 835,30837
-(defsubst proof-shell-string-match-safe 847,31372
-(defun proof-shell-process-output 852,31540
-(defvar proof-shell-insert-space-fudge 963,36180
-(defun proof-shell-insert 972,36489
-(defun proof-shell-command-queue-item 1046,39401
-(defun proof-shell-set-silent 1051,39558
-(defun proof-shell-start-silent-item 1057,39777
-(defun proof-shell-clear-silent 1063,39969
-(defun proof-shell-stop-silent-item 1069,40191
-(defun proof-shell-should-be-silent 1076,40463
-(defun proof-append-alist 1089,41019
-(defun proof-start-queue 1148,43256
-(defun proof-extend-queue 1159,43605
-(defun proof-shell-exec-loop 1170,43986
-(defun proof-shell-insert-loopback-cmd 1235,46574
-(defun proof-shell-message 1263,47900
-(defun proof-shell-process-urgent-message 1269,48116
-(defvar proof-shell-minibuffer-urgent-interactive-input-history 1481,57074
-(defun proof-shell-minibuffer-urgent-interactive-input 1483,57144
-(defun proof-shell-process-urgent-messages 1495,57514
-(defun proof-shell-filter 1568,60685
-(defun proof-shell-filter-process-output 1727,67274
-(defvar pg-last-tracing-output-time 1780,69328
-(defvar pg-tracing-slow-mode 1783,69434
-(defconst pg-slow-mode-duration 1786,69523
-(defconst pg-fast-tracing-mode-threshold 1789,69605
-(defvar pg-tracing-cleanup-timer 1792,69733
-(defun pg-tracing-tight-loop 1794,69772
-(defun pg-finish-tracing-display 1837,71490
-(defun proof-shell-dont-show-annotations 1850,71796
-(defun proof-shell-show-annotations 1866,72331
-(defun proof-shell-wait 1887,72828
-(defun proof-done-invisible 1907,73738
-(defun proof-shell-invisible-command 1950,75461
-(defun proof-shell-invisible-cmd-get-result 1983,76711
-(defun proof-shell-invisible-command-invisible-result 2000,77392
-(define-derived-mode proof-shell-mode 2020,77896
-(defconst proof-shell-important-settings2091,80567
-(defun proof-shell-config-done 2096,80667
-
-generic/proof-site.el,719
-(defgroup proof-general 20,594
-(defgroup proof-general-internals 32,994
-(defun proof-home-directory-fn 43,1234
-(defcustom proof-home-directory54,1604
-(defcustom proof-images-directory63,1970
-(defcustom proof-info-directory69,2171
-(defcustom proof-assistant-table98,3420
-(defun proof-string-to-list 160,5417
-(defcustom proof-assistants 176,5908
-(defun proof-ready-for-assistant 212,7321
-(defconst proof-general-version 325,11540
-(defconst proof-general-short-version 328,11681
-(defconst proof-general-version-year 333,11841
-(defcustom proof-assistant-cusgrp 347,12309
-(defcustom proof-assistant-internals-cusgrp 355,12612
-(defcustom proof-assistant 363,12924
-(defcustom proof-assistant-symbol 371,13193
-
-generic/proof-splash.el,727
-(defcustom proof-splash-enable 16,433
-(defcustom proof-splash-time 21,585
-(defcustom proof-splash-contents29,870
-(defconst proof-splash-startup-msg 58,1985
-(defconst proof-splash-welcome 67,2364
-(defun proof-get-image 85,2900
-(defvar proof-splash-timeout-conf 125,4263
-(defun proof-splash-centre-spaces 128,4376
-(defun proof-splash-remove-screen 156,5545
-(defun proof-splash-remove-buffer 176,6271
-(defvar proof-splash-seen 192,6935
-(defun proof-splash-display-screen 196,7052
-(defun proof-splash-message 271,10211
-(defun proof-splash-timeout-waiter 281,10574
-(defvar proof-splash-old-frame-title-format 298,11313
-(defun proof-splash-set-frame-titles 300,11363
-(defun proof-splash-unset-frame-titles 309,11679
-
-generic/proof-syntax.el,972
-(defun proof-ids-to-regexp 16,445
-(defun proof-anchor-regexp 22,701
-(defconst proof-no-regexp26,803
-(defun proof-regexp-alt 31,898
-(defun proof-regexp-region 40,1184
-(defun proof-re-search-forward-region 49,1607
-(defun proof-search-forward 62,2102
-(defun proof-replace-regexp-in-string 68,2354
-(defun proof-re-search-forward 74,2608
-(defun proof-re-search-backward 80,2869
-(defun proof-string-match 86,3133
-(defun proof-string-match-safe 92,3365
-(defun proof-stringfn-match 96,3570
-(defun proof-looking-at 103,3830
-(defun proof-looking-at-safe 109,4020
-(defun proof-looking-at-syntactic-context 113,4160
-(defun proof-replace-string 125,4523
-(defun proof-replace-regexp 130,4724
-(defun proof-replace-regexp-nocasefold 135,4930
-(defvar proof-id 143,5209
-(defun proof-ids 149,5429
-(defun proof-zap-commas 162,5990
-(defun proof-format 180,6559
-(defun proof-format-filename 199,7198
-(defun proof-insert 248,8676
-(defun proof-splice-separator 284,9685
-
-generic/proof-toolbar.el,2877
-(defun proof-toolbar-function 49,1595
-(defun proof-toolbar-icon 52,1692
-(defun proof-toolbar-enabler 55,1793
-(defun proof-toolbar-function-with-enabler 58,1901
-(defun proof-toolbar-make-icon 65,2074
-(defun proof-toolbar-make-toolbar-item 83,2674
-(defvar proof-toolbar 122,4055
-(deflocal proof-toolbar-itimer 126,4184
-(defun proof-toolbar-setup 130,4294
-(defun proof-toolbar-build 174,5861
-(defalias 'proof-toolbar-enable proof-toolbar-enable
239,8074
-(defun proof-toolbar-setup-refresh 248,8313
-(defun proof-toolbar-disable-refresh 269,9083
-(deflocal proof-toolbar-refresh-flag 276,9405
-(defun proof-toolbar-refresh 282,9676
-(defvar proof-toolbar-enablers286,9821
-(defvar proof-toolbar-enablers-last-state292,9997
-(defun proof-toolbar-really-refresh 296,10088
-(defun proof-toolbar-undo-enable-p 349,11918
-(defalias 'proof-toolbar-undo proof-toolbar-undo
354,12066
-(defun proof-toolbar-delete-enable-p 360,12185
-(defalias 'proof-toolbar-delete proof-toolbar-delete
366,12359
-(defun proof-toolbar-lockedend-enable-p 373,12495
-(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
376,12545
-(defun proof-toolbar-next-enable-p 385,12633
-(defalias 'proof-toolbar-next proof-toolbar-next
389,12740
-(defun proof-toolbar-goto-enable-p 396,12834
-(defalias 'proof-toolbar-goto proof-toolbar-goto
399,12907
-(defun proof-toolbar-retract-enable-p 406,12983
-(defalias 'proof-toolbar-retract proof-toolbar-retract
410,13094
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
417,13173
-(defalias 'proof-toolbar-use proof-toolbar-use
418,13241
-(defun proof-toolbar-restart-enable-p 424,13319
-(defalias 'proof-toolbar-restart proof-toolbar-restart
429,13480
-(defun proof-toolbar-goal-enable-p 435,13558
-(defalias 'proof-toolbar-goal proof-toolbar-goal
442,13791
-(defun proof-toolbar-qed-enable-p 449,13863
-(defalias 'proof-toolbar-qed proof-toolbar-qed
455,14015
-(defun proof-toolbar-state-enable-p 461,14087
-(defalias 'proof-toolbar-state proof-toolbar-state
464,14158
-(defun proof-toolbar-context-enable-p 470,14227
-(defalias 'proof-toolbar-context proof-toolbar-context
473,14300
-(defun proof-toolbar-info-enable-p 481,14460
-(defalias 'proof-toolbar-info proof-toolbar-info
484,14504
-(defun proof-toolbar-command-enable-p 490,14573
-(defalias 'proof-toolbar-command proof-toolbar-command
493,14644
-(defun proof-toolbar-help-enable-p 499,14724
-(defun proof-toolbar-help 502,14769
-(defun proof-toolbar-find-enable-p 510,14863
-(defalias 'proof-toolbar-find proof-toolbar-find
513,14932
-(defun proof-toolbar-visibility-enable-p 519,15030
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
522,15130
-(defun proof-toolbar-interrupt-enable-p 528,15218
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
531,15282
-(defun proof-toolbar-make-menu-item 540,15471
-(defconst proof-toolbar-scripting-menu562,16159
-
-generic/proof-utils.el,2102
-(defmacro deflocal 19,531
-(defmacro proof-with-current-buffer-if-exists 26,769
-(defmacro proof-with-script-buffer 35,1146
-(defmacro proof-map-buffers 46,1533
-(defmacro proof-sym 51,1718
-(defun proof-try-require 56,1879
-(defmacro proof-face-specs 63,2073
-(defun proof-save-some-buffers 85,2728
-(defun proof-set-value 109,3419
-(defun proof-ass-symv 169,5596
-(defmacro proof-ass-sym 174,5783
-(defun proof-defpgcustom-fn 178,5922
-(defun undefpgcustom 203,7006
-(defmacro defpgcustom 209,7230
-(defmacro proof-ass 218,7647
-(defun proof-defpgdefault-fn 223,7823
-(defmacro defpgdefault 237,8282
-(defmacro defpgfun 248,8644
-(defun proof-file-truename 263,8938
-(defun proof-file-to-buffer 267,9121
-(defun proof-files-to-buffers 278,9450
-(defun proof-buffers-in-mode 285,9733
-(defun pg-save-from-death 299,10184
-(defun proof-define-keys 318,10802
-(deflocal proof-font-lock-keywords 347,11803
-(deflocal proof-font-lock-keywords-case-fold-search 353,12068
-(defun proof-font-lock-configure-defaults 356,12191
-(defun proof-font-lock-clear-font-lock-vars 404,14504
-(defun proof-font-lock-set-font-lock-vars 415,14877
-(defun proof-fontify-region 422,15090
-(defun pg-remove-specials 480,17318
-(defun pg-remove-specials-in-string 490,17657
-(defun proof-fontify-buffer 497,17844
-(defun proof-warn-if-unset 510,18085
-(defun proof-get-window-for-buffer 515,18303
-(defun proof-display-and-keep-buffer 566,20617
-(defun proof-clean-buffer 598,21926
-(defun proof-message 613,22547
-(defun proof-warning 618,22760
-(defun pg-internal-warning 624,23042
-(defun proof-debug 632,23361
-(defun proof-switch-to-buffer 647,24032
-(defun proof-resize-window-tofit 680,25724
-(defun proof-submit-bug-report 780,29736
-(defun proof-deftoggle-fn 816,31124
-(defmacro proof-deftoggle 831,31779
-(defun proof-defintset-fn 838,32153
-(defmacro proof-defintset 854,32861
-(defun proof-defstringset-fn 861,33238
-(defmacro proof-defstringset 874,33865
-(defun pg-custom-save-vars 888,34330
-(defun pg-custom-reset-vars 906,35056
-(defun proof-locate-executable 919,35393
-(defconst proof-extra-fls948,36574
-
-generic/proof-x-symbol.el,653
-(defpgcustom x-symbol-language 52,2063
-(defvar proof-x-symbol-initialized 57,2285
-(defun proof-x-symbol-tokenlang-file 60,2380
-(defun proof-x-symbol-support-maybe-available 66,2562
-(defun proof-x-symbol-initialize 86,3312
-(defun proof-x-symbol-enable 177,6973
-(defun proof-x-symbol-refresh-output-buffers 207,8290
-(defun proof-x-symbol-mode-associated-buffers 222,9044
-(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
244,9748
-(defun proof-x-symbol-encode-shell-input 246,9814
-(defun proof-x-symbol-set-language 263,10405
-(defun proof-x-symbol-shell-config 268,10576
-(defun proof-x-symbol-config-output-buffer 316,12743
+(defun proof-mmm-support-available 30,995
+(defun proof-mmm-set-global 54,1843
+(defun proof-mmm-enable 69,2384
+
+generic/proof-script.el,5103
+(defvar proof-last-theorem-dependencies 36,964
+(defvar proof-nesting-depth 40,1126
+(defvar proof-element-counters 47,1357
+(deflocal proof-active-buffer-fake-minor-mode 53,1497
+(deflocal proof-script-buffer-file-name 56,1623
+(defun proof-next-element-count 70,2147
+(defun proof-element-id 79,2474
+(defun proof-next-element-id 83,2643
+(deflocal proof-script-last-entity 97,2960
+(defun proof-script-find-next-entity 104,3240
+(deflocal proof-locked-span 180,5982
+(deflocal proof-queue-span 187,6248
+(defun proof-span-read-only 199,6762
+(defun proof-strict-read-only 206,7019
+(defsubst proof-set-queue-endpoints 221,7689
+(defsubst proof-set-locked-endpoints 225,7830
+(defsubst proof-detach-queue 229,7974
+(defsubst proof-detach-locked 233,8106
+(defsubst proof-set-queue-start 237,8242
+(defsubst proof-set-locked-end 241,8368
+(defsubst proof-set-queue-end 256,8947
+(defun proof-init-segmentation 266,9203
+(defun proof-restart-buffers 298,10574
+(defun proof-script-buffers-with-spans 320,11506
+(defun proof-script-remove-all-spans-and-deactivate 330,11862
+(defun proof-script-clear-queue-spans 334,12050
+(defun proof-unprocessed-begin 352,12596
+(defun proof-script-end 360,12850
+(defun proof-queue-or-locked-end 369,13151
+(defun proof-locked-end 383,13814
+(defun proof-locked-region-full-p 399,14184
+(defun proof-locked-region-empty-p 407,14441
+(defun proof-only-whitespace-to-locked-region-p 411,14591
+(defun proof-in-locked-region-p 424,15227
+(defun proof-goto-end-of-locked 436,15490
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 453,16249
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 464,16730
+(defun proof-end-of-locked-visible-p 478,17383
+(defun proof-goto-end-of-queue-or-locked-if-not-visible 487,17834
+(defvar pg-idioms 506,18484
+(defvar pg-visibility-specs 509,18580
+(deflocal pg-script-portions 514,18787
+(defun pg-clear-script-portions 517,18909
+(defun pg-add-script-element 531,19438
+(defun pg-remove-script-element 534,19514
+(defsubst pg-visname 542,19792
+(defun pg-add-element 546,19937
+(defun pg-open-invisible-span 580,21566
+(defun pg-remove-element 591,21929
+(defun pg-make-element-invisible 598,22199
+(defun pg-make-element-visible 604,22456
+(defun pg-toggle-element-visibility 609,22635
+(defun pg-redisplay-for-gnuemacs 617,22965
+(defun pg-show-all-portions 624,23236
+(defun pg-show-all-proofs 642,23907
+(defun pg-hide-all-proofs 647,24035
+(defun pg-add-proof-element 652,24166
+(defun pg-span-name 666,24786
+(defun pg-set-span-helphighlights 687,25493
+(defun proof-complete-buffer-atomic 712,26317
+(defun proof-register-possibly-new-processed-file 753,28232
+(defun proof-inform-prover-file-retracted 804,30360
+(defun proof-auto-retract-dependencies 823,31146
+(defun proof-unregister-buffer-file-name 877,33686
+(defun proof-protected-process-or-retract 923,35509
+(defun proof-deactivate-scripting-auto 950,36679
+(defun proof-deactivate-scripting 959,37037
+(defun proof-activate-scripting 1096,42442
+(defun proof-toggle-active-scripting 1224,48196
+(defun proof-done-advancing 1265,49557
+(defun proof-done-advancing-comment 1351,52924
+(defun proof-done-advancing-save 1370,53666
+(defun proof-make-goalsave 1463,57281
+(defun proof-get-name-from-goal 1478,58024
+(defun proof-done-advancing-autosave 1497,59050
+(defun proof-done-advancing-other 1562,61596
+(defun proof-segment-up-to-parser 1590,62555
+(defun proof-script-generic-parse-find-comment-end 1653,64631
+(defun proof-script-generic-parse-cmdend 1662,65047
+(defun proof-script-generic-parse-cmdstart 1687,65942
+(defun proof-script-generic-parse-sexp 1750,68650
+(defun proof-cmdstart-add-segment-for-cmd 1774,69586
+(defun proof-segment-up-to-cmdstart 1826,71785
+(defun proof-segment-up-to-cmdend 1887,74145
+(defun proof-semis-to-vanillas 1958,76792
+(defun proof-script-new-command-advance 1997,78118
+(defun proof-script-next-command-advance 2039,79859
+(defun proof-assert-until-point-interactive 2051,80300
+(defun proof-assert-until-point 2077,81422
+(defun proof-assert-next-command2130,83854
+(defun proof-goto-point 2178,86117
+(defun proof-insert-pbp-command 2195,86643
+(defun proof-done-retracting 2228,87756
+(defun proof-setup-retract-action 2255,88877
+(defun proof-last-goal-or-goalsave 2265,89360
+(defun proof-retract-target 2288,90200
+(defun proof-retract-until-point-interactive 2373,93841
+(defun proof-retract-until-point 2381,94226
+(define-derived-mode proof-mode 2424,95975
+(defun proof-script-set-visited-file-name 2469,97736
+(defun proof-script-set-buffer-hooks 2493,98738
+(defun proof-script-kill-buffer-fn 2501,99156
+(defun proof-config-done-related 2545,100978
+(defun proof-generic-goal-command-p 2617,103546
+(defun proof-generic-state-preserving-p 2622,103758
+(defun proof-generic-count-undos 2631,104275
+(defun proof-generic-find-and-forget 2660,105305
+(defconst proof-script-important-settings2711,107130
+(defun proof-config-done 2726,107683
+(defun proof-setup-parsing-mechanism 2819,111086
+(defun proof-setup-imenu 2863,112939
+(defun proof-setup-func-menu 2880,113544
+
+generic/proof-shell.el,3350
+(defvar proof-shell-last-output 27,613
+(defvar proof-marker 63,1714
+(defvar proof-action-list 66,1811
+(defvar proof-shell-silent 74,1987
+(defvar proof-shell-last-prompt 88,2470
+(defvar proof-shell-last-output-kind 93,2700
+(defvar proof-shell-delayed-output 114,3522
+(defvar proof-shell-delayed-output-kind 117,3643
+(defcustom proof-shell-active-scripting-indicator126,3846
+(defun proof-shell-ready-prover 179,5317
+(defun proof-shell-live-buffer 193,5857
+(defun proof-shell-available-p 200,6092
+(defun proof-grab-lock 206,6315
+(defun proof-release-lock 223,7027
+(defcustom proof-shell-fiddle-frames 243,7578
+(defun proof-shell-set-text-representation 250,7819
+(defun proof-shell-start 263,8374
+(defvar proof-shell-kill-function-hooks 472,15899
+(defun proof-shell-kill-function 475,15997
+(defun proof-shell-clear-state 564,19800
+(defun proof-shell-exit 579,20243
+(defun proof-shell-bail-out 591,20688
+(defun proof-shell-restart 600,21165
+(defvar proof-shell-no-response-display 642,22549
+(defvar proof-shell-urgent-message-marker 645,22653
+(defvar proof-shell-urgent-message-scanner 648,22774
+(defun proof-shell-handle-output 652,22901
+(defun proof-shell-handle-delayed-output 712,25542
+(defvar proof-shell-no-error-display 740,26585
+(defun proof-shell-handle-error 746,26789
+(defun proof-shell-handle-interrupt 764,27625
+(defun proof-shell-error-or-interrupt-action 778,28238
+(defun proof-goals-pos 803,29383
+(defun proof-pbp-focus-on-first-goal 808,29588
+(defsubst proof-shell-string-match-safe 820,30118
+(defun proof-shell-process-output 825,30286
+(defvar proof-shell-insert-space-fudge 936,34926
+(defun proof-shell-insert 946,35245
+(defun proof-shell-command-queue-item 1020,38157
+(defun proof-shell-set-silent 1025,38314
+(defun proof-shell-start-silent-item 1031,38533
+(defun proof-shell-clear-silent 1037,38725
+(defun proof-shell-stop-silent-item 1043,38947
+(defun proof-shell-should-be-silent 1050,39219
+(defun proof-append-alist 1063,39775
+(defun proof-start-queue 1122,42012
+(defun proof-extend-queue 1133,42361
+(defun proof-shell-exec-loop 1144,42742
+(defun proof-shell-insert-loopback-cmd 1209,45330
+(defun proof-shell-message 1237,46656
+(defun proof-shell-process-urgent-message 1243,46872
+(defvar proof-shell-minibuffer-urgent-interactive-input-history 1455,55812
+(defun proof-shell-minibuffer-urgent-interactive-input 1457,55882
+(defun proof-shell-process-urgent-messages 1469,56252
+(defun proof-shell-filter 1542,59423
+(defun proof-shell-filter-process-output 1701,66012
+(defvar pg-last-tracing-output-time 1754,68066
+(defvar pg-tracing-slow-mode 1757,68172
+(defconst pg-slow-mode-duration 1760,68261
+(defconst pg-fast-tracing-mode-threshold 1763,68343
+(defvar pg-tracing-cleanup-timer 1766,68471
+(defun pg-tracing-tight-loop 1768,68510
+(defun pg-finish-tracing-display 1811,70228
+(defun proof-shell-dont-show-annotations 1824,70534
+(defun proof-shell-show-annotations 1840,71069
+(defun proof-shell-wait 1861,71566
+(defun proof-done-invisible 1881,72476
+(defun proof-shell-invisible-command 1924,74199
+(defun proof-shell-invisible-cmd-get-result 1957,75449
+(defun proof-shell-invisible-command-invisible-result 1974,76130
+(define-derived-mode proof-shell-mode 1993,76560
+(defconst proof-shell-important-settings2063,79226
+(defun proof-shell-config-done 2069,79341
+
+generic/proof-site.el,827
+(defconst proof-general-short-version 50,1694
+(defconst proof-general-version-year 56,1882
+(defgroup proof-general 63,2035
+(defgroup proof-general-internals 68,2143
+(defun proof-home-directory-fn 81,2531
+(defcustom proof-home-directory92,2902
+(defcustom proof-images-directory101,3269
+(defcustom proof-info-directory107,3471
+(defconst proof-assistant-table-default136,4685
+(defcustom proof-assistant-table164,5782
+(defcustom proof-assistants 199,6898
+(defvar proof-assistant-cusgrp 229,8076
+(defvar proof-assistant-internals-cusgrp 235,8338
+(defvar proof-assistant 241,8609
+(defvar proof-assistant-symbol 246,8831
+(defvar proof-ready-for-assistant-hook 255,9222
+(defvar proof-ready-for-assistant-flag 260,9422
+(defun proof-ready-for-assistant 266,9622
+(defmacro proof-eval-when-ready-for-assistant 324,12080
+
+generic/proof-splash.el,726
+(defcustom proof-splash-enable 14,379
+(defcustom proof-splash-time 19,531
+(defcustom proof-splash-contents27,816
+(defconst proof-splash-startup-msg 53,1776
+(defconst proof-splash-welcome 62,2155
+(defun proof-get-image 81,2702
+(defvar proof-splash-timeout-conf 120,4053
+(defun proof-splash-centre-spaces 123,4166
+(defun proof-splash-remove-screen 151,5336
+(defun proof-splash-remove-buffer 171,6057
+(defvar proof-splash-seen 187,6721
+(defun proof-splash-display-screen 191,6838
+(defun proof-splash-message 266,9992
+(defun proof-splash-timeout-waiter 277,10388
+(defvar proof-splash-old-frame-title-format 293,11084
+(defun proof-splash-set-frame-titles 295,11134
+(defun proof-splash-unset-frame-titles 304,11450
+
+generic/proof-syntax.el,981
+(defun proof-ids-to-regexp 15,421
+(defun proof-anchor-regexp 21,677
+(defconst proof-no-regexp25,779
+(defun proof-regexp-alt 30,874
+(defun proof-regexp-region 39,1160
+(defun proof-re-search-forward-region 48,1583
+(defun proof-search-forward 61,2078
+(defun proof-replace-regexp-in-string 67,2330
+(defun proof-re-search-forward 73,2584
+(defun proof-re-search-backward 79,2845
+(defun proof-string-match 85,3109
+(defun proof-string-match-safe 91,3341
+(defun proof-stringfn-match 95,3546
+(defun proof-looking-at 102,3806
+(defun proof-looking-at-safe 108,3996
+(defun proof-looking-at-syntactic-context 112,4136
+(defsubst proof-replace-string 124,4499
+(defsubst proof-replace-regexp 129,4703
+(defsubst proof-replace-regexp-nocasefold 134,4912
+(defvar proof-id 142,5194
+(defun proof-ids 148,5414
+(defun proof-zap-commas 161,5975
+(defun proof-format 179,6544
+(defun proof-format-filename 198,7183
+(defun proof-insert 247,8661
+(defun proof-splice-separator 283,9670
+
+generic/proof-toolbar.el,2874
+(defun proof-toolbar-function 38,1281
+(defun proof-toolbar-icon 41,1378
+(defun proof-toolbar-enabler 44,1479
+(defun proof-toolbar-function-with-enabler 47,1587
+(defun proof-toolbar-make-icon 54,1760
+(defun proof-toolbar-make-toolbar-item 72,2360
+(defvar proof-toolbar 111,3736
+(deflocal proof-toolbar-itimer 115,3865
+(defun proof-toolbar-setup 119,3975
+(defun proof-toolbar-build 162,5518
+(defalias 'proof-toolbar-enable proof-toolbar-enable
227,7728
+(defun proof-toolbar-setup-refresh 238,8032
+(defun proof-toolbar-disable-refresh 259,8802
+(deflocal proof-toolbar-refresh-flag 266,9124
+(defun proof-toolbar-refresh 272,9395
+(defvar proof-toolbar-enablers276,9540
+(defvar proof-toolbar-enablers-last-state282,9722
+(defun proof-toolbar-really-refresh 286,9813
+(defun proof-toolbar-undo-enable-p 339,11643
+(defalias 'proof-toolbar-undo proof-toolbar-undo
344,11791
+(defun proof-toolbar-delete-enable-p 350,11910
+(defalias 'proof-toolbar-delete proof-toolbar-delete
356,12084
+(defun proof-toolbar-lockedend-enable-p 363,12220
+(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
366,12270
+(defun proof-toolbar-next-enable-p 375,12358
+(defalias 'proof-toolbar-next proof-toolbar-next
379,12465
+(defun proof-toolbar-goto-enable-p 386,12559
+(defalias 'proof-toolbar-goto proof-toolbar-goto
389,12632
+(defun proof-toolbar-retract-enable-p 396,12708
+(defalias 'proof-toolbar-retract proof-toolbar-retract
400,12819
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
407,12898
+(defalias 'proof-toolbar-use proof-toolbar-use
408,12966
+(defun proof-toolbar-restart-enable-p 414,13044
+(defalias 'proof-toolbar-restart proof-toolbar-restart
419,13205
+(defun proof-toolbar-goal-enable-p 425,13283
+(defalias 'proof-toolbar-goal proof-toolbar-goal
432,13516
+(defun proof-toolbar-qed-enable-p 439,13588
+(defalias 'proof-toolbar-qed proof-toolbar-qed
445,13740
+(defun proof-toolbar-state-enable-p 451,13812
+(defalias 'proof-toolbar-state proof-toolbar-state
454,13883
+(defun proof-toolbar-context-enable-p 460,13952
+(defalias 'proof-toolbar-context proof-toolbar-context
463,14025
+(defun proof-toolbar-info-enable-p 471,14185
+(defalias 'proof-toolbar-info proof-toolbar-info
474,14229
+(defun proof-toolbar-command-enable-p 480,14298
+(defalias 'proof-toolbar-command proof-toolbar-command
483,14369
+(defun proof-toolbar-help-enable-p 489,14449
+(defun proof-toolbar-help 492,14494
+(defun proof-toolbar-find-enable-p 500,14588
+(defalias 'proof-toolbar-find proof-toolbar-find
503,14657
+(defun proof-toolbar-visibility-enable-p 509,14755
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
512,14855
+(defun proof-toolbar-interrupt-enable-p 518,14943
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
521,15007
+(defun proof-toolbar-make-menu-item 530,15196
+(defun proof-toolbar-scripting-menu 553,15896
+
+generic/proof-utils.el,2153
+(defmacro deflocal 26,852
+(defmacro proof-with-current-buffer-if-exists 33,1090
+(defmacro proof-with-script-buffer 42,1467
+(defmacro proof-map-buffers 53,1854
+(defmacro proof-sym 58,2039
+(defsubst proof-try-require 63,2200
+(defmacro proof-face-specs 70,2397
+(defun proof-save-some-buffers 92,3051
+(defun proof-set-value 116,3742
+(defsubst proof-ass-symv 176,5912
+(defmacro proof-ass-sym 183,6213
+(defmacro proof-ass 188,6423
+(defun proof-defpgcustom-fn 193,6587
+(defun undefpgcustom 214,7458
+(defmacro defpgcustom 220,7682
+(defun proof-defpgdefault-fn 231,8100
+(defmacro defpgdefault 245,8558
+(defmacro defpgfun 256,8920
+(defun proof-file-truename 271,9214
+(defun proof-file-to-buffer 275,9397
+(defun proof-files-to-buffers 286,9726
+(defun proof-buffers-in-mode 293,10009
+(defun pg-save-from-death 307,10459
+(defun proof-define-keys 326,11076
+(deflocal proof-font-lock-keywords 355,12075
+(deflocal proof-font-lock-keywords-case-fold-search 361,12340
+(defun proof-font-lock-configure-defaults 364,12463
+(defun proof-font-lock-clear-font-lock-vars 412,14768
+(defun proof-font-lock-set-font-lock-vars 423,15141
+(defun proof-fontify-region 430,15351
+(defun pg-remove-specials 488,17569
+(defun pg-remove-specials-in-string 498,17907
+(defun proof-fontify-buffer 505,18094
+(defun proof-warn-if-unset 518,18335
+(defun proof-get-window-for-buffer 523,18553
+(defun proof-display-and-keep-buffer 574,20861
+(defun proof-clean-buffer 606,22168
+(defun proof-message 621,22789
+(defun proof-warning 626,23002
+(defun pg-internal-warning 632,23284
+(defun proof-debug 640,23603
+(defun proof-switch-to-buffer 655,24274
+(defun proof-resize-window-tofit 688,25963
+(defun proof-submit-bug-report 788,29975
+(defun proof-deftoggle-fn 824,31354
+(defmacro proof-deftoggle 839,32007
+(defun proof-defintset-fn 846,32381
+(defmacro proof-defintset 862,33085
+(defun proof-defstringset-fn 869,33462
+(defmacro proof-defstringset 882,34088
+(defmacro proof-defshortcut 896,34545
+(defmacro proof-definvisible 911,35184
+(defun pg-custom-save-vars 939,36161
+(defun pg-custom-reset-vars 957,36884
+(defun proof-locate-executable 970,37221
+
+generic/proof-x-symbol.el,612
+(defvar proof-x-symbol-initialized 52,2072
+(defun proof-x-symbol-tokenlang-file 55,2167
+(defun proof-x-symbol-support-maybe-available 61,2349
+(defun proof-x-symbol-initialize 81,3078
+(defun proof-x-symbol-enable 164,6345
+(defun proof-x-symbol-refresh-output-buffers 196,7771
+(defun proof-x-symbol-mode-associated-buffers 211,8516
+(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
233,9220
+(defun proof-x-symbol-encode-shell-input 235,9286
+(defun proof-x-symbol-set-language 252,9877
+(defun proof-x-symbol-shell-config 257,10048
+(defun proof-x-symbol-config-output-buffer 305,12215
+
+generic/test-compile.el,21
+(defconst bar 8,139
+
+generic/test-mac.el,21
+(defvar testme 3,26
+
+generic/test-req2.el,48
+(define-derived-mode proof-response-mode 8,138
 
 lib/bufhist.el,1099
 (defun bufhist-ring-update 32,1226
@@ -2217,34 +2245,34 @@ lib/holes.el,2447
 (defun holes-clear-hole-at 425,13013
 (defun holes-map-holes 434,13272
 (defun holes-mapcar-holes 442,13455
-(defun holes-clear-all-buffer-holes 448,13622
-(defun holes-next 459,13922
-(defun holes-next-after-active-hole 466,14173
-(defun holes-set-active-hole-next 474,14392
-(defun holes-replace-segment 496,14945
-(defun holes-replace 506,15299
-(defun holes-replace-active-hole 537,16494
-(defun holes-replace-update-active-hole 546,16795
-(defun holes-delete-update-active-hole 567,17485
-(defun holes-set-make-active-hole 574,17699
-(defun holes-mouse-replace-active-hole 621,19327
-(defun holes-destroy-hole 641,19866
-(defun holes-hole-at-event 658,20277
-(defun holes-mouse-destroy-hole 663,20390
-(defun holes-mouse-forget-hole 673,20630
-(defun holes-mouse-set-make-active-hole 689,20940
-(defun holes-mouse-set-active-hole 711,21501
-(defun holes-set-point-next-hole-destroy 723,21765
-(defvar hole-map739,22215
-(defvar holes-mode-map755,22835
-(defun holes-replace-string-by-holes-backward 792,24300
-(defun holes-skeleton-end-hook 810,25001
-(defconst holes-jump-doc 819,25410
-(defun holes-replace-string-by-holes-backward-jump 826,25617
-(defun holes-abbrev-complete 843,26248
-(defun holes-insert-and-expand 852,26555
-(defvar holes-mode 863,26987
-(defun holes-mode 869,27183
+(defun holes-clear-all-buffer-holes 448,13627
+(defun holes-next 459,13927
+(defun holes-next-after-active-hole 466,14178
+(defun holes-set-active-hole-next 474,14397
+(defun holes-replace-segment 496,14950
+(defun holes-replace 506,15304
+(defun holes-replace-active-hole 537,16499
+(defun holes-replace-update-active-hole 546,16800
+(defun holes-delete-update-active-hole 567,17490
+(defun holes-set-make-active-hole 574,17704
+(defun holes-mouse-replace-active-hole 621,19332
+(defun holes-destroy-hole 641,19871
+(defun holes-hole-at-event 658,20282
+(defun holes-mouse-destroy-hole 663,20395
+(defun holes-mouse-forget-hole 673,20635
+(defun holes-mouse-set-make-active-hole 689,20945
+(defun holes-mouse-set-active-hole 711,21506
+(defun holes-set-point-next-hole-destroy 723,21770
+(defvar hole-map739,22220
+(defvar holes-mode-map755,22840
+(defun holes-replace-string-by-holes-backward 792,24305
+(defun holes-skeleton-end-hook 810,25006
+(defconst holes-jump-doc 819,25444
+(defun holes-replace-string-by-holes-backward-jump 826,25651
+(defun holes-abbrev-complete 843,26282
+(defun holes-insert-and-expand 852,26589
+(defvar holes-mode 863,27021
+(defun holes-mode 869,27217
 
 lib/local-vars-list.el,372
 (defconst local-vars-list-doc 25,759
@@ -2263,78 +2291,77 @@ lib/maths-menu.el,153
 (defvar maths-menu-mode-map312,11648
 (define-minor-mode maths-menu-mode337,12521
 
-lib/proof-compat.el,1003
-(defvar proof-running-on-XEmacs 25,818
-(defvar proof-running-on-Emacs21 27,940
-(defvar proof-running-on-win32 31,1187
-(defun pg-custom-undeclare-variable 43,1621
-(defun pg-window-system 118,4103
-(defconst pg-defface-window-systems 127,4474
-(defun subst-char-in-string 151,5191
-(defun replace-regexp-in-string 165,5745
-(defconst menuvisiblep 227,8458
-(defun set-window-text-height 244,9077
-(defmacro save-selected-frame 270,10027
-(defun warn 309,11329
-(defun redraw-modeline 316,11584
-(defun replace-in-string 331,12151
-(defun proof-buffer-syntactic-context-emulate 380,13669
-(defvar read-shell-command-map413,14976
-(defun read-shell-command 431,15678
-(defun remassq 443,16159
-(defun remassoc 455,16548
-(defun frames-of-buffer 468,16993
-(defmacro with-selected-window 507,18255
-(defun pg-pop-to-buffer 550,19644
-(defun process-live-p 601,21496
-(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
618,21999
-(defun select-buffers-tab-buffers-by-mode 662,23347
-
-lib/span.el,132
-(defsubst delete-spans 24,499
-(defsubst span-property-safe 28,653
-(defsubst set-span-start 32,792
-(defsubst set-span-end 36,924
-
-lib/span-extent.el,968
-(defsubst make-span 12,367
-(defsubst detach-span 16,489
-(defsubst set-span-endpoints 20,576
-(defsubst set-span-property 24,709
+lib/pg-dev.el,75
+(defconst pg-dev-lisp-font-lock-keywords35,1049
+(defun unload-pg 69,1986
+
+lib/proof-compat.el,795
+(defvar proof-running-on-win32 26,856
+(defconst pg-defface-window-systems 34,1235
+(defun pg-custom-undeclare-variable 56,2062
+(defun subst-char-in-string 118,3707
+(defun replace-regexp-in-string 133,4296
+(defconst menuvisiblep 195,7009
+(defun set-window-text-height 212,7622
+(defmacro save-selected-frame 238,8572
+(defun warn 277,9869
+(defun redraw-modeline 284,10124
+(defun proof-buffer-syntactic-context-emulate 301,10720
+(defvar read-shell-command-map334,12027
+(defun read-shell-command 352,12729
+(defun remassq 364,13210
+(defun remassoc 376,13599
+(defun frames-of-buffer 389,14044
+(defmacro with-selected-window 428,15306
+(defun pg-pop-to-buffer 471,16684
+(defun process-live-p 522,18517
+(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
539,19020
+
+lib/span.el,137
+(defsubst span-delete-spans 22,471
+(defsubst span-property-safe 26,635
+(defsubst span-set-start 30,774
+(defsubst span-set-end 34,906
+
+lib/span-extent.el,973
+(defsubst span-make 12,367
+(defsubst span-detach 16,489
+(defsubst span-set-endpoints 20,576
+(defsubst span-set-property 24,709
 (defsubst span-read-only 28,836
 (defsubst span-read-write 32,940
 (defun span-give-warning 36,1047
 (defun span-write-warning 40,1155
 (defsubst span-property 45,1355
-(defsubst delete-span 49,1470
-(defsubst mapcar-spans 55,1641
-(defsubst span-at 59,1847
-(defsubst span-at-before 63,1964
-(defsubst span-start 68,2161
-(defsubst span-end 72,2290
-(defsubst prev-span 76,2413
-(defsubst next-span 80,2559
-(defsubst span-live-p 84,2701
-(defun span-raise 92,2973
-(defalias 'span-object span-object
96,3072
-(defalias 'span-string span-string
97,3111
-(defsubst make-detached-span 100,3197
-(defsubst span-buffer 105,3259
-(defsubst span-detached-p 110,3351
-(defsubst set-span-face 115,3463
-(defsubst fold-spans 119,3558
-(defsubst set-span-properties 123,3755
-(defsubst set-span-keymap 127,3863
-(defsubst span-at-event 132,4007
-
-lib/span-overlay.el,1201
+(defsubst span-delete 49,1470
+(defsubst span-mapcar-spans 55,1641
+(defsubst span-at 59,1852
+(defsubst span-at-before 63,1969
+(defsubst span-start 68,2166
+(defsubst span-end 72,2295
+(defsubst prev-span 76,2418
+(defsubst next-span 80,2564
+(defsubst span-live-p 84,2706
+(defun span-raise 92,2978
+(defalias 'span-object span-object
96,3077
+(defalias 'span-string span-string
97,3116
+(defsubst make-detached-span 100,3202
+(defsubst span-buffer 105,3264
+(defsubst span-detached-p 110,3356
+(defsubst set-span-face 115,3468
+(defsubst fold-spans 119,3563
+(defsubst set-span-properties 123,3760
+(defsubst set-span-keymap 127,3868
+(defsubst span-at-event 132,4012
+
+lib/span-overlay.el,1206
 (defalias 'span-start span-start
12,370
 (defalias 'span-end span-end
13,408
-(defalias 'set-span-property set-span-property
14,442
+(defalias 'span-set-property span-set-property
14,442
 (defalias 'span-property span-property
15,485
-(defalias 'make-span make-span
16,524
-(defalias 'detach-span detach-span
17,560
-(defalias 'set-span-endpoints set-span-endpoints
18,600
+(defalias 'span-make span-make
16,524
+(defalias 'span-detach span-detach
17,560
+(defalias 'span-set-endpoints span-set-endpoints
18,600
 (defalias 'span-buffer span-buffer
19,645
 (defun span-read-only-hook 21,686
 (defun span-read-only 25,818
@@ -2345,37 +2372,37 @@ lib/span-overlay.el,1201
 (defun spans-at-point-prop 62,2388
 (defun spans-at-region-prop 68,2553
 (defun span-at 76,2797
-(defsubst delete-span 82,3011
-(defsubst mapcar-spans 89,3233
-(defun span-at-before 93,3437
-(defun prev-span 110,4163
-(defun next-span 116,4314
-(defsubst span-live-p 145,5539
-(defun span-raise 151,5705
-(defalias 'span-object span-object
157,5948
-(defun span-string 159,5989
-(defun set-span-properties 165,6171
-(defun span-find-span 177,6426
-(defsubst span-at-event 184,6733
-(defun make-detached-span 189,6857
-(defun fold-spans 194,6953
-(defsubst span-detached-p 209,7487
-(defsubst set-span-face 213,7602
-(defun set-span-keymap 217,7699
+(defsubst span-delete 82,3011
+(defsubst span-mapcar-spans 89,3233
+(defun span-at-before 93,3442
+(defun prev-span 110,4168
+(defun next-span 116,4319
+(defsubst span-live-p 145,5544
+(defun span-raise 151,5710
+(defalias 'span-object span-object
157,5953
+(defun span-string 159,5994
+(defun set-span-properties 165,6176
+(defun span-find-span 177,6431
+(defsubst span-at-event 184,6738
+(defun make-detached-span 189,6862
+(defun fold-spans 194,6958
+(defsubst span-detached-p 209,7492
+(defsubst set-span-face 213,7607
+(defun set-span-keymap 217,7704
 
 lib/texi-docstring-magic.el,584
 (defun texi-docstring-magic-find-face 85,2997
 (defun texi-docstring-magic-splice-sep 90,3162
 (defconst texi-docstring-magic-munge-table100,3467
-(defun texi-docstring-magic-untabify 190,7187
-(defun texi-docstring-magic-munge-docstring 200,7502
-(defun texi-docstring-magic-texi 239,8789
-(defun texi-docstring-magic-format-default 252,9229
-(defun texi-docstring-magic-texi-for 268,9864
-(defconst texi-docstring-magic-comment326,11824
-(defun texi-docstring-magic 332,11978
-(defun texi-docstring-magic-face-at-point 366,13058
-(defun texi-docstring-magic-insert-magic 381,13581
+(defun texi-docstring-magic-untabify 190,7234
+(defun texi-docstring-magic-munge-docstring 200,7549
+(defun texi-docstring-magic-texi 239,8836
+(defun texi-docstring-magic-format-default 252,9276
+(defun texi-docstring-magic-texi-for 268,9911
+(defconst texi-docstring-magic-comment326,11871
+(defun texi-docstring-magic 332,12025
+(defun texi-docstring-magic-face-at-point 366,13105
+(defun texi-docstring-magic-insert-magic 381,13628
 
 lib/unichars.el,35
 (defvar unicode-character-list1,0
@@ -3460,91 +3487,91 @@ doc/ProofGeneral.texi,5379
 @node Top166,5052
 @node Preface203,6168
 @node Latest news for version 3.7Latest news for version 3.7
226,6764
-@node Future264,8432
-@node Credits295,9731
-@node Introducing Proof GeneralIntroducing Proof General
394,13165
-@node Installing Proof GeneralInstalling Proof General
450,15197
-@node Quick start guideQuick start guide
464,15645
-@node Features of Proof GeneralFeatures of Proof General
508,17753
-@node Supported proof assistantsSupported proof assistants
597,21678
-@node Prerequisites for this manualPrerequisites for this manual
646,23584
-@node Organization of this manualOrganization of this manual
690,25210
-@node Basic Script ManagementBasic Script Management
716,26038
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
735,26638
-@node Proof scriptsProof scripts
986,36291
-@node Script buffersScript buffers
1029,38411
-@node Locked queue and editing regionsLocked queue and editing regions
1051,38988
-@node Goal-save sequencesGoal-save sequences
1107,41135
-@node Active scripting bufferActive scripting buffer
1144,42621
-@node Summary of Proof General buffersSummary of Proof General buffers
1213,46041
-@node Script editing commandsScript editing commands
1275,48715
-@node Script processing commandsScript processing commands
1353,51573
-@node Proof assistant commandsProof assistant commands
1481,56874
-@node Toolbar commandsToolbar commands
1631,61878
-@node Interrupting during trace outputInterrupting during trace output
1655,62807
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1694,64731
-@node Goals buffer commandsGoals buffer commands
1708,65231
-@node Advanced Script ManagementAdvanced Script Management
1797,68764
-@node Visibility of completed proofsVisibility of completed proofs
1828,69918
-@node Switching between proof scriptsSwitching between proof scripts
1883,71841
-@node View of processed files View of processed files 
1920,73813
-@node Retracting across filesRetracting across files
1980,76864
-@node Asserting across filesAsserting across files
1993,77495
-@node Automatic multiple file handlingAutomatic multiple file handling
2006,78061
-@node Escaping script managementEscaping script management
2031,79095
-@node Experimental featuresExperimental features
2089,81298
-@node Support for other PackagesSupport for other Packages
2123,82561
-@node Syntax highlightingSyntax highlighting
2155,83436
-@node X-Symbol supportX-Symbol support
2194,85057
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2253,87603
-@node Support for outline modeSupport for outline mode
2312,89733
-@node Support for completionSupport for completion
2338,90863
-@node Support for tagsSupport for tags
2395,93031
-@node Customizing Proof GeneralCustomizing Proof General
2447,95360
-@node Basic optionsBasic options
2487,97030
-@node How to customizeHow to customize
2511,97788
-@node Display customizationDisplay customization
2562,99890
-@node User optionsUser options
2687,105124
-@node Changing facesChanging faces
2951,114523
-@node Tweaking configuration settingsTweaking configuration settings
3026,117192
-@node Hints and TipsHints and Tips
3083,119718
-@node Adding your own keybindingsAdding your own keybindings
3102,120319
-@node Using file variablesUsing file variables
3158,122852
-@node Using abbreviationsUsing abbreviations
3217,125038
-@node LEGO Proof GeneralLEGO Proof General
3256,126454
-@node LEGO specific commandsLEGO specific commands
3297,127823
-@node LEGO tagsLEGO tags
3317,128278
-@node LEGO customizationsLEGO customizations
3327,128525
-@node Coq Proof GeneralCoq Proof General
3359,129444
-@node Coq-specific commandsCoq-specific commands
3375,129853
-@node Coq-specific variablesCoq-specific variables
3397,130360
-@node Editing multiple proofsEditing multiple proofs
3419,131018
-@node User-loaded tacticsUser-loaded tactics
3443,132126
-@node Holes featureHoles feature
3507,134600
-@node Isabelle Proof GeneralIsabelle Proof General
3534,135887
-@node Isabelle commandsIsabelle commands
3564,137017
-@node Logics and SettingsLogics and Settings
3671,140065
-@node Isabelle customizationsIsabelle customizations
3705,141605
-@node HOL Proof GeneralHOL Proof General
3729,142087
-@node Shell Proof GeneralShell Proof General
3771,143909
-@node Obtaining and InstallingObtaining and Installing
3807,145368
-@node Obtaining Proof GeneralObtaining Proof General
3823,145781
-@node Installing Proof General from tarballInstalling Proof General from tarball
3854,147020
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
3879,147852
-@node Setting the names of binariesSetting the names of binaries
3894,148260
-@node Notes for syssiesNotes for syssies
3922,149200
-@node Bugs and EnhancementsBugs and Enhancements
3995,152138
-@node References4016,152953
-@node History of Proof GeneralHistory of Proof General
4056,153977
-@node Old News for 3.0Old News for 3.0
4147,158079
-@node Old News for 3.1Old News for 3.1
4217,161773
-@node Old News for 3.2Old News for 3.2
4243,162945
-@node Old News for 3.3Old News for 3.3
4304,165948
-@node Old News for 3.4Old News for 3.4
4323,166845
-@node Function IndexFunction Index
4346,167901
-@node Variable IndexVariable Index
4350,167977
-@node Keystroke IndexKeystroke Index
4354,168057
-@node Concept IndexConcept Index
4358,168123
+@node Future265,8408
+@node Credits296,9707
+@node Introducing Proof GeneralIntroducing Proof General
395,13141
+@node Installing Proof GeneralInstalling Proof General
451,15183
+@node Quick start guideQuick start guide
465,15631
+@node Features of Proof GeneralFeatures of Proof General
509,17739
+@node Supported proof assistantsSupported proof assistants
598,21664
+@node Prerequisites for this manualPrerequisites for this manual
647,23570
+@node Organization of this manualOrganization of this manual
691,25196
+@node Basic Script ManagementBasic Script Management
717,26024
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
736,26624
+@node Proof scriptsProof scripts
987,36277
+@node Script buffersScript buffers
1030,38397
+@node Locked queue and editing regionsLocked queue and editing regions
1052,38974
+@node Goal-save sequencesGoal-save sequences
1108,41121
+@node Active scripting bufferActive scripting buffer
1145,42607
+@node Summary of Proof General buffersSummary of Proof General buffers
1214,46027
+@node Script editing commandsScript editing commands
1276,48701
+@node Script processing commandsScript processing commands
1354,51552
+@node Proof assistant commandsProof assistant commands
1482,56853
+@node Toolbar commandsToolbar commands
1632,61857
+@node Interrupting during trace outputInterrupting during trace output
1656,62786
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1695,64710
+@node Goals buffer commandsGoals buffer commands
1709,65210
+@node Advanced Script ManagementAdvanced Script Management
1798,68743
+@node Visibility of completed proofsVisibility of completed proofs
1829,69897
+@node Switching between proof scriptsSwitching between proof scripts
1884,71820
+@node View of processed files View of processed files 
1921,73792
+@node Retracting across filesRetracting across files
1981,76843
+@node Asserting across filesAsserting across files
1994,77474
+@node Automatic multiple file handlingAutomatic multiple file handling
2007,78040
+@node Escaping script managementEscaping script management
2032,79074
+@node Experimental featuresExperimental features
2090,81277
+@node Support for other PackagesSupport for other Packages
2124,82539
+@node Syntax highlightingSyntax highlighting
2156,83414
+@node X-Symbol supportX-Symbol support
2195,85035
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2254,87581
+@node Support for outline modeSupport for outline mode
2313,89711
+@node Support for completionSupport for completion
2339,90841
+@node Support for tagsSupport for tags
2397,93017
+@node Customizing Proof GeneralCustomizing Proof General
2449,95346
+@node Basic optionsBasic options
2489,97016
+@node How to customizeHow to customize
2513,97774
+@node Display customizationDisplay customization
2564,99876
+@node User optionsUser options
2689,105114
+@node Changing facesChanging faces
2953,114504
+@node Tweaking configuration settingsTweaking configuration settings
3028,117173
+@node Hints and TipsHints and Tips
3085,119699
+@node Adding your own keybindingsAdding your own keybindings
3104,120300
+@node Using file variablesUsing file variables
3160,122833
+@node Using abbreviationsUsing abbreviations
3219,125019
+@node LEGO Proof GeneralLEGO Proof General
3258,126435
+@node LEGO specific commandsLEGO specific commands
3299,127804
+@node LEGO tagsLEGO tags
3319,128259
+@node LEGO customizationsLEGO customizations
3329,128506
+@node Coq Proof GeneralCoq Proof General
3361,129425
+@node Coq-specific commandsCoq-specific commands
3377,129834
+@node Coq-specific variablesCoq-specific variables
3399,130341
+@node Editing multiple proofsEditing multiple proofs
3421,130999
+@node User-loaded tacticsUser-loaded tactics
3445,132107
+@node Holes featureHoles feature
3509,134581
+@node Isabelle Proof GeneralIsabelle Proof General
3536,135868
+@node Isabelle commandsIsabelle commands
3566,136998
+@node Logics and SettingsLogics and Settings
3673,140046
+@node Isabelle customizationsIsabelle customizations
3707,141586
+@node HOL Proof GeneralHOL Proof General
3731,142068
+@node Shell Proof GeneralShell Proof General
3773,143890
+@node Obtaining and InstallingObtaining and Installing
3809,145349
+@node Obtaining Proof GeneralObtaining Proof General
3825,145762
+@node Installing Proof General from tarballInstalling Proof General from tarball
3856,147001
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package
3881,147833
+@node Setting the names of binariesSetting the names of binaries
3896,148241
+@node Notes for syssiesNotes for syssies
3924,149181
+@node Bugs and EnhancementsBugs and Enhancements
3999,152217
+@node References4020,153032
+@node History of Proof GeneralHistory of Proof General
4060,154056
+@node Old News for 3.0Old News for 3.0
4151,158158
+@node Old News for 3.1Old News for 3.1
4221,161852
+@node Old News for 3.2Old News for 3.2
4247,163024
+@node Old News for 3.3Old News for 3.3
4308,166027
+@node Old News for 3.4Old News for 3.4
4327,166924
+@node Function IndexFunction Index
4350,167980
+@node Variable IndexVariable Index
4354,168056
+@node Keystroke IndexKeystroke Index
4358,168136
+@node Concept IndexConcept Index
4362,168202
 
 doc/PG-adapting.texi,3776
 @node Top157,4775
@@ -3553,58 +3580,58 @@ doc/PG-adapting.texi,3776
 @node Credits272,9169
 @node Beginning with a New ProverBeginning with a New Prover
282,9461
 @node Overview of adding a new proverOverview of adding a new prover
323,11410
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration
397,14831
-@node Major modes used by Proof GeneralMajor modes used by Proof General
466,18222
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
539,21305
-@node Settings for generic user-level commandsSettings for generic user-level commands
554,21851
-@node Menu configurationMenu configuration
599,23587
-@node Toolbar configurationToolbar configuration
623,24505
-@node Proof Script SettingsProof Script Settings
681,26750
-@node Recognizing commands and commentsRecognizing commands and comments
703,27330
-@node Recognizing proofsRecognizing proofs
824,32857
-@node Recognizing other elementsRecognizing other elements
936,37676
-@node Configuring undo behaviourConfiguring undo behaviour
1062,43154
-@node Nested proofsNested proofs
1200,48501
-@node Safe (state-preserving) commandsSafe (state-preserving) commands
1240,50128
-@node Activate scripting hookActivate scripting hook
1263,51074
-@node Automatic multiple filesAutomatic multiple files
1287,51938
-@node Completions1309,52785
-@node Proof Shell SettingsProof Shell Settings
1349,54263
-@node Proof shell commandsProof shell commands
1380,55545
-@node Script input to the shellScript input to the shell
1547,62724
-@node Settings for matching various output from proof processSettings for matching various output from proof process
1614,65767
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1745,71534
-@node Hooks and other settingsHooks and other settings
1955,81081
-@node Goals Buffer SettingsGoals Buffer Settings
2054,85078
-@node Splash Screen SettingsSplash Screen Settings
2131,88192
-@node Global ConstantsGlobal Constants
2157,88950
-@node Handling Multiple FilesHandling Multiple Files
2183,89799
-@node Configuring Editing SyntaxConfiguring Editing Syntax
2335,97583
-@node Configuring Font LockConfiguring Font Lock
2392,99700
-@node Configuring X-SymbolConfiguring X-Symbol
2479,103943
-@node Writing More Lisp CodeWriting More Lisp Code
2539,106466
-@node Default values for generic settingsDefault values for generic settings
2556,107111
-@node Adding prover-specific configurationsAdding prover-specific configurations
2586,108194
-@node Useful variablesUseful variables
2629,109476
-@node Useful functions and macrosUseful functions and macros
2655,110270
-@node Internals of Proof GeneralInternals of Proof General
2758,114233
-@node Spans2786,115141
-@node Proof General site configurationProof General site configuration
2799,115515
-@node Configuration variable mechanismsConfiguration variable mechanisms
2879,118603
-@node Global variablesGlobal variables
2997,123839
-@node Proof script modeProof script mode
3067,126389
-@node Proof shell modeProof shell mode
3326,138044
-@node Debugging3732,154091
-@node Plans and IdeasPlans and Ideas
3775,154968
-@node Proof by pointing and similar featuresProof by pointing and similar features
3796,155690
-@node Granularity of atomic command sequencesGranularity of atomic command sequences
3834,157348
-@node Browser mode for script files and theoriesBrowser mode for script files and theories
3879,159573
-@node Demonstration InstantiationsDemonstration Instantiations
3909,160604
-@node demoisa-easy.el3925,161035
-@node demoisa.el3988,163274
-@node Function IndexFunction Index
4156,168803
-@node Variable IndexVariable Index
4160,168879
-@node Concept IndexConcept Index
4169,169058
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration
398,14707
+@node Major modes used by Proof GeneralMajor modes used by Proof General
467,18098
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
500,19449
+@node Settings for generic user-level commandsSettings for generic user-level commands
515,19995
+@node Menu configurationMenu configuration
560,21729
+@node Toolbar configurationToolbar configuration
584,22646
+@node Proof Script SettingsProof Script Settings
642,24888
+@node Recognizing commands and commentsRecognizing commands and comments
664,25468
+@node Recognizing proofsRecognizing proofs
785,31003
+@node Recognizing other elementsRecognizing other elements
897,35821
+@node Configuring undo behaviourConfiguring undo behaviour
1023,41332
+@node Nested proofsNested proofs
1160,46743
+@node Safe (state-preserving) commandsSafe (state-preserving) commands
1200,48369
+@node Activate scripting hookActivate scripting hook
1223,49315
+@node Automatic multiple filesAutomatic multiple files
1247,50178
+@node Completions1269,51025
+@node Proof Shell SettingsProof Shell Settings
1310,52514
+@node Proof shell commandsProof shell commands
1341,53796
+@node Script input to the shellScript input to the shell
1508,60959
+@node Settings for matching various output from proof processSettings for matching various output from proof process
1575,63999
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1706,69760
+@node Hooks and other settingsHooks and other settings
1916,79353
+@node Goals Buffer SettingsGoals Buffer Settings
1997,82722
+@node Splash Screen SettingsSplash Screen Settings
2074,85821
+@node Global ConstantsGlobal Constants
2100,86579
+@node Handling Multiple FilesHandling Multiple Files
2126,87420
+@node Configuring Editing SyntaxConfiguring Editing Syntax
2278,95204
+@node Configuring Font LockConfiguring Font Lock
2337,97325
+@node Configuring X-SymbolConfiguring X-Symbol
2424,101610
+@node Writing More Lisp CodeWriting More Lisp Code
2484,104130
+@node Default values for generic settingsDefault values for generic settings
2501,104775
+@node Adding prover-specific configurationsAdding prover-specific configurations
2531,105858
+@node Useful variablesUseful variables
2574,107140
+@node Useful functions and macrosUseful functions and macros
2589,107629
+@node Internals of Proof GeneralInternals of Proof General
2692,111592
+@node Spans2720,112500
+@node Proof General site configurationProof General site configuration
2733,112874
+@node Configuration variable mechanismsConfiguration variable mechanisms
2813,115962
+@node Global variablesGlobal variables
2931,121198
+@node Proof script modeProof script mode
3001,123748
+@node Proof shell modeProof shell mode
3260,135403
+@node Debugging3665,151380
+@node Plans and IdeasPlans and Ideas
3708,152256
+@node Proof by pointing and similar featuresProof by pointing and similar features
3729,152978
+@node Granularity of atomic command sequencesGranularity of atomic command sequences
3767,154636
+@node Browser mode for script files and theoriesBrowser mode for script files and theories
3812,156861
+@node Demonstration InstantiationsDemonstration Instantiations
3842,157892
+@node demoisa-easy.el3858,158323
+@node demoisa.el3921,160562
+@node Function IndexFunction Index
4089,166091
+@node Variable IndexVariable Index
4093,166167
+@node Concept IndexConcept Index
4102,166346
 
 x-symbol/lisp/_pkg.el,0
 
@@ -3612,9 +3639,9 @@ x-symbol/lisp/custom-load.el,0
 
 lib/holes-load.el,0
 
-generic/proof-system.el,0
+generic/test-req.el,0
 
-generic/_pkg.el,0
+generic/test-mac2.el,0
 
 twelf/x-symbol-twelf.el,0
 
@@ -3622,7 +3649,7 @@ pgshell/pgshell.el,0
 
 lego/x-symbol-lego.el,0
 
-isar/x-symbol-isar.el,0
+isar/test.el,0
 
 isar/isar-templates.el,0
 
@@ -3630,6 +3657,8 @@ isar/isar-autotest.el,0
 
 isar/interface-setup.el,0
 
+isar/comptest.el,0
+
 hol98/x-symbol-hol98.el,0
 
 hol98/hol98.el,0
diff --git a/acl2/acl2.el b/acl2/acl2.el
index e1262277..a3e4fadd 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.el
@@ -24,8 +24,7 @@
  proof-prog-name		 "acl2"
 
  proof-script-sexp-commands	 t
- proof-script-comment-start             ";"
- proof-script-comment-start             ";"
+ proof-script-comment-start	";"
 
  proof-shell-annotated-prompt-regexp "ACL2[ !]*>+"
 
@@ -85,9 +84,6 @@
  ;; End of easy config.
  )
 
-(eval-when-compile 
-  (require 'proof-shell))		; nuke warning
-
 ;; Interrupts and errors enter another loop; break out of it
 (add-hook
  'proof-shell-handle-error-or-interrupt-hook
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index b6ad7b51..6f156a8c 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -66,7 +66,7 @@
     (message "Coq default abbrevs loaded")
     ))
 
-(unless (noninteractive)
+(unless noninteractive
   (coq-install-abbrevs))
 ;;;;;
 
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index a5b35ba4..a179a596 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -8,7 +8,7 @@
 (require 'pg-autotest)
 
 ;; The included test files
-(unless (noninteractive)
+(unless noninteractive
   (pg-autotest  message "Testing standard examples")
   (pg-autotest script-wholefile "coq/example.v")
   (pg-autotest script-wholefile "coq/example-x-symbol.v")
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 87ec0f4e..d575ad09 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -16,7 +16,7 @@
 
 ;;; Code:
 
-(require 'proof-utils)			; for proof-face-specs, a macro
+(require 'proof-config)			; for proof-face-specs, a macro
 (require 'holes)
 
 (defconst coq-syntax-db nil
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 51c89986..72190872 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -86,7 +86,7 @@
             (message (concat "Falling back to default: " v81))
             (setq coq-version-is-V8-1 t)))))))))
 
-(unless (noninteractive)
+(unless noninteractive
   (coq-determine-version))
 
 
diff --git a/coq/coq.el b/coq/coq.el
index 58b018f3..b33fab02 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -12,7 +12,14 @@
 ;;; History:
 
 (require 'proof)
-(require 'local-vars-list) ; in lib directory
+
+(require 'local-vars-list)              ; in lib directory
+
+(eval-when-compile
+  (proof-ready-for-assistant 'coq)      ; compile for coq
+  (require 'proof-menu)                 ; for defpacustom
+  (require 'cl)                         ; remove-if
+  (require 'span))
 
 (require 'coq-local-vars) 
 (require 'coq-syntax)      ; determines coq version
@@ -47,7 +54,7 @@
   )
 
 ;; fix it
-(unless (noninteractive) ;; compiling 
+(unless noninteractive ;; compiling 
   (coq-build-prog-args))
 
 (defcustom coq-compile-file-command "coqc %s"
@@ -326,17 +333,19 @@ toplevel \"Coq <\".  Returns nil if yes.  This assumes that no
   "Return a list with all informations from the last prompt.
 The list contains the state number, the proof stack depth, and the names of all
 pending proofs (in a list)."
+  (coq-last-prompt-info proof-shell-last-prompt))
+
+(defvar coq-last-but-one-statenum 1
+  "The state number we want to put in a span.
+This is the prompt number given *just before* the command was sent. 
+This variable remembers this number and will be updated when
+used see coq-set-state-number. Initially 1 because Coq initial state has number 1.")
 
-(coq-last-prompt-info proof-shell-last-prompt) )
+(defvar coq-last-but-one-proofnum 1
+  "As for `coq-last-but-one-statenum' but for stack depth.")
 
-;; The state number we want to put in a span is the prompt number given *just before*
-;; the command was sent. This variable remembers this number and will be updated when
-;; used see coq-set-state-number. Initially 1 because Coq initial state has number 1.
-(defvar coq-last-but-one-statenum 1)
-;; same for proof stack depth
-(defvar coq-last-but-one-proofnum 1)
-;;same for pending proofs
-(defvar coq-last-but-one-proofstack '())
+(defvar coq-last-but-one-proofstack '()
+  "As for `coq-last-but-one-statenum' but for proof stack symbols.")
 
 (defun coq-get-span-statenum (span)
   "Return the state number of the SPAN."
@@ -355,7 +364,7 @@ pending proofs (in a list)."
 
 (defun coq-set-span-statenum (span val)
   "Set the state number of the SPAN to VAL."
-  (set-span-property span 'statenum val)
+  (span-set-property span 'statenum val)
   )
 
 (defun coq-get-span-goalcmd (span)
@@ -365,17 +374,17 @@ pending proofs (in a list)."
 
 (defun coq-set-span-goalcmd (span val)
   "Set the 'goalcmd flag of the SPAN to VAL."
-  (set-span-property span 'goalcmd val)
+  (span-set-property span 'goalcmd val)
   )
 
 (defun coq-set-span-proofnum (span val)
   "Set the proof number of the SPAN to VAL."
-  (set-span-property span 'proofnum val)
+  (span-set-property span 'proofnum val)
   )
 
 (defun coq-set-span-proofstack (span val)
   "Set the proof stack (names of pending proofs) of the SPAN to VAL."
-  (set-span-property span 'proofstack val)
+  (span-set-property span 'proofstack val)
   )
 
 (defun proof-last-locked-span () 
@@ -790,17 +799,6 @@ This is specific to `coq-mode'."
 	   (if coq-version-is-V8-1 '("-emacs-U") '("-emacs"))))
       coq-prog-name)))
 
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Coq shell startup and exit hooks                               ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun coq-pre-shell-start ()
-  (setq proof-prog-name         coq-prog-name)
-  (setq proof-mode-for-shell    'coq-shell-mode)
-  (setq proof-mode-for-goals    'coq-goals-mode)
-  (setq proof-mode-for-response 'coq-response-mode))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Configuring proof and pbp mode and setting up various utilities  ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -817,8 +815,7 @@ This is specific to `coq-mode'."
 
   (setq proof-assistant-home-page coq-www-home-page)
 
-  (setq proof-mode-for-script 'coq-mode)
-
+  (setq proof-prog-name           coq-prog-name)
   (setq proof-guess-command-line 'coq-guess-command-line)
 
   ;; Commands sent to proof engine
@@ -910,8 +907,6 @@ This is specific to `coq-mode'."
         proof-shell-require-command-regexp coq-require-command-regexp
         proof-done-advancing-require-function 'coq-process-require-command)
 
-  ;; hooks and callbacks
-  (add-hook 'proof-pre-shell-start-hook 'coq-pre-shell-start nil t)
   ;; FIXME: PG 3.5, next one shouldn't be needed but setting is
   ;; now lost in define-derived-mode for some reason.
   (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)
@@ -1006,6 +1001,72 @@ To be used in `proof-shell-process-output-system-specific'."
   (proof-response-config-done))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Flags and other settings for Coq.
+;; These appear on the Coq -> Setting menu.
+;;
+
+; FIXME da: we should send this command only inside a proof,
+; otherwise it gives an error message.  It should be on
+; a different menu command.
+;(defpacustom print-only-first-subgoal  nil
+;  "Whether to just print the first subgoal in Coq."
+;  :type 'boolean
+;  :setting ("Focus. " . "Unfocus. "))
+
+
+;; FIXME: to handle "printing all" properly, we should change the state
+;; of the variables that also depend on it.
+(defpacustom print-fully-explicit nil
+  "*Print fully explicit terms."
+  :type 'boolean
+  :setting ("Set Printing All. " . "Unset Printing All. "))
+
+(defpacustom print-implicit nil
+  "*Print implicit arguments in applications."
+  :type 'boolean
+  :setting ("Set Printing Implicit. " . "Unset Printing Implicit. "))
+
+(defpacustom print-coercions nil
+  "*Print coercions."
+  :type 'boolean
+  :setting ("Set Printing Coercions. " . "Unset Printing Coercions. "))
+
+(defpacustom print-match-wildcards t
+  "*Print underscores for unused variables in matches."
+  :type 'boolean
+  :setting ("Set Printing Wildcard. " . "Unset Printing Wildcard. "))
+
+(defpacustom print-elim-types t
+  "*Print synthesised result type for eliminations."
+  :type 'boolean
+  :setting ("Set Printing Synth. " . "Unset Printing Synth. "))
+
+(defpacustom printing-depth 50
+  "*Depth of pretty printer formatting, beyond which dots are displayed."
+  :type 'integer
+  :setting "Set Printing Depth %i . ")
+
+(defpacustom time-commands nil
+  "*Whether to display timing information for each command."
+  :type 'boolean)
+
+(defpacustom auto-compile-vos nil
+  "Whether to automatically compile vos and track dependencies."
+  :type 'boolean)
+
+;; old adjustments:
+;;  :eval (if coq-auto-compile-vos
+;            (setq proof-shell-process-file
+;                  coq-proof-shell-process-file
+;                  proof-shell-inform-file-retracted-cmd
+;                  coq-proof-shell-inform-file-retracted-cmd)
+;          (setq proof-shell-inform-file-processed-cmd nil
+;                proof-shell-process-file nil
+;                proof-shell-inform-file-retracted-cmd nil)))
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Multiple file handling
@@ -1131,71 +1192,6 @@ Group number 1 matches the name of the library which is required.")
         ;; recursively call on ancestors: we hope coqdep doesn't give loop!
         (coq-process-file (coq-ancestors-of rfilename)))))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Flags and other settings for Coq.
-;; These appear on the Coq -> Setting menu.
-;;
-
-; FIXME da: we should send this command only inside a proof,
-; otherwise it gives an error message.  It should be on
-; a different menu command.
-;(defpacustom print-only-first-subgoal  nil
-;  "Whether to just print the first subgoal in Coq."
-;  :type 'boolean
-;  :setting ("Focus. " . "Unfocus. "))
-
-
-;; FIXME: to handle "printing all" properly, we should change the state
-;; of the variables that also depend on it.
-(defpacustom print-fully-explicit nil
-  "*Print fully explicit terms."
-  :type 'boolean
-  :setting ("Set Printing All. " . "Unset Printing All. "))
-
-(defpacustom print-implicit nil
-  "*Print implicit arguments in applications."
-  :type 'boolean
-  :setting ("Set Printing Implicit. " . "Unset Printing Implicit. "))
-
-(defpacustom print-coercions nil
-  "*Print coercions."
-  :type 'boolean
-  :setting ("Set Printing Coercions. " . "Unset Printing Coercions. "))
-
-(defpacustom print-match-wildcards t
-  "*Print underscores for unused variables in matches."
-  :type 'boolean
-  :setting ("Set Printing Wildcard. " . "Unset Printing Wildcard. "))
-
-(defpacustom print-elim-types t
-  "*Print synthesised result type for eliminations."
-  :type 'boolean
-  :setting ("Set Printing Synth. " . "Unset Printing Synth. "))
-
-(defpacustom printing-depth 50
-  "*Depth of pretty printer formatting, beyond which dots are displayed."
-  :type 'integer
-  :setting "Set Printing Depth %i . ")
-
-(defpacustom time-commands nil
-  "*Whether to display timing information for each command."
-  :type 'boolean)
-
-(defpacustom auto-compile-vos nil
-  "Whether to automatically compile vos and track dependencies."
-  :type 'boolean)
-
-;; old adjustments:
-;;  :eval (if coq-auto-compile-vos
-;            (setq proof-shell-process-file
-;                  coq-proof-shell-process-file
-;                  proof-shell-inform-file-retracted-cmd
-;                  coq-proof-shell-inform-file-retracted-cmd)
-;          (setq proof-shell-inform-file-processed-cmd nil
-;                proof-shell-process-file nil
-;                proof-shell-inform-file-retracted-cmd nil)))
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -1250,14 +1246,7 @@ mouse activation."
               (vector
                "Print Proof"
                `(proof-shell-invisible-command 
-                 ,(format "Print Proof %s." thm))))))
-  (if (string-equal idiom "proof")
-      (let ((thm (span-property span 'name)))
-        (list (vector
-               "Check"
-               `(proof-shell-invisible-command 
-                 ,(format "Check %s." thm))))))
-  )
+                 ,(format "Print Proof %s." thm)))))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;
@@ -1533,12 +1522,12 @@ buffer."
             ;(setq legth ??))
           ))
         (forward-char pos)
-        (let ((sp (make-span (point) (+ (point) lgth))))
+        (let ((sp (span-make (point) (+ (point) lgth))))
           (set-span-face sp 'proof-warning-face)
           ;; delete timer if exist
-          ;;(setq coq-highlight-error-timer (run-with-timer 10 nil 'delete-span sp))
+          ;;(setq coq-highlight-error-timer (run-with-timer 10 nil 'span-delete sp))
           (ignore-errors (sit-for 20)) ; errors here would skip the next delete
-          (delete-span sp)
+          (span-delete sp)
           )))))
 
 
diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el
index c9d1869f..f5957f2d 100644
--- a/demoisa/demoisa-easy.el
+++ b/demoisa/demoisa-easy.el
@@ -1,6 +1,6 @@
-;; demoisa-easy.el Example Proof General instance for Isabelle
+;; demoisa-easy.el --- Example Proof General instance for Isabelle
 ;;
-;; Copyright (C) 1999 LFCS Edinburgh. 
+;; Copyright (C) 1999 LFCS Edinburgh.
 ;;
 ;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
@@ -12,10 +12,10 @@
 ;; This mechanism is recommended for new instantiations of
 ;; Proof General since it follows a regular pattern, and we can more
 ;; easily adapt it in the future to new versions of Proof General
-;; using alternative architectures. It is still easy to augment 
+;; using alternative architectures. It is still easy to augment
 ;; with additional elisp functions and other settings.
 ;;
-;; The most important setting is `proof-shell-annotated-prompt-regexp' 
+;; The most important setting is `proof-shell-annotated-prompt-regexp'
 ;; used to recognize prompt texts from the prover.
 ;;
 ;; See demoisa.el and the Adapting Proof General manual for more
@@ -25,10 +25,15 @@
 ;; To test this file you must rename it demoisa.el.
 ;;
 
+(eval-when-compile
+  (require 'proof-site)			; compilation for demoisa
+  (proof-ready-for-assistant 'demoisa))
+
+(require 'proof)
 (require 'proof-easy-config)            ; easy configure mechanism
 
-(proof-easy-config 
- 'demoisa "Isabelle Demo" 
+(proof-easy-config
+ 'demoisa "Isabelle Demo"
  proof-prog-name		 "isabelle"
  proof-terminal-char             ?\;
  proof-script-comment-start             "(*"
@@ -58,3 +63,5 @@
  proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading")
 
 (provide 'demoisa)
+
+;;; demoisa-easy.el ends here
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index f9b75845..ed3aa8e1 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -84,6 +84,7 @@
    proof-save-command		"qed \"%s\";"
    proof-kill-goal-command	"Goal \"PROP no_goal_set\";"
    proof-assistant-home-page	isabelledemo-web-page
+   proof-prog-name		isabelledemo-prog-name
    proof-auto-multiple-files    t))
 
 
@@ -110,9 +111,6 @@
 ;; ======== Defining the derived modes ========
 ;;
 
-;; The name of the script mode is always <proofsym>-script,
-;; but the others can be whatever you like.
-;;
 ;; The derived modes set the variables, then call the
 ;; <mode>-config-done function to complete configuration.
 
@@ -134,25 +132,8 @@
   "Isabelle Demo goals" nil
   (proof-goals-config-done))
 
-;; The response buffer and goals buffer modes defined above are
-;; trivial.  In fact, we don't need to define them at all -- they
-;; would simply default to "proof-response-mode" and "pg-goals-mode".
-
 ;; A more sophisticated instantiation might set font-lock-keywords to
 ;; add highlighting, or some of the proof by pointing markup
 ;; configuration for the goals buffer.
 
-;; The final piece of magic here is a hook which configures settings
-;; to get the proof shell running.  Proof General needs to know the
-;; name of the program to run, and the modes for the shell, response,
-;; and goals buffers.
-
-(add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start)
-
-(defun demoisa-pre-shell-start ()
-  (setq proof-prog-name		isabelledemo-prog-name)
-  (setq proof-mode-for-shell    'demoisa-shell-mode)
-  (setq proof-mode-for-response 'demoisa-response-mode)
-  (setq proof-mode-for-goals	'demoisa-goals-mode))
-
 (provide 'demoisa)
diff --git a/etc/development-tips.txt b/etc/development-tips.txt
index b2f73cf0..89a525b8 100644
--- a/etc/development-tips.txt
+++ b/etc/development-tips.txt
@@ -1,3 +1,16 @@
+Please follow Emacs Lisp conventions as documented in the Emacs Lisp
+manual.  The 'checkdoc' mode helps with this, enabled automatically,
+alongside eldoc and Flyspell, in the development file:
+
+ M-x load-file RET generic/pg-dev.el RET
+
+ (load-file "../generic/pg-dev.el")
+
+
+
+
+
+
 Some Emacs Resources
 ====================
 
diff --git a/isa/README b/isa/README
index 4266b5e2..2be47ea5 100644
--- a/isa/README
+++ b/isa/README
@@ -1,4 +1,5 @@
 Support for Isabelle/classic has been removed from Proof General.
+
 The default and only supported interface is now Isabelle/Isar.
 
 If you need to use an older version of Isabelle, you will have
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index 65953162..e0dd6207 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -1,6 +1,6 @@
-;; isabelle-system.el Interface with Isabelle system
+;; isabelle-system.el --- Interface with Isabelle system
 ;;
-;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall. 
+;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall.
 ;;
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk>
 ;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
@@ -11,6 +11,11 @@
 ;; --------------------------------------------------------------
 ;;
 
+;;; Code:
+(eval-when-compile
+  (require 'proof-site)			; compile for isar (defpgdefault, etc)
+  (proof-ready-for-assistant 'isar))
+
 (require 'proof)			; for proof-assistant-symbol, etc.
 (require 'proof-syntax)			; for proof-string-match
 
@@ -32,7 +37,7 @@
 ;;; ================ Extract Isabelle settings ================
 
 (defcustom isa-isatool-command
-  (or (getenv "ISATOOL") 
+  (or (getenv "ISATOOL")
       (proof-locate-executable "isatool")
       ;; FIXME: use same mechanism as isabelle-program-name below.
       (let ((possibilities
@@ -53,7 +58,7 @@
   "Command to invoke Isabelle tool 'isatool'.
 XEmacs should be able to find `isatool' if it is on the PATH when
 started.  Then several standard locations are attempted.
-Otherwise you should set this, using a full path name here for reliable 
+Otherwise you should set this, using a full path name here for reliable
 working."
   :type 'file
   :group 'isabelle)
@@ -88,7 +93,7 @@ with full path."
       (substring s 0 -1))))
 
 (defun isa-getenv (envvar &optional default)
-  "Extract an environment variable setting using the `isatool' program.
+  "Extract environment variable ENVVAR setting using the `isatool' program.
 If the isatool command is not available, try using elisp's getenv
 to extract the value from Emacs' environment.
 If there is no setting for the variable, DEFAULT will be returned"
@@ -106,8 +111,8 @@ If there is no setting for the variable, DEFAULT will be returned"
 ;;; ======= Interaction with System using Isabelle tools =======
 ;;;
 
-(defcustom isabelle-program-name 
-  (if (fboundp 'proof-running-on-win32)	
+(defcustom isabelle-program-name
+  (if proof-running-on-win32
       "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\"
     (proof-locate-executable "isabelle" t
 			     '("/usr/local/Isabelle/bin/"
@@ -118,14 +123,14 @@ If there is no setting for the variable, DEFAULT will be returned"
 
 The default value except when running under Windows is \"isabelle\",
 which will get expanded using PATH if possible, or in a number
-of standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc). 
+of standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc).
 
 The default value when running under Windows is:
 
   C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\
 
-This expects SML/NJ in C:\\sml and Isabelle images in C:\Isabelle.  
-The logic image name is tagged onto the end.  
+This expects SML/NJ in C:\\sml and Isabelle images in C:\Isabelle.
+The logic image name is tagged onto the end.
 
 NB: The Isabelle settings mechanism or the environment variable
 ISABELLE will always override this setting."
@@ -136,7 +141,7 @@ ISABELLE will always override this setting."
   "Set from `isabelle-program-name', has name of logic appended sometimes.")
 
 (defun isabelle-command-line ()
-  "Make proper command line for running Isabelle"
+  "Make proper command line for running Isabelle."
   (let*
       ;; The ISABELLE and PROOFGENERAL_LOGIC values (as set when run
       ;; under the interface wrapper script) indicate that we should
@@ -161,22 +166,22 @@ ISABELLE will always override this setting."
 
 (defun isabelle-choose-logic (logic)
   "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
-  (interactive 
-   (list (completing-read 
+  (interactive
+   (list (completing-read
 	  "Use logic: "
-	  (mapcar 'list (cons "Default" 
+	  (mapcar 'list (cons "Default"
 			      isabelle-logics-available)))))
   ;; a little bit obnoxious maybe (but maybe what naive user would expect)
   ;; (customize-save-variable 'isabelle-chosen-logic logic)
   (if (proof-shell-live-buffer)
       (error "Can't change logic while Isabelle is running, please exit process first!"))
-  (customize-set-variable 'isabelle-chosen-logic 
+  (customize-set-variable 'isabelle-chosen-logic
 			  (unless (string-equal logic "Default") logic))
   (setq isabelle-prog-name (isabelle-command-line))
   (setq proof-prog-name isabelle-prog-name)
   ;; Settings are potentially different between logics, and
   ;; so are Isar keywords.  Set these to nil so they get
-  ;; automatically re-initialised.  
+  ;; automatically re-initialised.
   ;; FIXME: Isar keywords change not handled yet.
   (setq proof-assistant-settings nil)
   (setq proof-menu-settings nil))
@@ -184,7 +189,7 @@ ISABELLE will always override this setting."
 (defun isa-tool-list-logics ()
   "Generate a list of available object logics."
   (if (isa-set-isatool-command)
-      (delete "" (split-string 
+      (delete "" (split-string
 		  (isa-shell-command-to-string
 		   (concat isa-isatool-command " findlogics")) "[ \t]"))))
 
@@ -209,7 +214,7 @@ passed to isa-tool-doc-command, DOCNAME will be viewed."
 	  (mapcan
 	   (function (lambda (docdes)
 		       (if (proof-string-match "^[ \t]+\\(\\S-+\\)[ \t]+" docdes)
-			   (list (list 
+			   (list (list
 				  (substring docdes (match-beginning 1) (match-end 1))
 				  (substring docdes (match-end 0)))))))
 	   (split-string docs "\n"))))))
@@ -224,10 +229,10 @@ passed to isa-tool-doc-command, DOCNAME will be viewed."
 ;   (comint-send-eof))
 
 (defconst isabelle-verbatim-regexp "\\`\^VERBATIM: \\(\\(.\\|\n\\)*\\)\\'"
-  "Regexp matching internal marker for verbatim command output")
+  "Regexp matching internal marker for verbatim command output.")
 
 (defun isabelle-verbatim (str)
-  "Mark internal command for verbatim output"
+  "Mark internal command STR for verbatim output."
   (concat "\^VERBATIM: " str))
 
 
@@ -244,7 +249,7 @@ for you, you should disable this behaviour."
 (defcustom isabelle-logics-available (isa-tool-list-logics)
   "*List of logics available to use with Isabelle.
 If the `isatool' program is available, this is automatically
-generated with the lisp form `(isa-tool-list-logics)'."
+generated with the Lisp form `(isa-tool-list-logics)'."
   :type (list 'string)
   :group 'isabelle)
 
@@ -262,7 +267,7 @@ until Proof General is restarted."
 	       '(const :tag "Unset (use default)" nil)))
   :group 'isabelle)
 
-(defconst isabelle-docs-menu 
+(defconst isabelle-docs-menu
   (let ((vc '(lambda (docdes)
 	       (vector (car (cdr docdes))
 		       (list 'isa-view-doc (car docdes)) t))))
@@ -276,12 +281,12 @@ until Proof General is restarted."
   (setq isabelle-logics-menu-entries
 	(cons "Logics"
 	      (append
-	       '(["Default" 
+	       '(["Default"
 		  (isabelle-choose-logic nil)
 		  :active (not (proof-shell-live-buffer))
 		  :style radio
 		  :selected (not isabelle-chosen-logic)])
-	       (mapcar (lambda (l) 
+	       (mapcar (lambda (l)
 		   (vector l (list 'isabelle-choose-logic l)
 			   :active '(not (proof-shell-live-buffer))
 			   :style 'radio
@@ -289,7 +294,7 @@ until Proof General is restarted."
 		       isabelle-logics-available)))))
 
 (defvar isabelle-time-to-refresh-logics t
-  "Non-nil if we should refresh the logics list")
+  "Non-nil if we should refresh the logics list.")
 
 (defun isabelle-logics-menu-refresh ()
   "Refresh isabelle-logics-menu-entries, returning new entries."
@@ -299,9 +304,9 @@ until Proof General is restarted."
       (progn
 	(setq isabelle-logics-available (isa-tool-list-logics))
 	(isabelle-logics-menu-calculate)
-	(if proof-running-on-Emacs21 
+	(if (not (featurep 'xemacs))
 	    ;; update the menu manually
-	    (easy-menu-add-item proof-assistant-menu nil 
+	    (easy-menu-add-item proof-assistant-menu nil
 				isabelle-logics-menu-entries))
 	(setq isabelle-time-to-refresh-logics nil) ;; just done it, don't repeat!
 	(run-with-timer 2 nil ;; short delay to avoid doing this too often
@@ -313,22 +318,22 @@ until Proof General is restarted."
   (cdr isabelle-logics-menu-entries))
 
 ;; Functions for GNU Emacs only to update logics menu
-(if proof-running-on-Emacs21
+(if (not (featurep 'xemacs))
 (defun isabelle-menu-bar-update-logics ()
-  ;; standard check we're being invoked
+  "Update logics menu."
   (and (current-local-map)
-       (keymapp (lookup-key (current-local-map) 
+       (keymapp (lookup-key (current-local-map)
  			    (vector 'menu-bar (intern proof-assistant))))
        (isabelle-logics-menu-refresh))))
 
-(if proof-running-on-Emacs21
+(if (not (featurep 'xemacs))
     (add-hook 'menu-bar-update-hook 'isabelle-menu-bar-update-logics))
 
 
 (defvar isabelle-logics-menu-entries (isabelle-logics-menu-calculate))
 
-(defvar isabelle-logics-menu 
-   (if proof-running-on-XEmacs
+(defvar isabelle-logics-menu
+   (if (featurep 'xemacs)
        (cons (car isabelle-logics-menu-entries)
 	     (list :filter 'isabelle-logics-menu-filter)) ;; generates menu on click
      isabelle-logics-menu-entries)
@@ -373,17 +378,17 @@ until Proof General is restarted."
 ;;
 
 (eval-after-load "x-symbol-isar"
- ;; Add x-symbol tokens to isa-completion-table and rebuild
- ;; internal completion table if completion is already active
-'(progn
-   (defpgdefault completion-table
-     (append (proof-ass completion-table)
-	     (mapcar (lambda (xsym) (nth 2 xsym))
-		     x-symbol-isar-table)))
-   (setq proof-xsym-font-lock-keywords
-	 x-symbol-isar-font-lock-keywords)
-   (if (featurep 'completion)
-       (proof-add-completions))))
+  ;; Add x-symbol tokens to isa-completion-table and rebuild
+  ;; internal completion table if completion is already active
+  '(progn
+     (defpgdefault completion-table
+       (append isar-completion-table
+	       (mapcar (lambda (xsym) (nth 2 xsym))
+		       x-symbol-isar-table)))
+     (setq proof-xsym-font-lock-keywords
+	   x-symbol-isar-font-lock-keywords)
+     (if (featurep 'completion)
+	 (proof-add-completions))))
 
 
 
@@ -413,15 +418,15 @@ the function `pg-remove-specials' can be used instead)."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Context-senstive in-span menu additions 
+;; Context-senstive in-span menu additions
 ;;
 
 (defun isabelle-create-span-menu (span idiom name)
   (if (string-equal idiom "proof")
       (let ((thm (span-property span 'name)))
-	(list (vector 
-	       "Visualise dependencies" 
-	       `(proof-shell-invisible-command 
+	(list (vector
+	       "Visualise dependencies"
+	       `(proof-shell-invisible-command
 		 ,(format "thm_deps %s;" thm))
 	       (not (string-equal thm proof-unnamed-theorem-name)))))))
 
@@ -442,4 +447,4 @@ the function `pg-remove-specials' can be used instead)."
 
 
 (provide 'isabelle-system)
-;; End of isabelle-system.el
+;;; isabelle-system.el ends here
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 98f5798a..8bd908b4 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -9,6 +9,8 @@
 ;; $Id$
 ;;
 
+(require 'cl)				; remove-if, remove-if-not
+
 (require 'proof-syntax)
 (require 'isar-keywords)
 
@@ -35,7 +37,7 @@
          ?\( "()1"
          ?\) ")(4")
    (cond
-    (proof-running-on-XEmacs
+    ((featurep 'xemacs)
      ;; We classify {* sequences *} as comments, although
      ;; they need to be passed as command args as text.
      ;; NB: adding a comment sequence b seems to break
@@ -49,7 +51,7 @@
     ;;(?\{ "(}1")
     ;;(?\} "){4")
     ;;(?\* ". 23"))
-    (proof-running-on-Emacs21
+    ((not (featurep 'xemacs))
      '(?\{ "(}1b"
        ?\} "){4b"
        ?\* ". 23n"))))
@@ -460,7 +462,7 @@ matches contents of quotes for quoted identifiers.")
 
 (defun isar-undos (i)
   (if (> i 0) (concat "undos_proof " (int-to-string i) ";")
-    proof-no-command))
+    nil))
 
 (defun isar-cannot-undo (cmd)
   (concat "cannot_undo \"" cmd "\";"))
diff --git a/isar/isar.el b/isar/isar.el
index 1c3f86c1..a3d2629f 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -1,9 +1,9 @@
-; isar.el	  Major mode for Isabelle/Isar proof assistant
+; isar.el --- Major mode for Isabelle/Isar proof assistant
 ;; Copyright (C) 1994-2004 LFCS Edinburgh.
 ;;
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
-;; Maintainers:   David Aspinall, Stefan Berghofer
+;; Maintainers:   David Aspinall, Makarius, Stefan Berghofer
 ;;
 ;; Authors:       David Aspinall <David.Aspinall@ed.ac.uk>
 ;;   	          Markus Wenzel <wenzelm@in.tum.de>
@@ -14,13 +14,16 @@
 ;; $Id$
 ;;
 
+;;; Code:
 (require 'proof)
 
-;; System code
-(require 'isabelle-system)
+(eval-when-compile
+  (require 'span)
+  (require 'proof-syntax)
+  (proof-ready-for-assistant 'isar))	; compile for isar
 
-;; "Find Theorems" search form
-(require 'isar-find-theorems)
+(require 'isabelle-system)		; system code
+(require 'isar-find-theorems)		; "Find Theorems" search form
 
 ;;
 ;; Load syntax
@@ -35,7 +38,7 @@ See -k option for Isabelle interface script."
     ;; Pickup isar-keywords file from somewhere appropriate,
     ;; giving user chance to set name of file, or based on
     ;; name of logic.
-    (isabelle-load-isar-keywords 
+    (isabelle-load-isar-keywords
      (or isar-keywords-name
 	 isabelle-chosen-logic)))
 (require 'isar-syntax)
@@ -53,9 +56,9 @@ See -k option for Isabelle interface script."
 
 ;; Adjust toolbar entries (must be done before proof-toolbar is loaded).
 
-(if proof-running-on-XEmacs
-    (setq isar-toolbar-entries
-	  (remassoc 'qed (remassoc 'goal isar-toolbar-entries))))
+(eval-after-load "pg-custom"
+  '(setq isar-toolbar-entries
+	 (remassoc 'qed (remassoc 'goal isar-toolbar-entries))))
 
 
 (defun isar-strip-terminators ()
@@ -80,10 +83,10 @@ See -k option for Isabelle interface script."
   "Configure generic proof scripting mode variables for Isabelle/Isar."
   (setq
    proof-assistant-home-page    isar-web-page
-   proof-mode-for-script        'isar-mode
+   proof-prog-name		(isabelle-command-line)
    ;; proof script syntax
    proof-terminal-char          ?\;     ; forcibly ends a command
-   proof-script-command-start-regexp 
+   proof-script-command-start-regexp
    (proof-regexp-alt
     ;; FIXME: this gets { and } wrong: they must _not_ appear as {* *}
     ;; because that's lexically a kind of comment.
@@ -138,7 +141,7 @@ See -k option for Isabelle interface script."
    proof-find-and-forget-fn     'isar-find-and-forget
    proof-state-preserving-p     'isar-state-preserving-p
    proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list
-   ;; span menu 
+   ;; span menu
    proof-script-span-context-menu-extensions 'isabelle-create-span-menu))
 
 (defun isar-shell-mode-config-set-variables ()
@@ -189,7 +192,7 @@ See -k option for Isabelle interface script."
    proof-shell-eager-annotation-start-length 1
    proof-shell-eager-annotation-start   "\360\\|\362\\|\^AI\\|\^AK"
    proof-shell-eager-annotation-end     "\361\\|\363\\|\^AJ\\|\^AL"
-   ;; see isar-pre-shell-start for proof-shell-trace-output-regexp
+   proof-shell-trace-output-regexp	"\375\\|\^AV"
 
    ;; Isabelle is learning to talk PGIP...
    proof-shell-match-pgip-cmd		"<pgip"
@@ -203,7 +206,7 @@ See -k option for Isabelle interface script."
    proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\\(\361\\|\^AJ\\)"
    proof-shell-theorem-dependency-list-split "\" \""
    proof-shell-show-dependency-cmd "thm %s;"
-   proof-shell-identifier-under-mouse-cmd 
+   proof-shell-identifier-under-mouse-cmd
    '((nil     "thm %s;")
      (string  "term \"%s\";")
      (comment "term \"%s\";"))
@@ -218,7 +221,7 @@ See -k option for Isabelle interface script."
      ;; next string could be: "[\350-\377]", but that's buggy with XEmacs 21.5 (beta)
      "×\\|Ø\\|Ù\\|Ú\\|Û\\|Ü\\|Ý\\|Þ\\|ß\\|8\\|è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ")
 
-   pg-subterm-help-cmd			"term %s" 
+   pg-subterm-help-cmd			"term %s"
 
    proof-cannot-reopen-processed-files  t
    proof-shell-process-file
@@ -295,7 +298,7 @@ proof-shell-retract-files-regexp."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;;;
-;;; help menu  
+;;; help menu
 ;;;
 
 ;;; da: how about a `C-c C-a h ?' for listing available keys?
@@ -320,15 +323,15 @@ proof-shell-retract-files-regexp."
 ;; Command menu
 ;;
 
-;; NB: would be nice to query save of the buffer first for these 
+;; NB: would be nice to query save of the buffer first for these
 ;; next two: but only convenient emacs functions offer save for
 ;; all buffers.
 (proof-definvisible isar-cmd-display-draft
  '(format "display_drafts \"%s\"" buffer-file-name)
  [(control d)])
 
-(proof-definvisible isar-cmd-print-draft 
-  '(if (y-or-n-p 
+(proof-definvisible isar-cmd-print-draft
+  '(if (y-or-n-p
 	(format "Print draft of file %s ?" buffer-file-name))
        (format "print_drafts \"%s\"" buffer-file-name)
      (error "Aborted."))
@@ -369,7 +372,7 @@ proof-shell-retract-files-regexp."
 
 ;; undo proof commands
 (defun isar-count-undos (span)
-  "Count number of undos in a span, return the command needed to undo that far."
+  "Count number of undos SPAN, return command needed to undo that far."
   (let
       ((case-fold-search nil)       ;FIXME ??
        (ct 0) str i)
@@ -379,7 +382,7 @@ proof-shell-retract-files-regexp."
              (or (proof-string-match isar-undo-skip-regexp str)
 		 (proof-string-match isar-undo-ignore-regexp str)
                  (setq ct (+ 1 ct))))
-            ((eq (span-property span 'type) 'pbp)  
+            ((eq (span-property span 'type) 'pbp)
              ;; this case for automatically inserted text (e.g. sledgehammer)
              (cond ((not (proof-string-match isar-undo-skip-regexp str))
 		    (setq ct 1)
@@ -404,7 +407,7 @@ proof-shell-retract-files-regexp."
       (cond
        ;; comment, diagnostic, nested proof command: skip
        ;; (da: adding new span types may break this code,
-       ;;  ought to test for type 'cmd before looking at 
+       ;;  ought to test for type 'cmd before looking at
        ;;  str below)
        ;; FIXME: should adjust proof-nesting-depth here.
        ((or (eq (span-property span 'type) 'comment)
@@ -434,15 +437,13 @@ proof-shell-retract-files-regexp."
       (if span (setq span (next-span span 'type))))
     (if (null answers) proof-no-command (apply 'concat answers))))
 
-
-
 (defun isar-goal-command-p (span)
-  "Decide whether argument is a goal or not"
-  (proof-string-match isar-goal-command-regexp 
+  "Decide whether argument SPAN is a goal or not."
+  (proof-string-match isar-goal-command-regexp
 		      (or (span-property span 'cmd) "")))
 
 (defun isar-global-save-command-p (span str)
-  "Decide whether argument really is a global save command"
+  "Decide whether argument SPAN with command STR is a global save command."
   (or
    (proof-string-match isar-global-save-command-regexp str)
    (let ((ans nil) (lev 0) cmd)
@@ -463,10 +464,10 @@ proof-shell-retract-files-regexp."
      (eq ans 'yes))))
 
 (defvar isar-current-goal 1
-  "Last goal that emacs looked at.")
+  "Last goal that Emacs looked at.")
 
 (defun isar-state-preserving-p (cmd)
-  "Non-nil if command preserves the proofstate."
+  "Non-nil if command CMD preserves the proofstate."
   (proof-string-match isar-undo-skip-regexp cmd))
 
 
@@ -489,13 +490,11 @@ proof-shell-retract-files-regexp."
 ;;   Isar shell startup and exit hooks                              ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;borrowed from plastic.el
 (defvar isar-shell-current-line-width nil
   "Current line width of the Isabelle process's pretty printing module.
 Its value will be updated whenever the corresponding screen gets
 selected.")
 
-;borrowed from plastic.el
 (defun isar-shell-adjust-line-width ()
   "Use Isabelle's pretty printing facilities to adjust output line width.
 Checks the width in the `proof-goals-buffer'"
@@ -505,9 +504,8 @@ Checks the width in the `proof-goals-buffer'"
          (save-excursion
            (set-buffer proof-goals-buffer)
            (let ((current-width
-                  ;; Actually, one might sometimes
-                  ;; want to get the width of the proof-response-buffer
-                  ;; instead. Never mind.
+                  ;; Actually, one might want the width of the
+                  ;; proof-response-buffer instead. Never mind.
                   (max 20 (window-width (get-buffer-window proof-goals-buffer t)))))
 
              (if (equal current-width isar-shell-current-line-width) ()
@@ -516,20 +514,12 @@ Checks the width in the `proof-goals-buffer'"
                (setq ans (format "pretty_setmargin %d;" (- current-width 4)))))))
     ans))
 
-(defun isar-pre-shell-start ()
-  (setq proof-prog-name         (isabelle-command-line))
-  (setq proof-mode-for-shell    'isar-shell-mode)
-  (setq proof-mode-for-goals    'isar-goals-mode)
-  (setq proof-mode-for-response 'isar-response-mode)
-  (setq proof-shell-trace-output-regexp "\375\\|\^AV"))
-
-
 ;;
 ;;   Configuring proof output buffer
 ;;
 
 (defun isar-preprocessing ()  ;dynamic scoping of `string'
-  "Insert sync markers - acts on variable STRING by dynamic scoping"
+  "Insert sync markers - acts on variable STRING by dynamic scoping."
   (if (proof-string-match isabelle-verbatim-regexp string)
       (setq string (match-string 1 string))
     (unless (proof-string-match ";[ \t]*\\'" string)
@@ -556,18 +546,17 @@ Checks the width in the `proof-goals-buffer'"
   (isar-init-syntax-table)
   (setq font-lock-keywords isar-font-lock-keywords-1)
   (setq comment-quote-nested nil) ;; can cope with nested comments
-  (proof-config-done)
   (set (make-local-variable 'outline-regexp) isar-outline-regexp)
   (set (make-local-variable 'outline-heading-end-regexp) isar-outline-heading-end-regexp)
   (setq blink-matching-paren-dont-ignore-comments t)
-  (add-hook 'proof-pre-shell-start-hook 'isar-pre-shell-start nil t)
-  (add-hook 'proof-shell-insert-hook 'isar-preprocessing))
+  (add-hook 'proof-shell-insert-hook 'isar-preprocessing)
+  (proof-config-done))
 
 (defun isar-shell-mode-config ()
   "Configure Proof General proof shell for Isabelle/Isar."
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords  
-	(append 
+  (setq font-lock-keywords
+	(append
 	 isar-output-font-lock-keywords-1
 	 (if (boundp 'x-symbol-isar-font-lock-keywords)
 	     x-symbol-isar-font-lock-keywords)))
@@ -576,10 +565,10 @@ Checks the width in the `proof-goals-buffer'"
 
 (defun isar-response-mode-config ()
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords  
-	(append 
+  (setq font-lock-keywords
+	(append
 	 isar-output-font-lock-keywords-1
-	 (if (proof-ass x-symbol-enable)
+	 (if isar-x-symbol-enable
 	     x-symbol-isar-font-lock-keywords)))
   (proof-response-config-done))
 
@@ -587,31 +576,23 @@ Checks the width in the `proof-goals-buffer'"
   (setq pg-goals-change-goal "prefer %s")
   (setq pg-goals-error-regexp proof-shell-error-regexp)
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords  
-	(append 
+  (setq font-lock-keywords
+	(append
 	 isar-goals-font-lock-keywords
-	 (if (proof-ass x-symbol-enable)
+	 (if isar-x-symbol-enable
 	     x-symbol-isar-font-lock-keywords)))
   (proof-goals-config-done))
 
 (defun isar-goalhyplit-test ()
   "Value for `pg-topterm-goalhyplit-fn' (see that variable for documentation)."
   (let ((start (point)))
-    (if (proof-re-search-forward "\377\\|\^AX" nil t) ;; end of literal command (non-standard)
+    (if (proof-re-search-forward
+	 "\377\\|\^AX" nil t) ; end of literal command (non-standard)
 	(progn
 	  (delete-region (match-beginning 0) (match-end 0))
 	  (cons 'lit (buffer-substring start (match-beginning 0)))))))
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Remove isa-mode from auto-mode-alist, 
-;; to allow SML mode to work in preference to isa-mode.
-;;
-
-(setq auto-mode-alist
-      (delete-if 
-       (lambda (strmod) (memq (cdr strmod) '(demoisa-mode)))
-       auto-mode-alist))
-
 (provide 'isar)
+
+;;; isar.el ends here
diff --git a/isar/x-symbol-isar.el b/isar/x-symbol-isar.el
index 4f61d702..9bb3c28e 100644
--- a/isar/x-symbol-isar.el
+++ b/isar/x-symbol-isar.el
@@ -505,10 +505,10 @@ variable `x-symbol-auto-coding-alist' for details."
 ;;
 
 (eval-after-load "isar" ;; allow use outside PG
-  (setq 
-   proof-xsym-activate-command
-   (isar-markup-ml "change print_mode (insert (op =) \"xsymbols\")")
-   proof-xsym-deactivate-command
-   (isar-markup-ml "change print_mode (remove (op =) \"xsymbols\")")))
+  '(setq 
+    proof-xsym-activate-command
+    (isar-markup-ml "change print_mode (insert (op =) \"xsymbols\")")
+    proof-xsym-deactivate-command
+    (isar-markup-ml "change print_mode (remove (op =) \"xsymbols\")")))
 
 (provide 'x-symbol-isar)
diff --git a/lclam/lclam.el b/lclam/lclam.el
index ae171aa0..2cc14d66 100644
--- a/lclam/lclam.el
+++ b/lclam/lclam.el
@@ -47,6 +47,8 @@
    proof-kill-goal-command         nil
    proof-assistant-homepage        lclam-web-page
    proof-auto-multiple-files       nil 
+   proof-prog-name		   lclam-prog-name
+   proof-shell-process-connection-type t
    ))
 
 (defun lclam-shell-config ()
@@ -100,16 +102,6 @@
     (lclam-proofscript-mode)))
 )
 
-;; Hook which configures settings to get the proof shell running 
-
-(add-hook 'proof-pre-shell-start-hook 'lclam-pre-shell-start)
-
-(defun lclam-pre-shell-start ()
-  (setq proof-prog-name         lclam-prog-name)
-  (setq proof-mode-for-shell    'lclam-shell-mode)
-  (setq proof-mode-for-response 'lclam-response-mode)
-  (setq proof-mode-for-goals    'lclam-goals-mode)
-  (setq proof-shell-process-connection-type t))
 
 
 ;;
@@ -197,7 +189,7 @@
   (proof-shell-invisible-command
    (proof-format-filename
     ;; %r parameter means relative (don't expand) path
-    (format "use_thy \"%%r\"." (if try "try_" ""))
+    (format "use_thy \"%s%%r\"." (if try "try_" ""))
     (file-name-nondirectory file))
    wait))
 
diff --git a/lego/lego.el b/lego/lego.el
index 7a80df31..bffdf290 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -195,7 +195,7 @@ Given is the first SPAN which needs to be undone."
     ;; FIXME: make this stuff generic.  This should be undo-n-times-cmd
     (concat "Undo " (int-to-string ct) ";")))
 
-(defun lego-goal-command-p (str)
+(defun lego-goal-command-p (span)
   "Decide whether argument is a goal or not"
   (proof-string-match lego-goal-command-regexp
 		      (or (span-property span 'cmd) "")))
@@ -294,13 +294,6 @@ Checks the width in the `proof-goals-buffer'"
 	     (insert (format lego-pretty-set-width (- current-width 1)))
 	     )))))
 
-(defun lego-pre-shell-start ()
-  (setq proof-prog-name lego-prog-name
-	proof-mode-for-shell 'lego-shell-mode
-	proof-mode-for-response 'lego-response-mode
-	proof-mode-for-goals 'lego-goals-mode))
-
-
 (defun lego-mode-config ()
 
   (setq proof-terminal-char ?\;)
@@ -309,14 +302,14 @@ Checks the width in the `proof-goals-buffer'"
 
   (setq proof-assistant-home-page lego-www-home-page)
   
-  (setq proof-mode-for-script 'lego-mode)
-
   (setq proof-showproof-command "Prf;"
 	proof-goal-command "Goal %s;"
 	proof-save-command "Save %s;"
 	proof-context-command "Ctxt;"
 	proof-info-command "Help;")
 
+  (setq proof-prog-name lego-prog-name)
+
   (setq proof-goal-command-p 'lego-goal-command-p
 	proof-completed-proof-behaviour 'closeany ; new in 3.0
 	proof-count-undos-fn 'lego-count-undos
@@ -367,7 +360,6 @@ Checks the width in the `proof-goals-buffer'"
 
 ;; hooks and callbacks
 
-  (add-hook 'proof-pre-shell-start-hook 'lego-pre-shell-start nil t)
   (add-hook 'proof-shell-insert-hook 'lego-shell-adjust-line-width))
 
 (defun lego-equal-module-filename (module filename)
diff --git a/lib/bufhist.el b/lib/bufhist.el
index aa58a37d..4917819f 100644
--- a/lib/bufhist.el
+++ b/lib/bufhist.el
@@ -73,14 +73,18 @@
        indicator
        'help-echo desc
        'keymap (eval-when-compile
-		 (let ((map (make-sparse-keymap)))
-		   ;; FIXME: clicking can go wrong here because the
-		   ;; current buffer can be something else which has no hist!
-		   (define-key map [mode-line mouse-1] 'bufhist-prev)
-		   (define-key map [mode-line mouse-3] 'bufhist-next)
-;		   (define-key map [mode-line control mouse-1] 'bufhist-first)
-;		   (define-key map [mode-line control mouse-3] 'bufhist-last)
-		   map))
+		 (cond 
+		  ((featurep 'xemacs)
+		   nil)
+		  (t
+		   (let ((map (make-sparse-keymap)))
+		     ;; FIXME: clicking can go wrong here because the
+		     ;; current buffer can be something else which has no hist!
+		     (define-key map [mode-line mouse-1] 'bufhist-prev)
+		     (define-key map [mode-line mouse-3] 'bufhist-next)
+		     ;; (define-key map [mode-line control mouse-1] 'bufhist-first)
+		     ;; (define-key map [mode-line control mouse-3] 'bufhist-last)
+		   map))))
        'mouse-face 'mode-line-highlight))))
      
 ;simple:
diff --git a/lib/holes.el b/lib/holes.el
index a4db4a23..fa7f6f92 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -143,7 +143,7 @@ is), which is annoying.
 (defvar holes-default-hole (make-detached-span)
   "An empty detached hole used as the default hole.
 You should not use this variable.")
-(detach-span holes-default-hole)
+(span-detach holes-default-hole)
 (defvar holes-active-hole holes-default-hole
   "The current active hole.
 There can be only one active hole at a time,
@@ -366,7 +366,7 @@ Error if HOLE is not a hole."
 
 (defun holes-make-hole (start end)
   "Make and return an (span) hole from START to END."
-  (let ((ext (make-span start end)))
+  (let ((ext (span-make start end)))
     (set-span-properties
      ext `(
 	   hole t
@@ -419,7 +419,7 @@ the span."
   (if (and (holes-active-hole-exist-p) (eq holes-active-hole HOLE))
       (holes-disable-active-hole)
     )
-  (delete-span HOLE)
+  (span-delete HOLE)
   )
 
 (defun holes-clear-hole-at (&optional pos)
@@ -442,7 +442,7 @@ the span."
 (defun holes-mapcar-holes (FUNCTION &optional FROM TO PROP)
 					; checkdoc-params: (FUNCTION FROM TO PROP)
   "Internal."
-  (mapcar-spans FUNCTION FROM TO 'hole)
+  (span-mapcar-spans FUNCTION FROM TO 'hole)
   )
 
 (defun holes-clear-all-buffer-holes (&optional start end)
@@ -524,7 +524,7 @@ goal(FIXME?).  Use `replace-active-hole' instead."
 			     (or str (car kill-ring)) ;kill ring?
 			     (span-buffer exthole)
 			     )
-      (detach-span exthole) ;; this seems necessary for span overlays,
+      (span-detach exthole) ;; this seems necessary for span overlays,
       ;; where the buffer attached to the span is
       ;; not removed automatically by the fact
       ;; that the span is removed from the buffer
@@ -648,7 +648,7 @@ Sets `holes-active-hole' to the next hole if it exists."
 	       (eq sp holes-active-hole))
 	  (holes-disable-active-hole))
       (holes-replace "" sp)
-      (detach-span sp)
+      (span-detach sp)
       )
     (message "hole killed")
     )
@@ -678,7 +678,7 @@ Sets `holes-active-hole' to the next hole if it exists."
     (let ((ext (holes-hole-at-event event)))
       (if (eq ext holes-active-hole)
 	  (holes-disable-active-hole))
-      (detach-span ext)
+      (span-detach ext)
       )
     )
   (message "hole deleted")
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 96a73ff3..43e8a2f2 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -10,27 +10,22 @@
 ;; operating systems and Emacs versions.  This is to help keep
 ;; track of them.
 ;;
-;; The development policy for Proof General is for the main codebase
-;; to be written for the latest stable version of GNU Emacs (previously
-;; XEmacs, not yet reworked since 3.7). 
-;; We follow GNU Emacs advice on removing obsolete function calls.
+;; The development policy for Proof General (since v3.7) is for the
+;; main codebase to be written for the latest stable version of GNU
+;; Emacs, following GNU Emacs advice on obsolete function calls.
 ;;
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
 ;;; Architecture flags
 ;;;
 
-(eval-and-compile
-(defvar proof-running-on-XEmacs (string-match "XEmacs" emacs-version)
-  "Non-nil if Proof General is running on XEmacs.")
-(defvar proof-running-on-Emacs21 (and (not proof-running-on-XEmacs)
-				      (>= emacs-major-version 21))
-  "Non-nil if Proof General is running on GNU Emacs 21 or later.")
-;; rough test for XEmacs on win32, anyone know about GNU Emacs on win32?
-(defvar proof-running-on-win32 (fboundp 'win32-long-file-name)
-  "Non-nil if Proof General is running on a win32 system.")
-)
+;; can use eval-and-compile to allow optimisation, but that would
+;; require recompilation for Windows
+(defvar proof-running-on-win32 (memq system-type '(win32 windows-nt cygwin))
+  "Non-nil if Proof General is running on a windows variant system.")
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -83,9 +78,7 @@ Search for COMMAND in exec-path and return the absolute file name.
 Return nil if COMMAND is not found anywhere in `exec-path'." nil nil))
 
 
-;; Compatibility with XEmacs 20.3/4
-(or (boundp 'path-separator)
-    (setq path-separator (if proof-running-on-win32 ";" ":")))
+;; Compatibility with XEmacs 20.3
 (or (fboundp 'split-path)
     (defun split-path (path)
       "Explode a search path into a list of strings.
@@ -95,50 +88,6 @@ with `path-separator'."
 
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;;
-;;; Window systems
-;;;
-
-;; A useful function of GNU Emacs: support it in XEmacs if not already there
-;; NOTE!  Unfortunately this is present in some XEmacs versions but
-;; returns the wrong value (e.g. nil on a graphic display).
-; (or (fboundp 'display-graphic-p)
-;     (defun display-graphic-p ()
-;       "Return non-nil if DISPLAY is a graphic display.
-; Graphical displays are those which are capable of displaying several
-; frames and several different fonts at once.  This is true for displays
-; that use a window system such as X, and false for text-only terminals."
-;       (not (memq (console-type) '(tty stream dead)))))
-
-;; Let's define our own version based on window-system.  
-;; Even though this is deprecated on XEmacs, it seems more likely
-;; that things will go wrong on badly ported Emacs than users
-;; using multiple devices, some of which are ttys...
-(defun pg-window-system ()
-  "Return non-nil if we're on a window system.  Simply use `window-system'."
-  (and window-system t))
-
-;; The next constant is used in proof-config for defface calls.
-;; Unfortunately defface uses window-system, which Emacs porters like
-;; to invent new symbols for each time, which is a pain.
-;; This list has the ones I know about so far.  
-
-(defconst pg-defface-window-systems 
-  '(x            ;; bog standard
-    mswindows    ;; Windows
-    gtk          ;; gtk emacs (obsolete?)
-    mac          ;; used by Aquamacs
-    carbon       ;; used by Carbon XEmacs
-    ns           ;; NeXTstep Emacs (Emacs.app)
-    x-toolkit)   ;; possible catch all (but probably not)
-  "A list of possible values for `window-system'.
-If you are on a window system and your value of `window-system' is
-not listed here, you may not get the correct syntax colouring behaviour.")
-
-
-
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -161,7 +110,8 @@ Unless optional argument INPLACE is non-nil, return a new string."
 
 ;; Required by xmltok.el [not used at present], proof-shell.el
 (or (fboundp 'replace-regexp-in-string)
-;; Code is taken from Emacs 21.1.1/subr.el 
+
+;; Code is taken from Emacs 21.1.1/subr.el. Now in XEmacs (21.5b28, at least)
 (defun replace-regexp-in-string (regexp rep string &optional
 					fixedcase literal subexp start)
   "Replace all matches for REGEXP with REP in STRING.
@@ -224,7 +174,7 @@ and replace a sub-expression, e.g.
 ;; :visible keyword.  To use that when it's available, we set a
 ;; constant to be :visible or :active
 
-(defconst menuvisiblep (if proof-running-on-Emacs21 :visible :active)
+(defconst menuvisiblep (if (featurep 'xemacs) :active :visible)
   ":visible (on GNU Emacs) or :active (otherwise). 
 The GNU Emacs implementation of easy-menu-define has a very handy
 :visible keyword.  To use that when it's available, we use this constant.")
@@ -294,7 +244,7 @@ The value returned is the value of the last form in BODY."
 ;; dynamic-completion-mode after loading it.
 (or (fboundp 'complete)
     (autoload 'complete "completion"))
-(unless proof-running-on-XEmacs
+(unless (featurep 'xemacs)
   (eval-after-load "completion"
     '(dynamic-completion-mode)))
 
@@ -317,64 +267,11 @@ The value returned is the value of the last form in BODY."
   "Dummy function for Proof General on GNU Emacs."
   (force-mode-line-update)))
 
-;; Interactive flag
-(or (fboundp 'noninteractive)
-    (defun noninteractive ()
-      "Dummy function for Proof General on GNU Emacs."
-      noninteractive))
-
-;; Replacing in string (useful function from subr.el in XEmacs 21.1.9)
+;; Replace in string: XEmacs original now in GNU Emacs as replace-regexp-in-string
 (or (fboundp 'replace-in-string)
-    (if (fboundp 'replace-regexp-in-string)
-      (defun replace-in-string (str regexp newtext &optional literal)
-        (replace-regexp-in-string regexp newtext str 'fixedcase literal))
-(defun replace-in-string (str regexp newtext &optional literal)
-  "Replace all matches in STR for REGEXP with NEWTEXT string,
- and returns the new string.
-Optional LITERAL non-nil means do a literal replacement.
-Otherwise treat \\ in NEWTEXT string as special:
-  \\& means substitute original matched text,
-  \\N means substitute match for \(...\) number N,
-  \\\\ means insert one \\."
-  ;; Not present in GNU
-  ;; (check-argument-type 'stringp str)
-  ;; (check-argument-type 'stringp newtext)
-  (let ((rtn-str "")
-	(start 0)
-	(special)
-	match prev-start)
-    (while (setq match (string-match regexp str start))
-      (setq prev-start start
-	    start (match-end 0)
-	    rtn-str
-	    (concat
-	      rtn-str
-	      (substring str prev-start match)
-	      (cond (literal newtext)
-		    (t (mapconcat
-			(lambda (c)
-			  (if special
-			      (progn
-				(setq special nil)
-				(cond ((eq c ?\\) "\\")
-				      ((eq c ?&)
-				       (substring str
-						  (match-beginning 0)
-						  (match-end 0)))
-				      ((and (>= c ?0) (<= c ?9))
-				       (if (> c (+ ?0 (length
-						       (match-data))))
-					   ;; Invalid match num
-					   (error "Invalid match num: %c" c)
-					 (setq c (- c ?0))
-					 (substring str
-						    (match-beginning c)
-						    (match-end c))))
-				      (t (char-to-string c))))
-			    (if (eq c ?\\) (progn (setq special t) nil)
-			      (char-to-string c))))
-			 newtext ""))))))
-    (concat rtn-str (substring str start))))))
+    (defun replace-in-string (str regexp newtext &optional literal)
+      (replace-regexp-in-string regexp newtext str 'fixedcase literal)))
+
 
 ;; An implemenation of buffer-syntactic-context for GNU Emacs
 (defun proof-buffer-syntactic-context-emulate (&optional buffer)
@@ -540,11 +437,11 @@ The value returned is the value of the last form in BODY."
 ;;; Attempt to harmonise pop-to-buffer behaviour 
 ;;;
 
-(if proof-running-on-Emacs21
+(or (featurep 'xemacs)
     ;; NB: GNU Emacs version has fewer args
     (defalias 'pg-pop-to-buffer 'pop-to-buffer))
 
-(if proof-running-on-XEmacs
+(if (featurep 'xemacs)
 ;; Version from XEmacs 21.4.12, with args to match GNU Emacs
 ;; NB: GNU Emacs version has fewer args, we don't use ON-FRAME
 (defun pg-pop-to-buffer (bufname &optional not-this-window-p no-record on-frame)
@@ -585,7 +482,7 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
       ;; select-window will modify the internal keyboard focus of XEmacs
       (select-window window))
     buf))
-);;; End XEmacs only
+)
 
   
 
@@ -630,7 +527,7 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
 ;; PG 3.5.1: add hack in proof-compat.el to deal with this
 (if
     (and
-     proof-running-on-Emacs21
+     (not (featurep 'xemacs))
      (or
       (string-equal emacs-version "21.2.1")
       (string-equal emacs-version "21.1.0")))
@@ -653,23 +550,23 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
 ;; in this function.  In XEmacs post 21.5 one can set names of buffers
 ;; to omit just from tabs list.
 
-(if proof-running-on-XEmacs
+(if (featurep 'xemacs)
     (progn
 
-(fset 'select-buffers-tab-buffers-by-mode-old 
-      (symbol-function 'select-buffers-tab-buffers-by-mode))
-
-(defun select-buffers-tab-buffers-by-mode (buf1 buf2)
-      (let* ((mode1 (symbol-value-in-buffer 'major-mode buf1)) ;; candidate buf
-	     (mode2 (symbol-value-in-buffer 'major-mode buf2)) ;; displayed buf
-	     (auxes '(proof-goals-mode proof-shell-mode proof-response-mode))
-	     (mode1aux (memq (get mode1 'derived-mode-parent) auxes))
-	     (mode2aux (memq (get mode2 'derived-mode-parent) auxes)))
-	(cond
-	 (mode1aux	mode2aux)
-	 (mode2aux	nil)
-	 (t             (select-buffers-tab-buffers-by-mode-old buf1 buf2)))))
-)) ;; end running-on-XEmacs
+      (fset 'select-buffers-tab-buffers-by-mode-old 
+	    (symbol-function 'select-buffers-tab-buffers-by-mode))
+
+      (defun select-buffers-tab-buffers-by-mode (buf1 buf2)
+	(let* ((mode1 (symbol-value-in-buffer 'major-mode buf1)) ;; candidate buf
+	       (mode2 (symbol-value-in-buffer 'major-mode buf2)) ;; displayed buf
+	       (auxes '(proof-goals-mode proof-shell-mode proof-response-mode))
+	       (mode1aux (memq (get mode1 'derived-mode-parent) auxes))
+	       (mode2aux (memq (get mode2 'derived-mode-parent) auxes)))
+	  (cond
+	   (mode1aux	mode2aux)
+	   (mode2aux	nil)
+	   (t             (select-buffers-tab-buffers-by-mode-old buf1 buf2)))))
+      )) ;; end XEmacs featurep
       
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -677,10 +574,10 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
 ;; Workaround GNU Emacs problems in easymenu-add
 ;;
 
-(if proof-running-on-Emacs21
-     ;; This has a nasty side effect of removing accelerators
-     ;; from existing menus when easy-menu-add is called.
-     ;; Problem confirmed in versions: 21.4.1, OK: 22.1.1
+(if (not (featurep 'xemacs))
+    ;; This has a nasty side effect of removing accelerators
+    ;; from existing menus when easy-menu-add is called.
+    ;; Problem confirmed in versions: 21.4.1, OK: 22.1.1
     (or (< emacs-major-version 22)
 	(setq easy-menu-precalculate-equivalent-keybindings nil)))
 
diff --git a/lib/span-extent.el b/lib/span-extent.el
index 78eb52f5..481933fc 100644
--- a/lib/span-extent.el
+++ b/lib/span-extent.el
@@ -9,29 +9,29 @@
 
 ;; XEmacs-Emacs compatibility: define "spans" in terms of extents.
 
-(defsubst make-span (start end)
+(defsubst span-make (start end)
   "Make a span for the range [START, END) in current buffer."
   (make-extent start end))
 
-(defsubst detach-span (span)
+(defsubst span-detach (span)
   "Remove SPAN from its buffer."
   (detach-extent span))
 
-(defsubst set-span-endpoints (span start end)
+(defsubst span-set-endpoints (span start end)
   "Set the endpoints of SPAN to START, END."
   (set-extent-endpoints span start end))
 
-(defsubst set-span-property (span name value)
+(defsubst span-set-property (span name value)
   "Set SPAN's property NAME to VALUE."
   (set-extent-property span name value))
 
 (defsubst span-read-only (span)
   "Set SPAN to be read only."
-  (set-span-property span 'read-only t))
+  (span-set-property span 'read-only t))
 
 (defsubst span-read-write (span)
   "Set SPAN to be writeable."
-  (set-span-property span 'read-only nil))
+  (span-set-property span 'read-only nil))
 
 (defun span-give-warning (&rest args)
   "Give a warning message."
@@ -40,19 +40,19 @@
 (defun span-write-warning (span)
   "Give a warning message when SPAN is changed."
   ;; FIXME: implement this in XEmacs, perhaps with after-change-functions
-  (set-span-property span 'read-only nil))
+  (span-set-property span 'read-only nil))
 
 (defsubst span-property (span name)
   "Return SPAN's value for property PROPERTY."
   (extent-property span name))
 
-(defsubst delete-span (span)
+(defsubst span-delete (span)
   "Delete SPAN."
   (let ((predelfn (span-property span 'span-delete-action)))
     (and predelfn (funcall predelfn)))
   (delete-extent span))
 
-(defsubst mapcar-spans (fn start end prop &optional val)
+(defsubst span-mapcar-spans (fn start end prop &optional val)
   "Apply function FN to all spans between START and END with property PROP set"
   (mapcar-extents fn nil (current-buffer) start end  nil prop val))
 
diff --git a/lib/span-overlay.el b/lib/span-overlay.el
index 1b4402db..1d246e87 100644
--- a/lib/span-overlay.el
+++ b/lib/span-overlay.el
@@ -11,11 +11,11 @@
 
 (defalias 'span-start 'overlay-start)
 (defalias 'span-end 'overlay-end)
-(defalias 'set-span-property 'overlay-put)
+(defalias 'span-set-property 'overlay-put)
 (defalias 'span-property 'overlay-get)
-(defalias 'make-span 'make-overlay)
-(defalias 'detach-span 'delete-overlay)
-(defalias 'set-span-endpoints 'move-overlay)
+(defalias 'span-make 'make-overlay)
+(defalias 'span-detach 'delete-overlay)
+(defalias 'span-set-endpoints 'move-overlay)
 (defalias 'span-buffer 'overlay-buffer)
 
 (defun span-read-only-hook (overlay after start end &optional len)
@@ -34,14 +34,14 @@
   ;; the buffer.  (Maybe read-only is only a text property, not an
   ;; overlay property?).
   ;; (overlay-put span 'read-only t))
-  (set-span-property span 'modification-hooks '(span-read-only-hook))
-  (set-span-property span 'insert-in-front-hooks '(span-read-only-hook)))
+  (span-set-property span 'modification-hooks '(span-read-only-hook))
+  (span-set-property span 'insert-in-front-hooks '(span-read-only-hook)))
 
 (defun span-read-write (span)
   "Set SPAN to be writeable."
   ;; See comment above for text properties problem.
-  (set-span-property span 'modification-hooks nil)
-  (set-span-property span 'insert-in-front-hooks nil))
+  (span-set-property span 'modification-hooks nil)
+  (span-set-property span 'insert-in-front-hooks nil))
 
 (defun span-give-warning (&rest args)
   "Give a warning message."
@@ -49,8 +49,8 @@
 
 (defun span-write-warning (span)
   "Give a warning message when SPAN is changed."
-  (set-span-property span 'modification-hooks '(span-give-warning))
-  (set-span-property span 'insert-in-front-hooks '(span-give-warning)))
+  (span-set-property span 'modification-hooks '(span-give-warning))
+  (span-set-property span 'insert-in-front-hooks '(span-give-warning)))
 
 ;; We use end first because proof-locked-queue is often changed, and
 ;; its starting point is always 1
@@ -79,14 +79,14 @@ For XEmacs, span-at gives smallest extent at pos.
 For Emacs, we assume that spans don't overlap."
   (car (spans-at-point-prop pt prop)))
 
-(defsubst delete-span (span)
+(defsubst span-delete (span)
   "Delete SPAN."
   (let ((predelfn (span-property span 'span-delete-action)))
     (and predelfn (funcall predelfn)))
   (delete-overlay span))
 
 ;; The next two change ordering of list of spans:
-(defsubst mapcar-spans (fn start end prop &optional val)
+(defsubst span-mapcar-spans (fn start end prop &optional val)
   "Apply function FN to all spans between START and END with property PROP set"
   (mapcar fn (spans-at-region-prop start end prop (or val nil))))
 
@@ -152,7 +152,7 @@ A span is before PT if it begins before the character before PT."
   "Set priority of span to make it appear above other spans.
 FIXME: new hack added nov 99 because of disappearing overlays.
 Behaviour is still worse than before."	;??? --Stef
-  (set-span-property span 'priority 100))
+  (span-set-property span 'priority 100))
 
 (defalias 'span-object 'overlay-buffer)
 
diff --git a/lib/span.el b/lib/span.el
index 8e2c05f4..6fd8371d 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -5,12 +5,10 @@
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
-
-;; FIXME: NAMESPACE!!!!!!!
-
 ;;
 ;; Spans are our abstraction of extents/overlays.
 ;;
+
 (eval-and-compile
   (cond ((string-match "XEmacs" emacs-version)  
 	 (require 'span-extent))
@@ -21,21 +19,21 @@
 ;; Generic functions built on low-level concrete ones.
 ;; 
 
-(defsubst delete-spans (start end prop)
+(defsubst span-delete-spans (start end prop)
   "Delete all spans between START and END with property PROP set."
-  (mapcar-spans 'delete-span start end prop))
+  (span-mapcar-spans 'span-delete start end prop))
 
 (defsubst span-property-safe (span name)
   "Like span-property, but return nil if SPAN is nil."
   (and span (span-property span name)))
   
-(defsubst set-span-start (span value)
+(defsubst span-set-start (span value)
   "Set the start point of SPAN to VALUE."
-  (set-span-endpoints span value (span-end span)))
+  (span-set-endpoints span value (span-end span)))
 
-(defsubst set-span-end (span value)
+(defsubst span-set-end (span value)
   "Set the end point of SPAN to VALUE."
-  (set-span-endpoints span (span-start span) value))
+  (span-set-endpoints span (span-start span) value))
 
 (provide 'span)
 ;; span.el ends here.
diff --git a/phox/phox-font.el b/phox/phox-font.el
index efd44420..37a6a910 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -58,7 +58,7 @@
 ;;                       phox-sym-lock tables
 ;;--------------------------------------------------------------------------;;
 
-(if proof-running-on-XEmacs (require 'phox-sym-lock))
+(if (featurep 'xemacs) (require 'phox-sym-lock))
 
 ;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be
 ;; used to determine the symbol character codes.
diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el
index 9c06d319..f5d94362 100644
--- a/phox/phox-pbrpm.el
+++ b/phox/phox-pbrpm.el
@@ -289,7 +289,7 @@
 (defalias 'proof-pbrpm-right-paren-p 'phox-pbrpm-right-paren-p)
 
 ;;--------------------------------------------------------------------------;;
-(require 'pg-pbrpm)
+;(require 'pg-pbrpm)  da: causes compile error
 (require 'phox-lang)
 (provide 'phox-pbrpm)
 ;; phox-pbrpm ends here
diff --git a/phox/phox-sym-lock.el b/phox/phox-sym-lock.el
index e3ab2db0..e13f56a8 100644
--- a/phox/phox-sym-lock.el
+++ b/phox/phox-sym-lock.el
@@ -1,5 +1,4 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; phox-sym-lock.el - Extension of Font-Lock mode for symbol fontification.
+;; phox-sym-lock.el --- Extension of Font-Lock mode for symbol fontification.
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;        Copyright © 1997-1998 Albert Cohen, all rights reserved.
@@ -29,7 +28,7 @@
 ;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*'
 
 (require 'font-lock)
-(if (string-match "XEmacs" emacs-version) 
+(if (featurep 'xemacs)
     (require 'atomic-extents))  ;; not available on GNU Emacs
 
 (defvar phox-sym-lock-sym-count 0
@@ -169,7 +168,11 @@
 		    (list 'registry "adobe-fontspecific"
 			  'dimension 1
 			  'chars 94
-			  'final 53
+;;			  'final 53
+;; DA PG 3.7: above line doesn't work on XEmacs 21.5b28, gives
+;; Character set already defined for this DIMENSION/CHARS/FINAL/DIRECTION combo (indian-is13194)
+;; DA: Will 55 work?  
+			  'final 55 
 			  'graphic 0))
       (make-charset 'phox-sym-lock-cset-right "Char set for symbol font"
 		    (list 'registry "adobe-fontspecific"
diff --git a/phox/phox-tags.el b/phox/phox-tags.el
index e24e6ce7..c62fe331 100644
--- a/phox/phox-tags.el
+++ b/phox/phox-tags.el
@@ -21,7 +21,7 @@
 (defun phox-tags-add-table(table)
   "add tags table"
   (interactive "D directory, location of a file named TAGS to add : ")
-  (if proof-running-on-XEmacs
+  (if (featurep 'xemacs)
       (let ((association (cons buffer-file-name table)))
 	(if (member association tag-table-alist)
 	    (message "%s already loaded." table)
@@ -39,7 +39,7 @@
   "Set tags-table-list to nil."
   (interactive)
 ;  (make-local-variable 'tags-table-list)
-  (if proof-running-on-XEmacs
+  (if (featurep 'xemacs)
       (progn
 	(setq tag-table-alist (remassoc buffer-file-name tag-table-alist)))
     (setq tags-table-list nil))
@@ -85,7 +85,7 @@
 ;; hook for that.
 ;; 
 (interactive)
-(if proof-running-on-XEmacs
+(if (featurep 'xemacs)
      (tag-complete-symbol)
   (complete-tag)
   )
diff --git a/phox/phox.el b/phox/phox.el
index 2c51e434..6edae61d 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -1,13 +1,13 @@
 ;; $State$ $Date$ $Revision$ 
 
 (require 'proof)			; load generic parts
-(require 'proof-config)
 
-;; Adjust toolbar entries.  (Must be done
-;; before proof-toolbar is loaded).
+;; Adjust toolbar entries.  (Must be done before proof-toolbar is
+;; loaded).
 
-(if proof-running-on-XEmacs (setq phox-toolbar-entries
-      (remassoc 'context phox-toolbar-entries)))
+(eval-after-load "pg-custom"
+  '(setq phox-toolbar-entries
+    (remassoc 'context phox-toolbar-entries)))
 
 
 ;; ======== User settings for PhoX ========
@@ -225,27 +225,10 @@
   (proof-goals-config-done))
 
 
-;; The response buffer and goals buffer modes defined above are
-;; trivial.  In fact, we don't need t²o define them at all -- they
-;; would simply default to "proof-response-mode" and "pg-goals-mode".
-
 ;; A more sophisticated instantiation might set font-lock-keywords to
 ;; add highlighting, or some of the proof by pointing markup
 ;; configuration for the goals buffer.
 
-;; The final piece of magic here is a hook which configures settings
-;; to get the proof shell running.  Proof General needs to know the
-;; name of the program to run, and the modes for the shell, response,
-;; and goals buffers.
-
-(add-hook 'proof-pre-shell-start-hook 'phox-pre-shell-start)
-
-(defun phox-pre-shell-start ()
-  (setq proof-prog-name		phox-prog-name)
-  (setq proof-mode-for-shell    'phox-shell-mode)
-  (setq proof-mode-for-response 'phox-response-mode)
-  (setq proof-mode-for-goals	'phox-goals-mode))
-
 ; completions
 ; dans completions.el
 ;(setq completion-min-length 6)
diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el
index 038b6112..7acd776f 100644
--- a/phox/x-symbol-phox.el
+++ b/phox/x-symbol-phox.el
@@ -11,6 +11,8 @@
 ;; NB: Part of Proof General distribution.
 ;;
 
+(require 'proof-utils)
+
 (defvar x-symbol-phox-required-fonts nil)
 
 ;;;===========================================================================
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 800ac869..6ae4b35e 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -17,6 +17,7 @@
 
 
 (require 'proof)
+(require 'span)
 (require 'plastic-syntax)
 
 
@@ -36,9 +37,10 @@
   :type 'string
   :group 'plastic)
 
+(eval-and-compile
 (defvar plastic-lit-string 
   ">" 
-  "*Prefix of literate lines. Set to empty string to get non-literate mode")
+  "*Prefix of literate lines. Set to empty string to get non-literate mode"))
 
 (defcustom plastic-help-menu-list
   '(["The PLASTIC Reference Card" (browse-url plastic-www-refcard) t]
@@ -292,14 +294,15 @@ Given is the first SPAN which needs to be undone."
 ;;   Commands specific to plastic                                      ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; da: FIXME added quoting/eval here because of macros.  Probably better
-;; to turn proof-defshortcut and co into functions.
-`(proof-defshortcut plastic-Intros 
-		   ,(concat plastic-lit-string "Intros ")  ?i)
-`(proof-defshortcut plastic-Refine
-		   ,(concat plastic-lit-string "Refine ")  ?r)
-`(proof-defshortcut plastic-ReturnAll
-		   ,(concat plastic-lit-string "ReturnAll ") ?u)
+(eval-after-load "plastic" ;; da: so that plastic-lit-string can be changed
+  '(progn
+     (eval `(proof-defshortcut plastic-Intros 
+			       ,(concat plastic-lit-string "Intros ")  ?i))
+     (eval `(proof-defshortcut plastic-Refine
+			       ,(concat plastic-lit-string "Refine ")  ?r))
+     (eval `(proof-defshortcut plastic-ReturnAll
+			       ,(concat plastic-lit-string "ReturnAll ") ?u))))
+
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -335,15 +338,6 @@ Given is the first SPAN which needs to be undone."
 	     (insert (format plastic-pretty-set-width (- current-width 1)))
 	     )))))
 
-(defun plastic-pre-shell-start ()
-  (setq proof-prog-name (concat plastic-prog-name "")
-        ;; set cmd-line flag 
-        proof-mode-for-shell    'plastic-shell-mode
-        proof-mode-for-response 'plastic-response-mode
-        proof-mode-for-goals    'plastic-goals-mode)
-
-  (setenv "PROOF_GENERAL" "")		;; signal to plastic, use annotations
-  )
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -351,16 +345,15 @@ Given is the first SPAN which needs to be undone."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun plastic-mode-config ()
-  ;; da: this is now a user-option, please set it in your .emacs
-  ;; via customize mechanism.
-  ;; (setq proof-electric-terminator-enable t)	;; force semicolons active.
 
   (setq proof-terminal-char ?\;)
   (setq proof-script-comment-start "(*")			;; these still active
   (setq proof-script-comment-end "*)")
 
+  (setq proof-prog-name (concat plastic-prog-name ""))
+  (setenv "PROOF_GENERAL" "") ;; signal to plastic, use annotations
+
   (setq proof-assistant-home-page plastic-www-home-page)
-  (setq proof-mode-for-script 'plastic-mode)
 
   (setq proof-showproof-command (concat plastic-lit-string " &S PrfCtxt")
 	proof-goal-command      (concat plastic-lit-string " Claim %s;")
@@ -400,12 +393,6 @@ Given is the first SPAN which needs to be undone."
 
   (setq font-lock-keywords plastic-font-lock-keywords-1)
 
-;; FIXME da: this is done generically now.  If you want
-;; the zap commas behaviour, set proof-font-lock-zap-commas=t here.
-;;  (and (boundp 'font-lock-always-fontify-immediately)
-;;       (setq font-lock-always-fontify-immediately t))
-
-
   (proof-config-done)
 
 ;; outline
@@ -431,7 +418,6 @@ Given is the first SPAN which needs to be undone."
 
 ;; hooks and callbacks
 
-  (add-hook 'proof-pre-shell-start-hook    'plastic-pre-shell-start nil t)
   (add-hook 'proof-shell-insert-hook       'plastic-shell-adjust-line-width)
   (add-hook 'proof-shell-handle-error-or-interrupt-hook 'plastic-had-error)
   (add-hook 'proof-shell-insert-hook       'plastic-preprocessing)