update TAGS

1 files changed, 576 insertions, 521 deletions

diff --git a/TAGS b/TAGS
index 9d7c6b73..567f1f4d 100644
--- a/TAGS
+++ b/TAGS
@@ -21,34 +21,50 @@ coq/coq-abbrev.el,590
 (defpgdefault help-menu-entries213,8253
 (defpgdefault other-buffers-menu-entries 217,8383
 
-coq/coq-compile-common.el,1154
-(defun get-coq-library-directory 30,756
-(defconst coq-library-directory 36,943
-(defcustom coq-dependency-analyzer39,1070
-(defcustom coq-compiler45,1210
-(defgroup coq-auto-compile 54,1379
-(defpacustom compile-before-require 59,1530
-(defcustom coq-compile-command 71,2022
-(defconst coq-compile-substitution-list101,3301
-(defcustom coq-load-path 121,4222
-(defcustom coq-compile-auto-save 158,5967
-(defcustom coq-lock-ancestors 183,7024
-(defpacustom confirm-external-compilation 192,7345
-(defcustom coq-load-path-include-current 201,7652
-(defcustom coq-compile-ignored-directories 210,7970
-(defcustom coq-compile-ignore-library-directory 223,8602
-(defcustom coq-coqdep-error-regexp235,9090
-(defconst coq-require-command-regexp252,9869
-(defconst coq-require-id-regexp259,10226
-(defvar coq-compile-history 267,10660
-(defvar coq-compile-response-buffer 270,10744
-(defvar coq-debug-auto-compilation 274,10879
-(defun time-less-or-equal 280,10987
-(defun coq-max-dep-mod-time 288,11325
-(defun coq-load-path-safep 311,12123
-(defun coq-option-of-load-path-entry 333,12764
-(defun coq-include-options 347,13279
-(defun coq-prog-args 369,14199
+coq/coq-compile-common.el,1880
+(defun get-coq-library-directory 31,820
+(defconst coq-library-directory 37,1007
+(defcustom coq-dependency-analyzer40,1134
+(defcustom coq-compiler46,1274
+(defun coq-par-enable 60,1799
+(defun coq-par-disable 68,2071
+(defun coq-seq-enable 76,2356
+(defun coq-seq-disable 82,2562
+(defun coq-load-path-safep 91,2813
+(defun coq-switch-compilation-method 111,3409
+(defgroup coq-auto-compile 123,3677
+(defpacustom compile-before-require 128,3828
+(defpacustom compile-parallel-in-background 140,4320
+(defcustom coq-compile-command 161,5210
+(defconst coq-compile-substitution-list191,6489
+(defcustom coq-load-path 211,7410
+(defcustom coq-compile-auto-save 248,9155
+(defcustom coq-lock-ancestors 273,10212
+(defpacustom confirm-external-compilation 282,10533
+(defcustom coq-load-path-include-current 291,10840
+(defcustom coq-compile-ignored-directories 300,11158
+(defcustom coq-compile-ignore-library-directory 313,11790
+(defcustom coq-coqdep-error-regexp325,12278
+(defconst coq-require-command-regexp342,13057
+(defconst coq-require-id-regexp349,13414
+(defvar coq-compile-history 357,13848
+(defvar coq-compile-response-buffer 360,13932
+(defvar coq-debug-auto-compilation 364,14067
+(defun time-less-or-equal 370,14176
+(defun coq-max-dep-mod-time 378,14514
+(defun coq-option-of-load-path-entry 401,15319
+(defun coq-include-options 415,15834
+(defun coq-prog-args 439,16853
+(defun coq-compile-ignore-file 448,17126
+(defun coq-library-src-of-obj-file 474,18048
+(defun coq-unlock-ancestor 483,18372
+(defun coq-unlock-all-ancestors-of-span 490,18667
+(defun coq-init-compile-response-buffer 498,18952
+(defun coq-display-compile-response-buffer 521,20024
+(defvar coq-compile-buffer-with-current-require534,20543
+(defun coq-compile-save-buffer-filter 540,20779
+(defun coq-compile-save-some-buffers 551,21205
+(defun coq-switch-buffer-kill-proof-shell 576,22159
 
 coq/coq-db.el,678
 (defconst coq-syntax-db 24,596
@@ -70,218 +86,218 @@ coq/coq-db.el,678
 (defconst coq-cheat-face 270,9679
 
 coq/coq.el,8821
-(defcustom coq-prog-name60,1986
-(defcustom coq-translate-to-v8 79,2837
-(defun coq-build-prog-args 84,2952
-(defcustom coq-use-makefile 94,3275
-(defcustom coq-default-undo-limit 100,3447
-(defconst coq-shell-init-cmd105,3575
-(defcustom coq-prog-env 114,3902
-(defconst coq-shell-restart-cmd 122,4151
-(defvar coq-shell-prompt-pattern124,4205
-(defvar coq-shell-cd 132,4508
-(defvar coq-shell-proof-completed-regexp 136,4668
-(defvar coq-goal-regexp139,4883
-(defcustom coq-tags 143,4974
-(defconst coq-interrupt-regexp 148,5122
-(defcustom coq-www-home-page 151,5215
-(defcustom coq-end-goals-regexp-show-subgoals 156,5322
-(defcustom coq-end-goals-regexp-hide-subgoals163,5606
-(defgroup coq-proof-tree 174,5938
-(defcustom coq-proof-tree-ignored-commands-regexp182,6301
-(defcustom coq-navigation-command-regexp191,6695
-(defcustom coq-proof-tree-cheating-regexp197,6867
-(defcustom coq-proof-tree-current-goal-regexp203,7007
-(defcustom coq-proof-tree-update-goal-regexp211,7341
-(defcustom coq-proof-tree-additional-subgoal-ID-regexp218,7575
-(defcustom coq-proof-tree-existential-regexp 224,7773
-(defcustom coq-proof-tree-instantiated-existential-regexp229,7927
-(defcustom coq-proof-tree-existentials-state-start-regexp235,8147
-(defcustom coq-proof-tree-existentials-state-end-regexp 241,8337
-(defcustom coq-proof-tree-proof-finished-regexp246,8506
-(defvar coq-outline-regexp258,8775
-(defvar coq-outline-heading-end-regexp 267,9049
-(defvar coq-shell-outline-regexp 269,9103
-(defvar coq-shell-outline-heading-end-regexp 270,9153
-(defconst coq-state-preserving-tactics-regexp273,9217
-(defconst coq-state-changing-commands-regexp275,9319
-(defconst coq-state-preserving-commands-regexp277,9428
-(defconst coq-commands-regexp279,9541
-(defvar coq-retractable-instruct-regexp281,9620
-(defvar coq-non-retractable-instruct-regexp283,9712
-(defcustom coq-use-smie 315,10408
-(defconst coq-script-command-end-regexp 340,11246
-(defun coq-script-parse-function 349,11675
-(defun coq-set-undo-limit 356,11901
-(defun build-list-id-from-string 362,12033
-(defun coq-last-prompt-info 371,12508
-(defun coq-last-prompt-info-safe 389,13402
-(defvar coq-last-but-one-statenum 397,13755
-(defvar coq-last-but-one-proofnum 404,14052
-(defvar coq-last-but-one-proofstack 407,14150
-(defsubst coq-get-span-statenum 410,14260
-(defsubst coq-get-span-proofnum 414,14375
-(defsubst coq-get-span-proofstack 418,14490
-(defsubst coq-set-span-statenum 422,14634
-(defsubst coq-get-span-goalcmd 426,14765
-(defsubst coq-set-span-goalcmd 430,14879
-(defsubst coq-set-span-proofnum 434,15009
-(defsubst coq-set-span-proofstack 438,15140
-(defsubst proof-last-locked-span 442,15300
-(defun proof-clone-buffer 446,15434
-(defun proof-store-buffer-win 460,15971
-(defun proof-store-response-win 471,16464
-(defun proof-store-goals-win 475,16591
-(defun coq-set-state-infos 487,17123
-(defun count-not-intersection 525,19213
-(defun coq-find-and-forget 555,20465
-(defvar coq-current-goal 582,21770
-(defun coq-goal-hyp 585,21835
-(defun coq-state-preserving-p 598,22315
-(defun coq-hide-additional-subgoals-switch 608,22609
-(defconst notation-print-kinds-table620,22950
-(defun coq-PrintScope 624,23117
-(defun coq-remove-trailing-dot 642,23666
-(defun coq-id-at-point 650,23903
-(defun coq-guess-or-ask-for-string 664,24466
-(defun coq-ask-do 683,25081
-(defun coq-flag-is-on-p 692,25464
-(defun coq-command-with-set-unset 698,25671
-(defun coq-ask-do-set-unset 709,26321
-(defun coq-ask-do-show-implicits 719,26851
-(defun coq-ask-do-show-all 727,27211
-(defsubst coq-put-into-brackets 748,27892
-(defsubst coq-put-into-quotes 751,27953
-(defun coq-SearchIsos 754,28012
-(defun coq-SearchConstant 762,28251
-(defun coq-Searchregexp 766,28344
-(defun coq-SearchRewrite 772,28485
-(defun coq-SearchAbout 776,28582
-(defun coq-Print 782,28725
-(defun coq-Print-with-implicits 790,28995
-(defun coq-Print-with-all 795,29149
-(defun coq-About 800,29291
-(defun coq-About-with-implicits 807,29498
-(defun coq-About-with-all 812,29647
-(defun coq-LocateConstant 818,29785
-(defun coq-LocateLibrary 823,29888
-(defun coq-LocateNotation 828,30005
-(defun coq-Pwd 836,30236
-(defun coq-Inspect 841,30360
-(defun coq-PrintSection(845,30460
-(defun coq-Print-implicit 849,30553
-(defun coq-Check 854,30704
-(defun coq-Check-show-implicits 862,30958
-(defun coq-Check-show-all 867,31096
-(defun coq-get-response-string-at 872,31222
-(defun coq-Show 886,31812
-(defun coq-Show-with-implicits 916,33220
-(defun coq-Show-with-all 921,33376
-(defun coq-Compile 948,34753
-(defun coq-guess-command-line 960,35078
-(defun coq-mode-config 1018,37430
-(defun coq-shell-mode-config 1129,41541
-(defun coq-goals-mode-config 1220,45339
-(defun coq-response-config 1227,45583
-(defpacustom hide-additional-subgoals 1250,46300
-(defpacustom printing-depth 1271,46963
-(defpacustom undo-depth 1276,47124
-(defpacustom time-commands 1281,47290
-(defun coq-proof-tree-get-proof-info 1291,47495
-(defun coq-extract-instantiated-existentials 1301,47883
-(defun coq-show-sequent-command 1310,48275
-(defun coq-proof-tree-get-new-subgoals 1314,48429
-(defun coq-find-begin-of-unfinished-proof 1358,50554
-(defun coq-preprocessing 1383,51568
-(defun coq-fake-constant-markup 1397,52023
-(defun coq-create-span-menu 1413,52628
-(defconst module-kinds-table1431,53141
-(defconst modtype-kinds-table1435,53290
-(defun coq-postfix-.v-p 1439,53419
-(defun coq-directories-files 1442,53480
-(defun coq-remove-dot-v-extension 1448,53708
-(defun coq-load-path-to-paths 1451,53769
-(defun coq-build-accessible-modules-list 1454,53848
-(defun coq-insert-section-or-module 1461,54165
-(defconst reqkinds-kinds-table1483,55045
-(defun coq-insert-requires 1487,55202
-(defun coq-end-Section 1501,55755
-(defun coq-insert-intros 1519,56333
-(defvar coq-commands-accepting-as 1532,56865
-(defvar coq-last-input-action 1534,56964
-(defun coq-insert-infoH 1540,57180
-(defun coq-auto-insert-as 1554,57845
-(defpacustom auto-insert-as 1564,58259
-(defun coq-tactic-already-has-an-as-close(1571,58494
-(defun coq-insert-as 1586,59259
-(defun coq-insert-as-in-region 1625,61355
-(defun coq-insert-match 1637,61628
-(defun coq-insert-solve-tactic 1666,62797
-(defun coq-insert-tactic 1672,63048
-(defun coq-insert-tactical 1678,63250
-(defun coq-insert-command 1684,63481
-(defun coq-insert-term 1689,63646
-(define-key coq-keymap 1695,63829
-(define-key coq-keymap 1696,63887
-(define-key coq-keymap 1697,63944
-(define-key coq-keymap 1698,64013
-(define-key coq-keymap 1699,64069
-(define-key coq-keymap 1700,64127
-(define-key coq-keymap 1701,64177
-(define-key coq-keymap 1702,64250
-(define-key coq-keymap 1703,64307
+(defcustom coq-prog-name61,2049
+(defcustom coq-translate-to-v8 80,2900
+(defun coq-build-prog-args 85,3015
+(defcustom coq-use-makefile 95,3338
+(defcustom coq-default-undo-limit 101,3510
+(defconst coq-shell-init-cmd106,3638
+(defcustom coq-prog-env 115,3965
+(defconst coq-shell-restart-cmd 123,4214
+(defvar coq-shell-prompt-pattern125,4268
+(defvar coq-shell-cd 133,4571
+(defvar coq-shell-proof-completed-regexp 137,4731
+(defvar coq-goal-regexp140,4946
+(defcustom coq-tags 144,5037
+(defconst coq-interrupt-regexp 149,5185
+(defcustom coq-www-home-page 152,5278
+(defcustom coq-end-goals-regexp-show-subgoals 157,5385
+(defcustom coq-end-goals-regexp-hide-subgoals164,5669
+(defgroup coq-proof-tree 175,6001
+(defcustom coq-proof-tree-ignored-commands-regexp183,6364
+(defcustom coq-navigation-command-regexp192,6758
+(defcustom coq-proof-tree-cheating-regexp198,6930
+(defcustom coq-proof-tree-current-goal-regexp204,7070
+(defcustom coq-proof-tree-update-goal-regexp212,7404
+(defcustom coq-proof-tree-additional-subgoal-ID-regexp219,7638
+(defcustom coq-proof-tree-existential-regexp 225,7836
+(defcustom coq-proof-tree-instantiated-existential-regexp230,7990
+(defcustom coq-proof-tree-existentials-state-start-regexp236,8210
+(defcustom coq-proof-tree-existentials-state-end-regexp 242,8400
+(defcustom coq-proof-tree-proof-finished-regexp247,8569
+(defvar coq-outline-regexp259,8838
+(defvar coq-outline-heading-end-regexp 268,9112
+(defvar coq-shell-outline-regexp 270,9166
+(defvar coq-shell-outline-heading-end-regexp 271,9216
+(defconst coq-state-preserving-tactics-regexp274,9280
+(defconst coq-state-changing-commands-regexp276,9382
+(defconst coq-state-preserving-commands-regexp278,9491
+(defconst coq-commands-regexp280,9604
+(defvar coq-retractable-instruct-regexp282,9683
+(defvar coq-non-retractable-instruct-regexp284,9775
+(defcustom coq-use-smie 316,10471
+(defconst coq-script-command-end-regexp 341,11309
+(defun coq-script-parse-function 350,11738
+(defun coq-set-undo-limit 357,11964
+(defun build-list-id-from-string 363,12096
+(defun coq-last-prompt-info 372,12571
+(defun coq-last-prompt-info-safe 390,13465
+(defvar coq-last-but-one-statenum 398,13818
+(defvar coq-last-but-one-proofnum 405,14115
+(defvar coq-last-but-one-proofstack 408,14213
+(defsubst coq-get-span-statenum 411,14323
+(defsubst coq-get-span-proofnum 415,14438
+(defsubst coq-get-span-proofstack 419,14553
+(defsubst coq-set-span-statenum 423,14697
+(defsubst coq-get-span-goalcmd 427,14828
+(defsubst coq-set-span-goalcmd 431,14942
+(defsubst coq-set-span-proofnum 435,15072
+(defsubst coq-set-span-proofstack 439,15203
+(defsubst proof-last-locked-span 443,15363
+(defun proof-clone-buffer 447,15497
+(defun proof-store-buffer-win 461,16034
+(defun proof-store-response-win 472,16527
+(defun proof-store-goals-win 476,16654
+(defun coq-set-state-infos 488,17186
+(defun count-not-intersection 526,19276
+(defun coq-find-and-forget 556,20528
+(defvar coq-current-goal 583,21833
+(defun coq-goal-hyp 586,21898
+(defun coq-state-preserving-p 599,22378
+(defun coq-hide-additional-subgoals-switch 609,22672
+(defconst notation-print-kinds-table621,23013
+(defun coq-PrintScope 625,23180
+(defun coq-remove-trailing-dot 643,23729
+(defun coq-id-at-point 651,23966
+(defun coq-guess-or-ask-for-string 665,24529
+(defun coq-ask-do 684,25144
+(defun coq-flag-is-on-p 693,25527
+(defun coq-command-with-set-unset 699,25734
+(defun coq-ask-do-set-unset 710,26384
+(defun coq-ask-do-show-implicits 720,26914
+(defun coq-ask-do-show-all 728,27274
+(defsubst coq-put-into-brackets 749,27955
+(defsubst coq-put-into-quotes 752,28016
+(defun coq-SearchIsos 755,28075
+(defun coq-SearchConstant 763,28314
+(defun coq-Searchregexp 767,28407
+(defun coq-SearchRewrite 773,28548
+(defun coq-SearchAbout 777,28645
+(defun coq-Print 783,28788
+(defun coq-Print-with-implicits 791,29058
+(defun coq-Print-with-all 796,29212
+(defun coq-About 801,29354
+(defun coq-About-with-implicits 808,29561
+(defun coq-About-with-all 813,29710
+(defun coq-LocateConstant 819,29848
+(defun coq-LocateLibrary 824,29951
+(defun coq-LocateNotation 829,30068
+(defun coq-Pwd 837,30299
+(defun coq-Inspect 842,30423
+(defun coq-PrintSection(846,30523
+(defun coq-Print-implicit 850,30616
+(defun coq-Check 855,30767
+(defun coq-Check-show-implicits 863,31021
+(defun coq-Check-show-all 868,31159
+(defun coq-get-response-string-at 873,31285
+(defun coq-Show 887,31875
+(defun coq-Show-with-implicits 917,33283
+(defun coq-Show-with-all 922,33439
+(defun coq-Compile 949,34816
+(defun coq-guess-command-line 961,35141
+(defun coq-mode-config 1019,37493
+(defun coq-shell-mode-config 1130,41604
+(defun coq-goals-mode-config 1221,45402
+(defun coq-response-config 1228,45646
+(defpacustom hide-additional-subgoals 1251,46363
+(defpacustom printing-depth 1272,47026
+(defpacustom undo-depth 1277,47187
+(defpacustom time-commands 1282,47353
+(defun coq-proof-tree-get-proof-info 1292,47558
+(defun coq-extract-instantiated-existentials 1302,47946
+(defun coq-show-sequent-command 1311,48338
+(defun coq-proof-tree-get-new-subgoals 1315,48492
+(defun coq-find-begin-of-unfinished-proof 1359,50617
+(defun coq-preprocessing 1384,51631
+(defun coq-fake-constant-markup 1398,52086
+(defun coq-create-span-menu 1414,52691
+(defconst module-kinds-table1432,53204
+(defconst modtype-kinds-table1436,53353
+(defun coq-postfix-.v-p 1440,53482
+(defun coq-directories-files 1443,53543
+(defun coq-remove-dot-v-extension 1449,53771
+(defun coq-load-path-to-paths 1452,53832
+(defun coq-build-accessible-modules-list 1455,53911
+(defun coq-insert-section-or-module 1462,54228
+(defconst reqkinds-kinds-table1484,55108
+(defun coq-insert-requires 1488,55265
+(defun coq-end-Section 1502,55818
+(defun coq-insert-intros 1520,56396
+(defvar coq-commands-accepting-as 1533,56928
+(defvar coq-last-input-action 1535,57027
+(defun coq-insert-infoH 1541,57243
+(defun coq-auto-insert-as 1555,57908
+(defpacustom auto-insert-as 1565,58322
+(defun coq-tactic-already-has-an-as-close(1572,58557
+(defun coq-insert-as 1587,59322
+(defun coq-insert-as-in-region 1626,61418
+(defun coq-insert-match 1638,61691
+(defun coq-insert-solve-tactic 1667,62860
+(defun coq-insert-tactic 1673,63111
+(defun coq-insert-tactical 1679,63313
+(defun coq-insert-command 1685,63544
+(defun coq-insert-term 1690,63709
+(define-key coq-keymap 1696,63892
+(define-key coq-keymap 1697,63950
+(define-key coq-keymap 1698,64007
+(define-key coq-keymap 1699,64076
+(define-key coq-keymap 1700,64132
+(define-key coq-keymap 1701,64190
+(define-key coq-keymap 1702,64240
+(define-key coq-keymap 1703,64313
 (define-key coq-keymap 1704,64370
-(define-key coq-keymap 1707,64448
-(define-key coq-keymap 1708,64497
-(define-key coq-keymap 1709,64552
-(define-key coq-keymap 1710,64604
-(define-key coq-keymap 1711,64659
-(define-key coq-keymap 1712,64709
-(define-key coq-keymap 1713,64759
-(define-key coq-keymap 1714,64815
-(define-key coq-keymap 1715,64865
-(define-key coq-keymap 1716,64909
-(define-key coq-keymap 1717,64968
-(define-key coq-goals-mode-map 1725,65236
-(define-key coq-goals-mode-map 1726,65318
-(define-key coq-goals-mode-map 1727,65400
-(define-key coq-goals-mode-map 1728,65487
-(define-key coq-goals-mode-map 1729,65569
-(define-key coq-goals-mode-map 1730,65657
-(define-key coq-goals-mode-map 1731,65738
-(define-key coq-goals-mode-map 1732,65825
-(define-key coq-goals-mode-map 1733,65909
-(define-key coq-response-mode-map 1736,65987
-(define-key coq-response-mode-map 1737,66072
-(define-key coq-response-mode-map 1738,66157
-(define-key coq-response-mode-map 1739,66247
-(define-key coq-response-mode-map 1740,66332
-(define-key coq-response-mode-map 1741,66423
-(define-key coq-response-mode-map 1742,66507
-(define-key coq-response-mode-map 1743,66607
-(define-key coq-response-mode-map 1744,66704
-(defvar last-coq-error-location 1751,66854
-(defun coq-get-last-error-location 1759,67238
-(defun coq-highlight-error 1809,69801
-(defun coq-highlight-error-hook 1837,70882
-(defun coq-first-word-before 1847,71099
-(defun coq-get-from-to-paren 1857,71430
-(defun coq-show-first-goal 1870,71836
-(defvar coq-modeline-string2 1886,72501
-(defvar coq-modeline-string1 1887,72535
-(defvar coq-modeline-string0 1888,72569
-(defun coq-build-subgoals-string 1889,72610
-(defun coq-update-minor-mode-alist 1895,72794
-(defun is-not-split-vertic 1929,74363
-(defun coq-optimise-resp-windows 1943,75156
-(defcustom coq-double-hit-enable 1983,76978
-(defadvice proof-electric-terminator-enable 2002,77764
-(defvar coq-double-hit-delay 2010,78142
-(defvar coq-double-hit-timer 2013,78257
-(defvar coq-double-hit-hot 2016,78337
-(defun coq-unset-double-hit-hot 2020,78433
-(defun coq-colon-self-insert 2028,78764
-(defun coq-terminator-insert 2042,79320
+(define-key coq-keymap 1705,64433
+(define-key coq-keymap 1708,64511
+(define-key coq-keymap 1709,64560
+(define-key coq-keymap 1710,64615
+(define-key coq-keymap 1711,64667
+(define-key coq-keymap 1712,64722
+(define-key coq-keymap 1713,64772
+(define-key coq-keymap 1714,64822
+(define-key coq-keymap 1715,64878
+(define-key coq-keymap 1716,64928
+(define-key coq-keymap 1717,64972
+(define-key coq-keymap 1718,65031
+(define-key coq-goals-mode-map 1726,65299
+(define-key coq-goals-mode-map 1727,65381
+(define-key coq-goals-mode-map 1728,65463
+(define-key coq-goals-mode-map 1729,65550
+(define-key coq-goals-mode-map 1730,65632
+(define-key coq-goals-mode-map 1731,65720
+(define-key coq-goals-mode-map 1732,65801
+(define-key coq-goals-mode-map 1733,65888
+(define-key coq-goals-mode-map 1734,65972
+(define-key coq-response-mode-map 1737,66050
+(define-key coq-response-mode-map 1738,66135
+(define-key coq-response-mode-map 1739,66220
+(define-key coq-response-mode-map 1740,66310
+(define-key coq-response-mode-map 1741,66395
+(define-key coq-response-mode-map 1742,66486
+(define-key coq-response-mode-map 1743,66570
+(define-key coq-response-mode-map 1744,66670
+(define-key coq-response-mode-map 1745,66767
+(defvar last-coq-error-location 1752,66917
+(defun coq-get-last-error-location 1760,67301
+(defun coq-highlight-error 1810,69864
+(defun coq-highlight-error-hook 1838,70945
+(defun coq-first-word-before 1848,71162
+(defun coq-get-from-to-paren 1858,71493
+(defun coq-show-first-goal 1871,71899
+(defvar coq-modeline-string2 1887,72564
+(defvar coq-modeline-string1 1888,72598
+(defvar coq-modeline-string0 1889,72632
+(defun coq-build-subgoals-string 1890,72673
+(defun coq-update-minor-mode-alist 1896,72857
+(defun is-not-split-vertic 1930,74426
+(defun coq-optimise-resp-windows 1944,75219
+(defcustom coq-double-hit-enable 1984,77041
+(defadvice proof-electric-terminator-enable 2003,77827
+(defvar coq-double-hit-delay 2011,78205
+(defvar coq-double-hit-timer 2014,78320
+(defvar coq-double-hit-hot 2017,78400
+(defun coq-unset-double-hit-hot 2021,78496
+(defun coq-colon-self-insert 2029,78827
+(defun coq-terminator-insert 2043,79383
 
 coq/coq-indent.el,2698
 (defconst coq-any-command-regexp20,368
@@ -356,26 +372,63 @@ coq/coq-local-vars.el,229
 (defun coq-ask-prog-name 135,5165
 (defun coq-ask-insert-coq-prog-name 152,5876
 
-coq/coq-seq-compile.el,862
-(defun coq-lock-ancestor 35,1055
-(defun coq-unlock-ancestor 51,1830
-(defun coq-unlock-all-ancestors-of-span 58,2125
-(defun coq-compile-ignore-file 65,2421
-(defun coq-library-src-of-obj-file 89,3308
-(defun coq-init-compile-response-buffer 94,3540
-(defun coq-display-compile-response-buffer 117,4612
-(defun coq-get-library-dependencies 131,5246
-(defun coq-compile-library 183,7641
-(defun coq-compile-library-if-necessary 210,8852
-(defun coq-make-lib-up-to-date 256,10724
-(defun coq-auto-compile-externally 312,13187
-(defun coq-map-module-id-to-obj-file 355,15333
-(defun coq-check-module 408,17935
-(defvar coq-process-require-current-buffer436,19377
-(defun coq-compile-save-buffer-filter 442,19642
-(defun coq-compile-save-some-buffers 452,20056
-(defun coq-preprocess-require-commands 474,20958
-(defun coq-switch-buffer-kill-proof-shell 507,22527
+coq/coq-par-compile.el,2021
+(defcustom coq-max-background-compilation-jobs 224,10071
+(defvar coq-par-ancestor-files 230,10265
+(defvar coq-current-background-jobs 246,10914
+(defvar coq-compilation-object-hash 249,11003
+(defvar coq-last-compilation-job 257,11376
+(defvar coq-par-next-id 261,11519
+(defun split-list-at-predicate 268,11676
+(defun coq-par-time-less 292,12528
+(defun coq-par-init-compilation-hash 302,12876
+(defun coq-par-init-ancestor-hash 306,13037
+(defconst coq-par-empty-compilation-queue 317,13322
+(defvar coq-par-compilation-queue320,13431
+(defun coq-par-enqueue 325,13617
+(defun coq-par-dequeue 331,13851
+(defun coq-par-coq-arguments 366,14905
+(defun coq-par-analyse-coq-dep-exit 374,15274
+(defun coq-par-get-library-dependencies 393,16057
+(defun coq-par-map-module-id-to-obj-file 437,18027
+(defun coq-par-kill-all-processes 496,20856
+(defun coq-par-unlock-ancestors-on-error 506,21188
+(defun coq-par-emergency-cleanup 516,21531
+(defun coq-par-process-filter 532,22152
+(defun coq-par-start-process 537,22361
+(defun coq-par-process-sentinel 563,23623
+(defun coq-par-job-is-ready 598,24927
+(defun coq-par-dependencies-ready 602,25033
+(defun coq-par-add-coqc-dependency 606,25177
+(defun coq-par-add-queue-dependency 615,25590
+(defun coq-par-get-obj-mod-time 625,26056
+(defun coq-par-job-needs-compilation 639,26586
+(defun coq-par-kickoff-queue-maybe 668,27817
+(defun coq-par-compile-job-maybe 733,30617
+(defun coq-par-decrease-coqc-dependency 747,31288
+(defun coq-par-kickoff-coqc-dependants 782,33058
+(defun coq-par-start-coqdep 824,34988
+(defun coq-par-start-task 840,35644
+(defun coq-par-start-jobs-until-full 856,36205
+(defun coq-par-start-or-enqueue 866,36521
+(defun coq-par-create-library-job 875,36922
+(defun coq-par-process-coqdep-result 947,40080
+(defun coq-par-coqc-continuation 1004,42525
+(defun coq-par-handle-module 1027,43371
+(defun coq-par-handle-require-list 1055,44571
+(defun coq-par-item-require-predicate 1101,46629
+(defun coq-par-preprocess-require-commands 1110,46952
+
+coq/coq-seq-compile.el,422
+(defun coq-seq-lock-ancestor 38,1174
+(defun coq-seq-get-library-dependencies 56,2005
+(defun coq-seq-compile-library 109,4420
+(defun coq-seq-compile-library-if-necessary 136,5649
+(defun coq-seq-make-lib-up-to-date 182,7533
+(defun coq-seq-auto-compile-externally 240,10027
+(defun coq-seq-map-module-id-to-obj-file 284,12191
+(defun coq-seq-check-module 337,14809
+(defun coq-seq-preprocess-require-commands 365,16275
 
 coq/coq-smie-lexer.el,862
 (defconst coq-smie-dot-friends 21,987
@@ -1410,163 +1463,164 @@ generic/proof-auxmodes.el,149
 (defun proof-maths-menu-support-available 42,1096
 (defun proof-unicode-tokens-support-available 56,1513
 
-generic/proof-config.el,7845
-(defgroup prover-config 80,2632
-(defcustom proof-guess-command-line 98,3482
-(defcustom proof-assistant-home-page 113,3977
-(defcustom proof-context-command 119,4147
-(defcustom proof-info-command 124,4281
-(defcustom proof-showproof-command 131,4552
-(defcustom proof-goal-command 136,4688
-(defcustom proof-save-command 144,4985
-(defcustom proof-find-theorems-command 152,5294
-(defcustom proof-query-identifier-command 159,5602
-(defcustom proof-assistant-true-value 173,6291
-(defcustom proof-assistant-false-value 179,6481
-(defcustom proof-assistant-format-int-fn 185,6675
-(defcustom proof-assistant-format-float-fn 192,6924
-(defcustom proof-assistant-format-string-fn 199,7179
-(defcustom proof-assistant-setting-format 206,7446
-(defcustom proof-tree-configured 216,7929
-(defgroup proof-script 234,8395
-(defcustom proof-terminal-string 239,8525
-(defcustom proof-electric-terminator-noterminator 249,8913
-(defcustom proof-script-sexp-commands 254,9085
-(defcustom proof-script-command-end-regexp 265,9544
-(defcustom proof-script-command-start-regexp 283,10365
-(defcustom proof-script-integral-proofs 294,10828
-(defcustom proof-script-fly-past-comments 309,11484
-(defcustom proof-script-parse-function 314,11655
-(defcustom proof-script-comment-start 332,12300
-(defcustom proof-script-comment-start-regexp 343,12737
-(defcustom proof-script-comment-end 351,13056
-(defcustom proof-script-comment-end-regexp 363,13478
-(defcustom proof-string-start-regexp 371,13791
-(defcustom proof-string-end-regexp 376,13956
-(defcustom proof-case-fold-search 381,14117
-(defcustom proof-save-command-regexp 390,14529
-(defcustom proof-save-with-hole-regexp 395,14639
-(defcustom proof-save-with-hole-result 406,15014
-(defcustom proof-goal-command-regexp 416,15458
-(defcustom proof-goal-with-hole-regexp 424,15745
-(defcustom proof-goal-with-hole-result 436,16188
-(defcustom proof-non-undoables-regexp 445,16566
-(defcustom proof-nested-undo-regexp 456,17029
-(defcustom proof-ignore-for-undo-count 472,17749
-(defcustom proof-script-imenu-generic-expression 480,18060
-(defcustom proof-goal-command-p 488,18399
-(defcustom proof-really-save-command-p 499,18890
-(defcustom proof-completed-proof-behaviour 508,19197
-(defcustom proof-count-undos-fn 536,20546
-(defcustom proof-find-and-forget-fn 548,21097
-(defcustom proof-forget-id-command 565,21806
-(defcustom pg-topterm-goalhyplit-fn 575,22164
-(defcustom proof-kill-goal-command 587,22707
-(defcustom proof-undo-n-times-cmd 601,23211
-(defcustom proof-nested-goals-history-p 615,23748
-(defcustom proof-arbitrary-undo-positions 624,24085
-(defcustom proof-state-preserving-p 638,24666
-(defcustom proof-activate-scripting-hook 648,25138
-(defcustom proof-deactivate-scripting-hook 667,25919
-(defcustom proof-no-fully-processed-buffer 676,26249
-(defcustom proof-script-evaluate-elisp-comment-regexp 687,26747
-(defcustom proof-indent 705,27333
-(defcustom proof-indent-hang 710,27440
-(defcustom proof-indent-enclose-offset 715,27566
-(defcustom proof-indent-open-offset 720,27708
-(defcustom proof-indent-close-offset 725,27845
-(defcustom proof-indent-any-regexp 730,27983
-(defcustom proof-indent-inner-regexp 735,28143
-(defcustom proof-indent-enclose-regexp 740,28297
-(defcustom proof-indent-open-regexp 745,28451
-(defcustom proof-indent-close-regexp 750,28603
-(defcustom proof-script-font-lock-keywords 756,28757
-(defcustom proof-script-syntax-table-entries 764,29109
-(defcustom proof-script-span-context-menu-extensions 782,29505
-(defgroup proof-shell 808,30265
-(defcustom proof-prog-name 818,30435
-(defcustom proof-shell-auto-terminate-commands 830,30902
-(defcustom proof-shell-pre-sync-init-cmd 839,31307
-(defcustom proof-shell-init-cmd 853,31865
-(defcustom proof-shell-init-hook 865,32411
-(defcustom proof-shell-restart-cmd 870,32550
-(defcustom proof-shell-quit-cmd 875,32705
-(defcustom proof-shell-cd-cmd 880,32872
-(defcustom proof-shell-start-silent-cmd 897,33543
-(defcustom proof-shell-stop-silent-cmd 906,33919
-(defcustom proof-shell-silent-threshold 915,34254
-(defcustom  proof-shell-inform-file-processed-cmd 923,34588
-(defcustom  proof-shell-inform-file-retracted-cmd 944,35516
-(defcustom proof-auto-multiple-files 972,36788
-(defcustom proof-cannot-reopen-processed-files 987,37509
-(defcustom proof-shell-annotated-prompt-regexp 1007,38300
-(defcustom proof-shell-error-regexp 1022,38865
-(defcustom proof-shell-truncate-before-error 1042,39675
-(defcustom pg-next-error-regexp 1056,40214
-(defcustom pg-next-error-filename-regexp 1071,40823
-(defcustom pg-next-error-extract-filename 1095,41856
-(defcustom proof-shell-interrupt-regexp 1102,42099
-(defcustom proof-shell-proof-completed-regexp 1116,42702
-(defcustom proof-shell-clear-response-regexp 1129,43218
-(defcustom proof-shell-clear-goals-regexp 1141,43678
-(defcustom proof-shell-start-goals-regexp 1153,44132
-(defcustom proof-shell-end-goals-regexp 1166,44707
-(defcustom proof-shell-eager-annotation-start 1180,45297
-(defcustom proof-shell-eager-annotation-start-length 1203,46316
-(defcustom proof-shell-eager-annotation-end 1214,46742
-(defcustom proof-shell-strip-output-markup 1230,47417
-(defcustom proof-shell-assumption-regexp 1239,47802
-(defcustom proof-shell-process-file 1249,48206
-(defcustom proof-shell-retract-files-regexp 1275,49282
-(defcustom proof-shell-compute-new-files-list 1288,49770
-(defcustom pg-special-char-regexp 1303,50337
-(defcustom proof-shell-set-elisp-variable-regexp 1308,50481
-(defcustom proof-shell-match-pgip-cmd 1346,52155
-(defcustom proof-shell-issue-pgip-cmd 1360,52645
-(defcustom proof-use-pgip-askprefs 1365,52818
-(defcustom proof-shell-query-dependencies-cmd 1373,53165
-(defcustom proof-shell-theorem-dependency-list-regexp 1380,53425
-(defcustom proof-shell-theorem-dependency-list-split 1396,54093
-(defcustom proof-shell-show-dependency-cmd 1405,54524
-(defcustom proof-shell-trace-output-regexp 1427,55430
-(defcustom proof-shell-thms-output-regexp 1445,56032
-(defcustom proof-shell-interactive-prompt-regexp 1453,56366
-(defcustom proof-tokens-activate-command 1472,57019
-(defcustom proof-tokens-deactivate-command 1479,57259
-(defcustom proof-tokens-extra-modes 1486,57504
-(defcustom proof-shell-unicode 1501,58009
-(defcustom proof-shell-filename-escapes 1510,58399
-(defcustom proof-shell-process-connection-type 1527,59079
-(defcustom proof-shell-strip-crs-from-input 1533,59306
-(defcustom proof-shell-strip-crs-from-output 1545,59789
-(defcustom proof-shell-extend-queue-hook 1553,60157
-(defcustom proof-shell-insert-hook 1563,60587
-(defcustom proof-script-preprocess 1606,62685
-(defcustom proof-shell-handle-delayed-output-hook1612,62836
-(defcustom proof-shell-handle-error-or-interrupt-hook1618,63051
-(defcustom proof-shell-pre-interrupt-hook1636,63797
-(defcustom proof-shell-handle-output-system-specific 1644,64068
-(defcustom proof-state-change-hook 1667,65041
-(defcustom proof-shell-syntax-table-entries 1677,65434
-(defgroup proof-goals 1695,65805
-(defcustom pg-subterm-first-special-char 1700,65926
-(defcustom pg-subterm-anns-use-stack 1708,66238
-(defcustom pg-goals-change-goal 1717,66537
-(defcustom pbp-goal-command 1722,66653
-(defcustom pbp-hyp-command 1727,66817
-(defcustom pg-subterm-help-cmd 1732,66987
-(defcustom pg-goals-error-regexp 1739,67231
-(defcustom proof-shell-result-start 1744,67399
-(defcustom proof-shell-result-end 1750,67641
-(defcustom pg-subterm-start-char 1756,67854
-(defcustom pg-subterm-sep-char 1767,68328
-(defcustom pg-subterm-end-char 1773,68507
-(defcustom pg-topterm-regexp 1779,68664
-(defcustom proof-goals-font-lock-keywords 1794,69264
-(defcustom proof-response-font-lock-keywords 1802,69623
-(defcustom proof-shell-font-lock-keywords 1810,69985
-(defcustom pg-before-fontify-output-hook 1821,70499
-(defcustom pg-after-fontify-output-hook 1829,70860
+generic/proof-config.el,7902
+(defgroup prover-config 80,2634
+(defcustom proof-guess-command-line 98,3484
+(defcustom proof-assistant-home-page 113,3979
+(defcustom proof-context-command 119,4149
+(defcustom proof-info-command 124,4283
+(defcustom proof-showproof-command 131,4554
+(defcustom proof-goal-command 136,4690
+(defcustom proof-save-command 144,4987
+(defcustom proof-find-theorems-command 152,5296
+(defcustom proof-query-identifier-command 159,5604
+(defcustom proof-assistant-true-value 173,6293
+(defcustom proof-assistant-false-value 179,6483
+(defcustom proof-assistant-format-int-fn 185,6677
+(defcustom proof-assistant-format-float-fn 192,6926
+(defcustom proof-assistant-format-string-fn 199,7181
+(defcustom proof-assistant-setting-format 206,7448
+(defcustom proof-tree-configured 216,7931
+(defgroup proof-script 234,8397
+(defcustom proof-terminal-string 239,8527
+(defcustom proof-electric-terminator-noterminator 249,8915
+(defcustom proof-script-sexp-commands 254,9087
+(defcustom proof-script-command-end-regexp 265,9546
+(defcustom proof-script-command-start-regexp 283,10367
+(defcustom proof-script-integral-proofs 294,10830
+(defcustom proof-script-fly-past-comments 309,11486
+(defcustom proof-script-parse-function 314,11657
+(defcustom proof-script-comment-start 332,12302
+(defcustom proof-script-comment-start-regexp 343,12739
+(defcustom proof-script-comment-end 351,13058
+(defcustom proof-script-comment-end-regexp 363,13480
+(defcustom proof-string-start-regexp 371,13793
+(defcustom proof-string-end-regexp 376,13958
+(defcustom proof-case-fold-search 381,14119
+(defcustom proof-save-command-regexp 390,14531
+(defcustom proof-save-with-hole-regexp 395,14641
+(defcustom proof-save-with-hole-result 406,15016
+(defcustom proof-goal-command-regexp 416,15460
+(defcustom proof-goal-with-hole-regexp 424,15747
+(defcustom proof-goal-with-hole-result 436,16190
+(defcustom proof-non-undoables-regexp 445,16568
+(defcustom proof-nested-undo-regexp 456,17031
+(defcustom proof-ignore-for-undo-count 472,17751
+(defcustom proof-script-imenu-generic-expression 480,18062
+(defcustom proof-goal-command-p 488,18401
+(defcustom proof-really-save-command-p 499,18892
+(defcustom proof-completed-proof-behaviour 508,19199
+(defcustom proof-count-undos-fn 536,20548
+(defcustom proof-find-and-forget-fn 548,21099
+(defcustom proof-forget-id-command 565,21808
+(defcustom pg-topterm-goalhyplit-fn 575,22166
+(defcustom proof-kill-goal-command 587,22709
+(defcustom proof-undo-n-times-cmd 601,23213
+(defcustom proof-nested-goals-history-p 615,23750
+(defcustom proof-arbitrary-undo-positions 624,24087
+(defcustom proof-state-preserving-p 638,24668
+(defcustom proof-activate-scripting-hook 648,25140
+(defcustom proof-deactivate-scripting-hook 667,25921
+(defcustom proof-no-fully-processed-buffer 676,26251
+(defcustom proof-script-evaluate-elisp-comment-regexp 687,26749
+(defcustom proof-indent 705,27335
+(defcustom proof-indent-hang 710,27442
+(defcustom proof-indent-enclose-offset 715,27568
+(defcustom proof-indent-open-offset 720,27710
+(defcustom proof-indent-close-offset 725,27847
+(defcustom proof-indent-any-regexp 730,27985
+(defcustom proof-indent-inner-regexp 735,28145
+(defcustom proof-indent-enclose-regexp 740,28299
+(defcustom proof-indent-open-regexp 745,28453
+(defcustom proof-indent-close-regexp 750,28605
+(defcustom proof-script-font-lock-keywords 756,28759
+(defcustom proof-script-syntax-table-entries 764,29111
+(defcustom proof-script-span-context-menu-extensions 782,29507
+(defgroup proof-shell 808,30267
+(defcustom proof-prog-name 818,30437
+(defcustom proof-shell-auto-terminate-commands 830,30904
+(defcustom proof-shell-pre-sync-init-cmd 839,31309
+(defcustom proof-shell-init-cmd 853,31867
+(defcustom proof-shell-init-hook 865,32413
+(defcustom proof-shell-restart-cmd 870,32552
+(defcustom proof-shell-quit-cmd 875,32707
+(defcustom proof-shell-cd-cmd 880,32874
+(defcustom proof-shell-start-silent-cmd 897,33545
+(defcustom proof-shell-stop-silent-cmd 906,33921
+(defcustom proof-shell-silent-threshold 915,34256
+(defcustom  proof-shell-inform-file-processed-cmd 923,34590
+(defcustom  proof-shell-inform-file-retracted-cmd 944,35518
+(defcustom proof-auto-multiple-files 972,36790
+(defcustom proof-cannot-reopen-processed-files 987,37511
+(defcustom proof-shell-annotated-prompt-regexp 1007,38302
+(defcustom proof-shell-error-regexp 1022,38867
+(defcustom proof-shell-truncate-before-error 1042,39677
+(defcustom pg-next-error-regexp 1056,40216
+(defcustom pg-next-error-filename-regexp 1071,40825
+(defcustom pg-next-error-extract-filename 1095,41858
+(defcustom proof-shell-interrupt-regexp 1102,42101
+(defcustom proof-shell-proof-completed-regexp 1116,42704
+(defcustom proof-shell-clear-response-regexp 1129,43220
+(defcustom proof-shell-clear-goals-regexp 1141,43680
+(defcustom proof-shell-start-goals-regexp 1153,44134
+(defcustom proof-shell-end-goals-regexp 1166,44709
+(defcustom proof-shell-eager-annotation-start 1180,45299
+(defcustom proof-shell-eager-annotation-start-length 1203,46318
+(defcustom proof-shell-eager-annotation-end 1214,46744
+(defcustom proof-shell-strip-output-markup 1230,47419
+(defcustom proof-shell-assumption-regexp 1239,47804
+(defcustom proof-shell-process-file 1249,48208
+(defcustom proof-shell-retract-files-regexp 1275,49284
+(defcustom proof-shell-compute-new-files-list 1288,49772
+(defcustom pg-special-char-regexp 1303,50339
+(defcustom proof-shell-set-elisp-variable-regexp 1308,50483
+(defcustom proof-shell-match-pgip-cmd 1346,52157
+(defcustom proof-shell-issue-pgip-cmd 1360,52647
+(defcustom proof-use-pgip-askprefs 1365,52820
+(defcustom proof-shell-query-dependencies-cmd 1373,53167
+(defcustom proof-shell-theorem-dependency-list-regexp 1380,53427
+(defcustom proof-shell-theorem-dependency-list-split 1396,54095
+(defcustom proof-shell-show-dependency-cmd 1405,54526
+(defcustom proof-shell-trace-output-regexp 1427,55432
+(defcustom proof-shell-thms-output-regexp 1445,56034
+(defcustom proof-shell-interactive-prompt-regexp 1453,56368
+(defcustom proof-tokens-activate-command 1472,57021
+(defcustom proof-tokens-deactivate-command 1479,57261
+(defcustom proof-tokens-extra-modes 1486,57506
+(defcustom proof-shell-unicode 1501,58011
+(defcustom proof-shell-filename-escapes 1510,58401
+(defcustom proof-shell-process-connection-type 1527,59081
+(defcustom proof-shell-strip-crs-from-input 1533,59308
+(defcustom proof-shell-strip-crs-from-output 1545,59791
+(defcustom proof-shell-extend-queue-hook 1553,60159
+(defcustom proof-shell-insert-hook 1563,60589
+(defcustom proof-script-preprocess 1606,62687
+(defcustom proof-shell-handle-delayed-output-hook1612,62838
+(defcustom proof-shell-handle-error-or-interrupt-hook1618,63053
+(defcustom proof-shell-signal-interrupt-hook 1636,63799
+(defcustom proof-shell-pre-interrupt-hook1647,64268
+(defcustom proof-shell-handle-output-system-specific 1655,64539
+(defcustom proof-state-change-hook 1678,65512
+(defcustom proof-shell-syntax-table-entries 1688,65905
+(defgroup proof-goals 1706,66276
+(defcustom pg-subterm-first-special-char 1711,66397
+(defcustom pg-subterm-anns-use-stack 1719,66709
+(defcustom pg-goals-change-goal 1728,67008
+(defcustom pbp-goal-command 1733,67124
+(defcustom pbp-hyp-command 1738,67288
+(defcustom pg-subterm-help-cmd 1743,67458
+(defcustom pg-goals-error-regexp 1750,67702
+(defcustom proof-shell-result-start 1755,67870
+(defcustom proof-shell-result-end 1761,68112
+(defcustom pg-subterm-start-char 1767,68325
+(defcustom pg-subterm-sep-char 1778,68799
+(defcustom pg-subterm-end-char 1784,68978
+(defcustom pg-topterm-regexp 1790,69135
+(defcustom proof-goals-font-lock-keywords 1805,69735
+(defcustom proof-response-font-lock-keywords 1813,70094
+(defcustom proof-shell-font-lock-keywords 1821,70456
+(defcustom pg-before-fontify-output-hook 1832,70970
+(defcustom pg-after-fontify-output-hook 1840,71331
 
 generic/proof-depends.el,917
 (defvar proof-thm-names-of-files 25,639
@@ -1836,87 +1890,88 @@ generic/proof-script.el,5814
 (defun proof-script-after-change-function 2719,104191
 (defun proof-script-set-after-change-functions 2731,104698
 
-generic/proof-shell.el,3819
-(defvar proof-marker 35,773
-(defvar proof-action-list 38,869
-(defsubst proof-shell-invoke-callback 80,2582
-(defvar proof-shell-last-goals-output 94,3074
-(defvar proof-shell-last-response-output 97,3154
-(defvar proof-shell-delayed-output-start 100,3241
-(defvar proof-shell-delayed-output-end 104,3423
-(defvar proof-shell-delayed-output-flags 108,3603
-(defvar proof-shell-interrupt-pending 111,3728
-(defvar proof-shell-exit-in-progress 116,3952
-(defcustom proof-shell-active-scripting-indicator128,4297
-(defun proof-shell-ready-prover 180,5881
-(defsubst proof-shell-live-buffer 194,6420
-(defun proof-shell-available-p 201,6640
-(defun proof-grab-lock 207,6862
-(defun proof-release-lock 217,7291
-(defcustom proof-shell-fiddle-frames 227,7465
-(defun proof-shell-set-text-representation 232,7623
-(defun proof-shell-make-associated-buffers 239,7950
-(defun proof-shell-start 255,8616
-(defvar proof-shell-kill-function-hooks 417,14141
-(defun proof-shell-kill-function 420,14239
-(defun proof-shell-clear-state 484,16483
-(defun proof-shell-exit 500,16958
-(defun proof-shell-bail-out 524,17892
-(defun proof-shell-restart 534,18414
-(defvar proof-shell-urgent-message-marker 575,19786
-(defvar proof-shell-urgent-message-scanner 578,19907
-(defun proof-shell-handle-error-output 582,20092
-(defun proof-shell-handle-error-or-interrupt 608,20954
-(defun proof-shell-error-or-interrupt-action 651,22703
-(defun proof-goals-pos 678,23800
-(defun proof-pbp-focus-on-first-goal 683,24011
-(defsubst proof-shell-string-match-safe 695,24427
-(defun proof-shell-handle-immediate-output 699,24588
-(defun proof-interrupt-process 766,27195
-(defun proof-shell-insert 800,28428
-(defun proof-shell-action-list-item 857,30410
-(defun proof-shell-set-silent 862,30652
-(defun proof-shell-start-silent-item 868,30871
-(defun proof-shell-clear-silent 874,31060
-(defun proof-shell-stop-silent-item 880,31282
-(defsubst proof-shell-should-be-silent 886,31471
-(defsubst proof-shell-insert-action-item 898,32044
-(defsubst proof-shell-slurp-comments 902,32219
-(defun proof-add-to-queue 913,32624
-(defun proof-start-queue 965,34576
-(defun proof-extend-queue 977,34971
-(defun proof-shell-exec-loop 996,35590
-(defun proof-shell-insert-loopback-cmd 1078,38530
-(defun proof-shell-process-urgent-message 1103,39694
-(defun proof-shell-process-urgent-message-default 1159,41719
-(defun proof-shell-process-urgent-message-trace 1175,42303
-(defun proof-shell-process-urgent-message-retract 1187,42826
-(defun proof-shell-process-urgent-message-elisp 1213,43956
-(defun proof-shell-process-urgent-message-thmdeps 1228,44451
-(defun proof-shell-process-interactive-prompt-regexp 1238,44795
-(defun proof-shell-strip-eager-annotations 1250,45151
-(defun proof-shell-filter 1266,45651
-(defun proof-shell-filter-first-command 1366,49023
-(defun proof-shell-process-urgent-messages 1381,49566
-(defun proof-shell-filter-manage-output 1431,51132
-(defsubst proof-shell-display-output-as-response 1467,52555
-(defun proof-shell-handle-delayed-output 1473,52850
-(defvar pg-last-tracing-output-time 1577,56422
-(defvar pg-last-trace-output-count 1580,56535
-(defconst pg-slow-mode-trigger-count 1583,56620
-(defconst pg-slow-mode-duration 1586,56725
-(defconst pg-fast-tracing-mode-threshold 1589,56807
-(defun pg-tracing-tight-loop 1592,56936
-(defun pg-finish-tracing-display 1616,57968
-(defun proof-shell-wait 1634,58349
-(defun proof-done-invisible 1664,59560
-(defun proof-shell-invisible-command 1670,59730
-(defun proof-shell-invisible-cmd-get-result 1717,61322
-(defun proof-shell-invisible-command-invisible-result 1729,61758
-(defun pg-insert-last-output-as-comment 1749,62259
-(define-derived-mode proof-shell-mode 1768,62731
-(defconst proof-shell-important-settings1805,63758
-(defun proof-shell-config-done 1811,63873
+generic/proof-shell.el,3871
+(defvar proof-marker 35,775
+(defvar proof-action-list 38,871
+(defsubst proof-shell-invoke-callback 80,2584
+(defvar proof-second-action-list-active 86,2794
+(defvar proof-shell-last-goals-output 108,3747
+(defvar proof-shell-last-response-output 111,3827
+(defvar proof-shell-delayed-output-start 114,3914
+(defvar proof-shell-delayed-output-end 118,4096
+(defvar proof-shell-delayed-output-flags 122,4276
+(defvar proof-shell-interrupt-pending 125,4401
+(defvar proof-shell-exit-in-progress 130,4625
+(defcustom proof-shell-active-scripting-indicator142,4970
+(defun proof-shell-ready-prover 194,6554
+(defsubst proof-shell-live-buffer 208,7093
+(defun proof-shell-available-p 215,7313
+(defun proof-grab-lock 221,7535
+(defun proof-release-lock 231,7964
+(defcustom proof-shell-fiddle-frames 241,8138
+(defun proof-shell-set-text-representation 246,8296
+(defun proof-shell-make-associated-buffers 253,8623
+(defun proof-shell-start 269,9289
+(defvar proof-shell-kill-function-hooks 431,14814
+(defun proof-shell-kill-function 434,14912
+(defun proof-shell-clear-state 499,17211
+(defun proof-shell-exit 515,17686
+(defun proof-shell-bail-out 539,18620
+(defun proof-shell-restart 549,19142
+(defvar proof-shell-urgent-message-marker 590,20514
+(defvar proof-shell-urgent-message-scanner 593,20635
+(defun proof-shell-handle-error-output 597,20820
+(defun proof-shell-handle-error-or-interrupt 623,21682
+(defun proof-shell-error-or-interrupt-action 666,23431
+(defun proof-goals-pos 693,24528
+(defun proof-pbp-focus-on-first-goal 698,24739
+(defsubst proof-shell-string-match-safe 710,25155
+(defun proof-shell-handle-immediate-output 714,25316
+(defun proof-interrupt-process 781,27923
+(defun proof-shell-insert 816,29205
+(defun proof-shell-action-list-item 873,31187
+(defun proof-shell-set-silent 878,31429
+(defun proof-shell-start-silent-item 884,31648
+(defun proof-shell-clear-silent 890,31837
+(defun proof-shell-stop-silent-item 896,32059
+(defsubst proof-shell-should-be-silent 902,32248
+(defsubst proof-shell-insert-action-item 914,32821
+(defsubst proof-shell-slurp-comments 918,32996
+(defun proof-add-to-queue 929,33401
+(defun proof-start-queue 985,35507
+(defun proof-extend-queue 997,35902
+(defun proof-shell-exec-loop 1016,36521
+(defun proof-shell-insert-loopback-cmd 1100,39547
+(defun proof-shell-process-urgent-message 1125,40711
+(defun proof-shell-process-urgent-message-default 1181,42736
+(defun proof-shell-process-urgent-message-trace 1197,43320
+(defun proof-shell-process-urgent-message-retract 1209,43843
+(defun proof-shell-process-urgent-message-elisp 1235,44973
+(defun proof-shell-process-urgent-message-thmdeps 1250,45468
+(defun proof-shell-process-interactive-prompt-regexp 1260,45812
+(defun proof-shell-strip-eager-annotations 1272,46168
+(defun proof-shell-filter 1288,46668
+(defun proof-shell-filter-first-command 1388,50040
+(defun proof-shell-process-urgent-messages 1403,50583
+(defun proof-shell-filter-manage-output 1453,52149
+(defsubst proof-shell-display-output-as-response 1489,53572
+(defun proof-shell-handle-delayed-output 1495,53867
+(defvar pg-last-tracing-output-time 1599,57439
+(defvar pg-last-trace-output-count 1602,57552
+(defconst pg-slow-mode-trigger-count 1605,57637
+(defconst pg-slow-mode-duration 1608,57742
+(defconst pg-fast-tracing-mode-threshold 1611,57824
+(defun pg-tracing-tight-loop 1614,57953
+(defun pg-finish-tracing-display 1638,58985
+(defun proof-shell-wait 1658,59481
+(defun proof-done-invisible 1688,60692
+(defun proof-shell-invisible-command 1694,60862
+(defun proof-shell-invisible-cmd-get-result 1741,62454
+(defun proof-shell-invisible-command-invisible-result 1753,62890
+(defun pg-insert-last-output-as-comment 1773,63391
+(define-derived-mode proof-shell-mode 1792,63863
+(defconst proof-shell-important-settings1829,64890
+(defun proof-shell-config-done 1835,65005
 
 generic/proof-site.el,708
 (defconst proof-assistant-table-default36,1211
@@ -2139,30 +2194,30 @@ generic/proof-useropts.el,1785
 (defcustom proof-multiple-frames-enable 161,5911
 (defcustom proof-layout-windows-on-visit-file 171,6306
 (defcustom proof-three-window-mode-policy 180,6690
-(defcustom proof-delete-empty-windows 199,7414
-(defcustom proof-shrink-windows-tofit 210,7945
-(defcustom proof-auto-raise-buffers 217,8217
-(defcustom proof-colour-locked 224,8452
-(defcustom proof-sticky-errors 232,8702
-(defcustom proof-query-file-save-when-activating-scripting239,8919
-(defcustom proof-prog-name-ask255,9639
-(defcustom proof-prog-name-guess261,9799
-(defcustom proof-tidy-response269,10064
-(defcustom proof-keep-response-history283,10527
-(defcustom pg-input-ring-size 293,10915
-(defcustom proof-general-debug 298,11067
-(defcustom proof-use-parser-cache 307,11438
-(defcustom proof-follow-mode 314,11692
-(defcustom proof-auto-action-when-deactivating-scripting 338,12869
-(defcustom proof-rsh-command 366,14051
-(defcustom proof-disappearing-proofs 382,14609
-(defcustom proof-full-annotation 387,14770
-(defcustom proof-output-tooltips 397,15233
-(defcustom proof-minibuffer-messages 408,15740
-(defcustom proof-autosend-enable 416,16049
-(defcustom proof-autosend-delay 422,16229
-(defcustom proof-autosend-all 428,16387
-(defcustom proof-fast-process-buffer 433,16556
+(defcustom proof-delete-empty-windows 199,7405
+(defcustom proof-shrink-windows-tofit 210,7936
+(defcustom proof-auto-raise-buffers 217,8208
+(defcustom proof-colour-locked 224,8443
+(defcustom proof-sticky-errors 232,8693
+(defcustom proof-query-file-save-when-activating-scripting239,8910
+(defcustom proof-prog-name-ask255,9630
+(defcustom proof-prog-name-guess261,9790
+(defcustom proof-tidy-response269,10055
+(defcustom proof-keep-response-history283,10518
+(defcustom pg-input-ring-size 293,10906
+(defcustom proof-general-debug 298,11058
+(defcustom proof-use-parser-cache 307,11429
+(defcustom proof-follow-mode 314,11683
+(defcustom proof-auto-action-when-deactivating-scripting 338,12860
+(defcustom proof-rsh-command 366,14042
+(defcustom proof-disappearing-proofs 382,14600
+(defcustom proof-full-annotation 387,14761
+(defcustom proof-output-tooltips 397,15224
+(defcustom proof-minibuffer-messages 408,15731
+(defcustom proof-autosend-enable 416,16040
+(defcustom proof-autosend-delay 422,16220
+(defcustom proof-autosend-all 428,16378
+(defcustom proof-fast-process-buffer 433,16547
 
 generic/proof-utils.el,1645
 (defmacro proof-with-current-buffer-if-exists 61,1737