Updated.

1 files changed, 570 insertions, 570 deletions

diff --git a/TAGS b/TAGS
index a026c998..c3180dc8 100644
--- a/TAGS
+++ b/TAGS
@@ -38,6 +38,198 @@ coq/coq-db.el,678
 (defconst coq-solve-tactics-face 266,9562
 (defconst coq-cheat-face 270,9726
 
+coq/coq.el,7728
+(defcustom coq-translate-to-v8 60,1872
+(defun coq-build-prog-args 66,2051
+(defcustom coq-compiler76,2345
+(defcustom coq-dependency-analyzer82,2482
+(defcustom coq-use-makefile 88,2622
+(defcustom coq-default-undo-limit 96,2844
+(defconst coq-shell-init-cmd101,2972
+(defcustom coq-prog-env 109,3237
+(defconst coq-shell-restart-cmd 117,3486
+(defvar coq-shell-prompt-pattern119,3540
+(defvar coq-shell-cd 127,3843
+(defvar coq-shell-proof-completed-regexp 131,4003
+(defvar coq-goal-regexp134,4158
+(defun get-coq-library-directory 139,4254
+(defconst coq-library-directory 145,4436
+(defcustom coq-tags 148,4562
+(defconst coq-interrupt-regexp 153,4710
+(defcustom coq-www-home-page 156,4803
+(defvar coq-outline-regexp167,4978
+(defvar coq-outline-heading-end-regexp 174,5190
+(defvar coq-shell-outline-regexp 176,5244
+(defvar coq-shell-outline-heading-end-regexp 177,5294
+(defconst coq-state-preserving-tactics-regexp180,5358
+(defconst coq-state-changing-commands-regexp182,5460
+(defconst coq-state-preserving-commands-regexp184,5569
+(defconst coq-commands-regexp186,5682
+(defvar coq-retractable-instruct-regexp188,5761
+(defvar coq-non-retractable-instruct-regexp190,5853
+(defcustom coq-use-smie 222,6549
+(defconst coq-smie-grammar230,6777
+(defun coq-smie-rules 268,8598
+(defun coq-set-undo-limit 291,9329
+(defun build-list-id-from-string 295,9459
+(defun coq-last-prompt-info 307,9957
+(defun coq-last-prompt-info-safe 319,10489
+(defvar coq-last-but-one-statenum 325,10746
+(defvar coq-last-but-one-proofnum 332,11044
+(defvar coq-last-but-one-proofstack 335,11142
+(defsubst coq-get-span-statenum 338,11252
+(defsubst coq-get-span-proofnum 342,11367
+(defsubst coq-get-span-proofstack 346,11482
+(defsubst coq-set-span-statenum 350,11626
+(defsubst coq-get-span-goalcmd 354,11757
+(defsubst coq-set-span-goalcmd 358,11871
+(defsubst coq-set-span-proofnum 362,12001
+(defsubst coq-set-span-proofstack 366,12132
+(defsubst proof-last-locked-span 370,12292
+(defun proof-clone-buffer 374,12426
+(defun proof-store-buffer-win 388,12961
+(defun proof-store-response-win 399,13454
+(defun proof-store-goals-win 403,13581
+(defun coq-set-state-infos 415,14113
+(defun count-not-intersection 453,16200
+(defun coq-find-and-forget 483,17452
+(defvar coq-current-goal 510,18760
+(defun coq-goal-hyp 513,18825
+(defun coq-state-preserving-p 526,19299
+(defconst notation-print-kinds-table540,19613
+(defun coq-PrintScope 544,19780
+(defun coq-guess-or-ask-for-string 562,20329
+(defun coq-ask-do 576,20869
+(defsubst coq-put-into-brackets 585,21254
+(defsubst coq-put-into-quotes 588,21315
+(defun coq-SearchIsos 591,21375
+(defun coq-SearchConstant 599,21616
+(defun coq-Searchregexp 603,21709
+(defun coq-SearchRewrite 609,21852
+(defun coq-SearchAbout 613,21949
+(defun coq-Print 619,22094
+(defun coq-About 624,22219
+(defun coq-LocateConstant 629,22339
+(defun coq-LocateLibrary 634,22442
+(defun coq-LocateNotation 639,22559
+(defun coq-Pwd 647,22791
+(defun coq-Inspect 652,22915
+(defun coq-PrintSection(656,23015
+(defun coq-Print-implicit 660,23108
+(defun coq-Check 665,23259
+(defun coq-Show 670,23367
+(defun coq-Compile 684,23810
+(defun coq-guess-command-line 696,24128
+(defpacustom use-editing-holes 733,25681
+(defun coq-mode-config 742,25984
+(defun coq-shell-mode-config 836,29313
+(defun coq-goals-mode-config 881,31141
+(defun coq-response-config 888,31385
+(defpacustom print-fully-explicit 913,32210
+(defpacustom print-implicit 918,32358
+(defpacustom print-coercions 923,32524
+(defpacustom print-match-wildcards 928,32668
+(defpacustom print-elim-types 933,32848
+(defpacustom printing-depth 938,33014
+(defpacustom undo-depth 943,33175
+(defpacustom time-commands 948,33341
+(defgroup coq-auto-compile 969,33999
+(defpacustom compile-before-require 974,34150
+(defcustom coq-compile-command 986,34642
+(defpacustom confirm-external-compilation 1016,35925
+(defconst coq-compile-substitution-list1025,36232
+(defcustom coq-compile-auto-save 1045,37153
+(defcustom coq-lock-ancestors 1070,38211
+(defcustom coq-compile-ignore-library-directory 1079,38532
+(defcustom coq-compile-ignored-directories 1091,39020
+(defcustom coq-load-path 1104,39653
+(defcustom coq-load-path-include-current 1119,40209
+(defconst coq-require-command-regexp1128,40527
+(defconst coq-require-id-regexp1135,40884
+(defvar coq-compile-history 1143,41318
+(defvar coq-compile-response-buffer-name 1146,41402
+(defvar coq-compile-response-buffer 1149,41541
+(defvar coq-debug-auto-compilation 1153,41643
+(defun time-less-or-equal 1159,41750
+(defun coq-max-dep-mod-time 1167,42088
+(defun coq-prog-args 1190,42892
+(defun coq-lock-ancestor 1199,43151
+(defun coq-unlock-ancestor 1215,43926
+(defun coq-unlock-all-ancestors-of-span 1222,44221
+(defun coq-compile-ignore-file 1229,44517
+(defun coq-library-src-of-obj-file 1253,45400
+(defun coq-include-options 1258,45632
+(defun coq-init-compile-response-buffer 1277,46405
+(defun coq-display-compile-response-buffer 1299,47473
+(defun coq-get-library-dependencies 1313,48096
+(defun coq-compile-library 1360,50324
+(defun coq-compile-library-if-necessary 1387,51529
+(defun coq-make-lib-up-to-date 1433,53401
+(defun coq-auto-compile-externally 1489,55862
+(defun coq-map-module-id-to-obj-file 1532,58008
+(defun coq-check-module 1584,60540
+(defvar coq-process-require-current-buffer1612,61982
+(defun coq-compile-save-buffer-filter 1618,62247
+(defun coq-compile-save-some-buffers 1628,62661
+(defun coq-preprocess-require-commands 1650,63563
+(defun coq-switch-buffer-kill-proof-shell 1683,65132
+(defun coq-preprocessing 1703,65808
+(defun coq-fake-constant-markup 1717,66263
+(defun coq-create-span-menu 1733,66868
+(defconst module-kinds-table1751,67381
+(defconst modtype-kinds-table1755,67530
+(defun coq-insert-section-or-module 1759,67659
+(defconst reqkinds-kinds-table1780,68509
+(defun coq-insert-requires 1784,68653
+(defun coq-end-Section 1797,69133
+(defun coq-insert-intros 1815,69711
+(defun coq-insert-infoH-hook 1827,70244
+(defun coq-insert-as 1832,70452
+(defun coq-insert-match 1849,71145
+(defun coq-insert-solve-tactic 1878,72315
+(defun coq-insert-tactic 1884,72566
+(defun coq-insert-tactical 1890,72768
+(defun coq-insert-command 1896,72999
+(defun coq-insert-term 1901,73164
+(define-key coq-keymap 1906,73325
+(define-key coq-keymap 1907,73383
+(define-key coq-keymap 1908,73440
+(define-key coq-keymap 1909,73509
+(define-key coq-keymap 1910,73565
+(define-key coq-keymap 1911,73614
+(define-key coq-keymap 1912,73672
+(define-key coq-keymap 1913,73732
+(define-key coq-keymap 1914,73797
+(define-key coq-keymap 1917,73925
+(define-key coq-keymap 1919,73999
+(define-key coq-keymap 1920,74056
+(define-key coq-keymap 1924,74181
+(define-key coq-keymap 1926,74237
+(define-key coq-keymap 1927,74287
+(define-key coq-keymap 1928,74337
+(define-key coq-keymap 1929,74393
+(define-key coq-keymap 1930,74443
+(define-key coq-keymap 1931,74497
+(define-key coq-keymap 1932,74556
+(define-key coq-goals-mode-map 1935,74617
+(define-key coq-goals-mode-map 1936,74699
+(define-key coq-goals-mode-map 1937,74781
+(define-key coq-goals-mode-map 1938,74868
+(define-key coq-goals-mode-map 1939,74950
+(defvar last-coq-error-location 1948,75252
+(defun coq-get-last-error-location 1956,75636
+(defun coq-highlight-error 2006,78199
+(defun coq-highlight-error-hook 2034,79280
+(defun first-word-of-buffer 2044,79497
+(defun coq-show-first-goal 2052,79700
+(defvar coq-modeline-string2 2068,80365
+(defvar coq-modeline-string1 2069,80399
+(defvar coq-modeline-string0 2070,80433
+(defun coq-build-subgoals-string 2071,80474
+(defun coq-update-minor-mode-alist 2076,80640
+(defun is-not-split-vertic 2108,82034
+(defun optim-resp-windows 2117,82474
+
 coq/coq-indent.el,2515
 (defconst coq-any-command-regexp20,368
 (defconst coq-indent-inner-regexp23,442
@@ -107,76 +299,76 @@ coq/coq-local-vars.el,229
 (defun coq-ask-prog-name 131,4952
 (defun coq-ask-insert-coq-prog-name 148,5663
 
-coq/coq-syntax.el,2771
+coq/coq-syntax.el,2768
 (defcustom coq-prog-name 18,560
-(defcustom coq-user-tactics-db 38,1342
-(defcustom coq-user-commands-db 55,1855
-(defcustom coq-user-tacticals-db 71,2374
-(defcustom coq-user-solve-tactics-db 87,2895
-(defcustom coq-user-cheat-tactics-db 103,3414
-(defcustom coq-user-reserved-db 122,3960
-(defvar coq-tactics-db140,4491
-(defvar coq-solve-tactics-db298,12750
-(defvar coq-solve-cheat-tactics-db321,13595
-(defvar coq-tacticals-db333,13770
-(defvar coq-decl-db357,14656
-(defvar coq-defn-db382,16112
-(defvar coq-goal-starters-db440,20467
-(defvar coq-other-commands-db469,22224
-(defvar coq-commands-db598,31690
-(defvar coq-terms-db605,31910
-(defun coq-count-match 667,34525
-(defun coq-module-opening-p 683,35254
-(defun coq-section-command-p 694,35665
-(defun coq-goal-command-str-p 698,35762
-(defun coq-goal-command-p 725,36864
-(defvar coq-keywords-save-strict734,37147
-(defvar coq-keywords-save743,37260
-(defun coq-save-command-p 747,37338
-(defvar coq-keywords-kill-goal758,37666
-(defvar coq-keywords-state-changing-misc-commands762,37756
-(defvar coq-keywords-goal765,37881
-(defvar coq-keywords-decl768,37964
-(defvar coq-keywords-defn771,38038
-(defvar coq-keywords-state-changing-commands775,38113
-(defvar coq-keywords-state-preserving-commands784,38373
-(defvar coq-keywords-commands789,38589
-(defvar coq-solve-tactics794,38737
-(defvar coq-solve-tactics-regexp798,38858
-(defvar coq-solve-cheat-tactics802,38992
-(defvar coq-solve-cheat-tactics-regexp806,39137
-(defvar coq-tacticals810,39295
-(defvar coq-reserved816,39434
-(defvar coq-reserved-regexp 826,39761
-(defvar coq-state-changing-tactics828,39826
-(defvar coq-state-preserving-tactics831,39935
-(defvar coq-tactics835,40049
-(defvar coq-tactics-regexp 838,40138
-(defvar coq-retractable-instruct841,40293
-(defvar coq-non-retractable-instruct844,40403
-(defvar coq-keywords848,40531
-(defun proof-regexp-alt-list-symb 854,40755
-(defvar coq-keywords-regexp 857,40860
-(defvar coq-symbols860,40928
-(defvar coq-error-regexp 879,41141
-(defvar coq-id 882,41369
-(defvar coq-id-shy 883,41394
-(defvar coq-ids 886,41496
-(defun coq-first-abstr-regexp 888,41562
-(defcustom coq-variable-highlight-enable 891,41657
-(defvar coq-font-lock-terms897,41784
-(defconst coq-save-command-regexp-strict919,42867
-(defconst coq-save-command-regexp925,43037
-(defconst coq-save-with-hole-regexp930,43192
-(defconst coq-goal-command-regexp934,43352
-(defconst coq-goal-with-hole-regexp937,43454
-(defconst coq-decl-with-hole-regexp941,43588
-(defconst coq-defn-with-hole-regexp948,43838
-(defconst coq-with-with-hole-regexp958,44128
-(defvar coq-font-lock-keywords-1973,44658
-(defvar coq-font-lock-keywords 1001,45993
-(defun coq-init-syntax-table 1003,46051
-(defconst coq-generic-expression1028,46778
+(defcustom coq-user-tactics-db 33,1148
+(defcustom coq-user-commands-db 50,1661
+(defcustom coq-user-tacticals-db 66,2180
+(defcustom coq-user-solve-tactics-db 82,2701
+(defcustom coq-user-cheat-tactics-db 98,3220
+(defcustom coq-user-reserved-db 117,3766
+(defvar coq-tactics-db135,4297
+(defvar coq-solve-tactics-db293,12556
+(defvar coq-solve-cheat-tactics-db316,13401
+(defvar coq-tacticals-db328,13576
+(defvar coq-decl-db352,14462
+(defvar coq-defn-db377,15918
+(defvar coq-goal-starters-db435,20273
+(defvar coq-other-commands-db464,22030
+(defvar coq-commands-db593,31496
+(defvar coq-terms-db600,31716
+(defun coq-count-match 662,34331
+(defun coq-module-opening-p 678,35060
+(defun coq-section-command-p 689,35471
+(defun coq-goal-command-str-p 693,35568
+(defun coq-goal-command-p 720,36670
+(defvar coq-keywords-save-strict729,36953
+(defvar coq-keywords-save738,37066
+(defun coq-save-command-p 742,37144
+(defvar coq-keywords-kill-goal753,37472
+(defvar coq-keywords-state-changing-misc-commands757,37562
+(defvar coq-keywords-goal760,37687
+(defvar coq-keywords-decl763,37770
+(defvar coq-keywords-defn766,37844
+(defvar coq-keywords-state-changing-commands770,37919
+(defvar coq-keywords-state-preserving-commands779,38179
+(defvar coq-keywords-commands784,38395
+(defvar coq-solve-tactics789,38543
+(defvar coq-solve-tactics-regexp793,38664
+(defvar coq-solve-cheat-tactics797,38798
+(defvar coq-solve-cheat-tactics-regexp801,38943
+(defvar coq-tacticals805,39101
+(defvar coq-reserved811,39240
+(defvar coq-reserved-regexp 821,39567
+(defvar coq-state-changing-tactics823,39632
+(defvar coq-state-preserving-tactics826,39741
+(defvar coq-tactics830,39855
+(defvar coq-tactics-regexp 833,39944
+(defvar coq-retractable-instruct836,40099
+(defvar coq-non-retractable-instruct839,40209
+(defvar coq-keywords843,40337
+(defun proof-regexp-alt-list-symb 849,40561
+(defvar coq-keywords-regexp 852,40666
+(defvar coq-symbols855,40734
+(defvar coq-error-regexp 874,40947
+(defvar coq-id 877,41175
+(defvar coq-id-shy 878,41200
+(defvar coq-ids 881,41302
+(defun coq-first-abstr-regexp 883,41368
+(defcustom coq-variable-highlight-enable 886,41463
+(defvar coq-font-lock-terms892,41590
+(defconst coq-save-command-regexp-strict914,42673
+(defconst coq-save-command-regexp920,42843
+(defconst coq-save-with-hole-regexp925,42998
+(defconst coq-goal-command-regexp929,43158
+(defconst coq-goal-with-hole-regexp932,43260
+(defconst coq-decl-with-hole-regexp936,43394
+(defconst coq-defn-with-hole-regexp943,43644
+(defconst coq-with-with-hole-regexp953,43934
+(defvar coq-font-lock-keywords-1968,44464
+(defvar coq-font-lock-keywords 996,45799
+(defun coq-init-syntax-table 998,45857
+(defconst coq-generic-expression1023,46584
 
 coq/coq-unicode-tokens.el,454
 (defconst coq-token-format 39,1427
@@ -191,198 +383,6 @@ coq/coq-unicode-tokens.el,454
 (defconst coq-control-region-format-regexp 264,6997
 (defconst coq-control-regions266,7080
 
-coq/coq.el,7728
-(defcustom coq-translate-to-v8 60,1874
-(defun coq-build-prog-args 66,2054
-(defcustom coq-compiler76,2348
-(defcustom coq-dependency-analyzer82,2485
-(defcustom coq-use-makefile 88,2625
-(defcustom coq-default-undo-limit 96,2848
-(defconst coq-shell-init-cmd101,2976
-(defcustom coq-prog-env 109,3241
-(defconst coq-shell-restart-cmd 117,3491
-(defvar coq-shell-prompt-pattern119,3545
-(defvar coq-shell-cd 127,3848
-(defvar coq-shell-proof-completed-regexp 131,4008
-(defvar coq-goal-regexp134,4163
-(defun get-coq-library-directory 139,4259
-(defconst coq-library-directory 145,4441
-(defcustom coq-tags 148,4567
-(defconst coq-interrupt-regexp 153,4715
-(defcustom coq-www-home-page 156,4808
-(defvar coq-outline-regexp167,4983
-(defvar coq-outline-heading-end-regexp 174,5195
-(defvar coq-shell-outline-regexp 176,5249
-(defvar coq-shell-outline-heading-end-regexp 177,5299
-(defconst coq-state-preserving-tactics-regexp180,5363
-(defconst coq-state-changing-commands-regexp182,5465
-(defconst coq-state-preserving-commands-regexp184,5574
-(defconst coq-commands-regexp186,5687
-(defvar coq-retractable-instruct-regexp188,5766
-(defvar coq-non-retractable-instruct-regexp190,5858
-(defcustom coq-use-smie 222,6554
-(defconst coq-smie-grammar230,6782
-(defun coq-smie-rules 268,8603
-(defun coq-set-undo-limit 291,9334
-(defun build-list-id-from-string 295,9464
-(defun coq-last-prompt-info 307,9962
-(defun coq-last-prompt-info-safe 319,10494
-(defvar coq-last-but-one-statenum 325,10751
-(defvar coq-last-but-one-proofnum 332,11049
-(defvar coq-last-but-one-proofstack 335,11147
-(defsubst coq-get-span-statenum 338,11257
-(defsubst coq-get-span-proofnum 342,11372
-(defsubst coq-get-span-proofstack 346,11487
-(defsubst coq-set-span-statenum 350,11631
-(defsubst coq-get-span-goalcmd 354,11762
-(defsubst coq-set-span-goalcmd 358,11876
-(defsubst coq-set-span-proofnum 362,12006
-(defsubst coq-set-span-proofstack 366,12137
-(defsubst proof-last-locked-span 370,12297
-(defun proof-clone-buffer 374,12431
-(defun proof-store-buffer-win 388,12966
-(defun proof-store-response-win 399,13459
-(defun proof-store-goals-win 403,13586
-(defun coq-set-state-infos 415,14118
-(defun count-not-intersection 453,16205
-(defun coq-find-and-forget 483,17457
-(defvar coq-current-goal 510,18765
-(defun coq-goal-hyp 513,18830
-(defun coq-state-preserving-p 526,19304
-(defconst notation-print-kinds-table540,19618
-(defun coq-PrintScope 544,19785
-(defun coq-guess-or-ask-for-string 562,20334
-(defun coq-ask-do 576,20874
-(defsubst coq-put-into-brackets 585,21259
-(defsubst coq-put-into-quotes 588,21320
-(defun coq-SearchIsos 591,21380
-(defun coq-SearchConstant 599,21621
-(defun coq-Searchregexp 603,21714
-(defun coq-SearchRewrite 609,21857
-(defun coq-SearchAbout 613,21954
-(defun coq-Print 619,22099
-(defun coq-About 624,22224
-(defun coq-LocateConstant 629,22344
-(defun coq-LocateLibrary 634,22447
-(defun coq-LocateNotation 639,22564
-(defun coq-Pwd 647,22796
-(defun coq-Inspect 652,22920
-(defun coq-PrintSection(656,23020
-(defun coq-Print-implicit 660,23113
-(defun coq-Check 665,23264
-(defun coq-Show 670,23372
-(defun coq-Compile 684,23815
-(defun coq-guess-command-line 696,24133
-(defpacustom use-editing-holes 733,25686
-(defun coq-mode-config 742,25989
-(defun coq-shell-mode-config 836,29318
-(defun coq-goals-mode-config 881,31146
-(defun coq-response-config 888,31390
-(defpacustom print-fully-explicit 913,32215
-(defpacustom print-implicit 918,32363
-(defpacustom print-coercions 923,32529
-(defpacustom print-match-wildcards 928,32673
-(defpacustom print-elim-types 933,32853
-(defpacustom printing-depth 938,33019
-(defpacustom undo-depth 943,33180
-(defpacustom time-commands 948,33346
-(defgroup coq-auto-compile 969,34004
-(defpacustom compile-before-require 974,34155
-(defcustom coq-compile-command 986,34639
-(defpacustom confirm-external-compilation 1016,35923
-(defconst coq-compile-substitution-list1025,36231
-(defcustom coq-compile-auto-save 1045,37152
-(defcustom coq-lock-ancestors 1070,38211
-(defcustom coq-compile-ignore-library-directory 1079,38526
-(defcustom coq-compile-ignored-directories 1091,39010
-(defcustom coq-load-path 1104,39644
-(defcustom coq-load-path-include-current 1119,40201
-(defconst coq-require-command-regexp1128,40520
-(defconst coq-require-id-regexp1135,40877
-(defvar coq-compile-history 1143,41311
-(defvar coq-compile-response-buffer-name 1146,41395
-(defvar coq-compile-response-buffer 1149,41534
-(defvar coq-debug-auto-compilation 1153,41636
-(defun time-less-or-equal 1159,41743
-(defun coq-max-dep-mod-time 1167,42081
-(defun coq-prog-args 1190,42885
-(defun coq-lock-ancestor 1199,43144
-(defun coq-unlock-ancestor 1215,43919
-(defun coq-unlock-all-ancestors-of-span 1222,44214
-(defun coq-compile-ignore-file 1229,44510
-(defun coq-library-src-of-obj-file 1253,45393
-(defun coq-include-options 1258,45625
-(defun coq-init-compile-response-buffer 1277,46398
-(defun coq-display-compile-response-buffer 1299,47466
-(defun coq-get-library-dependencies 1313,48089
-(defun coq-compile-library 1360,50317
-(defun coq-compile-library-if-necessary 1387,51522
-(defun coq-make-lib-up-to-date 1433,53394
-(defun coq-auto-compile-externally 1489,55855
-(defun coq-map-module-id-to-obj-file 1532,58001
-(defun coq-check-module 1584,60533
-(defvar coq-process-require-current-buffer1612,61975
-(defun coq-compile-save-buffer-filter 1618,62240
-(defun coq-compile-save-some-buffers 1628,62654
-(defun coq-preprocess-require-commands 1650,63556
-(defun coq-switch-buffer-kill-proof-shell 1683,65118
-(defun coq-preprocessing 1703,65794
-(defun coq-fake-constant-markup 1717,66249
-(defun coq-create-span-menu 1733,66854
-(defconst module-kinds-table1751,67367
-(defconst modtype-kinds-table1755,67516
-(defun coq-insert-section-or-module 1759,67645
-(defconst reqkinds-kinds-table1780,68495
-(defun coq-insert-requires 1784,68639
-(defun coq-end-Section 1797,69119
-(defun coq-insert-intros 1815,69697
-(defun coq-insert-infoH-hook 1827,70230
-(defun coq-insert-as 1832,70438
-(defun coq-insert-match 1849,71131
-(defun coq-insert-solve-tactic 1878,72301
-(defun coq-insert-tactic 1884,72552
-(defun coq-insert-tactical 1890,72754
-(defun coq-insert-command 1896,72985
-(defun coq-insert-term 1901,73150
-(define-key coq-keymap 1906,73311
-(define-key coq-keymap 1907,73369
-(define-key coq-keymap 1908,73426
-(define-key coq-keymap 1909,73495
-(define-key coq-keymap 1910,73551
-(define-key coq-keymap 1911,73600
-(define-key coq-keymap 1912,73658
-(define-key coq-keymap 1913,73718
-(define-key coq-keymap 1914,73783
-(define-key coq-keymap 1917,73911
-(define-key coq-keymap 1919,73985
-(define-key coq-keymap 1920,74042
-(define-key coq-keymap 1924,74167
-(define-key coq-keymap 1926,74223
-(define-key coq-keymap 1927,74273
-(define-key coq-keymap 1928,74323
-(define-key coq-keymap 1929,74379
-(define-key coq-keymap 1930,74429
-(define-key coq-keymap 1931,74483
-(define-key coq-keymap 1932,74542
-(define-key coq-goals-mode-map 1935,74603
-(define-key coq-goals-mode-map 1936,74685
-(define-key coq-goals-mode-map 1937,74767
-(define-key coq-goals-mode-map 1938,74854
-(define-key coq-goals-mode-map 1939,74936
-(defvar last-coq-error-location 1948,75238
-(defun coq-get-last-error-location 1956,75622
-(defun coq-highlight-error 2006,78185
-(defun coq-highlight-error-hook 2034,79266
-(defun first-word-of-buffer 2044,79483
-(defun coq-show-first-goal 2052,79686
-(defvar coq-modeline-string2 2069,80381
-(defvar coq-modeline-string1 2070,80415
-(defvar coq-modeline-string0 2071,80449
-(defun coq-build-subgoals-string 2072,80490
-(defun coq-update-minor-mode-alist 2077,80656
-(defun is-not-split-vertic 2109,82050
-(defun optim-resp-windows 2118,82490
-
 hol98/hol98.el,121
 (defvar hol98-keywords 17,419
 (defvar hol98-rules 18,447
@@ -424,6 +424,46 @@ isar/isabelle-system.el,1254
 isar/isar-autotest.el,31
 (defvar isar-long-tests 8,186
 
+isar/isar.el,1595
+(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,8309
+(defpacustom use-find-theorems-form 241,8493
+(defun isar-set-undo-commands 246,8659
+(defpacustom use-linear-undo 261,9292
+(defun isar-configure-from-settings 266,9450
+(defun isar-remove-file 274,9600
+(defun isar-shell-compute-new-files-list 286,9904
+(define-derived-mode isar-shell-mode 305,10474
+(define-derived-mode isar-response-mode 310,10601
+(define-derived-mode isar-goals-mode 315,10734
+(define-derived-mode isar-mode 320,10860
+(defpgdefault menu-entries372,12575
+(defun isar-set-command 403,13769
+(defpgdefault help-menu-entries 408,13899
+(defun isar-count-undos 411,13975
+(defun isar-find-and-forget 437,14941
+(defun isar-goal-command-p 473,16284
+(defun isar-global-save-command-p 478,16461
+(defvar isar-current-goal 499,17245
+(defun isar-state-preserving-p 502,17311
+(defvar isar-shell-current-line-width 527,18160
+(defun isar-shell-adjust-line-width 532,18352
+(defsubst isar-string-wrapping 555,19117
+(defsubst isar-positions-of 564,19311
+(defcustom isar-wrap-commands-singly 570,19516
+(defun isar-command-wrapping 576,19712
+(defun isar-preprocessing 584,20026
+(defun isar-mode-config 602,20577
+(defun isar-shell-mode-config 616,21230
+(defun isar-response-mode-config 626,21579
+(defun isar-goals-mode-config 636,21914
+
 isar/isar-find-theorems.el,779
 (defvar isar-find-theorems-data 19,565
 (defun isar-find-theorems-minibuffer 35,1039
@@ -536,38 +576,38 @@ isar/isar-syntax.el,3975
 (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 420,13789
-(defun isar-output-flk 426,14041
-(defvar isar-output-font-lock-keywords-1429,14150
-(defun isar-strip-output-markup 465,15573
-(defconst isar-shell-font-lock-keywords469,15709
-(defvar isar-goals-font-lock-keywords472,15793
-(defconst isar-linear-undo 506,16472
-(defconst isar-undo 508,16515
-(defconst isar-pr510,16558
-(defun isar-remove 517,16716
-(defun isar-undos 520,16791
-(defun isar-cannot-undo 530,17025
-(defconst isar-undo-commands533,17095
-(defconst isar-theory-start-regexp541,17232
-(defconst isar-end-regexp547,17390
-(defconst isar-undo-fail-regexp551,17491
-(defconst isar-undo-skip-regexp555,17595
-(defconst isar-undo-ignore-regexp558,17716
-(defconst isar-undo-remove-regexp561,17781
-(defconst isar-keywords-imenu569,17938
-(defconst isar-entity-regexp 576,18129
-(defconst isar-named-entity-regexp579,18225
-(defconst isar-named-entity-name-match-number584,18355
-(defconst isar-generic-expression587,18456
-(defconst isar-indent-any-regexp598,18690
-(defconst isar-indent-inner-regexp600,18783
-(defconst isar-indent-enclose-regexp602,18849
-(defconst isar-indent-open-regexp604,18965
-(defconst isar-indent-close-regexp606,19075
-(defconst isar-outline-regexp612,19212
-(defconst isar-outline-heading-end-regexp 616,19365
-(defconst isar-outline-heading-alist 618,19414
+(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
@@ -601,64 +641,6 @@ isar/isar-unicode-tokens.el,1363
 (defun isar-init-shortcut-alists 640,17084
 (defconst isar-tokens-customizable-variables661,17747
 
-isar/isar.el,1595
-(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,8309
-(defpacustom use-find-theorems-form 241,8493
-(defun isar-set-undo-commands 246,8659
-(defpacustom use-linear-undo 261,9292
-(defun isar-configure-from-settings 266,9450
-(defun isar-remove-file 274,9600
-(defun isar-shell-compute-new-files-list 286,9904
-(define-derived-mode isar-shell-mode 305,10474
-(define-derived-mode isar-response-mode 310,10601
-(define-derived-mode isar-goals-mode 315,10734
-(define-derived-mode isar-mode 320,10860
-(defpgdefault menu-entries372,12575
-(defun isar-set-command 403,13769
-(defpgdefault help-menu-entries 408,13899
-(defun isar-count-undos 411,13975
-(defun isar-find-and-forget 437,14941
-(defun isar-goal-command-p 473,16284
-(defun isar-global-save-command-p 478,16461
-(defvar isar-current-goal 499,17245
-(defun isar-state-preserving-p 502,17311
-(defvar isar-shell-current-line-width 527,18160
-(defun isar-shell-adjust-line-width 532,18352
-(defsubst isar-string-wrapping 555,19117
-(defsubst isar-positions-of 564,19311
-(defcustom isar-wrap-commands-singly 570,19516
-(defun isar-command-wrapping 576,19712
-(defun isar-preprocessing 584,20026
-(defun isar-mode-config 602,20577
-(defun isar-shell-mode-config 616,21230
-(defun isar-response-mode-config 626,21579
-(defun isar-goals-mode-config 636,21914
-
-lego/lego-syntax.el,600
-(defconst lego-keywords-goal 15,358
-(defconst lego-keywords-save 17,401
-(defconst lego-commands19,472
-(defconst lego-keywords31,1030
-(defconst lego-tacticals 36,1207
-(defconst lego-error-regexp 39,1315
-(defvar lego-id 42,1473
-(defvar lego-ids 44,1500
-(defconst lego-arg-list-regexp 48,1696
-(defun lego-decl-defn-regexp 51,1812
-(defconst lego-definiendum-alternative-regexp59,2184
-(defvar lego-font-lock-terms63,2368
-(defconst lego-goal-with-hole-regexp89,3221
-(defconst lego-save-with-hole-regexp94,3443
-(defvar lego-font-lock-keywords-199,3660
-(defun lego-init-syntax-table 110,4122
-
 lego/lego.el,1636
 (defcustom lego-tags 21,534
 (defcustom lego-test-all-name 26,670
@@ -701,6 +683,41 @@ lego/lego.el,1636
 (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
+(defconst lego-keywords-save 17,401
+(defconst lego-commands19,472
+(defconst lego-keywords31,1030
+(defconst lego-tacticals 36,1207
+(defconst lego-error-regexp 39,1315
+(defvar lego-id 42,1473
+(defvar lego-ids 44,1500
+(defconst lego-arg-list-regexp 48,1696
+(defun lego-decl-defn-regexp 51,1812
+(defconst lego-definiendum-alternative-regexp59,2184
+(defvar lego-font-lock-terms63,2368
+(defconst lego-goal-with-hole-regexp89,3221
+(defconst lego-save-with-hole-regexp94,3443
+(defvar lego-font-lock-keywords-199,3660
+(defun lego-init-syntax-table 110,4122
+
+phox/phox.el,555
+(defcustom phox-prog-name 32,916
+(defcustom phox-web-page37,1018
+(defcustom phox-doc-dir43,1168
+(defcustom phox-lib-dir49,1315
+(defcustom phox-tags-program55,1458
+(defcustom phox-tags-doc61,1637
+(defcustom phox-etags67,1774
+(defpgdefault menu-entries88,2224
+(defun phox-config 102,2417
+(defun phox-shell-config 146,4343
+(define-derived-mode phox-mode 170,5205
+(define-derived-mode phox-shell-mode 186,5668
+(define-derived-mode phox-response-mode 191,5796
+(define-derived-mode phox-goals-mode 201,6157
+(defpgdefault completion-table224,6943
+
 phox/phox-extraction.el,383
 (defvar phox-prog-orig 19,619
 (defun phox-prog-flags-modify(21,687
@@ -839,23 +856,6 @@ phox/phox-tags.el,305
 (defun phox-complete-tag(69,2091
 (defvar phox-tags-menu76,2200
 
-phox/phox.el,555
-(defcustom phox-prog-name 32,916
-(defcustom phox-web-page37,1018
-(defcustom phox-doc-dir43,1168
-(defcustom phox-lib-dir49,1315
-(defcustom phox-tags-program55,1458
-(defcustom phox-tags-doc61,1637
-(defcustom phox-etags67,1774
-(defpgdefault menu-entries88,2224
-(defun phox-config 102,2417
-(defun phox-shell-config 146,4343
-(define-derived-mode phox-mode 170,5205
-(define-derived-mode phox-shell-mode 186,5668
-(define-derived-mode phox-response-mode 191,5796
-(define-derived-mode phox-goals-mode 201,6157
-(defpgdefault completion-table224,6943
-
 generic/pg-assoc.el,81
 (defun proof-associated-buffers 33,973
 (defun proof-associated-windows 43,1183
@@ -1383,32 +1383,32 @@ generic/proof-config.el,7859
 (defcustom proof-shell-strip-crs-from-output 1537,59239
 (defcustom proof-shell-extend-queue-hook 1545,59607
 (defcustom proof-shell-insert-hook 1555,60037
-(defcustom proof-script-preprocess 1596,61997
-(defcustom proof-shell-handle-delayed-output-hook1602,62148
-(defcustom proof-shell-handle-error-or-interrupt-hook1608,62363
-(defcustom proof-shell-pre-interrupt-hook1626,63109
-(defcustom proof-shell-handle-output-system-specific 1634,63380
-(defcustom proof-state-change-hook 1657,64353
-(defcustom proof-shell-syntax-table-entries 1667,64746
-(defgroup proof-goals 1685,65117
-(defcustom pg-subterm-first-special-char 1690,65238
-(defcustom pg-subterm-anns-use-stack 1698,65550
-(defcustom pg-goals-change-goal 1707,65849
-(defcustom pbp-goal-command 1712,65965
-(defcustom pbp-hyp-command 1717,66121
-(defcustom pg-subterm-help-cmd 1722,66283
-(defcustom pg-goals-error-regexp 1729,66519
-(defcustom proof-shell-result-start 1734,66679
-(defcustom proof-shell-result-end 1740,66913
-(defcustom pg-subterm-start-char 1746,67126
-(defcustom pg-subterm-sep-char 1757,67600
-(defcustom pg-subterm-end-char 1763,67779
-(defcustom pg-topterm-regexp 1769,67936
-(defcustom proof-goals-font-lock-keywords 1784,68536
-(defcustom proof-response-font-lock-keywords 1792,68895
-(defcustom proof-shell-font-lock-keywords 1800,69257
-(defcustom pg-before-fontify-output-hook 1811,69771
-(defcustom pg-after-fontify-output-hook 1819,70132
+(defcustom proof-script-preprocess 1598,62135
+(defcustom proof-shell-handle-delayed-output-hook1604,62286
+(defcustom proof-shell-handle-error-or-interrupt-hook1610,62501
+(defcustom proof-shell-pre-interrupt-hook1628,63247
+(defcustom proof-shell-handle-output-system-specific 1636,63518
+(defcustom proof-state-change-hook 1659,64491
+(defcustom proof-shell-syntax-table-entries 1669,64884
+(defgroup proof-goals 1687,65255
+(defcustom pg-subterm-first-special-char 1692,65376
+(defcustom pg-subterm-anns-use-stack 1700,65688
+(defcustom pg-goals-change-goal 1709,65987
+(defcustom pbp-goal-command 1714,66103
+(defcustom pbp-hyp-command 1719,66259
+(defcustom pg-subterm-help-cmd 1724,66421
+(defcustom pg-goals-error-regexp 1731,66657
+(defcustom proof-shell-result-start 1736,66817
+(defcustom proof-shell-result-end 1742,67051
+(defcustom pg-subterm-start-char 1748,67264
+(defcustom pg-subterm-sep-char 1759,67738
+(defcustom pg-subterm-end-char 1765,67917
+(defcustom pg-topterm-regexp 1771,68074
+(defcustom proof-goals-font-lock-keywords 1786,68674
+(defcustom proof-response-font-lock-keywords 1794,69033
+(defcustom proof-shell-font-lock-keywords 1802,69395
+(defcustom pg-before-fontify-output-hook 1813,69909
+(defcustom pg-after-fontify-output-hook 1821,70270
 
 generic/proof-depends.el,917
 (defvar proof-thm-names-of-files 25,639
@@ -1628,133 +1628,133 @@ generic/proof-script.el,5760
 (defun proof-deactivate-scripting-choose-action 1069,40378
 (defun proof-deactivate-scripting 1081,40763
 (defun proof-activate-scripting 1178,44886
-(defun proof-toggle-active-scripting 1279,49406
-(defun proof-done-advancing 1318,50651
-(defun proof-done-advancing-comment 1397,53636
-(defun proof-done-advancing-save 1431,55022
-(defun proof-make-goalsave1519,58386
-(defun proof-get-name-from-goal 1537,59251
-(defun proof-done-advancing-autosave 1557,60276
-(defun proof-done-advancing-other 1621,62772
-(defun proof-segment-up-to-parser 1650,63736
-(defun proof-script-generic-parse-find-comment-end 1719,66002
-(defun proof-script-generic-parse-cmdend 1728,66416
-(defun proof-script-generic-parse-cmdstart 1779,68312
-(defun proof-script-generic-parse-sexp 1818,69912
-(defun proof-semis-to-vanillas 1830,70378
-(defun proof-next-command-new-line 1883,72051
-(defun proof-script-next-command-advance 1888,72257
-(defun proof-assert-until-point 1907,72757
-(defun proof-assert-electric-terminator 1922,73384
-(defun proof-assert-semis 1965,75016
-(defun proof-retract-before-change 1979,75757
-(defun proof-insert-pbp-command 1999,76353
-(defun proof-insert-sendback-command 2014,76856
-(defun proof-done-retracting 2040,77759
-(defun proof-setup-retract-action 2075,79213
-(defun proof-last-goal-or-goalsave 2087,79818
-(defun proof-retract-target 2111,80730
-(defun proof-retract-until-point-interactive 2190,83983
-(defun proof-retract-until-point 2199,84390
-(define-derived-mode proof-mode 2254,86398
-(defun proof-script-set-visited-file-name 2290,87780
-(defun proof-script-set-buffer-hooks 2312,88793
-(defun proof-script-kill-buffer-fn 2320,89211
-(defun proof-config-done-related 2352,90528
-(defun proof-generic-goal-command-p 2417,93013
-(defun proof-generic-state-preserving-p 2422,93226
-(defun proof-generic-count-undos 2431,93743
-(defun proof-generic-find-and-forget 2462,94871
-(defconst proof-script-important-settings2513,96643
-(defun proof-config-done 2528,97189
-(defun proof-setup-parsing-mechanism 2595,99354
-(defun proof-setup-imenu 2619,100426
-(deflocal proof-segment-up-to-cache 2646,101204
-(deflocal proof-segment-up-to-cache-start 2647,101245
-(deflocal proof-last-edited-low-watermark 2648,101290
-(defun proof-segment-up-to-using-cache 2658,101777
-(defun proof-segment-cache-contents-for 2686,102779
-(defun proof-script-after-change-function 2698,103148
-(defun proof-script-set-after-change-functions 2710,103655
-
-generic/proof-shell.el,3652
+(defun proof-toggle-active-scripting 1278,49411
+(defun proof-done-advancing 1317,50656
+(defun proof-done-advancing-comment 1396,53641
+(defun proof-done-advancing-save 1430,55027
+(defun proof-make-goalsave1518,58391
+(defun proof-get-name-from-goal 1536,59256
+(defun proof-done-advancing-autosave 1556,60281
+(defun proof-done-advancing-other 1620,62777
+(defun proof-segment-up-to-parser 1649,63741
+(defun proof-script-generic-parse-find-comment-end 1718,66007
+(defun proof-script-generic-parse-cmdend 1727,66421
+(defun proof-script-generic-parse-cmdstart 1778,68317
+(defun proof-script-generic-parse-sexp 1817,69917
+(defun proof-semis-to-vanillas 1829,70383
+(defun proof-next-command-new-line 1882,72056
+(defun proof-script-next-command-advance 1887,72262
+(defun proof-assert-until-point 1906,72762
+(defun proof-assert-electric-terminator 1921,73389
+(defun proof-assert-semis 1964,75021
+(defun proof-retract-before-change 1978,75762
+(defun proof-insert-pbp-command 1998,76358
+(defun proof-insert-sendback-command 2013,76861
+(defun proof-done-retracting 2039,77764
+(defun proof-setup-retract-action 2074,79218
+(defun proof-last-goal-or-goalsave 2086,79823
+(defun proof-retract-target 2110,80735
+(defun proof-retract-until-point-interactive 2189,83988
+(defun proof-retract-until-point 2198,84395
+(define-derived-mode proof-mode 2253,86403
+(defun proof-script-set-visited-file-name 2289,87785
+(defun proof-script-set-buffer-hooks 2311,88798
+(defun proof-script-kill-buffer-fn 2319,89216
+(defun proof-config-done-related 2351,90533
+(defun proof-generic-goal-command-p 2416,93018
+(defun proof-generic-state-preserving-p 2421,93231
+(defun proof-generic-count-undos 2430,93748
+(defun proof-generic-find-and-forget 2461,94876
+(defconst proof-script-important-settings2512,96648
+(defun proof-config-done 2527,97194
+(defun proof-setup-parsing-mechanism 2594,99359
+(defun proof-setup-imenu 2618,100431
+(deflocal proof-segment-up-to-cache 2645,101209
+(deflocal proof-segment-up-to-cache-start 2646,101250
+(deflocal proof-last-edited-low-watermark 2647,101295
+(defun proof-segment-up-to-using-cache 2657,101782
+(defun proof-segment-cache-contents-for 2685,102784
+(defun proof-script-after-change-function 2697,103153
+(defun proof-script-set-after-change-functions 2709,103660
+
+generic/proof-shell.el,3653
 (defvar proof-marker 34,746
 (defvar proof-action-list 37,842
-(defsubst proof-shell-invoke-callback 75,2301
-(defvar proof-shell-last-goals-output 89,2793
-(defvar proof-shell-last-response-output 92,2873
-(defvar proof-shell-delayed-output-start 95,2960
-(defvar proof-shell-delayed-output-end 99,3142
-(defvar proof-shell-delayed-output-flags 103,3322
-(defvar proof-shell-interrupt-pending 106,3447
-(defcustom proof-shell-active-scripting-indicator117,3742
-(defun proof-shell-ready-prover 169,5326
-(defsubst proof-shell-live-buffer 183,5865
-(defun proof-shell-available-p 190,6085
-(defun proof-grab-lock 196,6307
-(defun proof-release-lock 206,6736
-(defcustom proof-shell-fiddle-frames 216,6910
-(defun proof-shell-set-text-representation 221,7068
-(defun proof-shell-start 229,7396
-(defvar proof-shell-kill-function-hooks 412,13632
-(defun proof-shell-kill-function 415,13730
-(defun proof-shell-clear-state 476,15848
-(defun proof-shell-exit 492,16323
-(defun proof-shell-bail-out 512,17095
-(defun proof-shell-restart 522,17617
-(defvar proof-shell-urgent-message-marker 563,18989
-(defvar proof-shell-urgent-message-scanner 566,19110
-(defun proof-shell-handle-error-output 570,19295
-(defun proof-shell-handle-error-or-interrupt 596,20157
-(defun proof-shell-error-or-interrupt-action 639,21906
-(defun proof-goals-pos 666,23003
-(defun proof-pbp-focus-on-first-goal 671,23214
-(defsubst proof-shell-string-match-safe 683,23630
-(defun proof-shell-handle-immediate-output 687,23791
-(defun proof-interrupt-process 754,26398
-(defun proof-shell-insert 788,27631
-(defun proof-shell-action-list-item 839,29457
-(defun proof-shell-set-silent 844,29699
-(defun proof-shell-start-silent-item 850,29918
-(defun proof-shell-clear-silent 856,30107
-(defun proof-shell-stop-silent-item 862,30329
-(defsubst proof-shell-should-be-silent 868,30518
-(defsubst proof-shell-insert-action-item 879,31028
-(defsubst proof-shell-slurp-comments 883,31203
-(defun proof-add-to-queue 894,31608
-(defun proof-start-queue 952,33632
-(defun proof-extend-queue 964,34027
-(defun proof-shell-exec-loop 983,34646
-(defun proof-shell-insert-loopback-cmd 1051,36949
-(defun proof-shell-process-urgent-message 1076,38113
-(defun proof-shell-process-urgent-message-default 1125,39833
-(defun proof-shell-process-urgent-message-trace 1141,40417
-(defun proof-shell-process-urgent-message-retract 1153,40940
-(defun proof-shell-process-urgent-message-elisp 1179,42070
-(defun proof-shell-process-urgent-message-thmdeps 1194,42565
-(defun proof-shell-strip-eager-annotations 1208,42944
-(defun proof-shell-filter 1224,43444
-(defun proof-shell-filter-first-command 1324,46816
-(defun proof-shell-process-urgent-messages 1339,47359
-(defun proof-shell-filter-manage-output 1389,48925
-(defsubst proof-shell-display-output-as-response 1421,50172
-(defun proof-shell-handle-delayed-output 1427,50467
-(defvar pg-last-tracing-output-time 1514,53595
-(defvar pg-last-trace-output-count 1517,53708
-(defconst pg-slow-mode-trigger-count 1520,53793
-(defconst pg-slow-mode-duration 1523,53898
-(defconst pg-fast-tracing-mode-threshold 1526,53980
-(defun pg-tracing-tight-loop 1529,54109
-(defun pg-finish-tracing-display 1553,55141
-(defun proof-shell-wait 1571,55522
-(defun proof-done-invisible 1601,56733
-(defun proof-shell-invisible-command 1607,56903
-(defun proof-shell-invisible-cmd-get-result 1654,58495
-(defun proof-shell-invisible-command-invisible-result 1666,58931
-(defun pg-insert-last-output-as-comment 1686,59432
-(define-derived-mode proof-shell-mode 1705,59904
-(defconst proof-shell-important-settings1742,60931
-(defun proof-shell-config-done 1748,61046
+(defsubst proof-shell-invoke-callback 77,2388
+(defvar proof-shell-last-goals-output 91,2880
+(defvar proof-shell-last-response-output 94,2960
+(defvar proof-shell-delayed-output-start 97,3047
+(defvar proof-shell-delayed-output-end 101,3229
+(defvar proof-shell-delayed-output-flags 105,3409
+(defvar proof-shell-interrupt-pending 108,3534
+(defcustom proof-shell-active-scripting-indicator119,3829
+(defun proof-shell-ready-prover 171,5413
+(defsubst proof-shell-live-buffer 185,5952
+(defun proof-shell-available-p 192,6172
+(defun proof-grab-lock 198,6394
+(defun proof-release-lock 208,6823
+(defcustom proof-shell-fiddle-frames 218,6997
+(defun proof-shell-set-text-representation 223,7155
+(defun proof-shell-start 231,7483
+(defvar proof-shell-kill-function-hooks 414,13719
+(defun proof-shell-kill-function 417,13817
+(defun proof-shell-clear-state 478,15935
+(defun proof-shell-exit 494,16410
+(defun proof-shell-bail-out 514,17182
+(defun proof-shell-restart 524,17704
+(defvar proof-shell-urgent-message-marker 565,19076
+(defvar proof-shell-urgent-message-scanner 568,19197
+(defun proof-shell-handle-error-output 572,19382
+(defun proof-shell-handle-error-or-interrupt 598,20244
+(defun proof-shell-error-or-interrupt-action 641,21993
+(defun proof-goals-pos 668,23090
+(defun proof-pbp-focus-on-first-goal 673,23301
+(defsubst proof-shell-string-match-safe 685,23717
+(defun proof-shell-handle-immediate-output 689,23878
+(defun proof-interrupt-process 756,26485
+(defun proof-shell-insert 790,27718
+(defun proof-shell-action-list-item 841,29544
+(defun proof-shell-set-silent 846,29786
+(defun proof-shell-start-silent-item 852,30005
+(defun proof-shell-clear-silent 858,30194
+(defun proof-shell-stop-silent-item 864,30416
+(defsubst proof-shell-should-be-silent 870,30605
+(defsubst proof-shell-insert-action-item 881,31115
+(defsubst proof-shell-slurp-comments 885,31290
+(defun proof-add-to-queue 896,31695
+(defun proof-start-queue 954,33719
+(defun proof-extend-queue 966,34114
+(defun proof-shell-exec-loop 985,34733
+(defun proof-shell-insert-loopback-cmd 1053,37036
+(defun proof-shell-process-urgent-message 1078,38200
+(defun proof-shell-process-urgent-message-default 1127,39920
+(defun proof-shell-process-urgent-message-trace 1143,40504
+(defun proof-shell-process-urgent-message-retract 1155,41027
+(defun proof-shell-process-urgent-message-elisp 1181,42157
+(defun proof-shell-process-urgent-message-thmdeps 1196,42652
+(defun proof-shell-strip-eager-annotations 1210,43031
+(defun proof-shell-filter 1226,43531
+(defun proof-shell-filter-first-command 1326,46903
+(defun proof-shell-process-urgent-messages 1341,47446
+(defun proof-shell-filter-manage-output 1391,49012
+(defsubst proof-shell-display-output-as-response 1423,50259
+(defun proof-shell-handle-delayed-output 1429,50554
+(defvar pg-last-tracing-output-time 1516,53688
+(defvar pg-last-trace-output-count 1519,53801
+(defconst pg-slow-mode-trigger-count 1522,53886
+(defconst pg-slow-mode-duration 1525,53991
+(defconst pg-fast-tracing-mode-threshold 1528,54073
+(defun pg-tracing-tight-loop 1531,54202
+(defun pg-finish-tracing-display 1555,55234
+(defun proof-shell-wait 1573,55615
+(defun proof-done-invisible 1603,56826
+(defun proof-shell-invisible-command 1609,56996
+(defun proof-shell-invisible-cmd-get-result 1656,58588
+(defun proof-shell-invisible-command-invisible-result 1668,59024
+(defun pg-insert-last-output-as-comment 1688,59525
+(define-derived-mode proof-shell-mode 1707,59997
+(defconst proof-shell-important-settings1744,61024
+(defun proof-shell-config-done 1750,61139
 
 generic/proof-site.el,665
 (defconst proof-assistant-table-default26,771
@@ -2084,12 +2084,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,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
+(defconst pg-dev-lisp-font-lock-keywords52,1580
+(defun pg-loadpath 78,2279
+(defun unload-pg 88,2450
+(defun profile-pg 119,3344
+(defun elp-pack-number 149,4451
+(defun pg-bug-references 158,4651
 
 lib/pg-fontsets.el,209
 (defcustom pg-fontsets-default-fontset 24,722
@@ -2381,34 +2381,34 @@ contrib/mmm/mmm-mason.el,410
 (defun mmm-mason-end-line 161,4903
 (defun mmm-mason-set-mode-line 168,4997
 
-contrib/mmm/mmm-mode.el,1023
+contrib/mmm/mmm-mode.el,1025
 (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
+(defun mmm-mode-off 183,7156
+(defvar mmm-mode-map 209,7897
+(defvar mmm-mode-prefix-map 212,7972
+(defvar mmm-mode-menu-map 215,8082
+(defun mmm-define-key 218,8173
+(define-key mmm-mode-prefix-map 242,8928
+(define-key mmm-mode-prefix-map 249,9186
+(define-key mmm-mode-map 252,9297
+(define-key mmm-mode-menu-map 255,9399
+(define-key mmm-mode-menu-map 257,9471
+(define-key mmm-mode-menu-map 259,9530
+(define-key mmm-mode-menu-map 261,9611
+(define-key mmm-mode-menu-map 263,9692
+(define-key mmm-mode-menu-map 265,9779
+(define-key mmm-mode-menu-map 268,9873
+(define-key mmm-mode-menu-map 270,9933
+(define-key mmm-mode-menu-map 273,10024
+(define-key mmm-mode-menu-map 275,10084
+(define-key mmm-mode-menu-map 277,10191
+(define-key mmm-mode-menu-map 279,10276
+(define-key mmm-mode-menu-map 282,10362
+(define-key mmm-mode-menu-map 284,10422
+(define-key mmm-mode-menu-map 286,10535
+(define-key mmm-mode-menu-map 288,10620
+(define-key mmm-mode-map 291,10703
 
 contrib/mmm/mmm-region.el,1643
 (defsubst mmm-overlay-at 54,1749
@@ -2435,25 +2435,25 @@ contrib/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 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
+(defun mmm-update-submode-region 572,21874
+(defun mmm-add-hooks 589,22604
+(defun mmm-remove-hooks 592,22701
+(defun mmm-get-local-variables-list 598,22828
+(defun mmm-get-locals 618,23524
+(defun mmm-get-saved-local 631,24021
+(defun mmm-set-local-variables 635,24186
+(defun mmm-get-saved-local-variables 646,24564
+(defun mmm-save-changed-local-variables 654,24839
+(defun mmm-clear-local-variables 673,25543
+(defun mmm-enable-font-lock 684,25808
+(defun mmm-update-font-lock-buffer 692,26068
+(defun mmm-refontify-maybe 705,26479
+(defun mmm-submode-changes-in 720,26959
+(defun mmm-regions-in 731,27316
+(defun mmm-regions-alist 745,27794
+(defun mmm-fontify-region 762,28321
+(defun mmm-fontify-region-list 783,29343
+(defun mmm-beginning-of-syntax 805,30091
 
 contrib/mmm/mmm-rpm.el,154
 (defconst mmm-rpm-sh-start-tags48,1618