Updated.

1 files changed, 2585 insertions, 2528 deletions

diff --git a/TAGS b/TAGS
index 8a45d493..bcd5e57c 100644
--- a/TAGS
+++ b/TAGS
@@ -38,231 +38,7 @@ coq/coq-db.el,678
 (defconst coq-solve-tactics-face 266,9550
 (defconst coq-cheat-face 270,9714
 
-coq/coq.el,9426
-(defcustom coq-prog-name61,1977
-(defcustom coq-translate-to-v8 80,2829
-(defun coq-build-prog-args 85,2944
-(defcustom coq-compiler95,3267
-(defcustom coq-dependency-analyzer101,3404
-(defcustom coq-use-makefile 107,3544
-(defcustom coq-default-undo-limit 113,3716
-(defconst coq-shell-init-cmd118,3844
-(defcustom coq-prog-env 127,4171
-(defconst coq-shell-restart-cmd 135,4420
-(defvar coq-shell-prompt-pattern137,4474
-(defvar coq-shell-cd 145,4777
-(defvar coq-shell-proof-completed-regexp 149,4937
-(defvar coq-goal-regexp152,5122
-(defun get-coq-library-directory 157,5218
-(defconst coq-library-directory 163,5400
-(defcustom coq-tags 166,5527
-(defconst coq-interrupt-regexp 171,5675
-(defcustom coq-www-home-page 174,5768
-(defcustom coq-end-goals-regexp-hide-subgoals 179,5875
-(defcustom coq-end-goals-regexp-show-subgoals 185,6112
-(defgroup coq-proof-tree 197,6413
-(defcustom coq-proof-tree-ignored-commands-regexp202,6553
-(defcustom coq-navigation-command-regexp208,6730
-(defcustom coq-proof-tree-cheating-regexp214,6902
-(defcustom coq-proof-tree-current-goal-regexp220,7042
-(defcustom coq-proof-tree-update-goal-regexp227,7296
-(defcustom coq-proof-tree-additional-subgoal-ID-regexp234,7530
-(defcustom coq-proof-tree-existential-regexp 240,7728
-(defcustom coq-proof-tree-instantiated-existential-regexp245,7882
-(defcustom coq-proof-tree-existentials-state-start-regexp251,8102
-(defcustom coq-proof-tree-existentials-state-end-regexp 257,8292
-(defcustom coq-proof-tree-proof-completed-regexp262,8461
-(defvar coq-outline-regexp274,8732
-(defvar coq-outline-heading-end-regexp 281,8945
-(defvar coq-shell-outline-regexp 283,8999
-(defvar coq-shell-outline-heading-end-regexp 284,9049
-(defconst coq-state-preserving-tactics-regexp287,9113
-(defconst coq-state-changing-commands-regexp289,9215
-(defconst coq-state-preserving-commands-regexp291,9324
-(defconst coq-commands-regexp293,9437
-(defvar coq-retractable-instruct-regexp295,9516
-(defvar coq-non-retractable-instruct-regexp297,9608
-(defcustom coq-use-smie 329,10304
-(defcustom coq-indent-box-style 335,10501
-(defconst coq-smie-grammar354,10795
-(defun coq-smie-search-token-forward 418,13720
-(defun coq-smie-search-token-backward 431,14227
-(defconst coq-smie-proof-end-tokens459,15562
-(defun coq-smie-forward-token 463,15692
-(defun coq-smie-backward-token 513,17645
-(defun coq-smie-rules 600,21089
-(defconst coq-script-command-end-regexp 682,24880
-(defun coq-script-parse-function 691,25309
-(defun coq-set-undo-limit 698,25535
-(defun build-list-id-from-string 702,25665
-(defun coq-last-prompt-info 711,26140
-(defun coq-last-prompt-info-safe 729,27034
-(defvar coq-last-but-one-statenum 737,27387
-(defvar coq-last-but-one-proofnum 744,27684
-(defvar coq-last-but-one-proofstack 747,27782
-(defsubst coq-get-span-statenum 750,27892
-(defsubst coq-get-span-proofnum 754,28007
-(defsubst coq-get-span-proofstack 758,28122
-(defsubst coq-set-span-statenum 762,28266
-(defsubst coq-get-span-goalcmd 766,28397
-(defsubst coq-set-span-goalcmd 770,28511
-(defsubst coq-set-span-proofnum 774,28641
-(defsubst coq-set-span-proofstack 778,28772
-(defsubst proof-last-locked-span 782,28932
-(defun proof-clone-buffer 786,29066
-(defun proof-store-buffer-win 800,29603
-(defun proof-store-response-win 811,30096
-(defun proof-store-goals-win 815,30223
-(defun coq-set-state-infos 827,30755
-(defun count-not-intersection 865,32845
-(defun coq-find-and-forget 895,34097
-(defvar coq-current-goal 922,35402
-(defun coq-goal-hyp 925,35467
-(defun coq-state-preserving-p 938,35941
-(defun coq-hide-additional-subgoals-switch 948,36235
-(defconst notation-print-kinds-table961,36600
-(defun coq-PrintScope 965,36767
-(defun coq-guess-or-ask-for-string 983,37316
-(defun coq-ask-do 997,37856
-(defsubst coq-put-into-brackets 1006,38241
-(defsubst coq-put-into-quotes 1009,38302
-(defun coq-SearchIsos 1012,38361
-(defun coq-SearchConstant 1020,38600
-(defun coq-Searchregexp 1024,38693
-(defun coq-SearchRewrite 1030,38834
-(defun coq-SearchAbout 1034,38931
-(defun coq-Print 1040,39074
-(defun coq-About 1045,39198
-(defun coq-LocateConstant 1050,39317
-(defun coq-LocateLibrary 1055,39420
-(defun coq-LocateNotation 1060,39537
-(defun coq-Pwd 1068,39768
-(defun coq-Inspect 1073,39892
-(defun coq-PrintSection(1077,39992
-(defun coq-Print-implicit 1081,40085
-(defun coq-Check 1086,40236
-(defun coq-Show 1091,40344
-(defun coq-Compile 1105,40787
-(defun coq-guess-command-line 1117,41105
-(defpacustom use-editing-holes 1154,42662
-(defun coq-mode-config 1163,42965
-(defun coq-shell-mode-config 1268,46776
-(defun coq-goals-mode-config 1341,49970
-(defun coq-response-config 1348,50214
-(defpacustom hide-additional-subgoals 1371,50931
-(defpacustom print-fully-explicit 1381,51241
-(defpacustom print-implicit 1386,51389
-(defpacustom print-coercions 1391,51555
-(defpacustom print-match-wildcards 1396,51699
-(defpacustom print-elim-types 1401,51879
-(defpacustom printing-depth 1406,52045
-(defpacustom undo-depth 1411,52206
-(defpacustom time-commands 1416,52372
-(defgroup coq-auto-compile 1427,52622
-(defpacustom compile-before-require 1432,52773
-(defcustom coq-compile-command 1444,53265
-(defconst coq-compile-substitution-list1474,54548
-(defcustom coq-load-path 1494,55469
-(defcustom coq-compile-auto-save 1545,57990
-(defcustom coq-lock-ancestors 1570,59048
-(defpacustom confirm-external-compilation 1579,59369
-(defcustom coq-load-path-include-current 1588,59676
-(defcustom coq-compile-ignored-directories 1597,59994
-(defcustom coq-compile-ignore-library-directory 1610,60627
-(defcustom coq-coqdep-error-regexp1622,61115
-(defconst coq-require-command-regexp1638,61833
-(defconst coq-require-id-regexp1645,62190
-(defvar coq-compile-history 1653,62624
-(defvar coq-compile-response-buffer 1656,62708
-(defvar coq-debug-auto-compilation 1660,62843
-(defun time-less-or-equal 1666,62951
-(defun coq-max-dep-mod-time 1674,63289
-(defun coq-prog-args 1697,64093
-(defun coq-lock-ancestor 1706,64352
-(defun coq-unlock-ancestor 1722,65127
-(defun coq-unlock-all-ancestors-of-span 1729,65422
-(defun coq-compile-ignore-file 1736,65718
-(defun coq-library-src-of-obj-file 1760,66605
-(defun coq-option-of-load-path-entry 1765,66837
-(defun coq-include-options 1781,67428
-(defun coq-init-compile-response-buffer 1801,68252
-(defun coq-display-compile-response-buffer 1824,69324
-(defun coq-get-library-dependencies 1838,69958
-(defun coq-compile-library 1885,72183
-(defun coq-compile-library-if-necessary 1912,73394
-(defun coq-make-lib-up-to-date 1958,75266
-(defun coq-auto-compile-externally 2014,77729
-(defun coq-map-module-id-to-obj-file 2057,79875
-(defun coq-check-module 2110,82477
-(defvar coq-process-require-current-buffer2138,83919
-(defun coq-compile-save-buffer-filter 2144,84184
-(defun coq-compile-save-some-buffers 2154,84598
-(defun coq-preprocess-require-commands 2176,85500
-(defun coq-switch-buffer-kill-proof-shell 2209,87069
-(defun coq-proof-tree-get-proof-info 2229,87702
-(defun coq-extract-instantiated-existentials 2239,88090
-(defun coq-show-sequent-command 2248,88482
-(defun coq-proof-tree-get-new-subgoals 2252,88636
-(defun coq-find-begin-of-unfinished-proof 2296,90761
-(defun coq-preprocessing 2321,91775
-(defun coq-fake-constant-markup 2335,92230
-(defun coq-create-span-menu 2351,92835
-(defconst module-kinds-table2369,93348
-(defconst modtype-kinds-table2373,93497
-(defun coq-insert-section-or-module 2377,93626
-(defconst reqkinds-kinds-table2398,94476
-(defun coq-insert-requires 2402,94620
-(defun coq-end-Section 2415,95099
-(defun coq-insert-intros 2433,95677
-(defun coq-insert-infoH-hook 2445,96208
-(defun coq-insert-as 2450,96416
-(defun coq-insert-match 2467,97109
-(defun coq-insert-solve-tactic 2496,98278
-(defun coq-insert-tactic 2502,98529
-(defun coq-insert-tactical 2508,98731
-(defun coq-insert-command 2514,98962
-(defun coq-insert-term 2519,99127
-(define-key coq-keymap 2524,99288
-(define-key coq-keymap 2525,99346
-(define-key coq-keymap 2526,99403
-(define-key coq-keymap 2527,99472
-(define-key coq-keymap 2528,99528
-(define-key coq-keymap 2529,99577
-(define-key coq-keymap 2530,99635
-(define-key coq-keymap 2531,99685
-(define-key coq-keymap 2532,99740
-(define-key coq-keymap 2534,99793
-(define-key coq-keymap 2536,99867
-(define-key coq-keymap 2537,99924
-(define-key coq-keymap 2540,99989
-(define-key coq-keymap 2541,100049
-(define-key coq-keymap 2543,100105
-(define-key coq-keymap 2544,100155
-(define-key coq-keymap 2545,100205
-(define-key coq-keymap 2546,100261
-(define-key coq-keymap 2547,100311
-(define-key coq-keymap 2548,100355
-(define-key coq-keymap 2549,100414
-(define-key coq-goals-mode-map 2552,100475
-(define-key coq-goals-mode-map 2553,100557
-(define-key coq-goals-mode-map 2554,100639
-(define-key coq-goals-mode-map 2555,100726
-(define-key coq-goals-mode-map 2556,100808
-(defvar last-coq-error-location 2565,101113
-(defun coq-get-last-error-location 2573,101497
-(defun coq-highlight-error 2623,104060
-(defun coq-highlight-error-hook 2651,105141
-(defun coq-first-word-before 2661,105358
-(defun coq-show-first-goal 2672,105690
-(defvar coq-modeline-string2 2688,106355
-(defvar coq-modeline-string1 2689,106389
-(defvar coq-modeline-string0 2690,106423
-(defun coq-build-subgoals-string 2691,106464
-(defun coq-update-minor-mode-alist 2696,106630
-(defun is-not-split-vertic 2728,108045
-(defun optim-resp-windows 2737,108485
-
-coq/coq-indent.el,2565
+coq/coq-indent.el,2698
 (defconst coq-any-command-regexp20,368
 (defconst coq-indent-inner-regexp23,442
 (defconst coq-comment-start-regexp 33,804
@@ -279,128 +55,131 @@ coq/coq-indent.el,2565
 (defconst coq-indent-kw58,1967
 (defconst coq-indent-pattern-regexp 68,2433
 (defun coq-indent-goal-command-p 72,2536
-(defconst coq-end-command-regexp94,3590
-(defun coq-search-comment-delimiter-forward 103,4095
-(defun coq-search-comment-delimiter-backward 112,4425
-(defun coq-skip-until-one-comment-backward 119,4699
-(defun coq-skip-until-one-comment-forward 134,5406
-(defun coq-looking-at-comment 145,5924
-(defun coq-find-comment-start 149,6065
-(defun coq-find-comment-end 160,6498
-(defun coq-looking-at-syntactic-context 172,6991
-(defconst coq-end-command-or-comment-regexp178,7213
-(defconst coq-end-command-or-comment-start-regexp181,7322
-(defun coq-find-not-in-comment-backward 184,7439
-(defun coq-find-not-in-comment-forward 204,8329
-(defun coq-is-on-ending-context 230,9521
-(defun coq-empty-command-p 239,9734
-(defun coq-script-parse-cmdend-forward 254,10475
-(defun coq-script-parse-cmdend-backward 306,12936
-(defun coq-find-current-start 347,14810
-(defun coq-find-real-start 356,15136
-(defun same-line 362,15354
-(defun coq-command-at-point 365,15441
-(defun coq-commands-at-line 380,16052
-(defun coq-indent-only-spaces-on-line 404,17018
-(defun coq-indent-find-reg 410,17295
-(defun coq-find-no-syntactic-on-line 424,17831
-(defun coq-back-to-indentation-prevline 437,18304
-(defun coq-find-unclosed 483,20371
-(defun coq-find-at-same-level-zero 513,21681
-(defun coq-find-unopened 542,22947
-(defun coq-find-last-unopened 585,24381
-(defun coq-end-offset 596,24778
-(defun coq-add-iter 621,25548
-(defun coq-goal-count 624,25654
-(defun coq-save-count 626,25726
-(defun coq-proof-count 631,25928
-(defun coq-goal-save-diff-maybe-proof 637,26216
-(defun coq-indent-command-offset 647,26510
-(defun coq-indent-expr-offset 713,29691
-(defun coq-indent-comment-offset 832,34573
-(defun coq-indent-offset 864,36025
-(defun coq-indent-calculate 883,36899
-(defun coq-indent-line 886,36987
-(defun coq-indent-line-not-comments 896,37353
-(defun coq-indent-region 906,37742
+(defconst coq-period-end-command93,3548
+(defconst coq-curlybracket-end-command99,3830
+(defconst coq-bullet-end-command104,4059
+(defconst coq-end-command-regexp117,4514
+(defun coq-search-comment-delimiter-forward 133,5239
+(defun coq-search-comment-delimiter-backward 142,5569
+(defun coq-skip-until-one-comment-backward 149,5843
+(defun coq-skip-until-one-comment-forward 164,6550
+(defun coq-looking-at-comment 175,7068
+(defun coq-find-comment-start 179,7209
+(defun coq-find-comment-end 190,7642
+(defun coq-looking-at-syntactic-context 202,8135
+(defconst coq-end-command-or-comment-regexp208,8357
+(defconst coq-end-command-or-comment-start-regexp211,8466
+(defun coq-find-not-in-comment-backward 214,8583
+(defun coq-find-not-in-comment-forward 234,9473
+(defun coq-is-on-ending-context 260,10665
+(defun coq-empty-command-p 269,10878
+(defun coq-script-parse-cmdend-forward 284,11619
+(defun coq-script-parse-cmdend-backward 336,14120
+(defun coq-find-current-start 377,16036
+(defun coq-find-real-start 386,16362
+(defun same-line 392,16580
+(defun coq-command-at-point 395,16667
+(defun coq-commands-at-line 410,17278
+(defun coq-indent-only-spaces-on-line 434,18244
+(defun coq-indent-find-reg 440,18521
+(defun coq-find-no-syntactic-on-line 454,19057
+(defun coq-back-to-indentation-prevline 467,19530
+(defun coq-find-unclosed 513,21597
+(defun coq-find-at-same-level-zero 543,22907
+(defun coq-find-unopened 572,24173
+(defun coq-find-last-unopened 615,25607
+(defun coq-end-offset 626,26004
+(defun coq-add-iter 651,26774
+(defun coq-goal-count 654,26880
+(defun coq-save-count 656,26952
+(defun coq-proof-count 661,27154
+(defun coq-goal-save-diff-maybe-proof 667,27442
+(defun coq-indent-command-offset 677,27736
+(defun coq-indent-expr-offset 743,30917
+(defun coq-indent-comment-offset 862,35799
+(defun coq-indent-offset 894,37251
+(defun coq-indent-calculate 913,38125
+(defun coq-indent-line 916,38213
+(defun coq-indent-line-not-comments 926,38579
+(defun coq-indent-region 936,38968
 
 coq/coq-local-vars.el,229
-(defconst coq-local-vars-doc 23,414
-(defun coq-insert-coq-prog-name 86,2736
-(defun coq-read-directory 99,3287
-(defun coq-ask-load-path 116,4102
-(defun coq-ask-prog-name 134,4935
-(defun coq-ask-insert-coq-prog-name 151,5646
+(defconst coq-local-vars-doc 23,468
+(defun coq-insert-coq-prog-name 86,2790
+(defun coq-read-directory 99,3341
+(defun coq-ask-load-path 116,4156
+(defun coq-ask-prog-name 134,4989
+(defun coq-ask-insert-coq-prog-name 151,5700
 
 coq/coq-syntax.el,2736
-(defcustom coq-user-tactics-db 21,533
-(defcustom coq-user-commands-db 38,1046
-(defcustom coq-user-tacticals-db 54,1565
-(defcustom coq-user-solve-tactics-db 70,2086
-(defcustom coq-user-cheat-tactics-db 86,2605
-(defcustom coq-user-reserved-db 105,3151
-(defvar coq-tactics-db123,3682
-(defvar coq-solve-tactics-db296,12816
-(defvar coq-solve-cheat-tactics-db323,13839
-(defvar coq-tacticals-db335,14014
-(defvar coq-decl-db359,14900
-(defvar coq-defn-db384,16356
-(defvar coq-goal-starters-db449,21078
-(defvar coq-other-commands-db479,22881
-(defvar coq-commands-db614,32866
-(defvar coq-terms-db621,33086
-(defun coq-count-match 683,35701
-(defun coq-module-opening-p 699,36430
-(defun coq-section-command-p 710,36841
-(defun coq-goal-command-str-p 714,36938
-(defun coq-goal-command-p 741,38040
-(defvar coq-keywords-save-strict751,38379
-(defvar coq-keywords-save758,38620
-(defun coq-save-command-p 763,38699
-(defvar coq-keywords-kill-goal774,39027
-(defvar coq-keywords-state-changing-misc-commands778,39117
-(defvar coq-keywords-goal781,39242
-(defvar coq-keywords-decl784,39325
-(defvar coq-keywords-defn787,39399
-(defvar coq-keywords-state-changing-commands791,39474
-(defvar coq-keywords-state-preserving-commands800,39734
-(defvar coq-keywords-commands805,39950
-(defvar coq-solve-tactics810,40098
-(defvar coq-solve-tactics-regexp814,40219
-(defvar coq-solve-cheat-tactics818,40353
-(defvar coq-solve-cheat-tactics-regexp822,40498
-(defvar coq-tacticals826,40656
-(defvar coq-reserved832,40795
-(defvar coq-reserved-regexp 842,41130
-(defvar coq-state-changing-tactics846,41241
-(defvar coq-state-preserving-tactics849,41350
-(defvar coq-tactics853,41464
-(defvar coq-tactics-regexp 856,41553
-(defvar coq-retractable-instruct859,41708
-(defvar coq-non-retractable-instruct862,41818
-(defvar coq-keywords866,41946
-(defun proof-regexp-alt-list-symb 872,42170
-(defvar coq-keywords-regexp 875,42275
-(defvar coq-symbols878,42348
-(defvar coq-error-regexp 900,42589
-(defvar coq-id 903,42817
-(defvar coq-id-shy 904,42842
-(defvar coq-ids 907,42944
-(defun coq-first-abstr-regexp 909,43010
-(defcustom coq-variable-highlight-enable 912,43105
-(defvar coq-font-lock-terms918,43232
-(defconst coq-save-command-regexp-strict940,44315
-(defconst coq-save-command-regexp946,44483
-(defconst coq-save-with-hole-regexp951,44636
-(defconst coq-goal-command-regexp955,44796
-(defconst coq-goal-with-hole-regexp958,44898
-(defconst coq-decl-with-hole-regexp962,45032
-(defconst coq-defn-with-hole-regexp969,45282
-(defconst coq-with-with-hole-regexp979,45572
-(defvar coq-font-lock-keywords-1994,46102
-(defvar coq-font-lock-keywords 1022,47437
-(defun coq-init-syntax-table 1024,47495
-(defconst coq-generic-expression1049,48222
+(defcustom coq-user-tactics-db 21,583
+(defcustom coq-user-commands-db 38,1096
+(defcustom coq-user-tacticals-db 54,1615
+(defcustom coq-user-solve-tactics-db 70,2136
+(defcustom coq-user-cheat-tactics-db 86,2655
+(defcustom coq-user-reserved-db 105,3201
+(defvar coq-tactics-db123,3732
+(defvar coq-solve-tactics-db296,12866
+(defvar coq-solve-cheat-tactics-db323,13889
+(defvar coq-tacticals-db335,14064
+(defvar coq-decl-db359,14950
+(defvar coq-defn-db384,16406
+(defvar coq-goal-starters-db449,21128
+(defvar coq-other-commands-db479,22931
+(defvar coq-commands-db614,32916
+(defvar coq-terms-db621,33136
+(defun coq-count-match 683,35751
+(defun coq-module-opening-p 699,36480
+(defun coq-section-command-p 710,36891
+(defun coq-goal-command-str-p 714,36988
+(defun coq-goal-command-p 741,38090
+(defvar coq-keywords-save-strict751,38429
+(defvar coq-keywords-save758,38670
+(defun coq-save-command-p 763,38749
+(defvar coq-keywords-kill-goal774,39077
+(defvar coq-keywords-state-changing-misc-commands778,39167
+(defvar coq-keywords-goal781,39292
+(defvar coq-keywords-decl784,39375
+(defvar coq-keywords-defn787,39449
+(defvar coq-keywords-state-changing-commands791,39524
+(defvar coq-keywords-state-preserving-commands800,39784
+(defvar coq-keywords-commands805,40000
+(defvar coq-solve-tactics810,40148
+(defvar coq-solve-tactics-regexp814,40269
+(defvar coq-solve-cheat-tactics818,40403
+(defvar coq-solve-cheat-tactics-regexp822,40548
+(defvar coq-tacticals826,40706
+(defvar coq-reserved832,40845
+(defvar coq-reserved-regexp 842,41180
+(defvar coq-state-changing-tactics846,41291
+(defvar coq-state-preserving-tactics849,41400
+(defvar coq-tactics853,41514
+(defvar coq-tactics-regexp 856,41603
+(defvar coq-retractable-instruct859,41758
+(defvar coq-non-retractable-instruct862,41868
+(defvar coq-keywords866,41996
+(defun proof-regexp-alt-list-symb 872,42220
+(defvar coq-keywords-regexp 875,42325
+(defvar coq-symbols878,42398
+(defvar coq-error-regexp 900,42639
+(defvar coq-id 903,42867
+(defvar coq-id-shy 904,42892
+(defvar coq-ids 907,42994
+(defun coq-first-abstr-regexp 909,43060
+(defcustom coq-variable-highlight-enable 912,43155
+(defvar coq-font-lock-terms918,43282
+(defconst coq-save-command-regexp-strict940,44365
+(defconst coq-save-command-regexp946,44533
+(defconst coq-save-with-hole-regexp951,44686
+(defconst coq-goal-command-regexp955,44846
+(defconst coq-goal-with-hole-regexp958,44948
+(defconst coq-decl-with-hole-regexp962,45082
+(defconst coq-defn-with-hole-regexp969,45332
+(defconst coq-with-with-hole-regexp979,45622
+(defvar coq-font-lock-keywords-1994,46152
+(defvar coq-font-lock-keywords 1022,47487
+(defun coq-init-syntax-table 1024,47545
+(defconst coq-generic-expression1049,48272
 
 coq/coq-unicode-tokens.el,454
 (defconst coq-token-format 39,1427
@@ -415,104 +194,288 @@ coq/coq-unicode-tokens.el,454
 (defconst coq-control-region-format-regexp 264,6997
 (defconst coq-control-regions266,7080
 
+coq/coq.el,9435
+(defcustom coq-prog-name61,2023
+(defcustom coq-translate-to-v8 80,2875
+(defun coq-build-prog-args 85,2990
+(defcustom coq-compiler95,3313
+(defcustom coq-dependency-analyzer101,3450
+(defcustom coq-use-makefile 107,3590
+(defcustom coq-default-undo-limit 113,3762
+(defconst coq-shell-init-cmd118,3890
+(defcustom coq-prog-env 127,4217
+(defconst coq-shell-restart-cmd 135,4466
+(defvar coq-shell-prompt-pattern137,4520
+(defvar coq-shell-cd 145,4823
+(defvar coq-shell-proof-completed-regexp 149,4983
+(defvar coq-goal-regexp152,5168
+(defun get-coq-library-directory 157,5264
+(defconst coq-library-directory 163,5446
+(defcustom coq-tags 166,5573
+(defconst coq-interrupt-regexp 171,5721
+(defcustom coq-www-home-page 174,5814
+(defcustom coq-end-goals-regexp-hide-subgoals 179,5921
+(defcustom coq-end-goals-regexp-show-subgoals 185,6158
+(defgroup coq-proof-tree 197,6477
+(defcustom coq-proof-tree-ignored-commands-regexp202,6617
+(defcustom coq-navigation-command-regexp208,6794
+(defcustom coq-proof-tree-cheating-regexp214,6966
+(defcustom coq-proof-tree-current-goal-regexp220,7106
+(defcustom coq-proof-tree-update-goal-regexp227,7360
+(defcustom coq-proof-tree-additional-subgoal-ID-regexp234,7594
+(defcustom coq-proof-tree-existential-regexp 240,7792
+(defcustom coq-proof-tree-instantiated-existential-regexp245,7946
+(defcustom coq-proof-tree-existentials-state-start-regexp251,8166
+(defcustom coq-proof-tree-existentials-state-end-regexp 257,8356
+(defcustom coq-proof-tree-proof-finished-regexp262,8525
+(defvar coq-outline-regexp274,8794
+(defvar coq-outline-heading-end-regexp 281,9007
+(defvar coq-shell-outline-regexp 283,9061
+(defvar coq-shell-outline-heading-end-regexp 284,9111
+(defconst coq-state-preserving-tactics-regexp287,9175
+(defconst coq-state-changing-commands-regexp289,9277
+(defconst coq-state-preserving-commands-regexp291,9386
+(defconst coq-commands-regexp293,9499
+(defvar coq-retractable-instruct-regexp295,9578
+(defvar coq-non-retractable-instruct-regexp297,9670
+(defcustom coq-use-smie 329,10366
+(defcustom coq-indent-box-style 335,10563
+(defconst coq-smie-grammar354,10857
+(defun coq-smie-search-token-forward 420,13906
+(defun coq-smie-search-token-backward 433,14413
+(defconst coq-smie-proof-end-tokens461,15748
+(defun coq-smie-forward-token 465,15878
+(defun coq-smie-backward-token 515,17831
+(defun coq-smie-rules 604,21467
+(defconst coq-script-command-end-regexp 688,25326
+(defun coq-script-parse-function 697,25755
+(defun coq-set-undo-limit 704,25981
+(defun build-list-id-from-string 708,26111
+(defun coq-last-prompt-info 717,26586
+(defun coq-last-prompt-info-safe 735,27480
+(defvar coq-last-but-one-statenum 743,27833
+(defvar coq-last-but-one-proofnum 750,28130
+(defvar coq-last-but-one-proofstack 753,28228
+(defsubst coq-get-span-statenum 756,28338
+(defsubst coq-get-span-proofnum 760,28453
+(defsubst coq-get-span-proofstack 764,28568
+(defsubst coq-set-span-statenum 768,28712
+(defsubst coq-get-span-goalcmd 772,28843
+(defsubst coq-set-span-goalcmd 776,28957
+(defsubst coq-set-span-proofnum 780,29087
+(defsubst coq-set-span-proofstack 784,29218
+(defsubst proof-last-locked-span 788,29378
+(defun proof-clone-buffer 792,29512
+(defun proof-store-buffer-win 806,30049
+(defun proof-store-response-win 817,30542
+(defun proof-store-goals-win 821,30669
+(defun coq-set-state-infos 833,31201
+(defun count-not-intersection 871,33291
+(defun coq-find-and-forget 901,34543
+(defvar coq-current-goal 928,35848
+(defun coq-goal-hyp 931,35913
+(defun coq-state-preserving-p 944,36387
+(defun coq-hide-additional-subgoals-switch 954,36681
+(defconst notation-print-kinds-table967,37046
+(defun coq-PrintScope 971,37213
+(defun coq-guess-or-ask-for-string 989,37762
+(defun coq-ask-do 1003,38302
+(defsubst coq-put-into-brackets 1012,38687
+(defsubst coq-put-into-quotes 1015,38748
+(defun coq-SearchIsos 1018,38807
+(defun coq-SearchConstant 1026,39046
+(defun coq-Searchregexp 1030,39139
+(defun coq-SearchRewrite 1036,39280
+(defun coq-SearchAbout 1040,39377
+(defun coq-Print 1046,39520
+(defun coq-About 1051,39644
+(defun coq-LocateConstant 1056,39763
+(defun coq-LocateLibrary 1061,39866
+(defun coq-LocateNotation 1066,39983
+(defun coq-Pwd 1074,40214
+(defun coq-Inspect 1079,40338
+(defun coq-PrintSection(1083,40438
+(defun coq-Print-implicit 1087,40531
+(defun coq-Check 1092,40682
+(defun coq-Show 1097,40790
+(defun coq-Compile 1111,41233
+(defun coq-guess-command-line 1123,41551
+(defpacustom use-editing-holes 1160,43108
+(defun coq-mode-config 1169,43411
+(defun coq-shell-mode-config 1274,47222
+(defun coq-goals-mode-config 1349,50469
+(defun coq-response-config 1356,50713
+(defpacustom hide-additional-subgoals 1379,51430
+(defpacustom print-fully-explicit 1389,51740
+(defpacustom print-implicit 1394,51888
+(defpacustom print-coercions 1399,52054
+(defpacustom print-match-wildcards 1404,52198
+(defpacustom print-elim-types 1409,52378
+(defpacustom printing-depth 1414,52544
+(defpacustom undo-depth 1419,52705
+(defpacustom time-commands 1424,52871
+(defgroup coq-auto-compile 1435,53121
+(defpacustom compile-before-require 1440,53272
+(defcustom coq-compile-command 1452,53764
+(defconst coq-compile-substitution-list1482,55047
+(defcustom coq-load-path 1502,55968
+(defcustom coq-compile-auto-save 1553,58489
+(defcustom coq-lock-ancestors 1578,59547
+(defpacustom confirm-external-compilation 1587,59868
+(defcustom coq-load-path-include-current 1596,60175
+(defcustom coq-compile-ignored-directories 1605,60493
+(defcustom coq-compile-ignore-library-directory 1618,61126
+(defcustom coq-coqdep-error-regexp1630,61614
+(defconst coq-require-command-regexp1646,62332
+(defconst coq-require-id-regexp1653,62689
+(defvar coq-compile-history 1661,63123
+(defvar coq-compile-response-buffer 1664,63207
+(defvar coq-debug-auto-compilation 1668,63342
+(defun time-less-or-equal 1674,63450
+(defun coq-max-dep-mod-time 1682,63788
+(defun coq-prog-args 1705,64592
+(defun coq-lock-ancestor 1714,64851
+(defun coq-unlock-ancestor 1730,65626
+(defun coq-unlock-all-ancestors-of-span 1737,65921
+(defun coq-compile-ignore-file 1744,66217
+(defun coq-library-src-of-obj-file 1768,67104
+(defun coq-option-of-load-path-entry 1773,67336
+(defun coq-include-options 1789,67927
+(defun coq-init-compile-response-buffer 1809,68751
+(defun coq-display-compile-response-buffer 1832,69823
+(defun coq-get-library-dependencies 1846,70457
+(defun coq-compile-library 1893,72682
+(defun coq-compile-library-if-necessary 1920,73893
+(defun coq-make-lib-up-to-date 1966,75765
+(defun coq-auto-compile-externally 2022,78228
+(defun coq-map-module-id-to-obj-file 2065,80374
+(defun coq-check-module 2118,82976
+(defvar coq-process-require-current-buffer2146,84418
+(defun coq-compile-save-buffer-filter 2152,84683
+(defun coq-compile-save-some-buffers 2162,85097
+(defun coq-preprocess-require-commands 2184,85999
+(defun coq-switch-buffer-kill-proof-shell 2217,87568
+(defun coq-proof-tree-get-proof-info 2237,88201
+(defun coq-extract-instantiated-existentials 2247,88589
+(defun coq-show-sequent-command 2256,88981
+(defun coq-proof-tree-get-new-subgoals 2260,89135
+(defun coq-find-begin-of-unfinished-proof 2304,91260
+(defun coq-preprocessing 2329,92274
+(defun coq-fake-constant-markup 2343,92729
+(defun coq-create-span-menu 2359,93334
+(defconst module-kinds-table2377,93847
+(defconst modtype-kinds-table2381,93996
+(defun coq-insert-section-or-module 2385,94125
+(defconst reqkinds-kinds-table2406,94975
+(defun coq-insert-requires 2410,95119
+(defun coq-end-Section 2423,95598
+(defun coq-insert-intros 2441,96176
+(defun coq-insert-infoH-hook 2453,96707
+(defun coq-insert-as 2458,96915
+(defun coq-insert-match 2475,97608
+(defun coq-insert-solve-tactic 2504,98777
+(defun coq-insert-tactic 2510,99028
+(defun coq-insert-tactical 2516,99230
+(defun coq-insert-command 2522,99461
+(defun coq-insert-term 2527,99626
+(define-key coq-keymap 2532,99787
+(define-key coq-keymap 2533,99845
+(define-key coq-keymap 2534,99902
+(define-key coq-keymap 2535,99971
+(define-key coq-keymap 2536,100027
+(define-key coq-keymap 2537,100076
+(define-key coq-keymap 2538,100134
+(define-key coq-keymap 2539,100184
+(define-key coq-keymap 2540,100239
+(define-key coq-keymap 2542,100292
+(define-key coq-keymap 2544,100366
+(define-key coq-keymap 2545,100423
+(define-key coq-keymap 2548,100488
+(define-key coq-keymap 2549,100548
+(define-key coq-keymap 2551,100604
+(define-key coq-keymap 2552,100654
+(define-key coq-keymap 2553,100704
+(define-key coq-keymap 2554,100760
+(define-key coq-keymap 2555,100810
+(define-key coq-keymap 2556,100854
+(define-key coq-keymap 2557,100913
+(define-key coq-goals-mode-map 2560,100974
+(define-key coq-goals-mode-map 2561,101056
+(define-key coq-goals-mode-map 2562,101138
+(define-key coq-goals-mode-map 2563,101225
+(define-key coq-goals-mode-map 2564,101307
+(defvar last-coq-error-location 2573,101612
+(defun coq-get-last-error-location 2581,101996
+(defun coq-highlight-error 2631,104559
+(defun coq-highlight-error-hook 2659,105640
+(defun coq-first-word-before 2669,105857
+(defun coq-show-first-goal 2680,106189
+(defvar coq-modeline-string2 2696,106854
+(defvar coq-modeline-string1 2697,106888
+(defvar coq-modeline-string0 2698,106922
+(defun coq-build-subgoals-string 2699,106963
+(defun coq-update-minor-mode-alist 2704,107129
+(defun is-not-split-vertic 2736,108544
+(defun optim-resp-windows 2745,108984
+
 hol98/hol98.el,121
-(defvar hol98-keywords 17,374
-(defvar hol98-rules 18,402
-(defvar hol98-tactics 19,427
-(defvar hol98-tacticals 20,454
-
-isar/isabelle-system.el,1254
-(defgroup isabelle 31,822
-(defcustom isabelle-web-page35,950
-(defcustom isa-isabelle-command44,1167
-(defvar isabelle-not-found 62,1849
-(defun isa-set-isabelle-command 65,1964
-(defun isa-shell-command-to-string 88,2982
-(defun isa-getenv 94,3206
-(defcustom isabelle-program-name-override 114,3905
-(defun isa-tool-list-logics 125,4251
-(defcustom isabelle-logics-available 132,4497
-(defcustom isabelle-chosen-logic 142,4834
-(defvar isabelle-chosen-logic-prev 158,5418
-(defun isabelle-hack-local-variables-function 161,5538
-(defun isabelle-set-prog-name 173,5977
-(defun isabelle-choose-logic 197,7097
-(defun isa-view-doc 216,7859
-(defun isa-tool-list-docs 223,8085
-(defconst isabelle-verbatim-regexp 241,8815
-(defun isabelle-verbatim 244,8957
-(defcustom isabelle-refresh-logics 251,9118
-(defvar isabelle-docs-menu259,9446
-(defvar isabelle-logics-menu-entries 266,9731
-(defun isabelle-logics-menu-calculate 269,9804
-(defvar isabelle-time-to-refresh-logics 290,10446
-(defun isabelle-logics-menu-refresh 294,10541
-(defun isabelle-menu-bar-update-logics 309,11188
-(defun isabelle-load-isar-keywords 325,11817
-(defun isabelle-create-span-menu 346,12545
-(defun isabelle-xml-sml-escapes 362,12976
-(defun isabelle-process-pgip 365,13077
+(defvar hol98-keywords 17,419
+(defvar hol98-rules 18,447
+(defvar hol98-tactics 19,472
+(defvar hol98-tacticals 20,499
+
+isar/isabelle-system.el,1255
+(defgroup isabelle 31,877
+(defcustom isabelle-web-page35,1005
+(defcustom isa-isabelle-command44,1222
+(defvar isabelle-not-found 62,1904
+(defun isa-set-isabelle-command 65,2019
+(defun isa-shell-command-to-string 88,3037
+(defun isa-getenv 94,3261
+(defcustom isabelle-program-name-override 114,3960
+(defun isa-tool-list-logics 125,4306
+(defcustom isabelle-logics-available 132,4552
+(defcustom isabelle-chosen-logic 142,4889
+(defvar isabelle-chosen-logic-prev 158,5473
+(defun isabelle-hack-local-variables-function 161,5593
+(defun isabelle-set-prog-name 173,6032
+(defun isabelle-choose-logic 197,7152
+(defun isa-view-doc 216,7914
+(defun isa-tool-list-docs 223,8140
+(defconst isabelle-verbatim-regexp 241,8870
+(defun isabelle-verbatim 244,9012
+(defcustom isabelle-refresh-logics 251,9173
+(defvar isabelle-docs-menu259,9501
+(defvar isabelle-logics-menu-entries 266,9786
+(defun isabelle-logics-menu-calculate 269,9859
+(defvar isabelle-time-to-refresh-logics 290,10501
+(defun isabelle-logics-menu-refresh 294,10596
+(defun isabelle-menu-bar-update-logics 309,11243
+(defun isabelle-load-isar-keywords 325,11872
+(defun isabelle-create-span-menu 346,12600
+(defun isabelle-xml-sml-escapes 362,13031
+(defun isabelle-process-pgip 365,13132
 
 isar/isar-autotest.el,31
-(defvar isar-long-tests 8,133
-
-isar/isar.el,1595
-(defcustom isar-keywords-name 41,895
-(defpgdefault completion-table 57,1406
-(defcustom isar-web-page59,1459
-(defun isar-strip-terminators 73,1809
-(defun isar-markup-ml 85,2165
-(defun isar-mode-config-set-variables 90,2300
-(defun isar-shell-mode-config-set-variables 155,5099
-(defun isar-set-proof-find-theorems-command 237,8289
-(defpacustom use-find-theorems-form 243,8473
-(defun isar-set-undo-commands 248,8639
-(defpacustom use-linear-undo 263,9272
-(defun isar-configure-from-settings 268,9430
-(defun isar-remove-file 276,9580
-(defun isar-shell-compute-new-files-list 288,9884
-(define-derived-mode isar-shell-mode 307,10454
-(define-derived-mode isar-response-mode 312,10581
-(define-derived-mode isar-goals-mode 317,10714
-(define-derived-mode isar-mode 322,10840
-(defpgdefault menu-entries374,12555
-(defun isar-set-command 405,13749
-(defpgdefault help-menu-entries 410,13879
-(defun isar-count-undos 413,13955
-(defun isar-find-and-forget 439,14921
-(defun isar-goal-command-p 475,16264
-(defun isar-global-save-command-p 480,16441
-(defvar isar-current-goal 501,17225
-(defun isar-state-preserving-p 504,17291
-(defvar isar-shell-current-line-width 529,18140
-(defun isar-shell-adjust-line-width 534,18332
-(defsubst isar-string-wrapping 557,19097
-(defsubst isar-positions-of 566,19291
-(defcustom isar-wrap-commands-singly 572,19496
-(defun isar-command-wrapping 578,19692
-(defun isar-preprocessing 586,20006
-(defun isar-mode-config 604,20557
-(defun isar-shell-mode-config 618,21210
-(defun isar-response-mode-config 628,21559
-(defun isar-goals-mode-config 638,21894
-
-isar/isar-find-theorems.el,778
-(defvar isar-find-theorems-data 19,507
-(defun isar-find-theorems-minibuffer 35,981
-(defun isar-find-theorems-form 49,1600
-(defvar isar-find-theorems-widget-number 92,3474
-(defvar isar-find-theorems-widget-pattern 95,3572
-(defvar isar-find-theorems-widget-intro 98,3664
-(defvar isar-find-theorems-widget-elim 101,3750
-(defvar isar-find-theorems-widget-dest 104,3834
-(defvar isar-find-theorems-widget-name 107,3918
-(defvar isar-find-theorems-widget-simp 110,4005
-(defun isar-find-theorems-create-searchform115,4151
-(defun isar-find-theorems-create-help 255,8694
-(defun isar-find-theorems-submit-searchform298,10866
-(defun isar-find-theorems-parse-criteria 376,13236
-(defun isar-find-theorems-parse-number 469,16217
-(defun isar-find-theorems-filter-empty 479,16494
+(defvar isar-long-tests 8,186
+
+isar/isar-find-theorems.el,779
+(defvar isar-find-theorems-data 19,565
+(defun isar-find-theorems-minibuffer 35,1039
+(defun isar-find-theorems-form 49,1658
+(defvar isar-find-theorems-widget-number 92,3532
+(defvar isar-find-theorems-widget-pattern 95,3630
+(defvar isar-find-theorems-widget-intro 98,3722
+(defvar isar-find-theorems-widget-elim 101,3808
+(defvar isar-find-theorems-widget-dest 104,3892
+(defvar isar-find-theorems-widget-name 107,3976
+(defvar isar-find-theorems-widget-simp 110,4063
+(defun isar-find-theorems-create-searchform115,4209
+(defun isar-find-theorems-create-help 255,8752
+(defun isar-find-theorems-submit-searchform298,10924
+(defun isar-find-theorems-parse-criteria 376,13294
+(defun isar-find-theorems-parse-number 469,16275
+(defun isar-find-theorems-filter-empty 479,16552
 
 isar/isar-keywords.el,1064
 (defconst isar-keywords-major7,222
@@ -541,106 +504,106 @@ isar/isar-keywords.el,1064
 (defconst isar-keywords-proof-script648,11005
 
 isar/isar-mmm.el,81
-(defconst isar-start-latex-regexp24,696
-(defconst isar-start-sml-regexp36,1124
+(defconst isar-start-latex-regexp24,744
+(defconst isar-start-sml-regexp36,1172
 
 isar/isar-syntax.el,4005
-(defconst isar-script-syntax-table-entries18,432
-(defconst isar-script-syntax-table-alist42,834
-(defun isar-init-syntax-table 51,1117
-(defun isar-init-output-syntax-table 59,1364
-(defconst isar-keyword-begin 74,1806
-(defconst isar-keyword-end 75,1844
-(defconst isar-keywords-theory-enclose77,1879
-(defconst isar-keywords-theory82,2017
-(defconst isar-keywords-save87,2148
-(defconst isar-keywords-proof-enclose92,2263
-(defconst isar-keywords-proof98,2424
-(defconst isar-keywords-proof-context105,2601
-(defconst isar-keywords-local-goal109,2708
-(defconst isar-keywords-proper113,2813
-(defconst isar-keywords-improper118,2932
-(defconst isar-keyword-level-alist123,3064
-(defconst isar-keywords-outline 138,3535
-(defconst isar-keywords-indent-open141,3611
-(defconst isar-keywords-indent-close148,3797
-(defconst isar-keywords-indent-enclose153,3930
-(defconst isar-ext-first 163,4159
-(defconst isar-ext-rest 164,4226
-(defconst isar-text 166,4298
-(defconst isar-long-id-stuff 167,4331
-(defconst isar-id 168,4405
-(defconst isar-idx 169,4475
-(defconst isar-string 171,4534
-(defun isar-ids-to-regexp 173,4594
-(defconst isar-any-command-regexp205,6386
-(defconst isar-name-regexp212,6759
-(defconst isar-improper-regexp218,7054
-(defconst isar-save-command-regexp222,7188
-(defconst isar-global-save-command-regexp225,7289
-(defconst isar-goal-command-regexp228,7403
-(defconst isar-local-goal-command-regexp231,7511
-(defconst isar-comment-start 234,7624
-(defconst isar-comment-end 235,7659
-(defconst isar-comment-start-regexp 236,7692
-(defconst isar-comment-end-regexp 237,7763
-(defconst isar-string-start-regexp 239,7831
-(defconst isar-string-end-regexp 240,7883
-(defun isar-syntactic-context 242,7934
-(defconst isar-antiq-regexp257,8329
-(defconst isar-nesting-regexp263,8480
-(defun isar-nesting 266,8578
-(defun isar-match-nesting 278,8971
-(defface isabelle-string-face 290,9305
-(defface isabelle-quote-face 298,9505
-(defface isabelle-class-name-face306,9701
-(defface isabelle-tfree-name-face314,9888
-(defface isabelle-tvar-name-face322,10081
-(defface isabelle-free-name-face330,10273
-(defface isabelle-bound-name-face338,10461
-(defface isabelle-var-name-face346,10652
-(defconst isabelle-string-face 354,10843
-(defconst isabelle-quote-face 355,10897
-(defconst isabelle-class-name-face 356,10950
-(defconst isabelle-tfree-name-face 357,11012
-(defconst isabelle-tvar-name-face 358,11074
-(defconst isabelle-free-name-face 359,11135
-(defconst isabelle-bound-name-face 360,11196
-(defconst isabelle-var-name-face 361,11258
-(defun isar-font-lock-fontify-syntactically-region 367,11407
-(defvar isar-font-lock-keywords-1402,12685
-(defun isar-output-flkprops 420,13693
-(defun isar-output-flk 426,13945
-(defvar isar-output-font-lock-keywords-1429,14054
-(defun isar-strip-output-markup 453,15053
-(defconst isar-shell-font-lock-keywords457,15189
-(defvar isar-goals-font-lock-keywords460,15273
-(defconst isar-linear-undo 494,15952
-(defconst isar-undo 496,15995
-(defconst isar-pr498,16038
-(defun isar-remove 505,16196
-(defun isar-undos 508,16271
-(defun isar-cannot-undo 518,16505
-(defconst isar-undo-commands521,16575
-(defconst isar-theory-start-regexp529,16712
-(defconst isar-end-regexp535,16870
-(defconst isar-undo-fail-regexp539,16971
-(defconst isar-undo-skip-regexp543,17075
-(defconst isar-undo-ignore-regexp546,17196
-(defconst isar-undo-remove-regexp549,17261
-(defconst isar-keywords-imenu557,17418
-(defconst isar-entity-regexp 564,17609
-(defconst isar-named-entity-regexp567,17705
-(defconst isar-named-entity-name-match-number572,17835
-(defconst isar-generic-expression575,17936
-(defconst isar-indent-any-regexp586,18170
-(defconst isar-indent-inner-regexp588,18263
-(defconst isar-indent-enclose-regexp590,18329
-(defconst isar-indent-open-regexp592,18445
-(defconst isar-indent-close-regexp594,18555
-(defconst isar-outline-regexp600,18692
-(defconst isar-outline-heading-end-regexp 604,18845
-(defconst isar-outline-heading-alist 606,18894
+(defconst isar-script-syntax-table-entries18,483
+(defconst isar-script-syntax-table-alist42,885
+(defun isar-init-syntax-table 51,1168
+(defun isar-init-output-syntax-table 59,1415
+(defconst isar-keyword-begin 74,1857
+(defconst isar-keyword-end 75,1895
+(defconst isar-keywords-theory-enclose77,1930
+(defconst isar-keywords-theory82,2068
+(defconst isar-keywords-save87,2199
+(defconst isar-keywords-proof-enclose92,2314
+(defconst isar-keywords-proof98,2475
+(defconst isar-keywords-proof-context105,2652
+(defconst isar-keywords-local-goal109,2759
+(defconst isar-keywords-proper113,2864
+(defconst isar-keywords-improper118,2983
+(defconst isar-keyword-level-alist123,3115
+(defconst isar-keywords-outline 138,3586
+(defconst isar-keywords-indent-open141,3662
+(defconst isar-keywords-indent-close148,3848
+(defconst isar-keywords-indent-enclose153,3981
+(defconst isar-ext-first 163,4210
+(defconst isar-ext-rest 164,4277
+(defconst isar-text 166,4349
+(defconst isar-long-id-stuff 167,4382
+(defconst isar-id 168,4456
+(defconst isar-idx 169,4526
+(defconst isar-string 171,4585
+(defun isar-ids-to-regexp 173,4645
+(defconst isar-any-command-regexp205,6437
+(defconst isar-name-regexp212,6810
+(defconst isar-improper-regexp218,7105
+(defconst isar-save-command-regexp222,7239
+(defconst isar-global-save-command-regexp225,7340
+(defconst isar-goal-command-regexp228,7454
+(defconst isar-local-goal-command-regexp231,7562
+(defconst isar-comment-start 234,7675
+(defconst isar-comment-end 235,7710
+(defconst isar-comment-start-regexp 236,7743
+(defconst isar-comment-end-regexp 237,7814
+(defconst isar-string-start-regexp 239,7882
+(defconst isar-string-end-regexp 240,7934
+(defun isar-syntactic-context 242,7985
+(defconst isar-antiq-regexp257,8380
+(defconst isar-nesting-regexp263,8531
+(defun isar-nesting 266,8629
+(defun isar-match-nesting 278,9022
+(defface isabelle-string-face 290,9356
+(defface isabelle-quote-face 298,9556
+(defface isabelle-class-name-face306,9752
+(defface isabelle-tfree-name-face314,9939
+(defface isabelle-tvar-name-face322,10132
+(defface isabelle-free-name-face330,10324
+(defface isabelle-bound-name-face338,10512
+(defface isabelle-var-name-face346,10703
+(defconst isabelle-string-face 354,10894
+(defconst isabelle-quote-face 355,10948
+(defconst isabelle-class-name-face 356,11001
+(defconst isabelle-tfree-name-face 357,11063
+(defconst isabelle-tvar-name-face 358,11125
+(defconst isabelle-free-name-face 359,11186
+(defconst isabelle-bound-name-face 360,11247
+(defconst isabelle-var-name-face 361,11309
+(defun isar-font-lock-fontify-syntactically-region 367,11458
+(defvar isar-font-lock-keywords-1402,12736
+(defun isar-output-flkprops 420,13744
+(defun isar-output-flk 426,13996
+(defvar isar-output-font-lock-keywords-1429,14105
+(defun isar-strip-output-markup 453,15104
+(defconst isar-shell-font-lock-keywords457,15240
+(defvar isar-goals-font-lock-keywords460,15324
+(defconst isar-linear-undo 494,16003
+(defconst isar-undo 496,16046
+(defconst isar-pr498,16089
+(defun isar-remove 505,16247
+(defun isar-undos 508,16322
+(defun isar-cannot-undo 518,16556
+(defconst isar-undo-commands521,16626
+(defconst isar-theory-start-regexp529,16763
+(defconst isar-end-regexp535,16921
+(defconst isar-undo-fail-regexp539,17022
+(defconst isar-undo-skip-regexp543,17126
+(defconst isar-undo-ignore-regexp546,17247
+(defconst isar-undo-remove-regexp549,17312
+(defconst isar-keywords-imenu557,17469
+(defconst isar-entity-regexp 564,17660
+(defconst isar-named-entity-regexp567,17756
+(defconst isar-named-entity-name-match-number572,17886
+(defconst isar-generic-expression575,17987
+(defconst isar-indent-any-regexp586,18221
+(defconst isar-indent-inner-regexp588,18314
+(defconst isar-indent-enclose-regexp590,18380
+(defconst isar-indent-open-regexp592,18496
+(defconst isar-indent-close-regexp594,18606
+(defconst isar-outline-regexp600,18743
+(defconst isar-outline-heading-end-regexp 604,18896
+(defconst isar-outline-heading-alist 606,18945
 
 isar/isar-unicode-tokens.el,1363
 (defgroup isabelle-tokens 25,672
@@ -674,94 +637,161 @@ 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 41,939
+(defpgdefault completion-table 57,1450
+(defcustom isar-web-page59,1503
+(defun isar-strip-terminators 73,1853
+(defun isar-markup-ml 85,2209
+(defun isar-mode-config-set-variables 90,2344
+(defun isar-shell-mode-config-set-variables 155,5143
+(defun isar-set-proof-find-theorems-command 237,8333
+(defpacustom use-find-theorems-form 243,8517
+(defun isar-set-undo-commands 248,8683
+(defpacustom use-linear-undo 263,9316
+(defun isar-configure-from-settings 268,9474
+(defun isar-remove-file 276,9624
+(defun isar-shell-compute-new-files-list 288,9928
+(define-derived-mode isar-shell-mode 307,10498
+(define-derived-mode isar-response-mode 312,10625
+(define-derived-mode isar-goals-mode 317,10758
+(define-derived-mode isar-mode 322,10884
+(defpgdefault menu-entries374,12599
+(defun isar-set-command 405,13793
+(defpgdefault help-menu-entries 410,13923
+(defun isar-count-undos 413,13999
+(defun isar-find-and-forget 439,14965
+(defun isar-goal-command-p 475,16308
+(defun isar-global-save-command-p 480,16485
+(defvar isar-current-goal 501,17269
+(defun isar-state-preserving-p 504,17335
+(defvar isar-shell-current-line-width 529,18184
+(defun isar-shell-adjust-line-width 534,18376
+(defsubst isar-string-wrapping 557,19141
+(defsubst isar-positions-of 566,19335
+(defcustom isar-wrap-commands-singly 572,19540
+(defun isar-command-wrapping 578,19736
+(defun isar-preprocessing 586,20050
+(defun isar-mode-config 604,20601
+(defun isar-shell-mode-config 618,21254
+(defun isar-response-mode-config 628,21603
+(defun isar-goals-mode-config 638,21938
+
+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,490
-(defcustom lego-test-all-name 26,626
-(defpgdefault help-menu-entries32,784
-(defpgdefault menu-entries36,944
-(defvar lego-shell-handle-output47,1245
-(defconst lego-process-config55,1543
-(defconst lego-pretty-set-width 66,1974
-(defconst lego-interrupt-regexp 70,2116
-(defcustom lego-www-home-page 75,2233
-(defcustom lego-www-latest-release80,2357
-(defcustom lego-www-refcard86,2532
-(defcustom lego-library-www-page92,2681
-(defvar lego-prog-name 101,2897
-(defvar lego-shell-cd 104,2966
-(defvar lego-shell-proof-completed-regexp 107,3065
-(defvar lego-save-command-regexp110,3205
-(defvar lego-goal-command-regexp112,3295
-(defvar lego-kill-goal-command 115,3386
-(defvar lego-forget-id-command 116,3429
-(defvar lego-undoable-commands-regexp118,3475
-(defvar lego-goal-regexp 127,3849
-(defvar lego-outline-regexp129,3894
-(defvar lego-outline-heading-end-regexp 135,4069
-(defvar lego-shell-outline-regexp 137,4122
-(defvar lego-shell-outline-heading-end-regexp 138,4174
-(define-derived-mode lego-shell-mode 144,4453
-(define-derived-mode lego-mode 151,4614
-(define-derived-mode lego-goals-mode 162,4924
-(defun lego-count-undos 173,5350
-(defun lego-goal-command-p 192,6087
-(defun lego-find-and-forget 197,6258
-(defun lego-goal-hyp 239,8094
-(defun lego-state-preserving-p 248,8291
-(defvar lego-shell-current-line-width 264,8994
-(defun lego-shell-adjust-line-width 272,9301
-(defun lego-mode-config 289,10002
-(defun lego-equal-module-filename 357,12053
-(defun lego-shell-compute-new-files-list 363,12328
-(defun lego-shell-mode-config 373,12711
-(defun lego-goals-mode-config 420,14378
-
-lego/lego-syntax.el,599
-(defconst lego-keywords-goal 15,307
-(defconst lego-keywords-save 17,350
-(defconst lego-commands19,421
-(defconst lego-keywords31,979
-(defconst lego-tacticals 36,1156
-(defconst lego-error-regexp 39,1264
-(defvar lego-id 42,1422
-(defvar lego-ids 44,1449
-(defconst lego-arg-list-regexp 48,1645
-(defun lego-decl-defn-regexp 51,1761
-(defconst lego-definiendum-alternative-regexp59,2133
-(defvar lego-font-lock-terms63,2317
-(defconst lego-goal-with-hole-regexp89,3170
-(defconst lego-save-with-hole-regexp94,3392
-(defvar lego-font-lock-keywords-199,3609
-(defun lego-init-syntax-table 110,4071
-
-phox/phox.el,554
-(defcustom phox-prog-name 32,881
-(defcustom phox-web-page37,983
-(defcustom phox-doc-dir43,1133
-(defcustom phox-lib-dir49,1280
-(defcustom phox-tags-program55,1423
-(defcustom phox-tags-doc61,1602
-(defcustom phox-etags67,1739
-(defpgdefault menu-entries88,2189
-(defun phox-config 102,2382
-(defun phox-shell-config 146,4308
-(define-derived-mode phox-mode 170,5170
-(define-derived-mode phox-shell-mode 186,5633
-(define-derived-mode phox-response-mode 191,5761
-(define-derived-mode phox-goals-mode 201,6122
-(defpgdefault completion-table224,6908
+(defcustom lego-tags 21,534
+(defcustom lego-test-all-name 26,670
+(defpgdefault help-menu-entries32,828
+(defpgdefault menu-entries36,988
+(defvar lego-shell-handle-output47,1289
+(defconst lego-process-config55,1587
+(defconst lego-pretty-set-width 66,2018
+(defconst lego-interrupt-regexp 70,2160
+(defcustom lego-www-home-page 75,2277
+(defcustom lego-www-latest-release80,2401
+(defcustom lego-www-refcard86,2576
+(defcustom lego-library-www-page92,2725
+(defvar lego-prog-name 101,2941
+(defvar lego-shell-cd 104,3010
+(defvar lego-shell-proof-completed-regexp 107,3109
+(defvar lego-save-command-regexp110,3249
+(defvar lego-goal-command-regexp112,3339
+(defvar lego-kill-goal-command 115,3430
+(defvar lego-forget-id-command 116,3473
+(defvar lego-undoable-commands-regexp118,3519
+(defvar lego-goal-regexp 127,3893
+(defvar lego-outline-regexp129,3938
+(defvar lego-outline-heading-end-regexp 135,4113
+(defvar lego-shell-outline-regexp 137,4166
+(defvar lego-shell-outline-heading-end-regexp 138,4218
+(define-derived-mode lego-shell-mode 144,4497
+(define-derived-mode lego-mode 151,4658
+(define-derived-mode lego-goals-mode 162,4968
+(defun lego-count-undos 173,5394
+(defun lego-goal-command-p 192,6131
+(defun lego-find-and-forget 197,6302
+(defun lego-goal-hyp 239,8138
+(defun lego-state-preserving-p 248,8335
+(defvar lego-shell-current-line-width 264,9038
+(defun lego-shell-adjust-line-width 272,9345
+(defun lego-mode-config 289,10046
+(defun lego-equal-module-filename 357,12097
+(defun lego-shell-compute-new-files-list 363,12372
+(defun lego-shell-mode-config 373,12755
+(defun lego-goals-mode-config 420,14422
+
+hol-light/hol-light-unicode-tokens.el,516
+(defconst hol-light-token-format 23,746
+(defconst hol-light-token-match 24,800
+(defconst hol-light-hexcode-match 25,837
+(defun hol-light-unicode-tokens-set 27,877
+(defcustom hol-light-token-symbol-map33,1117
+(defcustom hol-light-shortcut-alist128,3379
+(defconst hol-light-control-char-format-regexp217,5409
+(defconst hol-light-control-char-format 221,5540
+(defconst hol-light-control-characters223,5589
+(defconst hol-light-control-region-format-regexp 227,5687
+(defconst hol-light-control-regions229,5776
+
+hol-light/hol-light.el,1388
+(defcustom hol-light-home 16,478
+(defcustom hol-light-use-custom-toplevel 23,679
+(defconst hol-light-pre-sync-cmd38,1176
+(defcustom hol-light-init-cmd 42,1340
+(defconst hol-light-plain-start-goals-regexp55,1632
+(defconst hol-light-annotated-start-goals-regexp 62,1878
+(defconst hol-light-plain-interrupt-regexp66,2037
+(defconst hol-light-annotated-interrupt-regexp70,2168
+(defconst hol-light-plain-prompt-regexp74,2330
+(defconst hol-light-annotated-prompt-regexp78,2457
+(defconst hol-light-plain-error-regexp82,2602
+(defconst hol-light-annotated-error-regexp 90,2862
+(defconst hol-light-plain-proof-completed-regexp94,3022
+(defconst hol-light-annotated-proof-completed-regexp98,3175
+(defconst hol-light-plain-message-start 102,3356
+(defconst hol-light-annotated-message-start106,3489
+(defconst hol-light-plain-message-end110,3623
+(defconst hol-light-annotated-message-end114,3753
+(defvar hol-light-keywords 123,3908
+(defvar hol-light-rules 124,3940
+(defvar hol-light-tactics 125,3969
+(defvar hol-light-tacticals 126,4000
+(defvar hol-light-update-goal-regexp 336,12043
+(defvar hol-light-current-goal-regexp340,12169
+(defvar hol-light-newgoals-match 346,12356
+(defvar hol-light-statenumber-match 348,12427
+(defun hol-light-get-proof-info 373,13217
+(defun hol-light-find-begin-of-unfinished-proof 388,13693
+(defun hol-light-proof-tree-get-new-subgoals 399,14142
 
 phox/phox-extraction.el,383
-(defvar phox-prog-orig 19,584
-(defun phox-prog-flags-modify(21,652
-(defun phox-prog-flags-extract(50,1453
-(defun phox-prog-flags-erase(61,1743
-(defun phox-toggle-extraction(69,1939
-(defun phox-compile-theorem(81,2341
-(defun phox-compile-theorem-on-cursor(87,2566
-(defun phox-output 103,3044
-(defun phox-output-theorem 113,3256
-(defun phox-output-theorem-on-cursor(120,3555
+(defvar phox-prog-orig 19,619
+(defun phox-prog-flags-modify(21,687
+(defun phox-prog-flags-extract(50,1488
+(defun phox-prog-flags-erase(61,1778
+(defun phox-toggle-extraction(69,1974
+(defun phox-compile-theorem(81,2376
+(defun phox-compile-theorem-on-cursor(87,2601
+(defun phox-output 103,3079
+(defun phox-output-theorem 113,3291
+(defun phox-output-theorem-on-cursor(120,3590
 
 phox/phox-font.el,231
 (defvar phox-sym-lock-enabled 1,0
@@ -771,59 +801,59 @@ phox/phox-font.el,231
 (defconst phox-sym-lock-keywords-table70,2628
 (defun phox-sym-lock-start 93,3202
 
-phox/phox-fun.el,1658
-(defconst phox-forget-id-command 11,151
-(defconst phox-forget-proof-command 12,197
-(defconst phox-forget-new-elim-command 13,252
-(defconst phox-forget-new-intro-command 14,310
-(defconst phox-forget-new-equation-command 15,370
-(defconst phox-forget-close-def-command 16,436
-(defconst phox-comments-regexp 18,562
-(defconst phox-strict-comments-regexp 20,741
-(defconst phox-ident-regexp 21,906
-(defconst phox-inductive-option 22,992
-(defconst phox-spaces-regexp 23,1044
-(defconst phox-sy-definition-regexp 24,1087
-(defconst phox-sy-inductive-regexp 28,1274
-(defconst phox-inductive-regexp 34,1487
-(defconst phox-data-regexp 40,1638
-(defconst phox-definition-regexp 46,1792
-(defconst phox-prove-claim-regexp 50,1936
-(defconst phox-new-elim-regexp 54,2042
-(defconst phox-new-intro-regexp 57,2161
-(defconst phox-new-rewrite-regexp 60,2282
-(defconst phox-new-equation-regexp 63,2407
-(defconst phox-close-def-regexp 66,2534
-(defun phox-init-syntax-table 71,2671
-(defvar phox-top-keywords87,3143
-(defvar phox-proof-keywords135,3598
-(defun phox-find-and-forget 176,3948
-(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive
255,6364
-(defun phox-depend-theorem(274,7330
-(defun phox-eshow-extlist(283,7619
-(defun phox-flag-name(297,8216
-(defun phox-path(308,8518
-(defun phox-print-expression(319,8754
-(defun phox-print-sort-expression(332,9210
-(defun phox-priority-symbols-list(343,9522
-(defun phox-search-string(355,9894
-(defun phox-constraints(370,10419
-(defun phox-goals(381,10675
-(defvar phox-state-menu393,10884
-(defun phox-delete-symbol(418,11874
-(defun phox-delete-symbol-on-cursor(424,12082
+phox/phox-fun.el,1659
+(defconst phox-forget-id-command 11,186
+(defconst phox-forget-proof-command 12,232
+(defconst phox-forget-new-elim-command 13,287
+(defconst phox-forget-new-intro-command 14,345
+(defconst phox-forget-new-equation-command 15,405
+(defconst phox-forget-close-def-command 16,471
+(defconst phox-comments-regexp 18,597
+(defconst phox-strict-comments-regexp 20,776
+(defconst phox-ident-regexp 21,941
+(defconst phox-inductive-option 22,1027
+(defconst phox-spaces-regexp 23,1079
+(defconst phox-sy-definition-regexp 24,1122
+(defconst phox-sy-inductive-regexp 28,1309
+(defconst phox-inductive-regexp 34,1522
+(defconst phox-data-regexp 40,1673
+(defconst phox-definition-regexp 46,1827
+(defconst phox-prove-claim-regexp 50,1971
+(defconst phox-new-elim-regexp 54,2077
+(defconst phox-new-intro-regexp 57,2196
+(defconst phox-new-rewrite-regexp 60,2317
+(defconst phox-new-equation-regexp 63,2442
+(defconst phox-close-def-regexp 66,2569
+(defun phox-init-syntax-table 71,2706
+(defvar phox-top-keywords87,3178
+(defvar phox-proof-keywords135,3633
+(defun phox-find-and-forget 176,3983
+(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive
255,6399
+(defun phox-depend-theorem(274,7365
+(defun phox-eshow-extlist(283,7654
+(defun phox-flag-name(297,8251
+(defun phox-path(308,8553
+(defun phox-print-expression(319,8789
+(defun phox-print-sort-expression(332,9245
+(defun phox-priority-symbols-list(343,9557
+(defun phox-search-string(355,9929
+(defun phox-constraints(370,10454
+(defun phox-goals(381,10710
+(defvar phox-state-menu393,10919
+(defun phox-delete-symbol(418,11909
+(defun phox-delete-symbol-on-cursor(424,12117
 
 phox/phox-lang.el,323
-(defvar phox-lang9,271
-(defun phox-lang-absurd 17,500
-(defun phox-lang-suppress 22,594
-(defun phox-lang-opendef 27,791
-(defun phox-lang-instance 32,909
-(defun phox-lang-open-instance 37,1038
-(defun phox-lang-lock 42,1187
-(defun phox-lang-unlock 47,1317
-(defun phox-lang-prove 52,1453
-(defun phox-lang-let 57,1587
+(defvar phox-lang9,306
+(defun phox-lang-absurd 17,535
+(defun phox-lang-suppress 22,629
+(defun phox-lang-opendef 27,826
+(defun phox-lang-instance 32,944
+(defun phox-lang-open-instance 37,1073
+(defun phox-lang-lock 42,1222
+(defun phox-lang-unlock 47,1352
+(defun phox-lang-prove 52,1488
+(defun phox-lang-let 57,1622
 
 phox/phox-outline.el,254
 (defconst phox-outline-title-regexp 19,723
@@ -834,16 +864,16 @@ phox/phox-outline.el,254
 (defun phox-setup-outline 58,2036
 
 phox/phox-pbrpm.el,513
-(defun phox-pbrpm-left-paren-p 39,1636
-(defun phox-pbrpm-right-paren-p 46,1839
-(defun phox-pbrpm-menu-from-string 54,2043
-(defun phox-pbrpm-rename-in-cmd 63,2375
-(defun phox-pbrpm-get-region-name 96,3623
-(defun  phox-pbrpm-escape-string 99,3750
-(defun phox-pbrpm-generate-menu 103,3885
-(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
310,11365
-(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
311,11429
-(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
312,11491
+(defun phox-pbrpm-left-paren-p 39,1671
+(defun phox-pbrpm-right-paren-p 46,1874
+(defun phox-pbrpm-menu-from-string 54,2078
+(defun phox-pbrpm-rename-in-cmd 63,2410
+(defun phox-pbrpm-get-region-name 96,3658
+(defun  phox-pbrpm-escape-string 99,3785
+(defun phox-pbrpm-generate-menu 103,3920
+(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
310,11400
+(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
311,11464
+(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
312,11526
 
 phox/phox-sym-lock.el,1398
 (defcustom phox-sym-lock-enabled 19,871
@@ -880,81 +910,98 @@ phox/phox-sym-lock.el,1398
 (defun phox-sym-lock-patch-keywords 384,14798
 
 phox/phox-tags.el,305
-(defun phox-tags-add-table(26,834
-(defun phox-tags-reset-table(35,1229
-(defun phox-tags-add-doc-table(40,1339
-(defun phox-tags-add-lib-table(46,1488
-(defun phox-tags-add-local-table(52,1623
-(defun phox-tags-create-local-table(58,1806
-(defun phox-complete-tag(69,2056
-(defvar phox-tags-menu76,2165
+(defun phox-tags-add-table(26,869
+(defun phox-tags-reset-table(35,1264
+(defun phox-tags-add-doc-table(40,1374
+(defun phox-tags-add-lib-table(46,1523
+(defun phox-tags-add-local-table(52,1658
+(defun phox-tags-create-local-table(58,1841
+(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,925
-(defun proof-associated-windows 43,1135
+(defun proof-associated-buffers 33,973
+(defun proof-associated-windows 43,1183
 
 generic/pg-autotest.el,908
-(defvar pg-autotest-success 29,639
-(defvar pg-autotest-log 32,726
-(defun pg-autotest-find-file 37,820
-(defun pg-autotest-find-file-restart 44,1086
-(defmacro pg-autotest-apply 58,1560
-(defmacro pg-autotest 72,1975
-(defun pg-autotest-log 89,2412
-(defun pg-autotest-message 98,2675
-(defun pg-autotest-remark 107,2964
-(defun pg-autotest-timestart 110,3045
-(defun pg-autotest-timetaken 115,3228
-(defun pg-autotest-start 129,3616
-(defun pg-autotest-exit 140,4070
-(defun pg-autotest-test-process-wholefile 160,4853
-(defun pg-autotest-test-script-wholefile 168,5140
-(defun pg-autotest-test-script-randomjumps 193,6072
-(defun pg-autotest-test-retract-file 242,7629
-(defun pg-autotest-test-assert-processed 248,7770
-(defun pg-autotest-test-assert-full 254,7996
-(defun pg-autotest-test-assert-unprocessed 261,8237
-(defun pg-autotest-test-eval 268,8502
-(defun pg-autotest-test-quit-prover 272,8601
+(defvar pg-autotest-success 29,690
+(defvar pg-autotest-log 32,777
+(defun pg-autotest-find-file 37,871
+(defun pg-autotest-find-file-restart 44,1137
+(defmacro pg-autotest-apply 58,1611
+(defmacro pg-autotest 72,2026
+(defun pg-autotest-log 89,2463
+(defun pg-autotest-message 98,2726
+(defun pg-autotest-remark 107,3015
+(defun pg-autotest-timestart 110,3096
+(defun pg-autotest-timetaken 115,3279
+(defun pg-autotest-start 129,3667
+(defun pg-autotest-exit 140,4121
+(defun pg-autotest-test-process-wholefile 160,4904
+(defun pg-autotest-test-script-wholefile 168,5191
+(defun pg-autotest-test-script-randomjumps 193,6123
+(defun pg-autotest-test-retract-file 242,7680
+(defun pg-autotest-test-assert-processed 248,7821
+(defun pg-autotest-test-assert-full 254,8047
+(defun pg-autotest-test-assert-unprocessed 261,8288
+(defun pg-autotest-test-eval 268,8553
+(defun pg-autotest-test-quit-prover 272,8652
 
 generic/pg-custom.el,635
-(defpgcustom script-indent 37,1150
-(defconst proof-toolbar-entries-default42,1287
-(defpgcustom toolbar-entries 71,3122
-(defpgcustom prog-args 90,3855
-(defpgcustom prog-env 102,4433
-(defpgcustom quit-timeout 111,4862
-(defpgcustom favourites 123,5289
-(defpgcustom menu-entries 128,5478
-(defpgcustom help-menu-entries 135,5714
-(defpgcustom keymap 142,5977
-(defpgcustom completion-table 147,6148
-(defpgcustom tags-program 158,6524
-(defpgcustom use-holes 167,6908
-(defpgcustom one-command-per-line174,7166
-(defpgcustom maths-menu-enable 185,7402
-(defpgcustom unicode-tokens-enable 191,7582
-(defpgcustom mmm-enable 197,7789
+(defpgcustom script-indent 37,1201
+(defconst proof-toolbar-entries-default42,1338
+(defpgcustom toolbar-entries 71,3173
+(defpgcustom prog-args 90,3906
+(defpgcustom prog-env 102,4484
+(defpgcustom quit-timeout 111,4913
+(defpgcustom favourites 123,5340
+(defpgcustom menu-entries 128,5529
+(defpgcustom help-menu-entries 135,5765
+(defpgcustom keymap 142,6028
+(defpgcustom completion-table 147,6199
+(defpgcustom tags-program 158,6575
+(defpgcustom use-holes 167,6959
+(defpgcustom one-command-per-line174,7217
+(defpgcustom maths-menu-enable 185,7453
+(defpgcustom unicode-tokens-enable 191,7633
+(defpgcustom mmm-enable 197,7840
 
 generic/pg-goals.el,285
-(define-derived-mode proof-goals-mode 29,686
-(define-key proof-goals-mode-map 56,1544
-(define-key proof-goals-mode-map 58,1660
-(define-key proof-goals-mode-map 59,1728
-(defun proof-goals-config-done 68,1875
-(defun pg-goals-display 76,2141
-(defun pg-goals-button-action 117,3445
+(define-derived-mode proof-goals-mode 29,734
+(define-key proof-goals-mode-map 56,1592
+(define-key proof-goals-mode-map 58,1708
+(define-key proof-goals-mode-map 59,1776
+(defun proof-goals-config-done 68,1923
+(defun pg-goals-display 76,2189
+(defun pg-goals-button-action 119,3648
 
 generic/pg-movie.el,333
-(defconst pg-movie-xml-header 32,875
-(defconst pg-movie-stylesheet34,933
-(defun pg-movie-stylesheet-location 37,1032
-(defvar pg-movie-frame 41,1140
-(defun pg-movie-of-span 43,1194
-(defun pg-movie-of-region 79,2314
-(defun pg-movie-export 86,2502
-(defun pg-movie-export-from 108,3106
-(defun pg-movie-export-directory 119,3427
+(defconst pg-movie-xml-header 32,923
+(defconst pg-movie-stylesheet34,981
+(defun pg-movie-stylesheet-location 37,1080
+(defvar pg-movie-frame 41,1188
+(defun pg-movie-of-span 43,1242
+(defun pg-movie-of-region 79,2362
+(defun pg-movie-export 86,2550
+(defun pg-movie-export-from 108,3154
+(defun pg-movie-export-directory 119,3475
 
 generic/pg-pamacs.el,534
 (defmacro deflocal 35,1138
@@ -974,307 +1021,306 @@ generic/pg-pamacs.el,534
 (defmacro proof-eval-when-ready-for-assistant 270,9510
 
 generic/pg-pbrpm.el,1808
-(defvar pg-pbrpm-use-buffer-menu 45,1159
-(defvar pg-pbrpm-start-goal-regexp 48,1281
-(defvar pg-pbrpm-start-goal-regexp-par-num 52,1438
-(defvar pg-pbrpm-end-goal-regexp 55,1561
-(defvar pg-pbrpm-start-hyp-regexp 59,1713
-(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1874
-(defvar pg-pbrpm-start-concl-regexp 67,2081
-(defvar pg-pbrpm-auto-select-regexp 71,2245
-(defvar pg-pbrpm-buffer-menu 78,2406
-(defvar pg-pbrpm-spans 79,2440
-(defvar pg-pbrpm-goal-description 80,2468
-(defvar pg-pbrpm-windows-dialog-bug 81,2507
-(defvar pbrpm-menu-desc 82,2548
-(defun pg-pbrpm-erase-buffer-menu 84,2578
-(defun pg-pbrpm-menu-change-hook 90,2750
-(defun pg-pbrpm-create-reset-buffer-menu 108,3325
-(defun pg-pbrpm-analyse-goal-buffer 127,4167
-(defun pg-pbrpm-button-action 187,6572
-(defun pg-pbrpm-exists 194,6798
-(defun pg-pbrpm-eliminate-id 198,6910
-(defun pg-pbrpm-build-menu 206,7156
-(defun pg-pbrpm-setup-span 269,9476
-(defun pg-pbrpm-run-command 329,11775
-(defun pg-pbrpm-get-pos-info 362,13300
-(defun pg-pbrpm-get-region-info 404,14599
-(defun pg-pbrpm-auto-select-around-point 415,15011
-(defun pg-pbrpm-translate-position 430,15535
-(defun pg-pbrpm-process-click 438,15789
-(defvar pg-pbrpm-remember-region-selected-region 458,16814
-(defvar pg-pbrpm-regions-list 459,16868
-(defun pg-pbrpm-erase-regions-list 461,16904
-(defun pg-pbrpm-filter-regions-list 470,17212
-(defface pg-pbrpm-multiple-selection-face477,17475
-(defface pg-pbrpm-menu-input-face485,17677
-(defun pg-pbrpm-do-remember-region 493,17867
-(defun pg-pbrpm-remember-region-drag-up-hook 514,18715
-(defun pg-pbrpm-remember-region-click-hook 518,18886
-(defun pg-pbrpm-remember-region 523,19071
-(defun pg-pbrpm-process-region 537,19785
-(defun pg-pbrpm-process-regions-list 555,20514
-(defun pg-pbrpm-region-expression 559,20697
-
-generic/pg-pgip.el,2931
-(defalias 'pg-pgip-debug pg-pgip-debug
39,1044
-(defalias 'pg-pgip-error pg-pgip-error
40,1085
-(defalias 'pg-pgip-warning pg-pgip-warning
41,1120
-(defconst pg-pgip-version-supported 43,1170
-(defun pg-pgip-process-packet 47,1276
-(defvar pg-pgip-last-seen-id 57,1844
-(defvar pg-pgip-last-seen-seq 58,1878
-(defun pg-pgip-process-pgip 60,1914
-(defun pg-pgip-process-msg 79,2854
-(defvar pg-pgip-post-process-functions94,3445
-(defun pg-pgip-post-process 104,3920
-(defun pg-pgip-process-askpgip 121,4535
-(defun pg-pgip-process-usespgip 127,4739
-(defun pg-pgip-process-usespgml 131,4903
-(defun pg-pgip-process-pgmlconfig 135,5067
-(defun pg-pgip-process-proverinfo 151,5684
-(defun pg-pgip-process-hasprefs 168,6349
-(defun pg-pgip-haspref 182,6981
-(defun pg-pgip-process-prefval 200,7697
-(defun pg-pgip-process-guiconfig 227,8405
-(defvar proof-assistant-idtables 234,8522
-(defun pg-pgip-process-ids 237,8639
-(defun pg-complete-idtable-symbol 263,9711
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids
268,9803
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids
269,9859
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids
270,9915
-(defun pg-pgip-process-idvalue 273,9973
-(defun pg-pgip-process-menuadd 285,10319
-(defun pg-pgip-process-menudel 288,10362
-(defun pg-pgip-process-ready 297,10594
-(defun pg-pgip-process-cleardisplay 300,10635
-(defun pg-pgip-process-proofstate 314,11092
-(defun pg-pgip-process-normalresponse 318,11169
-(defun pg-pgip-process-errorresponse 322,11299
-(defun pg-pgip-process-scriptinsert 326,11428
-(defun pg-pgip-process-metainforesponse 331,11562
-(defun pg-pgip-file-of-url 340,11802
-(defun pg-pgip-process-informfileloaded 345,11937
-(defun pg-pgip-process-informfileretracted 351,12169
-(defun pg-pgip-process-brokerstatus 364,12616
-(defun pg-pgip-process-proveravailmsg 367,12664
-(defun pg-pgip-process-newprovermsg 370,12714
-(defun pg-pgip-process-proverstatusmsg 373,12762
-(defvar pg-pgip-srcids 382,13008
-(defun pg-pgip-process-newfile 386,13115
-(defun pg-pgip-process-filestatus 402,13697
-(defun pg-pgip-process-newobj 422,14351
-(defun pg-pgip-process-delobj 425,14393
-(defun pg-pgip-process-objectstatus 428,14435
-(defun pg-pgip-process-parsescript 442,14787
-(defun pg-pgip-get-pgiptype 465,15661
-(defun pg-pgip-default-for 486,16524
-(defun pg-pgip-subst-for 499,16919
-(defun pg-pgip-interpret-value 512,17289
-(defun pg-pgip-interpret-choice 531,18014
-(defun pg-pgip-string-of-command 562,19031
-(defconst pg-pgip-id579,19792
-(defvar pg-pgip-refseq 585,20072
-(defvar pg-pgip-refid 587,20169
-(defvar pg-pgip-seq 590,20261
-(defun pg-pgip-assemble-packet 592,20325
-(defun pg-pgip-issue 610,21136
-(defun pg-pgip-maybe-askpgip 627,21748
-(defun pg-pgip-askprefs 633,21939
-(defun pg-pgip-askids 637,22053
-(defun pg-pgip-reset 650,22341
-(defconst pg-pgip-start-element-regexp 681,23039
-(defconst pg-pgip-end-element-regexp 682,23091
-
-generic/pg-response.el,1251
-(deflocal pg-response-eagerly-raise 32,737
-(define-derived-mode proof-response-mode 42,962
-(define-key proof-response-mode-map 69,1899
-(define-key proof-response-mode-map 70,1970
-(define-key proof-response-mode-map 71,2024
-(defun proof-response-config-done 75,2110
-(defvar pg-response-special-display-regexp 86,2456
-(defconst proof-multiframe-parameters90,2623
-(defun proof-multiple-frames-enable 99,2913
-(defun proof-three-window-enable 109,3241
-(defun proof-select-three-b 112,3304
-(defun proof-display-three-b 127,3795
-(defvar pg-frame-configuration 138,4185
-(defun pg-cache-frame-configuration 142,4332
-(defun proof-layout-windows 146,4503
-(defun proof-delete-other-frames 186,6290
-(defvar pg-response-erase-flag 217,7378
-(defun pg-response-maybe-erase221,7507
-(defun pg-response-display 251,8611
-(defun pg-response-display-with-face 276,9394
-(defun pg-response-clear-displays 304,10240
-(defun pg-response-message 322,10946
-(defun pg-response-warning 328,11181
-(defun proof-next-error 343,11587
-(defun pg-response-has-error-location 421,14396
-(defcustom proof-trace-buffer-max-lines 436,14815
-(defun proof-trace-buffer-display 443,15050
-(defun proof-trace-buffer-finish 457,15457
-(defun pg-thms-buffer-clear 481,16110
-
-generic/pg-user.el,3635
-(defun proof-script-new-command-advance 43,1185
-(defun proof-maybe-follow-locked-end 67,2110
-(defun proof-goto-command-start 93,2946
-(defun proof-goto-command-end 116,3893
-(defun proof-forward-command 131,4315
-(defun proof-backward-command 152,5036
-(defun proof-goto-point 163,5250
-(defun proof-assert-next-command-interactive 177,5684
-(defun proof-assert-until-point-interactive 189,6170
-(defun proof-process-buffer 196,6415
-(defun proof-undo-last-successful-command 214,6927
-(defun proof-undo-and-delete-last-successful-command 219,7089
-(defun proof-undo-last-successful-command-1 231,7608
-(defun proof-retract-buffer 248,8272
-(defun proof-retract-current-goal 257,8556
-(defun proof-mouse-goto-point 276,9076
-(defvar proof-minibuffer-history 291,9352
-(defun proof-minibuffer-cmd 294,9447
-(defun proof-frob-locked-end 333,10854
-(defmacro proof-if-setting-configured 369,11955
-(defmacro proof-define-assistant-command 377,12224
-(defmacro proof-define-assistant-command-witharg 390,12679
-(defun proof-issue-new-command 410,13501
-(defun proof-cd-sync 450,14724
-(defun proof-electric-terminator-enable 501,16323
-(defun proof-electric-terminator 509,16627
-(defun proof-add-completions 537,17597
-(defun proof-script-complete 560,18420
-(defun pg-copy-span-contents 574,18729
-(defun pg-numth-span-higher-or-lower 588,19153
-(defun pg-control-span-of 614,19899
-(defun pg-move-span-contents 620,20103
-(defun pg-fixup-children-spans 671,22221
-(defun pg-move-region-down 681,22478
-(defun pg-move-region-up 690,22771
-(defun pg-pos-for-event 704,23045
-(defun pg-span-for-event 710,23266
-(defun pg-span-context-menu 714,23410
-(defun pg-toggle-visibility 730,23927
-(defun pg-create-in-span-context-menu 739,24234
-(defun pg-span-undo 764,25262
-(defun pg-goals-buffers-hint 777,25500
-(defun pg-slow-fontify-tracing-hint 781,25718
-(defun pg-response-buffers-hint 785,25907
-(defun pg-jump-to-end-hint 797,26322
-(defun pg-processing-complete-hint 801,26451
-(defun pg-next-error-hint 818,27171
-(defun pg-hint 823,27323
-(defun pg-identifier-under-mouse-query 834,27672
-(defun pg-identifier-near-point-query 845,27996
-(defvar proof-query-identifier-history 874,28919
-(defun proof-query-identifier 877,29006
-(defun pg-identifier-query 888,29362
-(defun proof-imenu-enable 921,30510
-(defvar pg-input-ring 957,31813
-(defvar pg-input-ring-index 960,31870
-(defvar pg-stored-incomplete-input 963,31942
-(defun pg-previous-input 966,32045
-(defun pg-next-input 980,32508
-(defun pg-delete-input 985,32630
-(defun pg-get-old-input 998,32968
-(defun pg-restore-input 1012,33359
-(defun pg-search-start 1023,33649
-(defun pg-regexp-arg 1035,34141
-(defun pg-search-arg 1047,34589
-(defun pg-previous-matching-input-string-position 1061,35006
-(defun pg-previous-matching-input 1088,36171
-(defun pg-next-matching-input 1107,37021
-(defvar pg-matching-input-from-input-string 1115,37404
-(defun pg-previous-matching-input-from-input 1119,37518
-(defun pg-next-matching-input-from-input 1137,38283
-(defun pg-add-to-input-history 1148,38662
-(defun pg-remove-from-input-history 1160,39115
-(defun  pg-clear-input-ring 1171,39495
-(define-key proof-mode-map 1188,39965
-(define-key proof-mode-map 1189,40025
-(defun pg-protected-undo 1191,40097
-(defun pg-protected-undo-1 1221,41391
-(defun next-undo-elt 1252,42828
-(defvar proof-autosend-timer 1279,43784
-(deflocal proof-autosend-modified-tick 1281,43845
-(defun proof-autosend-enable 1285,43967
-(defun proof-autosend-delay 1299,44510
-(defun proof-autosend-loop 1303,44643
-(defun proof-autosend-loop-all 1317,45203
-(defun proof-autosend-loop-next 1341,45983
+(defvar pg-pbrpm-use-buffer-menu 45,1207
+(defvar pg-pbrpm-start-goal-regexp 48,1329
+(defvar pg-pbrpm-start-goal-regexp-par-num 52,1486
+(defvar pg-pbrpm-end-goal-regexp 55,1609
+(defvar pg-pbrpm-start-hyp-regexp 59,1761
+(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1922
+(defvar pg-pbrpm-start-concl-regexp 67,2129
+(defvar pg-pbrpm-auto-select-regexp 71,2293
+(defvar pg-pbrpm-buffer-menu 78,2454
+(defvar pg-pbrpm-spans 79,2488
+(defvar pg-pbrpm-goal-description 80,2516
+(defvar pg-pbrpm-windows-dialog-bug 81,2555
+(defvar pbrpm-menu-desc 82,2596
+(defun pg-pbrpm-erase-buffer-menu 84,2626
+(defun pg-pbrpm-menu-change-hook 90,2798
+(defun pg-pbrpm-create-reset-buffer-menu 108,3373
+(defun pg-pbrpm-analyse-goal-buffer 127,4215
+(defun pg-pbrpm-button-action 187,6620
+(defun pg-pbrpm-exists 194,6846
+(defun pg-pbrpm-eliminate-id 198,6958
+(defun pg-pbrpm-build-menu 206,7204
+(defun pg-pbrpm-setup-span 269,9524
+(defun pg-pbrpm-run-command 329,11823
+(defun pg-pbrpm-get-pos-info 362,13348
+(defun pg-pbrpm-get-region-info 404,14647
+(defun pg-pbrpm-auto-select-around-point 415,15059
+(defun pg-pbrpm-translate-position 430,15583
+(defun pg-pbrpm-process-click 438,15837
+(defvar pg-pbrpm-remember-region-selected-region 458,16862
+(defvar pg-pbrpm-regions-list 459,16916
+(defun pg-pbrpm-erase-regions-list 461,16952
+(defun pg-pbrpm-filter-regions-list 470,17260
+(defface pg-pbrpm-multiple-selection-face477,17523
+(defface pg-pbrpm-menu-input-face485,17725
+(defun pg-pbrpm-do-remember-region 493,17915
+(defun pg-pbrpm-remember-region-drag-up-hook 514,18763
+(defun pg-pbrpm-remember-region-click-hook 518,18934
+(defun pg-pbrpm-remember-region 523,19119
+(defun pg-pbrpm-process-region 537,19833
+(defun pg-pbrpm-process-regions-list 555,20562
+(defun pg-pbrpm-region-expression 559,20745
+
+generic/pg-pgip.el,2932
+(defalias 'pg-pgip-debug pg-pgip-debug
39,1091
+(defalias 'pg-pgip-error pg-pgip-error
40,1132
+(defalias 'pg-pgip-warning pg-pgip-warning
41,1167
+(defconst pg-pgip-version-supported 43,1217
+(defun pg-pgip-process-packet 47,1323
+(defvar pg-pgip-last-seen-id 57,1891
+(defvar pg-pgip-last-seen-seq 58,1925
+(defun pg-pgip-process-pgip 60,1961
+(defun pg-pgip-process-msg 79,2901
+(defvar pg-pgip-post-process-functions94,3492
+(defun pg-pgip-post-process 104,3967
+(defun pg-pgip-process-askpgip 121,4582
+(defun pg-pgip-process-usespgip 127,4786
+(defun pg-pgip-process-usespgml 131,4950
+(defun pg-pgip-process-pgmlconfig 135,5114
+(defun pg-pgip-process-proverinfo 151,5731
+(defun pg-pgip-process-hasprefs 168,6396
+(defun pg-pgip-haspref 182,7028
+(defun pg-pgip-process-prefval 200,7744
+(defun pg-pgip-process-guiconfig 227,8452
+(defvar proof-assistant-idtables 234,8569
+(defun pg-pgip-process-ids 237,8686
+(defun pg-complete-idtable-symbol 263,9758
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids
268,9850
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids
269,9906
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids
270,9962
+(defun pg-pgip-process-idvalue 273,10020
+(defun pg-pgip-process-menuadd 285,10366
+(defun pg-pgip-process-menudel 288,10409
+(defun pg-pgip-process-ready 297,10641
+(defun pg-pgip-process-cleardisplay 300,10682
+(defun pg-pgip-process-proofstate 314,11139
+(defun pg-pgip-process-normalresponse 318,11216
+(defun pg-pgip-process-errorresponse 322,11346
+(defun pg-pgip-process-scriptinsert 326,11475
+(defun pg-pgip-process-metainforesponse 331,11609
+(defun pg-pgip-file-of-url 340,11849
+(defun pg-pgip-process-informfileloaded 345,11984
+(defun pg-pgip-process-informfileretracted 351,12216
+(defun pg-pgip-process-brokerstatus 364,12663
+(defun pg-pgip-process-proveravailmsg 367,12711
+(defun pg-pgip-process-newprovermsg 370,12761
+(defun pg-pgip-process-proverstatusmsg 373,12809
+(defvar pg-pgip-srcids 382,13055
+(defun pg-pgip-process-newfile 386,13162
+(defun pg-pgip-process-filestatus 402,13744
+(defun pg-pgip-process-newobj 422,14398
+(defun pg-pgip-process-delobj 425,14440
+(defun pg-pgip-process-objectstatus 428,14482
+(defun pg-pgip-process-parsescript 442,14834
+(defun pg-pgip-get-pgiptype 465,15708
+(defun pg-pgip-default-for 486,16571
+(defun pg-pgip-subst-for 499,16966
+(defun pg-pgip-interpret-value 512,17336
+(defun pg-pgip-interpret-choice 531,18061
+(defun pg-pgip-string-of-command 562,19078
+(defconst pg-pgip-id579,19839
+(defvar pg-pgip-refseq 585,20119
+(defvar pg-pgip-refid 587,20216
+(defvar pg-pgip-seq 590,20308
+(defun pg-pgip-assemble-packet 592,20372
+(defun pg-pgip-issue 610,21183
+(defun pg-pgip-maybe-askpgip 627,21795
+(defun pg-pgip-askprefs 633,21986
+(defun pg-pgip-askids 637,22100
+(defun pg-pgip-reset 650,22388
+(defconst pg-pgip-start-element-regexp 681,23086
+(defconst pg-pgip-end-element-regexp 682,23138
+
+generic/pg-response.el,1252
+(deflocal pg-response-eagerly-raise 32,788
+(define-derived-mode proof-response-mode 42,1013
+(define-key proof-response-mode-map 69,1950
+(define-key proof-response-mode-map 70,2021
+(define-key proof-response-mode-map 71,2075
+(defun proof-response-config-done 75,2161
+(defvar pg-response-special-display-regexp 86,2507
+(defconst proof-multiframe-parameters90,2674
+(defun proof-multiple-frames-enable 99,2964
+(defun proof-three-window-enable 109,3292
+(defun proof-select-three-b 112,3355
+(defun proof-display-three-b 127,3846
+(defvar pg-frame-configuration 138,4236
+(defun pg-cache-frame-configuration 142,4383
+(defun proof-layout-windows 146,4554
+(defun proof-delete-other-frames 186,6341
+(defvar pg-response-erase-flag 217,7429
+(defun pg-response-maybe-erase221,7558
+(defun pg-response-display 265,9021
+(defun pg-response-display-with-face 290,9804
+(defun pg-response-clear-displays 318,10650
+(defun pg-response-message 336,11356
+(defun pg-response-warning 342,11591
+(defun proof-next-error 357,11997
+(defun pg-response-has-error-location 435,14806
+(defcustom proof-trace-buffer-max-lines 450,15225
+(defun proof-trace-buffer-display 457,15460
+(defun proof-trace-buffer-finish 471,15867
+(defun pg-thms-buffer-clear 495,16520
+
+generic/pg-user.el,3603
+(defun proof-script-new-command-advance 43,1232
+(defun proof-maybe-follow-locked-end 67,2157
+(defun proof-goto-command-start 93,2993
+(defun proof-goto-command-end 116,3940
+(defun proof-forward-command 131,4362
+(defun proof-backward-command 152,5083
+(defun proof-goto-point 163,5297
+(defun proof-assert-next-command-interactive 177,5731
+(defun proof-assert-until-point-interactive 189,6217
+(defun proof-process-buffer 196,6462
+(defun proof-undo-last-successful-command 214,6974
+(defun proof-undo-and-delete-last-successful-command 219,7136
+(defun proof-undo-last-successful-command-1 231,7655
+(defun proof-retract-buffer 248,8319
+(defun proof-retract-current-goal 257,8603
+(defun proof-mouse-goto-point 276,9123
+(defvar proof-minibuffer-history 291,9399
+(defun proof-minibuffer-cmd 294,9494
+(defun proof-frob-locked-end 333,10901
+(defmacro proof-if-setting-configured 369,12002
+(defmacro proof-define-assistant-command 377,12271
+(defmacro proof-define-assistant-command-witharg 390,12726
+(defun proof-issue-new-command 410,13548
+(defun proof-electric-terminator-enable 492,16028
+(defun proof-electric-terminator 500,16332
+(defun proof-add-completions 528,17302
+(defun proof-script-complete 551,18125
+(defun pg-copy-span-contents 565,18434
+(defun pg-numth-span-higher-or-lower 579,18858
+(defun pg-control-span-of 605,19604
+(defun pg-move-span-contents 611,19808
+(defun pg-fixup-children-spans 662,21926
+(defun pg-move-region-down 672,22183
+(defun pg-move-region-up 681,22476
+(defun pg-pos-for-event 695,22750
+(defun pg-span-for-event 701,22971
+(defun pg-span-context-menu 705,23115
+(defun pg-toggle-visibility 721,23632
+(defun pg-create-in-span-context-menu 730,23939
+(defun pg-span-undo 755,24967
+(defun pg-goals-buffers-hint 768,25205
+(defun pg-slow-fontify-tracing-hint 772,25423
+(defun pg-response-buffers-hint 776,25612
+(defun pg-jump-to-end-hint 788,26027
+(defun pg-processing-complete-hint 792,26156
+(defun pg-next-error-hint 809,26876
+(defun pg-hint 814,27028
+(defun pg-identifier-under-mouse-query 825,27377
+(defun pg-identifier-near-point-query 836,27701
+(defvar proof-query-identifier-history 865,28624
+(defun proof-query-identifier 868,28711
+(defun pg-identifier-query 879,29067
+(defun proof-imenu-enable 912,30258
+(defvar pg-input-ring 948,31561
+(defvar pg-input-ring-index 951,31618
+(defvar pg-stored-incomplete-input 954,31690
+(defun pg-previous-input 957,31793
+(defun pg-next-input 971,32256
+(defun pg-delete-input 976,32378
+(defun pg-get-old-input 989,32716
+(defun pg-restore-input 1003,33107
+(defun pg-search-start 1014,33397
+(defun pg-regexp-arg 1026,33889
+(defun pg-search-arg 1038,34337
+(defun pg-previous-matching-input-string-position 1052,34754
+(defun pg-previous-matching-input 1079,35919
+(defun pg-next-matching-input 1098,36769
+(defvar pg-matching-input-from-input-string 1106,37152
+(defun pg-previous-matching-input-from-input 1110,37266
+(defun pg-next-matching-input-from-input 1128,38031
+(defun pg-add-to-input-history 1139,38410
+(defun pg-remove-from-input-history 1151,38863
+(defun  pg-clear-input-ring 1162,39243
+(define-key proof-mode-map 1179,39713
+(define-key proof-mode-map 1180,39773
+(defun pg-protected-undo 1182,39845
+(defun pg-protected-undo-1 1212,41139
+(defun next-undo-elt 1243,42576
+(defvar proof-autosend-timer 1270,43532
+(deflocal proof-autosend-modified-tick 1272,43593
+(defun proof-autosend-enable 1276,43715
+(defun proof-autosend-delay 1290,44258
+(defun proof-autosend-loop 1294,44391
+(defun proof-autosend-loop-all 1308,44951
+(defun proof-autosend-loop-next 1332,45731
 
 generic/pg-vars.el,1500
-(defvar proof-assistant-cusgrp 22,341
-(defvar proof-assistant-internals-cusgrp 28,601
-(defvar proof-assistant 34,871
-(defvar proof-assistant-symbol 39,1094
-(defvar proof-mode-for-shell 52,1636
-(defvar proof-mode-for-response 57,1826
-(defvar proof-mode-for-goals 62,2052
-(defvar proof-mode-for-script 67,2241
-(defvar proof-ready-for-assistant-hook 72,2418
-(defvar proof-shell-busy 83,2706
-(defvar proof-shell-last-queuemode 101,3377
-(defvar proof-included-files-list 105,3532
-(defvar proof-script-buffer 127,4551
-(defvar proof-previous-script-buffer 130,4643
-(defvar proof-shell-buffer 134,4816
-(defvar proof-goals-buffer 137,4902
-(defvar proof-response-buffer 140,4957
-(defvar proof-trace-buffer 143,5018
-(defvar proof-thms-buffer 147,5172
-(defvar proof-shell-error-or-interrupt-seen 151,5327
-(defvar pg-response-next-error 156,5551
-(defvar proof-shell-proof-completed 159,5658
-(defvar proof-shell-silent 173,6043
-(defvar proof-shell-last-prompt 176,6131
-(defvar proof-shell-last-output 180,6301
-(defvar proof-shell-last-output-kind 184,6441
-(defvar proof-assistant-settings 204,7205
-(defvar pg-tracing-slow-mode 214,7719
-(defvar proof-nesting-depth 217,7808
-(defvar proof-last-theorem-dependencies 224,8043
-(defvar proof-autosend-running 228,8205
-(defvar proof-next-command-on-new-line 233,8404
-(defcustom proof-general-name 244,8638
-(defcustom proof-general-home-page249,8795
-(defcustom proof-unnamed-theorem-name255,8955
-(defcustom proof-universal-keys261,9139
-
-generic/pg-xml.el,1176
-(defalias 'pg-xml-error pg-xml-error
18,335
-(defun pg-xml-parse-string 41,977
-(defun pg-xml-parse-buffer 51,1289
-(defun pg-xml-get-attr 70,1904
-(defun pg-xml-child-elts 78,2206
-(defun pg-xml-child-elt 83,2411
-(defun pg-xml-get-child 91,2693
-(defun pg-xml-get-text-content 101,3060
-(defmacro pg-xml-attr 112,3410
-(defmacro pg-xml-node 114,3472
-(defconst pg-xml-header117,3564
-(defun pg-xml-string-of 121,3640
-(defun pg-xml-output-internal 132,4007
-(defun pg-xml-cdata 166,5146
-(defsubst pg-pgip-get-area 174,5339
-(defun pg-pgip-get-icon 177,5456
-(defsubst pg-pgip-get-name 181,5604
-(defsubst pg-pgip-get-version 184,5721
-(defsubst pg-pgip-get-descr 187,5844
-(defsubst pg-pgip-get-thmname 190,5963
-(defsubst pg-pgip-get-thyname 193,6086
-(defsubst pg-pgip-get-url 196,6209
-(defsubst pg-pgip-get-srcid 199,6324
-(defsubst pg-pgip-get-proverid 202,6443
-(defsubst pg-pgip-get-symname 205,6568
-(defsubst pg-pgip-get-prefcat 208,6688
-(defsubst pg-pgip-get-default 211,6816
-(defsubst pg-pgip-get-objtype 214,6939
-(defsubst pg-pgip-get-value 217,7062
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7132
-(defun pg-pgip-get-pgmltext 222,7191
+(defvar proof-assistant-cusgrp 22,388
+(defvar proof-assistant-internals-cusgrp 28,648
+(defvar proof-assistant 34,918
+(defvar proof-assistant-symbol 39,1141
+(defvar proof-mode-for-shell 52,1683
+(defvar proof-mode-for-response 57,1873
+(defvar proof-mode-for-goals 62,2099
+(defvar proof-mode-for-script 67,2288
+(defvar proof-ready-for-assistant-hook 72,2465
+(defvar proof-shell-busy 83,2753
+(defvar proof-shell-last-queuemode 104,3534
+(defvar proof-included-files-list 108,3689
+(defvar proof-script-buffer 130,4708
+(defvar proof-previous-script-buffer 133,4800
+(defvar proof-shell-buffer 137,4973
+(defvar proof-goals-buffer 140,5059
+(defvar proof-response-buffer 143,5114
+(defvar proof-trace-buffer 146,5175
+(defvar proof-thms-buffer 150,5329
+(defvar proof-shell-error-or-interrupt-seen 154,5484
+(defvar pg-response-next-error 159,5708
+(defvar proof-shell-proof-completed 162,5815
+(defvar proof-shell-silent 176,6200
+(defvar proof-shell-last-prompt 179,6288
+(defvar proof-shell-last-output 183,6458
+(defvar proof-shell-last-output-kind 187,6598
+(defvar proof-assistant-settings 207,7362
+(defvar pg-tracing-slow-mode 217,7876
+(defvar proof-nesting-depth 220,7965
+(defvar proof-last-theorem-dependencies 227,8200
+(defvar proof-autosend-running 231,8362
+(defvar proof-next-command-on-new-line 236,8561
+(defcustom proof-general-name 247,8795
+(defcustom proof-general-home-page252,8952
+(defcustom proof-unnamed-theorem-name258,9112
+(defcustom proof-universal-keys264,9296
+
+generic/pg-xml.el,1177
+(defalias 'pg-xml-error pg-xml-error
18,381
+(defun pg-xml-parse-string 41,1023
+(defun pg-xml-parse-buffer 51,1335
+(defun pg-xml-get-attr 70,1950
+(defun pg-xml-child-elts 78,2252
+(defun pg-xml-child-elt 83,2457
+(defun pg-xml-get-child 91,2739
+(defun pg-xml-get-text-content 101,3106
+(defmacro pg-xml-attr 112,3456
+(defmacro pg-xml-node 114,3518
+(defconst pg-xml-header117,3610
+(defun pg-xml-string-of 121,3686
+(defun pg-xml-output-internal 132,4053
+(defun pg-xml-cdata 166,5192
+(defsubst pg-pgip-get-area 174,5385
+(defun pg-pgip-get-icon 177,5502
+(defsubst pg-pgip-get-name 181,5650
+(defsubst pg-pgip-get-version 184,5767
+(defsubst pg-pgip-get-descr 187,5890
+(defsubst pg-pgip-get-thmname 190,6009
+(defsubst pg-pgip-get-thyname 193,6132
+(defsubst pg-pgip-get-url 196,6255
+(defsubst pg-pgip-get-srcid 199,6370
+(defsubst pg-pgip-get-proverid 202,6489
+(defsubst pg-pgip-get-symname 205,6614
+(defsubst pg-pgip-get-prefcat 208,6734
+(defsubst pg-pgip-get-default 211,6862
+(defsubst pg-pgip-get-objtype 214,6985
+(defsubst pg-pgip-get-value 217,7108
+(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7178
+(defun pg-pgip-get-pgmltext 222,7237
 
 generic/proof-autoloads.el,97
 (defsubst proof-shell-live-buffer 727,23601
@@ -1286,1562 +1332,1573 @@ generic/proof-auxmodes.el,149
 (defun proof-unicode-tokens-support-available 58,1531
 
 generic/proof-config.el,7845
-(defgroup prover-config 80,2580
-(defcustom proof-guess-command-line 98,3430
-(defcustom proof-assistant-home-page 113,3925
-(defcustom proof-context-command 119,4095
-(defcustom proof-info-command 124,4229
-(defcustom proof-showproof-command 131,4500
-(defcustom proof-goal-command 136,4636
-(defcustom proof-save-command 144,4933
-(defcustom proof-find-theorems-command 152,5242
-(defcustom proof-query-identifier-command 159,5550
-(defcustom proof-assistant-true-value 173,6239
-(defcustom proof-assistant-false-value 179,6429
-(defcustom proof-assistant-format-int-fn 185,6623
-(defcustom proof-assistant-format-float-fn 192,6872
-(defcustom proof-assistant-format-string-fn 199,7127
-(defcustom proof-assistant-setting-format 206,7394
-(defcustom proof-tree-configured 216,7877
-(defgroup proof-script 234,8343
-(defcustom proof-terminal-string 239,8473
-(defcustom proof-electric-terminator-noterminator 249,8861
-(defcustom proof-script-sexp-commands 254,9033
-(defcustom proof-script-command-end-regexp 265,9492
-(defcustom proof-script-command-start-regexp 283,10313
-(defcustom proof-script-integral-proofs 294,10776
-(defcustom proof-script-fly-past-comments 309,11432
-(defcustom proof-script-parse-function 314,11603
-(defcustom proof-script-comment-start 332,12248
-(defcustom proof-script-comment-start-regexp 343,12685
-(defcustom proof-script-comment-end 351,13004
-(defcustom proof-script-comment-end-regexp 363,13426
-(defcustom proof-string-start-regexp 371,13739
-(defcustom proof-string-end-regexp 376,13904
-(defcustom proof-case-fold-search 381,14065
-(defcustom proof-save-command-regexp 390,14477
-(defcustom proof-save-with-hole-regexp 395,14587
-(defcustom proof-save-with-hole-result 406,14962
-(defcustom proof-goal-command-regexp 416,15406
-(defcustom proof-goal-with-hole-regexp 424,15693
-(defcustom proof-goal-with-hole-result 436,16136
-(defcustom proof-non-undoables-regexp 445,16514
-(defcustom proof-nested-undo-regexp 456,16977
-(defcustom proof-ignore-for-undo-count 472,17697
-(defcustom proof-script-imenu-generic-expression 480,18008
-(defcustom proof-goal-command-p 488,18347
-(defcustom proof-really-save-command-p 499,18838
-(defcustom proof-completed-proof-behaviour 508,19145
-(defcustom proof-count-undos-fn 536,20494
-(defcustom proof-find-and-forget-fn 548,21045
-(defcustom proof-forget-id-command 565,21754
-(defcustom pg-topterm-goalhyplit-fn 575,22112
-(defcustom proof-kill-goal-command 587,22655
-(defcustom proof-undo-n-times-cmd 601,23159
-(defcustom proof-nested-goals-history-p 615,23696
-(defcustom proof-arbitrary-undo-positions 624,24033
-(defcustom proof-state-preserving-p 638,24614
-(defcustom proof-activate-scripting-hook 648,25086
-(defcustom proof-deactivate-scripting-hook 667,25867
-(defcustom proof-no-fully-processed-buffer 676,26197
-(defcustom proof-script-evaluate-elisp-comment-regexp 687,26695
-(defcustom proof-indent 705,27281
-(defcustom proof-indent-hang 710,27388
-(defcustom proof-indent-enclose-offset 715,27514
-(defcustom proof-indent-open-offset 720,27656
-(defcustom proof-indent-close-offset 725,27793
-(defcustom proof-indent-any-regexp 730,27931
-(defcustom proof-indent-inner-regexp 735,28091
-(defcustom proof-indent-enclose-regexp 740,28245
-(defcustom proof-indent-open-regexp 745,28399
-(defcustom proof-indent-close-regexp 750,28551
-(defcustom proof-script-font-lock-keywords 756,28705
-(defcustom proof-script-syntax-table-entries 764,29057
-(defcustom proof-script-span-context-menu-extensions 782,29453
-(defgroup proof-shell 808,30213
-(defcustom proof-prog-name 818,30383
-(defcustom proof-shell-auto-terminate-commands 830,30850
-(defcustom proof-shell-pre-sync-init-cmd 839,31255
-(defcustom proof-shell-init-cmd 853,31813
-(defcustom proof-shell-init-hook 865,32359
-(defcustom proof-shell-restart-cmd 870,32498
-(defcustom proof-shell-quit-cmd 875,32653
-(defcustom proof-shell-cd-cmd 880,32820
-(defcustom proof-shell-start-silent-cmd 897,33491
-(defcustom proof-shell-stop-silent-cmd 906,33867
-(defcustom proof-shell-silent-threshold 915,34202
-(defcustom  proof-shell-inform-file-processed-cmd 923,34536
-(defcustom  proof-shell-inform-file-retracted-cmd 944,35464
-(defcustom proof-auto-multiple-files 972,36736
-(defcustom proof-cannot-reopen-processed-files 987,37457
-(defcustom proof-shell-annotated-prompt-regexp 1007,38248
-(defcustom proof-shell-error-regexp 1022,38813
-(defcustom proof-shell-truncate-before-error 1042,39623
-(defcustom pg-next-error-regexp 1056,40162
-(defcustom pg-next-error-filename-regexp 1071,40771
-(defcustom pg-next-error-extract-filename 1095,41804
-(defcustom proof-shell-interrupt-regexp 1102,42047
-(defcustom proof-shell-proof-completed-regexp 1116,42650
-(defcustom proof-shell-clear-response-regexp 1129,43166
-(defcustom proof-shell-clear-goals-regexp 1141,43626
-(defcustom proof-shell-start-goals-regexp 1153,44080
-(defcustom proof-shell-end-goals-regexp 1162,44512
-(defcustom proof-shell-eager-annotation-start 1176,45093
-(defcustom proof-shell-eager-annotation-start-length 1199,46112
-(defcustom proof-shell-eager-annotation-end 1210,46538
-(defcustom proof-shell-strip-output-markup 1226,47213
-(defcustom proof-shell-assumption-regexp 1235,47598
-(defcustom proof-shell-process-file 1245,48002
-(defcustom proof-shell-retract-files-regexp 1271,49078
-(defcustom proof-shell-compute-new-files-list 1284,49566
-(defcustom pg-special-char-regexp 1299,50133
-(defcustom proof-shell-set-elisp-variable-regexp 1304,50277
-(defcustom proof-shell-match-pgip-cmd 1342,51951
-(defcustom proof-shell-issue-pgip-cmd 1356,52441
-(defcustom proof-use-pgip-askprefs 1361,52614
-(defcustom proof-shell-query-dependencies-cmd 1369,52961
-(defcustom proof-shell-theorem-dependency-list-regexp 1376,53221
-(defcustom proof-shell-theorem-dependency-list-split 1392,53889
-(defcustom proof-shell-show-dependency-cmd 1401,54320
-(defcustom proof-shell-trace-output-regexp 1423,55226
-(defcustom proof-shell-thms-output-regexp 1441,55828
-(defcustom proof-shell-interactive-prompt-regexp 1449,56162
-(defcustom proof-tokens-activate-command 1468,56815
-(defcustom proof-tokens-deactivate-command 1475,57055
-(defcustom proof-tokens-extra-modes 1482,57300
-(defcustom proof-shell-unicode 1497,57805
-(defcustom proof-shell-filename-escapes 1506,58195
-(defcustom proof-shell-process-connection-type 1523,58875
-(defcustom proof-shell-strip-crs-from-input 1529,59066
-(defcustom proof-shell-strip-crs-from-output 1541,59549
-(defcustom proof-shell-extend-queue-hook 1549,59917
-(defcustom proof-shell-insert-hook 1559,60347
-(defcustom proof-script-preprocess 1602,62445
-(defcustom proof-shell-handle-delayed-output-hook1608,62596
-(defcustom proof-shell-handle-error-or-interrupt-hook1614,62811
-(defcustom proof-shell-pre-interrupt-hook1632,63557
-(defcustom proof-shell-handle-output-system-specific 1640,63828
-(defcustom proof-state-change-hook 1663,64801
-(defcustom proof-shell-syntax-table-entries 1673,65194
-(defgroup proof-goals 1691,65565
-(defcustom pg-subterm-first-special-char 1696,65686
-(defcustom pg-subterm-anns-use-stack 1704,65998
-(defcustom pg-goals-change-goal 1713,66297
-(defcustom pbp-goal-command 1718,66413
-(defcustom pbp-hyp-command 1723,66577
-(defcustom pg-subterm-help-cmd 1728,66747
-(defcustom pg-goals-error-regexp 1735,66991
-(defcustom proof-shell-result-start 1740,67159
-(defcustom proof-shell-result-end 1746,67401
-(defcustom pg-subterm-start-char 1752,67614
-(defcustom pg-subterm-sep-char 1763,68088
-(defcustom pg-subterm-end-char 1769,68267
-(defcustom pg-topterm-regexp 1775,68424
-(defcustom proof-goals-font-lock-keywords 1790,69024
-(defcustom proof-response-font-lock-keywords 1798,69383
-(defcustom proof-shell-font-lock-keywords 1806,69745
-(defcustom pg-before-fontify-output-hook 1817,70259
-(defcustom pg-after-fontify-output-hook 1825,70620
+(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 829,30901
+(defcustom proof-shell-pre-sync-init-cmd 838,31306
+(defcustom proof-shell-init-cmd 853,31894
+(defcustom proof-shell-init-hook 866,32489
+(defcustom proof-shell-restart-cmd 871,32628
+(defcustom proof-shell-quit-cmd 876,32783
+(defcustom proof-shell-cd-cmd 881,32950
+(defcustom proof-shell-start-silent-cmd 898,33621
+(defcustom proof-shell-stop-silent-cmd 907,33997
+(defcustom proof-shell-silent-threshold 916,34332
+(defcustom  proof-shell-inform-file-processed-cmd 924,34666
+(defcustom  proof-shell-inform-file-retracted-cmd 945,35594
+(defcustom proof-auto-multiple-files 973,36866
+(defcustom proof-cannot-reopen-processed-files 988,37587
+(defcustom proof-shell-annotated-prompt-regexp 1008,38378
+(defcustom proof-shell-error-regexp 1023,38943
+(defcustom proof-shell-truncate-before-error 1043,39753
+(defcustom pg-next-error-regexp 1057,40292
+(defcustom pg-next-error-filename-regexp 1072,40901
+(defcustom pg-next-error-extract-filename 1096,41934
+(defcustom proof-shell-interrupt-regexp 1103,42177
+(defcustom proof-shell-proof-completed-regexp 1117,42780
+(defcustom proof-shell-clear-response-regexp 1130,43296
+(defcustom proof-shell-clear-goals-regexp 1142,43756
+(defcustom proof-shell-start-goals-regexp 1154,44210
+(defcustom proof-shell-end-goals-regexp 1167,44785
+(defcustom proof-shell-eager-annotation-start 1181,45375
+(defcustom proof-shell-eager-annotation-start-length 1204,46394
+(defcustom proof-shell-eager-annotation-end 1215,46820
+(defcustom proof-shell-strip-output-markup 1231,47495
+(defcustom proof-shell-assumption-regexp 1240,47880
+(defcustom proof-shell-process-file 1250,48284
+(defcustom proof-shell-retract-files-regexp 1276,49360
+(defcustom proof-shell-compute-new-files-list 1289,49848
+(defcustom pg-special-char-regexp 1304,50415
+(defcustom proof-shell-set-elisp-variable-regexp 1309,50559
+(defcustom proof-shell-match-pgip-cmd 1347,52233
+(defcustom proof-shell-issue-pgip-cmd 1361,52723
+(defcustom proof-use-pgip-askprefs 1366,52896
+(defcustom proof-shell-query-dependencies-cmd 1374,53243
+(defcustom proof-shell-theorem-dependency-list-regexp 1381,53503
+(defcustom proof-shell-theorem-dependency-list-split 1397,54171
+(defcustom proof-shell-show-dependency-cmd 1406,54602
+(defcustom proof-shell-trace-output-regexp 1428,55508
+(defcustom proof-shell-thms-output-regexp 1446,56110
+(defcustom proof-shell-interactive-prompt-regexp 1454,56444
+(defcustom proof-tokens-activate-command 1473,57097
+(defcustom proof-tokens-deactivate-command 1480,57337
+(defcustom proof-tokens-extra-modes 1487,57582
+(defcustom proof-shell-unicode 1502,58087
+(defcustom proof-shell-filename-escapes 1511,58477
+(defcustom proof-shell-process-connection-type 1528,59157
+(defcustom proof-shell-strip-crs-from-input 1534,59348
+(defcustom proof-shell-strip-crs-from-output 1546,59831
+(defcustom proof-shell-extend-queue-hook 1554,60199
+(defcustom proof-shell-insert-hook 1564,60629
+(defcustom proof-script-preprocess 1607,62718
+(defcustom proof-shell-handle-delayed-output-hook1613,62869
+(defcustom proof-shell-handle-error-or-interrupt-hook1619,63084
+(defcustom proof-shell-pre-interrupt-hook1637,63830
+(defcustom proof-shell-handle-output-system-specific 1645,64101
+(defcustom proof-state-change-hook 1668,65074
+(defcustom proof-shell-syntax-table-entries 1678,65467
+(defgroup proof-goals 1696,65838
+(defcustom pg-subterm-first-special-char 1701,65959
+(defcustom pg-subterm-anns-use-stack 1709,66271
+(defcustom pg-goals-change-goal 1718,66570
+(defcustom pbp-goal-command 1723,66686
+(defcustom pbp-hyp-command 1728,66850
+(defcustom pg-subterm-help-cmd 1733,67020
+(defcustom pg-goals-error-regexp 1740,67264
+(defcustom proof-shell-result-start 1745,67432
+(defcustom proof-shell-result-end 1751,67674
+(defcustom pg-subterm-start-char 1757,67887
+(defcustom pg-subterm-sep-char 1768,68361
+(defcustom pg-subterm-end-char 1774,68540
+(defcustom pg-topterm-regexp 1780,68697
+(defcustom proof-goals-font-lock-keywords 1795,69297
+(defcustom proof-response-font-lock-keywords 1803,69656
+(defcustom proof-shell-font-lock-keywords 1811,70018
+(defcustom pg-before-fontify-output-hook 1822,70532
+(defcustom pg-after-fontify-output-hook 1830,70893
 
 generic/proof-depends.el,917
-(defvar proof-thm-names-of-files 25,586
-(defvar proof-def-names-of-files 31,870
-(defun proof-depends-module-name-for-buffer 42,1185
-(defun proof-depends-module-of 52,1626
-(defun proof-depends-names-in-same-file 60,1917
-(defun proof-depends-process-dependencies 79,2525
-(defun proof-dependency-in-span-context-menu 132,4260
-(defun proof-dep-alldeps-menu 155,5150
-(defun proof-dep-make-alldeps-menu 161,5376
-(defun proof-dep-split-deps 179,5871
-(defun proof-dep-make-submenu 198,6537
-(defun proof-make-highlight-depts-menu 209,6948
-(defun proof-goto-dependency 220,7256
-(defun proof-show-dependency 227,7508
-(defconst pg-dep-span-priority 234,7797
-(defconst pg-ordinary-span-priority 235,7833
-(defun proof-highlight-depcs 237,7875
-(defun proof-highlight-depts 248,8341
-(defun proof-depends-save-old-face 260,8851
-(defun proof-depends-restore-old-face 265,9028
-(defun proof-dep-unhighlight 271,9257
-
-generic/proof-easy-config.el,192
-(defconst proof-easy-config-derived-modes-table16,487
-(defun proof-easy-config-define-derived-modes 23,893
-(defun proof-easy-config-check-setup 52,2078
-(defmacro proof-easy-config 84,3408
+(defvar proof-thm-names-of-files 25,639
+(defvar proof-def-names-of-files 31,923
+(defun proof-depends-module-name-for-buffer 42,1238
+(defun proof-depends-module-of 52,1679
+(defun proof-depends-names-in-same-file 60,1970
+(defun proof-depends-process-dependencies 79,2578
+(defun proof-dependency-in-span-context-menu 132,4313
+(defun proof-dep-alldeps-menu 155,5203
+(defun proof-dep-make-alldeps-menu 161,5429
+(defun proof-dep-split-deps 179,5924
+(defun proof-dep-make-submenu 198,6590
+(defun proof-make-highlight-depts-menu 209,7001
+(defun proof-goto-dependency 220,7309
+(defun proof-show-dependency 227,7561
+(defconst pg-dep-span-priority 234,7850
+(defconst pg-ordinary-span-priority 235,7886
+(defun proof-highlight-depcs 237,7928
+(defun proof-highlight-depts 248,8394
+(defun proof-depends-save-old-face 260,8904
+(defun proof-depends-restore-old-face 265,9081
+(defun proof-dep-unhighlight 271,9310
+
+generic/proof-easy-config.el,193
+(defconst proof-easy-config-derived-modes-table17,605
+(defun proof-easy-config-define-derived-modes 24,1011
+(defun proof-easy-config-check-setup 53,2196
+(defmacro proof-easy-config 85,3526
 
 generic/proof-faces.el,1809
-(defgroup proof-faces 29,758
-(defconst pg-defface-window-systems36,938
-(defmacro proof-face-specs 49,1500
-(defface proof-queue-face64,1952
-(defface proof-locked-face72,2230
-(defface proof-declaration-name-face82,2551
-(defface proof-tacticals-name-face91,2837
-(defface proof-tactics-name-face100,3099
-(defface proof-error-face109,3364
-(defface proof-warning-face117,3585
-(defface proof-eager-annotation-face126,3842
-(defface proof-debug-message-face134,4060
-(defface proof-boring-face142,4259
-(defface proof-mouse-highlight-face150,4451
-(defface proof-command-mouse-highlight-face158,4669
-(defface proof-region-mouse-highlight-face166,4908
-(defface proof-highlight-dependent-face174,5150
-(defface proof-highlight-dependency-face182,5357
-(defface proof-active-area-face190,5554
-(defface proof-script-sticky-error-face198,5866
-(defface proof-script-highlight-error-face206,6095
-(defconst proof-face-compat-doc 218,6440
-(defconst proof-queue-face 219,6520
-(defconst proof-locked-face 220,6588
-(defconst proof-declaration-name-face 221,6658
-(defconst proof-tacticals-name-face 222,6748
-(defconst proof-tactics-name-face 223,6834
-(defconst proof-error-face 224,6916
-(defconst proof-script-sticky-error-face 225,6984
-(defconst proof-script-highlight-error-face 226,7080
-(defconst proof-warning-face 227,7182
-(defconst proof-eager-annotation-face 228,7254
-(defconst proof-debug-message-face 229,7344
-(defconst proof-boring-face 230,7428
-(defconst proof-mouse-highlight-face 231,7498
-(defconst proof-command-mouse-highlight-face 232,7586
-(defconst proof-region-mouse-highlight-face 233,7690
-(defconst proof-highlight-dependent-face 234,7792
-(defconst proof-highlight-dependency-face 235,7888
-(defconst proof-active-area-face 236,7986
-(defconst proof-script-error-face 237,8066
+(defgroup proof-faces 29,809
+(defconst pg-defface-window-systems36,989
+(defmacro proof-face-specs 49,1551
+(defface proof-queue-face64,2003
+(defface proof-locked-face72,2281
+(defface proof-declaration-name-face82,2602
+(defface proof-tacticals-name-face91,2888
+(defface proof-tactics-name-face100,3150
+(defface proof-error-face109,3415
+(defface proof-warning-face117,3636
+(defface proof-eager-annotation-face126,3893
+(defface proof-debug-message-face134,4111
+(defface proof-boring-face142,4310
+(defface proof-mouse-highlight-face150,4502
+(defface proof-command-mouse-highlight-face158,4720
+(defface proof-region-mouse-highlight-face166,4959
+(defface proof-highlight-dependent-face174,5201
+(defface proof-highlight-dependency-face182,5408
+(defface proof-active-area-face190,5605
+(defface proof-script-sticky-error-face198,5917
+(defface proof-script-highlight-error-face206,6146
+(defconst proof-face-compat-doc 218,6491
+(defconst proof-queue-face 219,6571
+(defconst proof-locked-face 220,6639
+(defconst proof-declaration-name-face 221,6709
+(defconst proof-tacticals-name-face 222,6799
+(defconst proof-tactics-name-face 223,6885
+(defconst proof-error-face 224,6967
+(defconst proof-script-sticky-error-face 225,7035
+(defconst proof-script-highlight-error-face 226,7131
+(defconst proof-warning-face 227,7233
+(defconst proof-eager-annotation-face 228,7305
+(defconst proof-debug-message-face 229,7395
+(defconst proof-boring-face 230,7479
+(defconst proof-mouse-highlight-face 231,7549
+(defconst proof-command-mouse-highlight-face 232,7637
+(defconst proof-region-mouse-highlight-face 233,7741
+(defconst proof-highlight-dependent-face 234,7843
+(defconst proof-highlight-dependency-face 235,7939
+(defconst proof-active-area-face 236,8037
+(defconst proof-script-error-face 237,8117
 
 generic/proof-indent.el,219
-(defun proof-indent-indent 19,397
-(defun proof-indent-offset 28,663
-(defun proof-indent-inner-p 45,1264
-(defun proof-indent-goto-prev 54,1564
-(defun proof-indent-calculate 61,1897
-(defun proof-indent-line 82,2656
+(defun proof-indent-indent 19,449
+(defun proof-indent-offset 28,715
+(defun proof-indent-inner-p 45,1316
+(defun proof-indent-goto-prev 54,1616
+(defun proof-indent-calculate 61,1949
+(defun proof-indent-line 82,2708
 
 generic/proof-maths-menu.el,83
-(defun proof-maths-menu-set-global 32,850
-(defun proof-maths-menu-enable 46,1301
+(defun proof-maths-menu-set-global 32,906
+(defun proof-maths-menu-enable 46,1357
 
 generic/proof-menu.el,2215
-(defvar proof-display-some-buffers-count 36,770
-(defun proof-display-some-buffers 38,815
-(defun proof-menu-define-keys 95,2956
-(defun proof-menu-define-main 154,5862
-(defvar proof-menu-favourites 163,6047
-(defvar proof-menu-settings 166,6154
-(defun proof-menu-define-specific 170,6243
-(defun proof-assistant-menu-update 213,7505
-(defvar proof-help-menu227,7938
-(defvar proof-show-hide-menu235,8202
-(defvar proof-buffer-menu246,8626
-(defun proof-keep-response-history 310,10982
-(defconst proof-quick-opts-menu318,11292
-(defun proof-quick-opts-vars 540,20359
-(defun proof-quick-opts-changed-from-defaults-p 572,21299
-(defun proof-quick-opts-changed-from-saved-p 576,21404
-(defun proof-set-document-centred 584,21560
-(defun proof-set-non-document-centred 597,21986
-(defun proof-quick-opts-save 616,22697
-(defun proof-quick-opts-reset 621,22865
-(defconst proof-config-menu633,23133
-(defconst proof-advanced-menu640,23312
-(defvar proof-menu658,23996
-(defun proof-main-menu 667,24278
-(defun proof-aux-menu 679,24617
-(defun proof-menu-define-favourites-menu 695,24963
-(defun proof-def-favourite 715,25612
-(defvar proof-make-favourite-cmd-history 742,26605
-(defvar proof-make-favourite-menu-history 745,26690
-(defun proof-save-favourites 748,26776
-(defun proof-del-favourite 753,26924
-(defun proof-read-favourite 770,27480
-(defun proof-add-favourite 794,28254
-(defun proof-menu-define-settings-menu 821,29299
-(defun proof-menu-entry-name 850,30291
-(defun proof-menu-entry-for-setting 860,30641
-(defun proof-settings-vars 883,31279
-(defun proof-settings-changed-from-defaults-p 888,31456
-(defun proof-settings-changed-from-saved-p 892,31562
-(defun proof-settings-save 896,31665
-(defun proof-settings-reset 901,31832
-(defun proof-assistant-invisible-command-ifposs 906,31995
-(defun proof-maybe-askprefs 928,32965
-(defun proof-assistant-settings-cmd 944,33582
-(defun proof-assistant-settings-cmds 952,33865
-(defvar proof-assistant-format-table967,34307
-(defun proof-assistant-format-bool 976,34733
-(defun proof-assistant-format-int 979,34846
-(defun proof-assistant-format-float 982,34938
-(defun proof-assistant-format-string 985,35034
-(defun proof-assistant-format 988,35132
+(defvar proof-display-some-buffers-count 36,822
+(defun proof-display-some-buffers 38,867
+(defun proof-menu-define-keys 95,3008
+(defun proof-menu-define-main 154,5914
+(defvar proof-menu-favourites 163,6099
+(defvar proof-menu-settings 166,6206
+(defun proof-menu-define-specific 170,6295
+(defun proof-assistant-menu-update 213,7557
+(defvar proof-help-menu227,7990
+(defvar proof-show-hide-menu235,8254
+(defvar proof-buffer-menu246,8678
+(defun proof-keep-response-history 310,11034
+(defconst proof-quick-opts-menu318,11344
+(defun proof-quick-opts-vars 540,20411
+(defun proof-quick-opts-changed-from-defaults-p 572,21351
+(defun proof-quick-opts-changed-from-saved-p 576,21456
+(defun proof-set-document-centred 584,21612
+(defun proof-set-non-document-centred 597,22038
+(defun proof-quick-opts-save 616,22749
+(defun proof-quick-opts-reset 621,22917
+(defconst proof-config-menu633,23185
+(defconst proof-advanced-menu640,23364
+(defvar proof-menu658,24048
+(defun proof-main-menu 667,24330
+(defun proof-aux-menu 679,24669
+(defun proof-menu-define-favourites-menu 695,25015
+(defun proof-def-favourite 715,25664
+(defvar proof-make-favourite-cmd-history 742,26657
+(defvar proof-make-favourite-menu-history 745,26742
+(defun proof-save-favourites 748,26828
+(defun proof-del-favourite 753,26976
+(defun proof-read-favourite 770,27532
+(defun proof-add-favourite 794,28306
+(defun proof-menu-define-settings-menu 821,29351
+(defun proof-menu-entry-name 850,30343
+(defun proof-menu-entry-for-setting 860,30693
+(defun proof-settings-vars 883,31331
+(defun proof-settings-changed-from-defaults-p 888,31508
+(defun proof-settings-changed-from-saved-p 892,31614
+(defun proof-settings-save 896,31717
+(defun proof-settings-reset 901,31884
+(defun proof-assistant-invisible-command-ifposs 906,32047
+(defun proof-maybe-askprefs 928,33021
+(defun proof-assistant-settings-cmd 944,33638
+(defun proof-assistant-settings-cmds 952,33921
+(defvar proof-assistant-format-table967,34363
+(defun proof-assistant-format-bool 976,34789
+(defun proof-assistant-format-int 979,34902
+(defun proof-assistant-format-float 982,34994
+(defun proof-assistant-format-string 985,35090
+(defun proof-assistant-format 988,35188
 
 generic/proof-mmm.el,70
-(defun proof-mmm-set-global 43,1390
-(defun proof-mmm-enable 58,1929
+(defun proof-mmm-set-global 43,1439
+(defun proof-mmm-enable 58,1978
 
 generic/proof-script.el,5813
-(deflocal proof-active-buffer-fake-minor-mode 46,1361
-(deflocal proof-script-buffer-file-name 49,1487
-(deflocal pg-script-portions 56,1897
-(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode
59,2003
-(defun proof-next-element-count 68,2198
-(defun proof-element-id 74,2440
-(defun proof-next-element-id 78,2609
-(deflocal proof-locked-span 114,3913
-(deflocal proof-queue-span 121,4179
-(deflocal proof-overlay-arrow 130,4665
-(defun proof-span-give-warning 136,4792
-(defun proof-span-read-only 142,4972
-(defun proof-strict-read-only 151,5345
-(defsubst proof-set-queue-endpoints 161,5723
-(defun proof-set-overlay-arrow 165,5864
-(defsubst proof-set-locked-endpoints 176,6202
-(defsubst proof-detach-queue 181,6378
-(defsubst proof-detach-locked 186,6517
-(defsubst proof-set-queue-start 193,6742
-(defsubst proof-set-locked-end 197,6868
-(defsubst proof-set-queue-end 209,7338
-(defun proof-init-segmentation 220,7635
-(defun proof-colour-locked 250,8886
-(defun proof-colour-locked-span 257,9159
-(defun proof-sticky-errors 263,9432
-(defun proof-restart-buffers 276,9848
-(defun proof-script-buffers-with-spans 300,10781
-(defun proof-script-remove-all-spans-and-deactivate 310,11137
-(defun proof-script-clear-queue-spans-on-error 314,11327
-(defun proof-script-delete-spans 340,12344
-(defun proof-script-delete-secondary-spans 345,12543
-(defun proof-unprocessed-begin 358,12832
-(defun proof-script-end 366,13086
-(defun proof-queue-or-locked-end 375,13396
-(defun proof-locked-region-full-p 394,13989
-(defun proof-locked-region-empty-p 403,14261
-(defun proof-only-whitespace-to-locked-region-p 407,14411
-(defun proof-in-locked-region-p 417,14760
-(defun proof-goto-end-of-locked 429,15017
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15804
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16285
-(defun proof-end-of-locked-visible-p 469,16825
-(defconst pg-idioms 488,17418
-(defconst pg-all-idioms 491,17514
-(defun pg-clear-script-portions 495,17635
-(defun pg-remove-element 501,17870
-(defun pg-get-element 509,18173
-(defun pg-add-element 519,18488
-(defun pg-invisible-prop 567,20450
-(defun pg-set-element-span-invisible 572,20651
-(defun pg-toggle-element-span-visibility 585,21217
-(defun pg-open-invisible-span 590,21378
-(defun pg-make-element-invisible 595,21549
-(defun pg-make-element-visible 600,21760
-(defun pg-toggle-element-visibility 605,21954
-(defun pg-show-all-portions 611,22217
-(defun pg-show-all-proofs 633,22961
-(defun pg-hide-all-proofs 638,23089
-(defun pg-add-proof-element 643,23220
-(defun pg-span-name 658,24007
-(defvar pg-span-context-menu-keymap691,25214
-(defun pg-last-output-displayform 698,25452
-(defun pg-set-span-helphighlights 721,26343
-(defun proof-complete-buffer-atomic 784,28490
-(defun proof-register-possibly-new-processed-file813,29760
-(defun proof-query-save-this-buffer-p 859,31634
-(defun proof-inform-prover-file-retracted 864,31859
-(defun proof-auto-retract-dependencies 884,32710
-(defun proof-unregister-buffer-file-name 938,35260
-(defsubst proof-action-completed 984,37085
-(defun proof-protected-process-or-retract 988,37255
-(defun proof-deactivate-scripting-auto 1016,38486
-(defun proof-deactivate-scripting-query-user-action 1025,38844
-(defun proof-deactivate-scripting-choose-action 1069,40353
-(defun proof-deactivate-scripting 1081,40738
-(defun proof-activate-scripting 1178,44861
-(defun proof-toggle-active-scripting 1278,49400
-(defun proof-done-advancing 1317,50645
-(defun proof-done-advancing-comment 1385,53142
-(defun proof-done-advancing-save 1419,54528
-(defun proof-make-goalsave1507,57892
-(defun proof-get-name-from-goal 1525,58757
-(defun proof-done-advancing-autosave 1545,59782
-(defun proof-done-advancing-other 1609,62278
-(defun proof-segment-up-to-parser 1638,63242
-(defun proof-script-generic-parse-find-comment-end 1708,65523
-(defun proof-script-generic-parse-cmdend 1717,65937
-(defun proof-script-generic-parse-cmdstart 1768,67833
-(defun proof-script-generic-parse-sexp 1807,69433
-(defun proof-semis-to-vanillas 1819,69899
-(defun proof-next-command-new-line 1872,71572
-(defun proof-script-next-command-advance 1877,71778
-(defun proof-assert-until-point 1896,72278
-(defun proof-assert-electric-terminator 1912,72949
-(defun proof-assert-semis 1956,74629
-(defun proof-retract-before-change 1970,75390
-(defun proof-insert-pbp-command 1993,76046
-(defun proof-insert-sendback-command 2008,76549
-(defun proof-done-retracting 2034,77452
-(defun proof-setup-retract-action 2069,78906
-(defun proof-last-goal-or-goalsave 2081,79511
-(defun proof-retract-target 2105,80423
-(defun proof-retract-until-point-interactive 2184,83676
-(defun proof-retract-until-point 2193,84083
-(define-derived-mode proof-mode 2248,86088
-(defun proof-script-set-visited-file-name 2284,87470
-(defun proof-script-set-buffer-hooks 2306,88483
-(defun proof-script-kill-buffer-fn 2314,88901
-(defun proof-config-done-related 2346,90218
-(defun proof-generic-goal-command-p 2411,92703
-(defun proof-generic-state-preserving-p 2416,92916
-(defun proof-generic-count-undos 2425,93433
-(defun proof-generic-find-and-forget 2456,94561
-(defconst proof-script-important-settings2507,96333
-(defun proof-config-done 2522,96879
-(defun proof-setup-parsing-mechanism 2589,99044
-(defun proof-setup-imenu 2613,100116
-(deflocal proof-segment-up-to-cache 2650,101398
-(deflocal proof-segment-up-to-cache-start 2654,101541
-(deflocal proof-segment-up-to-cache-end 2655,101586
-(deflocal proof-last-edited-low-watermark 2656,101629
-(defun proof-segment-up-to-using-cache 2658,101677
-(defun proof-segment-cache-contents-for 2686,102797
-(defun proof-script-after-change-function 2703,103379
-(defun proof-script-set-after-change-functions 2715,103886
-
-generic/proof-shell.el,3766
-(defvar proof-marker 35,721
-(defvar proof-action-list 38,817
-(defsubst proof-shell-invoke-callback 80,2530
-(defvar proof-shell-last-goals-output 94,3022
-(defvar proof-shell-last-response-output 97,3102
-(defvar proof-shell-delayed-output-start 100,3189
-(defvar proof-shell-delayed-output-end 104,3371
-(defvar proof-shell-delayed-output-flags 108,3551
-(defvar proof-shell-interrupt-pending 111,3676
-(defvar proof-shell-exit-in-progress 116,3900
-(defcustom proof-shell-active-scripting-indicator128,4245
-(defun proof-shell-ready-prover 180,5829
-(defsubst proof-shell-live-buffer 194,6368
-(defun proof-shell-available-p 201,6588
-(defun proof-grab-lock 207,6810
-(defun proof-release-lock 217,7239
-(defcustom proof-shell-fiddle-frames 227,7413
-(defun proof-shell-set-text-representation 232,7571
-(defun proof-shell-start 240,7899
-(defvar proof-shell-kill-function-hooks 419,13993
-(defun proof-shell-kill-function 422,14091
-(defun proof-shell-clear-state 485,16293
-(defun proof-shell-exit 501,16768
-(defun proof-shell-bail-out 525,17702
-(defun proof-shell-restart 535,18224
-(defvar proof-shell-urgent-message-marker 576,19596
-(defvar proof-shell-urgent-message-scanner 579,19717
-(defun proof-shell-handle-error-output 583,19902
-(defun proof-shell-handle-error-or-interrupt 609,20764
-(defun proof-shell-error-or-interrupt-action 652,22513
-(defun proof-goals-pos 679,23610
-(defun proof-pbp-focus-on-first-goal 684,23821
-(defsubst proof-shell-string-match-safe 696,24237
-(defun proof-shell-handle-immediate-output 700,24398
-(defun proof-interrupt-process 767,27005
-(defun proof-shell-insert 801,28238
-(defun proof-shell-action-list-item 858,30220
-(defun proof-shell-set-silent 863,30462
-(defun proof-shell-start-silent-item 869,30681
-(defun proof-shell-clear-silent 875,30870
-(defun proof-shell-stop-silent-item 881,31092
-(defsubst proof-shell-should-be-silent 887,31281
-(defsubst proof-shell-insert-action-item 899,31854
-(defsubst proof-shell-slurp-comments 903,32029
-(defun proof-add-to-queue 914,32434
-(defun proof-start-queue 966,34386
-(defun proof-extend-queue 978,34781
-(defun proof-shell-exec-loop 997,35400
-(defun proof-shell-insert-loopback-cmd 1079,38340
-(defun proof-shell-process-urgent-message 1104,39504
-(defun proof-shell-process-urgent-message-default 1160,41529
-(defun proof-shell-process-urgent-message-trace 1176,42113
-(defun proof-shell-process-urgent-message-retract 1188,42636
-(defun proof-shell-process-urgent-message-elisp 1214,43766
-(defun proof-shell-process-urgent-message-thmdeps 1229,44261
-(defun proof-shell-process-interactive-prompt-regexp 1239,44605
-(defun proof-shell-strip-eager-annotations 1251,44961
-(defun proof-shell-filter 1267,45461
-(defun proof-shell-filter-first-command 1367,48833
-(defun proof-shell-process-urgent-messages 1382,49376
-(defun proof-shell-filter-manage-output 1432,50942
-(defsubst proof-shell-display-output-as-response 1468,52365
-(defun proof-shell-handle-delayed-output 1474,52660
-(defvar pg-last-tracing-output-time 1562,55835
-(defvar pg-last-trace-output-count 1565,55948
-(defconst pg-slow-mode-trigger-count 1568,56033
-(defconst pg-slow-mode-duration 1571,56138
-(defconst pg-fast-tracing-mode-threshold 1574,56220
-(defun pg-tracing-tight-loop 1577,56349
-(defun pg-finish-tracing-display 1601,57381
-(defun proof-shell-wait 1619,57762
-(defun proof-done-invisible 1649,58973
-(defun proof-shell-invisible-command 1655,59143
-(defun proof-shell-invisible-cmd-get-result 1702,60735
-(defun proof-shell-invisible-command-invisible-result 1714,61171
-(defun pg-insert-last-output-as-comment 1734,61672
-(define-derived-mode proof-shell-mode 1753,62144
-(defconst proof-shell-important-settings1790,63171
-(defun proof-shell-config-done 1796,63286
-
-generic/proof-site.el,666
-(defconst proof-assistant-table-default35,1157
-(defconst proof-general-short-version68,2172
-(defconst proof-general-version-year 74,2359
-(defgroup proof-general 81,2512
-(defgroup proof-general-internals 86,2620
-(defun proof-home-directory-fn 99,3008
-(defcustom proof-home-directory110,3380
-(defcustom proof-images-directory119,3746
-(defcustom proof-info-directory125,3948
-(defcustom proof-assistant-table154,4925
-(defcustom proof-assistants 195,6367
-(defun proof-ready-for-assistant 224,7521
-(defvar proof-general-configured-provers 276,9813
-(defun proof-chose-prover 349,12424
-(defun proofgeneral 354,12556
-(defun proof-visit-example-file 363,12874
-
-generic/proof-splash.el,990
-(defcustom proof-splash-enable 34,955
-(defcustom proof-splash-time 39,1107
-(defcustom proof-splash-contents47,1391
-(defconst proof-splash-startup-msg91,2956
-(defconst proof-splash-welcome 100,3334
-(define-derived-mode proof-splash-mode 103,3438
-(define-key proof-splash-mode-map 109,3612
-(define-key proof-splash-mode-map 110,3664
-(defsubst proof-emacs-imagep 115,3791
-(defun proof-get-image 120,3916
-(defvar proof-splash-timeout-conf 142,4716
-(defun proof-splash-centre-spaces 145,4829
-(defun proof-splash-remove-screen 172,5985
-(defun proof-splash-remove-buffer 189,6641
-(defvar proof-splash-seen 200,7029
-(defun proof-splash-insert-contents 203,7131
-(defun proof-splash-display-screen 243,8261
-(defalias 'pg-about pg-about
279,9783
-(defun proof-splash-message 282,9849
-(defun proof-splash-timeout-waiter 295,10307
-(defvar proof-splash-old-frame-title-format 308,10865
-(defun proof-splash-set-frame-titles 310,10915
-(defun proof-splash-unset-frame-titles 319,11230
+(deflocal proof-active-buffer-fake-minor-mode 46,1413
+(deflocal proof-script-buffer-file-name 49,1539
+(deflocal pg-script-portions 56,1949
+(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode
59,2055
+(defun proof-next-element-count 68,2250
+(defun proof-element-id 74,2492
+(defun proof-next-element-id 78,2661
+(deflocal proof-locked-span 114,3965
+(deflocal proof-queue-span 121,4231
+(deflocal proof-overlay-arrow 130,4717
+(defun proof-span-give-warning 136,4844
+(defun proof-span-read-only 142,5024
+(defun proof-strict-read-only 151,5397
+(defsubst proof-set-queue-endpoints 161,5775
+(defun proof-set-overlay-arrow 165,5916
+(defsubst proof-set-locked-endpoints 176,6254
+(defsubst proof-detach-queue 181,6430
+(defsubst proof-detach-locked 186,6569
+(defsubst proof-set-queue-start 193,6794
+(defsubst proof-set-locked-end 197,6920
+(defsubst proof-set-queue-end 209,7390
+(defun proof-init-segmentation 220,7687
+(defun proof-colour-locked 250,8938
+(defun proof-colour-locked-span 257,9211
+(defun proof-sticky-errors 263,9484
+(defun proof-restart-buffers 276,9900
+(defun proof-script-buffers-with-spans 300,10833
+(defun proof-script-remove-all-spans-and-deactivate 310,11189
+(defun proof-script-clear-queue-spans-on-error 314,11379
+(defun proof-script-delete-spans 340,12396
+(defun proof-script-delete-secondary-spans 345,12595
+(defun proof-unprocessed-begin 358,12884
+(defun proof-script-end 366,13138
+(defun proof-queue-or-locked-end 375,13448
+(defun proof-locked-region-full-p 394,14041
+(defun proof-locked-region-empty-p 403,14313
+(defun proof-only-whitespace-to-locked-region-p 407,14463
+(defun proof-in-locked-region-p 417,14812
+(defun proof-goto-end-of-locked 429,15069
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15856
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16337
+(defun proof-end-of-locked-visible-p 469,16877
+(defconst pg-idioms 488,17470
+(defconst pg-all-idioms 491,17566
+(defun pg-clear-script-portions 495,17687
+(defun pg-remove-element 501,17922
+(defun pg-get-element 509,18225
+(defun pg-add-element 519,18540
+(defun pg-invisible-prop 567,20502
+(defun pg-set-element-span-invisible 572,20703
+(defun pg-toggle-element-span-visibility 585,21269
+(defun pg-open-invisible-span 590,21430
+(defun pg-make-element-invisible 595,21601
+(defun pg-make-element-visible 600,21812
+(defun pg-toggle-element-visibility 605,22006
+(defun pg-show-all-portions 611,22269
+(defun pg-show-all-proofs 633,23013
+(defun pg-hide-all-proofs 638,23141
+(defun pg-add-proof-element 643,23272
+(defun pg-span-name 658,24059
+(defvar pg-span-context-menu-keymap691,25266
+(defun pg-last-output-displayform 698,25504
+(defun pg-set-span-helphighlights 721,26395
+(defun proof-complete-buffer-atomic 784,28542
+(defun proof-register-possibly-new-processed-file813,29812
+(defun proof-query-save-this-buffer-p 859,31686
+(defun proof-inform-prover-file-retracted 864,31911
+(defun proof-auto-retract-dependencies 884,32762
+(defun proof-unregister-buffer-file-name 938,35312
+(defsubst proof-action-completed 984,37137
+(defun proof-protected-process-or-retract 988,37307
+(defun proof-deactivate-scripting-auto 1016,38538
+(defun proof-deactivate-scripting-query-user-action 1025,38896
+(defun proof-deactivate-scripting-choose-action 1069,40405
+(defun proof-deactivate-scripting 1081,40790
+(defun proof-activate-scripting 1178,44913
+(defun proof-toggle-active-scripting 1278,49452
+(defun proof-done-advancing 1317,50697
+(defun proof-done-advancing-comment 1385,53194
+(defun proof-done-advancing-save 1419,54580
+(defun proof-make-goalsave1507,57944
+(defun proof-get-name-from-goal 1525,58809
+(defun proof-done-advancing-autosave 1545,59834
+(defun proof-done-advancing-other 1609,62330
+(defun proof-segment-up-to-parser 1638,63294
+(defun proof-script-generic-parse-find-comment-end 1708,65575
+(defun proof-script-generic-parse-cmdend 1717,65989
+(defun proof-script-generic-parse-cmdstart 1768,67885
+(defun proof-script-generic-parse-sexp 1807,69485
+(defun proof-semis-to-vanillas 1819,69951
+(defun proof-next-command-new-line 1872,71624
+(defun proof-script-next-command-advance 1877,71830
+(defun proof-assert-until-point 1896,72330
+(defun proof-assert-electric-terminator 1912,73001
+(defun proof-assert-semis 1956,74681
+(defun proof-retract-before-change 1970,75442
+(defun proof-insert-pbp-command 1993,76098
+(defun proof-insert-sendback-command 2008,76601
+(defun proof-done-retracting 2034,77504
+(defun proof-setup-retract-action 2069,78958
+(defun proof-last-goal-or-goalsave 2081,79563
+(defun proof-retract-target 2105,80475
+(defun proof-retract-until-point-interactive 2184,83728
+(defun proof-retract-until-point 2193,84135
+(define-derived-mode proof-mode 2248,86140
+(defun proof-script-set-visited-file-name 2284,87517
+(defun proof-script-set-buffer-hooks 2306,88530
+(defun proof-script-kill-buffer-fn 2314,88948
+(defun proof-config-done-related 2346,90265
+(defun proof-generic-goal-command-p 2411,92750
+(defun proof-generic-state-preserving-p 2416,92963
+(defun proof-generic-count-undos 2425,93480
+(defun proof-generic-find-and-forget 2456,94608
+(defconst proof-script-important-settings2507,96380
+(defun proof-config-done 2522,96926
+(defun proof-setup-parsing-mechanism 2589,99091
+(defun proof-setup-imenu 2613,100163
+(deflocal proof-segment-up-to-cache 2650,101445
+(deflocal proof-segment-up-to-cache-start 2654,101588
+(deflocal proof-segment-up-to-cache-end 2655,101633
+(deflocal proof-last-edited-low-watermark 2656,101676
+(defun proof-segment-up-to-using-cache 2658,101724
+(defun proof-segment-cache-contents-for 2686,102844
+(defun proof-script-after-change-function 2703,103426
+(defun proof-script-set-after-change-functions 2715,103933
+
+generic/proof-shell.el,3904
+(defvar proof-marker 35,772
+(defvar proof-action-list 38,868
+(defsubst proof-shell-invoke-callback 80,2581
+(defvar proof-shell-last-goals-output 94,3073
+(defvar proof-shell-last-response-output 97,3153
+(defvar proof-shell-delayed-output-start 100,3240
+(defvar proof-shell-delayed-output-end 104,3422
+(defvar proof-shell-delayed-output-flags 108,3602
+(defvar proof-shell-interrupt-pending 111,3727
+(defvar proof-shell-exit-in-progress 116,3951
+(defcustom proof-shell-active-scripting-indicator128,4296
+(defun proof-shell-ready-prover 180,5880
+(defsubst proof-shell-live-buffer 194,6419
+(defun proof-shell-available-p 201,6639
+(defun proof-grab-lock 207,6861
+(defun proof-release-lock 219,7363
+(defcustom proof-shell-fiddle-frames 229,7537
+(defun proof-shell-set-text-representation 234,7695
+(defun proof-shell-start 242,8023
+(defvar proof-shell-kill-function-hooks 422,14139
+(defun proof-shell-kill-function 425,14237
+(defun proof-shell-clear-state 495,16684
+(defun proof-shell-exit 511,17159
+(defun proof-shell-bail-out 535,18093
+(defun proof-shell-restart 545,18615
+(defvar proof-shell-urgent-message-marker 586,19987
+(defvar proof-shell-urgent-message-scanner 589,20108
+(defun proof-shell-handle-error-output 593,20293
+(defun proof-shell-handle-error-or-interrupt 619,21155
+(defun proof-shell-error-or-interrupt-action 662,22904
+(defun proof-goals-pos 689,24001
+(defun proof-pbp-focus-on-first-goal 694,24212
+(defsubst proof-shell-string-match-safe 706,24628
+(defun proof-shell-handle-immediate-output 710,24789
+(defun proof-interrupt-process 777,27396
+(defun proof-shell-insert 811,28629
+(defun proof-shell-action-list-item 868,30611
+(defun proof-shell-set-silent 873,30853
+(defun proof-shell-start-silent-item 879,31072
+(defun proof-shell-clear-silent 885,31261
+(defun proof-shell-stop-silent-item 891,31483
+(defsubst proof-shell-should-be-silent 897,31672
+(defsubst proof-shell-insert-action-item 909,32245
+(defsubst proof-shell-slurp-comments 913,32420
+(defun proof-add-to-queue 924,32825
+(defun proof-start-queue 979,34884
+(defun proof-extend-queue 991,35269
+(defun proof-shell-exec-loop 1010,35888
+(defun proof-shell-insert-loopback-cmd 1092,38828
+(defun proof-shell-process-urgent-message 1117,39992
+(defun proof-shell-process-urgent-message-default 1173,42017
+(defun proof-shell-process-urgent-message-trace 1189,42601
+(defun proof-shell-process-urgent-message-retract 1201,43124
+(defun proof-shell-process-urgent-message-elisp 1227,44254
+(defun proof-shell-process-urgent-message-thmdeps 1242,44749
+(defun proof-shell-process-interactive-prompt-regexp 1252,45093
+(defun proof-shell-strip-eager-annotations 1264,45449
+(defun proof-shell-filter 1280,45949
+(defun proof-shell-filter-first-command 1380,49322
+(defun proof-shell-process-urgent-messages 1398,49961
+(defun proof-shell-filter-manage-output 1448,51527
+(defsubst proof-shell-display-output-as-response 1484,52950
+(defun proof-shell-handle-delayed-output 1490,53245
+(defvar pg-last-tracing-output-time 1594,56817
+(defvar pg-last-trace-output-count 1597,56930
+(defconst pg-slow-mode-trigger-count 1600,57015
+(defconst pg-slow-mode-duration 1603,57120
+(defconst pg-fast-tracing-mode-threshold 1606,57202
+(defun pg-tracing-tight-loop 1609,57331
+(defun pg-finish-tracing-display 1633,58363
+(defun proof-shell-wait 1652,58778
+(defun proof-done-invisible 1682,59989
+(defun proof-shell-invisible-command 1688,60159
+(defun proof-shell-terminate 1742,62097
+(defun proof-shell-invisible-cmd-get-result 1755,62476
+(defun proof-shell-invisible-command-invisible-result 1767,62907
+(defun pg-insert-last-output-as-comment 1787,63403
+(define-derived-mode proof-shell-mode 1806,63875
+(defconst proof-shell-important-settings1843,64902
+(defun proof-shell-config-done 1849,65017
+(defun proof-shell-setup-init-commands 1879,66289
+(defun proof-shell-during-init-p 1901,67043
+
+generic/proof-site.el,668
+(defconst proof-assistant-table-default36,1210
+(defconst proof-general-short-version78,2411
+(defconst proof-general-version-year 84,2598
+(defgroup proof-general 91,2751
+(defgroup proof-general-internals 96,2859
+(defun proof-home-directory-fn 109,3247
+(defcustom proof-home-directory120,3619
+(defcustom proof-images-directory129,3985
+(defcustom proof-info-directory135,4187
+(defcustom proof-assistant-table164,5164
+(defcustom proof-assistants 205,6606
+(defun proof-ready-for-assistant 234,7760
+(defvar proof-general-configured-provers 286,10052
+(defun proof-chose-prover 359,12663
+(defun proofgeneral 364,12795
+(defun proof-visit-example-file 373,13113
+
+generic/proof-splash.el,991
+(defcustom proof-splash-enable 34,1009
+(defcustom proof-splash-time 39,1161
+(defcustom proof-splash-contents47,1445
+(defconst proof-splash-startup-msg91,3010
+(defconst proof-splash-welcome 100,3388
+(define-derived-mode proof-splash-mode 103,3492
+(define-key proof-splash-mode-map 109,3666
+(define-key proof-splash-mode-map 110,3718
+(defsubst proof-emacs-imagep 115,3845
+(defun proof-get-image 120,3970
+(defvar proof-splash-timeout-conf 142,4770
+(defun proof-splash-centre-spaces 145,4883
+(defun proof-splash-remove-screen 172,6039
+(defun proof-splash-remove-buffer 189,6695
+(defvar proof-splash-seen 200,7083
+(defun proof-splash-insert-contents 203,7185
+(defun proof-splash-display-screen 243,8315
+(defalias 'pg-about pg-about
279,9837
+(defun proof-splash-message 282,9903
+(defun proof-splash-timeout-waiter 295,10361
+(defvar proof-splash-old-frame-title-format 308,10921
+(defun proof-splash-set-frame-titles 310,10971
+(defun proof-splash-unset-frame-titles 319,11286
 
 generic/proof-syntax.el,1278
-(defsubst proof-ids-to-regexp 22,464
-(defsubst proof-anchor-regexp 29,702
-(defconst proof-no-regexp 33,807
-(defsubst proof-regexp-alt 36,898
-(defsubst proof-regexp-alt-list 45,1210
-(defsubst proof-re-search-forward-region 49,1345
-(defsubst proof-search-forward 62,1843
-(defsubst proof-replace-regexp-in-string 69,2113
-(defsubst proof-re-search-forward 74,2364
-(defsubst proof-re-search-backward 79,2622
-(defsubst proof-re-search-forward-safe 84,2883
-(defsubst proof-string-match 90,3164
-(defsubst proof-string-match-safe 95,3393
-(defsubst proof-stringfn-match 99,3597
-(defsubst proof-looking-at 106,3860
-(defsubst proof-looking-at-safe 111,4047
-(defun proof-buffer-syntactic-context 120,4260
-(defsubst proof-looking-at-syntactic-context-default 141,5122
-(defun proof-looking-at-syntactic-context 150,5477
-(defun proof-inside-comment 159,5939
-(defun proof-inside-string 165,6112
-(defsubst proof-replace-string 175,6311
-(defsubst proof-replace-regexp 180,6515
-(defsubst proof-replace-regexp-nocasefold 185,6724
-(defvar proof-id 195,7012
-(defsubst proof-ids 201,7232
-(defun proof-zap-commas 208,7484
-(defadvice font-lock-fontify-keywords-region234,8370
-(defun proof-format 250,8966
-(defun proof-format-filename 269,9605
-(defun proof-insert 316,11007
+(defsubst proof-ids-to-regexp 22,516
+(defsubst proof-anchor-regexp 29,754
+(defconst proof-no-regexp 33,859
+(defsubst proof-regexp-alt 36,950
+(defsubst proof-regexp-alt-list 45,1262
+(defsubst proof-re-search-forward-region 49,1397
+(defsubst proof-search-forward 62,1895
+(defsubst proof-replace-regexp-in-string 69,2165
+(defsubst proof-re-search-forward 74,2416
+(defsubst proof-re-search-backward 79,2674
+(defsubst proof-re-search-forward-safe 84,2935
+(defsubst proof-string-match 90,3216
+(defsubst proof-string-match-safe 95,3445
+(defsubst proof-stringfn-match 99,3649
+(defsubst proof-looking-at 106,3912
+(defsubst proof-looking-at-safe 111,4099
+(defun proof-buffer-syntactic-context 120,4312
+(defsubst proof-looking-at-syntactic-context-default 141,5174
+(defun proof-looking-at-syntactic-context 150,5529
+(defun proof-inside-comment 159,5991
+(defun proof-inside-string 165,6164
+(defsubst proof-replace-string 175,6363
+(defsubst proof-replace-regexp 180,6567
+(defsubst proof-replace-regexp-nocasefold 185,6776
+(defvar proof-id 195,7064
+(defsubst proof-ids 201,7284
+(defun proof-zap-commas 208,7536
+(defadvice font-lock-fontify-keywords-region234,8422
+(defun proof-format 250,9018
+(defun proof-format-filename 269,9657
+(defun proof-insert 316,11059
 
 generic/proof-toolbar.el,2401
-(defun proof-toolbar-function 33,759
-(defun proof-toolbar-icon 37,906
-(defun proof-toolbar-enabler 41,1053
-(defun proof-toolbar-make-icon 50,1255
-(defun proof-toolbar-make-toolbar-items 59,1563
-(defvar proof-toolbar-map 85,2424
-(defun proof-toolbar-available-p 88,2523
-(defun proof-toolbar-setup 98,2829
-(defun proof-toolbar-enable 119,3686
-(defalias 'proof-toolbar-undo proof-toolbar-undo
152,4744
-(defun proof-toolbar-undo-enable-p 154,4812
-(defalias 'proof-toolbar-delete proof-toolbar-delete
161,4970
-(defun proof-toolbar-delete-enable-p 163,5051
-(defalias 'proof-toolbar-home proof-toolbar-home
171,5233
-(defalias 'proof-toolbar-next proof-toolbar-next
175,5300
-(defun proof-toolbar-next-enable-p 177,5371
-(defalias 'proof-toolbar-goto proof-toolbar-goto
183,5487
-(defun proof-toolbar-goto-enable-p 185,5537
-(defalias 'proof-toolbar-retract proof-toolbar-retract
190,5622
-(defun proof-toolbar-retract-enable-p 192,5679
-(defalias 'proof-toolbar-use proof-toolbar-use
198,5798
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
199,5850
-(defalias 'proof-toolbar-prooftree proof-toolbar-prooftree
203,5933
-(defalias 'proof-toolbar-restart proof-toolbar-restart
207,6018
-(defalias 'proof-toolbar-goal proof-toolbar-goal
211,6083
-(defalias 'proof-toolbar-qed proof-toolbar-qed
215,6141
-(defun proof-toolbar-qed-enable-p 217,6190
-(defalias 'proof-toolbar-state proof-toolbar-state
225,6352
-(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
226,6395
-(defalias 'proof-toolbar-context proof-toolbar-context
230,6474
-(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
231,6520
-(defalias 'proof-toolbar-command proof-toolbar-command
235,6601
-(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
236,6657
-(defun proof-toolbar-help 240,6762
-(defalias 'proof-toolbar-find proof-toolbar-find
246,6842
-(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
247,6894
-(defalias 'proof-toolbar-info proof-toolbar-info
251,6969
-(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
252,7024
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
256,7122
-(defun proof-toolbar-visibility-enable-p 258,7182
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
263,7296
-(defun proof-toolbar-interrupt-enable-p 264,7357
-(defun proof-toolbar-scripting-menu 272,7510
-
-generic/proof-tree.el,3278
-(defgroup proof-tree 90,3806
-(defcustom proof-tree-program 95,3947
-(defcustom proof-tree-arguments 100,4093
-(defgroup proof-tree-internals 110,4253
-(defcustom proof-tree-ignored-commands-regexp 118,4522
-(defcustom proof-tree-navigation-command-regexp 127,4921
-(defcustom proof-tree-cheating-regexp 135,5240
-(defcustom proof-tree-current-goal-regexp 144,5637
-(defcustom proof-tree-update-goal-regexp 154,6039
-(defcustom proof-tree-additional-subgoal-ID-regexp 166,6608
-(defcustom proof-tree-existential-regexp 174,6927
-(defcustom proof-tree-existentials-state-start-regexp 188,7547
-(defcustom proof-tree-existentials-state-end-regexp 199,8098
-(defcustom proof-tree-proof-completed-regexp 211,8741
-(defcustom proof-tree-get-proof-info 216,8890
-(defcustom proof-tree-extract-instantiated-existentials 240,9931
-(defcustom proof-tree-show-sequent-command 257,10649
-(defcustom proof-tree-find-begin-of-unfinished-proof 271,11271
-(defcustom proof-tree-urgent-action-hook 282,11833
-(defvar proof-tree-external-display 306,12688
-(defvar proof-tree-process 317,13193
-(defconst proof-tree-process-name 320,13282
-(defconst proof-tree-process-buffer323,13381
-(defconst proof-tree-emacs-exec-regexp327,13521
-(defvar proof-tree-last-state 331,13688
-(defvar proof-tree-current-proof 335,13792
-(defvar proof-tree-sequent-hash 340,13973
-(defvar proof-tree-existentials-alist 355,14680
-(defvar proof-tree-existentials-alist-history 366,15179
-(defun proof-tree-stop-external-display 375,15398
-(defun proof-tree-insert-output 383,15662
-(defun proof-tree-process-filter 394,16045
-(defun proof-tree-process-sentinel 420,16743
-(defun proof-tree-start-process 428,17069
-(defun proof-tree-is-running 457,18252
-(defun proof-tree-ensure-running 462,18413
-(defconst proof-tree-protocol-version 472,18617
-(defun proof-tree-send-message 477,18817
-(defun proof-tree-send-configure 491,19303
-(defun proof-tree-send-goal-state 499,19520
-(defun proof-tree-send-update-sequent 525,20569
-(defun proof-tree-send-switch-goal 538,21006
-(defun proof-tree-send-proof-completed 547,21332
-(defun proof-tree-send-undo 561,21773
-(defun proof-tree-send-quit-proof 566,21955
-(defun proof-tree-record-existentials-state 577,22290
-(defun proof-tree-undo-state-var 590,22840
-(defun proof-tree-undo-existentials 609,23621
-(defun proof-tree-delete-existential-assoc 617,23936
-(defun proof-tree-add-existential-assoc 623,24199
-(defun proof-tree-reset-existentials 636,24814
-(defun proof-tree-show-goal-callback 646,25090
-(defun proof-tree-make-show-goal-callback 667,26077
-(defun proof-tree-urgent-action 671,26238
-(defun proof-tree-quit-proof 736,28774
-(defun proof-tree-register-existentials 746,29210
-(defun proof-tree-extract-goals 759,29754
-(defun proof-tree-extract-list 781,30699
-(defun proof-tree-extract-existential-info 804,31669
-(defun proof-tree-handle-proof-progress 824,32540
-(defun proof-tree-handle-navigation 874,34611
-(defun proof-tree-handle-proof-command 892,35337
-(defun proof-tree-handle-undo 907,35999
-(defun proof-tree-update-sequent 939,37298
-(defun proof-tree-handle-delayed-output 980,39066
-(defun proof-tree-leave-buffer 1031,41089
-(defun proof-tree-display-current-proof 1043,41372
-(defun proof-tree-external-display-toggle 1075,42713
+(defun proof-toolbar-function 33,814
+(defun proof-toolbar-icon 37,961
+(defun proof-toolbar-enabler 41,1108
+(defun proof-toolbar-make-icon 50,1310
+(defun proof-toolbar-make-toolbar-items 59,1618
+(defvar proof-toolbar-map 85,2479
+(defun proof-toolbar-available-p 88,2578
+(defun proof-toolbar-setup 98,2884
+(defun proof-toolbar-enable 119,3741
+(defalias 'proof-toolbar-undo proof-toolbar-undo
152,4799
+(defun proof-toolbar-undo-enable-p 154,4867
+(defalias 'proof-toolbar-delete proof-toolbar-delete
161,5025
+(defun proof-toolbar-delete-enable-p 163,5106
+(defalias 'proof-toolbar-home proof-toolbar-home
171,5288
+(defalias 'proof-toolbar-next proof-toolbar-next
175,5355
+(defun proof-toolbar-next-enable-p 177,5426
+(defalias 'proof-toolbar-goto proof-toolbar-goto
183,5542
+(defun proof-toolbar-goto-enable-p 185,5592
+(defalias 'proof-toolbar-retract proof-toolbar-retract
190,5677
+(defun proof-toolbar-retract-enable-p 192,5734
+(defalias 'proof-toolbar-use proof-toolbar-use
198,5853
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
199,5905
+(defalias 'proof-toolbar-prooftree proof-toolbar-prooftree
203,5988
+(defalias 'proof-toolbar-restart proof-toolbar-restart
207,6073
+(defalias 'proof-toolbar-goal proof-toolbar-goal
211,6138
+(defalias 'proof-toolbar-qed proof-toolbar-qed
215,6196
+(defun proof-toolbar-qed-enable-p 217,6245
+(defalias 'proof-toolbar-state proof-toolbar-state
225,6407
+(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
226,6450
+(defalias 'proof-toolbar-context proof-toolbar-context
230,6529
+(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
231,6575
+(defalias 'proof-toolbar-command proof-toolbar-command
235,6656
+(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
236,6712
+(defun proof-toolbar-help 240,6817
+(defalias 'proof-toolbar-find proof-toolbar-find
246,6897
+(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
247,6949
+(defalias 'proof-toolbar-info proof-toolbar-info
251,7024
+(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
252,7079
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
256,7177
+(defun proof-toolbar-visibility-enable-p 258,7237
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
263,7351
+(defun proof-toolbar-interrupt-enable-p 264,7412
+(defun proof-toolbar-scripting-menu 272,7565
+
+generic/proof-tree.el,3325
+(defgroup proof-tree 90,3804
+(defcustom proof-tree-program 95,3945
+(defcustom proof-tree-arguments 100,4091
+(defgroup proof-tree-internals 110,4251
+(defcustom proof-tree-ignored-commands-regexp 118,4520
+(defcustom proof-tree-navigation-command-regexp 127,4919
+(defcustom proof-tree-cheating-regexp 135,5238
+(defcustom proof-tree-current-goal-regexp 144,5635
+(defcustom proof-tree-update-goal-regexp 154,6037
+(defcustom proof-tree-additional-subgoal-ID-regexp 166,6606
+(defcustom proof-tree-existential-regexp 174,6925
+(defcustom proof-tree-existentials-state-start-regexp 188,7545
+(defcustom proof-tree-existentials-state-end-regexp 199,8096
+(defcustom proof-tree-proof-finished-regexp 211,8739
+(defcustom proof-tree-get-proof-info 216,8886
+(defcustom proof-tree-extract-instantiated-existentials 240,9927
+(defcustom proof-tree-show-sequent-command 257,10645
+(defcustom proof-tree-find-begin-of-unfinished-proof 271,11267
+(defcustom proof-tree-urgent-action-hook 282,11830
+(defvar proof-tree-external-display 306,12685
+(defvar proof-tree-process 317,13190
+(defconst proof-tree-process-name 320,13279
+(defconst proof-tree-process-buffer323,13378
+(defconst proof-tree-emacs-exec-regexp327,13518
+(defvar proof-tree-last-state 331,13685
+(defvar proof-tree-current-proof 335,13789
+(defvar proof-tree-sequent-hash 340,13970
+(defvar proof-tree-existentials-alist 355,14677
+(defvar proof-tree-existentials-alist-history 366,15176
+(defun proof-tree-stop-external-display 375,15395
+(defun proof-tree-insert-output 383,15659
+(defun proof-tree-process-filter 394,16042
+(defun proof-tree-process-sentinel 420,16740
+(defun proof-tree-start-process 428,17066
+(defun proof-tree-is-running 457,18249
+(defun proof-tree-ensure-running 462,18410
+(defconst proof-tree-protocol-version 472,18614
+(defun proof-tree-send-message 477,18814
+(defun proof-tree-send-configure 491,19300
+(defun proof-tree-send-goal-state 499,19517
+(defun proof-tree-send-update-sequent 525,20566
+(defun proof-tree-send-switch-goal 538,21003
+(defun proof-tree-send-proof-finished 547,21329
+(defun proof-tree-send-proof-complete 561,21841
+(defun proof-tree-send-undo 569,22090
+(defun proof-tree-send-quit-proof 574,22272
+(defun proof-tree-record-existentials-state 585,22607
+(defun proof-tree-undo-state-var 598,23157
+(defun proof-tree-undo-existentials 617,23938
+(defun proof-tree-delete-existential-assoc 625,24253
+(defun proof-tree-add-existential-assoc 631,24516
+(defun proof-tree-clear-existentials 644,25131
+(defun proof-tree-show-goal-callback 654,25399
+(defun proof-tree-make-show-goal-callback 675,26386
+(defun proof-tree-urgent-action 679,26547
+(defun proof-tree-quit-proof 744,29083
+(defun proof-tree-register-existentials 754,29502
+(defun proof-tree-extract-goals 767,30046
+(defun proof-tree-extract-list 789,30991
+(defun proof-tree-extract-existential-info 812,31961
+(defun proof-tree-handle-proof-progress 832,32832
+(defun proof-tree-handle-navigation 883,34868
+(defun proof-tree-handle-proof-command 901,35594
+(defun proof-tree-handle-undo 916,36256
+(defun proof-tree-update-sequent 948,37555
+(defun proof-tree-handle-delayed-output 989,39323
+(defun proof-tree-leave-buffer 1042,41435
+(defun proof-tree-display-current-proof 1054,41718
+(defun proof-tree-external-display-toggle 1086,43059
 
 generic/proof-unicode-tokens.el,497
-(defvar proof-unicode-tokens-initialised 31,767
-(defun proof-unicode-tokens-init 34,874
-(defun proof-unicode-tokens-configure 48,1376
-(defun proof-unicode-tokens-mode-if-enabled 60,1822
-(defun proof-unicode-tokens-set-global 66,2021
-(defun proof-unicode-tokens-enable 82,2591
-(defun proof-unicode-tokens-reconfigure 102,3444
-(defun proof-unicode-tokens-configure-prover 128,4332
-(defun proof-unicode-tokens-activate-prover 133,4513
-(defun proof-unicode-tokens-deactivate-prover 140,4759
+(defvar proof-unicode-tokens-initialised 31,827
+(defun proof-unicode-tokens-init 34,934
+(defun proof-unicode-tokens-configure 48,1436
+(defun proof-unicode-tokens-mode-if-enabled 60,1882
+(defun proof-unicode-tokens-set-global 66,2081
+(defun proof-unicode-tokens-enable 82,2651
+(defun proof-unicode-tokens-reconfigure 102,3504
+(defun proof-unicode-tokens-configure-prover 128,4392
+(defun proof-unicode-tokens-activate-prover 133,4573
+(defun proof-unicode-tokens-deactivate-prover 140,4819
 
 generic/proof-useropts.el,1619
-(defgroup proof-user-options 21,510
-(defun proof-set-value 29,689
-(defcustom proof-electric-terminator-enable 62,1812
-(defcustom proof-toolbar-enable 74,2344
-(defcustom proof-imenu-enable 80,2517
-(defcustom pg-show-hints 86,2688
-(defcustom proof-shell-quiet-errors 91,2821
-(defcustom proof-trace-output-slow-catchup 98,3092
-(defcustom proof-strict-state-preserving 108,3589
-(defcustom proof-strict-read-only 121,4198
-(defcustom proof-three-window-enable 134,4777
-(defcustom proof-multiple-frames-enable 153,5527
-(defcustom proof-delete-empty-windows 162,5860
-(defcustom proof-shrink-windows-tofit 173,6391
-(defcustom proof-auto-raise-buffers 180,6663
-(defcustom proof-colour-locked 187,6898
-(defcustom proof-sticky-errors 195,7148
-(defcustom proof-query-file-save-when-activating-scripting202,7365
-(defcustom proof-prog-name-ask218,8085
-(defcustom proof-prog-name-guess224,8245
-(defcustom proof-tidy-response232,8510
-(defcustom proof-keep-response-history246,8973
-(defcustom pg-input-ring-size 256,9361
-(defcustom proof-general-debug 261,9513
-(defcustom proof-use-parser-cache 270,9884
-(defcustom proof-follow-mode 277,10138
-(defcustom proof-auto-action-when-deactivating-scripting 301,11315
-(defcustom proof-rsh-command 329,12497
-(defcustom proof-disappearing-proofs 345,13055
-(defcustom proof-full-annotation 350,13216
-(defcustom proof-output-tooltips 360,13679
-(defcustom proof-minibuffer-messages 371,14186
-(defcustom proof-autosend-enable 379,14495
-(defcustom proof-autosend-delay 385,14675
-(defcustom proof-autosend-all 391,14833
-(defcustom proof-fast-process-buffer 396,15002
+(defgroup proof-user-options 21,564
+(defun proof-set-value 29,743
+(defcustom proof-electric-terminator-enable 62,1866
+(defcustom proof-toolbar-enable 74,2398
+(defcustom proof-imenu-enable 80,2571
+(defcustom pg-show-hints 86,2742
+(defcustom proof-shell-quiet-errors 91,2875
+(defcustom proof-trace-output-slow-catchup 98,3146
+(defcustom proof-strict-state-preserving 108,3643
+(defcustom proof-strict-read-only 121,4252
+(defcustom proof-three-window-enable 134,4831
+(defcustom proof-multiple-frames-enable 153,5581
+(defcustom proof-delete-empty-windows 162,5914
+(defcustom proof-shrink-windows-tofit 173,6445
+(defcustom proof-auto-raise-buffers 180,6717
+(defcustom proof-colour-locked 187,6952
+(defcustom proof-sticky-errors 195,7202
+(defcustom proof-query-file-save-when-activating-scripting202,7419
+(defcustom proof-prog-name-ask218,8139
+(defcustom proof-prog-name-guess224,8299
+(defcustom proof-tidy-response232,8564
+(defcustom proof-keep-response-history246,9027
+(defcustom pg-input-ring-size 256,9415
+(defcustom proof-general-debug 261,9567
+(defcustom proof-use-parser-cache 270,9938
+(defcustom proof-follow-mode 277,10192
+(defcustom proof-auto-action-when-deactivating-scripting 301,11369
+(defcustom proof-rsh-command 329,12551
+(defcustom proof-disappearing-proofs 345,13109
+(defcustom proof-full-annotation 350,13270
+(defcustom proof-output-tooltips 360,13733
+(defcustom proof-minibuffer-messages 371,14240
+(defcustom proof-autosend-enable 379,14549
+(defcustom proof-autosend-delay 385,14729
+(defcustom proof-autosend-all 391,14887
+(defcustom proof-fast-process-buffer 396,15056
 
 generic/proof-utils.el,1645
-(defmacro proof-with-current-buffer-if-exists 61,1684
-(defmacro proof-with-script-buffer 70,2061
-(defmacro proof-map-buffers 81,2442
-(defmacro proof-sym 86,2627
-(defsubst proof-try-require 91,2788
-(defun proof-save-some-buffers 104,3119
-(defun proof-save-this-buffer 124,3715
-(defun proof-file-truename 137,4079
-(defun proof-files-to-buffers 141,4261
-(defun proof-buffers-in-mode 149,4500
-(defun pg-save-from-death 163,4950
-(defun proof-define-keys 182,5566
-(defun pg-remove-specials 193,5851
-(defun pg-remove-specials-in-string 203,6187
-(defun proof-safe-split-window-vertically 213,6412
-(defun proof-warn-if-unset 218,6592
-(defun proof-get-window-for-buffer 223,6810
-(defun proof-display-and-keep-buffer 272,9120
-(defun proof-clean-buffer 314,10843
-(defun pg-internal-warning 330,11499
-(defun proof-debug 338,11781
-(defun proof-switch-to-buffer 353,12332
-(defun proof-resize-window-tofit 375,13456
-(defun proof-submit-bug-report 470,17304
-(defun proof-deftoggle-fn 505,18661
-(defmacro proof-deftoggle 520,19327
-(defun proof-defintset-fn 531,19840
-(defmacro proof-defintset 550,20664
-(defun proof-deffloatset-fn 557,21043
-(defmacro proof-deffloatset 573,21757
-(defun proof-defstringset-fn 580,22142
-(defmacro proof-defstringset 593,22768
-(defun proof-escape-keymap-doc 606,23224
-(defmacro proof-defshortcut 610,23378
-(defmacro proof-definvisible 625,23976
-(defun pg-custom-save-vars 652,24905
-(defun pg-custom-reset-vars 668,25549
-(defun proof-locate-executable 681,25886
-(defun pg-current-word-pos 696,26436
-(defsubst proof-shell-strip-output-markup 741,28091
-(defun proof-minibuffer-message 747,28355
+(defmacro proof-with-current-buffer-if-exists 61,1735
+(defmacro proof-with-script-buffer 70,2112
+(defmacro proof-map-buffers 81,2493
+(defmacro proof-sym 86,2678
+(defsubst proof-try-require 91,2839
+(defun proof-save-some-buffers 104,3170
+(defun proof-save-this-buffer 124,3766
+(defun proof-file-truename 137,4130
+(defun proof-files-to-buffers 141,4312
+(defun proof-buffers-in-mode 149,4551
+(defun pg-save-from-death 163,5001
+(defun proof-define-keys 182,5617
+(defun pg-remove-specials 193,5902
+(defun pg-remove-specials-in-string 203,6238
+(defun proof-safe-split-window-vertically 213,6463
+(defun proof-warn-if-unset 218,6643
+(defun proof-get-window-for-buffer 223,6861
+(defun proof-display-and-keep-buffer 272,9171
+(defun proof-clean-buffer 314,10894
+(defun pg-internal-warning 330,11550
+(defun proof-debug 338,11832
+(defun proof-switch-to-buffer 353,12383
+(defun proof-resize-window-tofit 375,13507
+(defun proof-submit-bug-report 470,17355
+(defun proof-deftoggle-fn 505,18712
+(defmacro proof-deftoggle 520,19378
+(defun proof-defintset-fn 531,19891
+(defmacro proof-defintset 550,20715
+(defun proof-deffloatset-fn 557,21094
+(defmacro proof-deffloatset 573,21808
+(defun proof-defstringset-fn 580,22193
+(defmacro proof-defstringset 593,22819
+(defun proof-escape-keymap-doc 606,23275
+(defmacro proof-defshortcut 610,23429
+(defmacro proof-definvisible 625,24027
+(defun pg-custom-save-vars 652,24956
+(defun pg-custom-reset-vars 668,25600
+(defun proof-locate-executable 681,25937
+(defun pg-current-word-pos 696,26487
+(defsubst proof-shell-strip-output-markup 741,28142
+(defun proof-minibuffer-message 747,28406
 
 lib/bufhist.el,1257
-(defun bufhist-ring-update 38,1344
-(defgroup bufhist 47,1666
-(defcustom bufhist-ring-size 51,1747
-(defvar bufhist-ring 56,1858
-(defvar bufhist-ring-pos 59,1932
-(defvar bufhist-lastswitch-modified-tick 62,2011
-(defvar bufhist-read-only-history 65,2117
-(defvar bufhist-saved-mode-line-format 68,2188
-(defvar bufhist-normal-read-only 71,2291
-(defvar bufhist-top-point 74,2385
-(defun bufhist-mode-line-format-entry 77,2475
-(defconst bufhist-minor-mode-map106,3549
-(define-minor-mode bufhist-mode119,4026
-(defun bufhist-get-buffer-contents 141,4907
-(defun bufhist-restore-buffer-contents 150,5249
-(defun bufhist-checkpoint 159,5563
-(defun bufhist-erase-buffer 167,5932
-(defun bufhist-checkpoint-and-erase 178,6303
-(defun bufhist-switch-to-index 184,6489
-(defun bufhist-first 223,8088
-(defun bufhist-last 228,8247
-(defun bufhist-prev 233,8391
-(defun bufhist-next 241,8614
-(defun bufhist-delete 246,8754
-(defun bufhist-clear 258,9295
-(defun bufhist-init 273,9690
-(defun bufhist-exit 301,10699
-(defun bufhist-set-readwrite 311,10963
-(defun bufhist-before-change-function 326,11583
-(define-button-type 'bufhist-nextbufhist-next
340,12006
-(define-button-type 'bufhist-prevbufhist-prev
344,12103
-(defun bufhist-insert-buttons 351,12315
+(defun bufhist-ring-update 38,1391
+(defgroup bufhist 47,1713
+(defcustom bufhist-ring-size 51,1794
+(defvar bufhist-ring 56,1905
+(defvar bufhist-ring-pos 59,1979
+(defvar bufhist-lastswitch-modified-tick 62,2058
+(defvar bufhist-read-only-history 65,2164
+(defvar bufhist-saved-mode-line-format 68,2235
+(defvar bufhist-normal-read-only 71,2338
+(defvar bufhist-top-point 74,2432
+(defun bufhist-mode-line-format-entry 77,2522
+(defconst bufhist-minor-mode-map106,3596
+(define-minor-mode bufhist-mode119,4073
+(defun bufhist-get-buffer-contents 141,4954
+(defun bufhist-restore-buffer-contents 150,5296
+(defun bufhist-checkpoint 159,5610
+(defun bufhist-erase-buffer 167,5979
+(defun bufhist-checkpoint-and-erase 178,6350
+(defun bufhist-switch-to-index 184,6536
+(defun bufhist-first 223,8135
+(defun bufhist-last 228,8294
+(defun bufhist-prev 233,8438
+(defun bufhist-next 241,8661
+(defun bufhist-delete 246,8801
+(defun bufhist-clear 258,9342
+(defun bufhist-init 273,9737
+(defun bufhist-exit 301,10746
+(defun bufhist-set-readwrite 311,11010
+(defun bufhist-before-change-function 326,11630
+(define-button-type 'bufhist-nextbufhist-next
340,12053
+(define-button-type 'bufhist-prevbufhist-prev
344,12150
+(defun bufhist-insert-buttons 351,12362
 
 lib/holes.el,2465
-(defvar holes-default-hole 44,1076
-(defvar holes-active-hole 50,1254
-(defgroup holes 60,1451
-(defcustom holes-empty-hole-string 65,1550
-(defcustom holes-empty-hole-regexp 70,1693
-(defface active-hole-face92,2395
-(defface inactive-hole-face102,2811
-(defvar hole-map116,3252
-(defvar holes-mode-map126,3643
-(defun holes-region-beginning-or-nil 172,5380
-(defun holes-region-end-or-nil 176,5516
-(defun holes-copy-active-region 180,5634
-(defun holes-is-hole-p 186,5844
-(defun holes-hole-start-position 190,5936
-(defun holes-hole-end-position 196,6119
-(defun holes-hole-buffer 201,6290
-(defun holes-hole-at 207,6464
-(defun holes-active-hole-exist-p 212,6634
-(defun holes-active-hole-start-position 219,6887
-(defun holes-active-hole-end-position 227,7255
-(defun holes-active-hole-buffer 236,7618
-(defun holes-goto-active-hole 244,7919
-(defun holes-highlight-hole-as-active 253,8178
-(defun holes-highlight-hole 261,8486
-(defun holes-disable-active-hole 269,8773
-(defun holes-set-active-hole 282,9305
-(defun holes-is-in-hole-p 292,9650
-(defun holes-make-hole 296,9788
-(defun holes-make-hole-at 314,10444
-(defun holes-clear-hole 328,10897
-(defun holes-clear-hole-at 337,11155
-(defun holes-map-holes 345,11411
-(defun holes-clear-all-buffer-holes 349,11565
-(defun holes-next 359,11866
-(defun holes-next-after-active-hole 366,12118
-(defun holes-set-active-hole-next 373,12334
-(defun holes-replace-segment 392,12871
-(defun holes-replace 401,13224
-(defun holes-replace-active-hole 429,14402
-(defun holes-replace-update-active-hole 436,14693
-(defun holes-delete-update-active-hole 454,15340
-(defun holes-set-make-active-hole 462,15567
-(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16122
-(defsubst holes-track-mouse-clicks 478,16180
-(defun holes-mouse-replace-active-hole 482,16290
-(defun holes-destroy-hole 496,16761
-(defsubst holes-hole-at-event 510,17143
-(defun holes-mouse-destroy-hole 514,17243
-(defun holes-mouse-forget-hole 521,17464
-(defun holes-mouse-set-make-active-hole 531,17756
-(defun holes-mouse-set-active-hole 547,18255
-(defun holes-set-point-next-hole-destroy 556,18506
-(defun holes-replace-string-by-holes-backward 582,19487
-(defun holes-skeleton-end-hook 600,20187
-(defconst holes-jump-doc609,20625
-(defun holes-replace-string-by-holes-backward-jump 616,20831
-(define-minor-mode holes-mode 633,21513
-(defun holes-abbrev-complete 728,24995
-(defun holes-insert-and-expand 738,25338
+(defvar holes-default-hole 44,1121
+(defvar holes-active-hole 50,1299
+(defgroup holes 60,1496
+(defcustom holes-empty-hole-string 65,1595
+(defcustom holes-empty-hole-regexp 70,1738
+(defface active-hole-face92,2440
+(defface inactive-hole-face102,2856
+(defvar hole-map116,3297
+(defvar holes-mode-map126,3688
+(defun holes-region-beginning-or-nil 172,5425
+(defun holes-region-end-or-nil 176,5561
+(defun holes-copy-active-region 180,5679
+(defun holes-is-hole-p 186,5889
+(defun holes-hole-start-position 190,5981
+(defun holes-hole-end-position 196,6164
+(defun holes-hole-buffer 201,6335
+(defun holes-hole-at 207,6509
+(defun holes-active-hole-exist-p 212,6679
+(defun holes-active-hole-start-position 219,6932
+(defun holes-active-hole-end-position 227,7300
+(defun holes-active-hole-buffer 236,7663
+(defun holes-goto-active-hole 244,7964
+(defun holes-highlight-hole-as-active 253,8223
+(defun holes-highlight-hole 261,8531
+(defun holes-disable-active-hole 269,8818
+(defun holes-set-active-hole 282,9350
+(defun holes-is-in-hole-p 292,9695
+(defun holes-make-hole 296,9833
+(defun holes-make-hole-at 314,10489
+(defun holes-clear-hole 328,10942
+(defun holes-clear-hole-at 337,11200
+(defun holes-map-holes 345,11456
+(defun holes-clear-all-buffer-holes 349,11610
+(defun holes-next 359,11911
+(defun holes-next-after-active-hole 366,12163
+(defun holes-set-active-hole-next 373,12379
+(defun holes-replace-segment 392,12916
+(defun holes-replace 401,13269
+(defun holes-replace-active-hole 429,14447
+(defun holes-replace-update-active-hole 436,14738
+(defun holes-delete-update-active-hole 454,15385
+(defun holes-set-make-active-hole 462,15612
+(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16167
+(defsubst holes-track-mouse-clicks 478,16225
+(defun holes-mouse-replace-active-hole 482,16335
+(defun holes-destroy-hole 496,16806
+(defsubst holes-hole-at-event 510,17188
+(defun holes-mouse-destroy-hole 514,17288
+(defun holes-mouse-forget-hole 521,17509
+(defun holes-mouse-set-make-active-hole 531,17801
+(defun holes-mouse-set-active-hole 547,18300
+(defun holes-set-point-next-hole-destroy 556,18551
+(defun holes-replace-string-by-holes-backward 582,19532
+(defun holes-skeleton-end-hook 600,20232
+(defconst holes-jump-doc609,20670
+(defun holes-replace-string-by-holes-backward-jump 616,20876
+(define-minor-mode holes-mode 633,21558
+(defun holes-abbrev-complete 728,25040
+(defun holes-insert-and-expand 738,25383
 
 lib/local-vars-list.el,373
-(defconst local-vars-list-doc 28,770
-(defun local-vars-list-insert-empty-zone 44,1332
-(defun local-vars-list-find 82,2035
-(defun local-vars-list-goto-var 101,2806
-(defun local-vars-list-get-current 127,3853
-(defun local-vars-list-set-current 148,4703
-(defun local-vars-list-get 171,5418
-(defun local-vars-list-get-safe 188,5948
-(defun local-vars-list-set 193,6142
+(defconst local-vars-list-doc 28,825
+(defun local-vars-list-insert-empty-zone 44,1387
+(defun local-vars-list-find 82,2090
+(defun local-vars-list-goto-var 101,2861
+(defun local-vars-list-get-current 127,3908
+(defun local-vars-list-set-current 148,4758
+(defun local-vars-list-get 171,5473
+(defun local-vars-list-get-safe 188,6003
+(defun local-vars-list-set 193,6197
 
 lib/maths-menu.el,242
-(defvar maths-menu-filter-predicate 56,2267
-(defvar maths-menu-tokenise-insert 59,2376
-(defun maths-menu-build-menu 62,2513
-(defvar maths-menu-menu84,3274
-(defvar maths-menu-mode-map344,12832
-(define-minor-mode maths-menu-mode352,13051
+(defvar maths-menu-filter-predicate 56,2317
+(defvar maths-menu-tokenise-insert 59,2426
+(defun maths-menu-build-menu 62,2563
+(defvar maths-menu-menu84,3324
+(defvar maths-menu-mode-map344,12882
+(define-minor-mode maths-menu-mode352,13101
 
 lib/pg-dev.el,199
-(defconst pg-dev-lisp-font-lock-keywords52,1534
-(defun pg-loadpath 78,2233
-(defun unload-pg 88,2404
-(defun profile-pg 119,3298
-(defun elp-pack-number 149,4405
-(defun pg-bug-references 158,4605
+(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,671
-(defvar pg-fontsets-names 29,817
-(defun pg-fontsets-make-fontsetsizes 32,898
-(defconst pg-fontsets-base-fonts51,1659
-(defun pg-fontsets-make-fontsets 57,1789
+(defcustom pg-fontsets-default-fontset 24,722
+(defvar pg-fontsets-names 29,868
+(defun pg-fontsets-make-fontsetsizes 32,949
+(defconst pg-fontsets-base-fonts51,1710
+(defun pg-fontsets-make-fontsets 57,1840
 
 lib/proof-compat.el,160
-(defvar proof-running-on-win32 32,923
-(defun pg-custom-undeclare-variable 53,1725
-(defmacro save-selected-frame 86,2550
-(defmacro declare-function 152,4558
-
-lib/scomint.el,787
-(defvar scomint-buffer-maximum-size 19,446
-(defvar scomint-output-filter-functions 24,637
-(defvar scomint-mode-map27,747
-(defvar scomint-last-input-start 33,926
-(defvar scomint-last-input-end 34,964
-(defvar scomint-last-output-start 35,1000
-(defvar scomint-exec-hook 37,1040
-(define-derived-mode scomint-mode 46,1383
-(defsubst scomint-check-proc 65,2298
-(defun scomint-make-in-buffer 73,2638
-(defun scomint-make 97,3905
-(defun scomint-exec 110,4616
-(defun scomint-exec-1 147,6209
-(defalias 'scomint-send-string scomint-send-string
197,8339
-(defun scomint-send-eof 199,8393
-(defun scomint-send-input 208,8626
-(defun scomint-truncate-buffer 234,9522
-(defun scomint-strip-ctrl-m 247,9916
-(defun scomint-output-filter 261,10493
-(defun scomint-interrupt-process 284,11248
+(defvar proof-running-on-win32 32,975
+(defun pg-custom-undeclare-variable 53,1777
+(defmacro save-selected-frame 86,2602
+(defmacro declare-function 152,4610
+
+lib/scomint.el,788
+(defvar scomint-buffer-maximum-size 19,493
+(defvar scomint-output-filter-functions 24,684
+(defvar scomint-mode-map27,794
+(defvar scomint-last-input-start 33,973
+(defvar scomint-last-input-end 34,1011
+(defvar scomint-last-output-start 35,1047
+(defvar scomint-exec-hook 37,1087
+(define-derived-mode scomint-mode 46,1430
+(defsubst scomint-check-proc 65,2345
+(defun scomint-make-in-buffer 73,2685
+(defun scomint-make 97,3952
+(defun scomint-exec 110,4663
+(defun scomint-exec-1 147,6256
+(defalias 'scomint-send-string scomint-send-string
197,8386
+(defun scomint-send-eof 199,8440
+(defun scomint-send-input 208,8673
+(defun scomint-truncate-buffer 234,9569
+(defun scomint-strip-ctrl-m 247,9963
+(defun scomint-output-filter 261,10540
+(defun scomint-interrupt-process 284,11295
 
 lib/span.el,1553
-(defalias 'span-start span-start
22,565
-(defalias 'span-end span-end
23,603
-(defalias 'span-set-property span-set-property
24,637
-(defalias 'span-property span-property
25,680
-(defalias 'span-make span-make
26,719
-(defalias 'span-detach span-detach
27,755
-(defalias 'span-set-endpoints span-set-endpoints
28,795
-(defalias 'span-buffer span-buffer
29,840
-(defun span-read-only-hook 31,881
-(defsubst span-read-only 36,1071
-(defsubst span-read-write 43,1381
-(defsubst span-write-warning 48,1551
-(defsubst span-lt 59,2075
-(defsubst spans-at-point-prop 64,2219
-(defsubst spans-at-region-prop 73,2410
-(defsubst span-at 83,2676
-(defsubst span-delete 87,2802
-(defsubst span-add-delete-action 93,2998
-(defsubst span-mapcar-spans 99,3277
-(defsubst span-mapc-spans 103,3452
-(defsubst span-mapcar-spans-inorder 107,3623
-(defun span-at-before 113,3828
-(defsubst prev-span 130,4552
-(defsubst next-span 136,4705
-(defsubst span-live-p 142,4919
-(defsubst span-raise 148,5085
-(defsubst span-string 152,5218
-(defsubst set-span-properties 157,5378
-(defsubst span-find-span 163,5572
-(defsubst span-at-event 171,5884
-(defun fold-spans 177,6081
-(defsubst span-detached-p 191,6614
-(defsubst set-span-face 195,6730
-(defsubst set-span-keymap 199,6828
-(defsubst span-delete-spans 207,6997
-(defsubst span-property-safe 211,7159
-(defsubst span-set-start 215,7296
-(defsubst span-set-end 219,7428
-(defun span-make-self-removing-span 227,7588
-(defun span-delete-self-modification-hook 237,7956
-(defun span-make-modifying-removing-span 242,8130
+(defalias 'span-start span-start
22,609
+(defalias 'span-end span-end
23,647
+(defalias 'span-set-property span-set-property
24,681
+(defalias 'span-property span-property
25,724
+(defalias 'span-make span-make
26,763
+(defalias 'span-detach span-detach
27,799
+(defalias 'span-set-endpoints span-set-endpoints
28,839
+(defalias 'span-buffer span-buffer
29,884
+(defun span-read-only-hook 31,925
+(defsubst span-read-only 36,1115
+(defsubst span-read-write 43,1425
+(defsubst span-write-warning 48,1595
+(defsubst span-lt 59,2119
+(defsubst spans-at-point-prop 64,2263
+(defsubst spans-at-region-prop 73,2454
+(defsubst span-at 83,2720
+(defsubst span-delete 87,2846
+(defsubst span-add-delete-action 93,3042
+(defsubst span-mapcar-spans 99,3321
+(defsubst span-mapc-spans 103,3496
+(defsubst span-mapcar-spans-inorder 107,3667
+(defun span-at-before 113,3872
+(defsubst prev-span 130,4596
+(defsubst next-span 136,4749
+(defsubst span-live-p 142,4963
+(defsubst span-raise 148,5129
+(defsubst span-string 152,5262
+(defsubst set-span-properties 157,5422
+(defsubst span-find-span 163,5616
+(defsubst span-at-event 171,5928
+(defun fold-spans 177,6125
+(defsubst span-detached-p 191,6658
+(defsubst set-span-face 195,6774
+(defsubst set-span-keymap 199,6872
+(defsubst span-delete-spans 207,7041
+(defsubst span-property-safe 211,7203
+(defsubst span-set-start 215,7340
+(defsubst span-set-end 219,7472
+(defun span-make-self-removing-span 227,7632
+(defun span-delete-self-modification-hook 237,8000
+(defun span-make-modifying-removing-span 242,8174
 
 lib/texi-docstring-magic.el,584
-(defun texi-docstring-magic-find-face 88,2967
-(defun texi-docstring-magic-splice-sep 93,3132
-(defconst texi-docstring-magic-munge-table103,3437
-(defun texi-docstring-magic-untabify 193,7200
-(defun texi-docstring-magic-munge-docstring 200,7398
-(defun texi-docstring-magic-texi 239,8679
-(defun texi-docstring-magic-format-default 252,9119
-(defun texi-docstring-magic-texi-for 268,9752
-(defconst texi-docstring-magic-comment326,11711
-(defun texi-docstring-magic 332,11865
-(defun texi-docstring-magic-face-at-point 366,12944
-(defun texi-docstring-magic-insert-magic 381,13467
+(defun texi-docstring-magic-find-face 88,3027
+(defun texi-docstring-magic-splice-sep 93,3192
+(defconst texi-docstring-magic-munge-table103,3497
+(defun texi-docstring-magic-untabify 193,7260
+(defun texi-docstring-magic-munge-docstring 200,7458
+(defun texi-docstring-magic-texi 239,8739
+(defun texi-docstring-magic-format-default 252,9179
+(defun texi-docstring-magic-texi-for 268,9812
+(defconst texi-docstring-magic-comment326,11771
+(defun texi-docstring-magic 332,11925
+(defun texi-docstring-magic-face-at-point 366,13004
+(defun texi-docstring-magic-insert-magic 381,13527
 
 lib/unicode-chars.el,80
-(defvar unicode-chars-alist12,295
-(defun unicode-chars-list-chars 5051,245922
-
-lib/unicode-tokens.el,5900
-(defgroup unicode-tokens-options 55,1657
-(defcustom unicode-tokens-add-help-echo 60,1782
-(defun unicode-tokens-toggle-add-help-echo 65,1949
-(defvar unicode-tokens-token-symbol-map 79,2355
-(defvar unicode-tokens-token-format 98,3014
-(defvar unicode-tokens-token-variant-format-regexp 104,3263
-(defvar unicode-tokens-shortcut-alist 118,3796
-(defvar unicode-tokens-shortcut-replacement-alist 124,4073
-(defvar unicode-tokens-control-region-format-regexp 132,4279
-(defvar unicode-tokens-control-char-format-regexp 139,4647
-(defvar unicode-tokens-control-regions 146,5008
-(defvar unicode-tokens-control-characters 149,5084
-(defvar unicode-tokens-control-char-format 152,5166
-(defvar unicode-tokens-control-region-format-start 155,5279
-(defvar unicode-tokens-control-region-format-end 158,5396
-(defvar unicode-tokens-tokens-customizable-variables 161,5509
-(defconst unicode-tokens-configuration-variables168,5677
-(defun unicode-tokens-config 183,6076
-(defun unicode-tokens-config-var 187,6221
-(defun unicode-tokens-copy-configuration-variables 199,6661
-(defvar unicode-tokens-token-list 227,7877
-(defvar unicode-tokens-hash-table 230,7997
-(defvar unicode-tokens-token-match-regexp 233,8113
-(defvar unicode-tokens-uchar-hash-table 239,8396
-(defvar unicode-tokens-uchar-regexp 243,8583
-(defgroup unicode-tokens-faces 251,8768
-(defconst unicode-tokens-font-family-alternatives261,9070
-(defface unicode-tokens-symbol-font-face276,9588
-(defface unicode-tokens-script-font-face286,9946
-(defface unicode-tokens-fraktur-font-face291,10090
-(defface unicode-tokens-serif-font-face296,10215
-(defface unicode-tokens-sans-font-face301,10352
-(defface unicode-tokens-highlight-face306,10474
-(defconst unicode-tokens-fonts315,10836
-(defconst unicode-tokens-fontsymb-properties324,11053
-(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
352,12674
-(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
370,13226
-(defconst unicode-tokens-font-lock-extra-managed-props383,13557
-(defun unicode-tokens-font-lock-keywords 387,13711
-(defun unicode-tokens-calculate-token-match 420,15082
-(defun unicode-tokens-usable-composition 450,16118
-(defun unicode-tokens-help-echo 463,16497
-(defvar unicode-tokens-show-symbols 468,16699
-(defun unicode-tokens-interpret-composition 471,16813
-(defun unicode-tokens-font-lock-compose-symbol 489,17325
-(defun unicode-tokens-prepend-text-properties-in-match 527,18857
-(defun unicode-tokens-prepend-text-property 541,19435
-(defun unicode-tokens-show-symbols 566,20580
-(defun unicode-tokens-symbs-to-props 574,20890
-(defvar unicode-tokens-show-controls 594,21589
-(defun unicode-tokens-show-controls 597,21680
-(defun unicode-tokens-control-char 609,22193
-(defun unicode-tokens-control-region 618,22632
-(defun unicode-tokens-control-font-lock-keywords 629,23179
-(defvar unicode-tokens-use-shortcuts 640,23503
-(defun unicode-tokens-use-shortcuts 643,23606
-(defun unicode-tokens-map-ordering 659,24202
-(defun unicode-tokens-quail-define-rules 668,24555
-(defun unicode-tokens-insert-token 691,25232
-(defun unicode-tokens-annotate-region 700,25536
-(defun unicode-tokens-insert-control 724,26374
-(defun unicode-tokens-insert-uchar-as-token 734,26823
-(defun unicode-tokens-delete-token-near-point 740,27044
-(defun unicode-tokens-delete-backward-char 752,27485
-(defun unicode-tokens-delete-char 763,27866
-(defun unicode-tokens-delete-backward-1 774,28220
-(defun unicode-tokens-delete-1 791,28816
-(defun unicode-tokens-prev-token 807,29360
-(defun unicode-tokens-rotate-token-forward 815,29657
-(defun unicode-tokens-rotate-token-backward 842,30547
-(defun unicode-tokens-replace-shortcut-match 847,30749
-(defun unicode-tokens-replace-shortcuts 856,31119
-(defun unicode-tokens-replace-unicode-match 870,31717
-(defun unicode-tokens-replace-unicode 877,32018
-(defun unicode-tokens-copy-token 894,32617
-(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32838
-(defun unicode-tokens-list-tokens 907,33042
-(defun unicode-tokens-list-shortcuts 946,34226
-(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34864
-(defun unicode-tokens-encode-in-temp-buffer 966,34937
-(defun unicode-tokens-encode 984,35593
-(defun unicode-tokens-encode-str 990,35829
-(defun unicode-tokens-copy 994,35991
-(defun unicode-tokens-paste 1003,36397
-(defvar unicode-tokens-highlight-unicode 1022,37118
-(defconst unicode-tokens-unicode-highlight-patterns1025,37210
-(defun unicode-tokens-highlight-unicode 1029,37379
-(defun unicode-tokens-highlight-unicode-setkeywords 1041,37842
-(defun unicode-tokens-initialise 1053,38211
-(defvar unicode-tokens-mode-map 1073,38882
-(defvar unicode-tokens-display-table1076,38979
-(define-minor-mode unicode-tokens-mode1083,39230
-(defun unicode-tokens-set-font-var 1219,43805
-(defun unicode-tokens-set-font-var-aux 1235,44294
-(defun unicode-tokens-mouse-set-font 1266,45455
-(defsubst unicode-tokens-face-font-sym 1279,45969
-(defun unicode-tokens-set-font-restart 1283,46149
-(defun unicode-tokens-save-fonts 1294,46459
-(defun unicode-tokens-custom-save-faces 1302,46715
-(define-key unicode-tokens-mode-map1319,47171
-(define-key unicode-tokens-mode-map1322,47278
-(defvar unicode-tokens-quail-translation-keymap1330,47537
-(define-key unicode-tokens-quail-translation-keymap1337,47727
-(defun unicode-tokens-quail-delete-last-char 1341,47861
-(define-key unicode-tokens-mode-map 1356,48288
-(define-key unicode-tokens-mode-map 1358,48380
-(define-key unicode-tokens-mode-map1360,48471
-(define-key unicode-tokens-mode-map1362,48577
-(define-key unicode-tokens-mode-map1365,48692
-(define-key unicode-tokens-mode-map1367,48801
-(define-key unicode-tokens-mode-map1369,48909
-(define-key unicode-tokens-mode-map1371,49015
-(defun unicode-tokens-customize-submenu 1379,49139
-(defun unicode-tokens-define-menu 1386,49362
+(defvar unicode-chars-alist12,348
+(defun unicode-chars-list-chars 5051,245975
+
+lib/unicode-tokens.el,5901
+(defgroup unicode-tokens-options 55,1711
+(defcustom unicode-tokens-add-help-echo 60,1836
+(defun unicode-tokens-toggle-add-help-echo 65,2003
+(defvar unicode-tokens-token-symbol-map 79,2409
+(defvar unicode-tokens-token-format 98,3068
+(defvar unicode-tokens-token-variant-format-regexp 104,3317
+(defvar unicode-tokens-shortcut-alist 118,3850
+(defvar unicode-tokens-shortcut-replacement-alist 124,4127
+(defvar unicode-tokens-control-region-format-regexp 132,4333
+(defvar unicode-tokens-control-char-format-regexp 139,4701
+(defvar unicode-tokens-control-regions 146,5062
+(defvar unicode-tokens-control-characters 149,5138
+(defvar unicode-tokens-control-char-format 152,5220
+(defvar unicode-tokens-control-region-format-start 155,5333
+(defvar unicode-tokens-control-region-format-end 158,5450
+(defvar unicode-tokens-tokens-customizable-variables 161,5563
+(defconst unicode-tokens-configuration-variables168,5731
+(defun unicode-tokens-config 183,6130
+(defun unicode-tokens-config-var 187,6275
+(defun unicode-tokens-copy-configuration-variables 199,6715
+(defvar unicode-tokens-token-list 227,7931
+(defvar unicode-tokens-hash-table 230,8051
+(defvar unicode-tokens-token-match-regexp 233,8167
+(defvar unicode-tokens-uchar-hash-table 239,8450
+(defvar unicode-tokens-uchar-regexp 243,8637
+(defgroup unicode-tokens-faces 251,8822
+(defconst unicode-tokens-font-family-alternatives261,9124
+(defface unicode-tokens-symbol-font-face276,9642
+(defface unicode-tokens-script-font-face286,10000
+(defface unicode-tokens-fraktur-font-face291,10144
+(defface unicode-tokens-serif-font-face296,10269
+(defface unicode-tokens-sans-font-face301,10406
+(defface unicode-tokens-highlight-face306,10528
+(defconst unicode-tokens-fonts315,10890
+(defconst unicode-tokens-fontsymb-properties324,11107
+(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
352,12728
+(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
370,13280
+(defconst unicode-tokens-font-lock-extra-managed-props383,13611
+(defun unicode-tokens-font-lock-keywords 387,13765
+(defun unicode-tokens-calculate-token-match 420,15136
+(defun unicode-tokens-usable-composition 450,16172
+(defun unicode-tokens-help-echo 463,16551
+(defvar unicode-tokens-show-symbols 468,16753
+(defun unicode-tokens-interpret-composition 471,16867
+(defun unicode-tokens-font-lock-compose-symbol 489,17379
+(defun unicode-tokens-prepend-text-properties-in-match 527,18911
+(defun unicode-tokens-prepend-text-property 541,19489
+(defun unicode-tokens-show-symbols 566,20634
+(defun unicode-tokens-symbs-to-props 574,20944
+(defvar unicode-tokens-show-controls 594,21643
+(defun unicode-tokens-show-controls 597,21734
+(defun unicode-tokens-control-char 609,22247
+(defun unicode-tokens-control-region 618,22686
+(defun unicode-tokens-control-font-lock-keywords 629,23233
+(defvar unicode-tokens-use-shortcuts 640,23557
+(defun unicode-tokens-use-shortcuts 643,23660
+(defun unicode-tokens-map-ordering 659,24256
+(defun unicode-tokens-quail-define-rules 668,24609
+(defun unicode-tokens-insert-token 691,25286
+(defun unicode-tokens-annotate-region 700,25590
+(defun unicode-tokens-insert-control 724,26428
+(defun unicode-tokens-insert-uchar-as-token 734,26877
+(defun unicode-tokens-delete-token-near-point 740,27098
+(defun unicode-tokens-delete-backward-char 752,27539
+(defun unicode-tokens-delete-char 763,27920
+(defun unicode-tokens-delete-backward-1 774,28274
+(defun unicode-tokens-delete-1 791,28870
+(defun unicode-tokens-prev-token 807,29414
+(defun unicode-tokens-rotate-token-forward 815,29711
+(defun unicode-tokens-rotate-token-backward 842,30601
+(defun unicode-tokens-replace-shortcut-match 847,30803
+(defun unicode-tokens-replace-shortcuts 856,31173
+(defun unicode-tokens-replace-unicode-match 870,31771
+(defun unicode-tokens-replace-unicode 877,32072
+(defun unicode-tokens-copy-token 894,32671
+(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32892
+(defun unicode-tokens-list-tokens 907,33096
+(defun unicode-tokens-list-shortcuts 946,34280
+(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34918
+(defun unicode-tokens-encode-in-temp-buffer 966,34991
+(defun unicode-tokens-encode 984,35647
+(defun unicode-tokens-encode-str 990,35883
+(defun unicode-tokens-copy 994,36045
+(defun unicode-tokens-paste 1003,36451
+(defvar unicode-tokens-highlight-unicode 1022,37172
+(defconst unicode-tokens-unicode-highlight-patterns1025,37264
+(defun unicode-tokens-highlight-unicode 1029,37433
+(defun unicode-tokens-highlight-unicode-setkeywords 1041,37896
+(defun unicode-tokens-initialise 1053,38265
+(defvar unicode-tokens-mode-map 1073,38936
+(defvar unicode-tokens-display-table1076,39033
+(define-minor-mode unicode-tokens-mode1083,39284
+(defun unicode-tokens-set-font-var 1219,43859
+(defun unicode-tokens-set-font-var-aux 1235,44348
+(defun unicode-tokens-mouse-set-font 1266,45509
+(defsubst unicode-tokens-face-font-sym 1279,46023
+(defun unicode-tokens-set-font-restart 1283,46203
+(defun unicode-tokens-save-fonts 1294,46513
+(defun unicode-tokens-custom-save-faces 1302,46769
+(define-key unicode-tokens-mode-map1319,47225
+(define-key unicode-tokens-mode-map1322,47332
+(defvar unicode-tokens-quail-translation-keymap1330,47591
+(define-key unicode-tokens-quail-translation-keymap1337,47781
+(defun unicode-tokens-quail-delete-last-char 1341,47915
+(define-key unicode-tokens-mode-map 1356,48342
+(define-key unicode-tokens-mode-map 1358,48434
+(define-key unicode-tokens-mode-map1360,48525
+(define-key unicode-tokens-mode-map1362,48631
+(define-key unicode-tokens-mode-map1365,48746
+(define-key unicode-tokens-mode-map1367,48855
+(define-key unicode-tokens-mode-map1369,48963
+(define-key unicode-tokens-mode-map1371,49069
+(defun unicode-tokens-customize-submenu 1379,49193
+(defun unicode-tokens-define-menu 1386,49416
 
 contrib/mmm/mmm-auto.el,343
-(defvar mmm-autoloaded-classes67,2628
-(defun mmm-autoload-class 89,3391
-(defvar mmm-changed-buffers-list 129,4944
-(defun mmm-major-mode-change 132,5051
-(defun mmm-check-changed-buffers 145,5572
-(defun mmm-mode-on-maybe 154,5922
-(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
166,6326
-(defun mmm-add-find-file-hook 167,6386
+(defvar mmm-autoloaded-classes67,2676
+(defun mmm-autoload-class 89,3439
+(defvar mmm-changed-buffers-list 129,4992
+(defun mmm-major-mode-change 132,5099
+(defun mmm-check-changed-buffers 145,5620
+(defun mmm-mode-on-maybe 154,5970
+(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
166,6374
+(defun mmm-add-find-file-hook 167,6434
 
 contrib/mmm/mmm-class.el,415
-(defun mmm-get-class-spec 42,1247
-(defun mmm-get-class-parameter 59,1890
-(defun mmm-set-class-parameter 63,2056
-(defun* mmm-apply-class75,2406
-(defun* mmm-apply-classes90,3023
-(defun* mmm-apply-all 110,3754
-(defun* mmm-ify124,4201
-(defun* mmm-match-region206,7046
-(defun mmm-match->point 269,9431
-(defun mmm-match-and-verify 284,10001
-(defun mmm-get-form 310,11052
-(defun mmm-default-get-form 321,11527
+(defun mmm-get-class-spec 42,1296
+(defun mmm-get-class-parameter 59,1939
+(defun mmm-set-class-parameter 63,2105
+(defun* mmm-apply-class75,2455
+(defun* mmm-apply-classes90,3072
+(defun* mmm-apply-all 110,3803
+(defun* mmm-ify124,4250
+(defun* mmm-match-region206,7095
+(defun mmm-match->point 269,9480
+(defun mmm-match-and-verify 284,10050
+(defun mmm-get-form 310,11101
+(defun mmm-default-get-form 321,11576
 
 contrib/mmm/mmm-cmds.el,712
-(defun mmm-ify-by-class 41,1162
-(defun mmm-ify-region 63,1774
-(defun mmm-ify-by-regexp75,2195
-(defun mmm-parse-buffer 97,2838
-(defun mmm-parse-region 106,3174
-(defun mmm-parse-block 115,3553
-(defun mmm-get-block 132,4304
-(defun mmm-reparse-current-region 146,4586
-(defun mmm-clear-current-region 167,5162
-(defun mmm-clear-regions 172,5326
-(defun mmm-clear-all-regions 177,5472
-(defun* mmm-end-current-region 185,5632
-(defun mmm-narrow-to-submode-region 220,6880
-(defun mmm-insert-region 239,7494
-(defun mmm-insert-by-key 258,8300
-(defun mmm-get-insertion-spec 342,11565
-(defun mmm-insertion-help 369,12525
-(defun mmm-display-insertion-key 379,12888
-(defun mmm-get-all-insertion-keys 401,13675
+(defun mmm-ify-by-class 41,1210
+(defun mmm-ify-region 63,1822
+(defun mmm-ify-by-regexp75,2243
+(defun mmm-parse-buffer 97,2886
+(defun mmm-parse-region 106,3222
+(defun mmm-parse-block 115,3601
+(defun mmm-get-block 132,4352
+(defun mmm-reparse-current-region 146,4634
+(defun mmm-clear-current-region 167,5210
+(defun mmm-clear-regions 172,5374
+(defun mmm-clear-all-regions 177,5520
+(defun* mmm-end-current-region 185,5680
+(defun mmm-narrow-to-submode-region 220,6928
+(defun mmm-insert-region 239,7542
+(defun mmm-insert-by-key 258,8348
+(defun mmm-get-insertion-spec 342,11613
+(defun mmm-insertion-help 369,12573
+(defun mmm-display-insertion-key 379,12936
+(defun mmm-get-all-insertion-keys 401,13723
 
 contrib/mmm/mmm-compat.el,418
-(defvar mmm-xemacs 40,1263
-(defvar mmm-keywords-used49,1566
-(defmacro mmm-regexp-opt 91,2582
-(defvar mmm-evaporate-property110,3231
-(defmacro mmm-set-keymap-default 128,3997
-(defmacro mmm-event-key 137,4439
-(defvar skeleton-positions 146,4658
-(defun mmm-fixup-skeleton 147,4689
-(defmacro mmm-make-temp-buffer 159,5112
-(defvar mmm-font-lock-available-p 172,5508
-(defmacro mmm-set-font-lock-defaults 179,5722
+(defvar mmm-xemacs 40,1313
+(defvar mmm-keywords-used49,1616
+(defmacro mmm-regexp-opt 91,2632
+(defvar mmm-evaporate-property110,3281
+(defmacro mmm-set-keymap-default 128,4047
+(defmacro mmm-event-key 137,4489
+(defvar skeleton-positions 146,4708
+(defun mmm-fixup-skeleton 147,4739
+(defmacro mmm-make-temp-buffer 159,5162
+(defvar mmm-font-lock-available-p 172,5558
+(defmacro mmm-set-font-lock-defaults 179,5772
 
 contrib/mmm/mmm-cweb.el,228
-(defvar mmm-cweb-section-tags38,1069
-(defvar mmm-cweb-section-regexp41,1116
-(defvar mmm-cweb-c-part-tags44,1206
-(defvar mmm-cweb-c-part-regexp47,1265
-(defun mmm-cweb-in-limbo 50,1349
-(defun mmm-cweb-verify-brief-c 57,1574
+(defvar mmm-cweb-section-tags38,1117
+(defvar mmm-cweb-section-regexp41,1164
+(defvar mmm-cweb-c-part-tags44,1254
+(defvar mmm-cweb-c-part-regexp47,1313
+(defun mmm-cweb-in-limbo 50,1397
+(defun mmm-cweb-verify-brief-c 57,1622
 
 contrib/mmm/mmm-mason.el,410
-(defvar mmm-mason-perl-tags41,1187
-(defvar mmm-mason-pseudo-perl-tags45,1328
-(defvar mmm-mason-non-perl-tags48,1404
-(defvar mmm-mason-perl-tags-regexp51,1505
-(defvar mmm-mason-pseudo-perl-tags-regexp56,1700
-(defvar mmm-mason-tag-names-regexp61,1917
-(defun mmm-mason-verify-inline 66,2137
-(defun mmm-mason-start-line 156,4789
-(defun mmm-mason-end-line 161,4854
-(defun mmm-mason-set-mode-line 168,4948
-
-contrib/mmm/mmm-mode.el,1024
-(defun mmm-mode 101,3819
-(defun mmm-mode-on 140,5324
-(defun mmm-mode-off 183,7108
-(defvar mmm-mode-map 209,7849
-(defvar mmm-mode-prefix-map 212,7924
-(defvar mmm-mode-menu-map 215,8034
-(defun mmm-define-key 218,8125
-(define-key mmm-mode-prefix-map 242,8880
-(define-key mmm-mode-prefix-map 249,9138
-(define-key mmm-mode-map 252,9249
-(define-key mmm-mode-menu-map 255,9351
-(define-key mmm-mode-menu-map 257,9423
-(define-key mmm-mode-menu-map 259,9482
-(define-key mmm-mode-menu-map 261,9563
-(define-key mmm-mode-menu-map 263,9644
-(define-key mmm-mode-menu-map 265,9731
-(define-key mmm-mode-menu-map 268,9825
-(define-key mmm-mode-menu-map 270,9885
-(define-key mmm-mode-menu-map 273,9976
-(define-key mmm-mode-menu-map 275,10036
-(define-key mmm-mode-menu-map 277,10143
-(define-key mmm-mode-menu-map 279,10228
-(define-key mmm-mode-menu-map 282,10314
-(define-key mmm-mode-menu-map 284,10374
-(define-key mmm-mode-menu-map 286,10487
-(define-key mmm-mode-menu-map 288,10572
-(define-key mmm-mode-map 291,10655
+(defvar mmm-mason-perl-tags41,1236
+(defvar mmm-mason-pseudo-perl-tags45,1377
+(defvar mmm-mason-non-perl-tags48,1453
+(defvar mmm-mason-perl-tags-regexp51,1554
+(defvar mmm-mason-pseudo-perl-tags-regexp56,1749
+(defvar mmm-mason-tag-names-regexp61,1966
+(defun mmm-mason-verify-inline 66,2186
+(defun mmm-mason-start-line 156,4838
+(defun mmm-mason-end-line 161,4903
+(defun mmm-mason-set-mode-line 168,4997
+
+contrib/mmm/mmm-mode.el,1025
+(defun mmm-mode 101,3867
+(defun mmm-mode-on 140,5372
+(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,1699
-(defun mmm-overlays-at 59,1884
-(defun mmm-included-p 72,2337
-(defun mmm-overlays-containing 112,3826
-(defun mmm-overlays-contained-in 125,4264
-(defun mmm-overlays-overlapping 138,4704
-(defun mmm-sort-overlays 149,5067
-(defvar mmm-current-overlay 158,5309
-(defvar mmm-previous-overlay 163,5524
-(defvar mmm-current-submode 168,5712
-(defvar mmm-previous-submode 173,5912
-(defun mmm-update-current-submode 178,6085
-(defun mmm-set-current-submode 199,6880
-(defun mmm-submode-at 210,7323
-(defun mmm-match-front 219,7598
-(defun mmm-match-back 238,8359
-(defun mmm-front-start 257,9104
-(defun mmm-back-end 265,9408
-(defun mmm-valid-submode-region 278,9755
-(defun* mmm-make-region305,10911
-(defun mmm-make-overlay 431,16261
-(defun mmm-get-face 459,17394
-(defun mmm-clear-overlays 470,17686
-(defun mmm-update-mode-info 486,18151
-(defun mmm-update-submode-region 572,21824
-(defun mmm-add-hooks 589,22554
-(defun mmm-remove-hooks 592,22651
-(defun mmm-get-local-variables-list 598,22778
-(defun mmm-get-locals 618,23474
-(defun mmm-get-saved-local 631,23971
-(defun mmm-set-local-variables 635,24136
-(defun mmm-get-saved-local-variables 646,24514
-(defun mmm-save-changed-local-variables 654,24789
-(defun mmm-clear-local-variables 673,25493
-(defun mmm-enable-font-lock 684,25758
-(defun mmm-update-font-lock-buffer 692,26018
-(defun mmm-refontify-maybe 705,26429
-(defun mmm-submode-changes-in 720,26909
-(defun mmm-regions-in 731,27266
-(defun mmm-regions-alist 745,27744
-(defun mmm-fontify-region 762,28271
-(defun mmm-fontify-region-list 783,29293
-(defun mmm-beginning-of-syntax 805,30041
+(defsubst mmm-overlay-at 54,1749
+(defun mmm-overlays-at 59,1934
+(defun mmm-included-p 72,2387
+(defun mmm-overlays-containing 112,3876
+(defun mmm-overlays-contained-in 125,4314
+(defun mmm-overlays-overlapping 138,4754
+(defun mmm-sort-overlays 149,5117
+(defvar mmm-current-overlay 158,5359
+(defvar mmm-previous-overlay 163,5574
+(defvar mmm-current-submode 168,5762
+(defvar mmm-previous-submode 173,5962
+(defun mmm-update-current-submode 178,6135
+(defun mmm-set-current-submode 199,6930
+(defun mmm-submode-at 210,7373
+(defun mmm-match-front 219,7648
+(defun mmm-match-back 238,8409
+(defun mmm-front-start 257,9154
+(defun mmm-back-end 265,9458
+(defun mmm-valid-submode-region 278,9805
+(defun* mmm-make-region305,10961
+(defun mmm-make-overlay 431,16311
+(defun mmm-get-face 459,17444
+(defun mmm-clear-overlays 470,17736
+(defun mmm-update-mode-info 486,18201
+(defun mmm-update-submode-region 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,1571
-(defvar mmm-rpm-sh-end-tags53,1795
-(defvar mmm-rpm-sh-start-regexp57,1969
-(defvar mmm-rpm-sh-end-regexp61,2147
+(defconst mmm-rpm-sh-start-tags48,1618
+(defvar mmm-rpm-sh-end-tags53,1842
+(defvar mmm-rpm-sh-start-regexp57,2016
+(defvar mmm-rpm-sh-end-regexp61,2194
 
 contrib/mmm/mmm-sample.el,168
-(defvar mmm-here-doc-mode-alist 84,2551
-(defun mmm-here-doc-get-mode 93,3036
-(defun mmm-file-variables-verify 208,6293
-(defun mmm-file-variables-find-back 232,7098
+(defvar mmm-here-doc-mode-alist 84,2601
+(defun mmm-here-doc-get-mode 93,3086
+(defun mmm-file-variables-verify 208,6343
+(defun mmm-file-variables-find-back 232,7148
 
 contrib/mmm/mmm-univ.el,34
 (defun mmm-univ-get-mode 38,1205
 
 contrib/mmm/mmm-utils.el,282
-(defmacro mmm-valid-buffer 42,1283
-(defmacro mmm-save-all 61,1892
-(defun mmm-format-string 74,2174
-(defun mmm-format-matches 85,2612
-(defmacro mmm-save-keyword 108,3370
-(defmacro mmm-save-keywords 116,3697
-(defun mmm-looking-back-at 129,4195
-(defun mmm-make-marker 146,4735
+(defmacro mmm-valid-buffer 42,1332
+(defmacro mmm-save-all 61,1941
+(defun mmm-format-string 74,2223
+(defun mmm-format-matches 85,2661
+(defmacro mmm-save-keyword 108,3419
+(defmacro mmm-save-keywords 116,3746
+(defun mmm-looking-back-at 129,4244
+(defun mmm-make-marker 146,4784
 
 contrib/mmm/mmm-vars.el,2668
-(defgroup mmm 104,3235
-(defvar mmm-c-derived-modes111,3345
-(defvar mmm-save-local-variables115,3464
-(defvar mmm-buffer-saved-locals 341,10245
-(defvar mmm-region-saved-locals-defaults 346,10445
-(defvar mmm-region-saved-locals-for-dominant 352,10705
-(defgroup mmm-faces 362,11082
-(defcustom mmm-submode-decoration-level 368,11253
-(defface mmm-init-submode-face 386,12097
-(defface mmm-cleanup-submode-face 390,12237
-(defface mmm-declaration-submode-face 394,12374
-(defface mmm-comment-submode-face 398,12520
-(defface mmm-output-submode-face 402,12673
-(defface mmm-special-submode-face 406,12822
-(defface mmm-code-submode-face 410,12986
-(defface mmm-default-submode-face 414,13125
-(defface mmm-delimiter-face 419,13333
-(defcustom mmm-mode-string 426,13459
-(defcustom mmm-submode-mode-line-format 431,13590
-(defvar mmm-primary-mode-display-name 448,14245
-(defvar mmm-buffer-mode-display-name 453,14459
-(defun mmm-set-mode-line 459,14758
-(defvar mmm-classes 483,15566
-(defvar mmm-global-classes 489,15811
-(defcustom mmm-mode-ext-classes-alist 496,15993
-(defun mmm-add-mode-ext-class 515,16783
-(defcustom mmm-major-mode-preferences524,17108
-(defun mmm-add-to-major-mode-preferences 542,17836
-(defun mmm-ensure-modename 558,18594
-(defun mmm-modename->function 567,18897
-(defcustom mmm-delimiter-mode 581,19346
-(defcustom mmm-mode-prefix-key 591,19615
-(defcustom mmm-command-modifiers 596,19742
-(defcustom mmm-insert-modifiers 610,20375
-(defcustom mmm-use-old-command-keys 625,21053
-(defun mmm-use-old-command-keys 635,21517
-(defcustom mmm-mode-hook 643,21709
-(defun mmm-run-constructed-hook 663,22516
-(defun mmm-run-major-hook 671,22860
-(defun mmm-run-submode-hook 674,22937
-(defvar mmm-class-hooks-run 677,23024
-(defun mmm-run-class-hook 682,23196
-(defvar mmm-primary-mode-entry-hook 687,23368
-(defcustom mmm-major-mode-hook 702,24015
-(defun mmm-run-major-mode-hook 716,24646
-(defcustom mmm-global-mode 729,25187
-(defcustom mmm-never-modes745,25854
-(defvar mmm-set-file-name-for-modes 763,26154
-(defvar mmm-mode 774,26513
-(defvar mmm-primary-mode 782,26721
-(defvar mmm-classes-alist 793,27087
-(defun mmm-add-classes 948,35294
-(defun mmm-add-group 953,35459
-(defun mmm-add-to-group 963,35832
-(defconst mmm-version 977,36259
-(defun mmm-version 980,36324
-(defvar mmm-temp-buffer-name 987,36467
-(defvar mmm-interactive-history 993,36597
-(defun mmm-add-to-history 999,36866
-(defun mmm-clear-history 1002,36949
-(defvar mmm-mode-ext-classes 1010,37134
-(defun mmm-get-mode-ext-classes 1015,37345
-(defun mmm-clear-mode-ext-classes 1024,37672
-(defun mmm-mode-ext-applies 1028,37797
-(defun mmm-get-all-classes 1042,38176
-
-doc/ProofGeneral.texi,7046
-@node Top145,4126
-@node Preface184,5319
-@node News for Version 4.1News for Version 4.1
208,5933
-@node News for Version 4.0News for Version 4.0
219,6240
-@node Future240,7091
-@node Credits269,8426
-@node Introducing Proof GeneralIntroducing Proof General
391,12535
-@node Installing Proof GeneralInstalling Proof General
446,14509
-@node Quick start guideQuick start guide
460,14958
-@node Features of Proof GeneralFeatures of Proof General
504,17079
-@node Supported proof assistantsSupported proof assistants
610,21623
-@node Prerequisites for this manualPrerequisites for this manual
659,23504
-@node Organization of this manualOrganization of this manual
703,25123
-@node Basic Script ManagementBasic Script Management
729,25951
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
748,26551
-@node Proof scriptsProof scripts
1033,37946
-@node Script buffersScript buffers
1076,40066
-@node Locked queue and editing regionsLocked queue and editing regions
1098,40643
-@node Goal-save sequencesGoal-save sequences
1154,42790
-@node Active scripting bufferActive scripting buffer
1191,44274
-@node Summary of Proof General buffersSummary of Proof General buffers
1264,47907
-@node Script editing commandsScript editing commands
1313,50164
-@node Script processing commandsScript processing commands
1393,53123
-@node Proof assistant commandsProof assistant commands
1519,58368
-@node Toolbar commandsToolbar commands
1712,65296
-@node Interrupting during trace outputInterrupting during trace output
1737,66255
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1777,68185
-@node Document centred workingDocument centred working
1798,68806
-@node Automatic processingAutomatic processing
1910,73484
-@node Visibility of completed proofsVisibility of completed proofs
1965,75532
-@node Switching between proof scriptsSwitching between proof scripts
2020,77472
-@node View of processed files View of processed files 
2057,79444
-@node Retracting across filesRetracting across files
2117,82495
-@node Asserting across filesAsserting across files
2130,83126
-@node Automatic multiple file handlingAutomatic multiple file handling
2143,83692
-@node Escaping script managementEscaping script management
2168,84726
-@node Editing featuresEditing features
2225,86838
-@node Unicode symbols and special layout supportUnicode symbols and special layout support
2295,89617
-@node Maths menuMaths menu
2337,91175
-@node Unicode Tokens modeUnicode Tokens mode
2354,91866
-@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2404,94289
-@node Special layout Special layout 
2434,95250
-@node Moving between Unicode and tokensMoving between Unicode and tokens
2544,99368
-@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2599,101479
-@node Selecting suitable fontsSelecting suitable fonts
2638,102653
-@node Support for other PackagesSupport for other Packages
2703,105641
-@node Syntax highlightingSyntax highlighting
2733,106477
-@node Imenu and SpeedbarImenu and Speedbar
2761,107480
-@node Support for outline modeSupport for outline mode
2807,109151
-@node Support for completionSupport for completion
2832,110280
-@node Support for tagsSupport for tags
2889,112442
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2941,114790
-@node Goals buffer commandsGoals buffer commands
2957,115385
-@node Graphical Proof-Tree VisualizationGraphical Proof-Tree Visualization
3056,119538
-@node Starting and Stopping Proof-Tree VisualizationStarting and Stopping Proof-Tree Visualization
3079,120430
-@node Features of ProoftreeFeatures of Prooftree
3107,121587
-@node Prooftree CustomizationProoftree Customization
3139,122799
-@node Customizing Proof GeneralCustomizing Proof General
3163,123678
-@node Basic optionsBasic options
3203,125348
-@node How to customizeHow to customize
3227,126118
-@node Display customizationDisplay customization
3274,128085
-@node User optionsUser options
3442,135047
-@node Changing facesChanging faces
3678,143715
-@node Script buffer facesScript buffer faces
3700,144590
-@node Goals and response facesGoals and response faces
3746,146190
-@node Tweaking configuration settingsTweaking configuration settings
3791,147722
-@node Hints and TipsHints and Tips
3848,150248
-@node Adding your own keybindingsAdding your own keybindings
3867,150849
-@node Using file variablesUsing file variables
3931,153463
-@node Using abbreviationsUsing abbreviations
4007,156134
-@node LEGO Proof GeneralLEGO Proof General
4046,157549
-@node LEGO specific commandsLEGO specific commands
4087,158918
-@node LEGO tagsLEGO tags
4107,159373
-@node LEGO customizationsLEGO customizations
4117,159620
-@node Coq Proof GeneralCoq Proof General
4149,160539
-@node Coq-specific commandsCoq-specific commands
4165,160905
-@node Multiple File SupportMultiple File Support
4188,161413
-@node Automatic Compilation in DetailAutomatic Compilation in Detail
4258,164002
-@node Locking AncestorsLocking Ancestors
4333,167353
-@node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support
4366,168778
-@node Current LimitationsCurrent Limitations
4598,178548
-@node Editing multiple proofsEditing multiple proofs
4624,179400
-@node User-loaded tacticsUser-loaded tactics
4648,180508
-@node Holes featureHoles feature
4712,182982
-@node Proof-Tree VisualizationProof-Tree Visualization
4737,184201
-@node Isabelle Proof GeneralIsabelle Proof General
4749,184551
-@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4775,185427
-@node Isabelle commandsIsabelle commands
4844,188228
-@node Isabelle settingsIsabelle settings
4987,192420
-@node Isabelle customizationsIsabelle customizations
5001,193002
-@node HOL Proof GeneralHOL Proof General
5024,193489
-@node Shell Proof GeneralShell Proof General
5066,195311
-@node Obtaining and InstallingObtaining and Installing
5102,196770
-@node Obtaining Proof GeneralObtaining Proof General
5117,197135
-@node Installing Proof General from tarballInstalling Proof General from tarball
5143,198017
-@node Setting the names of binariesSetting the names of binaries
5167,198807
-@node Notes for syssiesNotes for syssies
5195,199747
-@node Bugs and EnhancementsBugs and Enhancements
5271,202744
-@node References5292,203559
-@node History of Proof GeneralHistory of Proof General
5332,204582
-@node Old News for 3.0Old News for 3.0
5426,208747
-@node Old News for 3.1Old News for 3.1
5496,212441
-@node Old News for 3.2Old News for 3.2
5522,213613
-@node Old News for 3.3Old News for 3.3
5583,216616
-@node Old News for 3.4Old News for 3.4
5602,217513
-@node Old News for 3.5Old News for 3.5
5624,218568
-@node Old News for 3.6Old News for 3.6
5628,218625
-@node Old News for 3.7Old News for 3.7
5633,218725
-@node Function IndexFunction Index
5663,220179
-@node Variable IndexVariable Index
5667,220255
-@node Keystroke IndexKeystroke Index
5671,220335
-@node Concept IndexConcept Index
5675,220401
+(defgroup mmm 104,3283
+(defvar mmm-c-derived-modes111,3393
+(defvar mmm-save-local-variables115,3512
+(defvar mmm-buffer-saved-locals 341,10293
+(defvar mmm-region-saved-locals-defaults 346,10493
+(defvar mmm-region-saved-locals-for-dominant 352,10753
+(defgroup mmm-faces 362,11130
+(defcustom mmm-submode-decoration-level 368,11301
+(defface mmm-init-submode-face 386,12145
+(defface mmm-cleanup-submode-face 390,12285
+(defface mmm-declaration-submode-face 394,12422
+(defface mmm-comment-submode-face 398,12568
+(defface mmm-output-submode-face 402,12721
+(defface mmm-special-submode-face 406,12870
+(defface mmm-code-submode-face 410,13034
+(defface mmm-default-submode-face 414,13173
+(defface mmm-delimiter-face 419,13381
+(defcustom mmm-mode-string 426,13507
+(defcustom mmm-submode-mode-line-format 431,13638
+(defvar mmm-primary-mode-display-name 448,14293
+(defvar mmm-buffer-mode-display-name 453,14507
+(defun mmm-set-mode-line 459,14806
+(defvar mmm-classes 483,15614
+(defvar mmm-global-classes 489,15859
+(defcustom mmm-mode-ext-classes-alist 496,16041
+(defun mmm-add-mode-ext-class 515,16831
+(defcustom mmm-major-mode-preferences524,17156
+(defun mmm-add-to-major-mode-preferences 542,17884
+(defun mmm-ensure-modename 558,18642
+(defun mmm-modename->function 567,18945
+(defcustom mmm-delimiter-mode 581,19394
+(defcustom mmm-mode-prefix-key 591,19663
+(defcustom mmm-command-modifiers 596,19790
+(defcustom mmm-insert-modifiers 610,20423
+(defcustom mmm-use-old-command-keys 625,21101
+(defun mmm-use-old-command-keys 635,21565
+(defcustom mmm-mode-hook 643,21757
+(defun mmm-run-constructed-hook 663,22564
+(defun mmm-run-major-hook 671,22908
+(defun mmm-run-submode-hook 674,22985
+(defvar mmm-class-hooks-run 677,23072
+(defun mmm-run-class-hook 682,23244
+(defvar mmm-primary-mode-entry-hook 687,23416
+(defcustom mmm-major-mode-hook 702,24063
+(defun mmm-run-major-mode-hook 716,24694
+(defcustom mmm-global-mode 729,25235
+(defcustom mmm-never-modes745,25902
+(defvar mmm-set-file-name-for-modes 763,26202
+(defvar mmm-mode 774,26561
+(defvar mmm-primary-mode 782,26769
+(defvar mmm-classes-alist 793,27135
+(defun mmm-add-classes 948,35342
+(defun mmm-add-group 953,35507
+(defun mmm-add-to-group 963,35880
+(defconst mmm-version 977,36307
+(defun mmm-version 980,36372
+(defvar mmm-temp-buffer-name 987,36515
+(defvar mmm-interactive-history 993,36645
+(defun mmm-add-to-history 999,36914
+(defun mmm-clear-history 1002,36997
+(defvar mmm-mode-ext-classes 1010,37182
+(defun mmm-get-mode-ext-classes 1015,37393
+(defun mmm-clear-mode-ext-classes 1024,37720
+(defun mmm-mode-ext-applies 1028,37845
+(defun mmm-get-all-classes 1042,38224
+
+doc/ProofGeneral.texi,7116
+@node Top145,4234
+@node Preface184,5433
+@node News for Version 4.2News for Version 4.2
209,6072
+@node News for Version 4.1News for Version 4.1
222,6528
+@node News for Version 4.0News for Version 4.0
233,6835
+@node Future254,7686
+@node Credits283,9021
+@node Introducing Proof GeneralIntroducing Proof General
405,13130
+@node Installing Proof GeneralInstalling Proof General
460,15104
+@node Quick start guideQuick start guide
474,15553
+@node Features of Proof GeneralFeatures of Proof General
519,17747
+@node Supported proof assistantsSupported proof assistants
625,22291
+@node Prerequisites for this manualPrerequisites for this manual
677,24281
+@node Organization of this manualOrganization of this manual
721,25900
+@node Basic Script ManagementBasic Script Management
747,26728
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
766,27328
+@node Proof scriptsProof scripts
1051,38723
+@node Script buffersScript buffers
1094,40843
+@node Locked queue and editing regionsLocked queue and editing regions
1116,41420
+@node Goal-save sequencesGoal-save sequences
1172,43567
+@node Active scripting bufferActive scripting buffer
1209,45051
+@node Summary of Proof General buffersSummary of Proof General buffers
1282,48684
+@node Script editing commandsScript editing commands
1331,50941
+@node Script processing commandsScript processing commands
1411,53900
+@node Proof assistant commandsProof assistant commands
1537,59145
+@node Toolbar commandsToolbar commands
1730,66073
+@node Interrupting during trace outputInterrupting during trace output
1755,67032
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1795,68962
+@node Document centred workingDocument centred working
1816,69583
+@node Automatic processingAutomatic processing
1928,74261
+@node Visibility of completed proofsVisibility of completed proofs
1983,76309
+@node Switching between proof scriptsSwitching between proof scripts
2038,78249
+@node View of processed files View of processed files 
2075,80221
+@node Retracting across filesRetracting across files
2135,83272
+@node Asserting across filesAsserting across files
2148,83903
+@node Automatic multiple file handlingAutomatic multiple file handling
2161,84469
+@node Escaping script managementEscaping script management
2186,85503
+@node Editing featuresEditing features
2243,87615
+@node Unicode symbols and special layout supportUnicode symbols and special layout support
2313,90394
+@node Maths menuMaths menu
2355,91952
+@node Unicode Tokens modeUnicode Tokens mode
2372,92643
+@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2422,95066
+@node Special layout Special layout 
2452,96027
+@node Moving between Unicode and tokensMoving between Unicode and tokens
2562,100145
+@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2617,102256
+@node Selecting suitable fontsSelecting suitable fonts
2656,103430
+@node Support for other PackagesSupport for other Packages
2721,106418
+@node Syntax highlightingSyntax highlighting
2751,107254
+@node Imenu and SpeedbarImenu and Speedbar
2779,108257
+@node Support for outline modeSupport for outline mode
2825,109928
+@node Support for completionSupport for completion
2850,111057
+@node Support for tagsSupport for tags
2907,113219
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2959,115567
+@node Goals buffer commandsGoals buffer commands
2975,116162
+@node Graphical Proof-Tree VisualizationGraphical Proof-Tree Visualization
3074,120315
+@node Starting and Stopping Proof-Tree VisualizationStarting and Stopping Proof-Tree Visualization
3097,121207
+@node Features of ProoftreeFeatures of Prooftree
3125,122364
+@node Prooftree CustomizationProoftree Customization
3157,123576
+@node Customizing Proof GeneralCustomizing Proof General
3181,124455
+@node Basic optionsBasic options
3221,126125
+@node How to customizeHow to customize
3245,126895
+@node Display customizationDisplay customization
3292,128862
+@node User optionsUser options
3460,135824
+@node Changing facesChanging faces
3696,144492
+@node Script buffer facesScript buffer faces
3718,145367
+@node Goals and response facesGoals and response faces
3764,146967
+@node Tweaking configuration settingsTweaking configuration settings
3809,148499
+@node Hints and TipsHints and Tips
3866,151025
+@node Adding your own keybindingsAdding your own keybindings
3885,151626
+@node Using file variablesUsing file variables
3949,154240
+@node Using abbreviationsUsing abbreviations
4025,156911
+@node LEGO Proof GeneralLEGO Proof General
4064,158326
+@node LEGO specific commandsLEGO specific commands
4105,159695
+@node LEGO tagsLEGO tags
4125,160150
+@node LEGO customizationsLEGO customizations
4135,160397
+@node Coq Proof GeneralCoq Proof General
4165,161237
+@node Coq-specific commandsCoq-specific commands
4181,161603
+@node Multiple File SupportMultiple File Support
4204,162111
+@node Automatic Compilation in DetailAutomatic Compilation in Detail
4274,164700
+@node Locking AncestorsLocking Ancestors
4349,168051
+@node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support
4382,169476
+@node Current LimitationsCurrent Limitations
4614,179246
+@node Editing multiple proofsEditing multiple proofs
4640,180098
+@node User-loaded tacticsUser-loaded tactics
4664,181206
+@node Holes featureHoles feature
4728,183680
+@node Proof-Tree VisualizationProof-Tree Visualization
4753,184899
+@node Isabelle Proof GeneralIsabelle Proof General
4765,185249
+@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4791,186125
+@node Isabelle commandsIsabelle commands
4860,188926
+@node Isabelle settingsIsabelle settings
5003,193118
+@node Isabelle customizationsIsabelle customizations
5017,193700
+@node HOL Light Proof GeneralHOL Light Proof General
5040,194193
+@node Shell Proof GeneralShell Proof General
5087,196172
+@node Obtaining and InstallingObtaining and Installing
5123,197631
+@node Obtaining Proof GeneralObtaining Proof General
5138,197996
+@node Installing Proof General from tarballInstalling Proof General from tarball
5164,198878
+@node Setting the names of binariesSetting the names of binaries
5188,199668
+@node Notes for syssiesNotes for syssies
5216,200608
+@node Bugs and EnhancementsBugs and Enhancements
5292,203605
+@node References5313,204420
+@node History of Proof GeneralHistory of Proof General
5353,205443
+@node Old News for 3.0Old News for 3.0
5447,209608
+@node Old News for 3.1Old News for 3.1
5517,213302
+@node Old News for 3.2Old News for 3.2
5543,214474
+@node Old News for 3.3Old News for 3.3
5604,217477
+@node Old News for 3.4Old News for 3.4
5623,218374
+@node Old News for 3.5Old News for 3.5
5645,219429
+@node Old News for 3.6Old News for 3.6
5649,219486
+@node Old News for 3.7Old News for 3.7
5654,219586
+@node Function IndexFunction Index
5684,221040
+@node Variable IndexVariable Index
5688,221116
+@node Keystroke IndexKeystroke Index
5692,221196
+@node Concept IndexConcept Index
5696,221262
 
 doc/PG-adapting.texi,4541
-@node Top137,3889
-@node Introduction175,5039
-@node Future216,6692
-@node Credits252,8288
-@node Beginning with a New ProverBeginning with a New Prover
262,8580
-@node Overview of adding a new proverOverview of adding a new prover
302,10522
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration
384,14071
-@node Major modes used by Proof GeneralMajor modes used by Proof General
453,17462
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
496,19172
-@node Settings for generic user-level commandsSettings for generic user-level commands
511,19718
-@node Menu configurationMenu configuration
556,21450
-@node Toolbar configurationToolbar configuration
580,22367
-@node Proof Script SettingsProof Script Settings
639,24604
-@node Recognizing commands and commentsRecognizing commands and comments
662,25216
-@node Recognizing proofsRecognizing proofs
799,31669
-@node Recognizing other elementsRecognizing other elements
903,35973
-@node Configuring undo behaviourConfiguring undo behaviour
966,38452
-@node Nested proofsNested proofs
1103,43839
-@node Safe (state-preserving) commandsSafe (state-preserving) commands
1143,45465
-@node Activate scripting hookActivate scripting hook
1166,46418
-@node Automatic multiple filesAutomatic multiple files
1190,47288
-@node Completely asserted buffersCompletely asserted buffers
1211,48134
-@node Completions1244,49599
-@node Proof Shell SettingsProof Shell Settings
1285,51089
-@node Proof shell commandsProof shell commands
1316,52371
-@node Script input to the shellScript input to the shell
1493,60135
-@node Settings for matching various output from proof processSettings for matching various output from proof process
1563,63339
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1686,68750
-@node Hooks and other settingsHooks and other settings
1913,78712
-@node Goals Buffer SettingsGoals Buffer Settings
1992,81856
-@node Splash Screen SettingsSplash Screen Settings
2066,84846
-@node Global ConstantsGlobal Constants
2092,85601
-@node Handling Multiple FilesHandling Multiple Files
2118,86430
-@node Configuring Editing SyntaxConfiguring Editing Syntax
2287,95099
-@node Configuring Font LockConfiguring Font Lock
2344,97216
-@node Configuring TokensConfiguring Tokens
2420,100928
-@node Configuring Proof-Tree VisualizationConfiguring Proof-Tree Visualization
2470,103048
-@node Prerequisites2487,103588
-@node Proof-Tree Display InternalsProof-Tree Display Internals
2550,106239
-@node Organization of the CodeOrganization of the Code
2568,106729
-@node Communication2664,110992
-@node Guards2689,112104
-@node Urgent and Delayed ActionsUrgent and Delayed Actions
2743,114249
-@node Full AnnotationFull Annotation
2804,116757
-@node Configuring Prooftree for a New Proof AssistantConfiguring Prooftree for a New Proof Assistant
2818,117331
-@node Proof Tree Elisp configurationProof Tree Elisp configuration
2830,117663
-@node Prooftree AdaptionProoftree Adaption
2851,118493
-@node Writing More Lisp CodeWriting More Lisp Code
2871,119172
-@node Default values for generic settingsDefault values for generic settings
2888,119817
-@node Adding prover-specific configurationsAdding prover-specific configurations
2918,120900
-@node Useful variablesUseful variables
2961,122182
-@node Useful functions and macrosUseful functions and macros
2976,122681
-@node Internals of Proof GeneralInternals of Proof General
3086,126993
-@node Spans3116,127923
-@node Proof General site configurationProof General site configuration
3131,128296
-@node Configuration variable mechanismsConfiguration variable mechanisms
3214,131377
-@node Global variablesGlobal variables
3344,137093
-@node Proof script modeProof script mode
3419,139717
-@node Proof shell modeProof shell mode
3683,151674
-@node Debugging4234,174109
-@node Plans and IdeasPlans and Ideas
4277,174985
-@node Proof by pointing and similar featuresProof by pointing and similar features
4298,175707
-@node Granularity of atomic command sequencesGranularity of atomic command sequences
4336,177365
-@node Browser mode for script files and theoriesBrowser mode for script files and theories
4381,179590
-@node Demonstration InstantiationsDemonstration Instantiations
4411,180621
-@node demoisa-easy.el4427,181052
-@node demoisa.el4489,183190
-@node Function IndexFunction Index
4643,188056
-@node Variable IndexVariable Index
4647,188132
-@node Concept IndexConcept Index
4656,188311
+@node Top137,3995
+@node Introduction175,5145
+@node Future216,6798
+@node Credits252,8394
+@node Beginning with a New ProverBeginning with a New Prover
262,8686
+@node Overview of adding a new proverOverview of adding a new prover
302,10628
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration
384,14206
+@node Major modes used by Proof GeneralMajor modes used by Proof General
453,17597
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
496,19307
+@node Settings for generic user-level commandsSettings for generic user-level commands
511,19853
+@node Menu configurationMenu configuration
556,21585
+@node Toolbar configurationToolbar configuration
580,22502
+@node Proof Script SettingsProof Script Settings
639,24739
+@node Recognizing commands and commentsRecognizing commands and comments
662,25351
+@node Recognizing proofsRecognizing proofs
799,31804
+@node Recognizing other elementsRecognizing other elements
903,36108
+@node Configuring undo behaviourConfiguring undo behaviour
966,38587
+@node Nested proofsNested proofs
1103,43974
+@node Safe (state-preserving) commandsSafe (state-preserving) commands
1143,45600
+@node Activate scripting hookActivate scripting hook
1166,46553
+@node Automatic multiple filesAutomatic multiple files
1190,47423
+@node Completely asserted buffersCompletely asserted buffers
1211,48269
+@node Completions1244,49734
+@node Proof Shell SettingsProof Shell Settings
1285,51224
+@node Proof shell commandsProof shell commands
1316,52506
+@node Script input to the shellScript input to the shell
1493,60270
+@node Settings for matching various output from proof processSettings for matching various output from proof process
1563,63474
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1690,69030
+@node Hooks and other settingsHooks and other settings
1950,80320
+@node Goals Buffer SettingsGoals Buffer Settings
2029,83464
+@node Splash Screen SettingsSplash Screen Settings
2103,86454
+@node Global ConstantsGlobal Constants
2129,87209
+@node Handling Multiple FilesHandling Multiple Files
2155,88038
+@node Configuring Editing SyntaxConfiguring Editing Syntax
2324,96707
+@node Configuring Font LockConfiguring Font Lock
2381,98824
+@node Configuring TokensConfiguring Tokens
2457,102536
+@node Configuring Proof-Tree VisualizationConfiguring Proof-Tree Visualization
2507,104656
+@node Prerequisites2524,105196
+@node Proof-Tree Display InternalsProof-Tree Display Internals
2587,107847
+@node Organization of the CodeOrganization of the Code
2605,108337
+@node Communication2701,112600
+@node Guards2726,113712
+@node Urgent and Delayed ActionsUrgent and Delayed Actions
2780,115857
+@node Full AnnotationFull Annotation
2841,118365
+@node Configuring Prooftree for a New Proof AssistantConfiguring Prooftree for a New Proof Assistant
2855,118939
+@node Proof Tree Elisp configurationProof Tree Elisp configuration
2867,119271
+@node Prooftree AdaptionProoftree Adaption
2888,120101
+@node Writing More Lisp CodeWriting More Lisp Code
2908,120780
+@node Default values for generic settingsDefault values for generic settings
2925,121425
+@node Adding prover-specific configurationsAdding prover-specific configurations
2955,122508
+@node Useful variablesUseful variables
2998,123790
+@node Useful functions and macrosUseful functions and macros
3013,124289
+@node Internals of Proof GeneralInternals of Proof General
3123,128601
+@node Spans3153,129531
+@node Proof General site configurationProof General site configuration
3168,129904
+@node Configuration variable mechanismsConfiguration variable mechanisms
3251,133003
+@node Global variablesGlobal variables
3381,138719
+@node Proof script modeProof script mode
3456,141343
+@node Proof shell modeProof shell mode
3720,153300
+@node Debugging4271,175735
+@node Plans and IdeasPlans and Ideas
4314,176611
+@node Proof by pointing and similar featuresProof by pointing and similar features
4335,177333
+@node Granularity of atomic command sequencesGranularity of atomic command sequences
4373,178991
+@node Browser mode for script files and theoriesBrowser mode for script files and theories
4418,181216
+@node Demonstration InstantiationsDemonstration Instantiations
4448,182247
+@node demoisa-easy.el4464,182678
+@node demoisa.el4526,184869
+@node Function IndexFunction Index
4680,189788
+@node Variable IndexVariable Index
4684,189864
+@node Concept IndexConcept Index
4693,190043
 
 generic/proof.el,0
 
+pghaskell/pghaskell.el,0
+
+pghaskell/pghashell.el,0
+
+pgocaml/pgocaml.el,0
+
 pgshell/pgshell.el,0
 
 isar/isar-profiling.el,0