Add additional support for pgipfloat type

6 files changed, 1922 insertions, 1860 deletions

diff --git a/TAGS b/TAGS
index 134e6da3..ac9c4026 100644
--- a/TAGS
+++ b/TAGS
@@ -38,159 +38,191 @@ coq/coq-db.el,678
 (defconst coq-solve-tactics-face 266,9562
 (defconst coq-cheat-face 270,9726
 
-coq/coq.el,5959
-(defcustom coq-translate-to-v8 48,1381
-(defun coq-build-prog-args 54,1561
-(defcustom coq-compile-file-command 64,1857
-(defcustom coq-use-makefile 72,2176
-(defcustom coq-default-undo-limit 80,2399
-(defconst coq-shell-init-cmd85,2527
-(defcustom coq-prog-env 91,2654
-(defconst coq-shell-restart-cmd 99,2904
-(defvar coq-shell-prompt-pattern101,2958
-(defvar coq-shell-cd 109,3261
-(defvar coq-shell-proof-completed-regexp 113,3421
-(defvar coq-goal-regexp116,3576
-(defun coq-library-directory 121,3672
-(defcustom coq-tags 127,3850
-(defconst coq-interrupt-regexp 132,4000
-(defcustom coq-www-home-page 135,4093
-(defvar coq-outline-regexp146,4268
-(defvar coq-outline-heading-end-regexp 153,4480
-(defvar coq-shell-outline-regexp 155,4534
-(defvar coq-shell-outline-heading-end-regexp 156,4584
-(defconst coq-state-preserving-tactics-regexp159,4648
-(defconst coq-state-changing-commands-regexp161,4750
-(defconst coq-state-preserving-commands-regexp163,4859
-(defconst coq-commands-regexp165,4972
-(defvar coq-retractable-instruct-regexp167,5051
-(defvar coq-non-retractable-instruct-regexp169,5143
-(defun coq-set-undo-limit 204,5830
-(defun build-list-id-from-string 208,5960
-(defun coq-last-prompt-info 220,6458
-(defun coq-last-prompt-info-safe 232,6990
-(defvar coq-last-but-one-statenum 238,7247
-(defvar coq-last-but-one-proofnum 245,7545
-(defvar coq-last-but-one-proofstack 248,7643
-(defsubst coq-get-span-statenum 251,7753
-(defsubst coq-get-span-proofnum 255,7868
-(defsubst coq-get-span-proofstack 259,7983
-(defsubst coq-set-span-statenum 263,8127
-(defsubst coq-get-span-goalcmd 267,8258
-(defsubst coq-set-span-goalcmd 271,8372
-(defsubst coq-set-span-proofnum 275,8502
-(defsubst coq-set-span-proofstack 279,8633
-(defsubst proof-last-locked-span 283,8793
-(defun proof-clone-buffer 287,8927
-(defun proof-store-buffer-win 301,9462
-(defun proof-store-response-win 312,9955
-(defun proof-store-goals-win 316,10082
-(defun coq-set-state-infos 328,10614
-(defun count-not-intersection 366,12701
-(defun coq-find-and-forget 396,13950
-(defvar coq-current-goal 420,15044
-(defun coq-goal-hyp 423,15109
-(defun coq-state-preserving-p 436,15541
-(defconst notation-print-kinds-table450,15855
-(defun coq-PrintScope 454,16022
-(defun coq-guess-or-ask-for-string 472,16571
-(defun coq-ask-do 486,17139
-(defsubst coq-put-into-brackets 495,17524
-(defsubst coq-put-into-quotes 498,17585
-(defun coq-SearchIsos 501,17645
-(defun coq-SearchConstant 509,17886
-(defun coq-Searchregexp 513,17979
-(defun coq-SearchRewrite 519,18122
-(defun coq-SearchAbout 523,18219
-(defun coq-Print 529,18364
-(defun coq-About 534,18489
-(defun coq-LocateConstant 539,18609
-(defun coq-LocateLibrary 544,18712
-(defun coq-LocateNotation 549,18829
-(defun coq-Pwd 557,19061
-(defun coq-Inspect 562,19185
-(defun coq-PrintSection(566,19285
-(defun coq-Print-implicit 570,19378
-(defun coq-Check 575,19529
-(defun coq-Show 580,19637
-(defun coq-Compile 594,20080
-(defun coq-guess-command-line 606,20398
-(defpacustom use-editing-holes 643,21951
-(defun coq-mode-config 652,22254
-(defun coq-shell-mode-config 745,25597
-(defun coq-goals-mode-config 788,27387
-(defun coq-response-config 795,27631
-(defpacustom print-fully-explicit 820,28456
-(defpacustom print-implicit 825,28604
-(defpacustom print-coercions 830,28770
-(defpacustom print-match-wildcards 835,28914
-(defpacustom print-elim-types 840,29094
-(defpacustom printing-depth 845,29260
-(defpacustom undo-depth 850,29421
-(defpacustom time-commands 855,29587
-(defpacustom auto-compile-vos 859,29697
-(defun coq-maybe-compile-buffer 888,30811
-(defun coq-ancestors-of 924,32339
-(defun coq-all-ancestors-of 947,33303
-(defun coq-process-require-command 958,33650
-(defun coq-included-children 963,33777
-(defun coq-process-file 984,34616
-(defun coq-preprocessing 999,35145
-(defun coq-fake-constant-markup 1013,35600
-(defun coq-create-span-menu 1029,36205
-(defconst module-kinds-table1047,36718
-(defconst modtype-kinds-table1051,36867
-(defun coq-insert-section-or-module 1055,36996
-(defconst reqkinds-kinds-table1076,37846
-(defun coq-insert-requires 1080,37990
-(defun coq-end-Section 1093,38470
-(defun coq-insert-intros 1111,39048
-(defun coq-insert-infoH-hook 1123,39581
-(defun coq-insert-as 1128,39789
-(defun coq-insert-match 1145,40482
-(defun coq-insert-solve-tactic 1174,41652
-(defun coq-insert-tactic 1180,41903
-(defun coq-insert-tactical 1186,42105
-(defun coq-insert-command 1192,42336
-(defun coq-insert-term 1197,42501
-(define-key coq-keymap 1202,42662
-(define-key coq-keymap 1203,42720
-(define-key coq-keymap 1204,42777
-(define-key coq-keymap 1205,42846
-(define-key coq-keymap 1206,42902
-(define-key coq-keymap 1207,42951
-(define-key coq-keymap 1208,43009
-(define-key coq-keymap 1209,43069
-(define-key coq-keymap 1210,43134
-(define-key coq-keymap 1213,43262
-(define-key coq-keymap 1215,43336
-(define-key coq-keymap 1216,43393
-(define-key coq-keymap 1220,43518
-(define-key coq-keymap 1222,43574
-(define-key coq-keymap 1223,43624
-(define-key coq-keymap 1224,43674
-(define-key coq-keymap 1225,43730
-(define-key coq-keymap 1226,43780
-(define-key coq-keymap 1227,43834
-(define-key coq-keymap 1228,43893
-(define-key coq-goals-mode-map 1231,43954
-(define-key coq-goals-mode-map 1232,44036
-(define-key coq-goals-mode-map 1233,44118
-(define-key coq-goals-mode-map 1234,44205
-(define-key coq-goals-mode-map 1235,44287
-(defvar last-coq-error-location 1244,44589
-(defun coq-get-last-error-location 1252,44973
-(defun coq-highlight-error 1302,47530
-(defun coq-highlight-error-hook 1330,48611
-(defun first-word-of-buffer 1340,48828
-(defun coq-show-first-goal 1348,49031
-(defvar coq-modeline-string2 1365,49726
-(defvar coq-modeline-string1 1366,49760
-(defvar coq-modeline-string0 1367,49794
-(defun coq-build-subgoals-string 1368,49835
-(defun coq-update-minor-mode-alist 1373,50001
-(defun is-not-split-vertic 1405,51395
-(defun optim-resp-windows 1414,51835
+coq/coq.el,7421
+(defcustom coq-translate-to-v8 56,1700
+(defun coq-build-prog-args 62,1880
+(defcustom coq-compiler72,2174
+(defcustom coq-dependency-analyzer78,2311
+(defcustom coq-compile-file-command 84,2451
+(defcustom coq-use-makefile 92,2788
+(defcustom coq-default-undo-limit 100,3011
+(defconst coq-shell-init-cmd105,3139
+(defcustom coq-prog-env 113,3404
+(defconst coq-shell-restart-cmd 121,3654
+(defvar coq-shell-prompt-pattern123,3708
+(defvar coq-shell-cd 131,4011
+(defvar coq-shell-proof-completed-regexp 135,4171
+(defvar coq-goal-regexp138,4326
+(defun get-coq-library-directory 143,4422
+(defconst coq-library-directory 149,4604
+(defcustom coq-tags 152,4730
+(defconst coq-interrupt-regexp 157,4878
+(defcustom coq-www-home-page 160,4971
+(defvar coq-outline-regexp171,5146
+(defvar coq-outline-heading-end-regexp 178,5358
+(defvar coq-shell-outline-regexp 180,5412
+(defvar coq-shell-outline-heading-end-regexp 181,5462
+(defconst coq-state-preserving-tactics-regexp184,5526
+(defconst coq-state-changing-commands-regexp186,5628
+(defconst coq-state-preserving-commands-regexp188,5737
+(defconst coq-commands-regexp190,5850
+(defvar coq-retractable-instruct-regexp192,5929
+(defvar coq-non-retractable-instruct-regexp194,6021
+(defcustom coq-use-smie 226,6717
+(defconst coq-smie-grammar234,6945
+(defun coq-smie-rules 272,8766
+(defun coq-set-undo-limit 295,9497
+(defun build-list-id-from-string 299,9627
+(defun coq-last-prompt-info 311,10125
+(defun coq-last-prompt-info-safe 323,10657
+(defvar coq-last-but-one-statenum 329,10914
+(defvar coq-last-but-one-proofnum 336,11212
+(defvar coq-last-but-one-proofstack 339,11310
+(defsubst coq-get-span-statenum 342,11420
+(defsubst coq-get-span-proofnum 346,11535
+(defsubst coq-get-span-proofstack 350,11650
+(defsubst coq-set-span-statenum 354,11794
+(defsubst coq-get-span-goalcmd 358,11925
+(defsubst coq-set-span-goalcmd 362,12039
+(defsubst coq-set-span-proofnum 366,12169
+(defsubst coq-set-span-proofstack 370,12300
+(defsubst proof-last-locked-span 374,12460
+(defun proof-clone-buffer 378,12594
+(defun proof-store-buffer-win 392,13129
+(defun proof-store-response-win 403,13622
+(defun proof-store-goals-win 407,13749
+(defun coq-set-state-infos 419,14281
+(defun count-not-intersection 457,16368
+(defun coq-find-and-forget 487,17620
+(defvar coq-current-goal 511,18714
+(defun coq-goal-hyp 514,18779
+(defun coq-state-preserving-p 527,19253
+(defconst notation-print-kinds-table541,19567
+(defun coq-PrintScope 545,19734
+(defun coq-guess-or-ask-for-string 563,20283
+(defun coq-ask-do 577,20823
+(defsubst coq-put-into-brackets 586,21208
+(defsubst coq-put-into-quotes 589,21269
+(defun coq-SearchIsos 592,21329
+(defun coq-SearchConstant 600,21570
+(defun coq-Searchregexp 604,21663
+(defun coq-SearchRewrite 610,21806
+(defun coq-SearchAbout 614,21903
+(defun coq-Print 620,22048
+(defun coq-About 625,22173
+(defun coq-LocateConstant 630,22293
+(defun coq-LocateLibrary 635,22396
+(defun coq-LocateNotation 640,22513
+(defun coq-Pwd 648,22745
+(defun coq-Inspect 653,22869
+(defun coq-PrintSection(657,22969
+(defun coq-Print-implicit 661,23062
+(defun coq-Check 666,23213
+(defun coq-Show 671,23321
+(defun coq-Compile 685,23764
+(defun coq-guess-command-line 697,24082
+(defpacustom use-editing-holes 734,25635
+(defun coq-mode-config 743,25938
+(defun coq-shell-mode-config 839,29424
+(defun coq-goals-mode-config 884,31252
+(defun coq-response-config 891,31496
+(defpacustom print-fully-explicit 916,32321
+(defpacustom print-implicit 921,32469
+(defpacustom print-coercions 926,32635
+(defpacustom print-match-wildcards 931,32779
+(defpacustom print-elim-types 936,32959
+(defpacustom printing-depth 941,33125
+(defpacustom undo-depth 946,33286
+(defpacustom time-commands 951,33452
+(defpacustom auto-compile-vos 955,33562
+(defun coq-maybe-compile-buffer 984,34676
+(defun coq-ancestors-of 1020,36204
+(defun coq-all-ancestors-of 1043,37168
+(defun coq-process-require-command 1054,37515
+(defun coq-included-children 1059,37642
+(defun coq-process-file 1080,38481
+(defgroup coq-auto-recompile 1096,38971
+(defcustom coq-recompile-before-require 1101,39126
+(defcustom coq-recompile-command 1109,39515
+(defconst coq-recompile-substitution-list1129,40467
+(defcustom coq-recompile-auto-save 1144,41224
+(defcustom coq-recompile-ignore-library-directory 1162,41952
+(defcustom coq-recompile-ignored-directories 1169,42229
+(defcustom coq-load-path 1180,42825
+(defcustom coq-load-path-include-current 1189,43227
+(defconst coq-require-command-regexp1197,43529
+(defconst coq-require-id-regexp1204,43886
+(defvar coq-internal-load-path 1212,44320
+(defun time-less-or-equal 1221,44647
+(defun get-coq-load-path 1234,45094
+(defun coq-recompile-ignore-file 1276,47004
+(defun coq-library-src-of-obj-file 1296,47793
+(defun coq-get-library-dependencies 1301,48025
+(defun coq-recompile-library 1321,49019
+(defun coq-recompile-library-if-necessary 1343,49954
+(defun coq-make-lib-up-to-date 1360,50709
+(defun coq-auto-recompile-externally 1378,51690
+(defun coq-split-module-id 1402,52921
+(defun coq-check-module 1411,53296
+(defun coq-recompile-save-buffer-filter 1442,54799
+(defun coq-recompile-save-some-buffers 1452,55217
+(defun coq-preprocess-require-commands 1474,56137
+(defun coq-preprocessing 1507,57456
+(defun coq-fake-constant-markup 1521,57911
+(defun coq-create-span-menu 1537,58516
+(defconst module-kinds-table1555,59029
+(defconst modtype-kinds-table1559,59178
+(defun coq-insert-section-or-module 1563,59307
+(defconst reqkinds-kinds-table1584,60157
+(defun coq-insert-requires 1588,60301
+(defun coq-end-Section 1601,60781
+(defun coq-insert-intros 1619,61359
+(defun coq-insert-infoH-hook 1631,61892
+(defun coq-insert-as 1636,62100
+(defun coq-insert-match 1653,62793
+(defun coq-insert-solve-tactic 1682,63963
+(defun coq-insert-tactic 1688,64214
+(defun coq-insert-tactical 1694,64416
+(defun coq-insert-command 1700,64647
+(defun coq-insert-term 1705,64812
+(define-key coq-keymap 1710,64973
+(define-key coq-keymap 1711,65031
+(define-key coq-keymap 1712,65088
+(define-key coq-keymap 1713,65157
+(define-key coq-keymap 1714,65213
+(define-key coq-keymap 1715,65262
+(define-key coq-keymap 1716,65320
+(define-key coq-keymap 1717,65380
+(define-key coq-keymap 1718,65445
+(define-key coq-keymap 1721,65573
+(define-key coq-keymap 1723,65647
+(define-key coq-keymap 1724,65704
+(define-key coq-keymap 1728,65829
+(define-key coq-keymap 1730,65885
+(define-key coq-keymap 1731,65935
+(define-key coq-keymap 1732,65985
+(define-key coq-keymap 1733,66041
+(define-key coq-keymap 1734,66091
+(define-key coq-keymap 1735,66145
+(define-key coq-keymap 1736,66204
+(define-key coq-goals-mode-map 1739,66265
+(define-key coq-goals-mode-map 1740,66347
+(define-key coq-goals-mode-map 1741,66429
+(define-key coq-goals-mode-map 1742,66516
+(define-key coq-goals-mode-map 1743,66598
+(defvar last-coq-error-location 1752,66900
+(defun coq-get-last-error-location 1760,67284
+(defun coq-highlight-error 1810,69847
+(defun coq-highlight-error-hook 1838,70928
+(defun first-word-of-buffer 1848,71145
+(defun coq-show-first-goal 1856,71348
+(defvar coq-modeline-string2 1873,72043
+(defvar coq-modeline-string1 1874,72077
+(defvar coq-modeline-string0 1875,72111
+(defun coq-build-subgoals-string 1876,72152
+(defun coq-update-minor-mode-alist 1881,72318
+(defun is-not-split-vertic 1913,73712
+(defun optim-resp-windows 1922,74152
 
 coq/coq-indent.el,2515
 (defconst coq-any-command-regexp20,368
@@ -262,77 +294,76 @@ coq/coq-local-vars.el,280
 (defun coq-ask-prog-name 150,6153
 (defun coq-ask-insert-coq-prog-name 167,6864
 
-coq/coq-syntax.el,2818
-(defcustom coq-prog-name 18,559
-(defcustom coq-user-tactics-db 38,1341
-(defcustom coq-user-commands-db 55,1854
-(defcustom coq-user-tacticals-db 71,2373
-(defcustom coq-user-solve-tactics-db 87,2894
-(defcustom coq-user-cheat-tactics-db 103,3413
-(defcustom coq-user-reserved-db 122,3959
-(defvar coq-tactics-db140,4490
-(defvar coq-solve-tactics-db298,12749
-(defvar coq-solve-cheat-tactics-db321,13594
-(defvar coq-tacticals-db333,13769
-(defvar coq-decl-db357,14655
-(defvar coq-defn-db382,16111
-(defvar coq-goal-starters-db440,20466
-(defvar coq-other-commands-db469,22223
-(defvar coq-commands-db598,31689
-(defvar coq-terms-db605,31909
-(defun coq-count-match 667,34524
-(defun coq-module-opening-p 683,35253
-(defun coq-section-command-p 694,35664
-(defun coq-goal-command-str-p 698,35761
-(defun coq-goal-command-p 725,36863
-(defvar coq-keywords-save-strict734,37146
-(defvar coq-keywords-save743,37259
-(defun coq-save-command-p 747,37337
-(defvar coq-keywords-kill-goal758,37665
-(defvar coq-keywords-state-changing-misc-commands762,37755
-(defvar coq-keywords-goal765,37880
-(defvar coq-keywords-decl768,37963
-(defvar coq-keywords-defn771,38037
-(defvar coq-keywords-state-changing-commands775,38112
-(defvar coq-keywords-state-preserving-commands784,38372
-(defvar coq-keywords-commands789,38588
-(defvar coq-solve-tactics794,38736
-(defvar coq-solve-tactics-regexp798,38857
-(defvar coq-solve-cheat-tactics802,38991
-(defvar coq-solve-cheat-tactics-regexp806,39136
-(defvar coq-tacticals810,39294
-(defvar coq-reserved816,39433
-(defvar coq-reserved-regexp 826,39760
-(defvar coq-state-changing-tactics828,39825
-(defvar coq-state-preserving-tactics831,39934
-(defvar coq-tactics835,40048
-(defvar coq-tactics-regexp 838,40137
-(defvar coq-retractable-instruct841,40292
-(defvar coq-non-retractable-instruct844,40402
-(defvar coq-keywords848,40530
-(defun proof-regexp-alt-list-symb 854,40754
-(defvar coq-keywords-regexp 857,40859
-(defvar coq-symbols860,40927
-(defvar coq-error-regexp 879,41140
-(defvar coq-id 882,41368
-(defvar coq-id-shy 883,41393
-(defvar coq-ids 886,41495
-(defun coq-first-abstr-regexp 888,41561
-(defcustom coq-variable-highlight-enable 891,41656
-(defvar coq-font-lock-terms897,41783
-(defconst coq-save-command-regexp-strict919,42866
-(defconst coq-save-command-regexp925,43036
-(defconst coq-save-with-hole-regexp930,43191
-(defconst coq-goal-command-regexp934,43351
-(defconst coq-goal-with-hole-regexp937,43453
-(defconst coq-decl-with-hole-regexp941,43587
-(defconst coq-defn-with-hole-regexp948,43837
-(defconst coq-with-with-hole-regexp958,44127
-(defconst coq-require-command-regexp965,44420
-(defvar coq-font-lock-keywords-1973,44645
-(defvar coq-font-lock-keywords 1001,45980
-(defun coq-init-syntax-table 1003,46038
-(defconst coq-generic-expression1028,46765
+coq/coq-syntax.el,2771
+(defcustom coq-prog-name 18,558
+(defcustom coq-user-tactics-db 38,1340
+(defcustom coq-user-commands-db 55,1853
+(defcustom coq-user-tacticals-db 71,2372
+(defcustom coq-user-solve-tactics-db 87,2893
+(defcustom coq-user-cheat-tactics-db 103,3412
+(defcustom coq-user-reserved-db 122,3958
+(defvar coq-tactics-db140,4489
+(defvar coq-solve-tactics-db298,12748
+(defvar coq-solve-cheat-tactics-db321,13593
+(defvar coq-tacticals-db333,13768
+(defvar coq-decl-db357,14654
+(defvar coq-defn-db382,16110
+(defvar coq-goal-starters-db440,20465
+(defvar coq-other-commands-db469,22222
+(defvar coq-commands-db598,31688
+(defvar coq-terms-db605,31908
+(defun coq-count-match 667,34523
+(defun coq-module-opening-p 683,35252
+(defun coq-section-command-p 694,35663
+(defun coq-goal-command-str-p 698,35760
+(defun coq-goal-command-p 725,36862
+(defvar coq-keywords-save-strict734,37145
+(defvar coq-keywords-save743,37258
+(defun coq-save-command-p 747,37336
+(defvar coq-keywords-kill-goal758,37664
+(defvar coq-keywords-state-changing-misc-commands762,37754
+(defvar coq-keywords-goal765,37879
+(defvar coq-keywords-decl768,37962
+(defvar coq-keywords-defn771,38036
+(defvar coq-keywords-state-changing-commands775,38111
+(defvar coq-keywords-state-preserving-commands784,38371
+(defvar coq-keywords-commands789,38587
+(defvar coq-solve-tactics794,38735
+(defvar coq-solve-tactics-regexp798,38856
+(defvar coq-solve-cheat-tactics802,38990
+(defvar coq-solve-cheat-tactics-regexp806,39135
+(defvar coq-tacticals810,39293
+(defvar coq-reserved816,39432
+(defvar coq-reserved-regexp 826,39759
+(defvar coq-state-changing-tactics828,39824
+(defvar coq-state-preserving-tactics831,39933
+(defvar coq-tactics835,40047
+(defvar coq-tactics-regexp 838,40136
+(defvar coq-retractable-instruct841,40291
+(defvar coq-non-retractable-instruct844,40401
+(defvar coq-keywords848,40529
+(defun proof-regexp-alt-list-symb 854,40753
+(defvar coq-keywords-regexp 857,40858
+(defvar coq-symbols860,40926
+(defvar coq-error-regexp 879,41139
+(defvar coq-id 882,41367
+(defvar coq-id-shy 883,41392
+(defvar coq-ids 886,41494
+(defun coq-first-abstr-regexp 888,41560
+(defcustom coq-variable-highlight-enable 891,41655
+(defvar coq-font-lock-terms897,41782
+(defconst coq-save-command-regexp-strict919,42865
+(defconst coq-save-command-regexp925,43035
+(defconst coq-save-with-hole-regexp930,43190
+(defconst coq-goal-command-regexp934,43350
+(defconst coq-goal-with-hole-regexp937,43452
+(defconst coq-decl-with-hole-regexp941,43586
+(defconst coq-defn-with-hole-regexp948,43836
+(defconst coq-with-with-hole-regexp958,44126
+(defvar coq-font-lock-keywords-1973,44656
+(defvar coq-font-lock-keywords 1001,45991
+(defun coq-init-syntax-table 1003,46049
+(defconst coq-generic-expression1028,46776
 
 coq/coq-unicode-tokens.el,454
 (defconst coq-token-format 39,1427
@@ -354,79 +385,79 @@ hol98/hol98.el,121
 (defvar hol98-tacticals 20,499
 
 isar/isabelle-system.el,1254
-(defgroup isabelle 28,798
-(defcustom isabelle-web-page32,926
-(defcustom isa-isabelle-command41,1143
-(defvar isabelle-not-found 59,1825
-(defun isa-set-isabelle-command 62,1940
-(defun isa-shell-command-to-string 85,2958
-(defun isa-getenv 91,3182
-(defcustom isabelle-program-name-override 111,3881
-(defun isa-tool-list-logics 122,4227
-(defcustom isabelle-logics-available 129,4473
-(defcustom isabelle-chosen-logic 139,4810
-(defvar isabelle-chosen-logic-prev 155,5394
-(defun isabelle-hack-local-variables-function 158,5514
-(defun isabelle-set-prog-name 170,5953
-(defun isabelle-choose-logic 194,7073
-(defun isa-view-doc 213,7835
-(defun isa-tool-list-docs 220,8061
-(defconst isabelle-verbatim-regexp 238,8791
-(defun isabelle-verbatim 241,8933
-(defcustom isabelle-refresh-logics 248,9094
-(defvar isabelle-docs-menu256,9422
-(defvar isabelle-logics-menu-entries 263,9707
-(defun isabelle-logics-menu-calculate 266,9780
-(defvar isabelle-time-to-refresh-logics 287,10422
-(defun isabelle-logics-menu-refresh 291,10517
-(defun isabelle-menu-bar-update-logics 306,11150
-(defun isabelle-load-isar-keywords 322,11779
-(defun isabelle-create-span-menu 343,12507
-(defun isabelle-xml-sml-escapes 359,12938
-(defun isabelle-process-pgip 362,13039
+(defgroup isabelle 28,797
+(defcustom isabelle-web-page32,925
+(defcustom isa-isabelle-command41,1142
+(defvar isabelle-not-found 59,1824
+(defun isa-set-isabelle-command 62,1939
+(defun isa-shell-command-to-string 85,2957
+(defun isa-getenv 91,3181
+(defcustom isabelle-program-name-override 111,3880
+(defun isa-tool-list-logics 122,4226
+(defcustom isabelle-logics-available 129,4472
+(defcustom isabelle-chosen-logic 139,4809
+(defvar isabelle-chosen-logic-prev 155,5393
+(defun isabelle-hack-local-variables-function 158,5513
+(defun isabelle-set-prog-name 170,5952
+(defun isabelle-choose-logic 194,7072
+(defun isa-view-doc 213,7834
+(defun isa-tool-list-docs 220,8060
+(defconst isabelle-verbatim-regexp 238,8790
+(defun isabelle-verbatim 241,8932
+(defcustom isabelle-refresh-logics 248,9093
+(defvar isabelle-docs-menu256,9421
+(defvar isabelle-logics-menu-entries 263,9706
+(defun isabelle-logics-menu-calculate 266,9779
+(defvar isabelle-time-to-refresh-logics 287,10421
+(defun isabelle-logics-menu-refresh 291,10516
+(defun isabelle-menu-bar-update-logics 306,11149
+(defun isabelle-load-isar-keywords 322,11778
+(defun isabelle-create-span-menu 343,12506
+(defun isabelle-xml-sml-escapes 359,12937
+(defun isabelle-process-pgip 362,13038
 
 isar/isar-autotest.el,31
-(defvar isar-long-tests 8,187
+(defvar isar-long-tests 8,186
 
 isar/isar.el,1595
-(defcustom isar-keywords-name 39,916
-(defpgdefault completion-table 55,1427
-(defcustom isar-web-page57,1480
-(defun isar-strip-terminators 71,1830
-(defun isar-markup-ml 83,2186
-(defun isar-mode-config-set-variables 88,2321
-(defun isar-shell-mode-config-set-variables 153,5120
-(defun isar-set-proof-find-theorems-command 235,8306
-(defpacustom use-find-theorems-form 241,8490
-(defun isar-set-undo-commands 246,8656
-(defpacustom use-linear-undo 260,9248
-(defun isar-configure-from-settings 265,9406
-(defun isar-remove-file 273,9550
-(defun isar-shell-compute-new-files-list 285,9854
-(define-derived-mode isar-shell-mode 304,10424
-(define-derived-mode isar-response-mode 309,10551
-(define-derived-mode isar-goals-mode 314,10684
-(define-derived-mode isar-mode 319,10810
-(defpgdefault menu-entries371,12525
-(defun isar-set-command 402,13719
-(defpgdefault help-menu-entries 407,13849
-(defun isar-count-undos 410,13925
-(defun isar-find-and-forget 436,14891
-(defun isar-goal-command-p 472,16234
-(defun isar-global-save-command-p 477,16411
-(defvar isar-current-goal 498,17195
-(defun isar-state-preserving-p 501,17261
-(defvar isar-shell-current-line-width 526,18110
-(defun isar-shell-adjust-line-width 531,18302
-(defsubst isar-string-wrapping 554,19067
-(defsubst isar-positions-of 563,19261
-(defcustom isar-wrap-commands-singly 569,19466
-(defun isar-command-wrapping 575,19662
-(defun isar-preprocessing 583,19976
-(defun isar-mode-config 601,20527
-(defun isar-shell-mode-config 615,21180
-(defun isar-response-mode-config 625,21529
-(defun isar-goals-mode-config 635,21864
+(defcustom isar-keywords-name 39,915
+(defpgdefault completion-table 55,1426
+(defcustom isar-web-page57,1479
+(defun isar-strip-terminators 71,1829
+(defun isar-markup-ml 83,2185
+(defun isar-mode-config-set-variables 88,2320
+(defun isar-shell-mode-config-set-variables 153,5119
+(defun isar-set-proof-find-theorems-command 235,8305
+(defpacustom use-find-theorems-form 241,8489
+(defun isar-set-undo-commands 246,8655
+(defpacustom use-linear-undo 261,9288
+(defun isar-configure-from-settings 266,9446
+(defun isar-remove-file 274,9596
+(defun isar-shell-compute-new-files-list 286,9900
+(define-derived-mode isar-shell-mode 305,10470
+(define-derived-mode isar-response-mode 310,10597
+(define-derived-mode isar-goals-mode 315,10730
+(define-derived-mode isar-mode 320,10856
+(defpgdefault menu-entries372,12571
+(defun isar-set-command 403,13765
+(defpgdefault help-menu-entries 408,13895
+(defun isar-count-undos 411,13971
+(defun isar-find-and-forget 437,14937
+(defun isar-goal-command-p 473,16280
+(defun isar-global-save-command-p 478,16457
+(defvar isar-current-goal 499,17241
+(defun isar-state-preserving-p 502,17307
+(defvar isar-shell-current-line-width 527,18156
+(defun isar-shell-adjust-line-width 532,18348
+(defsubst isar-string-wrapping 555,19113
+(defsubst isar-positions-of 564,19307
+(defcustom isar-wrap-commands-singly 570,19512
+(defun isar-command-wrapping 576,19708
+(defun isar-preprocessing 584,20022
+(defun isar-mode-config 602,20573
+(defun isar-shell-mode-config 616,21226
+(defun isar-response-mode-config 626,21575
+(defun isar-goals-mode-config 636,21910
 
 isar/isar-find-theorems.el,779
 (defvar isar-find-theorems-data 19,565
@@ -477,101 +508,101 @@ isar/isar-mmm.el,81
 (defconst isar-start-sml-regexp36,1172
 
 isar/isar-syntax.el,3975
-(defconst isar-script-syntax-table-entries18,484
-(defconst isar-script-syntax-table-alist42,886
-(defun isar-init-syntax-table 51,1169
-(defun isar-init-output-syntax-table 59,1416
-(defconst isar-keyword-begin 74,1858
-(defconst isar-keyword-end 75,1896
-(defconst isar-keywords-theory-enclose77,1931
-(defconst isar-keywords-theory82,2069
-(defconst isar-keywords-save87,2200
-(defconst isar-keywords-proof-enclose92,2315
-(defconst isar-keywords-proof98,2476
-(defconst isar-keywords-proof-context105,2653
-(defconst isar-keywords-local-goal109,2760
-(defconst isar-keywords-proper113,2865
-(defconst isar-keywords-improper118,2984
-(defconst isar-keyword-level-alist123,3116
-(defconst isar-keywords-outline 138,3587
-(defconst isar-keywords-indent-open141,3663
-(defconst isar-keywords-indent-close147,3826
-(defconst isar-keywords-indent-enclose151,3924
-(defconst isar-ext-first 160,4118
-(defconst isar-ext-rest 161,4185
-(defconst isar-long-id-stuff 163,4257
-(defconst isar-id 164,4331
-(defconst isar-idx 165,4401
-(defconst isar-string 167,4460
-(defun isar-ids-to-regexp 169,4520
-(defconst isar-any-command-regexp201,6312
-(defconst isar-name-regexp208,6685
-(defconst isar-improper-regexp214,6980
-(defconst isar-save-command-regexp218,7128
-(defconst isar-global-save-command-regexp221,7229
-(defconst isar-goal-command-regexp224,7343
-(defconst isar-local-goal-command-regexp227,7451
-(defconst isar-comment-start 230,7564
-(defconst isar-comment-end 231,7599
-(defconst isar-comment-start-regexp 232,7632
-(defconst isar-comment-end-regexp 233,7703
-(defconst isar-string-start-regexp 235,7771
-(defconst isar-string-end-regexp 236,7823
-(defun isar-syntactic-context 238,7874
-(defconst isar-antiq-regexp253,8269
-(defconst isar-nesting-regexp259,8420
-(defun isar-nesting 262,8518
-(defun isar-match-nesting 274,8911
-(defface isabelle-string-face 286,9245
-(defface isabelle-quote-face 294,9445
-(defface isabelle-class-name-face302,9641
-(defface isabelle-tfree-name-face310,9828
-(defface isabelle-tvar-name-face318,10021
-(defface isabelle-free-name-face326,10213
-(defface isabelle-bound-name-face334,10401
-(defface isabelle-var-name-face342,10592
-(defconst isabelle-string-face 350,10783
-(defconst isabelle-quote-face 351,10837
-(defconst isabelle-class-name-face 352,10890
-(defconst isabelle-tfree-name-face 353,10952
-(defconst isabelle-tvar-name-face 354,11014
-(defconst isabelle-free-name-face 355,11075
-(defconst isabelle-bound-name-face 356,11136
-(defconst isabelle-var-name-face 357,11198
-(defun isar-font-lock-fontify-syntactically-region 363,11347
-(defvar isar-font-lock-keywords-1398,12623
-(defun isar-output-flkprops 416,13631
-(defun isar-output-flk 422,13883
-(defvar isar-output-font-lock-keywords-1425,13992
-(defun isar-strip-output-markup 461,15415
-(defconst isar-shell-font-lock-keywords465,15551
-(defvar isar-goals-font-lock-keywords468,15635
-(defconst isar-linear-undo 502,16314
-(defconst isar-undo 504,16357
-(defconst isar-pr506,16400
-(defun isar-remove 513,16558
-(defun isar-undos 516,16633
-(defun isar-cannot-undo 526,16867
-(defconst isar-undo-commands529,16937
-(defconst isar-theory-start-regexp537,17074
-(defconst isar-end-regexp543,17232
-(defconst isar-undo-fail-regexp547,17333
-(defconst isar-undo-skip-regexp551,17437
-(defconst isar-undo-ignore-regexp554,17558
-(defconst isar-undo-remove-regexp557,17623
-(defconst isar-keywords-imenu565,17780
-(defconst isar-entity-regexp 572,17971
-(defconst isar-named-entity-regexp575,18067
-(defconst isar-named-entity-name-match-number580,18197
-(defconst isar-generic-expression583,18298
-(defconst isar-indent-any-regexp594,18532
-(defconst isar-indent-inner-regexp596,18625
-(defconst isar-indent-enclose-regexp598,18691
-(defconst isar-indent-open-regexp600,18807
-(defconst isar-indent-close-regexp602,18917
-(defconst isar-outline-regexp608,19054
-(defconst isar-outline-heading-end-regexp 612,19207
-(defconst isar-outline-heading-alist 614,19256
+(defconst isar-script-syntax-table-entries18,489
+(defconst isar-script-syntax-table-alist42,891
+(defun isar-init-syntax-table 51,1174
+(defun isar-init-output-syntax-table 59,1421
+(defconst isar-keyword-begin 74,1863
+(defconst isar-keyword-end 75,1901
+(defconst isar-keywords-theory-enclose77,1936
+(defconst isar-keywords-theory82,2074
+(defconst isar-keywords-save87,2205
+(defconst isar-keywords-proof-enclose92,2320
+(defconst isar-keywords-proof98,2481
+(defconst isar-keywords-proof-context105,2658
+(defconst isar-keywords-local-goal109,2765
+(defconst isar-keywords-proper113,2870
+(defconst isar-keywords-improper118,2989
+(defconst isar-keyword-level-alist123,3121
+(defconst isar-keywords-outline 138,3592
+(defconst isar-keywords-indent-open141,3668
+(defconst isar-keywords-indent-close148,3854
+(defconst isar-keywords-indent-enclose153,3987
+(defconst isar-ext-first 163,4216
+(defconst isar-ext-rest 164,4283
+(defconst isar-long-id-stuff 166,4355
+(defconst isar-id 167,4429
+(defconst isar-idx 168,4499
+(defconst isar-string 170,4558
+(defun isar-ids-to-regexp 172,4618
+(defconst isar-any-command-regexp204,6410
+(defconst isar-name-regexp211,6783
+(defconst isar-improper-regexp217,7078
+(defconst isar-save-command-regexp221,7226
+(defconst isar-global-save-command-regexp224,7327
+(defconst isar-goal-command-regexp227,7441
+(defconst isar-local-goal-command-regexp230,7549
+(defconst isar-comment-start 233,7662
+(defconst isar-comment-end 234,7697
+(defconst isar-comment-start-regexp 235,7730
+(defconst isar-comment-end-regexp 236,7801
+(defconst isar-string-start-regexp 238,7869
+(defconst isar-string-end-regexp 239,7921
+(defun isar-syntactic-context 241,7972
+(defconst isar-antiq-regexp256,8367
+(defconst isar-nesting-regexp262,8518
+(defun isar-nesting 265,8616
+(defun isar-match-nesting 277,9009
+(defface isabelle-string-face 289,9343
+(defface isabelle-quote-face 297,9543
+(defface isabelle-class-name-face305,9739
+(defface isabelle-tfree-name-face313,9926
+(defface isabelle-tvar-name-face321,10119
+(defface isabelle-free-name-face329,10311
+(defface isabelle-bound-name-face337,10499
+(defface isabelle-var-name-face345,10690
+(defconst isabelle-string-face 353,10881
+(defconst isabelle-quote-face 354,10935
+(defconst isabelle-class-name-face 355,10988
+(defconst isabelle-tfree-name-face 356,11050
+(defconst isabelle-tvar-name-face 357,11112
+(defconst isabelle-free-name-face 358,11173
+(defconst isabelle-bound-name-face 359,11234
+(defconst isabelle-var-name-face 360,11296
+(defun isar-font-lock-fontify-syntactically-region 366,11445
+(defvar isar-font-lock-keywords-1401,12721
+(defun isar-output-flkprops 419,13729
+(defun isar-output-flk 425,13981
+(defvar isar-output-font-lock-keywords-1428,14090
+(defun isar-strip-output-markup 464,15513
+(defconst isar-shell-font-lock-keywords468,15649
+(defvar isar-goals-font-lock-keywords471,15733
+(defconst isar-linear-undo 505,16412
+(defconst isar-undo 507,16455
+(defconst isar-pr509,16498
+(defun isar-remove 516,16656
+(defun isar-undos 519,16731
+(defun isar-cannot-undo 529,16965
+(defconst isar-undo-commands532,17035
+(defconst isar-theory-start-regexp540,17172
+(defconst isar-end-regexp546,17330
+(defconst isar-undo-fail-regexp550,17431
+(defconst isar-undo-skip-regexp554,17535
+(defconst isar-undo-ignore-regexp557,17656
+(defconst isar-undo-remove-regexp560,17721
+(defconst isar-keywords-imenu568,17878
+(defconst isar-entity-regexp 575,18069
+(defconst isar-named-entity-regexp578,18165
+(defconst isar-named-entity-name-match-number583,18295
+(defconst isar-generic-expression586,18396
+(defconst isar-indent-any-regexp597,18630
+(defconst isar-indent-inner-regexp599,18723
+(defconst isar-indent-enclose-regexp601,18789
+(defconst isar-indent-open-regexp603,18905
+(defconst isar-indent-close-regexp605,19015
+(defconst isar-outline-regexp611,19152
+(defconst isar-outline-heading-end-regexp 615,19305
+(defconst isar-outline-heading-alist 617,19354
 
 isar/isar-unicode-tokens.el,1363
 (defgroup isabelle-tokens 25,672
@@ -606,46 +637,46 @@ isar/isar-unicode-tokens.el,1363
 (defconst isar-tokens-customizable-variables661,17747
 
 lego/lego.el,1636
-(defcustom lego-tags 21,535
-(defcustom lego-test-all-name 26,671
-(defpgdefault help-menu-entries32,829
-(defpgdefault menu-entries36,989
-(defvar lego-shell-handle-output47,1290
-(defconst lego-process-config55,1588
-(defconst lego-pretty-set-width 66,2019
-(defconst lego-interrupt-regexp 70,2161
-(defcustom lego-www-home-page 75,2278
-(defcustom lego-www-latest-release80,2402
-(defcustom lego-www-refcard86,2577
-(defcustom lego-library-www-page92,2726
-(defvar lego-prog-name 101,2942
-(defvar lego-shell-cd 104,3011
-(defvar lego-shell-proof-completed-regexp 107,3110
-(defvar lego-save-command-regexp110,3250
-(defvar lego-goal-command-regexp112,3340
-(defvar lego-kill-goal-command 115,3431
-(defvar lego-forget-id-command 116,3474
-(defvar lego-undoable-commands-regexp118,3520
-(defvar lego-goal-regexp 127,3894
-(defvar lego-outline-regexp129,3939
-(defvar lego-outline-heading-end-regexp 135,4114
-(defvar lego-shell-outline-regexp 137,4167
-(defvar lego-shell-outline-heading-end-regexp 138,4219
-(define-derived-mode lego-shell-mode 144,4498
-(define-derived-mode lego-mode 151,4659
-(define-derived-mode lego-goals-mode 162,4969
-(defun lego-count-undos 173,5395
-(defun lego-goal-command-p 192,6132
-(defun lego-find-and-forget 197,6303
-(defun lego-goal-hyp 239,8139
-(defun lego-state-preserving-p 248,8336
-(defvar lego-shell-current-line-width 264,9039
-(defun lego-shell-adjust-line-width 272,9346
-(defun lego-mode-config 289,10047
-(defun lego-equal-module-filename 357,12098
-(defun lego-shell-compute-new-files-list 363,12373
-(defun lego-shell-mode-config 373,12756
-(defun lego-goals-mode-config 420,14423
+(defcustom lego-tags 21,534
+(defcustom lego-test-all-name 26,670
+(defpgdefault help-menu-entries32,828
+(defpgdefault menu-entries36,988
+(defvar lego-shell-handle-output47,1289
+(defconst lego-process-config55,1587
+(defconst lego-pretty-set-width 66,2018
+(defconst lego-interrupt-regexp 70,2160
+(defcustom lego-www-home-page 75,2277
+(defcustom lego-www-latest-release80,2401
+(defcustom lego-www-refcard86,2576
+(defcustom lego-library-www-page92,2725
+(defvar lego-prog-name 101,2941
+(defvar lego-shell-cd 104,3010
+(defvar lego-shell-proof-completed-regexp 107,3109
+(defvar lego-save-command-regexp110,3249
+(defvar lego-goal-command-regexp112,3339
+(defvar lego-kill-goal-command 115,3430
+(defvar lego-forget-id-command 116,3473
+(defvar lego-undoable-commands-regexp118,3519
+(defvar lego-goal-regexp 127,3893
+(defvar lego-outline-regexp129,3938
+(defvar lego-outline-heading-end-regexp 135,4113
+(defvar lego-shell-outline-regexp 137,4166
+(defvar lego-shell-outline-heading-end-regexp 138,4218
+(define-derived-mode lego-shell-mode 144,4497
+(define-derived-mode lego-mode 151,4658
+(define-derived-mode lego-goals-mode 162,4968
+(defun lego-count-undos 173,5394
+(defun lego-goal-command-p 192,6131
+(defun lego-find-and-forget 197,6302
+(defun lego-goal-hyp 239,8138
+(defun lego-state-preserving-p 248,8335
+(defvar lego-shell-current-line-width 264,9038
+(defun lego-shell-adjust-line-width 272,9345
+(defun lego-mode-config 289,10046
+(defun lego-equal-module-filename 357,12097
+(defun lego-shell-compute-new-files-list 363,12372
+(defun lego-shell-mode-config 373,12755
+(defun lego-goals-mode-config 420,14422
 
 lego/lego-syntax.el,600
 (defconst lego-keywords-goal 15,358
@@ -824,46 +855,46 @@ generic/pg-assoc.el,81
 (defun proof-associated-buffers 33,973
 (defun proof-associated-windows 43,1183
 
-generic/pg-autotest.el,869
-(defvar pg-autotest-success 30,692
-(defvar pg-autotest-log 33,779
-(defadvice proof-debug 39,972
-(defun pg-autotest-find-file 47,1176
-(defun pg-autotest-find-file-restart 54,1442
-(defmacro pg-autotest 68,1916
-(defun pg-autotest-log 95,2637
-(defun pg-autotest-message 103,2861
-(defun pg-autotest-remark 112,3150
-(defun pg-autotest-timestart 115,3231
-(defun pg-autotest-timetaken 120,3414
-(defun pg-autotest-exit 131,3778
-(defun pg-autotest-test-process-wholefile 142,4129
-(defun pg-autotest-test-script-wholefile 150,4416
-(defun pg-autotest-test-script-randomjumps 175,5348
-(defun pg-autotest-test-retract-file 224,6905
-(defun pg-autotest-test-assert-processed 230,7046
-(defun pg-autotest-test-assert-full 236,7272
-(defun pg-autotest-test-assert-unprocessed 243,7513
-(defun pg-autotest-test-eval 250,7778
-(defun pg-autotest-test-quit-prover 254,7877
+generic/pg-autotest.el,874
+(defconst pg-autotest-debug 27,679
+(defvar pg-autotest-success 32,752
+(defvar pg-autotest-log 35,839
+(defun pg-autotest-find-file 49,1272
+(defun pg-autotest-find-file-restart 56,1538
+(defmacro pg-autotest 70,2012
+(defun pg-autotest-log 97,2733
+(defun pg-autotest-message 105,2957
+(defun pg-autotest-remark 114,3246
+(defun pg-autotest-timestart 117,3327
+(defun pg-autotest-timetaken 122,3510
+(defun pg-autotest-exit 133,3874
+(defun pg-autotest-test-process-wholefile 144,4225
+(defun pg-autotest-test-script-wholefile 152,4512
+(defun pg-autotest-test-script-randomjumps 177,5444
+(defun pg-autotest-test-retract-file 226,7001
+(defun pg-autotest-test-assert-processed 232,7142
+(defun pg-autotest-test-assert-full 238,7368
+(defun pg-autotest-test-assert-unprocessed 245,7609
+(defun pg-autotest-test-eval 252,7874
+(defun pg-autotest-test-quit-prover 256,7973
 
 generic/pg-custom.el,599
-(defpgcustom script-indent 37,1199
-(defconst proof-toolbar-entries-default42,1336
-(defpgcustom toolbar-entries 70,3069
-(defpgcustom prog-args 89,3802
-(defpgcustom prog-env 102,4377
-(defpgcustom favourites 111,4804
-(defpgcustom menu-entries 116,4993
-(defpgcustom help-menu-entries 123,5229
-(defpgcustom keymap 130,5492
-(defpgcustom completion-table 135,5663
-(defpgcustom tags-program 146,6037
-(defpgcustom use-holes 155,6421
-(defpgcustom one-command-per-line162,6679
-(defpgcustom maths-menu-enable 173,6915
-(defpgcustom unicode-tokens-enable 179,7095
-(defpgcustom mmm-enable 185,7272
+(defpgcustom script-indent 37,1198
+(defconst proof-toolbar-entries-default42,1335
+(defpgcustom toolbar-entries 70,3068
+(defpgcustom prog-args 89,3801
+(defpgcustom prog-env 102,4376
+(defpgcustom favourites 111,4803
+(defpgcustom menu-entries 116,4992
+(defpgcustom help-menu-entries 123,5228
+(defpgcustom keymap 130,5491
+(defpgcustom completion-table 135,5662
+(defpgcustom tags-program 146,6036
+(defpgcustom use-holes 155,6420
+(defpgcustom one-command-per-line162,6678
+(defpgcustom maths-menu-enable 173,6914
+(defpgcustom unicode-tokens-enable 179,7094
+(defpgcustom mmm-enable 185,7301
 
 generic/pg-goals.el,285
 (define-derived-mode proof-goals-mode 29,734
@@ -898,51 +929,51 @@ generic/pg-pamacs.el,486
 (defmacro defpgdefault 120,4238
 (defmacro defpgfun 131,4600
 (defun proof-defpacustom-fn 145,4999
-(defmacro defpacustom 209,7183
-(defmacro proof-eval-when-ready-for-assistant 230,8130
+(defmacro defpacustom 212,7292
+(defmacro proof-eval-when-ready-for-assistant 233,8239
 
 generic/pg-pbrpm.el,1808
-(defvar pg-pbrpm-use-buffer-menu 45,1208
-(defvar pg-pbrpm-start-goal-regexp 48,1330
-(defvar pg-pbrpm-start-goal-regexp-par-num 52,1487
-(defvar pg-pbrpm-end-goal-regexp 55,1610
-(defvar pg-pbrpm-start-hyp-regexp 59,1762
-(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1923
-(defvar pg-pbrpm-start-concl-regexp 67,2130
-(defvar pg-pbrpm-auto-select-regexp 71,2294
-(defvar pg-pbrpm-buffer-menu 78,2455
-(defvar pg-pbrpm-spans 79,2489
-(defvar pg-pbrpm-goal-description 80,2517
-(defvar pg-pbrpm-windows-dialog-bug 81,2556
-(defvar pbrpm-menu-desc 82,2597
-(defun pg-pbrpm-erase-buffer-menu 84,2627
-(defun pg-pbrpm-menu-change-hook 90,2799
-(defun pg-pbrpm-create-reset-buffer-menu 108,3374
-(defun pg-pbrpm-analyse-goal-buffer 127,4216
-(defun pg-pbrpm-button-action 187,6621
-(defun pg-pbrpm-exists 194,6847
-(defun pg-pbrpm-eliminate-id 198,6959
-(defun pg-pbrpm-build-menu 206,7205
-(defun pg-pbrpm-setup-span 269,9525
-(defun pg-pbrpm-run-command 329,11824
-(defun pg-pbrpm-get-pos-info 362,13349
-(defun pg-pbrpm-get-region-info 404,14648
-(defun pg-pbrpm-auto-select-around-point 415,15060
-(defun pg-pbrpm-translate-position 430,15584
-(defun pg-pbrpm-process-click 438,15838
-(defvar pg-pbrpm-remember-region-selected-region 458,16863
-(defvar pg-pbrpm-regions-list 459,16917
-(defun pg-pbrpm-erase-regions-list 461,16953
-(defun pg-pbrpm-filter-regions-list 470,17261
-(defface pg-pbrpm-multiple-selection-face477,17524
-(defface pg-pbrpm-menu-input-face485,17726
-(defun pg-pbrpm-do-remember-region 493,17916
-(defun pg-pbrpm-remember-region-drag-up-hook 514,18764
-(defun pg-pbrpm-remember-region-click-hook 518,18935
-(defun pg-pbrpm-remember-region 523,19120
-(defun pg-pbrpm-process-region 537,19834
-(defun pg-pbrpm-process-regions-list 555,20563
-(defun pg-pbrpm-region-expression 559,20746
+(defvar pg-pbrpm-use-buffer-menu 45,1207
+(defvar pg-pbrpm-start-goal-regexp 48,1329
+(defvar pg-pbrpm-start-goal-regexp-par-num 52,1486
+(defvar pg-pbrpm-end-goal-regexp 55,1609
+(defvar pg-pbrpm-start-hyp-regexp 59,1761
+(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1922
+(defvar pg-pbrpm-start-concl-regexp 67,2129
+(defvar pg-pbrpm-auto-select-regexp 71,2293
+(defvar pg-pbrpm-buffer-menu 78,2454
+(defvar pg-pbrpm-spans 79,2488
+(defvar pg-pbrpm-goal-description 80,2516
+(defvar pg-pbrpm-windows-dialog-bug 81,2555
+(defvar pbrpm-menu-desc 82,2596
+(defun pg-pbrpm-erase-buffer-menu 84,2626
+(defun pg-pbrpm-menu-change-hook 90,2798
+(defun pg-pbrpm-create-reset-buffer-menu 108,3373
+(defun pg-pbrpm-analyse-goal-buffer 127,4215
+(defun pg-pbrpm-button-action 187,6620
+(defun pg-pbrpm-exists 194,6846
+(defun pg-pbrpm-eliminate-id 198,6958
+(defun pg-pbrpm-build-menu 206,7204
+(defun pg-pbrpm-setup-span 269,9524
+(defun pg-pbrpm-run-command 329,11823
+(defun pg-pbrpm-get-pos-info 362,13348
+(defun pg-pbrpm-get-region-info 404,14647
+(defun pg-pbrpm-auto-select-around-point 415,15059
+(defun pg-pbrpm-translate-position 430,15583
+(defun pg-pbrpm-process-click 438,15837
+(defvar pg-pbrpm-remember-region-selected-region 458,16862
+(defvar pg-pbrpm-regions-list 459,16916
+(defun pg-pbrpm-erase-regions-list 461,16952
+(defun pg-pbrpm-filter-regions-list 470,17260
+(defface pg-pbrpm-multiple-selection-face477,17523
+(defface pg-pbrpm-menu-input-face485,17725
+(defun pg-pbrpm-do-remember-region 493,17915
+(defun pg-pbrpm-remember-region-drag-up-hook 514,18763
+(defun pg-pbrpm-remember-region-click-hook 518,18934
+(defun pg-pbrpm-remember-region 523,19119
+(defun pg-pbrpm-process-region 537,19833
+(defun pg-pbrpm-process-regions-list 555,20562
+(defun pg-pbrpm-region-expression 559,20745
 
 generic/pg-pgip.el,2931
 (defalias 'pg-pgip-debug pg-pgip-debug
38,1032
@@ -996,181 +1027,181 @@ generic/pg-pgip.el,2931
 (defun pg-pgip-process-objectstatus 426,14409
 (defun pg-pgip-process-parsescript 440,14761
 (defun pg-pgip-get-pgiptype 463,15635
-(defun pg-pgip-default-for 483,16427
-(defun pg-pgip-subst-for 496,16822
-(defun pg-pgip-interpret-value 508,17165
-(defun pg-pgip-interpret-choice 526,17846
-(defun pg-pgip-string-of-command 557,18863
-(defconst pg-pgip-id574,19624
-(defvar pg-pgip-refseq 580,19904
-(defvar pg-pgip-refid 582,20001
-(defvar pg-pgip-seq 585,20093
-(defun pg-pgip-assemble-packet 587,20157
-(defun pg-pgip-issue 605,20968
-(defun pg-pgip-maybe-askpgip 622,21580
-(defun pg-pgip-askprefs 628,21771
-(defun pg-pgip-askids 632,21885
-(defun pg-pgip-reset 645,22173
-(defconst pg-pgip-start-element-regexp 676,22871
-(defconst pg-pgip-end-element-regexp 677,22923
+(defun pg-pgip-default-for 484,16498
+(defun pg-pgip-subst-for 497,16893
+(defun pg-pgip-interpret-value 510,17263
+(defun pg-pgip-interpret-choice 529,17988
+(defun pg-pgip-string-of-command 560,19005
+(defconst pg-pgip-id577,19766
+(defvar pg-pgip-refseq 583,20046
+(defvar pg-pgip-refid 585,20143
+(defvar pg-pgip-seq 588,20235
+(defun pg-pgip-assemble-packet 590,20299
+(defun pg-pgip-issue 608,21110
+(defun pg-pgip-maybe-askpgip 625,21722
+(defun pg-pgip-askprefs 631,21913
+(defun pg-pgip-askids 635,22027
+(defun pg-pgip-reset 648,22315
+(defconst pg-pgip-start-element-regexp 679,23013
+(defconst pg-pgip-end-element-regexp 680,23065
 
 generic/pg-response.el,1291
-(deflocal pg-response-eagerly-raise 32,789
-(define-derived-mode proof-response-mode 42,1014
-(define-key proof-response-mode-map 69,1951
-(define-key proof-response-mode-map 70,2022
-(define-key proof-response-mode-map 71,2076
-(defun proof-response-config-done 75,2162
-(defvar pg-response-special-display-regexp 86,2508
-(defconst proof-multiframe-parameters90,2675
-(defun proof-multiple-frames-enable 99,2965
-(defun proof-three-window-enable 109,3293
-(defun proof-select-three-b 112,3356
-(defun proof-display-three-b 127,3847
-(defvar pg-frame-configuration 138,4237
-(defun pg-cache-frame-configuration 142,4384
-(defun proof-layout-windows 146,4555
-(defun proof-delete-other-frames 186,6342
-(defvar pg-response-erase-flag 217,7430
-(defun pg-response-maybe-erase221,7559
-(defun pg-response-display 251,8663
-(defun pg-response-display-with-face 276,9446
-(defun pg-response-clear-displays 304,10292
-(defun pg-response-message 317,10811
-(defun pg-response-warning 323,11046
-(defun proof-next-error 338,11452
-(defun pg-response-has-error-location 416,14261
-(defvar proof-trace-last-fontify-pos 438,15074
-(defun proof-trace-fontify-pos 440,15117
-(defun proof-trace-buffer-display 448,15430
-(defun proof-trace-buffer-finish 459,15774
-(defun pg-thms-buffer-clear 477,16117
+(deflocal pg-response-eagerly-raise 32,788
+(define-derived-mode proof-response-mode 42,1013
+(define-key proof-response-mode-map 69,1950
+(define-key proof-response-mode-map 70,2021
+(define-key proof-response-mode-map 71,2075
+(defun proof-response-config-done 75,2161
+(defvar pg-response-special-display-regexp 86,2507
+(defconst proof-multiframe-parameters90,2674
+(defun proof-multiple-frames-enable 99,2964
+(defun proof-three-window-enable 109,3292
+(defun proof-select-three-b 112,3355
+(defun proof-display-three-b 127,3846
+(defvar pg-frame-configuration 138,4236
+(defun pg-cache-frame-configuration 142,4383
+(defun proof-layout-windows 146,4554
+(defun proof-delete-other-frames 186,6341
+(defvar pg-response-erase-flag 217,7429
+(defun pg-response-maybe-erase221,7558
+(defun pg-response-display 251,8662
+(defun pg-response-display-with-face 276,9445
+(defun pg-response-clear-displays 304,10291
+(defun pg-response-message 317,10810
+(defun pg-response-warning 323,11045
+(defun proof-next-error 338,11451
+(defun pg-response-has-error-location 416,14260
+(defvar proof-trace-last-fontify-pos 438,15073
+(defun proof-trace-fontify-pos 440,15116
+(defun proof-trace-buffer-display 448,15429
+(defun proof-trace-buffer-finish 459,15773
+(defun pg-thms-buffer-clear 477,16116
 
 generic/pg-user.el,3635
-(defun proof-script-new-command-advance 42,1232
-(defun proof-maybe-follow-locked-end 66,2157
-(defun proof-goto-command-start 92,2993
-(defun proof-goto-command-end 115,3940
-(defun proof-forward-command 130,4362
-(defun proof-backward-command 151,5083
-(defun proof-goto-point 162,5297
-(defun proof-assert-next-command-interactive 176,5731
-(defun proof-assert-until-point-interactive 188,6217
-(defun proof-process-buffer 194,6447
-(defun proof-undo-last-successful-command 212,6959
-(defun proof-undo-and-delete-last-successful-command 217,7121
-(defun proof-undo-last-successful-command-1 229,7642
-(defun proof-retract-buffer 246,8306
-(defun proof-retract-current-goal 255,8590
-(defun proof-mouse-goto-point 274,9110
-(defvar proof-minibuffer-history 289,9386
-(defun proof-minibuffer-cmd 292,9481
-(defun proof-frob-locked-end 331,10888
-(defmacro proof-if-setting-configured 367,11989
-(defmacro proof-define-assistant-command 375,12258
-(defmacro proof-define-assistant-command-witharg 388,12713
-(defun proof-issue-new-command 408,13535
-(defun proof-cd-sync 448,14758
-(defun proof-electric-terminator-enable 499,16357
-(defun proof-electric-terminator 507,16661
-(defun proof-add-completions 531,17441
-(defun proof-script-complete 554,18264
-(defun pg-copy-span-contents 568,18573
-(defun pg-numth-span-higher-or-lower 582,18997
-(defun pg-control-span-of 608,19743
-(defun pg-move-span-contents 614,19947
-(defun pg-fixup-children-spans 665,22065
-(defun pg-move-region-down 675,22322
-(defun pg-move-region-up 684,22615
-(defun pg-pos-for-event 698,22889
-(defun pg-span-for-event 704,23110
-(defun pg-span-context-menu 708,23254
-(defun pg-toggle-visibility 724,23771
-(defun pg-create-in-span-context-menu 733,24078
-(defun pg-span-undo 757,25010
-(defun pg-goals-buffers-hint 770,25248
-(defun pg-slow-fontify-tracing-hint 774,25430
-(defun pg-response-buffers-hint 778,25601
-(defun pg-jump-to-end-hint 790,26016
-(defun pg-processing-complete-hint 794,26145
-(defun pg-next-error-hint 811,26865
-(defun pg-hint 816,27017
-(defun pg-identifier-under-mouse-query 827,27366
-(defun pg-identifier-near-point-query 838,27690
-(defvar proof-query-identifier-history 867,28613
-(defun proof-query-identifier 870,28700
-(defun pg-identifier-query 881,29056
-(defun proof-imenu-enable 914,30204
-(defvar pg-input-ring 950,31507
-(defvar pg-input-ring-index 953,31564
-(defvar pg-stored-incomplete-input 956,31636
-(defun pg-previous-input 959,31739
-(defun pg-next-input 973,32202
-(defun pg-delete-input 978,32324
-(defun pg-get-old-input 991,32662
-(defun pg-restore-input 1005,33053
-(defun pg-search-start 1016,33343
-(defun pg-regexp-arg 1028,33835
-(defun pg-search-arg 1040,34283
-(defun pg-previous-matching-input-string-position 1054,34700
-(defun pg-previous-matching-input 1081,35865
-(defun pg-next-matching-input 1100,36715
-(defvar pg-matching-input-from-input-string 1108,37098
-(defun pg-previous-matching-input-from-input 1112,37212
-(defun pg-next-matching-input-from-input 1130,37977
-(defun pg-add-to-input-history 1141,38356
-(defun pg-remove-from-input-history 1153,38809
-(defun  pg-clear-input-ring 1164,39189
-(define-key proof-mode-map 1181,39659
-(define-key proof-mode-map 1182,39719
-(defun pg-protected-undo 1184,39791
-(defun pg-protected-undo-1 1214,41085
-(defun next-undo-elt 1245,42522
-(defvar proof-autosend-timer 1272,43478
-(deflocal proof-autosend-modified-tick 1274,43539
-(defun proof-autosend-enable 1278,43661
-(defun proof-autosend-delay 1292,44204
-(defun proof-autosend-loop 1296,44337
-(defun proof-autosend-loop-all 1310,44897
-(defun proof-autosend-loop-next 1334,45677
+(defun proof-script-new-command-advance 42,1231
+(defun proof-maybe-follow-locked-end 66,2156
+(defun proof-goto-command-start 92,2992
+(defun proof-goto-command-end 115,3939
+(defun proof-forward-command 130,4361
+(defun proof-backward-command 151,5082
+(defun proof-goto-point 162,5296
+(defun proof-assert-next-command-interactive 176,5730
+(defun proof-assert-until-point-interactive 188,6216
+(defun proof-process-buffer 194,6446
+(defun proof-undo-last-successful-command 212,6958
+(defun proof-undo-and-delete-last-successful-command 217,7120
+(defun proof-undo-last-successful-command-1 229,7641
+(defun proof-retract-buffer 246,8305
+(defun proof-retract-current-goal 255,8589
+(defun proof-mouse-goto-point 274,9109
+(defvar proof-minibuffer-history 289,9385
+(defun proof-minibuffer-cmd 292,9480
+(defun proof-frob-locked-end 331,10887
+(defmacro proof-if-setting-configured 367,11988
+(defmacro proof-define-assistant-command 375,12257
+(defmacro proof-define-assistant-command-witharg 388,12712
+(defun proof-issue-new-command 408,13534
+(defun proof-cd-sync 448,14757
+(defun proof-electric-terminator-enable 499,16356
+(defun proof-electric-terminator 507,16660
+(defun proof-add-completions 531,17440
+(defun proof-script-complete 554,18263
+(defun pg-copy-span-contents 568,18572
+(defun pg-numth-span-higher-or-lower 582,18996
+(defun pg-control-span-of 608,19742
+(defun pg-move-span-contents 614,19946
+(defun pg-fixup-children-spans 665,22064
+(defun pg-move-region-down 675,22321
+(defun pg-move-region-up 684,22614
+(defun pg-pos-for-event 698,22888
+(defun pg-span-for-event 704,23109
+(defun pg-span-context-menu 708,23253
+(defun pg-toggle-visibility 724,23770
+(defun pg-create-in-span-context-menu 733,24077
+(defun pg-span-undo 757,25009
+(defun pg-goals-buffers-hint 770,25247
+(defun pg-slow-fontify-tracing-hint 774,25429
+(defun pg-response-buffers-hint 778,25600
+(defun pg-jump-to-end-hint 790,26015
+(defun pg-processing-complete-hint 794,26144
+(defun pg-next-error-hint 811,26864
+(defun pg-hint 816,27016
+(defun pg-identifier-under-mouse-query 827,27365
+(defun pg-identifier-near-point-query 838,27689
+(defvar proof-query-identifier-history 867,28612
+(defun proof-query-identifier 870,28699
+(defun pg-identifier-query 881,29055
+(defun proof-imenu-enable 914,30203
+(defvar pg-input-ring 950,31506
+(defvar pg-input-ring-index 953,31563
+(defvar pg-stored-incomplete-input 956,31635
+(defun pg-previous-input 959,31738
+(defun pg-next-input 973,32201
+(defun pg-delete-input 978,32323
+(defun pg-get-old-input 991,32661
+(defun pg-restore-input 1005,33052
+(defun pg-search-start 1016,33342
+(defun pg-regexp-arg 1028,33834
+(defun pg-search-arg 1040,34282
+(defun pg-previous-matching-input-string-position 1054,34699
+(defun pg-previous-matching-input 1081,35864
+(defun pg-next-matching-input 1100,36714
+(defvar pg-matching-input-from-input-string 1108,37097
+(defun pg-previous-matching-input-from-input 1112,37211
+(defun pg-next-matching-input-from-input 1130,37976
+(defun pg-add-to-input-history 1141,38355
+(defun pg-remove-from-input-history 1153,38808
+(defun  pg-clear-input-ring 1164,39188
+(define-key proof-mode-map 1181,39658
+(define-key proof-mode-map 1182,39718
+(defun pg-protected-undo 1184,39790
+(defun pg-protected-undo-1 1214,41084
+(defun next-undo-elt 1245,42521
+(defvar proof-autosend-timer 1272,43477
+(deflocal proof-autosend-modified-tick 1274,43538
+(defun proof-autosend-enable 1278,43660
+(defun proof-autosend-delay 1292,44203
+(defun proof-autosend-loop 1296,44336
+(defun proof-autosend-loop-all 1310,44896
+(defun proof-autosend-loop-next 1334,45676
 
 generic/pg-vars.el,1500
-(defvar proof-assistant-cusgrp 22,389
-(defvar proof-assistant-internals-cusgrp 28,649
-(defvar proof-assistant 34,919
-(defvar proof-assistant-symbol 39,1142
-(defvar proof-mode-for-shell 52,1684
-(defvar proof-mode-for-response 57,1874
-(defvar proof-mode-for-goals 62,2100
-(defvar proof-mode-for-script 67,2289
-(defvar proof-ready-for-assistant-hook 72,2466
-(defvar proof-shell-busy 83,2754
-(defvar proof-shell-last-queuemode 101,3425
-(defvar proof-included-files-list 105,3580
-(defvar proof-script-buffer 127,4599
-(defvar proof-previous-script-buffer 130,4691
-(defvar proof-shell-buffer 134,4864
-(defvar proof-goals-buffer 137,4950
-(defvar proof-response-buffer 140,5005
-(defvar proof-trace-buffer 143,5066
-(defvar proof-thms-buffer 147,5220
-(defvar proof-shell-error-or-interrupt-seen 151,5375
-(defvar pg-response-next-error 156,5599
-(defvar proof-shell-proof-completed 159,5706
-(defvar proof-shell-silent 173,6091
-(defvar proof-shell-last-prompt 176,6179
-(defvar proof-shell-last-output 180,6349
-(defvar proof-shell-last-output-kind 184,6489
-(defvar proof-assistant-settings 204,7253
-(defvar pg-tracing-slow-mode 212,7701
-(defvar proof-nesting-depth 215,7790
-(defvar proof-last-theorem-dependencies 222,8025
-(defvar proof-autosend-running 226,8187
-(defvar proof-next-command-on-new-line 231,8386
-(defcustom proof-general-name 242,8620
-(defcustom proof-general-home-page247,8777
-(defcustom proof-unnamed-theorem-name253,8937
-(defcustom proof-universal-keys259,9121
+(defvar proof-assistant-cusgrp 22,388
+(defvar proof-assistant-internals-cusgrp 28,648
+(defvar proof-assistant 34,918
+(defvar proof-assistant-symbol 39,1141
+(defvar proof-mode-for-shell 52,1683
+(defvar proof-mode-for-response 57,1873
+(defvar proof-mode-for-goals 62,2099
+(defvar proof-mode-for-script 67,2288
+(defvar proof-ready-for-assistant-hook 72,2465
+(defvar proof-shell-busy 83,2753
+(defvar proof-shell-last-queuemode 101,3424
+(defvar proof-included-files-list 105,3579
+(defvar proof-script-buffer 127,4598
+(defvar proof-previous-script-buffer 130,4690
+(defvar proof-shell-buffer 134,4863
+(defvar proof-goals-buffer 137,4949
+(defvar proof-response-buffer 140,5004
+(defvar proof-trace-buffer 143,5065
+(defvar proof-thms-buffer 147,5219
+(defvar proof-shell-error-or-interrupt-seen 151,5374
+(defvar pg-response-next-error 156,5598
+(defvar proof-shell-proof-completed 159,5705
+(defvar proof-shell-silent 173,6090
+(defvar proof-shell-last-prompt 176,6178
+(defvar proof-shell-last-output 180,6348
+(defvar proof-shell-last-output-kind 184,6488
+(defvar proof-assistant-settings 204,7252
+(defvar pg-tracing-slow-mode 212,7700
+(defvar proof-nesting-depth 215,7789
+(defvar proof-last-theorem-dependencies 222,8024
+(defvar proof-autosend-running 226,8186
+(defvar proof-next-command-on-new-line 231,8385
+(defcustom proof-general-name 242,8619
+(defcustom proof-general-home-page247,8776
+(defcustom proof-unnamed-theorem-name253,8936
+(defcustom proof-universal-keys259,9120
 
 generic/pg-xml.el,1177
 (defalias 'pg-xml-error pg-xml-error
18,381
@@ -1206,169 +1237,171 @@ generic/pg-xml.el,1177
 (defun pg-pgip-get-pgmltext 222,7237
 
 generic/proof-autoloads.el,97
-(defsubst proof-shell-live-buffer 677,21893
-(defsubst proof-replace-regexp-in-string 822,27140
+(defsubst proof-shell-live-buffer 687,22247
+(defsubst proof-replace-regexp-in-string 840,27747
 
 generic/proof-auxmodes.el,149
 (defun proof-mmm-support-available 20,495
 (defun proof-maths-menu-support-available 44,1114
 (defun proof-unicode-tokens-support-available 58,1531
 
-generic/proof-config.el,7744
-(defgroup prover-config 80,2633
-(defcustom proof-guess-command-line 98,3483
-(defcustom proof-assistant-home-page 113,3978
-(defcustom proof-context-command 119,4148
-(defcustom proof-info-command 124,4282
-(defcustom proof-showproof-command 131,4553
-(defcustom proof-goal-command 136,4689
-(defcustom proof-save-command 144,4986
-(defcustom proof-find-theorems-command 152,5295
-(defcustom proof-query-identifier-command 159,5603
-(defcustom proof-assistant-true-value 173,6292
-(defcustom proof-assistant-false-value 179,6482
-(defcustom proof-assistant-format-int-fn 185,6676
-(defcustom proof-assistant-format-string-fn 192,6925
-(defcustom proof-assistant-setting-format 199,7192
-(defgroup proof-script 221,7887
-(defcustom proof-terminal-string 226,8017
-(defcustom proof-electric-terminator-noterminator 236,8405
-(defcustom proof-script-sexp-commands 241,8577
-(defcustom proof-script-command-end-regexp 252,9036
-(defcustom proof-script-command-start-regexp 270,9857
-(defcustom proof-script-integral-proofs 281,10320
-(defcustom proof-script-fly-past-comments 296,10976
-(defcustom proof-script-parse-function 301,11147
-(defcustom proof-script-comment-start 319,11792
-(defcustom proof-script-comment-start-regexp 330,12229
-(defcustom proof-script-comment-end 338,12548
-(defcustom proof-script-comment-end-regexp 350,12970
-(defcustom proof-string-start-regexp 358,13283
-(defcustom proof-string-end-regexp 363,13448
-(defcustom proof-case-fold-search 368,13609
-(defcustom proof-save-command-regexp 377,14021
-(defcustom proof-save-with-hole-regexp 382,14131
-(defcustom proof-save-with-hole-result 393,14506
-(defcustom proof-goal-command-regexp 403,14946
-(defcustom proof-goal-with-hole-regexp 411,15233
-(defcustom proof-goal-with-hole-result 423,15676
-(defcustom proof-non-undoables-regexp 432,16050
-(defcustom proof-nested-undo-regexp 443,16505
-(defcustom proof-ignore-for-undo-count 459,17217
-(defcustom proof-script-imenu-generic-expression 467,17520
-(defcustom proof-goal-command-p 475,17859
-(defcustom proof-really-save-command-p 486,18350
-(defcustom proof-completed-proof-behaviour 495,18657
-(defcustom proof-count-undos-fn 523,20006
-(defcustom proof-find-and-forget-fn 535,20557
-(defcustom proof-forget-id-command 552,21266
-(defcustom pg-topterm-goalhyplit-fn 562,21624
-(defcustom proof-kill-goal-command 574,22159
-(defcustom proof-undo-n-times-cmd 588,22663
-(defcustom proof-nested-goals-history-p 602,23200
-(defcustom proof-arbitrary-undo-positions 611,23537
-(defcustom proof-state-preserving-p 625,24118
-(defcustom proof-activate-scripting-hook 635,24590
-(defcustom proof-deactivate-scripting-hook 654,25371
-(defcustom proof-script-evaluate-elisp-comment-regexp 663,25701
-(defcustom proof-indent 681,26287
-(defcustom proof-indent-hang 686,26394
-(defcustom proof-indent-enclose-offset 691,26520
-(defcustom proof-indent-open-offset 696,26662
-(defcustom proof-indent-close-offset 701,26799
-(defcustom proof-indent-any-regexp 706,26937
-(defcustom proof-indent-inner-regexp 711,27097
-(defcustom proof-indent-enclose-regexp 716,27251
-(defcustom proof-indent-open-regexp 721,27405
-(defcustom proof-indent-close-regexp 726,27557
-(defcustom proof-script-font-lock-keywords 732,27711
-(defcustom proof-script-syntax-table-entries 740,28063
-(defcustom proof-script-span-context-menu-extensions 758,28459
-(defgroup proof-shell 784,29219
-(defcustom proof-prog-name 794,29389
-(defcustom proof-shell-auto-terminate-commands 805,29809
-(defcustom proof-shell-pre-sync-init-cmd 814,30214
-(defcustom proof-shell-init-cmd 828,30772
-(defcustom proof-shell-init-hook 840,31318
-(defcustom proof-shell-restart-cmd 845,31457
-(defcustom proof-shell-quit-cmd 850,31612
-(defcustom proof-shell-quit-timeout 855,31779
-(defcustom proof-shell-cd-cmd 864,32170
-(defcustom proof-shell-start-silent-cmd 881,32841
-(defcustom proof-shell-stop-silent-cmd 890,33217
-(defcustom proof-shell-silent-threshold 899,33552
-(defcustom  proof-shell-inform-file-processed-cmd 907,33886
-(defcustom  proof-shell-inform-file-retracted-cmd 928,34814
-(defcustom proof-auto-multiple-files 956,36086
-(defcustom proof-cannot-reopen-processed-files 971,36807
-(defcustom proof-shell-require-command-regexp 985,37473
-(defcustom proof-done-advancing-require-function 996,37935
-(defcustom proof-shell-annotated-prompt-regexp 1008,38295
-(defcustom proof-shell-error-regexp 1023,38860
-(defcustom proof-shell-truncate-before-error 1043,39662
-(defcustom pg-next-error-regexp 1057,40201
-(defcustom pg-next-error-filename-regexp 1072,40810
-(defcustom pg-next-error-extract-filename 1096,41843
-(defcustom proof-shell-interrupt-regexp 1103,42086
-(defcustom proof-shell-proof-completed-regexp 1117,42681
-(defcustom proof-shell-clear-response-regexp 1130,43189
-(defcustom proof-shell-clear-goals-regexp 1142,43641
-(defcustom proof-shell-start-goals-regexp 1154,44087
-(defcustom proof-shell-end-goals-regexp 1162,44454
-(defcustom proof-shell-eager-annotation-start 1176,45027
-(defcustom proof-shell-eager-annotation-start-length 1199,46046
-(defcustom proof-shell-eager-annotation-end 1210,46472
-(defcustom proof-shell-strip-output-markup 1226,47147
-(defcustom proof-shell-assumption-regexp 1235,47532
-(defcustom proof-shell-process-file 1245,47936
-(defcustom proof-shell-retract-files-regexp 1271,49012
-(defcustom proof-shell-compute-new-files-list 1284,49500
-(defcustom pg-special-char-regexp 1299,50067
-(defcustom proof-shell-set-elisp-variable-regexp 1304,50211
-(defcustom proof-shell-match-pgip-cmd 1342,51877
-(defcustom proof-shell-issue-pgip-cmd 1356,52359
-(defcustom proof-use-pgip-askprefs 1361,52524
-(defcustom proof-shell-query-dependencies-cmd 1369,52871
-(defcustom proof-shell-theorem-dependency-list-regexp 1376,53131
-(defcustom proof-shell-theorem-dependency-list-split 1392,53791
-(defcustom proof-shell-show-dependency-cmd 1401,54214
-(defcustom proof-shell-trace-output-regexp 1423,55120
-(defcustom proof-shell-thms-output-regexp 1441,55714
-(defcustom proof-tokens-activate-command 1454,56097
-(defcustom proof-tokens-deactivate-command 1461,56337
-(defcustom proof-tokens-extra-modes 1468,56582
-(defcustom proof-shell-unicode 1483,57087
-(defcustom proof-shell-filename-escapes 1492,57477
-(defcustom proof-shell-process-connection-type 1509,58157
-(defcustom proof-shell-strip-crs-from-input 1515,58348
-(defcustom proof-shell-strip-crs-from-output 1527,58831
-(defcustom proof-shell-insert-hook 1535,59199
-(defcustom proof-script-preprocess 1576,61159
-(defcustom proof-shell-handle-delayed-output-hook1582,61310
-(defcustom proof-shell-handle-error-or-interrupt-hook1588,61525
-(defcustom proof-shell-pre-interrupt-hook1606,62271
-(defcustom proof-shell-handle-output-system-specific 1614,62542
-(defcustom proof-state-change-hook 1637,63515
-(defcustom proof-shell-syntax-table-entries 1647,63908
-(defgroup proof-goals 1665,64279
-(defcustom pg-subterm-first-special-char 1670,64400
-(defcustom pg-subterm-anns-use-stack 1678,64712
-(defcustom pg-goals-change-goal 1687,65011
-(defcustom pbp-goal-command 1692,65127
-(defcustom pbp-hyp-command 1697,65283
-(defcustom pg-subterm-help-cmd 1702,65445
-(defcustom pg-goals-error-regexp 1709,65681
-(defcustom proof-shell-result-start 1714,65841
-(defcustom proof-shell-result-end 1720,66075
-(defcustom pg-subterm-start-char 1726,66288
-(defcustom pg-subterm-sep-char 1737,66762
-(defcustom pg-subterm-end-char 1743,66941
-(defcustom pg-topterm-regexp 1749,67098
-(defcustom proof-goals-font-lock-keywords 1764,67698
-(defcustom proof-response-font-lock-keywords 1772,68057
-(defcustom proof-shell-font-lock-keywords 1780,68419
-(defcustom pg-before-fontify-output-hook 1791,68933
-(defcustom pg-after-fontify-output-hook 1799,69294
+generic/proof-config.el,7852
+(defgroup prover-config 80,2632
+(defcustom proof-guess-command-line 98,3482
+(defcustom proof-assistant-home-page 113,3977
+(defcustom proof-context-command 119,4147
+(defcustom proof-info-command 124,4281
+(defcustom proof-showproof-command 131,4552
+(defcustom proof-goal-command 136,4688
+(defcustom proof-save-command 144,4985
+(defcustom proof-find-theorems-command 152,5294
+(defcustom proof-query-identifier-command 159,5602
+(defcustom proof-assistant-true-value 173,6291
+(defcustom proof-assistant-false-value 179,6481
+(defcustom proof-assistant-format-int-fn 185,6675
+(defcustom proof-assistant-format-float-fn 192,6924
+(defcustom proof-assistant-format-string-fn 199,7179
+(defcustom proof-assistant-setting-format 206,7446
+(defgroup proof-script 228,8141
+(defcustom proof-terminal-string 233,8271
+(defcustom proof-electric-terminator-noterminator 243,8659
+(defcustom proof-script-sexp-commands 248,8831
+(defcustom proof-script-command-end-regexp 259,9290
+(defcustom proof-script-command-start-regexp 277,10111
+(defcustom proof-script-integral-proofs 288,10574
+(defcustom proof-script-fly-past-comments 303,11230
+(defcustom proof-script-parse-function 308,11401
+(defcustom proof-script-comment-start 326,12046
+(defcustom proof-script-comment-start-regexp 337,12483
+(defcustom proof-script-comment-end 345,12802
+(defcustom proof-script-comment-end-regexp 357,13224
+(defcustom proof-string-start-regexp 365,13537
+(defcustom proof-string-end-regexp 370,13702
+(defcustom proof-case-fold-search 375,13863
+(defcustom proof-save-command-regexp 384,14275
+(defcustom proof-save-with-hole-regexp 389,14385
+(defcustom proof-save-with-hole-result 400,14760
+(defcustom proof-goal-command-regexp 410,15200
+(defcustom proof-goal-with-hole-regexp 418,15487
+(defcustom proof-goal-with-hole-result 430,15930
+(defcustom proof-non-undoables-regexp 439,16304
+(defcustom proof-nested-undo-regexp 450,16759
+(defcustom proof-ignore-for-undo-count 466,17471
+(defcustom proof-script-imenu-generic-expression 474,17774
+(defcustom proof-goal-command-p 482,18113
+(defcustom proof-really-save-command-p 493,18604
+(defcustom proof-completed-proof-behaviour 502,18911
+(defcustom proof-count-undos-fn 530,20260
+(defcustom proof-find-and-forget-fn 542,20811
+(defcustom proof-forget-id-command 559,21520
+(defcustom pg-topterm-goalhyplit-fn 569,21878
+(defcustom proof-kill-goal-command 581,22413
+(defcustom proof-undo-n-times-cmd 595,22917
+(defcustom proof-nested-goals-history-p 609,23454
+(defcustom proof-arbitrary-undo-positions 618,23791
+(defcustom proof-state-preserving-p 632,24372
+(defcustom proof-activate-scripting-hook 642,24844
+(defcustom proof-deactivate-scripting-hook 661,25625
+(defcustom proof-script-evaluate-elisp-comment-regexp 670,25955
+(defcustom proof-indent 688,26541
+(defcustom proof-indent-hang 693,26648
+(defcustom proof-indent-enclose-offset 698,26774
+(defcustom proof-indent-open-offset 703,26916
+(defcustom proof-indent-close-offset 708,27053
+(defcustom proof-indent-any-regexp 713,27191
+(defcustom proof-indent-inner-regexp 718,27351
+(defcustom proof-indent-enclose-regexp 723,27505
+(defcustom proof-indent-open-regexp 728,27659
+(defcustom proof-indent-close-regexp 733,27811
+(defcustom proof-script-font-lock-keywords 739,27965
+(defcustom proof-script-syntax-table-entries 747,28317
+(defcustom proof-script-span-context-menu-extensions 765,28713
+(defgroup proof-shell 791,29473
+(defcustom proof-prog-name 801,29643
+(defcustom proof-shell-auto-terminate-commands 812,30063
+(defcustom proof-shell-pre-sync-init-cmd 821,30468
+(defcustom proof-shell-init-cmd 835,31026
+(defcustom proof-shell-init-hook 847,31572
+(defcustom proof-shell-restart-cmd 852,31711
+(defcustom proof-shell-quit-cmd 857,31866
+(defcustom proof-shell-quit-timeout 862,32033
+(defcustom proof-shell-cd-cmd 871,32424
+(defcustom proof-shell-start-silent-cmd 888,33095
+(defcustom proof-shell-stop-silent-cmd 897,33471
+(defcustom proof-shell-silent-threshold 906,33806
+(defcustom  proof-shell-inform-file-processed-cmd 914,34140
+(defcustom  proof-shell-inform-file-retracted-cmd 935,35068
+(defcustom proof-auto-multiple-files 963,36340
+(defcustom proof-cannot-reopen-processed-files 978,37061
+(defcustom proof-shell-require-command-regexp 992,37727
+(defcustom proof-done-advancing-require-function 1003,38189
+(defcustom proof-shell-annotated-prompt-regexp 1015,38549
+(defcustom proof-shell-error-regexp 1030,39114
+(defcustom proof-shell-truncate-before-error 1050,39916
+(defcustom pg-next-error-regexp 1064,40455
+(defcustom pg-next-error-filename-regexp 1079,41064
+(defcustom pg-next-error-extract-filename 1103,42097
+(defcustom proof-shell-interrupt-regexp 1110,42340
+(defcustom proof-shell-proof-completed-regexp 1124,42935
+(defcustom proof-shell-clear-response-regexp 1137,43443
+(defcustom proof-shell-clear-goals-regexp 1149,43895
+(defcustom proof-shell-start-goals-regexp 1161,44341
+(defcustom proof-shell-end-goals-regexp 1169,44708
+(defcustom proof-shell-eager-annotation-start 1183,45281
+(defcustom proof-shell-eager-annotation-start-length 1206,46300
+(defcustom proof-shell-eager-annotation-end 1217,46726
+(defcustom proof-shell-strip-output-markup 1233,47401
+(defcustom proof-shell-assumption-regexp 1242,47786
+(defcustom proof-shell-process-file 1252,48190
+(defcustom proof-shell-retract-files-regexp 1278,49266
+(defcustom proof-shell-compute-new-files-list 1291,49754
+(defcustom pg-special-char-regexp 1306,50321
+(defcustom proof-shell-set-elisp-variable-regexp 1311,50465
+(defcustom proof-shell-match-pgip-cmd 1349,52131
+(defcustom proof-shell-issue-pgip-cmd 1363,52613
+(defcustom proof-use-pgip-askprefs 1368,52778
+(defcustom proof-shell-query-dependencies-cmd 1376,53125
+(defcustom proof-shell-theorem-dependency-list-regexp 1383,53385
+(defcustom proof-shell-theorem-dependency-list-split 1399,54045
+(defcustom proof-shell-show-dependency-cmd 1408,54468
+(defcustom proof-shell-trace-output-regexp 1430,55374
+(defcustom proof-shell-thms-output-regexp 1448,55968
+(defcustom proof-tokens-activate-command 1461,56351
+(defcustom proof-tokens-deactivate-command 1468,56591
+(defcustom proof-tokens-extra-modes 1475,56836
+(defcustom proof-shell-unicode 1490,57341
+(defcustom proof-shell-filename-escapes 1499,57731
+(defcustom proof-shell-process-connection-type 1516,58411
+(defcustom proof-shell-strip-crs-from-input 1522,58602
+(defcustom proof-shell-strip-crs-from-output 1534,59085
+(defcustom proof-shell-extend-queue-hook 1542,59453
+(defcustom proof-shell-insert-hook 1550,59820
+(defcustom proof-script-preprocess 1591,61780
+(defcustom proof-shell-handle-delayed-output-hook1597,61931
+(defcustom proof-shell-handle-error-or-interrupt-hook1603,62146
+(defcustom proof-shell-pre-interrupt-hook1621,62892
+(defcustom proof-shell-handle-output-system-specific 1629,63163
+(defcustom proof-state-change-hook 1652,64136
+(defcustom proof-shell-syntax-table-entries 1662,64529
+(defgroup proof-goals 1680,64900
+(defcustom pg-subterm-first-special-char 1685,65021
+(defcustom pg-subterm-anns-use-stack 1693,65333
+(defcustom pg-goals-change-goal 1702,65632
+(defcustom pbp-goal-command 1707,65748
+(defcustom pbp-hyp-command 1712,65904
+(defcustom pg-subterm-help-cmd 1717,66066
+(defcustom pg-goals-error-regexp 1724,66302
+(defcustom proof-shell-result-start 1729,66462
+(defcustom proof-shell-result-end 1735,66696
+(defcustom pg-subterm-start-char 1741,66909
+(defcustom pg-subterm-sep-char 1752,67383
+(defcustom pg-subterm-end-char 1758,67562
+(defcustom pg-topterm-regexp 1764,67719
+(defcustom proof-goals-font-lock-keywords 1779,68319
+(defcustom proof-response-font-lock-keywords 1787,68678
+(defcustom proof-shell-font-lock-keywords 1795,69040
+(defcustom pg-before-fontify-output-hook 1806,69554
+(defcustom pg-after-fontify-output-hook 1814,69915
 
 generic/proof-depends.el,917
 (defvar proof-thm-names-of-files 25,639
@@ -1454,381 +1487,383 @@ generic/proof-maths-menu.el,83
 (defun proof-maths-menu-set-global 32,906
 (defun proof-maths-menu-enable 46,1357
 
-generic/proof-menu.el,2168
-(defvar proof-display-some-buffers-count 36,816
-(defun proof-display-some-buffers 38,861
-(defun proof-menu-define-keys 95,2988
-(defun proof-menu-define-main 153,5813
-(defvar proof-menu-favourites 162,5998
-(defvar proof-menu-settings 165,6105
-(defun proof-menu-define-specific 169,6194
-(defun proof-assistant-menu-update 212,7456
-(defvar proof-help-menu226,7889
-(defvar proof-show-hide-menu234,8159
-(defvar proof-buffer-menu245,8583
-(defun proof-keep-response-history 308,10899
-(defconst proof-quick-opts-menu316,11209
-(defun proof-quick-opts-vars 534,20115
-(defun proof-quick-opts-changed-from-defaults-p 566,21055
-(defun proof-quick-opts-changed-from-saved-p 570,21160
-(defun proof-set-document-centred 578,21316
-(defun proof-set-non-document-centred 591,21742
-(defun proof-quick-opts-save 610,22453
-(defun proof-quick-opts-reset 615,22621
-(defconst proof-config-menu627,22889
-(defconst proof-advanced-menu634,23068
-(defvar proof-menu652,23752
-(defun proof-main-menu 661,24034
-(defun proof-aux-menu 673,24373
-(defun proof-menu-define-favourites-menu 689,24719
-(defun proof-def-favourite 709,25368
-(defvar proof-make-favourite-cmd-history 736,26361
-(defvar proof-make-favourite-menu-history 739,26446
-(defun proof-save-favourites 742,26532
-(defun proof-del-favourite 747,26680
-(defun proof-read-favourite 764,27236
-(defun proof-add-favourite 788,28010
-(defun proof-menu-define-settings-menu 815,29055
-(defun proof-menu-entry-name 848,30186
-(defun proof-menu-entry-for-setting 858,30536
-(defun proof-settings-vars 877,31068
-(defun proof-settings-changed-from-defaults-p 882,31245
-(defun proof-settings-changed-from-saved-p 886,31351
-(defun proof-settings-save 890,31454
-(defun proof-settings-reset 895,31621
-(defun proof-assistant-invisible-command-ifposs 900,31784
-(defun proof-maybe-askprefs 922,32754
-(defun proof-assistant-settings-cmd 928,32947
-(defun proof-assistant-settings-cmds 936,33231
-(defvar proof-assistant-format-table946,33573
-(defun proof-assistant-format-bool 954,33943
-(defun proof-assistant-format-int 957,34056
-(defun proof-assistant-format-string 960,34148
-(defun proof-assistant-format 963,34246
+generic/proof-menu.el,2215
+(defvar proof-display-some-buffers-count 36,815
+(defun proof-display-some-buffers 38,860
+(defun proof-menu-define-keys 95,2987
+(defun proof-menu-define-main 153,5812
+(defvar proof-menu-favourites 162,5997
+(defvar proof-menu-settings 165,6104
+(defun proof-menu-define-specific 169,6193
+(defun proof-assistant-menu-update 212,7455
+(defvar proof-help-menu226,7888
+(defvar proof-show-hide-menu234,8158
+(defvar proof-buffer-menu245,8582
+(defun proof-keep-response-history 308,10898
+(defconst proof-quick-opts-menu316,11208
+(defun proof-quick-opts-vars 534,20114
+(defun proof-quick-opts-changed-from-defaults-p 566,21054
+(defun proof-quick-opts-changed-from-saved-p 570,21159
+(defun proof-set-document-centred 578,21315
+(defun proof-set-non-document-centred 591,21741
+(defun proof-quick-opts-save 610,22452
+(defun proof-quick-opts-reset 615,22620
+(defconst proof-config-menu627,22888
+(defconst proof-advanced-menu634,23067
+(defvar proof-menu652,23751
+(defun proof-main-menu 661,24033
+(defun proof-aux-menu 673,24372
+(defun proof-menu-define-favourites-menu 689,24718
+(defun proof-def-favourite 709,25367
+(defvar proof-make-favourite-cmd-history 736,26360
+(defvar proof-make-favourite-menu-history 739,26445
+(defun proof-save-favourites 742,26531
+(defun proof-del-favourite 747,26679
+(defun proof-read-favourite 764,27235
+(defun proof-add-favourite 788,28009
+(defun proof-menu-define-settings-menu 815,29054
+(defun proof-menu-entry-name 848,30185
+(defun proof-menu-entry-for-setting 858,30535
+(defun proof-settings-vars 881,31172
+(defun proof-settings-changed-from-defaults-p 886,31349
+(defun proof-settings-changed-from-saved-p 890,31455
+(defun proof-settings-save 894,31558
+(defun proof-settings-reset 899,31725
+(defun proof-assistant-invisible-command-ifposs 904,31888
+(defun proof-maybe-askprefs 926,32858
+(defun proof-assistant-settings-cmd 932,33051
+(defun proof-assistant-settings-cmds 940,33335
+(defvar proof-assistant-format-table950,33677
+(defun proof-assistant-format-bool 959,34103
+(defun proof-assistant-format-int 962,34216
+(defun proof-assistant-format-float 965,34308
+(defun proof-assistant-format-string 968,34404
+(defun proof-assistant-format 971,34502
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 43,1439
 (defun proof-mmm-enable 58,1978
 
-generic/proof-script.el,5496
-(deflocal proof-active-buffer-fake-minor-mode 46,1414
-(deflocal proof-script-buffer-file-name 49,1540
-(deflocal pg-script-portions 56,1950
-(defun proof-next-element-count 66,2170
-(defun proof-element-id 72,2412
-(defun proof-next-element-id 76,2581
-(deflocal proof-locked-span 112,3885
-(deflocal proof-queue-span 119,4151
-(deflocal proof-overlay-arrow 128,4637
-(defun proof-span-give-warning 134,4764
-(defun proof-span-read-only 140,4944
-(defun proof-strict-read-only 149,5317
-(defsubst proof-set-queue-endpoints 159,5695
-(defun proof-set-overlay-arrow 163,5836
-(defsubst proof-set-locked-endpoints 174,6174
-(defsubst proof-detach-queue 179,6350
-(defsubst proof-detach-locked 184,6489
-(defsubst proof-set-queue-start 191,6714
-(defsubst proof-set-locked-end 195,6840
-(defsubst proof-set-queue-end 207,7310
-(defun proof-init-segmentation 218,7607
-(defun proof-colour-locked 248,8858
-(defun proof-colour-locked-span 255,9131
-(defun proof-sticky-errors 261,9404
-(defun proof-restart-buffers 274,9820
-(defun proof-script-buffers-with-spans 296,10639
-(defun proof-script-remove-all-spans-and-deactivate 306,10995
-(defun proof-script-clear-queue-spans-on-error 310,11185
-(defun proof-script-delete-spans 336,12202
-(defun proof-script-delete-secondary-spans 341,12401
-(defun proof-unprocessed-begin 354,12690
-(defun proof-script-end 362,12944
-(defun proof-queue-or-locked-end 371,13254
-(defun proof-locked-region-full-p 390,13847
-(defun proof-locked-region-empty-p 399,14119
-(defun proof-only-whitespace-to-locked-region-p 403,14269
-(defun proof-in-locked-region-p 413,14618
-(defun proof-goto-end-of-locked 425,14875
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 442,15634
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 453,16115
-(defun proof-end-of-locked-visible-p 465,16655
-(defconst pg-idioms 484,17248
-(defconst pg-all-idioms 487,17344
-(defun pg-clear-script-portions 491,17465
-(defun pg-remove-element 497,17700
-(defun pg-get-element 505,18003
-(defun pg-add-element 515,18318
-(defun pg-invisible-prop 563,20297
-(defun pg-set-element-span-invisible 568,20498
-(defun pg-toggle-element-span-visibility 581,21064
-(defun pg-open-invisible-span 586,21225
-(defun pg-make-element-invisible 591,21396
-(defun pg-make-element-visible 596,21607
-(defun pg-toggle-element-visibility 601,21801
-(defun pg-show-all-portions 607,22064
-(defun pg-show-all-proofs 626,22772
-(defun pg-hide-all-proofs 631,22900
-(defun pg-add-proof-element 636,23031
-(defun pg-span-name 651,23818
-(defvar pg-span-context-menu-keymap684,25025
-(defun pg-last-output-displayform 691,25263
-(defun pg-set-span-helphighlights 714,26154
-(defun proof-complete-buffer-atomic 772,28131
-(defun proof-register-possibly-new-processed-file801,29401
-(defun proof-query-save-this-buffer-p 847,31275
-(defun proof-inform-prover-file-retracted 852,31500
-(defun proof-auto-retract-dependencies 872,32351
-(defun proof-unregister-buffer-file-name 926,34901
-(defun proof-protected-process-or-retract 972,36726
-(defun proof-deactivate-scripting-auto 999,37896
-(defun proof-deactivate-scripting 1008,38254
-(defun proof-activate-scripting 1138,43398
-(defun proof-toggle-active-scripting 1239,47918
-(defun proof-done-advancing 1278,49163
-(defun proof-done-advancing-comment 1357,52148
-(defun proof-done-advancing-save 1391,53534
-(defun proof-make-goalsave1479,56898
-(defun proof-get-name-from-goal 1497,57763
-(defun proof-done-advancing-autosave 1517,58788
-(defun proof-done-advancing-other 1581,61284
-(defun proof-segment-up-to-parser 1610,62248
-(defun proof-script-generic-parse-find-comment-end 1679,64514
-(defun proof-script-generic-parse-cmdend 1688,64928
-(defun proof-script-generic-parse-cmdstart 1739,66824
-(defun proof-script-generic-parse-sexp 1778,68424
-(defun proof-semis-to-vanillas 1790,68890
-(defun proof-next-command-new-line 1843,70563
-(defun proof-script-next-command-advance 1848,70769
-(defun proof-assert-until-point 1867,71269
-(defun proof-assert-electric-terminator 1882,71896
-(defun proof-assert-semis 1925,73528
-(defun proof-retract-before-change 1939,74269
-(defun proof-insert-pbp-command 1959,74865
-(defun proof-insert-sendback-command 1974,75368
-(defun proof-done-retracting 2000,76271
-(defun proof-setup-retract-action 2035,77725
-(defun proof-last-goal-or-goalsave 2047,78330
-(defun proof-retract-target 2071,79242
-(defun proof-retract-until-point-interactive 2150,82495
-(defun proof-retract-until-point 2159,82902
-(define-derived-mode proof-mode 2214,84910
-(defun proof-script-set-visited-file-name 2250,86292
-(defun proof-script-set-buffer-hooks 2272,87305
-(defun proof-script-kill-buffer-fn 2280,87723
-(defun proof-config-done-related 2312,89040
-(defun proof-generic-goal-command-p 2377,91525
-(defun proof-generic-state-preserving-p 2382,91738
-(defun proof-generic-count-undos 2391,92255
-(defun proof-generic-find-and-forget 2422,93383
-(defconst proof-script-important-settings2473,95155
-(defun proof-config-done 2488,95701
-(defun proof-setup-parsing-mechanism 2555,97866
-(defun proof-setup-imenu 2579,98938
-(deflocal proof-segment-up-to-cache 2606,99716
-(deflocal proof-segment-up-to-cache-start 2607,99757
-(deflocal proof-last-edited-low-watermark 2608,99802
-(defun proof-segment-up-to-using-cache 2618,100289
-(defun proof-segment-cache-contents-for 2650,101534
-(defun proof-script-after-change-function 2662,101903
-(defun proof-script-set-after-change-functions 2674,102410
+generic/proof-script.el,5553
+(deflocal proof-active-buffer-fake-minor-mode 46,1413
+(deflocal proof-script-buffer-file-name 49,1539
+(deflocal pg-script-portions 56,1949
+(defun proof-next-element-count 66,2169
+(defun proof-element-id 72,2411
+(defun proof-next-element-id 76,2580
+(deflocal proof-locked-span 112,3884
+(deflocal proof-queue-span 119,4150
+(deflocal proof-overlay-arrow 128,4636
+(defun proof-span-give-warning 134,4763
+(defun proof-span-read-only 140,4943
+(defun proof-strict-read-only 149,5316
+(defsubst proof-set-queue-endpoints 159,5694
+(defun proof-set-overlay-arrow 163,5835
+(defsubst proof-set-locked-endpoints 174,6173
+(defsubst proof-detach-queue 179,6349
+(defsubst proof-detach-locked 184,6488
+(defsubst proof-set-queue-start 191,6713
+(defsubst proof-set-locked-end 195,6839
+(defsubst proof-set-queue-end 207,7309
+(defun proof-init-segmentation 218,7606
+(defun proof-colour-locked 248,8857
+(defun proof-colour-locked-span 255,9130
+(defun proof-sticky-errors 261,9403
+(defun proof-restart-buffers 274,9819
+(defun proof-script-buffers-with-spans 296,10638
+(defun proof-script-remove-all-spans-and-deactivate 306,10994
+(defun proof-script-clear-queue-spans-on-error 310,11184
+(defun proof-script-delete-spans 336,12201
+(defun proof-script-delete-secondary-spans 341,12400
+(defun proof-unprocessed-begin 354,12689
+(defun proof-script-end 362,12943
+(defun proof-queue-or-locked-end 371,13253
+(defun proof-locked-region-full-p 390,13846
+(defun proof-locked-region-empty-p 399,14118
+(defun proof-only-whitespace-to-locked-region-p 403,14268
+(defun proof-in-locked-region-p 413,14617
+(defun proof-goto-end-of-locked 425,14874
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 442,15633
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 453,16114
+(defun proof-end-of-locked-visible-p 465,16654
+(defconst pg-idioms 484,17247
+(defconst pg-all-idioms 487,17343
+(defun pg-clear-script-portions 491,17464
+(defun pg-remove-element 497,17699
+(defun pg-get-element 505,18002
+(defun pg-add-element 515,18317
+(defun pg-invisible-prop 563,20294
+(defun pg-set-element-span-invisible 568,20495
+(defun pg-toggle-element-span-visibility 581,21061
+(defun pg-open-invisible-span 586,21222
+(defun pg-make-element-invisible 591,21393
+(defun pg-make-element-visible 596,21604
+(defun pg-toggle-element-visibility 601,21798
+(defun pg-show-all-portions 607,22061
+(defun pg-show-all-proofs 626,22769
+(defun pg-hide-all-proofs 631,22897
+(defun pg-add-proof-element 636,23028
+(defun pg-span-name 651,23815
+(defvar pg-span-context-menu-keymap684,25022
+(defun pg-last-output-displayform 691,25260
+(defun pg-set-span-helphighlights 714,26151
+(defun proof-complete-buffer-atomic 772,28128
+(defun proof-register-possibly-new-processed-file801,29398
+(defun proof-query-save-this-buffer-p 847,31272
+(defun proof-inform-prover-file-retracted 852,31497
+(defun proof-auto-retract-dependencies 872,32348
+(defun proof-unregister-buffer-file-name 926,34898
+(defconst proof-no-fully-processed-buffer 972,36723
+(defun proof-protected-process-or-retract 980,37178
+(defun proof-deactivate-scripting-auto 1007,38348
+(defun proof-deactivate-scripting 1016,38706
+(defun proof-activate-scripting 1159,44398
+(defun proof-toggle-active-scripting 1260,48918
+(defun proof-done-advancing 1299,50163
+(defun proof-done-advancing-comment 1378,53148
+(defun proof-done-advancing-save 1412,54534
+(defun proof-make-goalsave1500,57898
+(defun proof-get-name-from-goal 1518,58763
+(defun proof-done-advancing-autosave 1538,59788
+(defun proof-done-advancing-other 1602,62284
+(defun proof-segment-up-to-parser 1631,63248
+(defun proof-script-generic-parse-find-comment-end 1700,65514
+(defun proof-script-generic-parse-cmdend 1709,65928
+(defun proof-script-generic-parse-cmdstart 1760,67824
+(defun proof-script-generic-parse-sexp 1799,69424
+(defun proof-semis-to-vanillas 1811,69890
+(defun proof-next-command-new-line 1864,71563
+(defun proof-script-next-command-advance 1869,71769
+(defun proof-assert-until-point 1888,72269
+(defun proof-assert-electric-terminator 1903,72896
+(defun proof-assert-semis 1946,74528
+(defun proof-retract-before-change 1960,75269
+(defun proof-insert-pbp-command 1980,75865
+(defun proof-insert-sendback-command 1995,76368
+(defun proof-done-retracting 2021,77271
+(defun proof-setup-retract-action 2056,78725
+(defun proof-last-goal-or-goalsave 2068,79330
+(defun proof-retract-target 2092,80242
+(defun proof-retract-until-point-interactive 2171,83495
+(defun proof-retract-until-point 2180,83902
+(define-derived-mode proof-mode 2235,85910
+(defun proof-script-set-visited-file-name 2271,87292
+(defun proof-script-set-buffer-hooks 2293,88305
+(defun proof-script-kill-buffer-fn 2301,88723
+(defun proof-config-done-related 2333,90040
+(defun proof-generic-goal-command-p 2398,92525
+(defun proof-generic-state-preserving-p 2403,92738
+(defun proof-generic-count-undos 2412,93255
+(defun proof-generic-find-and-forget 2443,94383
+(defconst proof-script-important-settings2494,96155
+(defun proof-config-done 2509,96701
+(defun proof-setup-parsing-mechanism 2576,98866
+(defun proof-setup-imenu 2600,99938
+(deflocal proof-segment-up-to-cache 2627,100716
+(deflocal proof-segment-up-to-cache-start 2628,100757
+(deflocal proof-last-edited-low-watermark 2629,100802
+(defun proof-segment-up-to-using-cache 2639,101289
+(defun proof-segment-cache-contents-for 2667,102291
+(defun proof-script-after-change-function 2679,102660
+(defun proof-script-set-after-change-functions 2691,103167
 
 generic/proof-shell.el,3598
-(defvar proof-marker 34,744
-(defvar proof-action-list 37,840
-(defsubst proof-shell-invoke-callback 57,1594
-(defvar proof-shell-last-goals-output 71,2086
-(defvar proof-shell-last-response-output 74,2166
-(defvar proof-shell-delayed-output-start 77,2253
-(defvar proof-shell-delayed-output-end 81,2435
-(defvar proof-shell-delayed-output-flags 85,2615
-(defvar proof-shell-interrupt-pending 88,2740
-(defcustom proof-shell-active-scripting-indicator99,3035
-(defun proof-shell-ready-prover 151,4619
-(defsubst proof-shell-live-buffer 165,5158
-(defun proof-shell-available-p 172,5397
-(defun proof-grab-lock 178,5619
-(defun proof-release-lock 188,6048
-(defcustom proof-shell-fiddle-frames 198,6222
-(defun proof-shell-set-text-representation 203,6380
-(defun proof-shell-start 211,6708
-(defvar proof-shell-kill-function-hooks 385,12533
-(defun proof-shell-kill-function 388,12631
-(defun proof-shell-clear-state 441,14526
-(defun proof-shell-exit 457,15001
-(defun proof-shell-bail-out 470,15505
-(defun proof-shell-restart 480,16027
-(defvar proof-shell-urgent-message-marker 521,17399
-(defvar proof-shell-urgent-message-scanner 524,17520
-(defun proof-shell-handle-error-output 528,17705
-(defun proof-shell-handle-error-or-interrupt 554,18567
-(defun proof-shell-error-or-interrupt-action 597,20316
-(defun proof-goals-pos 624,21413
-(defun proof-pbp-focus-on-first-goal 629,21624
-(defsubst proof-shell-string-match-safe 641,22040
-(defun proof-shell-handle-immediate-output 645,22201
-(defun proof-interrupt-process 712,24808
-(defun proof-shell-insert 746,26041
-(defun proof-shell-action-list-item 797,27867
-(defun proof-shell-set-silent 802,28109
-(defun proof-shell-start-silent-item 808,28328
-(defun proof-shell-clear-silent 814,28517
-(defun proof-shell-stop-silent-item 820,28739
-(defsubst proof-shell-should-be-silent 826,28928
-(defsubst proof-shell-insert-action-item 837,29438
-(defsubst proof-shell-slurp-comments 841,29613
-(defun proof-add-to-queue 852,30018
-(defun proof-start-queue 910,32042
-(defun proof-extend-queue 921,32436
-(defun proof-shell-exec-loop 935,32904
-(defun proof-shell-insert-loopback-cmd 1003,35207
-(defun proof-shell-process-urgent-message 1028,36371
-(defun proof-shell-process-urgent-message-default 1077,38091
-(defun proof-shell-process-urgent-message-trace 1093,38675
-(defun proof-shell-process-urgent-message-retract 1106,39234
-(defun proof-shell-process-urgent-message-elisp 1127,40082
-(defun proof-shell-process-urgent-message-thmdeps 1142,40577
-(defun proof-shell-strip-eager-annotations 1156,40956
-(defun proof-shell-filter 1172,41456
-(defun proof-shell-filter-first-command 1272,44828
-(defun proof-shell-process-urgent-messages 1287,45371
-(defun proof-shell-filter-manage-output 1337,46937
-(defsubst proof-shell-display-output-as-response 1369,48184
-(defun proof-shell-handle-delayed-output 1375,48479
-(defvar pg-last-tracing-output-time 1470,51938
-(defconst pg-slow-mode-duration 1473,52044
-(defconst pg-fast-tracing-mode-threshold 1476,52126
-(defvar pg-tracing-cleanup-timer 1479,52254
-(defun pg-tracing-tight-loop 1481,52293
-(defun pg-finish-tracing-display 1524,54005
-(defun proof-shell-wait 1542,54369
-(defun proof-done-invisible 1572,55574
-(defun proof-shell-invisible-command 1578,55744
-(defun proof-shell-invisible-cmd-get-result 1625,57336
-(defun proof-shell-invisible-command-invisible-result 1637,57772
-(defun pg-insert-last-output-as-comment 1657,58273
-(define-derived-mode proof-shell-mode 1676,58745
-(defconst proof-shell-important-settings1713,59772
-(defun proof-shell-config-done 1719,59887
+(defvar proof-marker 34,743
+(defvar proof-action-list 37,839
+(defsubst proof-shell-invoke-callback 57,1593
+(defvar proof-shell-last-goals-output 71,2085
+(defvar proof-shell-last-response-output 74,2165
+(defvar proof-shell-delayed-output-start 77,2252
+(defvar proof-shell-delayed-output-end 81,2434
+(defvar proof-shell-delayed-output-flags 85,2614
+(defvar proof-shell-interrupt-pending 88,2739
+(defcustom proof-shell-active-scripting-indicator99,3034
+(defun proof-shell-ready-prover 151,4618
+(defsubst proof-shell-live-buffer 165,5157
+(defun proof-shell-available-p 172,5396
+(defun proof-grab-lock 178,5618
+(defun proof-release-lock 188,6047
+(defcustom proof-shell-fiddle-frames 198,6221
+(defun proof-shell-set-text-representation 203,6379
+(defun proof-shell-start 211,6707
+(defvar proof-shell-kill-function-hooks 385,12532
+(defun proof-shell-kill-function 388,12630
+(defun proof-shell-clear-state 441,14525
+(defun proof-shell-exit 457,15000
+(defun proof-shell-bail-out 470,15504
+(defun proof-shell-restart 480,16026
+(defvar proof-shell-urgent-message-marker 521,17398
+(defvar proof-shell-urgent-message-scanner 524,17519
+(defun proof-shell-handle-error-output 528,17704
+(defun proof-shell-handle-error-or-interrupt 554,18566
+(defun proof-shell-error-or-interrupt-action 597,20315
+(defun proof-goals-pos 624,21412
+(defun proof-pbp-focus-on-first-goal 629,21623
+(defsubst proof-shell-string-match-safe 641,22039
+(defun proof-shell-handle-immediate-output 645,22200
+(defun proof-interrupt-process 712,24807
+(defun proof-shell-insert 746,26040
+(defun proof-shell-action-list-item 797,27866
+(defun proof-shell-set-silent 802,28108
+(defun proof-shell-start-silent-item 808,28327
+(defun proof-shell-clear-silent 814,28516
+(defun proof-shell-stop-silent-item 820,28738
+(defsubst proof-shell-should-be-silent 826,28927
+(defsubst proof-shell-insert-action-item 837,29437
+(defsubst proof-shell-slurp-comments 841,29612
+(defun proof-add-to-queue 852,30017
+(defun proof-start-queue 910,32041
+(defun proof-extend-queue 921,32435
+(defun proof-shell-exec-loop 936,32948
+(defun proof-shell-insert-loopback-cmd 1004,35251
+(defun proof-shell-process-urgent-message 1029,36415
+(defun proof-shell-process-urgent-message-default 1078,38135
+(defun proof-shell-process-urgent-message-trace 1094,38719
+(defun proof-shell-process-urgent-message-retract 1107,39278
+(defun proof-shell-process-urgent-message-elisp 1128,40126
+(defun proof-shell-process-urgent-message-thmdeps 1143,40621
+(defun proof-shell-strip-eager-annotations 1157,41000
+(defun proof-shell-filter 1173,41500
+(defun proof-shell-filter-first-command 1273,44872
+(defun proof-shell-process-urgent-messages 1288,45415
+(defun proof-shell-filter-manage-output 1338,46981
+(defsubst proof-shell-display-output-as-response 1370,48228
+(defun proof-shell-handle-delayed-output 1376,48523
+(defvar pg-last-tracing-output-time 1471,51982
+(defconst pg-slow-mode-duration 1474,52088
+(defconst pg-fast-tracing-mode-threshold 1477,52170
+(defvar pg-tracing-cleanup-timer 1480,52298
+(defun pg-tracing-tight-loop 1482,52337
+(defun pg-finish-tracing-display 1525,54049
+(defun proof-shell-wait 1543,54413
+(defun proof-done-invisible 1573,55618
+(defun proof-shell-invisible-command 1579,55788
+(defun proof-shell-invisible-cmd-get-result 1626,57380
+(defun proof-shell-invisible-command-invisible-result 1638,57816
+(defun pg-insert-last-output-as-comment 1658,58317
+(define-derived-mode proof-shell-mode 1677,58789
+(defconst proof-shell-important-settings1714,59816
+(defun proof-shell-config-done 1720,59931
 
 generic/proof-site.el,665
-(defconst proof-assistant-table-default26,771
-(defconst proof-general-short-version59,1766
-(defconst proof-general-version-year 65,1953
-(defgroup proof-general 72,2106
-(defgroup proof-general-internals 77,2214
-(defun proof-home-directory-fn 90,2602
-(defcustom proof-home-directory101,2974
-(defcustom proof-images-directory110,3340
-(defcustom proof-info-directory116,3542
-(defcustom proof-assistant-table145,4519
-(defcustom proof-assistants 182,5687
-(defun proof-ready-for-assistant 211,6841
-(defvar proof-general-configured-provers 263,9133
-(defun proof-chose-prover 333,11656
-(defun proofgeneral 338,11788
-(defun proof-visit-example-file 347,12106
+(defconst proof-assistant-table-default26,770
+(defconst proof-general-short-version59,1765
+(defconst proof-general-version-year 65,1952
+(defgroup proof-general 72,2105
+(defgroup proof-general-internals 77,2213
+(defun proof-home-directory-fn 90,2601
+(defcustom proof-home-directory101,2973
+(defcustom proof-images-directory110,3339
+(defcustom proof-info-directory116,3541
+(defcustom proof-assistant-table145,4518
+(defcustom proof-assistants 182,5686
+(defun proof-ready-for-assistant 211,6840
+(defvar proof-general-configured-provers 263,9132
+(defun proof-chose-prover 333,11655
+(defun proofgeneral 338,11787
+(defun proof-visit-example-file 347,12105
 
 generic/proof-splash.el,991
-(defcustom proof-splash-enable 34,1008
-(defcustom proof-splash-time 39,1160
-(defcustom proof-splash-contents47,1444
-(defconst proof-splash-startup-msg91,3009
-(defconst proof-splash-welcome 100,3387
-(define-derived-mode proof-splash-mode 103,3491
-(define-key proof-splash-mode-map 109,3665
-(define-key proof-splash-mode-map 110,3717
-(defsubst proof-emacs-imagep 115,3844
-(defun proof-get-image 120,3969
-(defvar proof-splash-timeout-conf 142,4769
-(defun proof-splash-centre-spaces 145,4882
-(defun proof-splash-remove-screen 172,6038
-(defun proof-splash-remove-buffer 189,6694
-(defvar proof-splash-seen 200,7082
-(defun proof-splash-insert-contents 203,7184
-(defun proof-splash-display-screen 243,8314
-(defalias 'pg-about pg-about
279,9836
-(defun proof-splash-message 282,9902
-(defun proof-splash-timeout-waiter 295,10346
-(defvar proof-splash-old-frame-title-format 308,10904
-(defun proof-splash-set-frame-titles 310,10954
-(defun proof-splash-unset-frame-titles 319,11269
+(defcustom proof-splash-enable 34,1007
+(defcustom proof-splash-time 39,1159
+(defcustom proof-splash-contents47,1443
+(defconst proof-splash-startup-msg91,3008
+(defconst proof-splash-welcome 100,3386
+(define-derived-mode proof-splash-mode 103,3490
+(define-key proof-splash-mode-map 109,3664
+(define-key proof-splash-mode-map 110,3716
+(defsubst proof-emacs-imagep 115,3843
+(defun proof-get-image 120,3968
+(defvar proof-splash-timeout-conf 142,4768
+(defun proof-splash-centre-spaces 145,4881
+(defun proof-splash-remove-screen 172,6037
+(defun proof-splash-remove-buffer 189,6693
+(defvar proof-splash-seen 200,7081
+(defun proof-splash-insert-contents 203,7183
+(defun proof-splash-display-screen 243,8313
+(defalias 'pg-about pg-about
279,9835
+(defun proof-splash-message 282,9901
+(defun proof-splash-timeout-waiter 295,10345
+(defvar proof-splash-old-frame-title-format 308,10903
+(defun proof-splash-set-frame-titles 310,10953
+(defun proof-splash-unset-frame-titles 319,11268
 
 generic/proof-syntax.el,1278
-(defsubst proof-ids-to-regexp 22,517
-(defsubst proof-anchor-regexp 29,755
-(defconst proof-no-regexp 33,860
-(defsubst proof-regexp-alt 36,951
-(defsubst proof-regexp-alt-list 45,1263
-(defsubst proof-re-search-forward-region 49,1398
-(defsubst proof-search-forward 62,1896
-(defsubst proof-replace-regexp-in-string 69,2166
-(defsubst proof-re-search-forward 74,2417
-(defsubst proof-re-search-backward 79,2675
-(defsubst proof-re-search-forward-safe 84,2936
-(defsubst proof-string-match 90,3217
-(defsubst proof-string-match-safe 95,3446
-(defsubst proof-stringfn-match 99,3650
-(defsubst proof-looking-at 106,3913
-(defsubst proof-looking-at-safe 111,4100
-(defun proof-buffer-syntactic-context 120,4313
-(defsubst proof-looking-at-syntactic-context-default 141,5175
-(defun proof-looking-at-syntactic-context 150,5530
-(defun proof-inside-comment 159,5992
-(defun proof-inside-string 165,6165
-(defsubst proof-replace-string 175,6364
-(defsubst proof-replace-regexp 180,6568
-(defsubst proof-replace-regexp-nocasefold 185,6777
-(defvar proof-id 195,7065
-(defsubst proof-ids 201,7285
-(defun proof-zap-commas 208,7537
-(defadvice font-lock-fontify-keywords-region234,8423
-(defun proof-format 250,9019
-(defun proof-format-filename 269,9658
-(defun proof-insert 316,11060
+(defsubst proof-ids-to-regexp 22,516
+(defsubst proof-anchor-regexp 29,754
+(defconst proof-no-regexp 33,859
+(defsubst proof-regexp-alt 36,950
+(defsubst proof-regexp-alt-list 45,1262
+(defsubst proof-re-search-forward-region 49,1397
+(defsubst proof-search-forward 62,1895
+(defsubst proof-replace-regexp-in-string 69,2165
+(defsubst proof-re-search-forward 74,2416
+(defsubst proof-re-search-backward 79,2674
+(defsubst proof-re-search-forward-safe 84,2935
+(defsubst proof-string-match 90,3216
+(defsubst proof-string-match-safe 95,3445
+(defsubst proof-stringfn-match 99,3649
+(defsubst proof-looking-at 106,3912
+(defsubst proof-looking-at-safe 111,4099
+(defun proof-buffer-syntactic-context 120,4312
+(defsubst proof-looking-at-syntactic-context-default 141,5174
+(defun proof-looking-at-syntactic-context 150,5529
+(defun proof-inside-comment 159,5991
+(defun proof-inside-string 165,6164
+(defsubst proof-replace-string 175,6363
+(defsubst proof-replace-regexp 180,6567
+(defsubst proof-replace-regexp-nocasefold 185,6776
+(defvar proof-id 195,7064
+(defsubst proof-ids 201,7284
+(defun proof-zap-commas 208,7536
+(defadvice font-lock-fontify-keywords-region234,8422
+(defun proof-format 250,9018
+(defun proof-format-filename 269,9657
+(defun proof-insert 316,11059
 
 generic/proof-toolbar.el,2332
-(defun proof-toolbar-function 33,813
-(defun proof-toolbar-icon 37,960
-(defun proof-toolbar-enabler 41,1107
-(defun proof-toolbar-make-icon 50,1309
-(defun proof-toolbar-make-toolbar-items 59,1617
-(defvar proof-toolbar-map 85,2493
-(defun proof-toolbar-available-p 88,2592
-(defun proof-toolbar-setup 98,2898
-(defun proof-toolbar-enable 119,3755
-(defalias 'proof-toolbar-undo proof-toolbar-undo
152,4813
-(defun proof-toolbar-undo-enable-p 154,4881
-(defalias 'proof-toolbar-delete proof-toolbar-delete
161,5039
-(defun proof-toolbar-delete-enable-p 163,5120
-(defalias 'proof-toolbar-home proof-toolbar-home
171,5302
-(defalias 'proof-toolbar-next proof-toolbar-next
175,5369
-(defun proof-toolbar-next-enable-p 177,5440
-(defalias 'proof-toolbar-goto proof-toolbar-goto
183,5556
-(defun proof-toolbar-goto-enable-p 185,5606
-(defalias 'proof-toolbar-retract proof-toolbar-retract
190,5691
-(defun proof-toolbar-retract-enable-p 192,5748
-(defalias 'proof-toolbar-use proof-toolbar-use
198,5867
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
199,5919
-(defalias 'proof-toolbar-restart proof-toolbar-restart
203,6000
-(defalias 'proof-toolbar-goal proof-toolbar-goal
207,6065
-(defalias 'proof-toolbar-qed proof-toolbar-qed
211,6123
-(defun proof-toolbar-qed-enable-p 213,6172
-(defalias 'proof-toolbar-state proof-toolbar-state
221,6334
-(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
222,6377
-(defalias 'proof-toolbar-context proof-toolbar-context
226,6456
-(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
227,6502
-(defalias 'proof-toolbar-command proof-toolbar-command
231,6583
-(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
232,6639
-(defun proof-toolbar-help 236,6744
-(defalias 'proof-toolbar-find proof-toolbar-find
242,6824
-(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
243,6876
-(defalias 'proof-toolbar-info proof-toolbar-info
247,6951
-(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
248,7006
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
252,7104
-(defun proof-toolbar-visibility-enable-p 254,7164
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
259,7278
-(defun proof-toolbar-interrupt-enable-p 260,7339
-(defun proof-toolbar-scripting-menu 268,7492
+(defun proof-toolbar-function 33,812
+(defun proof-toolbar-icon 37,959
+(defun proof-toolbar-enabler 41,1106
+(defun proof-toolbar-make-icon 50,1308
+(defun proof-toolbar-make-toolbar-items 59,1616
+(defvar proof-toolbar-map 85,2492
+(defun proof-toolbar-available-p 88,2591
+(defun proof-toolbar-setup 98,2897
+(defun proof-toolbar-enable 119,3754
+(defalias 'proof-toolbar-undo proof-toolbar-undo
152,4812
+(defun proof-toolbar-undo-enable-p 154,4880
+(defalias 'proof-toolbar-delete proof-toolbar-delete
161,5038
+(defun proof-toolbar-delete-enable-p 163,5119
+(defalias 'proof-toolbar-home proof-toolbar-home
171,5301
+(defalias 'proof-toolbar-next proof-toolbar-next
175,5368
+(defun proof-toolbar-next-enable-p 177,5439
+(defalias 'proof-toolbar-goto proof-toolbar-goto
183,5555
+(defun proof-toolbar-goto-enable-p 185,5605
+(defalias 'proof-toolbar-retract proof-toolbar-retract
190,5690
+(defun proof-toolbar-retract-enable-p 192,5747
+(defalias 'proof-toolbar-use proof-toolbar-use
198,5866
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
199,5918
+(defalias 'proof-toolbar-restart proof-toolbar-restart
203,5999
+(defalias 'proof-toolbar-goal proof-toolbar-goal
207,6064
+(defalias 'proof-toolbar-qed proof-toolbar-qed
211,6122
+(defun proof-toolbar-qed-enable-p 213,6171
+(defalias 'proof-toolbar-state proof-toolbar-state
221,6333
+(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
222,6376
+(defalias 'proof-toolbar-context proof-toolbar-context
226,6455
+(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
227,6501
+(defalias 'proof-toolbar-command proof-toolbar-command
231,6582
+(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
232,6638
+(defun proof-toolbar-help 236,6743
+(defalias 'proof-toolbar-find proof-toolbar-find
242,6823
+(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
243,6875
+(defalias 'proof-toolbar-info proof-toolbar-info
247,6950
+(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
248,7005
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
252,7103
+(defun proof-toolbar-visibility-enable-p 254,7163
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
259,7277
+(defun proof-toolbar-interrupt-enable-p 260,7338
+(defun proof-toolbar-scripting-menu 268,7491
 
 generic/proof-unicode-tokens.el,497
 (defvar proof-unicode-tokens-initialised 31,827
@@ -1843,82 +1878,82 @@ generic/proof-unicode-tokens.el,497
 (defun proof-unicode-tokens-deactivate-prover 140,4819
 
 generic/proof-useropts.el,1575
-(defgroup proof-user-options 21,559
-(defun proof-set-value 29,738
-(defcustom proof-electric-terminator-enable 62,1861
-(defcustom proof-toolbar-enable 74,2393
-(defcustom proof-imenu-enable 80,2566
-(defcustom pg-show-hints 86,2737
-(defcustom proof-shell-quiet-errors 91,2870
-(defcustom proof-trace-output-slow-catchup 98,3141
-(defcustom proof-strict-state-preserving 108,3638
-(defcustom proof-strict-read-only 121,4247
-(defcustom proof-three-window-enable 134,4826
-(defcustom proof-multiple-frames-enable 153,5576
-(defcustom proof-delete-empty-windows 162,5909
-(defcustom proof-shrink-windows-tofit 173,6440
-(defcustom proof-auto-raise-buffers 180,6712
-(defcustom proof-colour-locked 187,6947
-(defcustom proof-sticky-errors 195,7197
-(defcustom proof-query-file-save-when-activating-scripting202,7414
-(defcustom proof-prog-name-ask218,8134
-(defcustom proof-prog-name-guess224,8294
-(defcustom proof-tidy-response232,8559
-(defcustom proof-keep-response-history246,9022
-(defcustom pg-input-ring-size 256,9410
-(defcustom proof-general-debug 261,9562
-(defcustom proof-use-parser-cache 270,9933
-(defcustom proof-follow-mode 277,10189
-(defcustom proof-auto-action-when-deactivating-scripting 301,11366
-(defcustom proof-rsh-command 324,12315
-(defcustom proof-disappearing-proofs 340,12865
-(defcustom proof-full-annotation 345,13026
-(defcustom proof-minibuffer-messages 354,13396
-(defcustom proof-autosend-enable 362,13705
-(defcustom proof-autosend-delay 368,13885
-(defcustom proof-autosend-all 374,14043
-(defcustom proof-fast-process-buffer 379,14212
+(defgroup proof-user-options 21,558
+(defun proof-set-value 29,737
+(defcustom proof-electric-terminator-enable 62,1860
+(defcustom proof-toolbar-enable 74,2392
+(defcustom proof-imenu-enable 80,2565
+(defcustom pg-show-hints 86,2736
+(defcustom proof-shell-quiet-errors 91,2869
+(defcustom proof-trace-output-slow-catchup 98,3140
+(defcustom proof-strict-state-preserving 108,3637
+(defcustom proof-strict-read-only 121,4246
+(defcustom proof-three-window-enable 134,4825
+(defcustom proof-multiple-frames-enable 153,5575
+(defcustom proof-delete-empty-windows 162,5908
+(defcustom proof-shrink-windows-tofit 173,6439
+(defcustom proof-auto-raise-buffers 180,6711
+(defcustom proof-colour-locked 187,6946
+(defcustom proof-sticky-errors 195,7196
+(defcustom proof-query-file-save-when-activating-scripting202,7413
+(defcustom proof-prog-name-ask218,8133
+(defcustom proof-prog-name-guess224,8293
+(defcustom proof-tidy-response232,8558
+(defcustom proof-keep-response-history246,9021
+(defcustom pg-input-ring-size 256,9409
+(defcustom proof-general-debug 261,9561
+(defcustom proof-use-parser-cache 270,9932
+(defcustom proof-follow-mode 277,10186
+(defcustom proof-auto-action-when-deactivating-scripting 301,11363
+(defcustom proof-rsh-command 329,12546
+(defcustom proof-disappearing-proofs 345,13096
+(defcustom proof-full-annotation 350,13257
+(defcustom proof-minibuffer-messages 359,13627
+(defcustom proof-autosend-enable 367,13936
+(defcustom proof-autosend-delay 373,14116
+(defcustom proof-autosend-all 379,14274
+(defcustom proof-fast-process-buffer 384,14443
 
 generic/proof-utils.el,1567
-(defmacro proof-with-current-buffer-if-exists 61,1730
-(defmacro proof-with-script-buffer 70,2107
-(defmacro proof-map-buffers 81,2488
-(defmacro proof-sym 86,2673
-(defsubst proof-try-require 91,2834
-(defun proof-save-some-buffers 104,3165
-(defun proof-save-this-buffer 124,3761
-(defun proof-file-truename 137,4125
-(defun proof-files-to-buffers 141,4307
-(defun proof-buffers-in-mode 149,4546
-(defun pg-save-from-death 163,4996
-(defun proof-define-keys 182,5612
-(defun pg-remove-specials 193,5897
-(defun pg-remove-specials-in-string 203,6233
-(defun proof-safe-split-window-vertically 213,6458
-(defun proof-warn-if-unset 219,6656
-(defun proof-get-window-for-buffer 224,6874
-(defun proof-display-and-keep-buffer 273,9184
-(defun proof-clean-buffer 315,10907
-(defun pg-internal-warning 331,11563
-(defun proof-debug 339,11845
-(defun proof-switch-to-buffer 349,12216
-(defun proof-resize-window-tofit 371,13340
-(defun proof-submit-bug-report 466,17188
-(defun proof-deftoggle-fn 501,18545
-(defmacro proof-deftoggle 516,19211
-(defun proof-defintset-fn 527,19724
-(defmacro proof-defintset 543,20428
-(defun proof-defstringset-fn 550,20807
-(defmacro proof-defstringset 563,21433
-(defun proof-escape-keymap-doc 576,21889
-(defmacro proof-defshortcut 580,22043
-(defmacro proof-definvisible 595,22641
-(defun pg-custom-save-vars 622,23570
-(defun pg-custom-reset-vars 638,24214
-(defun proof-locate-executable 651,24551
-(defun pg-current-word-pos 666,25101
-(defsubst proof-shell-strip-output-markup 711,26756
-(defun proof-minibuffer-message 717,27020
+(defmacro proof-with-current-buffer-if-exists 61,1729
+(defmacro proof-with-script-buffer 70,2106
+(defmacro proof-map-buffers 81,2487
+(defmacro proof-sym 86,2672
+(defsubst proof-try-require 91,2833
+(defun proof-save-some-buffers 104,3164
+(defun proof-save-this-buffer 124,3760
+(defun proof-file-truename 137,4124
+(defun proof-files-to-buffers 141,4306
+(defun proof-buffers-in-mode 149,4545
+(defun pg-save-from-death 163,4995
+(defun proof-define-keys 182,5611
+(defun pg-remove-specials 193,5896
+(defun pg-remove-specials-in-string 203,6232
+(defun proof-safe-split-window-vertically 213,6457
+(defun proof-warn-if-unset 219,6655
+(defun proof-get-window-for-buffer 224,6873
+(defun proof-display-and-keep-buffer 273,9183
+(defun proof-clean-buffer 315,10906
+(defun pg-internal-warning 331,11562
+(defun proof-debug 339,11844
+(defun proof-switch-to-buffer 354,12388
+(defun proof-resize-window-tofit 376,13512
+(defun proof-submit-bug-report 471,17360
+(defun proof-deftoggle-fn 506,18717
+(defmacro proof-deftoggle 521,19383
+(defun proof-defintset-fn 532,19896
+(defmacro proof-defintset 548,20600
+(defun proof-defstringset-fn 555,20979
+(defmacro proof-defstringset 568,21605
+(defun proof-escape-keymap-doc 581,22061
+(defmacro proof-defshortcut 585,22215
+(defmacro proof-definvisible 600,22813
+(defun pg-custom-save-vars 627,23742
+(defun pg-custom-reset-vars 643,24386
+(defun proof-locate-executable 656,24723
+(defun pg-current-word-pos 671,25273
+(defsubst proof-shell-strip-output-markup 716,26928
+(defun proof-minibuffer-message 722,27192
 
 lib/bufhist.el,1257
 (defun bufhist-ring-update 38,1391
@@ -2035,12 +2070,12 @@ lib/maths-menu.el,242
 (define-minor-mode maths-menu-mode352,13101
 
 lib/pg-dev.el,199
-(defconst pg-dev-lisp-font-lock-keywords52,1588
-(defun pg-loadpath 78,2287
-(defun unload-pg 88,2458
-(defun profile-pg 119,3352
-(defun elp-pack-number 148,4379
-(defun pg-bug-references 157,4579
+(defconst pg-dev-lisp-font-lock-keywords52,1587
+(defun pg-loadpath 78,2286
+(defun unload-pg 88,2457
+(defun profile-pg 119,3351
+(defun elp-pack-number 148,4378
+(defun pg-bug-references 157,4578
 
 lib/pg-fontsets.el,209
 (defcustom pg-fontsets-default-fontset 24,722
@@ -2050,10 +2085,10 @@ lib/pg-fontsets.el,209
 (defun pg-fontsets-make-fontsets 57,1840
 
 lib/proof-compat.el,160
-(defvar proof-running-on-win32 32,976
-(defun pg-custom-undeclare-variable 53,1778
-(defmacro save-selected-frame 85,2549
-(defmacro declare-function 147,4461
+(defvar proof-running-on-win32 32,980
+(defun pg-custom-undeclare-variable 53,1782
+(defmacro save-selected-frame 85,2553
+(defmacro declare-function 151,4561
 
 lib/scomint.el,876
 (defface scomint-highlight-input 19,493
@@ -2080,46 +2115,46 @@ lib/scomint.el,876
 (defun scomint-interrupt-process 363,14257
 
 lib/span.el,1510
-(defalias 'span-start span-start
22,610
-(defalias 'span-end span-end
23,648
-(defalias 'span-set-property span-set-property
24,682
-(defalias 'span-property span-property
25,725
-(defalias 'span-make span-make
26,764
-(defalias 'span-detach span-detach
27,800
-(defalias 'span-set-endpoints span-set-endpoints
28,840
-(defalias 'span-buffer span-buffer
29,885
-(defun span-read-only-hook 31,926
-(defsubst span-read-only 36,1116
-(defsubst span-read-write 43,1426
-(defsubst span-write-warning 48,1596
-(defsubst span-lt 59,2120
-(defsubst spans-at-point-prop 64,2264
-(defsubst spans-at-region-prop 73,2455
-(defsubst span-at 83,2721
-(defsubst span-delete 87,2847
-(defsubst span-mapcar-spans 94,3069
-(defsubst span-mapc-spans 98,3244
-(defsubst span-mapcar-spans-inorder 102,3415
-(defun span-at-before 108,3620
-(defsubst prev-span 125,4344
-(defsubst next-span 131,4497
-(defsubst span-live-p 137,4711
-(defsubst span-raise 143,4877
-(defsubst span-string 147,5010
-(defsubst set-span-properties 152,5170
-(defsubst span-find-span 158,5364
-(defsubst span-at-event 166,5676
-(defun fold-spans 172,5873
-(defsubst span-detached-p 186,6406
-(defsubst set-span-face 190,6522
-(defsubst set-span-keymap 194,6620
-(defsubst span-delete-spans 202,6789
-(defsubst span-property-safe 206,6951
-(defsubst span-set-start 210,7088
-(defsubst span-set-end 214,7220
-(defun span-make-self-removing-span 222,7380
-(defun span-delete-self-modification-hook 232,7748
-(defun span-make-modifying-removing-span 237,7922
+(defalias 'span-start span-start
22,609
+(defalias 'span-end span-end
23,647
+(defalias 'span-set-property span-set-property
24,681
+(defalias 'span-property span-property
25,724
+(defalias 'span-make span-make
26,763
+(defalias 'span-detach span-detach
27,799
+(defalias 'span-set-endpoints span-set-endpoints
28,839
+(defalias 'span-buffer span-buffer
29,884
+(defun span-read-only-hook 31,925
+(defsubst span-read-only 36,1115
+(defsubst span-read-write 43,1425
+(defsubst span-write-warning 48,1595
+(defsubst span-lt 59,2119
+(defsubst spans-at-point-prop 64,2263
+(defsubst spans-at-region-prop 73,2454
+(defsubst span-at 83,2720
+(defsubst span-delete 87,2846
+(defsubst span-mapcar-spans 94,3068
+(defsubst span-mapc-spans 98,3243
+(defsubst span-mapcar-spans-inorder 102,3414
+(defun span-at-before 108,3619
+(defsubst prev-span 125,4343
+(defsubst next-span 131,4496
+(defsubst span-live-p 137,4710
+(defsubst span-raise 143,4876
+(defsubst span-string 147,5009
+(defsubst set-span-properties 152,5169
+(defsubst span-find-span 158,5363
+(defsubst span-at-event 166,5675
+(defun fold-spans 172,5872
+(defsubst span-detached-p 186,6405
+(defsubst set-span-face 190,6521
+(defsubst set-span-keymap 194,6619
+(defsubst span-delete-spans 202,6788
+(defsubst span-property-safe 206,6950
+(defsubst span-set-start 210,7087
+(defsubst span-set-end 214,7219
+(defun span-make-self-removing-span 222,7379
+(defun span-delete-self-modification-hook 232,7747
+(defun span-make-modifying-removing-span 237,7921
 
 lib/texi-docstring-magic.el,584
 (defun texi-docstring-magic-find-face 88,3027
@@ -2140,527 +2175,527 @@ lib/unicode-chars.el,80
 (defun unicode-chars-list-chars 5051,245975
 
 lib/unicode-tokens.el,5900
-(defgroup unicode-tokens-options 55,1712
-(defcustom unicode-tokens-add-help-echo 60,1837
-(defun unicode-tokens-toggle-add-help-echo 65,2004
-(defvar unicode-tokens-token-symbol-map 79,2410
-(defvar unicode-tokens-token-format 98,3069
-(defvar unicode-tokens-token-variant-format-regexp 104,3318
-(defvar unicode-tokens-shortcut-alist 118,3851
-(defvar unicode-tokens-shortcut-replacement-alist 124,4128
-(defvar unicode-tokens-control-region-format-regexp 132,4334
-(defvar unicode-tokens-control-char-format-regexp 139,4702
-(defvar unicode-tokens-control-regions 146,5063
-(defvar unicode-tokens-control-characters 149,5139
-(defvar unicode-tokens-control-char-format 152,5221
-(defvar unicode-tokens-control-region-format-start 155,5334
-(defvar unicode-tokens-control-region-format-end 158,5451
-(defvar unicode-tokens-tokens-customizable-variables 161,5564
-(defconst unicode-tokens-configuration-variables168,5732
-(defun unicode-tokens-config 183,6131
-(defun unicode-tokens-config-var 187,6276
-(defun unicode-tokens-copy-configuration-variables 199,6716
-(defvar unicode-tokens-token-list 227,7932
-(defvar unicode-tokens-hash-table 230,8052
-(defvar unicode-tokens-token-match-regexp 233,8168
-(defvar unicode-tokens-uchar-hash-table 239,8451
-(defvar unicode-tokens-uchar-regexp 243,8638
-(defgroup unicode-tokens-faces 251,8823
-(defconst unicode-tokens-font-family-alternatives261,9120
-(defface unicode-tokens-symbol-font-face276,9617
-(defface unicode-tokens-script-font-face286,9975
-(defface unicode-tokens-fraktur-font-face291,10119
-(defface unicode-tokens-serif-font-face296,10244
-(defface unicode-tokens-sans-font-face301,10381
-(defface unicode-tokens-highlight-face306,10503
-(defconst unicode-tokens-fonts315,10865
-(defconst unicode-tokens-fontsymb-properties324,11082
-(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
352,12698
-(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
370,13250
-(defconst unicode-tokens-font-lock-extra-managed-props383,13581
-(defun unicode-tokens-font-lock-keywords 387,13735
-(defun unicode-tokens-calculate-token-match 420,15106
-(defun unicode-tokens-usable-composition 450,16142
-(defun unicode-tokens-help-echo 463,16521
-(defvar unicode-tokens-show-symbols 468,16723
-(defun unicode-tokens-interpret-composition 471,16837
-(defun unicode-tokens-font-lock-compose-symbol 489,17349
-(defun unicode-tokens-prepend-text-properties-in-match 527,18881
-(defun unicode-tokens-prepend-text-property 541,19459
-(defun unicode-tokens-show-symbols 566,20604
-(defun unicode-tokens-symbs-to-props 574,20914
-(defvar unicode-tokens-show-controls 594,21613
-(defun unicode-tokens-show-controls 597,21704
-(defun unicode-tokens-control-char 609,22217
-(defun unicode-tokens-control-region 618,22656
-(defun unicode-tokens-control-font-lock-keywords 629,23203
-(defvar unicode-tokens-use-shortcuts 640,23527
-(defun unicode-tokens-use-shortcuts 643,23630
-(defun unicode-tokens-map-ordering 659,24226
-(defun unicode-tokens-quail-define-rules 668,24579
-(defun unicode-tokens-insert-token 691,25256
-(defun unicode-tokens-annotate-region 700,25560
-(defun unicode-tokens-insert-control 724,26398
-(defun unicode-tokens-insert-uchar-as-token 734,26847
-(defun unicode-tokens-delete-token-near-point 740,27068
-(defun unicode-tokens-delete-backward-char 752,27509
-(defun unicode-tokens-delete-char 763,27890
-(defun unicode-tokens-delete-backward-1 774,28244
-(defun unicode-tokens-delete-1 791,28840
-(defun unicode-tokens-prev-token 807,29384
-(defun unicode-tokens-rotate-token-forward 815,29681
-(defun unicode-tokens-rotate-token-backward 842,30571
-(defun unicode-tokens-replace-shortcut-match 847,30773
-(defun unicode-tokens-replace-shortcuts 856,31143
-(defun unicode-tokens-replace-unicode-match 870,31741
-(defun unicode-tokens-replace-unicode 877,32042
-(defun unicode-tokens-copy-token 894,32641
-(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32862
-(defun unicode-tokens-list-tokens 907,33066
-(defun unicode-tokens-list-shortcuts 946,34250
-(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34888
-(defun unicode-tokens-encode-in-temp-buffer 966,34961
-(defun unicode-tokens-encode 984,35617
-(defun unicode-tokens-encode-str 990,35853
-(defun unicode-tokens-copy 994,36015
-(defun unicode-tokens-paste 1003,36421
-(defvar unicode-tokens-highlight-unicode 1022,37142
-(defconst unicode-tokens-unicode-highlight-patterns1025,37234
-(defun unicode-tokens-highlight-unicode 1029,37403
-(defun unicode-tokens-highlight-unicode-setkeywords 1041,37866
-(defun unicode-tokens-initialise 1053,38235
-(defvar unicode-tokens-mode-map 1073,38906
-(defvar unicode-tokens-display-table1076,39003
-(define-minor-mode unicode-tokens-mode1083,39254
-(defun unicode-tokens-set-font-var 1219,43807
-(defun unicode-tokens-set-font-var-aux 1235,44296
-(defun unicode-tokens-mouse-set-font 1266,45457
-(defsubst unicode-tokens-face-font-sym 1279,45971
-(defun unicode-tokens-set-font-restart 1283,46151
-(defun unicode-tokens-save-fonts 1294,46461
-(defun unicode-tokens-custom-save-faces 1302,46717
-(define-key unicode-tokens-mode-map1319,47173
-(define-key unicode-tokens-mode-map1322,47280
-(defvar unicode-tokens-quail-translation-keymap1326,47370
-(define-key unicode-tokens-quail-translation-keymap1333,47560
-(defun unicode-tokens-quail-delete-last-char 1337,47694
-(define-key unicode-tokens-mode-map 1352,48121
-(define-key unicode-tokens-mode-map 1354,48213
-(define-key unicode-tokens-mode-map1356,48304
-(define-key unicode-tokens-mode-map1358,48410
-(define-key unicode-tokens-mode-map1361,48525
-(define-key unicode-tokens-mode-map1363,48634
-(define-key unicode-tokens-mode-map1365,48742
-(define-key unicode-tokens-mode-map1367,48848
-(defun unicode-tokens-customize-submenu 1375,48972
-(defun unicode-tokens-define-menu 1382,49195
+(defgroup unicode-tokens-options 55,1711
+(defcustom unicode-tokens-add-help-echo 60,1836
+(defun unicode-tokens-toggle-add-help-echo 65,2003
+(defvar unicode-tokens-token-symbol-map 79,2409
+(defvar unicode-tokens-token-format 98,3068
+(defvar unicode-tokens-token-variant-format-regexp 104,3317
+(defvar unicode-tokens-shortcut-alist 118,3850
+(defvar unicode-tokens-shortcut-replacement-alist 124,4127
+(defvar unicode-tokens-control-region-format-regexp 132,4333
+(defvar unicode-tokens-control-char-format-regexp 139,4701
+(defvar unicode-tokens-control-regions 146,5062
+(defvar unicode-tokens-control-characters 149,5138
+(defvar unicode-tokens-control-char-format 152,5220
+(defvar unicode-tokens-control-region-format-start 155,5333
+(defvar unicode-tokens-control-region-format-end 158,5450
+(defvar unicode-tokens-tokens-customizable-variables 161,5563
+(defconst unicode-tokens-configuration-variables168,5731
+(defun unicode-tokens-config 183,6130
+(defun unicode-tokens-config-var 187,6275
+(defun unicode-tokens-copy-configuration-variables 199,6715
+(defvar unicode-tokens-token-list 227,7931
+(defvar unicode-tokens-hash-table 230,8051
+(defvar unicode-tokens-token-match-regexp 233,8167
+(defvar unicode-tokens-uchar-hash-table 239,8450
+(defvar unicode-tokens-uchar-regexp 243,8637
+(defgroup unicode-tokens-faces 251,8822
+(defconst unicode-tokens-font-family-alternatives261,9119
+(defface unicode-tokens-symbol-font-face276,9616
+(defface unicode-tokens-script-font-face286,9974
+(defface unicode-tokens-fraktur-font-face291,10118
+(defface unicode-tokens-serif-font-face296,10243
+(defface unicode-tokens-sans-font-face301,10380
+(defface unicode-tokens-highlight-face306,10502
+(defconst unicode-tokens-fonts315,10864
+(defconst unicode-tokens-fontsymb-properties324,11081
+(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
352,12697
+(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
370,13249
+(defconst unicode-tokens-font-lock-extra-managed-props383,13580
+(defun unicode-tokens-font-lock-keywords 387,13734
+(defun unicode-tokens-calculate-token-match 420,15105
+(defun unicode-tokens-usable-composition 450,16141
+(defun unicode-tokens-help-echo 463,16520
+(defvar unicode-tokens-show-symbols 468,16722
+(defun unicode-tokens-interpret-composition 471,16836
+(defun unicode-tokens-font-lock-compose-symbol 489,17348
+(defun unicode-tokens-prepend-text-properties-in-match 527,18880
+(defun unicode-tokens-prepend-text-property 541,19458
+(defun unicode-tokens-show-symbols 566,20603
+(defun unicode-tokens-symbs-to-props 574,20913
+(defvar unicode-tokens-show-controls 594,21612
+(defun unicode-tokens-show-controls 597,21703
+(defun unicode-tokens-control-char 609,22216
+(defun unicode-tokens-control-region 618,22655
+(defun unicode-tokens-control-font-lock-keywords 629,23202
+(defvar unicode-tokens-use-shortcuts 640,23526
+(defun unicode-tokens-use-shortcuts 643,23629
+(defun unicode-tokens-map-ordering 659,24225
+(defun unicode-tokens-quail-define-rules 668,24578
+(defun unicode-tokens-insert-token 691,25255
+(defun unicode-tokens-annotate-region 700,25559
+(defun unicode-tokens-insert-control 724,26397
+(defun unicode-tokens-insert-uchar-as-token 734,26846
+(defun unicode-tokens-delete-token-near-point 740,27067
+(defun unicode-tokens-delete-backward-char 752,27508
+(defun unicode-tokens-delete-char 763,27889
+(defun unicode-tokens-delete-backward-1 774,28243
+(defun unicode-tokens-delete-1 791,28839
+(defun unicode-tokens-prev-token 807,29383
+(defun unicode-tokens-rotate-token-forward 815,29680
+(defun unicode-tokens-rotate-token-backward 842,30570
+(defun unicode-tokens-replace-shortcut-match 847,30772
+(defun unicode-tokens-replace-shortcuts 856,31142
+(defun unicode-tokens-replace-unicode-match 870,31740
+(defun unicode-tokens-replace-unicode 877,32041
+(defun unicode-tokens-copy-token 894,32640
+(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32861
+(defun unicode-tokens-list-tokens 907,33065
+(defun unicode-tokens-list-shortcuts 946,34249
+(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34887
+(defun unicode-tokens-encode-in-temp-buffer 966,34960
+(defun unicode-tokens-encode 984,35616
+(defun unicode-tokens-encode-str 990,35852
+(defun unicode-tokens-copy 994,36014
+(defun unicode-tokens-paste 1003,36420
+(defvar unicode-tokens-highlight-unicode 1022,37141
+(defconst unicode-tokens-unicode-highlight-patterns1025,37233
+(defun unicode-tokens-highlight-unicode 1029,37402
+(defun unicode-tokens-highlight-unicode-setkeywords 1041,37865
+(defun unicode-tokens-initialise 1053,38234
+(defvar unicode-tokens-mode-map 1073,38905
+(defvar unicode-tokens-display-table1076,39002
+(define-minor-mode unicode-tokens-mode1083,39253
+(defun unicode-tokens-set-font-var 1219,43806
+(defun unicode-tokens-set-font-var-aux 1235,44295
+(defun unicode-tokens-mouse-set-font 1266,45456
+(defsubst unicode-tokens-face-font-sym 1279,45970
+(defun unicode-tokens-set-font-restart 1283,46150
+(defun unicode-tokens-save-fonts 1294,46460
+(defun unicode-tokens-custom-save-faces 1302,46716
+(define-key unicode-tokens-mode-map1319,47172
+(define-key unicode-tokens-mode-map1322,47279
+(defvar unicode-tokens-quail-translation-keymap1326,47369
+(define-key unicode-tokens-quail-translation-keymap1333,47559
+(defun unicode-tokens-quail-delete-last-char 1337,47693
+(define-key unicode-tokens-mode-map 1352,48120
+(define-key unicode-tokens-mode-map 1354,48212
+(define-key unicode-tokens-mode-map1356,48303
+(define-key unicode-tokens-mode-map1358,48409
+(define-key unicode-tokens-mode-map1361,48524
+(define-key unicode-tokens-mode-map1363,48633
+(define-key unicode-tokens-mode-map1365,48741
+(define-key unicode-tokens-mode-map1367,48847
+(defun unicode-tokens-customize-submenu 1375,48971
+(defun unicode-tokens-define-menu 1382,49194
 
 contrib/mmm/mmm-auto.el,343
-(defvar mmm-autoloaded-classes67,2675
-(defun mmm-autoload-class 89,3438
-(defvar mmm-changed-buffers-list 129,4991
-(defun mmm-major-mode-change 132,5098
-(defun mmm-check-changed-buffers 145,5619
-(defun mmm-mode-on-maybe 154,5969
-(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
166,6373
-(defun mmm-add-find-file-hook 167,6433
+(defvar mmm-autoloaded-classes67,2676
+(defun mmm-autoload-class 89,3439
+(defvar mmm-changed-buffers-list 129,4992
+(defun mmm-major-mode-change 132,5099
+(defun mmm-check-changed-buffers 145,5620
+(defun mmm-mode-on-maybe 154,5970
+(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
166,6374
+(defun mmm-add-find-file-hook 167,6434
 
 contrib/mmm/mmm-class.el,415
-(defun mmm-get-class-spec 42,1295
-(defun mmm-get-class-parameter 59,1938
-(defun mmm-set-class-parameter 63,2104
-(defun* mmm-apply-class75,2454
-(defun* mmm-apply-classes90,3071
-(defun* mmm-apply-all 110,3802
-(defun* mmm-ify124,4249
-(defun* mmm-match-region206,7094
-(defun mmm-match->point 269,9479
-(defun mmm-match-and-verify 284,10049
-(defun mmm-get-form 310,11100
-(defun mmm-default-get-form 321,11575
+(defun mmm-get-class-spec 42,1296
+(defun mmm-get-class-parameter 59,1939
+(defun mmm-set-class-parameter 63,2105
+(defun* mmm-apply-class75,2455
+(defun* mmm-apply-classes90,3072
+(defun* mmm-apply-all 110,3803
+(defun* mmm-ify124,4250
+(defun* mmm-match-region206,7095
+(defun mmm-match->point 269,9480
+(defun mmm-match-and-verify 284,10050
+(defun mmm-get-form 310,11101
+(defun mmm-default-get-form 321,11576
 
 contrib/mmm/mmm-cmds.el,712
-(defun mmm-ify-by-class 41,1209
-(defun mmm-ify-region 63,1821
-(defun mmm-ify-by-regexp75,2242
-(defun mmm-parse-buffer 97,2885
-(defun mmm-parse-region 106,3221
-(defun mmm-parse-block 115,3600
-(defun mmm-get-block 132,4351
-(defun mmm-reparse-current-region 146,4633
-(defun mmm-clear-current-region 167,5209
-(defun mmm-clear-regions 172,5373
-(defun mmm-clear-all-regions 177,5519
-(defun* mmm-end-current-region 185,5679
-(defun mmm-narrow-to-submode-region 220,6927
-(defun mmm-insert-region 239,7541
-(defun mmm-insert-by-key 258,8347
-(defun mmm-get-insertion-spec 342,11612
-(defun mmm-insertion-help 369,12572
-(defun mmm-display-insertion-key 379,12935
-(defun mmm-get-all-insertion-keys 401,13722
+(defun mmm-ify-by-class 41,1210
+(defun mmm-ify-region 63,1822
+(defun mmm-ify-by-regexp75,2243
+(defun mmm-parse-buffer 97,2886
+(defun mmm-parse-region 106,3222
+(defun mmm-parse-block 115,3601
+(defun mmm-get-block 132,4352
+(defun mmm-reparse-current-region 146,4634
+(defun mmm-clear-current-region 167,5210
+(defun mmm-clear-regions 172,5374
+(defun mmm-clear-all-regions 177,5520
+(defun* mmm-end-current-region 185,5680
+(defun mmm-narrow-to-submode-region 220,6928
+(defun mmm-insert-region 239,7542
+(defun mmm-insert-by-key 258,8348
+(defun mmm-get-insertion-spec 342,11613
+(defun mmm-insertion-help 369,12573
+(defun mmm-display-insertion-key 379,12936
+(defun mmm-get-all-insertion-keys 401,13723
 
 contrib/mmm/mmm-compat.el,418
-(defvar mmm-xemacs 40,1312
-(defvar mmm-keywords-used49,1615
-(defmacro mmm-regexp-opt 91,2631
-(defvar mmm-evaporate-property110,3280
-(defmacro mmm-set-keymap-default 128,4046
-(defmacro mmm-event-key 137,4488
-(defvar skeleton-positions 146,4707
-(defun mmm-fixup-skeleton 147,4738
-(defmacro mmm-make-temp-buffer 159,5161
-(defvar mmm-font-lock-available-p 172,5557
-(defmacro mmm-set-font-lock-defaults 179,5771
+(defvar mmm-xemacs 40,1313
+(defvar mmm-keywords-used49,1616
+(defmacro mmm-regexp-opt 91,2632
+(defvar mmm-evaporate-property110,3281
+(defmacro mmm-set-keymap-default 128,4047
+(defmacro mmm-event-key 137,4489
+(defvar skeleton-positions 146,4708
+(defun mmm-fixup-skeleton 147,4739
+(defmacro mmm-make-temp-buffer 159,5162
+(defvar mmm-font-lock-available-p 172,5558
+(defmacro mmm-set-font-lock-defaults 179,5772
 
 contrib/mmm/mmm-cweb.el,228
-(defvar mmm-cweb-section-tags38,1116
-(defvar mmm-cweb-section-regexp41,1163
-(defvar mmm-cweb-c-part-tags44,1253
-(defvar mmm-cweb-c-part-regexp47,1312
-(defun mmm-cweb-in-limbo 50,1396
-(defun mmm-cweb-verify-brief-c 57,1621
+(defvar mmm-cweb-section-tags38,1117
+(defvar mmm-cweb-section-regexp41,1164
+(defvar mmm-cweb-c-part-tags44,1254
+(defvar mmm-cweb-c-part-regexp47,1313
+(defun mmm-cweb-in-limbo 50,1397
+(defun mmm-cweb-verify-brief-c 57,1622
 
 contrib/mmm/mmm-mason.el,410
-(defvar mmm-mason-perl-tags41,1235
-(defvar mmm-mason-pseudo-perl-tags45,1376
-(defvar mmm-mason-non-perl-tags48,1452
-(defvar mmm-mason-perl-tags-regexp51,1553
-(defvar mmm-mason-pseudo-perl-tags-regexp56,1748
-(defvar mmm-mason-tag-names-regexp61,1965
-(defun mmm-mason-verify-inline 66,2185
-(defun mmm-mason-start-line 156,4837
-(defun mmm-mason-end-line 161,4902
-(defun mmm-mason-set-mode-line 168,4996
+(defvar mmm-mason-perl-tags41,1236
+(defvar mmm-mason-pseudo-perl-tags45,1377
+(defvar mmm-mason-non-perl-tags48,1453
+(defvar mmm-mason-perl-tags-regexp51,1554
+(defvar mmm-mason-pseudo-perl-tags-regexp56,1749
+(defvar mmm-mason-tag-names-regexp61,1966
+(defun mmm-mason-verify-inline 66,2186
+(defun mmm-mason-start-line 156,4838
+(defun mmm-mason-end-line 161,4903
+(defun mmm-mason-set-mode-line 168,4997
 
 contrib/mmm/mmm-mode.el,1023
-(defun mmm-mode 101,3866
-(defun mmm-mode-on 140,5371
-(defun mmm-mode-off 181,7047
-(defvar mmm-mode-map 206,7759
-(defvar mmm-mode-prefix-map 209,7834
-(defvar mmm-mode-menu-map 212,7944
-(defun mmm-define-key 215,8035
-(define-key mmm-mode-prefix-map 239,8790
-(define-key mmm-mode-prefix-map 246,9048
-(define-key mmm-mode-map 249,9159
-(define-key mmm-mode-menu-map 252,9261
-(define-key mmm-mode-menu-map 254,9333
-(define-key mmm-mode-menu-map 256,9392
-(define-key mmm-mode-menu-map 258,9473
-(define-key mmm-mode-menu-map 260,9554
-(define-key mmm-mode-menu-map 262,9641
-(define-key mmm-mode-menu-map 265,9735
-(define-key mmm-mode-menu-map 267,9795
-(define-key mmm-mode-menu-map 270,9886
-(define-key mmm-mode-menu-map 272,9946
-(define-key mmm-mode-menu-map 274,10053
-(define-key mmm-mode-menu-map 276,10138
-(define-key mmm-mode-menu-map 279,10224
-(define-key mmm-mode-menu-map 281,10284
-(define-key mmm-mode-menu-map 283,10397
-(define-key mmm-mode-menu-map 285,10482
-(define-key mmm-mode-map 288,10565
+(defun mmm-mode 101,3867
+(defun mmm-mode-on 140,5372
+(defun mmm-mode-off 181,7048
+(defvar mmm-mode-map 206,7760
+(defvar mmm-mode-prefix-map 209,7835
+(defvar mmm-mode-menu-map 212,7945
+(defun mmm-define-key 215,8036
+(define-key mmm-mode-prefix-map 239,8791
+(define-key mmm-mode-prefix-map 246,9049
+(define-key mmm-mode-map 249,9160
+(define-key mmm-mode-menu-map 252,9262
+(define-key mmm-mode-menu-map 254,9334
+(define-key mmm-mode-menu-map 256,9393
+(define-key mmm-mode-menu-map 258,9474
+(define-key mmm-mode-menu-map 260,9555
+(define-key mmm-mode-menu-map 262,9642
+(define-key mmm-mode-menu-map 265,9736
+(define-key mmm-mode-menu-map 267,9796
+(define-key mmm-mode-menu-map 270,9887
+(define-key mmm-mode-menu-map 272,9947
+(define-key mmm-mode-menu-map 274,10054
+(define-key mmm-mode-menu-map 276,10139
+(define-key mmm-mode-menu-map 279,10225
+(define-key mmm-mode-menu-map 281,10285
+(define-key mmm-mode-menu-map 283,10398
+(define-key mmm-mode-menu-map 285,10483
+(define-key mmm-mode-map 288,10566
 
 contrib/mmm/mmm-region.el,1643
-(defsubst mmm-overlay-at 54,1748
-(defun mmm-overlays-at 59,1933
-(defun mmm-included-p 72,2386
-(defun mmm-overlays-containing 112,3875
-(defun mmm-overlays-contained-in 125,4313
-(defun mmm-overlays-overlapping 138,4753
-(defun mmm-sort-overlays 149,5116
-(defvar mmm-current-overlay 158,5358
-(defvar mmm-previous-overlay 163,5573
-(defvar mmm-current-submode 168,5761
-(defvar mmm-previous-submode 173,5961
-(defun mmm-update-current-submode 178,6134
-(defun mmm-set-current-submode 199,6929
-(defun mmm-submode-at 210,7372
-(defun mmm-match-front 219,7647
-(defun mmm-match-back 238,8408
-(defun mmm-front-start 257,9153
-(defun mmm-back-end 265,9457
-(defun mmm-valid-submode-region 278,9804
-(defun* mmm-make-region305,10960
-(defun mmm-make-overlay 431,16310
-(defun mmm-get-face 459,17443
-(defun mmm-clear-overlays 470,17735
-(defun mmm-update-mode-info 486,18200
-(defun mmm-update-submode-region 571,21840
-(defun mmm-add-hooks 588,22570
-(defun mmm-remove-hooks 591,22667
-(defun mmm-get-local-variables-list 597,22794
-(defun mmm-get-locals 617,23490
-(defun mmm-get-saved-local 630,23987
-(defun mmm-set-local-variables 634,24152
-(defun mmm-get-saved-local-variables 645,24530
-(defun mmm-save-changed-local-variables 653,24805
-(defun mmm-clear-local-variables 672,25509
-(defun mmm-enable-font-lock 683,25774
-(defun mmm-update-font-lock-buffer 691,26034
-(defun mmm-refontify-maybe 704,26445
-(defun mmm-submode-changes-in 719,26925
-(defun mmm-regions-in 730,27282
-(defun mmm-regions-alist 744,27760
-(defun mmm-fontify-region 761,28287
-(defun mmm-fontify-region-list 781,29283
-(defun mmm-beginning-of-syntax 803,30031
+(defsubst mmm-overlay-at 54,1749
+(defun mmm-overlays-at 59,1934
+(defun mmm-included-p 72,2387
+(defun mmm-overlays-containing 112,3876
+(defun mmm-overlays-contained-in 125,4314
+(defun mmm-overlays-overlapping 138,4754
+(defun mmm-sort-overlays 149,5117
+(defvar mmm-current-overlay 158,5359
+(defvar mmm-previous-overlay 163,5574
+(defvar mmm-current-submode 168,5762
+(defvar mmm-previous-submode 173,5962
+(defun mmm-update-current-submode 178,6135
+(defun mmm-set-current-submode 199,6930
+(defun mmm-submode-at 210,7373
+(defun mmm-match-front 219,7648
+(defun mmm-match-back 238,8409
+(defun mmm-front-start 257,9154
+(defun mmm-back-end 265,9458
+(defun mmm-valid-submode-region 278,9805
+(defun* mmm-make-region305,10961
+(defun mmm-make-overlay 431,16311
+(defun mmm-get-face 459,17444
+(defun mmm-clear-overlays 470,17736
+(defun mmm-update-mode-info 486,18201
+(defun mmm-update-submode-region 571,21841
+(defun mmm-add-hooks 588,22571
+(defun mmm-remove-hooks 591,22668
+(defun mmm-get-local-variables-list 597,22795
+(defun mmm-get-locals 617,23491
+(defun mmm-get-saved-local 630,23988
+(defun mmm-set-local-variables 634,24153
+(defun mmm-get-saved-local-variables 645,24531
+(defun mmm-save-changed-local-variables 653,24806
+(defun mmm-clear-local-variables 672,25510
+(defun mmm-enable-font-lock 683,25775
+(defun mmm-update-font-lock-buffer 691,26035
+(defun mmm-refontify-maybe 704,26446
+(defun mmm-submode-changes-in 719,26926
+(defun mmm-regions-in 730,27283
+(defun mmm-regions-alist 744,27761
+(defun mmm-fontify-region 761,28288
+(defun mmm-fontify-region-list 781,29284
+(defun mmm-beginning-of-syntax 803,30032
 
 contrib/mmm/mmm-rpm.el,154
-(defconst mmm-rpm-sh-start-tags48,1617
-(defvar mmm-rpm-sh-end-tags53,1841
-(defvar mmm-rpm-sh-start-regexp57,2015
-(defvar mmm-rpm-sh-end-regexp61,2193
+(defconst mmm-rpm-sh-start-tags48,1618
+(defvar mmm-rpm-sh-end-tags53,1842
+(defvar mmm-rpm-sh-start-regexp57,2016
+(defvar mmm-rpm-sh-end-regexp61,2194
 
 contrib/mmm/mmm-sample.el,168
-(defvar mmm-here-doc-mode-alist 84,2600
-(defun mmm-here-doc-get-mode 93,3085
-(defun mmm-file-variables-verify 208,6342
-(defun mmm-file-variables-find-back 232,7147
+(defvar mmm-here-doc-mode-alist 84,2601
+(defun mmm-here-doc-get-mode 93,3086
+(defun mmm-file-variables-verify 208,6343
+(defun mmm-file-variables-find-back 232,7148
 
 contrib/mmm/mmm-univ.el,34
 (defun mmm-univ-get-mode 38,1205
 
 contrib/mmm/mmm-utils.el,282
-(defmacro mmm-valid-buffer 42,1331
-(defmacro mmm-save-all 61,1940
-(defun mmm-format-string 74,2222
-(defun mmm-format-matches 85,2660
-(defmacro mmm-save-keyword 108,3418
-(defmacro mmm-save-keywords 116,3745
-(defun mmm-looking-back-at 129,4243
-(defun mmm-make-marker 146,4783
+(defmacro mmm-valid-buffer 42,1332
+(defmacro mmm-save-all 61,1941
+(defun mmm-format-string 74,2223
+(defun mmm-format-matches 85,2661
+(defmacro mmm-save-keyword 108,3419
+(defmacro mmm-save-keywords 116,3746
+(defun mmm-looking-back-at 129,4244
+(defun mmm-make-marker 146,4784
 
 contrib/mmm/mmm-vars.el,2668
-(defgroup mmm 104,3282
-(defvar mmm-c-derived-modes111,3392
-(defvar mmm-save-local-variables115,3511
-(defvar mmm-buffer-saved-locals 341,10292
-(defvar mmm-region-saved-locals-defaults 346,10492
-(defvar mmm-region-saved-locals-for-dominant 352,10752
-(defgroup mmm-faces 362,11129
-(defcustom mmm-submode-decoration-level 368,11300
-(defface mmm-init-submode-face 386,12144
-(defface mmm-cleanup-submode-face 390,12284
-(defface mmm-declaration-submode-face 394,12421
-(defface mmm-comment-submode-face 398,12567
-(defface mmm-output-submode-face 402,12720
-(defface mmm-special-submode-face 406,12869
-(defface mmm-code-submode-face 410,13033
-(defface mmm-default-submode-face 414,13172
-(defface mmm-delimiter-face 419,13380
-(defcustom mmm-mode-string 426,13506
-(defcustom mmm-submode-mode-line-format 431,13637
-(defvar mmm-primary-mode-display-name 448,14292
-(defvar mmm-buffer-mode-display-name 453,14506
-(defun mmm-set-mode-line 459,14805
-(defvar mmm-classes 483,15613
-(defvar mmm-global-classes 489,15858
-(defcustom mmm-mode-ext-classes-alist 496,16040
-(defun mmm-add-mode-ext-class 515,16830
-(defcustom mmm-major-mode-preferences524,17155
-(defun mmm-add-to-major-mode-preferences 542,17883
-(defun mmm-ensure-modename 558,18641
-(defun mmm-modename->function 567,18944
-(defcustom mmm-delimiter-mode 581,19393
-(defcustom mmm-mode-prefix-key 591,19662
-(defcustom mmm-command-modifiers 596,19789
-(defcustom mmm-insert-modifiers 610,20422
-(defcustom mmm-use-old-command-keys 625,21100
-(defun mmm-use-old-command-keys 635,21564
-(defcustom mmm-mode-hook 643,21756
-(defun mmm-run-constructed-hook 663,22563
-(defun mmm-run-major-hook 671,22907
-(defun mmm-run-submode-hook 674,22984
-(defvar mmm-class-hooks-run 677,23071
-(defun mmm-run-class-hook 682,23243
-(defvar mmm-primary-mode-entry-hook 687,23415
-(defcustom mmm-major-mode-hook 702,24062
-(defun mmm-run-major-mode-hook 716,24693
-(defcustom mmm-global-mode 729,25234
-(defcustom mmm-never-modes745,25901
-(defvar mmm-set-file-name-for-modes 763,26201
-(defvar mmm-mode 774,26560
-(defvar mmm-primary-mode 782,26768
-(defvar mmm-classes-alist 793,27134
-(defun mmm-add-classes 948,35341
-(defun mmm-add-group 953,35506
-(defun mmm-add-to-group 963,35879
-(defconst mmm-version 977,36306
-(defun mmm-version 980,36371
-(defvar mmm-temp-buffer-name 987,36514
-(defvar mmm-interactive-history 993,36644
-(defun mmm-add-to-history 999,36913
-(defun mmm-clear-history 1002,36996
-(defvar mmm-mode-ext-classes 1010,37181
-(defun mmm-get-mode-ext-classes 1015,37392
-(defun mmm-clear-mode-ext-classes 1024,37719
-(defun mmm-mode-ext-applies 1028,37844
-(defun mmm-get-all-classes 1042,38223
+(defgroup mmm 104,3283
+(defvar mmm-c-derived-modes111,3393
+(defvar mmm-save-local-variables115,3512
+(defvar mmm-buffer-saved-locals 341,10293
+(defvar mmm-region-saved-locals-defaults 346,10493
+(defvar mmm-region-saved-locals-for-dominant 352,10753
+(defgroup mmm-faces 362,11130
+(defcustom mmm-submode-decoration-level 368,11301
+(defface mmm-init-submode-face 386,12145
+(defface mmm-cleanup-submode-face 390,12285
+(defface mmm-declaration-submode-face 394,12422
+(defface mmm-comment-submode-face 398,12568
+(defface mmm-output-submode-face 402,12721
+(defface mmm-special-submode-face 406,12870
+(defface mmm-code-submode-face 410,13034
+(defface mmm-default-submode-face 414,13173
+(defface mmm-delimiter-face 419,13381
+(defcustom mmm-mode-string 426,13507
+(defcustom mmm-submode-mode-line-format 431,13638
+(defvar mmm-primary-mode-display-name 448,14293
+(defvar mmm-buffer-mode-display-name 453,14507
+(defun mmm-set-mode-line 459,14806
+(defvar mmm-classes 483,15614
+(defvar mmm-global-classes 489,15859
+(defcustom mmm-mode-ext-classes-alist 496,16041
+(defun mmm-add-mode-ext-class 515,16831
+(defcustom mmm-major-mode-preferences524,17156
+(defun mmm-add-to-major-mode-preferences 542,17884
+(defun mmm-ensure-modename 558,18642
+(defun mmm-modename->function 567,18945
+(defcustom mmm-delimiter-mode 581,19394
+(defcustom mmm-mode-prefix-key 591,19663
+(defcustom mmm-command-modifiers 596,19790
+(defcustom mmm-insert-modifiers 610,20423
+(defcustom mmm-use-old-command-keys 625,21101
+(defun mmm-use-old-command-keys 635,21565
+(defcustom mmm-mode-hook 643,21757
+(defun mmm-run-constructed-hook 663,22564
+(defun mmm-run-major-hook 671,22908
+(defun mmm-run-submode-hook 674,22985
+(defvar mmm-class-hooks-run 677,23072
+(defun mmm-run-class-hook 682,23244
+(defvar mmm-primary-mode-entry-hook 687,23416
+(defcustom mmm-major-mode-hook 702,24063
+(defun mmm-run-major-mode-hook 716,24694
+(defcustom mmm-global-mode 729,25235
+(defcustom mmm-never-modes745,25902
+(defvar mmm-set-file-name-for-modes 763,26202
+(defvar mmm-mode 774,26561
+(defvar mmm-primary-mode 782,26769
+(defvar mmm-classes-alist 793,27135
+(defun mmm-add-classes 948,35342
+(defun mmm-add-group 953,35507
+(defun mmm-add-to-group 963,35880
+(defconst mmm-version 977,36307
+(defun mmm-version 980,36372
+(defvar mmm-temp-buffer-name 987,36515
+(defvar mmm-interactive-history 993,36645
+(defun mmm-add-to-history 999,36914
+(defun mmm-clear-history 1002,36997
+(defvar mmm-mode-ext-classes 1010,37182
+(defun mmm-get-mode-ext-classes 1015,37393
+(defun mmm-clear-mode-ext-classes 1024,37720
+(defun mmm-mode-ext-applies 1028,37845
+(defun mmm-get-all-classes 1042,38224
 
 doc/ProofGeneral.texi,6240
-@node Top161,4917
-@node Preface199,6071
-@node News for Version 4.0News for Version 4.0
222,6660
-@node Future243,7504
-@node Credits272,8839
-@node Introducing Proof GeneralIntroducing Proof General
392,13042
-@node Installing Proof GeneralInstalling Proof General
447,15016
-@node Quick start guideQuick start guide
461,15465
-@node Features of Proof GeneralFeatures of Proof General
505,17586
-@node Supported proof assistantsSupported proof assistants
594,21523
-@node Prerequisites for this manualPrerequisites for this manual
643,23404
-@node Organization of this manualOrganization of this manual
687,25023
-@node Basic Script ManagementBasic Script Management
713,25851
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
732,26451
-@node Proof scriptsProof scripts
995,36579
-@node Script buffersScript buffers
1038,38699
-@node Locked queue and editing regionsLocked queue and editing regions
1060,39276
-@node Goal-save sequencesGoal-save sequences
1116,41423
-@node Active scripting bufferActive scripting buffer
1153,42889
-@node Summary of Proof General buffersSummary of Proof General buffers
1222,46309
-@node Script editing commandsScript editing commands
1271,48566
-@node Script processing commandsScript processing commands
1351,51525
-@node Proof assistant commandsProof assistant commands
1477,56770
-@node Toolbar commandsToolbar commands
1660,63241
-@node Interrupting during trace outputInterrupting during trace output
1685,64200
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1725,66130
-@node Document centred workingDocument centred working
1746,66751
-@node Automatic processingAutomatic processing
1825,69809
-@node Visibility of completed proofsVisibility of completed proofs
1880,71832
-@node Switching between proof scriptsSwitching between proof scripts
1935,73772
-@node View of processed files View of processed files 
1972,75744
-@node Retracting across filesRetracting across files
2032,78795
-@node Asserting across filesAsserting across files
2045,79426
-@node Automatic multiple file handlingAutomatic multiple file handling
2058,79992
-@node Escaping script managementEscaping script management
2083,81026
-@node Editing featuresEditing features
2140,83138
-@node Unicode symbols and special layout supportUnicode symbols and special layout support
2210,85917
-@node Maths menuMaths menu
2252,87475
-@node Unicode Tokens modeUnicode Tokens mode
2269,88166
-@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2319,90589
-@node Special layout Special layout 
2349,91550
-@node Moving between Unicode and tokensMoving between Unicode and tokens
2457,95666
-@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2512,97777
-@node Selecting suitable fontsSelecting suitable fonts
2551,98951
-@node Support for other PackagesSupport for other Packages
2616,101939
-@node Syntax highlightingSyntax highlighting
2646,102775
-@node Imenu and SpeedbarImenu and Speedbar
2674,103778
-@node Support for outline modeSupport for outline mode
2720,105449
-@node Support for completionSupport for completion
2745,106578
-@node Support for tagsSupport for tags
2802,108740
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2854,111088
-@node Goals buffer commandsGoals buffer commands
2870,111683
-@node Customizing Proof GeneralCustomizing Proof General
2969,115836
-@node Basic optionsBasic options
3009,117506
-@node How to customizeHow to customize
3033,118276
-@node Display customizationDisplay customization
3080,120243
-@node User optionsUser options
3234,126648
-@node Changing facesChanging faces
3454,134430
-@node Script buffer facesScript buffer faces
3476,135305
-@node Goals and response facesGoals and response faces
3522,136905
-@node Tweaking configuration settingsTweaking configuration settings
3567,138437
-@node Hints and TipsHints and Tips
3624,140963
-@node Adding your own keybindingsAdding your own keybindings
3643,141564
-@node Using file variablesUsing file variables
3707,144178
-@node Using abbreviationsUsing abbreviations
3766,146364
-@node LEGO Proof GeneralLEGO Proof General
3805,147779
-@node LEGO specific commandsLEGO specific commands
3846,149148
-@node LEGO tagsLEGO tags
3866,149603
-@node LEGO customizationsLEGO customizations
3876,149850
-@node Coq Proof GeneralCoq Proof General
3908,150769
-@node Coq-specific commandsCoq-specific commands
3922,151080
-@node Editing multiple proofsEditing multiple proofs
3945,151588
-@node User-loaded tacticsUser-loaded tactics
3969,152696
-@node Holes featureHoles feature
4033,155170
-@node Isabelle Proof GeneralIsabelle Proof General
4062,156500
-@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4088,157376
-@node Isabelle commandsIsabelle commands
4157,160177
-@node Isabelle settingsIsabelle settings
4300,164369
-@node Isabelle customizationsIsabelle customizations
4314,164951
-@node HOL Proof GeneralHOL Proof General
4337,165438
-@node Shell Proof GeneralShell Proof General
4379,167260
-@node Obtaining and InstallingObtaining and Installing
4415,168719
-@node Obtaining Proof GeneralObtaining Proof General
4430,169084
-@node Installing Proof General from tarballInstalling Proof General from tarball
4456,169966
-@node Setting the names of binariesSetting the names of binaries
4480,170756
-@node Notes for syssiesNotes for syssies
4508,171696
-@node Bugs and EnhancementsBugs and Enhancements
4584,174693
-@node References4605,175508
-@node History of Proof GeneralHistory of Proof General
4645,176531
-@node Old News for 3.0Old News for 3.0
4739,180696
-@node Old News for 3.1Old News for 3.1
4809,184390
-@node Old News for 3.2Old News for 3.2
4835,185562
-@node Old News for 3.3Old News for 3.3
4896,188565
-@node Old News for 3.4Old News for 3.4
4915,189462
-@node Old News for 3.5Old News for 3.5
4937,190517
-@node Old News for 3.6Old News for 3.6
4941,190574
-@node Old News for 3.7Old News for 3.7
4946,190674
-@node Function IndexFunction Index
4976,192128
-@node Variable IndexVariable Index
4980,192204
-@node Keystroke IndexKeystroke Index
4984,192284
-@node Concept IndexConcept Index
4988,192350
+@node Top161,4915
+@node Preface199,6069
+@node News for Version 4.0News for Version 4.0
222,6658
+@node Future243,7509
+@node Credits272,8844
+@node Introducing Proof GeneralIntroducing Proof General
393,13060
+@node Installing Proof GeneralInstalling Proof General
448,15034
+@node Quick start guideQuick start guide
462,15483
+@node Features of Proof GeneralFeatures of Proof General
506,17604
+@node Supported proof assistantsSupported proof assistants
595,21541
+@node Prerequisites for this manualPrerequisites for this manual
644,23422
+@node Organization of this manualOrganization of this manual
688,25041
+@node Basic Script ManagementBasic Script Management
714,25869
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
733,26469
+@node Proof scriptsProof scripts
996,36597
+@node Script buffersScript buffers
1039,38717
+@node Locked queue and editing regionsLocked queue and editing regions
1061,39294
+@node Goal-save sequencesGoal-save sequences
1117,41441
+@node Active scripting bufferActive scripting buffer
1154,42907
+@node Summary of Proof General buffersSummary of Proof General buffers
1223,46327
+@node Script editing commandsScript editing commands
1272,48584
+@node Script processing commandsScript processing commands
1352,51543
+@node Proof assistant commandsProof assistant commands
1478,56788
+@node Toolbar commandsToolbar commands
1661,63259
+@node Interrupting during trace outputInterrupting during trace output
1686,64218
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1726,66148
+@node Document centred workingDocument centred working
1747,66769
+@node Automatic processingAutomatic processing
1826,69827
+@node Visibility of completed proofsVisibility of completed proofs
1881,71850
+@node Switching between proof scriptsSwitching between proof scripts
1936,73790
+@node View of processed files View of processed files 
1973,75762
+@node Retracting across filesRetracting across files
2033,78813
+@node Asserting across filesAsserting across files
2046,79444
+@node Automatic multiple file handlingAutomatic multiple file handling
2059,80010
+@node Escaping script managementEscaping script management
2084,81044
+@node Editing featuresEditing features
2141,83156
+@node Unicode symbols and special layout supportUnicode symbols and special layout support
2211,85935
+@node Maths menuMaths menu
2253,87493
+@node Unicode Tokens modeUnicode Tokens mode
2270,88184
+@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2320,90607
+@node Special layout Special layout 
2350,91568
+@node Moving between Unicode and tokensMoving between Unicode and tokens
2460,95686
+@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2515,97797
+@node Selecting suitable fontsSelecting suitable fonts
2554,98971
+@node Support for other PackagesSupport for other Packages
2619,101959
+@node Syntax highlightingSyntax highlighting
2649,102795
+@node Imenu and SpeedbarImenu and Speedbar
2677,103798
+@node Support for outline modeSupport for outline mode
2723,105469
+@node Support for completionSupport for completion
2748,106598
+@node Support for tagsSupport for tags
2805,108760
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2857,111108
+@node Goals buffer commandsGoals buffer commands
2873,111703
+@node Customizing Proof GeneralCustomizing Proof General
2972,115856
+@node Basic optionsBasic options
3012,117526
+@node How to customizeHow to customize
3036,118296
+@node Display customizationDisplay customization
3083,120263
+@node User optionsUser options
3237,126668
+@node Changing facesChanging faces
3457,134450
+@node Script buffer facesScript buffer faces
3479,135325
+@node Goals and response facesGoals and response faces
3525,136925
+@node Tweaking configuration settingsTweaking configuration settings
3570,138457
+@node Hints and TipsHints and Tips
3627,140983
+@node Adding your own keybindingsAdding your own keybindings
3646,141584
+@node Using file variablesUsing file variables
3710,144198
+@node Using abbreviationsUsing abbreviations
3769,146384
+@node LEGO Proof GeneralLEGO Proof General
3808,147799
+@node LEGO specific commandsLEGO specific commands
3849,149168
+@node LEGO tagsLEGO tags
3869,149623
+@node LEGO customizationsLEGO customizations
3879,149870
+@node Coq Proof GeneralCoq Proof General
3911,150789
+@node Coq-specific commandsCoq-specific commands
3925,151100
+@node Editing multiple proofsEditing multiple proofs
3948,151608
+@node User-loaded tacticsUser-loaded tactics
3972,152716
+@node Holes featureHoles feature
4036,155190
+@node Isabelle Proof GeneralIsabelle Proof General
4065,156520
+@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4091,157396
+@node Isabelle commandsIsabelle commands
4160,160197
+@node Isabelle settingsIsabelle settings
4303,164389
+@node Isabelle customizationsIsabelle customizations
4317,164971
+@node HOL Proof GeneralHOL Proof General
4340,165458
+@node Shell Proof GeneralShell Proof General
4382,167280
+@node Obtaining and InstallingObtaining and Installing
4418,168739
+@node Obtaining Proof GeneralObtaining Proof General
4433,169104
+@node Installing Proof General from tarballInstalling Proof General from tarball
4459,169986
+@node Setting the names of binariesSetting the names of binaries
4483,170776
+@node Notes for syssiesNotes for syssies
4511,171716
+@node Bugs and EnhancementsBugs and Enhancements
4587,174713
+@node References4608,175528
+@node History of Proof GeneralHistory of Proof General
4648,176551
+@node Old News for 3.0Old News for 3.0
4742,180716
+@node Old News for 3.1Old News for 3.1
4812,184410
+@node Old News for 3.2Old News for 3.2
4838,185582
+@node Old News for 3.3Old News for 3.3
4899,188585
+@node Old News for 3.4Old News for 3.4
4918,189482
+@node Old News for 3.5Old News for 3.5
4940,190537
+@node Old News for 3.6Old News for 3.6
4944,190594
+@node Old News for 3.7Old News for 3.7
4949,190694
+@node Function IndexFunction Index
4979,192148
+@node Variable IndexVariable Index
4983,192224
+@node Keystroke IndexKeystroke Index
4987,192304
+@node Concept IndexConcept Index
4991,192370
 
 doc/PG-adapting.texi,3770
-@node Top153,4678
-@node Introduction190,5787
-@node Future231,7440
-@node Credits267,9036
-@node Beginning with a New ProverBeginning with a New Prover
277,9328
-@node Overview of adding a new proverOverview of adding a new prover
317,11270
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration
396,14573
-@node Major modes used by Proof GeneralMajor modes used by Proof General
465,17964
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
508,19674
-@node Settings for generic user-level commandsSettings for generic user-level commands
523,20220
-@node Menu configurationMenu configuration
568,21952
-@node Toolbar configurationToolbar configuration
592,22869
-@node Proof Script SettingsProof Script Settings
651,25106
-@node Recognizing commands and commentsRecognizing commands and comments
673,25686
-@node Recognizing proofsRecognizing proofs
810,32139
-@node Recognizing other elementsRecognizing other elements
914,36443
-@node Configuring undo behaviourConfiguring undo behaviour
977,38922
-@node Nested proofsNested proofs
1114,44309
-@node Safe (state-preserving) commandsSafe (state-preserving) commands
1154,45935
-@node Activate scripting hookActivate scripting hook
1177,46888
-@node Automatic multiple filesAutomatic multiple files
1201,47758
-@node Completions1223,48605
-@node Proof Shell SettingsProof Shell Settings
1264,50095
-@node Proof shell commandsProof shell commands
1295,51377
-@node Script input to the shellScript input to the shell
1459,58428
-@node Settings for matching various output from proof processSettings for matching various output from proof process
1527,61498
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1649,66852
-@node Hooks and other settingsHooks and other settings
1889,77606
-@node Goals Buffer SettingsGoals Buffer Settings
1968,80750
-@node Splash Screen SettingsSplash Screen Settings
2042,83740
-@node Global ConstantsGlobal Constants
2068,84495
-@node Handling Multiple FilesHandling Multiple Files
2094,85324
-@node Configuring Editing SyntaxConfiguring Editing Syntax
2246,93128
-@node Configuring Font LockConfiguring Font Lock
2303,95245
-@node Configuring TokensConfiguring Tokens
2379,98957
-@node Writing More Lisp CodeWriting More Lisp Code
2429,101077
-@node Default values for generic settingsDefault values for generic settings
2446,101722
-@node Adding prover-specific configurationsAdding prover-specific configurations
2476,102805
-@node Useful variablesUseful variables
2519,104087
-@node Useful functions and macrosUseful functions and macros
2534,104586
-@node Internals of Proof GeneralInternals of Proof General
2644,108898
-@node Spans2674,109828
-@node Proof General site configurationProof General site configuration
2689,110201
-@node Configuration variable mechanismsConfiguration variable mechanisms
2772,113282
-@node Global variablesGlobal variables
2898,118763
-@node Proof script modeProof script mode
2973,121387
-@node Proof shell modeProof shell mode
3223,132713
-@node Debugging3737,153362
-@node Plans and IdeasPlans and Ideas
3780,154238
-@node Proof by pointing and similar featuresProof by pointing and similar features
3801,154960
-@node Granularity of atomic command sequencesGranularity of atomic command sequences
3839,156618
-@node Browser mode for script files and theoriesBrowser mode for script files and theories
3884,158843
-@node Demonstration InstantiationsDemonstration Instantiations
3914,159874
-@node demoisa-easy.el3930,160305
-@node demoisa.el3992,162497
-@node Function IndexFunction Index
4146,167417
-@node Variable IndexVariable Index
4150,167493
-@node Concept IndexConcept Index
4159,167672
+@node Top153,4676
+@node Introduction190,5785
+@node Future231,7438
+@node Credits267,9034
+@node Beginning with a New ProverBeginning with a New Prover
277,9326
+@node Overview of adding a new proverOverview of adding a new prover
317,11268
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration
396,14571
+@node Major modes used by Proof GeneralMajor modes used by Proof General
465,17962
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
508,19672
+@node Settings for generic user-level commandsSettings for generic user-level commands
523,20218
+@node Menu configurationMenu configuration
568,21950
+@node Toolbar configurationToolbar configuration
592,22867
+@node Proof Script SettingsProof Script Settings
651,25104
+@node Recognizing commands and commentsRecognizing commands and comments
673,25684
+@node Recognizing proofsRecognizing proofs
810,32137
+@node Recognizing other elementsRecognizing other elements
914,36441
+@node Configuring undo behaviourConfiguring undo behaviour
977,38920
+@node Nested proofsNested proofs
1114,44307
+@node Safe (state-preserving) commandsSafe (state-preserving) commands
1154,45933
+@node Activate scripting hookActivate scripting hook
1177,46886
+@node Automatic multiple filesAutomatic multiple files
1201,47756
+@node Completions1223,48603
+@node Proof Shell SettingsProof Shell Settings
1264,50093
+@node Proof shell commandsProof shell commands
1295,51375
+@node Script input to the shellScript input to the shell
1459,58426
+@node Settings for matching various output from proof processSettings for matching various output from proof process
1527,61496
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1649,66850
+@node Hooks and other settingsHooks and other settings
1889,77604
+@node Goals Buffer SettingsGoals Buffer Settings
1968,80748
+@node Splash Screen SettingsSplash Screen Settings
2042,83738
+@node Global ConstantsGlobal Constants
2068,84493
+@node Handling Multiple FilesHandling Multiple Files
2094,85322
+@node Configuring Editing SyntaxConfiguring Editing Syntax
2246,93126
+@node Configuring Font LockConfiguring Font Lock
2303,95243
+@node Configuring TokensConfiguring Tokens
2379,98955
+@node Writing More Lisp CodeWriting More Lisp Code
2429,101075
+@node Default values for generic settingsDefault values for generic settings
2446,101720
+@node Adding prover-specific configurationsAdding prover-specific configurations
2476,102803
+@node Useful variablesUseful variables
2519,104085
+@node Useful functions and macrosUseful functions and macros
2534,104584
+@node Internals of Proof GeneralInternals of Proof General
2644,108896
+@node Spans2674,109826
+@node Proof General site configurationProof General site configuration
2689,110199
+@node Configuration variable mechanismsConfiguration variable mechanisms
2772,113280
+@node Global variablesGlobal variables
2898,118761
+@node Proof script modeProof script mode
2973,121385
+@node Proof shell modeProof shell mode
3223,132711
+@node Debugging3737,153360
+@node Plans and IdeasPlans and Ideas
3780,154236
+@node Proof by pointing and similar featuresProof by pointing and similar features
3801,154958
+@node Granularity of atomic command sequencesGranularity of atomic command sequences
3839,156616
+@node Browser mode for script files and theoriesBrowser mode for script files and theories
3884,158841
+@node Demonstration InstantiationsDemonstration Instantiations
3914,159872
+@node demoisa-easy.el3930,160303
+@node demoisa.el3992,162494
+@node Function IndexFunction Index
4146,167413
+@node Variable IndexVariable Index
4150,167489
+@node Concept IndexConcept Index
4159,167668
 
 generic/proof.el,0
 
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 20b6b4ef..60863d13 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -213,7 +213,7 @@ Usage: (defpgdefault SYM VALUE)"
   "Define a setting NAME for the current proof assitant, default VAL.
 NAME can correspond to some internal setting, flag, etc, for the
 proof assistant, in which case a :setting and :type value should be provided.
-The :type of NAME should be one of 'integer, 'boolean, 'string.
+The :type of NAME should be one of 'integer, 'float, 'boolean, 'string.
 The customization variable is automatically in group `proof-assistant-setting'.
 The function `proof-assistant-format' is used to format VAL.
 If NAME corresponds instead to a PG internal setting, then a form :eval to
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 45040c94..c6ecd8ec 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -206,8 +206,8 @@ to examine `proof-shell-last-output'.")
 A list of lists (SYMBOL SETTING TYPE DESCR) where SETTING is a string value
 to send to the proof assistant using the value of SYMBOL and
 and the function `proof-assistant-format'.  The TYPE item determines
-the form of the menu entry for the setting and the DESCR description
-string is used as a help tooltip in the settings menu.")
+the form of the menu entry for the setting (this is an Emacs widget type)
+and the DESCR description string is used as a help tooltip in the settings menu.")
 
 (defvar pg-tracing-slow-mode nil
   "Non-nil for slow refresh mode for tracing output.")
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 3fe0fa9b..fc8b33f2 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -8,7 +8,7 @@
 
 
 ;;;### (autoloads (bufhist-exit bufhist-init bufhist-mode) "bufhist"
-;;;;;;  "../lib/bufhist.el" (19157 7589))
+;;;;;;  "../lib/bufhist.el" (19665 37867))
 ;;; Generated autoloads from ../lib/bufhist.el
 
 (autoload 'bufhist-mode "bufhist" "\
@@ -41,15 +41,15 @@ Stop keeping ring history for current buffer.
 
 ;;;### (autoloads (holes-insert-and-expand holes-abbrev-complete
 ;;;;;;  holes-mode holes-set-make-active-hole) "holes" "../lib/holes.el"
-;;;;;;  (19108 1539))
+;;;;;;  (19665 37867))
 ;;; Generated autoloads from ../lib/holes.el
 
-(autoload (quote holes-set-make-active-hole) "holes" "\
+(autoload 'holes-set-make-active-hole "holes" "\
 Make a new hole between START and END or at point, and make it active.
 
 \(fn &optional START END)" t nil)
 
-(autoload (quote holes-mode) "holes" "\
+(autoload 'holes-mode "holes" "\
 Toggle Holes minor mode.
 With arg, turn Outline minor mode on if arg is positive, off otherwise.
 
@@ -139,7 +139,7 @@ undoing on holes cannot make holes re-appear.
 
 \(fn &optional ARG)" t nil)
 
-(autoload (quote holes-abbrev-complete) "holes" "\
+(autoload 'holes-abbrev-complete "holes" "\
 Complete abbrev by putting holes and indenting.
 Moves point at beginning of expanded text.  Put this function as
 call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will
@@ -147,7 +147,7 @@ become holes.
 
 \(fn)" nil nil)
 
-(autoload (quote holes-insert-and-expand) "holes" "\
+(autoload 'holes-insert-and-expand "holes" "\
 Insert S, expand it and replace #s and @{]s by holes.
 
 \(fn S)" nil nil)
@@ -155,10 +155,10 @@ Insert S, expand it and replace #s and @{]s by holes.
 ;;;***
 
 ;;;### (autoloads (maths-menu-mode) "maths-menu" "../lib/maths-menu.el"
-;;;;;;  (19107 62723))
+;;;;;;  (19665 37867))
 ;;; Generated autoloads from ../lib/maths-menu.el
 
-(autoload (quote maths-menu-mode) "maths-menu" "\
+(autoload 'maths-menu-mode "maths-menu" "\
 Install a menu for entering mathematical characters.
 Uses window system menus only when they can display multilingual text.
 Otherwise the menu-bar item activates the text-mode menu system.
@@ -169,7 +169,7 @@ This mode is only useful with a font which can display the maths repertoire.
 ;;;***
 
 ;;;### (autoloads (proof-associated-windows proof-associated-buffers)
-;;;;;;  "pg-assoc" "pg-assoc.el" (19550 46151))
+;;;;;;  "pg-assoc" "pg-assoc.el" (19665 37866))
 ;;; Generated autoloads from pg-assoc.el
 
 (autoload 'proof-associated-buffers "pg-assoc" "\
@@ -186,8 +186,8 @@ Dead or nil buffers are not represented in the list.
 
 ;;;***
 
-;;;### (autoloads (profile-pg) "pg-dev" "../lib/pg-dev.el" (19622
-;;;;;;  2314))
+;;;### (autoloads (profile-pg) "pg-dev" "../lib/pg-dev.el" (19665
+;;;;;;  37867))
 ;;; Generated autoloads from ../lib/pg-dev.el
 
 (autoload 'profile-pg "pg-dev" "\
@@ -198,7 +198,7 @@ Not documented
 ;;;***
 
 ;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
-;;;;;;  (19625 55352))
+;;;;;;  (19665 37866))
 ;;; Generated autoloads from pg-goals.el
 
 (autoload 'proof-goals-config-done "pg-goals" "\
@@ -209,7 +209,7 @@ Initialise the goals buffer after the child has been configured.
 ;;;***
 
 ;;;### (autoloads (pg-movie-export-directory pg-movie-export-from
-;;;;;;  pg-movie-export) "pg-movie" "pg-movie.el" (19570 20547))
+;;;;;;  pg-movie-export) "pg-movie" "pg-movie.el" (19665 37866))
 ;;; Generated autoloads from pg-movie.el
 
 (autoload 'pg-movie-export "pg-movie" "\
@@ -232,7 +232,7 @@ Existing XML files are overwritten.
 ;;;***
 
 ;;;### (autoloads (defpacustom proof-defpacustom-fn) "pg-pamacs"
-;;;;;;  "pg-pamacs.el" (19621 61895))
+;;;;;;  "pg-pamacs.el" (19756 35088))
 ;;; Generated autoloads from pg-pamacs.el
 
 (autoload 'proof-defpacustom-fn "pg-pamacs" "\
@@ -255,7 +255,7 @@ evaluate can be provided instead.
 ;;;***
 
 ;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
-;;;;;;  "pg-pgip" "pg-pgip.el" (19564 4338))
+;;;;;;  "pg-pgip" "pg-pgip.el" (19756 33437))
 ;;; Generated autoloads from pg-pgip.el
 
 (autoload 'pg-pgip-process-packet "pg-pgip" "\
@@ -279,7 +279,7 @@ Send an <askprefs> message to the prover.
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
 ;;;;;;  pg-response-message pg-response-display-with-face pg-response-maybe-erase
 ;;;;;;  proof-response-config-done proof-response-mode) "pg-response"
-;;;;;;  "pg-response.el" (19574 64296))
+;;;;;;  "pg-response.el" (19665 37866))
 ;;; Generated autoloads from pg-response.el
 
 (autoload 'proof-response-mode "pg-response" "\
@@ -343,7 +343,7 @@ See `pg-next-error-regexp'.
 ;;;;;;  pg-slow-fontify-tracing-hint proof-electric-terminator-enable
 ;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command
 ;;;;;;  proof-goto-point proof-script-new-command-advance) "pg-user"
-;;;;;;  "pg-user.el" (19633 61674))
+;;;;;;  "pg-user.el" (19665 37866))
 ;;; Generated autoloads from pg-user.el
 
 (autoload 'proof-script-new-command-advance "pg-user" "\
@@ -462,8 +462,8 @@ Enable or disable autosend behaviour.
 
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19542
-;;;;;;  60238))
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19665
+;;;;;;  37866))
 ;;; Generated autoloads from pg-xml.el
 
 (autoload 'pg-xml-parse-string "pg-xml" "\
@@ -474,7 +474,7 @@ Parse string in ARG, same as pg-xml-parse-buffer.
 ;;;***
 
 ;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies)
-;;;;;;  "proof-depends" "proof-depends.el" (19550 46151))
+;;;;;;  "proof-depends" "proof-depends.el" (19665 37866))
 ;;; Generated autoloads from proof-depends.el
 
 (autoload 'proof-depends-process-dependencies "proof-depends" "\
@@ -492,10 +492,10 @@ Make some menu entries showing proof dependencies of SPAN.
 ;;;***
 
 ;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
-;;;;;;  (19108 51621))
+;;;;;;  (19665 37866))
 ;;; Generated autoloads from proof-easy-config.el
 
-(autoload (quote proof-easy-config) "proof-easy-config" "\
+(autoload 'proof-easy-config "proof-easy-config" "\
 Configure Proof General for proof-assistant using BODY as a setq body.
 The symbol SYM and string name NAME must match those given in
 the `proof-assistant-table', which see.
@@ -505,7 +505,7 @@ the `proof-assistant-table', which see.
 ;;;***
 
 ;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el"
-;;;;;;  (19550 46151))
+;;;;;;  (19665 37866))
 ;;; Generated autoloads from proof-indent.el
 
 (autoload 'proof-indent-line "proof-indent" "\
@@ -516,7 +516,7 @@ Indent current line of proof script, if indentation enabled.
 ;;;***
 
 ;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-set-global)
-;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19575 41316))
+;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19665 37866))
 ;;; Generated autoloads from proof-maths-menu.el
 
 (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
@@ -537,8 +537,8 @@ in future if we have just activated it for this buffer.
 ;;;***
 
 ;;;### (autoloads (proof-aux-menu proof-menu-define-specific proof-menu-define-main
-;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19625
-;;;;;;  55352))
+;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19756
+;;;;;;  35398))
 ;;; Generated autoloads from proof-menu.el
 
 (autoload 'proof-menu-define-keys "proof-menu" "\
@@ -564,7 +564,7 @@ Construct and return PG auxiliary menu used in non-scripting buffers.
 ;;;***
 
 ;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm"
-;;;;;;  "proof-mmm.el" (19550 46151))
+;;;;;;  "proof-mmm.el" (19665 37866))
 ;;; Generated autoloads from proof-mmm.el
 
 (autoload 'proof-mmm-set-global "proof-mmm" "\
@@ -587,7 +587,7 @@ in future if we have just activated it for this buffer.
 ;;;;;;  proof-insert-pbp-command proof-register-possibly-new-processed-file
 ;;;;;;  pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p
 ;;;;;;  proof-unprocessed-begin proof-colour-locked) "proof-script"
-;;;;;;  "proof-script.el" (19633 62018))
+;;;;;;  "proof-script.el" (19756 34673))
 ;;; Generated autoloads from proof-script.el
 
 (autoload 'proof-colour-locked "proof-script" "\
@@ -672,7 +672,7 @@ finish setup which depends on specific proof assistant configuration.
 ;;;;;;  proof-shell-invisible-cmd-get-result proof-shell-invisible-command
 ;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
 ;;;;;;  proof-shell-available-p proof-shell-ready-prover) "proof-shell"
-;;;;;;  "proof-shell.el" (19633 48731))
+;;;;;;  "proof-shell.el" (19756 34673))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload 'proof-shell-ready-prover "proof-shell" "\
@@ -803,7 +803,7 @@ processing.
 ;;;***
 
 ;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el"
-;;;;;;  (19634 16192))
+;;;;;;  (19756 33437))
 ;;; Generated autoloads from proof-site.el
 
 (autoload 'proof-ready-for-assistant "proof-site" "\
@@ -815,7 +815,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
 ;;;***
 
 ;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;;  "proof-splash" "proof-splash.el" (19628 18525))
+;;;;;;  "proof-splash" "proof-splash.el" (19665 37866))
 ;;; Generated autoloads from proof-splash.el
 
 (autoload 'proof-splash-display-screen "proof-splash" "\
@@ -834,7 +834,7 @@ Make sure the user gets welcomed one way or another.
 ;;;***
 
 ;;;### (autoloads (proof-format) "proof-syntax" "proof-syntax.el"
-;;;;;;  (19609 53995))
+;;;;;;  (19665 37866))
 ;;; Generated autoloads from proof-syntax.el
 
 (defsubst proof-replace-regexp-in-string (regexp rep string) "\
@@ -850,7 +850,7 @@ may be a string or sexp evaluated to get a string.
 ;;;***
 
 ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;;  "proof-toolbar" "proof-toolbar.el" (19609 20575))
+;;;;;;  "proof-toolbar" "proof-toolbar.el" (19665 37866))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload 'proof-toolbar-setup "proof-toolbar" "\
@@ -870,21 +870,21 @@ Menu made from the Proof General toolbar commands.
 
 ;;;### (autoloads (proof-unicode-tokens-enable proof-unicode-tokens-set-global
 ;;;;;;  proof-unicode-tokens-mode-if-enabled) "proof-unicode-tokens"
-;;;;;;  "proof-unicode-tokens.el" (19126 41475))
+;;;;;;  "proof-unicode-tokens.el" (19665 37866))
 ;;; Generated autoloads from proof-unicode-tokens.el
 
-(autoload (quote proof-unicode-tokens-mode-if-enabled) "proof-unicode-tokens" "\
+(autoload 'proof-unicode-tokens-mode-if-enabled "proof-unicode-tokens" "\
 Turn on or off the Unicode Tokens minor mode in this buffer.
 
 \(fn)" nil nil)
 
-(autoload (quote proof-unicode-tokens-set-global) "proof-unicode-tokens" "\
+(autoload 'proof-unicode-tokens-set-global "proof-unicode-tokens" "\
 Set global status of unicode tokens mode for PG buffers to be FLAG.
 Turn on/off menu in all script buffers and ensure new buffers follow suit.
 
 \(fn FLAG)" nil nil)
 
-(autoload (quote proof-unicode-tokens-enable) "proof-unicode-tokens" "\
+(autoload 'proof-unicode-tokens-enable "proof-unicode-tokens" "\
 Turn on or off Unicode tokens mode in Proof General script buffer.
 This invokes `unicode-tokens-mode' to toggle the setting for the current
 buffer, and then sets PG's option for default to match.
@@ -897,12 +897,12 @@ is changed.
 
 ;;;***
 
-;;;### (autoloads (proof-debug) "proof-utils" "proof-utils.el" (19630
-;;;;;;  57223))
+;;;### (autoloads (proof-debug) "proof-utils" "proof-utils.el" (19690
+;;;;;;  31413))
 ;;; Generated autoloads from proof-utils.el
 
 (autoload 'proof-debug "proof-utils" "\
-Issue the debugging message (format MSG ARGS) in the response buffer, display it.
+Issue the debugging message (format MSG ARGS) in the *PG Debug* buffer.
 If proof-general-debug is nil, do nothing.
 
 \(fn MSG &rest ARGS)" nil nil)
@@ -910,10 +910,10 @@ If proof-general-debug is nil, do nothing.
 ;;;***
 
 ;;;### (autoloads (scomint-make scomint-make-in-buffer) "scomint"
-;;;;;;  "../lib/scomint.el" (19126 40592))
+;;;;;;  "../lib/scomint.el" (19665 37867))
 ;;; Generated autoloads from ../lib/scomint.el
 
-(autoload (quote scomint-make-in-buffer) "scomint" "\
+(autoload 'scomint-make-in-buffer "scomint" "\
 Make a Comint process NAME in BUFFER, running PROGRAM.
 If BUFFER is nil, it defaults to NAME surrounded by `*'s.
 PROGRAM should be either a string denoting an executable program to create
@@ -926,7 +926,7 @@ If PROGRAM is a string, any more args are arguments to PROGRAM.
 
 \(fn NAME BUFFER PROGRAM &optional STARTFILE &rest SWITCHES)" nil nil)
 
-(autoload (quote scomint-make) "scomint" "\
+(autoload 'scomint-make "scomint" "\
 Make a Comint process NAME in a buffer, running PROGRAM.
 The name of the buffer is made by surrounding NAME with `*'s.
 PROGRAM should be either a string denoting an executable program to create
@@ -942,7 +942,7 @@ If PROGRAM is a string, any more args are arguments to PROGRAM.
 ;;;***
 
 ;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el"
-;;;;;;  (19542 60238))
+;;;;;;  (19665 37867))
 ;;; Generated autoloads from ../lib/texi-docstring-magic.el
 
 (autoload 'texi-docstring-magic "texi-docstring-magic" "\
@@ -955,10 +955,10 @@ With prefix arg, no errors on unknown symbols.  (This results in
 ;;;***
 
 ;;;### (autoloads (unicode-chars-list-chars) "unicode-chars" "../lib/unicode-chars.el"
-;;;;;;  (19107 62795))
+;;;;;;  (19665 37867))
 ;;; Generated autoloads from ../lib/unicode-chars.el
 
-(autoload (quote unicode-chars-list-chars) "unicode-chars" "\
+(autoload 'unicode-chars-list-chars "unicode-chars" "\
 Insert each Unicode character into a buffer.
 Lets you see which characters are available for literal display
 in your emacs font.
@@ -968,7 +968,7 @@ in your emacs font.
 ;;;***
 
 ;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;;  (19591 34223))
+;;;;;;  (19665 37867))
 ;;; Generated autoloads from ../lib/unicode-tokens.el
 
 (autoload 'unicode-tokens-encode-str "unicode-tokens" "\
@@ -982,7 +982,7 @@ Return a unicode encoded version presentation of STR.
 ;;;;;;  "../lib/proof-compat.el" "../lib/span.el" "pg-autotest.el"
 ;;;;;;  "pg-custom.el" "pg-pbrpm.el" "pg-vars.el" "proof-auxmodes.el"
 ;;;;;;  "proof-config.el" "proof-faces.el" "proof-useropts.el" "proof.el")
-;;;;;;  (19634 16926 377965))
+;;;;;;  (19756 35402 417383))
 
 ;;;***
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 1253a12a..182368d9 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -869,6 +869,10 @@ KEY is the optional key binding."
       (vector entry-name
 	      (proof-defintset-fn pasym)
 	      :help descr))
+     ((eq type 'number)
+      (vector entry-name
+	      (proof-deffloatset-fn pasym)
+	      :help descr))
      ((eq type 'string)
       (vector entry-name
 	      (proof-defstringset-fn pasym)
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index eb170e23..0b73803b 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -552,6 +552,29 @@ OTHERNAME gives an alternative name than the default <VAR>-intset.
 The name of the defined function is returned."
   `(proof-defintset-fn (quote ,var) (quote ,othername)))
 
+(defun proof-deffloatset-fn (var &optional othername)
+  "Define a function <VAR>-floatset for setting an float customize setting VAR.
+Args as for the macro `proof-deffloatset', except will be evaluated."
+  (eval
+   `(defun ,(if othername othername
+	      (intern (concat (symbol-name var) "-floatset"))) (arg)
+	      ,(concat "Set `" (symbol-name var) "' to ARG.
+This function simply uses customize-set-variable to set the variable.
+It was constructed with `proof-deffloatset-fn'.")
+	      (interactive (list
+			    (read-number
+			     (format "Value for %s (float, currently %s): "
+				     (symbol-name (quote ,var))
+				     (symbol-value (quote ,var))))))
+	      (customize-set-variable (quote ,var) arg))))
+
+(defmacro proof-deffloatset (var &optional othername)
+  "Define a function <VAR>-floatset for setting an float customize setting VAR.
+The setting function uses `customize-set-variable' to change the variable.
+OTHERNAME gives an alternative name than the default <VAR>-floatset.
+The name of the defined function is returned."
+  `(proof-deffloatset-fn (quote ,var) (quote ,othername)))
+
 (defun proof-defstringset-fn (var &optional othername)
   "Define a function <VAR>-toggle for setting an integer customize setting VAR.
 Args as for the macro `proof-defstringset', except will be evaluated."