1 files changed, 718 insertions, 704 deletions

diff --git a/TAGS b/TAGS
index 7b5400f6..83c6cefc 100644
--- a/TAGS
+++ b/TAGS
@@ -39,159 +39,159 @@ coq/coq-db.el,668
 (defconst coq-cheat-face 251,9112
 
 coq/coq.el,5977
-(defcustom coq-translate-to-v8 46,1310
-(defun coq-build-prog-args 52,1490
-(defcustom coq-compile-file-command 62,1786
-(defcustom coq-use-makefile 70,2105
-(defcustom coq-default-undo-limit 78,2328
-(defconst coq-shell-init-cmd83,2456
-(defcustom coq-prog-env 89,2583
-(defconst coq-shell-restart-cmd 97,2833
-(defvar coq-shell-prompt-pattern99,2887
-(defvar coq-shell-cd 107,3191
-(defvar coq-shell-proof-completed-regexp 111,3351
-(defvar coq-goal-regexp114,3506
-(defun coq-library-directory 121,3620
-(defcustom coq-tags 128,3799
-(defconst coq-interrupt-regexp 133,3949
-(defcustom coq-www-home-page 138,4070
-(defvar coq-outline-regexp145,4238
-(defvar coq-outline-heading-end-regexp 152,4450
-(defvar coq-shell-outline-regexp 154,4504
-(defvar coq-shell-outline-heading-end-regexp 155,4554
-(defconst coq-state-preserving-tactics-regexp161,4719
-(defconst coq-state-changing-commands-regexp163,4819
-(defconst coq-state-preserving-commands-regexp165,4926
-(defconst coq-commands-regexp167,5037
-(defvar coq-retractable-instruct-regexp169,5114
-(defvar coq-non-retractable-instruct-regexp171,5204
-(defun coq-set-undo-limit 205,6081
-(defun build-list-id-from-string 209,6211
-(defun coq-last-prompt-info 221,6709
-(defun coq-last-prompt-info-safe 233,7241
-(defvar coq-last-but-one-statenum 239,7498
-(defvar coq-last-but-one-proofnum 245,7795
-(defvar coq-last-but-one-proofstack 248,7893
-(defun coq-get-span-statenum 251,8003
-(defun coq-get-span-proofnum 256,8118
-(defun coq-get-span-proofstack 261,8233
-(defun coq-set-span-statenum 266,8377
-(defun coq-get-span-goalcmd 271,8508
-(defun coq-set-span-goalcmd 276,8622
-(defun coq-set-span-proofnum 281,8752
-(defun coq-set-span-proofstack 286,8883
-(defun proof-last-locked-span 291,9043
-(defun proof-clone-buffer 300,9341
-(defun proof-store-buffer-win 314,9898
-(defun proof-store-response-win 322,10123
-(defun proof-store-goals-win 326,10252
-(defun coq-set-state-infos 339,10787
-(defun count-not-intersection 378,12782
-(defun coq-find-and-forget 409,14032
-(defvar coq-current-goal 429,14936
-(defun coq-goal-hyp 432,15001
-(defun coq-state-preserving-p 445,15433
-(defconst notation-print-kinds-table459,15934
-(defun coq-PrintScope 463,16101
-(defun coq-guess-or-ask-for-string 481,16650
-(defun coq-ask-do 495,17218
-(defun coq-put-into-brackets 504,17603
-(defun coq-put-into-quotes 508,17664
-(defun coq-SearchIsos 510,17718
-(defun coq-SearchConstant 516,17951
-(defun coq-Searchregexp 522,18046
-(defun coq-SearchRewrite 527,18182
-(defun coq-SearchAbout 531,18280
-(defun coq-Print 535,18418
-(defun coq-About 539,18540
-(defun coq-LocateConstant 543,18657
-(defun coq-LocateLibrary 549,18792
-(defun coq-LocateNotation 556,18943
-(defun coq-Pwd 563,19147
-(defun coq-Inspect 569,19279
-(defun coq-PrintSection(573,19379
-(defun coq-Print-implicit 577,19472
-(defun coq-Check 582,19623
-(defun coq-Show 587,19731
-(defun coq-Compile 601,20174
-(defun coq-guess-command-line 613,20492
-(defpacustom use-editing-holes 652,22164
-(defun coq-mode-config 662,22501
-(defun coq-shell-mode-config 766,26385
-(defun coq-goals-mode-config 809,28184
-(defun coq-response-config 816,28428
-(defpacustom print-fully-explicit 841,29253
-(defpacustom print-implicit 846,29401
-(defpacustom print-coercions 851,29567
-(defpacustom print-match-wildcards 856,29711
-(defpacustom print-elim-types 861,29891
-(defpacustom printing-depth 866,30057
-(defpacustom undo-depth 871,30218
-(defpacustom time-commands 876,30365
-(defpacustom undo-limit 880,30475
-(defpacustom auto-compile-vos 885,30577
-(defun coq-maybe-compile-buffer 914,31691
-(defun coq-ancestors-of 950,33219
-(defun coq-all-ancestors-of 973,34183
-(defun coq-process-require-command 984,34530
-(defun coq-included-children 989,34657
-(defun coq-process-file 1010,35496
-(defun coq-preprocessing 1025,36035
-(defun coq-fake-constant-markup 1039,36470
-(defun coq-create-span-menu 1055,37075
-(defconst module-kinds-table1072,37559
-(defconst modtype-kinds-table1076,37708
-(defun coq-insert-section-or-module 1080,37837
-(defconst reqkinds-kinds-table1103,38695
-(defun coq-insert-requires 1108,38840
-(defun coq-end-Section 1124,39343
-(defun coq-insert-intros 1142,39921
-(defun coq-insert-infoH-hook 1155,40455
-(defun coq-insert-as 1160,40663
-(defun coq-insert-match 1177,41366
-(defun coq-insert-tactic 1209,42548
-(defun coq-insert-tactical 1215,42787
-(defun coq-insert-command 1221,43036
-(defun coq-insert-term 1227,43280
-(define-key coq-keymap 1233,43477
-(define-key coq-keymap 1234,43535
-(define-key coq-keymap 1235,43592
-(define-key coq-keymap 1236,43661
-(define-key coq-keymap 1237,43717
-(define-key coq-keymap 1238,43766
-(define-key coq-keymap 1239,43824
-(define-key coq-keymap 1240,43884
-(define-key coq-keymap 1241,43949
-(define-key coq-keymap 1243,44012
-(define-key coq-keymap 1244,44071
-(define-key coq-keymap 1248,44196
-(define-key coq-keymap 1250,44252
-(define-key coq-keymap 1251,44302
-(define-key coq-keymap 1252,44352
-(define-key coq-keymap 1253,44408
-(define-key coq-keymap 1254,44458
-(define-key coq-keymap 1255,44512
-(define-key coq-keymap 1256,44571
-(define-key coq-goals-mode-map 1259,44632
-(define-key coq-goals-mode-map 1260,44714
-(define-key coq-goals-mode-map 1261,44796
-(define-key coq-goals-mode-map 1262,44883
-(define-key coq-goals-mode-map 1263,44965
-(defvar last-coq-error-location 1272,45267
-(defun coq-get-last-error-location 1281,45666
-(defun coq-highlight-error 1331,48207
-(defvar coq-allow-highlight-error 1362,49347
-(defun coq-decide-highlight-error 1369,49673
-(defun coq-highlight-error-hook 1374,49858
-(defun first-word-of-buffer 1385,50251
-(defun coq-show-first-goal 1393,50454
-(defvar coq-modeline-string2 1410,51149
-(defvar coq-modeline-string1 1411,51193
-(defvar coq-modeline-string0 1412,51236
-(defun coq-build-subgoals-string 1413,51281
-(defun coq-update-minor-mode-alist 1418,51447
-(defun is-not-split-vertic 1444,52518
-(defun optim-resp-windows 1453,52958
+(defcustom coq-translate-to-v8 46,1308
+(defun coq-build-prog-args 52,1488
+(defcustom coq-compile-file-command 62,1784
+(defcustom coq-use-makefile 70,2103
+(defcustom coq-default-undo-limit 78,2326
+(defconst coq-shell-init-cmd83,2454
+(defcustom coq-prog-env 89,2581
+(defconst coq-shell-restart-cmd 97,2831
+(defvar coq-shell-prompt-pattern99,2885
+(defvar coq-shell-cd 107,3189
+(defvar coq-shell-proof-completed-regexp 111,3349
+(defvar coq-goal-regexp114,3504
+(defun coq-library-directory 121,3618
+(defcustom coq-tags 128,3797
+(defconst coq-interrupt-regexp 133,3947
+(defcustom coq-www-home-page 138,4068
+(defvar coq-outline-regexp145,4236
+(defvar coq-outline-heading-end-regexp 152,4448
+(defvar coq-shell-outline-regexp 154,4502
+(defvar coq-shell-outline-heading-end-regexp 155,4552
+(defconst coq-state-preserving-tactics-regexp161,4717
+(defconst coq-state-changing-commands-regexp163,4817
+(defconst coq-state-preserving-commands-regexp165,4924
+(defconst coq-commands-regexp167,5035
+(defvar coq-retractable-instruct-regexp169,5112
+(defvar coq-non-retractable-instruct-regexp171,5202
+(defun coq-set-undo-limit 205,6079
+(defun build-list-id-from-string 209,6209
+(defun coq-last-prompt-info 221,6707
+(defun coq-last-prompt-info-safe 233,7239
+(defvar coq-last-but-one-statenum 239,7496
+(defvar coq-last-but-one-proofnum 245,7793
+(defvar coq-last-but-one-proofstack 248,7891
+(defun coq-get-span-statenum 251,8001
+(defun coq-get-span-proofnum 256,8116
+(defun coq-get-span-proofstack 261,8231
+(defun coq-set-span-statenum 266,8375
+(defun coq-get-span-goalcmd 271,8506
+(defun coq-set-span-goalcmd 276,8620
+(defun coq-set-span-proofnum 281,8750
+(defun coq-set-span-proofstack 286,8881
+(defun proof-last-locked-span 291,9041
+(defun proof-clone-buffer 297,9271
+(defun proof-store-buffer-win 311,9828
+(defun proof-store-response-win 319,10053
+(defun proof-store-goals-win 323,10182
+(defun coq-set-state-infos 336,10717
+(defun count-not-intersection 375,12712
+(defun coq-find-and-forget 406,13962
+(defvar coq-current-goal 426,14866
+(defun coq-goal-hyp 429,14931
+(defun coq-state-preserving-p 442,15363
+(defconst notation-print-kinds-table456,15864
+(defun coq-PrintScope 460,16031
+(defun coq-guess-or-ask-for-string 478,16580
+(defun coq-ask-do 492,17148
+(defun coq-put-into-brackets 501,17533
+(defun coq-put-into-quotes 505,17594
+(defun coq-SearchIsos 507,17648
+(defun coq-SearchConstant 513,17881
+(defun coq-Searchregexp 519,17976
+(defun coq-SearchRewrite 524,18112
+(defun coq-SearchAbout 528,18210
+(defun coq-Print 532,18348
+(defun coq-About 536,18470
+(defun coq-LocateConstant 540,18587
+(defun coq-LocateLibrary 546,18722
+(defun coq-LocateNotation 553,18873
+(defun coq-Pwd 560,19077
+(defun coq-Inspect 566,19209
+(defun coq-PrintSection(570,19309
+(defun coq-Print-implicit 574,19402
+(defun coq-Check 579,19553
+(defun coq-Show 584,19661
+(defun coq-Compile 598,20104
+(defun coq-guess-command-line 610,20422
+(defpacustom use-editing-holes 649,22094
+(defun coq-mode-config 659,22431
+(defun coq-shell-mode-config 763,26315
+(defun coq-goals-mode-config 806,28114
+(defun coq-response-config 813,28358
+(defpacustom print-fully-explicit 838,29183
+(defpacustom print-implicit 843,29331
+(defpacustom print-coercions 848,29497
+(defpacustom print-match-wildcards 853,29641
+(defpacustom print-elim-types 858,29821
+(defpacustom printing-depth 863,29987
+(defpacustom undo-depth 868,30148
+(defpacustom time-commands 873,30295
+(defpacustom undo-limit 877,30405
+(defpacustom auto-compile-vos 882,30507
+(defun coq-maybe-compile-buffer 911,31621
+(defun coq-ancestors-of 947,33149
+(defun coq-all-ancestors-of 970,34113
+(defun coq-process-require-command 981,34460
+(defun coq-included-children 986,34587
+(defun coq-process-file 1007,35426
+(defun coq-preprocessing 1022,35965
+(defun coq-fake-constant-markup 1036,36400
+(defun coq-create-span-menu 1052,37005
+(defconst module-kinds-table1069,37489
+(defconst modtype-kinds-table1073,37638
+(defun coq-insert-section-or-module 1077,37767
+(defconst reqkinds-kinds-table1100,38625
+(defun coq-insert-requires 1105,38770
+(defun coq-end-Section 1121,39273
+(defun coq-insert-intros 1139,39851
+(defun coq-insert-infoH-hook 1152,40385
+(defun coq-insert-as 1157,40593
+(defun coq-insert-match 1174,41296
+(defun coq-insert-tactic 1206,42478
+(defun coq-insert-tactical 1212,42717
+(defun coq-insert-command 1218,42966
+(defun coq-insert-term 1224,43210
+(define-key coq-keymap 1230,43407
+(define-key coq-keymap 1231,43465
+(define-key coq-keymap 1232,43522
+(define-key coq-keymap 1233,43591
+(define-key coq-keymap 1234,43647
+(define-key coq-keymap 1235,43696
+(define-key coq-keymap 1236,43754
+(define-key coq-keymap 1237,43814
+(define-key coq-keymap 1238,43879
+(define-key coq-keymap 1240,43942
+(define-key coq-keymap 1241,44001
+(define-key coq-keymap 1245,44126
+(define-key coq-keymap 1247,44182
+(define-key coq-keymap 1248,44232
+(define-key coq-keymap 1249,44282
+(define-key coq-keymap 1250,44338
+(define-key coq-keymap 1251,44388
+(define-key coq-keymap 1252,44442
+(define-key coq-keymap 1253,44501
+(define-key coq-goals-mode-map 1256,44562
+(define-key coq-goals-mode-map 1257,44644
+(define-key coq-goals-mode-map 1258,44726
+(define-key coq-goals-mode-map 1259,44813
+(define-key coq-goals-mode-map 1260,44895
+(defvar last-coq-error-location 1269,45197
+(defun coq-get-last-error-location 1278,45596
+(defun coq-highlight-error 1328,48137
+(defvar coq-allow-highlight-error 1359,49277
+(defun coq-decide-highlight-error 1366,49603
+(defun coq-highlight-error-hook 1371,49788
+(defun first-word-of-buffer 1382,50181
+(defun coq-show-first-goal 1390,50384
+(defvar coq-modeline-string2 1407,51079
+(defvar coq-modeline-string1 1408,51123
+(defvar coq-modeline-string0 1409,51166
+(defun coq-build-subgoals-string 1410,51211
+(defun coq-update-minor-mode-alist 1415,51377
+(defun is-not-split-vertic 1441,52448
+(defun optim-resp-windows 1450,52888
 
 coq/coq-indent.el,2223
 (defconst coq-any-command-regexp20,368
@@ -383,44 +383,44 @@ isar/isabelle-system.el,1254
 (defun isabelle-process-pgip 361,13019
 
 isar/isar.el,1595
-(defcustom isar-keywords-name 40,925
-(defpgdefault completion-table 56,1436
-(defcustom isar-web-page58,1489
-(defun isar-strip-terminators 72,1839
-(defun isar-markup-ml 85,2216
-(defun isar-mode-config-set-variables 90,2351
-(defun isar-shell-mode-config-set-variables 155,5123
-(defun isar-set-proof-find-theorems-command 236,8257
-(defpacustom use-find-theorems-form 242,8441
-(defun isar-set-undo-commands 247,8607
-(defpacustom use-linear-undo 258,9058
-(defun isar-configure-from-settings 263,9216
-(defun isar-remove-file 271,9360
-(defun isar-shell-compute-new-files-list 281,9715
-(define-derived-mode isar-shell-mode 300,10295
-(define-derived-mode isar-response-mode 305,10422
-(define-derived-mode isar-goals-mode 310,10555
-(define-derived-mode isar-mode 315,10681
-(defpgdefault menu-entries372,12574
-(defun isar-set-command 405,13874
-(defpgdefault help-menu-entries 410,14004
-(defun isar-count-undos 413,14080
-(defun isar-find-and-forget 439,15062
-(defun isar-goal-command-p 478,16519
-(defun isar-global-save-command-p 483,16696
-(defvar isar-current-goal 504,17480
-(defun isar-state-preserving-p 507,17546
-(defvar isar-shell-current-line-width 532,18395
-(defun isar-shell-adjust-line-width 537,18587
-(defsubst isar-string-wrapping 562,19385
-(defsubst isar-positions-of 571,19579
-(defcustom isar-wrap-commands-singly 577,19784
-(defun isar-command-wrapping 583,19980
-(defun isar-preprocessing 591,20294
-(defun isar-mode-config 609,20845
-(defun isar-shell-mode-config 623,21498
-(defun isar-response-mode-config 633,21847
-(defun isar-goals-mode-config 643,22182
+(defcustom isar-keywords-name 40,919
+(defpgdefault completion-table 56,1430
+(defcustom isar-web-page58,1483
+(defun isar-strip-terminators 72,1833
+(defun isar-markup-ml 85,2210
+(defun isar-mode-config-set-variables 90,2345
+(defun isar-shell-mode-config-set-variables 155,5151
+(defun isar-set-proof-find-theorems-command 236,8285
+(defpacustom use-find-theorems-form 242,8469
+(defun isar-set-undo-commands 247,8635
+(defpacustom use-linear-undo 258,9086
+(defun isar-configure-from-settings 263,9244
+(defun isar-remove-file 271,9388
+(defun isar-shell-compute-new-files-list 281,9743
+(define-derived-mode isar-shell-mode 300,10323
+(define-derived-mode isar-response-mode 305,10450
+(define-derived-mode isar-goals-mode 310,10583
+(define-derived-mode isar-mode 315,10709
+(defpgdefault menu-entries370,12502
+(defun isar-set-command 401,13696
+(defpgdefault help-menu-entries 406,13826
+(defun isar-count-undos 409,13902
+(defun isar-find-and-forget 435,14884
+(defun isar-goal-command-p 474,16341
+(defun isar-global-save-command-p 479,16518
+(defvar isar-current-goal 500,17302
+(defun isar-state-preserving-p 503,17368
+(defvar isar-shell-current-line-width 528,18217
+(defun isar-shell-adjust-line-width 533,18409
+(defsubst isar-string-wrapping 556,19174
+(defsubst isar-positions-of 565,19368
+(defcustom isar-wrap-commands-singly 571,19573
+(defun isar-command-wrapping 577,19769
+(defun isar-preprocessing 585,20083
+(defun isar-mode-config 603,20634
+(defun isar-shell-mode-config 617,21287
+(defun isar-response-mode-config 627,21636
+(defun isar-goals-mode-config 637,21971
 
 isar/isar-find-theorems.el,779
 (defvar isar-find-theorems-data 19,565
@@ -440,37 +440,37 @@ isar/isar-find-theorems.el,779
 (defun isar-find-theorems-parse-number 469,16275
 (defun isar-find-theorems-filter-empty 479,16552
 
-isar/isar-keywords.el,1052
-(defconst isar-keywords-major13,481
-(defconst isar-keywords-minor206,3641
-(defconst isar-keywords-control262,4395
-(defconst isar-keywords-diag282,4872
-(defconst isar-keywords-theory-begin338,5831
-(defconst isar-keywords-theory-switch341,5884
-(defconst isar-keywords-theory-end344,5939
-(defconst isar-keywords-theory-heading347,5987
-(defconst isar-keywords-theory-decl353,6094
-(defconst isar-keywords-theory-script412,7075
-(defconst isar-keywords-theory-goal416,7152
-(defconst isar-keywords-qed429,7369
-(defconst isar-keywords-qed-block436,7455
-(defconst isar-keywords-qed-global439,7502
-(defconst isar-keywords-proof-heading442,7551
-(defconst isar-keywords-proof-goal447,7634
-(defconst isar-keywords-proof-block454,7733
-(defconst isar-keywords-proof-open458,7795
-(defconst isar-keywords-proof-close461,7841
-(defconst isar-keywords-proof-chain464,7888
-(defconst isar-keywords-proof-decl471,7991
-(defconst isar-keywords-proof-asm480,8112
-(defconst isar-keywords-proof-asm-goal487,8207
-(defconst isar-keywords-proof-script490,8262
+isar/isar-keywords.el,1064
+(defconst isar-keywords-major7,222
+(defconst isar-keywords-minor280,4856
+(defconst isar-keywords-control339,5659
+(defconst isar-keywords-diag360,6153
+(defconst isar-keywords-theory-begin434,7438
+(defconst isar-keywords-theory-switch437,7491
+(defconst isar-keywords-theory-end440,7537
+(defconst isar-keywords-theory-heading443,7585
+(defconst isar-keywords-theory-decl449,7692
+(defconst isar-keywords-theory-script552,9481
+(defconst isar-keywords-theory-goal555,9544
+(defconst isar-keywords-qed583,10059
+(defconst isar-keywords-qed-block590,10145
+(defconst isar-keywords-qed-global593,10192
+(defconst isar-keywords-proof-heading596,10241
+(defconst isar-keywords-proof-goal601,10324
+(defconst isar-keywords-proof-block606,10401
+(defconst isar-keywords-proof-open610,10463
+(defconst isar-keywords-proof-close613,10509
+(defconst isar-keywords-proof-chain616,10556
+(defconst isar-keywords-proof-decl623,10659
+(defconst isar-keywords-proof-asm635,10821
+(defconst isar-keywords-proof-asm-goal642,10916
+(defconst isar-keywords-proof-script648,11005
 
 isar/isar-mmm.el,81
 (defconst isar-start-latex-regexp24,744
 (defconst isar-start-sml-regexp36,1172
 
-isar/isar-syntax.el,3652
+isar/isar-syntax.el,3748
 (defconst isar-script-syntax-table-entries18,478
 (defconst isar-script-syntax-table-alist42,880
 (defun isar-init-syntax-table 51,1163
@@ -549,16 +549,18 @@ isar/isar-syntax.el,3652
 (defconst isar-undo-ignore-regexp498,15659
 (defconst isar-undo-remove-regexp501,15724
 (defconst isar-keywords-imenu509,15881
-(defconst isar-named-entity-regexp516,16072
-(defconst isar-generic-expression521,16236
-(defconst isar-indent-any-regexp532,16470
-(defconst isar-indent-inner-regexp534,16563
-(defconst isar-indent-enclose-regexp536,16629
-(defconst isar-indent-open-regexp538,16745
-(defconst isar-indent-close-regexp540,16855
-(defconst isar-outline-regexp546,16992
-(defconst isar-outline-heading-end-regexp 550,17145
-(defconst isar-outline-heading-alist 552,17194
+(defconst isar-entity-regexp 516,16072
+(defconst isar-named-entity-regexp519,16168
+(defconst isar-named-entity-name-match-number524,16298
+(defconst isar-generic-expression527,16399
+(defconst isar-indent-any-regexp538,16633
+(defconst isar-indent-inner-regexp540,16726
+(defconst isar-indent-enclose-regexp542,16792
+(defconst isar-indent-open-regexp544,16908
+(defconst isar-indent-close-regexp546,17018
+(defconst isar-outline-regexp552,17155
+(defconst isar-outline-heading-end-regexp 556,17308
+(defconst isar-outline-heading-alist 558,17357
 
 isar/isar-unicode-tokens.el,1363
 (defgroup isabelle-tokens 25,672
@@ -644,11 +646,11 @@ lego/lego.el,1636
 (defun lego-state-preserving-p 248,8352
 (defvar lego-shell-current-line-width 264,9055
 (defun lego-shell-adjust-line-width 272,9362
-(defun lego-mode-config 291,10099
-(defun lego-equal-module-filename 359,12148
-(defun lego-shell-compute-new-files-list 365,12423
-(defun lego-shell-mode-config 375,12806
-(defun lego-goals-mode-config 422,14473
+(defun lego-mode-config 289,10063
+(defun lego-equal-module-filename 357,12112
+(defun lego-shell-compute-new-files-list 363,12387
+(defun lego-shell-mode-config 373,12770
+(defun lego-goals-mode-config 420,14437
 
 lego/lego-syntax.el,600
 (defconst lego-keywords-goal 15,358
@@ -862,33 +864,33 @@ plastic/plastic.el,2759
 (defun plastic-state-preserving-p 289,9136
 (defvar plastic-shell-current-line-width 312,10111
 (defun plastic-shell-adjust-line-width 320,10427
-(defun plastic-mode-config 347,11465
-(defun plastic-show-shell-buffer 436,14724
-(defun plastic-equal-module-filename 442,14827
-(defun plastic-shell-compute-new-files-list 448,15105
-(defun plastic-shell-mode-config 460,15499
-(defun plastic-goals-mode-config 508,17302
-(defun plastic-small-bar 520,17589
-(defun plastic-large-bar 522,17678
-(defun plastic-preprocessing 524,17816
-(defun plastic-all-ctxt 576,19619
-(defun plastic-send-one-undo 583,19788
-(defun plastic-minibuf-cmd 593,20094
-(defun plastic-minibuf 605,20566
-(defun plastic-synchro 612,20772
-(defun plastic-send-minibuf 617,20913
-(defun plastic-had-error 625,21221
-(defun plastic-reset-error 629,21396
-(defun plastic-call-if-no-error 632,21535
-(defun plastic-show-shell 637,21739
-(define-key plastic-keymap 642,21867
-(define-key plastic-keymap 643,21928
-(define-key plastic-keymap 644,21989
-(define-key plastic-keymap 645,22049
-(define-key plastic-keymap 646,22108
-(define-key plastic-keymap 647,22167
-(defalias 'proof-toolbar-command proof-toolbar-command
657,22416
-(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
658,22467
+(defun plastic-mode-config 345,11436
+(defun plastic-show-shell-buffer 434,14695
+(defun plastic-equal-module-filename 440,14798
+(defun plastic-shell-compute-new-files-list 446,15076
+(defun plastic-shell-mode-config 458,15470
+(defun plastic-goals-mode-config 506,17273
+(defun plastic-small-bar 518,17560
+(defun plastic-large-bar 520,17649
+(defun plastic-preprocessing 522,17787
+(defun plastic-all-ctxt 574,19590
+(defun plastic-send-one-undo 581,19759
+(defun plastic-minibuf-cmd 591,20065
+(defun plastic-minibuf 603,20537
+(defun plastic-synchro 610,20743
+(defun plastic-send-minibuf 615,20884
+(defun plastic-had-error 623,21192
+(defun plastic-reset-error 627,21367
+(defun plastic-call-if-no-error 630,21506
+(defun plastic-show-shell 635,21710
+(define-key plastic-keymap 640,21838
+(define-key plastic-keymap 641,21899
+(define-key plastic-keymap 642,21960
+(define-key plastic-keymap 643,22020
+(define-key plastic-keymap 644,22079
+(define-key plastic-keymap 645,22138
+(defalias 'proof-toolbar-command proof-toolbar-command
655,22387
+(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
656,22438
 
 plastic/plastic-syntax.el,648
 (defconst plastic-keywords-goal 18,536
@@ -913,17 +915,17 @@ generic/pg-assoc.el,81
 (defun proof-associated-windows 42,1160
 
 generic/pg-autotest.el,443
-(defvar pg-autotest-success 25,571
-(defun pg-autotest-find-file 29,655
-(defun pg-autotest-find-file-restart 36,935
-(defmacro pg-autotest 49,1383
-(defun pg-autotest-script-wholefile 63,1730
-(defun pg-autotest-retract-file 80,2350
-(defun pg-autotest-assert-processed 86,2486
-(defun pg-autotest-assert-unprocessed 93,2740
-(defun pg-autotest-message 100,3000
-(defun pg-autotest-quit-prover 107,3193
-(defun pg-autotest-finished 113,3374
+(defvar pg-autotest-success 26,572
+(defun pg-autotest-find-file 32,719
+(defun pg-autotest-find-file-restart 39,999
+(defmacro pg-autotest 52,1447
+(defun pg-autotest-script-wholefile 66,1797
+(defun pg-autotest-retract-file 83,2417
+(defun pg-autotest-assert-processed 89,2553
+(defun pg-autotest-assert-unprocessed 96,2807
+(defun pg-autotest-message 103,3067
+(defun pg-autotest-quit-prover 110,3260
+(defun pg-autotest-finished 116,3441
 
 generic/pg-custom.el,554
 (defpgcustom maths-menu-enable 36,1134
@@ -951,6 +953,15 @@ generic/pg-goals.el,285
 (defun pg-goals-display 77,2204
 (defun pg-goals-button-action 118,3508
 
+generic/pg-movie.el,244
+(defconst pg-movie-xml-header 27,800
+(defconst pg-movie-stylesheet 29,858
+(defvar pg-movie-frame 32,958
+(defun pg-movie-of-span 34,1011
+(defun pg-movie-of-region 58,1833
+(defun pg-movie-export 65,2023
+(defun pg-movie-export-from 85,2546
+
 generic/pg-pbrpm.el,1808
 (defvar pg-pbrpm-use-buffer-menu 41,1191
 (defvar pg-pbrpm-start-goal-regexp 44,1313
@@ -966,33 +977,33 @@ generic/pg-pbrpm.el,1808
 (defvar pg-pbrpm-windows-dialog-bug 77,2539
 (defvar pbrpm-menu-desc 78,2580
 (defun pg-pbrpm-erase-buffer-menu 80,2610
-(defun pg-pbrpm-menu-change-hook 87,2794
-(defun pg-pbrpm-create-reset-buffer-menu 105,3369
-(defun pg-pbrpm-analyse-goal-buffer 124,4211
-(defun pg-pbrpm-button-action 184,6609
-(defun pg-pbrpm-exists 191,6835
-(defun pg-pbrpm-eliminate-id 195,6947
-(defun pg-pbrpm-build-menu 203,7193
-(defun pg-pbrpm-setup-span 266,9513
-(defun pg-pbrpm-run-command 326,11828
-(defun pg-pbrpm-get-pos-info 359,13349
-(defun pg-pbrpm-get-region-info 401,14648
-(defun pg-pbrpm-auto-select-around-point 412,15060
-(defun pg-pbrpm-translate-position 427,15584
-(defun pg-pbrpm-process-click 435,15841
-(defvar pg-pbrpm-remember-region-selected-region 455,16866
-(defvar pg-pbrpm-regions-list 456,16920
-(defun pg-pbrpm-erase-regions-list 458,16956
-(defun pg-pbrpm-filter-regions-list 467,17264
-(defface pg-pbrpm-multiple-selection-face474,17527
-(defface pg-pbrpm-menu-input-face482,17729
-(defun pg-pbrpm-do-remember-region 490,17919
-(defun pg-pbrpm-remember-region-drag-up-hook 511,18767
-(defun pg-pbrpm-remember-region-click-hook 515,18938
-(defun pg-pbrpm-remember-region 520,19123
-(defun pg-pbrpm-process-region 534,19837
-(defun pg-pbrpm-process-regions-list 552,20566
-(defun pg-pbrpm-region-expression 556,20749
+(defun pg-pbrpm-menu-change-hook 86,2782
+(defun pg-pbrpm-create-reset-buffer-menu 104,3357
+(defun pg-pbrpm-analyse-goal-buffer 123,4199
+(defun pg-pbrpm-button-action 183,6604
+(defun pg-pbrpm-exists 190,6830
+(defun pg-pbrpm-eliminate-id 194,6942
+(defun pg-pbrpm-build-menu 202,7188
+(defun pg-pbrpm-setup-span 265,9508
+(defun pg-pbrpm-run-command 325,11823
+(defun pg-pbrpm-get-pos-info 358,13344
+(defun pg-pbrpm-get-region-info 400,14643
+(defun pg-pbrpm-auto-select-around-point 411,15055
+(defun pg-pbrpm-translate-position 426,15579
+(defun pg-pbrpm-process-click 434,15836
+(defvar pg-pbrpm-remember-region-selected-region 454,16861
+(defvar pg-pbrpm-regions-list 455,16915
+(defun pg-pbrpm-erase-regions-list 457,16951
+(defun pg-pbrpm-filter-regions-list 466,17259
+(defface pg-pbrpm-multiple-selection-face473,17522
+(defface pg-pbrpm-menu-input-face481,17724
+(defun pg-pbrpm-do-remember-region 489,17914
+(defun pg-pbrpm-remember-region-drag-up-hook 510,18762
+(defun pg-pbrpm-remember-region-click-hook 514,18933
+(defun pg-pbrpm-remember-region 519,19118
+(defun pg-pbrpm-process-region 533,19832
+(defun pg-pbrpm-process-regions-list 551,20561
+(defun pg-pbrpm-region-expression 555,20744
 
 generic/pg-pgip.el,2931
 (defalias 'pg-pgip-debug pg-pgip-debug
38,1032
@@ -1090,11 +1101,11 @@ generic/pg-response.el,1292
 (defun pg-response-warning 324,11041
 (defun proof-next-error 339,11445
 (defun pg-response-has-error-location 421,14406
-(defvar proof-trace-last-fontify-pos 444,15238
-(defun proof-trace-fontify-pos 446,15281
-(defun proof-trace-buffer-display 454,15594
-(defun proof-trace-buffer-finish 465,15938
-(defun pg-thms-buffer-clear 483,16281
+(defvar proof-trace-last-fontify-pos 442,15197
+(defun proof-trace-fontify-pos 444,15240
+(defun proof-trace-buffer-display 452,15553
+(defun proof-trace-buffer-finish 463,15897
+(defun pg-thms-buffer-clear 481,16240
 
 generic/pg-thymodes.el,152
 (defmacro pg-defthymode 23,499
@@ -1103,85 +1114,87 @@ generic/pg-thymodes.el,152
 (defun pg-modesym 82,2548
 (defun pg-modesymval 86,2662
 
-generic/pg-user.el,3332
-(defun proof-script-new-command-advance 41,1156
-(defun proof-maybe-follow-locked-end 84,2918
-(defun proof-goto-command-start 111,3766
-(defun proof-goto-command-end 134,4713
-(defun proof-goto-point 157,5238
-(defun proof-assert-next-command-interactive 171,5672
-(defun proof-assert-until-point-interactive 183,6158
-(defun proof-process-buffer 189,6388
-(defun proof-undo-last-successful-command 204,6765
-(defun proof-undo-and-delete-last-successful-command 209,6927
-(defun proof-undo-last-successful-command-1 222,7481
-(defun proof-retract-buffer 239,8100
-(defun proof-retract-current-goal 248,8384
-(defun proof-mouse-goto-point 267,8904
-(defvar proof-minibuffer-history 282,9180
-(defun proof-minibuffer-cmd 285,9275
-(defun proof-frob-locked-end 329,10897
-(defmacro proof-if-setting-configured 390,12835
-(defmacro proof-define-assistant-command 398,13104
-(defmacro proof-define-assistant-command-witharg 411,13559
-(defun proof-issue-new-command 431,14381
-(defun proof-cd-sync 477,15878
-(defun proof-electric-terminator-enable 531,17598
-(defun proof-electric-terminator 539,17888
-(defun proof-add-completions 565,18710
-(defun proof-script-complete 590,19617
-(defun pg-copy-span-contents 604,19926
-(defun pg-numth-span-higher-or-lower 621,20484
-(defun pg-control-span-of 647,21230
-(defun pg-move-span-contents 653,21434
-(defun pg-fixup-children-spans 705,23610
-(defun pg-move-region-down 715,23867
-(defun pg-move-region-up 724,24160
-(defun proof-forward-command 754,24988
-(defun proof-backward-command 775,25709
-(defun pg-pos-for-event 797,26053
-(defun pg-span-for-event 803,26274
-(defun pg-span-context-menu 807,26418
-(defun pg-toggle-visibility 822,26866
-(defun pg-create-in-span-context-menu 831,27173
-(defun pg-span-undo 860,28387
-(defun pg-goals-buffers-hint 906,29789
-(defun pg-slow-fontify-tracing-hint 910,29971
-(defun pg-response-buffers-hint 914,30142
-(defun pg-jump-to-end-hint 926,30557
-(defun pg-processing-complete-hint 930,30686
-(defun pg-next-error-hint 947,31385
-(defun pg-hint 952,31537
-(defun pg-identifier-under-mouse-query 968,32127
-(defun pg-identifier-near-point-query 977,32370
-(defvar proof-query-identifier-collection 1004,33213
-(defvar proof-query-identifier-history 1005,33260
-(defun proof-query-identifier 1007,33305
-(defun pg-identifier-query 1017,33574
-(defun proof-imenu-enable 1048,34652
-(defvar pg-input-ring 1084,35974
-(defvar pg-input-ring-index 1087,36031
-(defvar pg-stored-incomplete-input 1090,36103
-(defun pg-previous-input 1093,36206
-(defun pg-next-input 1107,36663
-(defun pg-delete-input 1112,36785
-(defun pg-get-old-input 1125,37123
-(defun pg-restore-input 1139,37514
-(defun pg-search-start 1150,37804
-(defun pg-regexp-arg 1162,38296
-(defun pg-search-arg 1174,38744
-(defun pg-previous-matching-input-string-position 1188,39161
-(defun pg-previous-matching-input 1215,40326
-(defun pg-next-matching-input 1234,41176
-(defvar pg-matching-input-from-input-string 1242,41559
-(defun pg-previous-matching-input-from-input 1246,41673
-(defun pg-next-matching-input-from-input 1264,42438
-(defun pg-add-to-input-history 1275,42817
-(defun pg-remove-from-input-history 1287,43270
-(defun  pg-clear-input-ring 1298,43650
-(define-key proof-mode-map 1312,44000
-(define-key proof-mode-map 1313,44060
-(defun pg-protected-undo 1315,44132
+generic/pg-user.el,3404
+(defun proof-script-new-command-advance 42,1230
+(defun proof-maybe-follow-locked-end 85,2992
+(defun proof-goto-command-start 112,3840
+(defun proof-goto-command-end 135,4787
+(defun proof-goto-point 158,5312
+(defun proof-assert-next-command-interactive 172,5746
+(defun proof-assert-until-point-interactive 184,6232
+(defun proof-process-buffer 190,6462
+(defun proof-undo-last-successful-command 205,6839
+(defun proof-undo-and-delete-last-successful-command 210,7001
+(defun proof-undo-last-successful-command-1 223,7555
+(defun proof-retract-buffer 240,8174
+(defun proof-retract-current-goal 249,8458
+(defun proof-mouse-goto-point 268,8978
+(defvar proof-minibuffer-history 283,9254
+(defun proof-minibuffer-cmd 286,9349
+(defun proof-frob-locked-end 330,10971
+(defmacro proof-if-setting-configured 391,12909
+(defmacro proof-define-assistant-command 399,13178
+(defmacro proof-define-assistant-command-witharg 412,13633
+(defun proof-issue-new-command 432,14455
+(defun proof-cd-sync 478,15952
+(defun proof-electric-terminator-enable 532,17672
+(defun proof-electric-terminator 540,17962
+(defun proof-add-completions 566,18785
+(defun proof-script-complete 591,19674
+(defun pg-copy-span-contents 605,19983
+(defun pg-numth-span-higher-or-lower 622,20541
+(defun pg-control-span-of 648,21287
+(defun pg-move-span-contents 654,21491
+(defun pg-fixup-children-spans 706,23667
+(defun pg-move-region-down 716,23924
+(defun pg-move-region-up 725,24217
+(defun proof-forward-command 755,25045
+(defun proof-backward-command 776,25766
+(defun pg-pos-for-event 798,26110
+(defun pg-span-for-event 804,26331
+(defun pg-span-context-menu 808,26475
+(defun pg-toggle-visibility 823,26923
+(defun pg-create-in-span-context-menu 832,27230
+(defun pg-span-undo 861,28444
+(defun pg-goals-buffers-hint 907,29846
+(defun pg-slow-fontify-tracing-hint 911,30028
+(defun pg-response-buffers-hint 915,30199
+(defun pg-jump-to-end-hint 927,30614
+(defun pg-processing-complete-hint 931,30743
+(defun pg-next-error-hint 947,31429
+(defun pg-hint 952,31581
+(defun pg-identifier-under-mouse-query 968,32171
+(defun pg-identifier-near-point-query 977,32414
+(defvar proof-query-identifier-collection 1004,33257
+(defvar proof-query-identifier-history 1005,33304
+(defun proof-query-identifier 1007,33349
+(defun pg-identifier-query 1017,33618
+(defun proof-imenu-enable 1048,34696
+(defvar pg-input-ring 1084,36018
+(defvar pg-input-ring-index 1087,36075
+(defvar pg-stored-incomplete-input 1090,36147
+(defun pg-previous-input 1093,36250
+(defun pg-next-input 1107,36707
+(defun pg-delete-input 1112,36829
+(defun pg-get-old-input 1125,37167
+(defun pg-restore-input 1139,37558
+(defun pg-search-start 1150,37848
+(defun pg-regexp-arg 1162,38340
+(defun pg-search-arg 1174,38788
+(defun pg-previous-matching-input-string-position 1188,39205
+(defun pg-previous-matching-input 1215,40370
+(defun pg-next-matching-input 1234,41220
+(defvar pg-matching-input-from-input-string 1242,41603
+(defun pg-previous-matching-input-from-input 1246,41717
+(defun pg-next-matching-input-from-input 1264,42482
+(defun pg-add-to-input-history 1275,42861
+(defun pg-remove-from-input-history 1287,43314
+(defun  pg-clear-input-ring 1298,43694
+(define-key proof-mode-map 1315,44164
+(define-key proof-mode-map 1316,44224
+(defun pg-protected-undo 1318,44296
+(defun pg-protected-undo-1 1346,45496
+(defun next-undo-elt 1380,47074
 
 generic/pg-vars.el,1452
 (defvar proof-assistant-cusgrp 22,382
@@ -1223,38 +1236,38 @@ generic/pg-vars.el,1452
 generic/pg-xml.el,1177
 (defalias 'pg-xml-error pg-xml-error
18,381
 (defun pg-xml-parse-string 41,1023
-(defun pg-xml-parse-buffer 52,1349
-(defun pg-xml-get-attr 71,1964
-(defun pg-xml-child-elts 79,2266
-(defun pg-xml-child-elt 84,2471
-(defun pg-xml-get-child 92,2753
-(defun pg-xml-get-text-content 102,3120
-(defmacro pg-xml-attr 113,3470
-(defmacro pg-xml-node 115,3532
-(defconst pg-xml-header118,3624
-(defun pg-xml-string-of 122,3700
-(defun pg-xml-output-internal 133,4067
-(defun pg-xml-cdata 167,5206
-(defsubst pg-pgip-get-area 175,5399
-(defun pg-pgip-get-icon 178,5516
-(defsubst pg-pgip-get-name 182,5664
-(defsubst pg-pgip-get-version 185,5781
-(defsubst pg-pgip-get-descr 188,5904
-(defsubst pg-pgip-get-thmname 191,6023
-(defsubst pg-pgip-get-thyname 194,6146
-(defsubst pg-pgip-get-url 197,6269
-(defsubst pg-pgip-get-srcid 200,6384
-(defsubst pg-pgip-get-proverid 203,6503
-(defsubst pg-pgip-get-symname 206,6628
-(defsubst pg-pgip-get-prefcat 209,6748
-(defsubst pg-pgip-get-default 212,6876
-(defsubst pg-pgip-get-objtype 215,6999
-(defsubst pg-pgip-get-value 218,7122
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
221,7192
-(defun pg-pgip-get-pgmltext 223,7251
+(defun pg-xml-parse-buffer 51,1335
+(defun pg-xml-get-attr 70,1950
+(defun pg-xml-child-elts 78,2252
+(defun pg-xml-child-elt 83,2457
+(defun pg-xml-get-child 91,2739
+(defun pg-xml-get-text-content 101,3106
+(defmacro pg-xml-attr 112,3456
+(defmacro pg-xml-node 114,3518
+(defconst pg-xml-header117,3610
+(defun pg-xml-string-of 121,3686
+(defun pg-xml-output-internal 132,4053
+(defun pg-xml-cdata 166,5192
+(defsubst pg-pgip-get-area 174,5385
+(defun pg-pgip-get-icon 177,5502
+(defsubst pg-pgip-get-name 181,5650
+(defsubst pg-pgip-get-version 184,5767
+(defsubst pg-pgip-get-descr 187,5890
+(defsubst pg-pgip-get-thmname 190,6009
+(defsubst pg-pgip-get-thyname 193,6132
+(defsubst pg-pgip-get-url 196,6255
+(defsubst pg-pgip-get-srcid 199,6370
+(defsubst pg-pgip-get-proverid 202,6489
+(defsubst pg-pgip-get-symname 205,6614
+(defsubst pg-pgip-get-prefcat 208,6734
+(defsubst pg-pgip-get-default 211,6862
+(defsubst pg-pgip-get-objtype 214,6985
+(defsubst pg-pgip-get-value 217,7108
+(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7178
+(defun pg-pgip-get-pgmltext 222,7237
 
 generic/proof-autoloads.el,45
-(defsubst proof-shell-live-buffer 633,20742
+(defsubst proof-shell-live-buffer 652,21076
 
 generic/proof-auxmodes.el,149
 (defun proof-mmm-support-available 20,489
@@ -1518,39 +1531,39 @@ generic/proof-menu.el,2026
 (defun proof-quick-opts-reset 554,20345
 (defconst proof-config-menu566,20613
 (defconst proof-advanced-menu573,20792
-(defvar proof-menu586,21224
-(defun proof-main-menu 595,21506
-(defun proof-aux-menu 607,21845
-(defun proof-menu-define-favourites-menu 623,22191
-(defun proof-def-favourite 643,22840
-(defvar proof-make-favourite-cmd-history 666,23811
-(defvar proof-make-favourite-menu-history 669,23896
-(defun proof-save-favourites 672,23982
-(defun proof-del-favourite 677,24130
-(defun proof-read-favourite 694,24686
-(defun proof-add-favourite 718,25462
-(defun proof-menu-define-settings-menu 745,26507
-(defun proof-menu-entry-name 778,27638
-(defun proof-menu-entry-for-setting 788,27988
-(defun proof-settings-vars 807,28520
-(defun proof-settings-changed-from-defaults-p 812,28697
-(defun proof-settings-changed-from-saved-p 816,28803
-(defun proof-settings-save 820,28906
-(defun proof-settings-reset 825,29073
-(defun proof-assistant-invisible-command-ifposs 830,29236
-(defun proof-maybe-askprefs 852,30206
-(defun proof-assistant-settings-cmd 858,30398
-(defvar proof-assistant-format-table875,31053
-(defun proof-assistant-format-bool 883,31421
-(defun proof-assistant-format-int 886,31534
-(defun proof-assistant-format-string 889,31626
-(defun proof-assistant-format 892,31724
+(defvar proof-menu593,21512
+(defun proof-main-menu 602,21794
+(defun proof-aux-menu 614,22133
+(defun proof-menu-define-favourites-menu 630,22479
+(defun proof-def-favourite 650,23128
+(defvar proof-make-favourite-cmd-history 673,24099
+(defvar proof-make-favourite-menu-history 676,24184
+(defun proof-save-favourites 679,24270
+(defun proof-del-favourite 684,24418
+(defun proof-read-favourite 701,24974
+(defun proof-add-favourite 725,25750
+(defun proof-menu-define-settings-menu 752,26795
+(defun proof-menu-entry-name 785,27926
+(defun proof-menu-entry-for-setting 795,28276
+(defun proof-settings-vars 814,28808
+(defun proof-settings-changed-from-defaults-p 819,28985
+(defun proof-settings-changed-from-saved-p 823,29091
+(defun proof-settings-save 827,29194
+(defun proof-settings-reset 832,29361
+(defun proof-assistant-invisible-command-ifposs 837,29524
+(defun proof-maybe-askprefs 859,30494
+(defun proof-assistant-settings-cmd 865,30686
+(defvar proof-assistant-format-table882,31341
+(defun proof-assistant-format-bool 890,31709
+(defun proof-assistant-format-int 893,31822
+(defun proof-assistant-format-string 896,31914
+(defun proof-assistant-format 899,32012
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 39,1466
 (defun proof-mmm-enable 54,2005
 
-generic/proof-script.el,5455
+generic/proof-script.el,5456
 (deflocal proof-active-buffer-fake-minor-mode 44,1308
 (deflocal proof-script-buffer-file-name 47,1434
 (deflocal pg-script-portions 54,1844
@@ -1597,79 +1610,79 @@ generic/proof-script.el,5455
 (defun pg-remove-element 491,17547
 (defun pg-get-element 499,17850
 (defun pg-add-element 509,18166
-(defun pg-set-element-span-invisible 551,19961
-(defun pg-open-invisible-span 555,20121
-(defun pg-make-element-invisible 560,20292
-(defun pg-make-element-visible 565,20503
-(defun pg-toggle-element-span-visibility 570,20697
-(defun pg-toggle-element-visibility 576,20861
-(defun pg-show-all-portions 582,21124
-(defun pg-show-all-proofs 601,21832
-(defun pg-hide-all-proofs 606,21960
-(defun pg-add-proof-element 611,22091
-(defun pg-span-name 626,22862
-(defvar pg-span-context-menu-keymap647,23562
-(defun pg-last-output-displayform 654,23800
-(defun pg-set-span-helphighlights 672,24496
-(defun pg-delete-self-modification-hook 713,26196
-(defun proof-complete-buffer-atomic 724,26469
-(defun proof-register-possibly-new-processed-file766,28389
-(defun proof-inform-prover-file-retracted 812,30226
-(defun proof-auto-retract-dependencies 832,31077
-(defun proof-unregister-buffer-file-name 886,33627
-(defun proof-protected-process-or-retract 932,35452
-(defun proof-deactivate-scripting-auto 959,36622
-(defun proof-deactivate-scripting 968,36980
-(defun proof-activate-scripting 1101,42236
-(defun proof-toggle-active-scripting 1216,47350
-(defun proof-done-advancing 1255,48595
-(defun proof-done-advancing-comment 1334,51580
-(defun proof-done-advancing-save 1368,52956
-(defun proof-make-goalsave 1456,56321
-(defun proof-get-name-from-goal 1474,57153
-(defun proof-done-advancing-autosave 1494,58178
-(defun proof-done-advancing-other 1559,60722
-(defun proof-segment-up-to-parser 1588,61652
-(defun proof-script-generic-parse-find-comment-end 1657,63922
-(defun proof-script-generic-parse-cmdend 1666,64336
-(defun proof-script-generic-parse-cmdstart 1717,66232
-(defun proof-script-generic-parse-sexp 1756,67832
-(defun proof-semis-to-vanillas 1768,68298
-(defun proof-script-next-command-advance 1817,69820
-(defun proof-assert-until-point 1836,70319
-(defun proof-assert-electric-terminator 1851,70912
-(defun proof-assert-semis 1886,72296
-(defun proof-retract-before-change 1900,73002
-(defun proof-inside-comment 1912,73403
-(defun proof-inside-string 1918,73577
-(defun proof-insert-pbp-command 1933,73858
-(defun proof-insert-sendback-command 1948,74359
-(defun proof-done-retracting 1974,75262
-(defun proof-setup-retract-action 2009,76703
-(defun proof-last-goal-or-goalsave 2019,77189
-(defun proof-retract-target 2043,78101
-(defun proof-retract-until-point-interactive 2124,81485
-(defun proof-retract-until-point 2132,81870
-(define-derived-mode proof-mode 2179,83705
-(defun proof-script-set-visited-file-name 2213,84976
-(defun proof-script-set-buffer-hooks 2235,85989
-(defun proof-script-kill-buffer-fn 2243,86407
-(defun proof-config-done-related 2275,87724
-(defun proof-generic-goal-command-p 2343,90247
-(defun proof-generic-state-preserving-p 2348,90460
-(defun proof-generic-count-undos 2357,90977
-(defun proof-generic-find-and-forget 2386,92030
-(defconst proof-script-important-settings2437,93802
-(defun proof-config-done 2452,94348
-(defun proof-setup-parsing-mechanism 2510,96248
-(defun proof-setup-imenu 2534,97327
-(deflocal proof-segment-up-to-cache 2558,98101
-(deflocal proof-segment-up-to-cache-start 2559,98142
-(deflocal proof-last-edited-low-watermark 2560,98187
-(defun proof-segment-up-to-using-cache 2570,98674
-(defun proof-segment-cache-contents-for 2599,99822
-(defun proof-script-after-change-function 2611,100191
-(defun proof-script-set-after-change-functions 2623,100698
+(defun pg-set-element-span-invisible 557,20148
+(defun pg-open-invisible-span 561,20308
+(defun pg-make-element-invisible 566,20479
+(defun pg-make-element-visible 571,20690
+(defun pg-toggle-element-span-visibility 576,20884
+(defun pg-toggle-element-visibility 582,21048
+(defun pg-show-all-portions 588,21311
+(defun pg-show-all-proofs 607,22019
+(defun pg-hide-all-proofs 612,22147
+(defun pg-add-proof-element 617,22278
+(defun pg-span-name 632,23049
+(defvar pg-span-context-menu-keymap653,23749
+(defun pg-last-output-displayform 660,23987
+(defun pg-set-span-helphighlights 685,24974
+(defun pg-delete-self-modification-hook 734,26799
+(defun proof-complete-buffer-atomic 745,27072
+(defun proof-register-possibly-new-processed-file786,28980
+(defun proof-inform-prover-file-retracted 832,30817
+(defun proof-auto-retract-dependencies 852,31668
+(defun proof-unregister-buffer-file-name 906,34218
+(defun proof-protected-process-or-retract 952,36043
+(defun proof-deactivate-scripting-auto 979,37213
+(defun proof-deactivate-scripting 988,37571
+(defun proof-activate-scripting 1121,42827
+(defun proof-toggle-active-scripting 1236,47941
+(defun proof-done-advancing 1275,49186
+(defun proof-done-advancing-comment 1354,52171
+(defun proof-done-advancing-save 1388,53547
+(defun proof-make-goalsave 1476,56912
+(defun proof-get-name-from-goal 1494,57744
+(defun proof-done-advancing-autosave 1514,58769
+(defun proof-done-advancing-other 1579,61313
+(defun proof-segment-up-to-parser 1608,62243
+(defun proof-script-generic-parse-find-comment-end 1677,64513
+(defun proof-script-generic-parse-cmdend 1686,64927
+(defun proof-script-generic-parse-cmdstart 1737,66823
+(defun proof-script-generic-parse-sexp 1776,68423
+(defun proof-semis-to-vanillas 1788,68889
+(defun proof-script-next-command-advance 1837,70411
+(defun proof-assert-until-point 1856,70910
+(defun proof-assert-electric-terminator 1871,71503
+(defun proof-assert-semis 1906,72887
+(defun proof-retract-before-change 1920,73593
+(defun proof-inside-comment 1932,73994
+(defun proof-inside-string 1938,74168
+(defun proof-insert-pbp-command 1953,74449
+(defun proof-insert-sendback-command 1968,74950
+(defun proof-done-retracting 1994,75853
+(defun proof-setup-retract-action 2029,77294
+(defun proof-last-goal-or-goalsave 2039,77780
+(defun proof-retract-target 2063,78692
+(defun proof-retract-until-point-interactive 2144,82076
+(defun proof-retract-until-point 2152,82461
+(define-derived-mode proof-mode 2199,84296
+(defun proof-script-set-visited-file-name 2233,85567
+(defun proof-script-set-buffer-hooks 2255,86580
+(defun proof-script-kill-buffer-fn 2263,86998
+(defun proof-config-done-related 2295,88315
+(defun proof-generic-goal-command-p 2363,90838
+(defun proof-generic-state-preserving-p 2368,91051
+(defun proof-generic-count-undos 2377,91568
+(defun proof-generic-find-and-forget 2406,92621
+(defconst proof-script-important-settings2457,94393
+(defun proof-config-done 2472,94939
+(defun proof-setup-parsing-mechanism 2530,96839
+(defun proof-setup-imenu 2554,97918
+(deflocal proof-segment-up-to-cache 2578,98692
+(deflocal proof-segment-up-to-cache-start 2579,98733
+(deflocal proof-last-edited-low-watermark 2580,98778
+(defun proof-segment-up-to-using-cache 2590,99265
+(defun proof-segment-cache-contents-for 2619,100413
+(defun proof-script-after-change-function 2631,100782
+(defun proof-script-set-after-change-functions 2643,101289
 
 generic/proof-shell.el,3793
 (defvar proof-marker 35,808
@@ -1904,7 +1917,7 @@ generic/proof-useropts.el,1552
 (defcustom proof-rsh-command 351,13186
 (defcustom proof-disappearing-proofs 367,13736
 (defcustom proof-full-annotation 372,13897
-(defcustom proof-minibuffer-messages 381,14269
+(defcustom proof-minibuffer-messages 381,14267
 
 generic/proof-utils.el,2073
 (defmacro deflocal 61,1871
@@ -2121,7 +2134,7 @@ lib/scomint.el,876
 (defun scomint-output-filter 291,11525
 (defun scomint-interrupt-process 363,14257
 
-lib/span.el,1315
+lib/span.el,1361
 (defalias 'span-start span-start
22,609
 (defalias 'span-end span-end
23,647
 (defalias 'span-set-property span-set-property
24,681
@@ -2141,37 +2154,38 @@ lib/span.el,1315
 (defsubst span-delete 87,2846
 (defsubst span-mapcar-spans 94,3068
 (defsubst span-mapc-spans 98,3243
-(defun span-at-before 102,3414
-(defsubst prev-span 119,4138
-(defsubst next-span 125,4291
-(defsubst span-live-p 131,4505
-(defsubst span-raise 137,4671
-(defsubst span-string 141,4804
-(defsubst set-span-properties 146,4964
-(defsubst span-find-span 152,5158
-(defsubst span-at-event 160,5470
-(defun fold-spans 166,5667
-(defsubst span-detached-p 180,6200
-(defsubst set-span-face 184,6316
-(defsubst set-span-keymap 188,6414
-(defsubst span-delete-spans 196,6583
-(defsubst span-property-safe 200,6745
-(defsubst span-set-start 204,6882
-(defsubst span-set-end 208,7014
+(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
 
 lib/texi-docstring-magic.el,584
 (defun texi-docstring-magic-find-face 88,3027
 (defun texi-docstring-magic-splice-sep 93,3192
 (defconst texi-docstring-magic-munge-table103,3497
 (defun texi-docstring-magic-untabify 193,7260
-(defun texi-docstring-magic-munge-docstring 203,7575
-(defun texi-docstring-magic-texi 242,8856
-(defun texi-docstring-magic-format-default 255,9296
-(defun texi-docstring-magic-texi-for 271,9929
-(defconst texi-docstring-magic-comment329,11888
-(defun texi-docstring-magic 335,12042
-(defun texi-docstring-magic-face-at-point 369,13121
-(defun texi-docstring-magic-insert-magic 384,13644
+(defun texi-docstring-magic-munge-docstring 200,7458
+(defun texi-docstring-magic-texi 239,8739
+(defun texi-docstring-magic-format-default 252,9179
+(defun texi-docstring-magic-texi-for 268,9812
+(defconst texi-docstring-magic-comment326,11771
+(defun texi-docstring-magic 332,11925
+(defun texi-docstring-magic-face-at-point 366,13004
+(defun texi-docstring-magic-insert-magic 381,13527
 
 lib/unicode-chars.el,80
 (defvar unicode-chars-alist12,348
@@ -2244,54 +2258,54 @@ lib/unicode-tokens.el,5902
 (defun unicode-tokens-delete-backward-char 746,27276
 (defun unicode-tokens-delete-char 757,27657
 (defun unicode-tokens-delete-backward-1 768,28011
-(defun unicode-tokens-delete-1 785,28614
-(defun unicode-tokens-prev-token 801,29158
-(defun unicode-tokens-rotate-token-forward 809,29455
-(defun unicode-tokens-rotate-token-backward 836,30345
-(defun unicode-tokens-replace-shortcut-match 841,30547
-(defun unicode-tokens-replace-shortcuts 850,30917
-(defun unicode-tokens-replace-unicode-match 864,31515
-(defun unicode-tokens-replace-unicode 871,31816
-(defun unicode-tokens-copy-token 888,32415
-(define-button-type 'unicode-tokens-listunicode-tokens-list
895,32636
-(defun unicode-tokens-list-tokens 901,32840
-(defun unicode-tokens-list-shortcuts 940,34024
-(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
958,34662
-(defun unicode-tokens-encode-in-temp-buffer 960,34735
-(defun unicode-tokens-encode 978,35391
-(defun unicode-tokens-encode-str 984,35627
-(defun unicode-tokens-copy 988,35789
-(defun unicode-tokens-paste 997,36195
-(defvar unicode-tokens-highlight-unicode 1016,36916
-(defconst unicode-tokens-unicode-highlight-patterns1019,37008
-(defun unicode-tokens-highlight-unicode 1023,37177
-(defun unicode-tokens-highlight-unicode-setkeywords 1035,37640
-(defun unicode-tokens-initialise 1047,38009
-(defvar unicode-tokens-mode-map 1067,38680
-(defvar unicode-tokens-display-table 1070,38777
-(define-minor-mode unicode-tokens-mode1077,39029
-(defun unicode-tokens-set-font-var 1210,43512
-(defun unicode-tokens-set-font-var-aux 1226,44001
-(defun unicode-tokens-mouse-set-font 1258,45282
-(defsubst unicode-tokens-face-font-sym 1271,45796
-(defun unicode-tokens-set-font-restart 1275,45976
-(defun unicode-tokens-save-fonts 1286,46286
-(defun unicode-tokens-custom-save-faces 1294,46542
-(define-key unicode-tokens-mode-map1311,46998
-(define-key unicode-tokens-mode-map1314,47105
-(defvar unicode-tokens-quail-translation-keymap 1318,47195
-(define-key unicode-tokens-quail-translation-keymap 1324,47361
-(defun unicode-tokens-quail-delete-last-char 1328,47496
-(define-key unicode-tokens-mode-map 1344,47946
-(define-key unicode-tokens-mode-map 1346,48038
-(define-key unicode-tokens-mode-map1348,48129
-(define-key unicode-tokens-mode-map1350,48235
-(define-key unicode-tokens-mode-map1353,48350
-(define-key unicode-tokens-mode-map1355,48459
-(define-key unicode-tokens-mode-map1357,48567
-(define-key unicode-tokens-mode-map1359,48673
-(defun unicode-tokens-customize-submenu 1367,48797
-(defun unicode-tokens-define-menu 1374,49020
+(defun unicode-tokens-delete-1 785,28615
+(defun unicode-tokens-prev-token 801,29159
+(defun unicode-tokens-rotate-token-forward 809,29456
+(defun unicode-tokens-rotate-token-backward 836,30346
+(defun unicode-tokens-replace-shortcut-match 841,30548
+(defun unicode-tokens-replace-shortcuts 850,30918
+(defun unicode-tokens-replace-unicode-match 864,31516
+(defun unicode-tokens-replace-unicode 871,31817
+(defun unicode-tokens-copy-token 888,32416
+(define-button-type 'unicode-tokens-listunicode-tokens-list
895,32637
+(defun unicode-tokens-list-tokens 901,32841
+(defun unicode-tokens-list-shortcuts 940,34025
+(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
958,34663
+(defun unicode-tokens-encode-in-temp-buffer 960,34736
+(defun unicode-tokens-encode 978,35392
+(defun unicode-tokens-encode-str 984,35628
+(defun unicode-tokens-copy 988,35790
+(defun unicode-tokens-paste 997,36196
+(defvar unicode-tokens-highlight-unicode 1016,36917
+(defconst unicode-tokens-unicode-highlight-patterns1019,37009
+(defun unicode-tokens-highlight-unicode 1023,37178
+(defun unicode-tokens-highlight-unicode-setkeywords 1035,37641
+(defun unicode-tokens-initialise 1047,38010
+(defvar unicode-tokens-mode-map 1067,38681
+(defvar unicode-tokens-display-table 1070,38778
+(define-minor-mode unicode-tokens-mode1077,39030
+(defun unicode-tokens-set-font-var 1210,43513
+(defun unicode-tokens-set-font-var-aux 1226,44002
+(defun unicode-tokens-mouse-set-font 1258,45283
+(defsubst unicode-tokens-face-font-sym 1271,45797
+(defun unicode-tokens-set-font-restart 1275,45977
+(defun unicode-tokens-save-fonts 1286,46287
+(defun unicode-tokens-custom-save-faces 1294,46543
+(define-key unicode-tokens-mode-map1311,46999
+(define-key unicode-tokens-mode-map1314,47106
+(defvar unicode-tokens-quail-translation-keymap 1318,47196
+(define-key unicode-tokens-quail-translation-keymap 1325,47388
+(defun unicode-tokens-quail-delete-last-char 1329,47523
+(define-key unicode-tokens-mode-map 1344,47950
+(define-key unicode-tokens-mode-map 1346,48042
+(define-key unicode-tokens-mode-map1348,48133
+(define-key unicode-tokens-mode-map1350,48239
+(define-key unicode-tokens-mode-map1353,48354
+(define-key unicode-tokens-mode-map1355,48463
+(define-key unicode-tokens-mode-map1357,48571
+(define-key unicode-tokens-mode-map1359,48677
+(defun unicode-tokens-customize-submenu 1367,48801
+(defun unicode-tokens-define-menu 1374,49024
 
 mmm/mmm-auto.el,343
 (defvar mmm-autoloaded-classes67,2676
@@ -2299,9 +2313,9 @@ mmm/mmm-auto.el,343
 (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 155,5979
-(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6383
-(defun mmm-add-find-file-hook 168,6443
+(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
 
 mmm/mmm-class.el,415
 (defun mmm-get-class-spec 42,1296
@@ -2425,25 +2439,25 @@ mmm/mmm-region.el,1643
 (defun mmm-get-face 459,17444
 (defun mmm-clear-overlays 470,17736
 (defun mmm-update-mode-info 486,18201
-(defun mmm-update-submode-region 572,21856
-(defun mmm-add-hooks 589,22586
-(defun mmm-remove-hooks 592,22683
-(defun mmm-get-local-variables-list 598,22810
-(defun mmm-get-locals 618,23506
-(defun mmm-get-saved-local 631,24003
-(defun mmm-set-local-variables 635,24168
-(defun mmm-get-saved-local-variables 646,24546
-(defun mmm-save-changed-local-variables 654,24821
-(defun mmm-clear-local-variables 673,25525
-(defun mmm-enable-font-lock 684,25790
-(defun mmm-update-font-lock-buffer 692,26050
-(defun mmm-refontify-maybe 705,26461
-(defun mmm-submode-changes-in 720,26941
-(defun mmm-regions-in 731,27298
-(defun mmm-regions-alist 745,27776
-(defun mmm-fontify-region 762,28303
-(defun mmm-fontify-region-list 782,29299
-(defun mmm-beginning-of-syntax 804,30047
+(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
 
 mmm/mmm-rpm.el,154
 (defconst mmm-rpm-sh-start-tags48,1618
@@ -2538,9 +2552,9 @@ mmm/mmm-vars.el,2668
 (defun mmm-get-all-classes 1042,38224
 
 doc/ProofGeneral.texi,6347
-@node Top164,4936
-@node Preface202,6090
-@node News for Version 4.0News for Version 4.0
225,6679
+@node Top164,4934
+@node Preface202,6088
+@node News for Version 4.0News for Version 4.0
225,6677
 @node Future246,7472
 @node Credits275,8807
 @node Introducing Proof GeneralIntroducing Proof General
387,12712
@@ -2548,98 +2562,98 @@ doc/ProofGeneral.texi,6347
 @node Quick start guideQuick start guide
456,15139
 @node Features of Proof GeneralFeatures of Proof General
500,17260
 @node Supported proof assistantsSupported proof assistants
589,21197
-@node Prerequisites for this manualPrerequisites for this manual
638,23086
-@node Organization of this manualOrganization of this manual
682,24705
-@node Basic Script ManagementBasic Script Management
708,25533
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
727,26133
-@node Proof scriptsProof scripts
993,36384
-@node Script buffersScript buffers
1036,38504
-@node Locked queue and editing regionsLocked queue and editing regions
1058,39081
-@node Goal-save sequencesGoal-save sequences
1114,41228
-@node Active scripting bufferActive scripting buffer
1151,42694
-@node Summary of Proof General buffersSummary of Proof General buffers
1220,46114
-@node Script editing commandsScript editing commands
1283,48854
-@node Script processing commandsScript processing commands
1363,51812
-@node Proof assistant commandsProof assistant commands
1490,57105
-@node Toolbar commandsToolbar commands
1665,63298
-@node Interrupting during trace outputInterrupting during trace output
1689,64227
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1729,66157
-@node Document centred workingDocument centred working
1761,67372
-@node Visibility of completed proofsVisibility of completed proofs
1838,69952
-@node Switching between proof scriptsSwitching between proof scripts
1893,71881
-@node View of processed files View of processed files 
1930,73853
-@node Retracting across filesRetracting across files
1990,76904
-@node Asserting across filesAsserting across files
2003,77535
-@node Automatic multiple file handlingAutomatic multiple file handling
2016,78101
-@node Escaping script managementEscaping script management
2041,79135
-@node Editing featuresEditing features
2098,81247
-@node Unicode symbols and special layout supportUnicode symbols and special layout support
2168,84026
-@node Maths menuMaths menu
2210,85584
-@node Unicode Tokens modeUnicode Tokens mode
2227,86275
-@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2277,88698
-@node Special layout Special layout 
2307,89659
-@node Moving between Unicode and tokensMoving between Unicode and tokens
2415,93775
-@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2470,95886
-@node Selecting suitable fontsSelecting suitable fonts
2509,97060
-@node Support for other PackagesSupport for other Packages
2574,100035
-@node Syntax highlightingSyntax highlighting
2604,100871
-@node Imenu and SpeedbarImenu and Speedbar
2632,101874
-@node Support for outline modeSupport for outline mode
2678,103530
-@node Support for completionSupport for completion
2703,104659
-@node Support for tagsSupport for tags
2760,106821
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2812,109169
-@node Goals buffer commandsGoals buffer commands
2827,109681
-@node Customizing Proof GeneralCustomizing Proof General
2915,113216
-@node Basic optionsBasic options
2955,114886
-@node How to customizeHow to customize
2979,115656
-@node Display customizationDisplay customization
3026,117623
-@node User optionsUser options
3180,124028
-@node Changing facesChanging faces
3420,132540
-@node Script buffer facesScript buffer faces
3442,133415
-@node Goals and response facesGoals and response faces
3488,135015
-@node Tweaking configuration settingsTweaking configuration settings
3533,136547
-@node Hints and TipsHints and Tips
3590,139073
-@node Adding your own keybindingsAdding your own keybindings
3609,139674
-@node Using file variablesUsing file variables
3673,142288
-@node Using abbreviationsUsing abbreviations
3732,144474
-@node LEGO Proof GeneralLEGO Proof General
3771,145889
-@node LEGO specific commandsLEGO specific commands
3812,147258
-@node LEGO tagsLEGO tags
3832,147713
-@node LEGO customizationsLEGO customizations
3842,147960
-@node Coq Proof GeneralCoq Proof General
3874,148879
-@node Coq-specific commandsCoq-specific commands
3890,149288
-@node Coq-specific variablesCoq-specific variables
3912,149795
-@node Editing multiple proofsEditing multiple proofs
3934,150453
-@node User-loaded tacticsUser-loaded tactics
3958,151561
-@node Holes featureHoles feature
4022,154035
-@node Isabelle Proof GeneralIsabelle Proof General
4049,155322
-@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4075,156198
-@node Isabelle commandsIsabelle commands
4144,158999
-@node Isabelle settingsIsabelle settings
4287,163191
-@node Isabelle customizationsIsabelle customizations
4301,163773
-@node HOL Proof GeneralHOL Proof General
4324,164260
-@node Shell Proof GeneralShell Proof General
4366,166082
-@node Obtaining and InstallingObtaining and Installing
4402,167541
-@node Obtaining Proof GeneralObtaining Proof General
4418,167954
-@node Installing Proof General from tarballInstalling Proof General from tarball
4449,169193
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4474,170025
-@node Setting the names of binariesSetting the names of binaries
4489,170433
-@node Notes for syssiesNotes for syssies
4517,171373
-@node Bugs and EnhancementsBugs and Enhancements
4592,174409
-@node References4613,175224
-@node History of Proof GeneralHistory of Proof General
4653,176247
-@node Old News for 3.0Old News for 3.0
4747,180412
-@node Old News for 3.1Old News for 3.1
4817,184106
-@node Old News for 3.2Old News for 3.2
4843,185278
-@node Old News for 3.3Old News for 3.3
4904,188281
-@node Old News for 3.4Old News for 3.4
4923,189178
-@node Old News for 3.5Old News for 3.5
4945,190233
-@node Old News for 3.6Old News for 3.6
4949,190290
-@node Old News for 3.7Old News for 3.7
4954,190390
-@node Function IndexFunction Index
4998,192301
-@node Variable IndexVariable Index
5002,192377
-@node Keystroke IndexKeystroke Index
5006,192457
-@node Concept IndexConcept Index
5010,192523
+@node Prerequisites for this manualPrerequisites for this manual
638,23088
+@node Organization of this manualOrganization of this manual
682,24707
+@node Basic Script ManagementBasic Script Management
708,25535
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
727,26135
+@node Proof scriptsProof scripts
993,36386
+@node Script buffersScript buffers
1036,38506
+@node Locked queue and editing regionsLocked queue and editing regions
1058,39083
+@node Goal-save sequencesGoal-save sequences
1114,41230
+@node Active scripting bufferActive scripting buffer
1151,42696
+@node Summary of Proof General buffersSummary of Proof General buffers
1220,46116
+@node Script editing commandsScript editing commands
1283,48856
+@node Script processing commandsScript processing commands
1363,51814
+@node Proof assistant commandsProof assistant commands
1490,57107
+@node Toolbar commandsToolbar commands
1665,63302
+@node Interrupting during trace outputInterrupting during trace output
1689,64231
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1729,66161
+@node Document centred workingDocument centred working
1761,67376
+@node Visibility of completed proofsVisibility of completed proofs
1838,69956
+@node Switching between proof scriptsSwitching between proof scripts
1893,71885
+@node View of processed files View of processed files 
1930,73857
+@node Retracting across filesRetracting across files
1990,76908
+@node Asserting across filesAsserting across files
2003,77539
+@node Automatic multiple file handlingAutomatic multiple file handling
2016,78105
+@node Escaping script managementEscaping script management
2041,79139
+@node Editing featuresEditing features
2098,81251
+@node Unicode symbols and special layout supportUnicode symbols and special layout support
2168,84030
+@node Maths menuMaths menu
2210,85588
+@node Unicode Tokens modeUnicode Tokens mode
2227,86279
+@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2277,88702
+@node Special layout Special layout 
2307,89663
+@node Moving between Unicode and tokensMoving between Unicode and tokens
2415,93779
+@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2470,95890
+@node Selecting suitable fontsSelecting suitable fonts
2509,97064
+@node Support for other PackagesSupport for other Packages
2574,100039
+@node Syntax highlightingSyntax highlighting
2604,100875
+@node Imenu and SpeedbarImenu and Speedbar
2632,101878
+@node Support for outline modeSupport for outline mode
2678,103534
+@node Support for completionSupport for completion
2703,104663
+@node Support for tagsSupport for tags
2760,106825
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2812,109173
+@node Goals buffer commandsGoals buffer commands
2827,109685
+@node Customizing Proof GeneralCustomizing Proof General
2915,113220
+@node Basic optionsBasic options
2955,114890
+@node How to customizeHow to customize
2979,115660
+@node Display customizationDisplay customization
3026,117627
+@node User optionsUser options
3180,124032
+@node Changing facesChanging faces
3420,132544
+@node Script buffer facesScript buffer faces
3442,133419
+@node Goals and response facesGoals and response faces
3488,135019
+@node Tweaking configuration settingsTweaking configuration settings
3533,136551
+@node Hints and TipsHints and Tips
3590,139077
+@node Adding your own keybindingsAdding your own keybindings
3609,139678
+@node Using file variablesUsing file variables
3673,142292
+@node Using abbreviationsUsing abbreviations
3732,144478
+@node LEGO Proof GeneralLEGO Proof General
3771,145893
+@node LEGO specific commandsLEGO specific commands
3812,147262
+@node LEGO tagsLEGO tags
3832,147717
+@node LEGO customizationsLEGO customizations
3842,147964
+@node Coq Proof GeneralCoq Proof General
3874,148883
+@node Coq-specific commandsCoq-specific commands
3890,149292
+@node Coq-specific variablesCoq-specific variables
3912,149799
+@node Editing multiple proofsEditing multiple proofs
3934,150457
+@node User-loaded tacticsUser-loaded tactics
3958,151565
+@node Holes featureHoles feature
4022,154039
+@node Isabelle Proof GeneralIsabelle Proof General
4049,155326
+@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4075,156202
+@node Isabelle commandsIsabelle commands
4144,159003
+@node Isabelle settingsIsabelle settings
4287,163195
+@node Isabelle customizationsIsabelle customizations
4301,163777
+@node HOL Proof GeneralHOL Proof General
4324,164264
+@node Shell Proof GeneralShell Proof General
4366,166086
+@node Obtaining and InstallingObtaining and Installing
4402,167545
+@node Obtaining Proof GeneralObtaining Proof General
4418,167958
+@node Installing Proof General from tarballInstalling Proof General from tarball
4449,169197
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4474,170029
+@node Setting the names of binariesSetting the names of binaries
4489,170437
+@node Notes for syssiesNotes for syssies
4517,171377
+@node Bugs and EnhancementsBugs and Enhancements
4592,174413
+@node References4613,175228
+@node History of Proof GeneralHistory of Proof General
4653,176251
+@node Old News for 3.0Old News for 3.0
4747,180416
+@node Old News for 3.1Old News for 3.1
4817,184110
+@node Old News for 3.2Old News for 3.2
4843,185282
+@node Old News for 3.3Old News for 3.3
4904,188285
+@node Old News for 3.4Old News for 3.4
4923,189182
+@node Old News for 3.5Old News for 3.5
4945,190237
+@node Old News for 3.6Old News for 3.6
4949,190294
+@node Old News for 3.7Old News for 3.7
4954,190394
+@node Function IndexFunction Index
4998,192305
+@node Variable IndexVariable Index
5002,192381
+@node Keystroke IndexKeystroke Index
5006,192461
+@node Concept IndexConcept Index
5010,192527
 
 doc/PG-adapting.texi,3770
 @node Top155,4688