Updated

4 files changed, 1323 insertions, 1284 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index e62c2f9a..1443b3cb 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -5,7 +5,7 @@ This version of Proof General has been tested with these Emacs versions
 on recent Linux systems:
 
  Emacs 23.2            -- recommended and supported
- Emacs 22.3.1	       -- previous version, may work
+ Emacs 22.3.1	       -- previous version, may work, *unsupported*
 
 and (main) prover versions:  Coq 8.1pl3, Isabelle2009{-1,-2}
 
@@ -54,9 +54,10 @@ into .emacs.  You should put .emacs in value of HOME if you set that,
 or else in directory you installled Emacs in, e.g.  
 c:\Program Files\Emacs\.emacs
 
-Note that Windows compatibility isn't thoroughly tested by the
-maintainers.  If you discover problems, please send a report and/or
-fix to the address above.
+Note that Windows compatibility isn't tested by the maintainers.  If
+you discover problems, please add notes on the Wiki page above, and
+submit patches to http://proofgeneral.inf.ed.ac.uk/trac
+
 
 
 
diff --git a/TAGS b/TAGS
index 554288d2..134e6da3 100644
--- a/TAGS
+++ b/TAGS
@@ -17,79 +17,241 @@ coq/coq-abbrev.el,495
 (defconst coq-terms-abbrev-table51,1434
 (defun coq-install-abbrevs 58,1628
 (defpgdefault menu-entries78,2365
-(defpgdefault help-menu-entries141,4384
-
-coq/coq-db.el,668
-(defconst coq-syntax-db 23,544
-(defvar coq-user-tactics-db59,1917
-(defun coq-insert-from-db 69,2266
-(defun coq-build-regexp-list-from-db 87,2998
-(defun max-length-db 109,3981
-(defun coq-build-menu-from-db-internal 121,4256
-(defun coq-build-title-menu 156,5879
-(defun coq-sort-menu-entries 165,6247
-(defun coq-build-menu-from-db 171,6374
-(defcustom coq-holes-minor-mode 193,7213
-(defun coq-build-abbrev-table-from-db 199,7357
-(defun filter-state-preserving 218,7995
-(defun filter-state-changing 223,8149
-(defface coq-solve-tactics-face230,8370
-(defface coq-cheat-face239,8700
-(defconst coq-solve-tactics-face 247,8948
-(defconst coq-cheat-face 251,9112
-
-coq/coq-indent.el,2223
+(defpgdefault help-menu-entries143,4479
+
+coq/coq-db.el,678
+(defconst coq-syntax-db 24,596
+(defun coq-insert-from-db 70,2319
+(defun coq-build-regexp-list-from-db 88,3050
+(defun coq-build-opt-regexp-from-db 107,3856
+(defun max-length-db 126,4677
+(defun coq-build-menu-from-db-internal 138,4952
+(defun coq-build-title-menu 175,6493
+(defun coq-sort-menu-entries 184,6861
+(defun coq-build-menu-from-db 190,6988
+(defcustom coq-holes-minor-mode 212,7827
+(defun coq-build-abbrev-table-from-db 218,7971
+(defun filter-state-preserving 237,8609
+(defun filter-state-changing 242,8763
+(defface coq-solve-tactics-face249,8984
+(defface coq-cheat-face258,9314
+(defconst coq-solve-tactics-face 266,9562
+(defconst coq-cheat-face 270,9726
+
+coq/coq.el,5959
+(defcustom coq-translate-to-v8 48,1381
+(defun coq-build-prog-args 54,1561
+(defcustom coq-compile-file-command 64,1857
+(defcustom coq-use-makefile 72,2176
+(defcustom coq-default-undo-limit 80,2399
+(defconst coq-shell-init-cmd85,2527
+(defcustom coq-prog-env 91,2654
+(defconst coq-shell-restart-cmd 99,2904
+(defvar coq-shell-prompt-pattern101,2958
+(defvar coq-shell-cd 109,3261
+(defvar coq-shell-proof-completed-regexp 113,3421
+(defvar coq-goal-regexp116,3576
+(defun coq-library-directory 121,3672
+(defcustom coq-tags 127,3850
+(defconst coq-interrupt-regexp 132,4000
+(defcustom coq-www-home-page 135,4093
+(defvar coq-outline-regexp146,4268
+(defvar coq-outline-heading-end-regexp 153,4480
+(defvar coq-shell-outline-regexp 155,4534
+(defvar coq-shell-outline-heading-end-regexp 156,4584
+(defconst coq-state-preserving-tactics-regexp159,4648
+(defconst coq-state-changing-commands-regexp161,4750
+(defconst coq-state-preserving-commands-regexp163,4859
+(defconst coq-commands-regexp165,4972
+(defvar coq-retractable-instruct-regexp167,5051
+(defvar coq-non-retractable-instruct-regexp169,5143
+(defun coq-set-undo-limit 204,5830
+(defun build-list-id-from-string 208,5960
+(defun coq-last-prompt-info 220,6458
+(defun coq-last-prompt-info-safe 232,6990
+(defvar coq-last-but-one-statenum 238,7247
+(defvar coq-last-but-one-proofnum 245,7545
+(defvar coq-last-but-one-proofstack 248,7643
+(defsubst coq-get-span-statenum 251,7753
+(defsubst coq-get-span-proofnum 255,7868
+(defsubst coq-get-span-proofstack 259,7983
+(defsubst coq-set-span-statenum 263,8127
+(defsubst coq-get-span-goalcmd 267,8258
+(defsubst coq-set-span-goalcmd 271,8372
+(defsubst coq-set-span-proofnum 275,8502
+(defsubst coq-set-span-proofstack 279,8633
+(defsubst proof-last-locked-span 283,8793
+(defun proof-clone-buffer 287,8927
+(defun proof-store-buffer-win 301,9462
+(defun proof-store-response-win 312,9955
+(defun proof-store-goals-win 316,10082
+(defun coq-set-state-infos 328,10614
+(defun count-not-intersection 366,12701
+(defun coq-find-and-forget 396,13950
+(defvar coq-current-goal 420,15044
+(defun coq-goal-hyp 423,15109
+(defun coq-state-preserving-p 436,15541
+(defconst notation-print-kinds-table450,15855
+(defun coq-PrintScope 454,16022
+(defun coq-guess-or-ask-for-string 472,16571
+(defun coq-ask-do 486,17139
+(defsubst coq-put-into-brackets 495,17524
+(defsubst coq-put-into-quotes 498,17585
+(defun coq-SearchIsos 501,17645
+(defun coq-SearchConstant 509,17886
+(defun coq-Searchregexp 513,17979
+(defun coq-SearchRewrite 519,18122
+(defun coq-SearchAbout 523,18219
+(defun coq-Print 529,18364
+(defun coq-About 534,18489
+(defun coq-LocateConstant 539,18609
+(defun coq-LocateLibrary 544,18712
+(defun coq-LocateNotation 549,18829
+(defun coq-Pwd 557,19061
+(defun coq-Inspect 562,19185
+(defun coq-PrintSection(566,19285
+(defun coq-Print-implicit 570,19378
+(defun coq-Check 575,19529
+(defun coq-Show 580,19637
+(defun coq-Compile 594,20080
+(defun coq-guess-command-line 606,20398
+(defpacustom use-editing-holes 643,21951
+(defun coq-mode-config 652,22254
+(defun coq-shell-mode-config 745,25597
+(defun coq-goals-mode-config 788,27387
+(defun coq-response-config 795,27631
+(defpacustom print-fully-explicit 820,28456
+(defpacustom print-implicit 825,28604
+(defpacustom print-coercions 830,28770
+(defpacustom print-match-wildcards 835,28914
+(defpacustom print-elim-types 840,29094
+(defpacustom printing-depth 845,29260
+(defpacustom undo-depth 850,29421
+(defpacustom time-commands 855,29587
+(defpacustom auto-compile-vos 859,29697
+(defun coq-maybe-compile-buffer 888,30811
+(defun coq-ancestors-of 924,32339
+(defun coq-all-ancestors-of 947,33303
+(defun coq-process-require-command 958,33650
+(defun coq-included-children 963,33777
+(defun coq-process-file 984,34616
+(defun coq-preprocessing 999,35145
+(defun coq-fake-constant-markup 1013,35600
+(defun coq-create-span-menu 1029,36205
+(defconst module-kinds-table1047,36718
+(defconst modtype-kinds-table1051,36867
+(defun coq-insert-section-or-module 1055,36996
+(defconst reqkinds-kinds-table1076,37846
+(defun coq-insert-requires 1080,37990
+(defun coq-end-Section 1093,38470
+(defun coq-insert-intros 1111,39048
+(defun coq-insert-infoH-hook 1123,39581
+(defun coq-insert-as 1128,39789
+(defun coq-insert-match 1145,40482
+(defun coq-insert-solve-tactic 1174,41652
+(defun coq-insert-tactic 1180,41903
+(defun coq-insert-tactical 1186,42105
+(defun coq-insert-command 1192,42336
+(defun coq-insert-term 1197,42501
+(define-key coq-keymap 1202,42662
+(define-key coq-keymap 1203,42720
+(define-key coq-keymap 1204,42777
+(define-key coq-keymap 1205,42846
+(define-key coq-keymap 1206,42902
+(define-key coq-keymap 1207,42951
+(define-key coq-keymap 1208,43009
+(define-key coq-keymap 1209,43069
+(define-key coq-keymap 1210,43134
+(define-key coq-keymap 1213,43262
+(define-key coq-keymap 1215,43336
+(define-key coq-keymap 1216,43393
+(define-key coq-keymap 1220,43518
+(define-key coq-keymap 1222,43574
+(define-key coq-keymap 1223,43624
+(define-key coq-keymap 1224,43674
+(define-key coq-keymap 1225,43730
+(define-key coq-keymap 1226,43780
+(define-key coq-keymap 1227,43834
+(define-key coq-keymap 1228,43893
+(define-key coq-goals-mode-map 1231,43954
+(define-key coq-goals-mode-map 1232,44036
+(define-key coq-goals-mode-map 1233,44118
+(define-key coq-goals-mode-map 1234,44205
+(define-key coq-goals-mode-map 1235,44287
+(defvar last-coq-error-location 1244,44589
+(defun coq-get-last-error-location 1252,44973
+(defun coq-highlight-error 1302,47530
+(defun coq-highlight-error-hook 1330,48611
+(defun first-word-of-buffer 1340,48828
+(defun coq-show-first-goal 1348,49031
+(defvar coq-modeline-string2 1365,49726
+(defvar coq-modeline-string1 1366,49760
+(defvar coq-modeline-string0 1367,49794
+(defun coq-build-subgoals-string 1368,49835
+(defun coq-update-minor-mode-alist 1373,50001
+(defun is-not-split-vertic 1405,51395
+(defun optim-resp-windows 1414,51835
+
+coq/coq-indent.el,2515
 (defconst coq-any-command-regexp20,368
-(defconst coq-indent-inner-regexp23,459
-(defconst coq-comment-start-regexp 33,813
-(defconst coq-comment-end-regexp 34,856
-(defconst coq-comment-start-or-end-regexp35,897
-(defconst coq-indent-open-regexp37,1005
-(defconst coq-indent-close-regexp42,1179
-(defconst coq-indent-closepar-regexp 47,1360
-(defconst coq-indent-closematch-regexp 48,1405
-(defconst coq-indent-openpar-regexp 49,1476
-(defconst coq-indent-openmatch-regexp 50,1520
-(defconst coq-indent-any-regexp51,1600
-(defconst coq-indent-kw56,1878
-(defconst coq-indent-pattern-regexp 66,2332
-(defun coq-indent-goal-command-p 70,2435
-(defconst coq-end-command-regexp92,3486
-(defun coq-search-comment-delimiter-forward 97,3638
-(defun coq-search-comment-delimiter-backward 106,3968
-(defun coq-skip-until-one-comment-backward 113,4242
-(defun coq-skip-until-one-comment-forward 128,4949
-(defun coq-looking-at-comment 139,5467
-(defun coq-find-comment-start 143,5608
-(defun coq-find-comment-end 154,6041
-(defun coq-looking-at-syntactic-context 166,6534
-(defconst coq-end-command-or-comment-regexp172,6756
-(defconst coq-end-command-or-comment-start-regexp175,6865
-(defun coq-find-not-in-comment-backward 179,6983
-(defun coq-find-not-in-comment-forward 199,7884
-(defun coq-find-command-end-backward 223,9023
-(defun coq-find-command-end-forward 232,9414
-(defun coq-find-command-end 241,9791
-(defun coq-find-current-start 249,10123
-(defun coq-find-real-start 258,10414
-(defun coq-command-at-point 265,10633
-(defun coq-indent-only-spaces-on-line 272,10918
-(defun coq-indent-find-reg 278,11195
-(defun coq-find-no-syntactic-on-line 292,11731
-(defun coq-back-to-indentation-prevline 305,12204
-(defun coq-find-unclosed 349,14112
-(defun coq-find-at-same-level-zero 379,15408
-(defun coq-find-unopened 407,16566
-(defun coq-find-last-unopened 450,18000
-(defun coq-end-offset 461,18397
-(defun coq-indent-command-offset 486,19167
-(defun coq-indent-expr-offset 533,20991
-(defun coq-indent-comment-offset 649,25674
-(defun coq-indent-offset 681,27123
-(defun coq-indent-calculate 699,27985
-(defun coq-indent-line 702,28073
-(defun coq-indent-line-not-comments 712,28439
-(defun coq-indent-region 722,28828
+(defconst coq-indent-inner-regexp23,442
+(defconst coq-comment-start-regexp 33,796
+(defconst coq-comment-end-regexp 34,839
+(defconst coq-comment-start-or-end-regexp35,880
+(defconst coq-indent-open-regexp37,988
+(defconst coq-indent-close-regexp42,1164
+(defconst coq-indent-closepar-regexp 45,1275
+(defconst coq-indent-closematch-regexp 46,1320
+(defconst coq-indent-openpar-regexp 47,1391
+(defconst coq-indent-openmatch-regexp 48,1435
+(defconst coq-tacticals-tactics-regex49,1515
+(defconst coq-indent-any-regexp51,1634
+(defconst coq-indent-kw55,1850
+(defconst coq-indent-pattern-regexp 65,2316
+(defun coq-indent-goal-command-p 69,2419
+(defconst coq-end-command-regexp91,3470
+(defun coq-search-comment-delimiter-forward 96,3622
+(defun coq-search-comment-delimiter-backward 105,3952
+(defun coq-skip-until-one-comment-backward 112,4226
+(defun coq-skip-until-one-comment-forward 127,4933
+(defun coq-looking-at-comment 138,5451
+(defun coq-find-comment-start 142,5592
+(defun coq-find-comment-end 153,6025
+(defun coq-looking-at-syntactic-context 165,6518
+(defconst coq-end-command-or-comment-regexp171,6740
+(defconst coq-end-command-or-comment-start-regexp174,6849
+(defun coq-find-not-in-comment-backward 178,6967
+(defun coq-find-not-in-comment-forward 198,7868
+(defun coq-find-command-end-backward 222,9007
+(defun coq-find-command-end-forward 231,9398
+(defun coq-find-command-end 240,9775
+(defun coq-find-current-start 248,10107
+(defun coq-find-real-start 257,10398
+(defun coq-command-at-point 264,10617
+(defun same-line 272,10903
+(defun coq-commands-at-line 275,10990
+(defun coq-indent-only-spaces-on-line 294,11613
+(defun coq-indent-find-reg 300,11890
+(defun coq-find-no-syntactic-on-line 314,12426
+(defun coq-back-to-indentation-prevline 327,12899
+(defun coq-find-unclosed 370,14785
+(defun coq-find-at-same-level-zero 400,16095
+(defun coq-find-unopened 429,17361
+(defun coq-find-last-unopened 472,18795
+(defun coq-end-offset 483,19192
+(defun coq-add-iter 508,19962
+(defun coq-goal-count 511,20068
+(defun coq-save-count 513,20140
+(defun coq-proof-count 515,20226
+(defun coq-goal-save-diff-maybe-proof 519,20401
+(defun coq-indent-command-offset 526,20622
+(defun coq-indent-expr-offset 558,22225
+(defun coq-indent-comment-offset 673,26909
+(defun coq-indent-offset 705,28358
+(defun coq-indent-calculate 724,29233
+(defun coq-indent-line 727,29321
+(defun coq-indent-line-not-comments 737,29687
+(defun coq-indent-region 747,30076
 
 coq/coq-local-vars.el,280
 (defconst coq-local-vars-doc 20,429
@@ -97,74 +259,80 @@ coq/coq-local-vars.el,280
 (defun coq-read-directory 89,3430
 (defun coq-extract-directories-from-args 113,4533
 (defun coq-ask-prog-args 128,5085
-(defun coq-ask-prog-name 150,6149
-(defun coq-ask-insert-coq-prog-name 168,6904
-
-coq/coq-syntax.el,2563
-(defcustom coq-prog-name 18,561
-(defcustom coq-user-tactics-db 38,1343
-(defcustom coq-user-commands-db 55,1856
-(defcustom coq-user-tacticals-db 71,2375
-(defcustom coq-user-solve-tactics-db 87,2896
-(defcustom coq-user-cheat-tactics-db 103,3415
-(defcustom coq-user-reserved-db 122,3961
-(defvar coq-tactics-db140,4492
-(defvar coq-solve-tactics-db298,12751
-(defvar coq-solve-cheat-tactics-db321,13596
-(defvar coq-tacticals-db333,13771
-(defvar coq-decl-db357,14657
-(defvar coq-defn-db380,15951
-(defvar coq-goal-starters-db438,20313
-(defvar coq-other-commands-db467,22070
-(defvar coq-commands-db592,31283
-(defvar coq-terms-db599,31503
-(defun coq-count-match 663,34152
-(defun coq-module-opening-p 679,34881
-(defun coq-section-command-p 690,35292
-(defun coq-goal-command-str-p 694,35389
-(defun coq-goal-command-p 721,36491
-(defvar coq-keywords-save-strict730,36774
-(defvar coq-keywords-save739,36887
-(defun coq-save-command-p 743,36965
-(defvar coq-keywords-kill-goal752,37259
-(defvar coq-keywords-state-changing-misc-commands756,37349
-(defvar coq-keywords-goal759,37474
-(defvar coq-keywords-decl762,37557
-(defvar coq-keywords-defn765,37631
-(defvar coq-keywords-state-changing-commands769,37706
-(defvar coq-keywords-state-preserving-commands778,37966
-(defvar coq-keywords-commands783,38182
-(defvar coq-solve-tactics788,38330
-(defvar coq-solve-cheat-tactics792,38451
-(defvar coq-tacticals796,38596
-(defvar coq-reserved802,38735
-(defvar coq-state-changing-tactics813,39063
-(defvar coq-state-preserving-tactics816,39172
-(defvar coq-tactics820,39286
-(defvar coq-retractable-instruct823,39375
-(defvar coq-non-retractable-instruct826,39485
-(defvar coq-keywords830,39613
-(defvar coq-symbols837,39780
-(defvar coq-error-regexp 856,39993
-(defvar coq-id 859,40221
-(defvar coq-id-shy 860,40246
-(defvar coq-ids 862,40300
-(defun coq-first-abstr-regexp 864,40341
-(defcustom coq-variable-highlight-enable 867,40436
-(defvar coq-font-lock-terms873,40563
-(defconst coq-save-command-regexp-strict894,41562
-(defconst coq-save-command-regexp898,41728
-(defconst coq-save-with-hole-regexp903,41881
-(defconst coq-goal-command-regexp907,42039
-(defconst coq-goal-with-hole-regexp910,42139
-(defconst coq-decl-with-hole-regexp914,42271
-(defconst coq-defn-with-hole-regexp921,42519
-(defconst coq-with-with-hole-regexp931,42807
-(defconst coq-require-command-regexp938,43100
-(defvar coq-font-lock-keywords-1946,43325
-(defvar coq-font-lock-keywords 974,44727
-(defun coq-init-syntax-table 976,44785
-(defconst coq-generic-expression1005,45683
+(defun coq-ask-prog-name 150,6153
+(defun coq-ask-insert-coq-prog-name 167,6864
+
+coq/coq-syntax.el,2818
+(defcustom coq-prog-name 18,559
+(defcustom coq-user-tactics-db 38,1341
+(defcustom coq-user-commands-db 55,1854
+(defcustom coq-user-tacticals-db 71,2373
+(defcustom coq-user-solve-tactics-db 87,2894
+(defcustom coq-user-cheat-tactics-db 103,3413
+(defcustom coq-user-reserved-db 122,3959
+(defvar coq-tactics-db140,4490
+(defvar coq-solve-tactics-db298,12749
+(defvar coq-solve-cheat-tactics-db321,13594
+(defvar coq-tacticals-db333,13769
+(defvar coq-decl-db357,14655
+(defvar coq-defn-db382,16111
+(defvar coq-goal-starters-db440,20466
+(defvar coq-other-commands-db469,22223
+(defvar coq-commands-db598,31689
+(defvar coq-terms-db605,31909
+(defun coq-count-match 667,34524
+(defun coq-module-opening-p 683,35253
+(defun coq-section-command-p 694,35664
+(defun coq-goal-command-str-p 698,35761
+(defun coq-goal-command-p 725,36863
+(defvar coq-keywords-save-strict734,37146
+(defvar coq-keywords-save743,37259
+(defun coq-save-command-p 747,37337
+(defvar coq-keywords-kill-goal758,37665
+(defvar coq-keywords-state-changing-misc-commands762,37755
+(defvar coq-keywords-goal765,37880
+(defvar coq-keywords-decl768,37963
+(defvar coq-keywords-defn771,38037
+(defvar coq-keywords-state-changing-commands775,38112
+(defvar coq-keywords-state-preserving-commands784,38372
+(defvar coq-keywords-commands789,38588
+(defvar coq-solve-tactics794,38736
+(defvar coq-solve-tactics-regexp798,38857
+(defvar coq-solve-cheat-tactics802,38991
+(defvar coq-solve-cheat-tactics-regexp806,39136
+(defvar coq-tacticals810,39294
+(defvar coq-reserved816,39433
+(defvar coq-reserved-regexp 826,39760
+(defvar coq-state-changing-tactics828,39825
+(defvar coq-state-preserving-tactics831,39934
+(defvar coq-tactics835,40048
+(defvar coq-tactics-regexp 838,40137
+(defvar coq-retractable-instruct841,40292
+(defvar coq-non-retractable-instruct844,40402
+(defvar coq-keywords848,40530
+(defun proof-regexp-alt-list-symb 854,40754
+(defvar coq-keywords-regexp 857,40859
+(defvar coq-symbols860,40927
+(defvar coq-error-regexp 879,41140
+(defvar coq-id 882,41368
+(defvar coq-id-shy 883,41393
+(defvar coq-ids 886,41495
+(defun coq-first-abstr-regexp 888,41561
+(defcustom coq-variable-highlight-enable 891,41656
+(defvar coq-font-lock-terms897,41783
+(defconst coq-save-command-regexp-strict919,42866
+(defconst coq-save-command-regexp925,43036
+(defconst coq-save-with-hole-regexp930,43191
+(defconst coq-goal-command-regexp934,43351
+(defconst coq-goal-with-hole-regexp937,43453
+(defconst coq-decl-with-hole-regexp941,43587
+(defconst coq-defn-with-hole-regexp948,43837
+(defconst coq-with-with-hole-regexp958,44127
+(defconst coq-require-command-regexp965,44420
+(defvar coq-font-lock-keywords-1973,44645
+(defvar coq-font-lock-keywords 1001,45980
+(defun coq-init-syntax-table 1003,46038
+(defconst coq-generic-expression1028,46765
 
 coq/coq-unicode-tokens.el,454
 (defconst coq-token-format 39,1427
@@ -172,167 +340,12 @@ coq/coq-unicode-tokens.el,454
 (defconst coq-hexcode-match 41,1506
 (defun coq-unicode-tokens-set 43,1540
 (defcustom coq-token-symbol-map49,1768
-(defcustom coq-shortcut-alist152,4361
-(defconst coq-control-char-format-regexp241,6379
-(defconst coq-control-char-format 245,6504
-(defconst coq-control-characters247,6547
-(defconst coq-control-region-format-regexp 251,6639
-(defconst coq-control-regions253,6722
-
-coq/coq.el,6009
-(defcustom coq-translate-to-v8 48,1381
-(defun coq-build-prog-args 54,1561
-(defcustom coq-compile-file-command 64,1857
-(defcustom coq-use-makefile 72,2176
-(defcustom coq-default-undo-limit 80,2399
-(defconst coq-shell-init-cmd85,2527
-(defcustom coq-prog-env 91,2654
-(defconst coq-shell-restart-cmd 99,2904
-(defvar coq-shell-prompt-pattern101,2958
-(defvar coq-shell-cd 109,3261
-(defvar coq-shell-proof-completed-regexp 113,3421
-(defvar coq-goal-regexp116,3576
-(defun coq-library-directory 123,3690
-(defcustom coq-tags 130,3869
-(defconst coq-interrupt-regexp 135,4019
-(defcustom coq-www-home-page 140,4140
-(defvar coq-outline-regexp147,4308
-(defvar coq-outline-heading-end-regexp 154,4520
-(defvar coq-shell-outline-regexp 156,4574
-(defvar coq-shell-outline-heading-end-regexp 157,4624
-(defconst coq-state-preserving-tactics-regexp163,4789
-(defconst coq-state-changing-commands-regexp165,4889
-(defconst coq-state-preserving-commands-regexp167,4996
-(defconst coq-commands-regexp169,5107
-(defvar coq-retractable-instruct-regexp171,5184
-(defvar coq-non-retractable-instruct-regexp173,5274
-(defun coq-set-undo-limit 207,6151
-(defun build-list-id-from-string 211,6281
-(defun coq-last-prompt-info 223,6779
-(defun coq-last-prompt-info-safe 235,7311
-(defvar coq-last-but-one-statenum 241,7568
-(defvar coq-last-but-one-proofnum 248,7866
-(defvar coq-last-but-one-proofstack 251,7964
-(defsubst coq-get-span-statenum 254,8074
-(defsubst coq-get-span-proofnum 258,8189
-(defsubst coq-get-span-proofstack 262,8304
-(defsubst coq-set-span-statenum 266,8448
-(defsubst coq-get-span-goalcmd 270,8579
-(defsubst coq-set-span-goalcmd 274,8693
-(defsubst coq-set-span-proofnum 278,8823
-(defsubst coq-set-span-proofstack 282,8954
-(defsubst proof-last-locked-span 286,9114
-(defun proof-clone-buffer 292,9347
-(defun proof-store-buffer-win 306,9904
-(defun proof-store-response-win 313,10176
-(defun proof-store-goals-win 317,10303
-(defun coq-set-state-infos 329,10835
-(defun count-not-intersection 366,12921
-(defun coq-find-and-forget 397,14171
-(defvar coq-current-goal 417,15075
-(defun coq-goal-hyp 420,15140
-(defun coq-state-preserving-p 433,15572
-(defconst notation-print-kinds-table447,16073
-(defun coq-PrintScope 451,16240
-(defun coq-guess-or-ask-for-string 469,16789
-(defun coq-ask-do 483,17357
-(defsubst coq-put-into-brackets 492,17742
-(defsubst coq-put-into-quotes 495,17803
-(defun coq-SearchIsos 498,17863
-(defun coq-SearchConstant 506,18104
-(defun coq-Searchregexp 510,18197
-(defun coq-SearchRewrite 516,18340
-(defun coq-SearchAbout 520,18438
-(defun coq-Print 526,18584
-(defun coq-About 531,18709
-(defun coq-LocateConstant 536,18829
-(defun coq-LocateLibrary 541,18932
-(defun coq-LocateNotation 546,19050
-(defun coq-Pwd 554,19247
-(defun coq-Inspect 559,19347
-(defun coq-PrintSection(563,19447
-(defun coq-Print-implicit 567,19540
-(defun coq-Check 572,19691
-(defun coq-Show 577,19799
-(defun coq-Compile 591,20242
-(defun coq-guess-command-line 603,20560
-(defpacustom use-editing-holes 640,22113
-(defun coq-mode-config 649,22416
-(defun coq-shell-mode-config 741,25721
-(defun coq-goals-mode-config 783,27444
-(defun coq-response-config 790,27688
-(defpacustom print-fully-explicit 815,28513
-(defpacustom print-implicit 820,28661
-(defpacustom print-coercions 825,28827
-(defpacustom print-match-wildcards 830,28971
-(defpacustom print-elim-types 835,29151
-(defpacustom printing-depth 840,29317
-(defpacustom undo-depth 845,29478
-(defpacustom time-commands 850,29625
-(defpacustom undo-limit 854,29735
-(defpacustom auto-compile-vos 859,29837
-(defun coq-maybe-compile-buffer 888,30951
-(defun coq-ancestors-of 924,32479
-(defun coq-all-ancestors-of 947,33443
-(defun coq-process-require-command 958,33790
-(defun coq-included-children 963,33917
-(defun coq-process-file 984,34756
-(defun coq-preprocessing 999,35295
-(defun coq-fake-constant-markup 1013,35730
-(defun coq-create-span-menu 1029,36335
-(defconst module-kinds-table1047,36848
-(defconst modtype-kinds-table1051,36997
-(defun coq-insert-section-or-module 1055,37126
-(defconst reqkinds-kinds-table1076,37976
-(defun coq-insert-requires 1080,38120
-(defun coq-end-Section 1093,38600
-(defun coq-insert-intros 1111,39178
-(defun coq-insert-infoH-hook 1123,39711
-(defun coq-insert-as 1128,39919
-(defun coq-insert-match 1145,40612
-(defun coq-insert-tactic 1174,41782
-(defun coq-insert-tactical 1180,42021
-(defun coq-insert-command 1186,42270
-(defun coq-insert-term 1192,42514
-(define-key coq-keymap 1198,42711
-(define-key coq-keymap 1199,42769
-(define-key coq-keymap 1200,42826
-(define-key coq-keymap 1201,42895
-(define-key coq-keymap 1202,42951
-(define-key coq-keymap 1203,43000
-(define-key coq-keymap 1204,43058
-(define-key coq-keymap 1205,43118
-(define-key coq-keymap 1206,43183
-(define-key coq-keymap 1208,43246
-(define-key coq-keymap 1209,43305
-(define-key coq-keymap 1213,43430
-(define-key coq-keymap 1215,43486
-(define-key coq-keymap 1216,43536
-(define-key coq-keymap 1217,43586
-(define-key coq-keymap 1218,43642
-(define-key coq-keymap 1219,43692
-(define-key coq-keymap 1220,43746
-(define-key coq-keymap 1221,43805
-(define-key coq-goals-mode-map 1224,43866
-(define-key coq-goals-mode-map 1225,43948
-(define-key coq-goals-mode-map 1226,44030
-(define-key coq-goals-mode-map 1227,44117
-(define-key coq-goals-mode-map 1228,44199
-(defvar last-coq-error-location 1237,44501
-(defun coq-get-last-error-location 1245,44885
-(defun coq-highlight-error 1295,47442
-(defvar coq-allow-highlight-error 1326,48638
-(defun coq-decide-highlight-error 1333,48964
-(defun coq-highlight-error-hook 1338,49149
-(defun first-word-of-buffer 1349,49542
-(defun coq-show-first-goal 1357,49745
-(defvar coq-modeline-string2 1374,50440
-(defvar coq-modeline-string1 1375,50484
-(defvar coq-modeline-string0 1376,50527
-(defun coq-build-subgoals-string 1377,50572
-(defun coq-update-minor-mode-alist 1382,50738
-(defun is-not-split-vertic 1408,51809
-(defun optim-resp-windows 1417,52249
+(defcustom coq-shortcut-alist165,4719
+(defconst coq-control-char-format-regexp254,6737
+(defconst coq-control-char-format 258,6862
+(defconst coq-control-characters260,6905
+(defconst coq-control-region-format-regexp 264,6997
+(defconst coq-control-regions266,7080
 
 hol98/hol98.el,121
 (defvar hol98-keywords 17,419
@@ -375,6 +388,46 @@ isar/isabelle-system.el,1254
 isar/isar-autotest.el,31
 (defvar isar-long-tests 8,187
 
+isar/isar.el,1595
+(defcustom isar-keywords-name 39,916
+(defpgdefault completion-table 55,1427
+(defcustom isar-web-page57,1480
+(defun isar-strip-terminators 71,1830
+(defun isar-markup-ml 83,2186
+(defun isar-mode-config-set-variables 88,2321
+(defun isar-shell-mode-config-set-variables 153,5120
+(defun isar-set-proof-find-theorems-command 235,8306
+(defpacustom use-find-theorems-form 241,8490
+(defun isar-set-undo-commands 246,8656
+(defpacustom use-linear-undo 260,9248
+(defun isar-configure-from-settings 265,9406
+(defun isar-remove-file 273,9550
+(defun isar-shell-compute-new-files-list 285,9854
+(define-derived-mode isar-shell-mode 304,10424
+(define-derived-mode isar-response-mode 309,10551
+(define-derived-mode isar-goals-mode 314,10684
+(define-derived-mode isar-mode 319,10810
+(defpgdefault menu-entries371,12525
+(defun isar-set-command 402,13719
+(defpgdefault help-menu-entries 407,13849
+(defun isar-count-undos 410,13925
+(defun isar-find-and-forget 436,14891
+(defun isar-goal-command-p 472,16234
+(defun isar-global-save-command-p 477,16411
+(defvar isar-current-goal 498,17195
+(defun isar-state-preserving-p 501,17261
+(defvar isar-shell-current-line-width 526,18110
+(defun isar-shell-adjust-line-width 531,18302
+(defsubst isar-string-wrapping 554,19067
+(defsubst isar-positions-of 563,19261
+(defcustom isar-wrap-commands-singly 569,19466
+(defun isar-command-wrapping 575,19662
+(defun isar-preprocessing 583,19976
+(defun isar-mode-config 601,20527
+(defun isar-shell-mode-config 615,21180
+(defun isar-response-mode-config 625,21529
+(defun isar-goals-mode-config 635,21864
+
 isar/isar-find-theorems.el,779
 (defvar isar-find-theorems-data 19,565
 (defun isar-find-theorems-minibuffer 35,1039
@@ -545,70 +598,12 @@ isar/isar-unicode-tokens.el,1363
 (defconst isar-fraktur-uppercase-letters-tokens 494,12636
 (defconst isar-fraktur-lowercase-letters-tokens 499,12805
 (defcustom isar-token-symbol-map 504,12996
-(defcustom isar-user-tokens 520,13465
-(defun isar-init-token-symbol-map 527,13702
-(defcustom isar-symbol-shortcuts552,14351
-(defcustom isar-shortcut-alist 624,16550
-(defun isar-init-shortcut-alists 632,16809
-(defconst isar-tokens-customizable-variables653,17472
-
-isar/isar.el,1595
-(defcustom isar-keywords-name 39,916
-(defpgdefault completion-table 55,1427
-(defcustom isar-web-page57,1480
-(defun isar-strip-terminators 71,1830
-(defun isar-markup-ml 83,2186
-(defun isar-mode-config-set-variables 88,2321
-(defun isar-shell-mode-config-set-variables 153,5120
-(defun isar-set-proof-find-theorems-command 235,8306
-(defpacustom use-find-theorems-form 241,8490
-(defun isar-set-undo-commands 246,8656
-(defpacustom use-linear-undo 260,9248
-(defun isar-configure-from-settings 265,9408
-(defun isar-remove-file 273,9552
-(defun isar-shell-compute-new-files-list 285,9856
-(define-derived-mode isar-shell-mode 304,10426
-(define-derived-mode isar-response-mode 309,10553
-(define-derived-mode isar-goals-mode 314,10686
-(define-derived-mode isar-mode 319,10812
-(defpgdefault menu-entries371,12527
-(defun isar-set-command 402,13721
-(defpgdefault help-menu-entries 407,13851
-(defun isar-count-undos 410,13927
-(defun isar-find-and-forget 436,14893
-(defun isar-goal-command-p 472,16245
-(defun isar-global-save-command-p 477,16422
-(defvar isar-current-goal 498,17206
-(defun isar-state-preserving-p 501,17272
-(defvar isar-shell-current-line-width 526,18121
-(defun isar-shell-adjust-line-width 531,18313
-(defsubst isar-string-wrapping 554,19078
-(defsubst isar-positions-of 563,19272
-(defcustom isar-wrap-commands-singly 569,19477
-(defun isar-command-wrapping 575,19673
-(defun isar-preprocessing 583,19987
-(defun isar-mode-config 601,20538
-(defun isar-shell-mode-config 615,21191
-(defun isar-response-mode-config 625,21540
-(defun isar-goals-mode-config 635,21875
-
-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
+(defcustom isar-user-tokens 521,13537
+(defun isar-init-token-symbol-map 535,13977
+(defcustom isar-symbol-shortcuts560,14626
+(defcustom isar-shortcut-alist 632,16825
+(defun isar-init-shortcut-alists 640,17084
+(defconst isar-tokens-customizable-variables661,17747
 
 lego/lego.el,1636
 (defcustom lego-tags 21,535
@@ -652,6 +647,41 @@ lego/lego.el,1636
 (defun lego-shell-mode-config 373,12756
 (defun lego-goals-mode-config 420,14423
 
+lego/lego-syntax.el,600
+(defconst lego-keywords-goal 15,358
+(defconst lego-keywords-save 17,401
+(defconst lego-commands19,472
+(defconst lego-keywords31,1030
+(defconst lego-tacticals 36,1207
+(defconst lego-error-regexp 39,1315
+(defvar lego-id 42,1473
+(defvar lego-ids 44,1500
+(defconst lego-arg-list-regexp 48,1696
+(defun lego-decl-defn-regexp 51,1812
+(defconst lego-definiendum-alternative-regexp59,2184
+(defvar lego-font-lock-terms63,2368
+(defconst lego-goal-with-hole-regexp89,3221
+(defconst lego-save-with-hole-regexp94,3443
+(defvar lego-font-lock-keywords-199,3660
+(defun lego-init-syntax-table 110,4122
+
+phox/phox.el,555
+(defcustom phox-prog-name 32,916
+(defcustom phox-web-page37,1018
+(defcustom phox-doc-dir43,1168
+(defcustom phox-lib-dir49,1315
+(defcustom phox-tags-program55,1458
+(defcustom phox-tags-doc61,1637
+(defcustom phox-etags67,1774
+(defpgdefault menu-entries88,2224
+(defun phox-config 102,2417
+(defun phox-shell-config 146,4343
+(define-derived-mode phox-mode 170,5205
+(define-derived-mode phox-shell-mode 186,5668
+(define-derived-mode phox-response-mode 191,5796
+(define-derived-mode phox-goals-mode 201,6157
+(defpgdefault completion-table224,6943
+
 phox/phox-extraction.el,383
 (defvar phox-prog-orig 19,619
 (defun phox-prog-flags-modify(21,687
@@ -790,75 +820,59 @@ phox/phox-tags.el,305
 (defun phox-complete-tag(69,2091
 (defvar phox-tags-menu76,2200
 
-phox/phox.el,555
-(defcustom phox-prog-name 32,916
-(defcustom phox-web-page37,1018
-(defcustom phox-doc-dir43,1168
-(defcustom phox-lib-dir49,1315
-(defcustom phox-tags-program55,1458
-(defcustom phox-tags-doc61,1637
-(defcustom phox-etags67,1774
-(defpgdefault menu-entries88,2224
-(defun phox-config 102,2417
-(defun phox-shell-config 146,4343
-(define-derived-mode phox-mode 170,5205
-(define-derived-mode phox-shell-mode 186,5668
-(define-derived-mode phox-response-mode 191,5796
-(define-derived-mode phox-goals-mode 201,6157
-(defpgdefault completion-table224,6943
-
 generic/pg-assoc.el,81
 (defun proof-associated-buffers 33,973
 (defun proof-associated-windows 43,1183
 
-generic/pg-autotest.el,868
+generic/pg-autotest.el,869
 (defvar pg-autotest-success 30,692
 (defvar pg-autotest-log 33,779
-(defadvice proof-debug 38,916
-(defun pg-autotest-find-file 44,1092
-(defun pg-autotest-find-file-restart 51,1358
-(defmacro pg-autotest 64,1811
-(defun pg-autotest-log 91,2532
-(defun pg-autotest-message 99,2756
-(defun pg-autotest-remark 108,3040
-(defun pg-autotest-timestart 111,3121
-(defun pg-autotest-timetaken 116,3304
-(defun pg-autotest-exit 127,3668
-(defun pg-autotest-test-process-wholefile 138,4019
-(defun pg-autotest-test-script-wholefile 146,4306
-(defun pg-autotest-test-script-randomjumps 171,5238
-(defun pg-autotest-test-retract-file 221,6847
-(defun pg-autotest-test-assert-processed 227,6988
-(defun pg-autotest-test-assert-full 233,7214
-(defun pg-autotest-test-assert-unprocessed 240,7455
-(defun pg-autotest-test-eval 247,7720
-(defun pg-autotest-test-quit-prover 251,7819
-
-generic/pg-custom.el,556
-(defpgcustom script-indent 36,1140
-(defconst proof-toolbar-entries-default41,1277
-(defpgcustom toolbar-entries 69,3008
-(defpgcustom prog-args 88,3741
-(defpgcustom prog-env 101,4316
-(defpgcustom favourites 110,4743
-(defpgcustom menu-entries 115,4932
-(defpgcustom help-menu-entries 122,5168
-(defpgcustom keymap 129,5431
-(defpgcustom completion-table 134,5602
-(defpgcustom tags-program 145,5976
-(defpgcustom use-holes 154,6360
-(defpgcustom maths-menu-enable 164,6641
-(defpgcustom unicode-tokens-enable 170,6821
-(defpgcustom mmm-enable 176,6998
+(defadvice proof-debug 39,972
+(defun pg-autotest-find-file 47,1176
+(defun pg-autotest-find-file-restart 54,1442
+(defmacro pg-autotest 68,1916
+(defun pg-autotest-log 95,2637
+(defun pg-autotest-message 103,2861
+(defun pg-autotest-remark 112,3150
+(defun pg-autotest-timestart 115,3231
+(defun pg-autotest-timetaken 120,3414
+(defun pg-autotest-exit 131,3778
+(defun pg-autotest-test-process-wholefile 142,4129
+(defun pg-autotest-test-script-wholefile 150,4416
+(defun pg-autotest-test-script-randomjumps 175,5348
+(defun pg-autotest-test-retract-file 224,6905
+(defun pg-autotest-test-assert-processed 230,7046
+(defun pg-autotest-test-assert-full 236,7272
+(defun pg-autotest-test-assert-unprocessed 243,7513
+(defun pg-autotest-test-eval 250,7778
+(defun pg-autotest-test-quit-prover 254,7877
+
+generic/pg-custom.el,599
+(defpgcustom script-indent 37,1199
+(defconst proof-toolbar-entries-default42,1336
+(defpgcustom toolbar-entries 70,3069
+(defpgcustom prog-args 89,3802
+(defpgcustom prog-env 102,4377
+(defpgcustom favourites 111,4804
+(defpgcustom menu-entries 116,4993
+(defpgcustom help-menu-entries 123,5229
+(defpgcustom keymap 130,5492
+(defpgcustom completion-table 135,5663
+(defpgcustom tags-program 146,6037
+(defpgcustom use-holes 155,6421
+(defpgcustom one-command-per-line162,6679
+(defpgcustom maths-menu-enable 173,6915
+(defpgcustom unicode-tokens-enable 179,7095
+(defpgcustom mmm-enable 185,7272
 
 generic/pg-goals.el,285
 (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,1921
-(defun pg-goals-display 76,2187
-(defun pg-goals-button-action 117,3491
+(defun proof-goals-config-done 68,1923
+(defun pg-goals-display 76,2189
+(defun pg-goals-button-action 117,3493
 
 generic/pg-movie.el,334
 (defconst pg-movie-xml-header 33,944
@@ -872,20 +886,20 @@ generic/pg-movie.el,334
 (defun pg-movie-export-directory 120,3496
 
 generic/pg-pamacs.el,486
-(defmacro deflocal 37,1200
-(deflocal proof-buffer-type 44,1438
-(defmacro proof-ass-sym 52,1574
-(defmacro proof-ass-symv 58,1833
-(defmacro proof-ass 64,2091
-(defun proof-defpgcustom-fn 70,2343
-(defun undefpgcustom 91,3213
-(defmacro defpgcustom 97,3437
-(defun proof-defpgdefault-fn 108,3848
-(defmacro defpgdefault 122,4306
-(defmacro defpgfun 133,4668
-(defun proof-defpacustom-fn 147,5067
-(defmacro defpacustom 211,7251
-(defmacro proof-eval-when-ready-for-assistant 232,8198
+(defmacro deflocal 35,1132
+(deflocal proof-buffer-type 42,1370
+(defmacro proof-ass-sym 50,1506
+(defmacro proof-ass-symv 56,1765
+(defmacro proof-ass 62,2023
+(defun proof-defpgcustom-fn 68,2275
+(defun undefpgcustom 89,3145
+(defmacro defpgcustom 95,3369
+(defun proof-defpgdefault-fn 106,3780
+(defmacro defpgdefault 120,4238
+(defmacro defpgfun 131,4600
+(defun proof-defpacustom-fn 145,4999
+(defmacro defpacustom 209,7183
+(defmacro proof-eval-when-ready-for-assistant 230,8130
 
 generic/pg-pbrpm.el,1808
 (defvar pg-pbrpm-use-buffer-menu 45,1208
@@ -911,24 +925,24 @@ generic/pg-pbrpm.el,1808
 (defun pg-pbrpm-build-menu 206,7205
 (defun pg-pbrpm-setup-span 269,9525
 (defun pg-pbrpm-run-command 329,11824
-(defun pg-pbrpm-get-pos-info 362,13345
-(defun pg-pbrpm-get-region-info 404,14644
-(defun pg-pbrpm-auto-select-around-point 415,15056
-(defun pg-pbrpm-translate-position 430,15580
-(defun pg-pbrpm-process-click 438,15834
-(defvar pg-pbrpm-remember-region-selected-region 458,16859
-(defvar pg-pbrpm-regions-list 459,16913
-(defun pg-pbrpm-erase-regions-list 461,16949
-(defun pg-pbrpm-filter-regions-list 470,17257
-(defface pg-pbrpm-multiple-selection-face477,17520
-(defface pg-pbrpm-menu-input-face485,17722
-(defun pg-pbrpm-do-remember-region 493,17912
-(defun pg-pbrpm-remember-region-drag-up-hook 514,18760
-(defun pg-pbrpm-remember-region-click-hook 518,18931
-(defun pg-pbrpm-remember-region 523,19116
-(defun pg-pbrpm-process-region 537,19830
-(defun pg-pbrpm-process-regions-list 555,20559
-(defun pg-pbrpm-region-expression 559,20742
+(defun pg-pbrpm-get-pos-info 362,13349
+(defun pg-pbrpm-get-region-info 404,14648
+(defun pg-pbrpm-auto-select-around-point 415,15060
+(defun pg-pbrpm-translate-position 430,15584
+(defun pg-pbrpm-process-click 438,15838
+(defvar pg-pbrpm-remember-region-selected-region 458,16863
+(defvar pg-pbrpm-regions-list 459,16917
+(defun pg-pbrpm-erase-regions-list 461,16953
+(defun pg-pbrpm-filter-regions-list 470,17261
+(defface pg-pbrpm-multiple-selection-face477,17524
+(defface pg-pbrpm-menu-input-face485,17726
+(defun pg-pbrpm-do-remember-region 493,17916
+(defun pg-pbrpm-remember-region-drag-up-hook 514,18764
+(defun pg-pbrpm-remember-region-click-hook 518,18935
+(defun pg-pbrpm-remember-region 523,19120
+(defun pg-pbrpm-process-region 537,19834
+(defun pg-pbrpm-process-regions-list 555,20563
+(defun pg-pbrpm-region-expression 559,20746
 
 generic/pg-pgip.el,2931
 (defalias 'pg-pgip-debug pg-pgip-debug
38,1032
@@ -1032,96 +1046,95 @@ generic/pg-response.el,1291
 (defun proof-trace-buffer-finish 459,15774
 (defun pg-thms-buffer-clear 477,16117
 
-generic/pg-user.el,3700
+generic/pg-user.el,3635
 (defun proof-script-new-command-advance 42,1232
-(defun proof-maybe-follow-locked-end 85,2994
-(defun proof-goto-command-start 112,3870
-(defun proof-goto-command-end 135,4817
-(defun proof-goto-point 158,5342
-(defun proof-assert-next-command-interactive 172,5776
-(defun proof-assert-until-point-interactive 184,6262
-(defun proof-process-buffer 190,6492
-(defun proof-undo-last-successful-command 208,7004
-(defun proof-undo-and-delete-last-successful-command 213,7166
-(defun proof-undo-last-successful-command-1 226,7720
-(defun proof-retract-buffer 243,8339
-(defun proof-retract-current-goal 252,8623
-(defun proof-mouse-goto-point 271,9143
-(defvar proof-minibuffer-history 286,9419
-(defun proof-minibuffer-cmd 289,9514
-(defun proof-frob-locked-end 328,10921
-(defmacro proof-if-setting-configured 389,12859
-(defmacro proof-define-assistant-command 397,13128
-(defmacro proof-define-assistant-command-witharg 410,13583
-(defun proof-issue-new-command 430,14405
-(defun proof-cd-sync 470,15628
-(defun proof-electric-terminator-enable 523,17298
-(defun proof-electric-terminator 530,17542
-(defun proof-add-completions 555,18346
-(defun proof-script-complete 580,19235
-(defun pg-copy-span-contents 594,19544
-(defun pg-numth-span-higher-or-lower 611,20102
-(defun pg-control-span-of 637,20848
-(defun pg-move-span-contents 643,21052
-(defun pg-fixup-children-spans 695,23228
-(defun pg-move-region-down 705,23485
-(defun pg-move-region-up 714,23778
-(defun proof-forward-command 744,24606
-(defun proof-backward-command 765,25327
-(defun pg-pos-for-event 787,25671
-(defun pg-span-for-event 793,25892
-(defun pg-span-context-menu 797,26036
-(defun pg-toggle-visibility 812,26484
-(defun pg-create-in-span-context-menu 821,26791
-(defun pg-span-undo 850,28005
-(defun pg-goals-buffers-hint 896,29388
-(defun pg-slow-fontify-tracing-hint 900,29570
-(defun pg-response-buffers-hint 904,29741
-(defun pg-jump-to-end-hint 916,30156
-(defun pg-processing-complete-hint 920,30285
-(defun pg-next-error-hint 937,31005
-(defun pg-hint 942,31157
-(defun pg-identifier-under-mouse-query 958,31747
-(defun pg-identifier-near-point-query 968,32056
-(defvar proof-query-identifier-collection 996,32953
-(defvar proof-query-identifier-history 997,33000
-(defun proof-query-identifier 999,33045
-(defun pg-identifier-query 1010,33364
-(defun proof-imenu-enable 1043,34512
-(defvar pg-input-ring 1079,35815
-(defvar pg-input-ring-index 1082,35872
-(defvar pg-stored-incomplete-input 1085,35944
-(defun pg-previous-input 1088,36047
-(defun pg-next-input 1102,36504
-(defun pg-delete-input 1107,36626
-(defun pg-get-old-input 1120,36964
-(defun pg-restore-input 1134,37355
-(defun pg-search-start 1145,37645
-(defun pg-regexp-arg 1157,38137
-(defun pg-search-arg 1169,38585
-(defun pg-previous-matching-input-string-position 1183,39002
-(defun pg-previous-matching-input 1210,40167
-(defun pg-next-matching-input 1229,41017
-(defvar pg-matching-input-from-input-string 1237,41400
-(defun pg-previous-matching-input-from-input 1241,41514
-(defun pg-next-matching-input-from-input 1259,42279
-(defun pg-add-to-input-history 1270,42658
-(defun pg-remove-from-input-history 1282,43111
-(defun  pg-clear-input-ring 1293,43491
-(define-key proof-mode-map 1310,43961
-(define-key proof-mode-map 1311,44021
-(defun pg-protected-undo 1313,44093
-(defun pg-protected-undo-1 1348,45483
-(defun next-undo-elt 1379,46917
-(defvar proof-autosend-timer 1406,47873
-(deflocal proof-autosend-modified-tick 1408,47934
-(defun proof-autosend-enable 1412,48056
-(defun proof-autosend-delay 1426,48599
-(defun proof-autosend-loop 1430,48732
-(defun proof-autosend-loop-all 1442,49191
-(defun proof-autosend-loop-next 1468,50117
-
-generic/pg-vars.el,1451
+(defun proof-maybe-follow-locked-end 66,2157
+(defun proof-goto-command-start 92,2993
+(defun proof-goto-command-end 115,3940
+(defun proof-forward-command 130,4362
+(defun proof-backward-command 151,5083
+(defun proof-goto-point 162,5297
+(defun proof-assert-next-command-interactive 176,5731
+(defun proof-assert-until-point-interactive 188,6217
+(defun proof-process-buffer 194,6447
+(defun proof-undo-last-successful-command 212,6959
+(defun proof-undo-and-delete-last-successful-command 217,7121
+(defun proof-undo-last-successful-command-1 229,7642
+(defun proof-retract-buffer 246,8306
+(defun proof-retract-current-goal 255,8590
+(defun proof-mouse-goto-point 274,9110
+(defvar proof-minibuffer-history 289,9386
+(defun proof-minibuffer-cmd 292,9481
+(defun proof-frob-locked-end 331,10888
+(defmacro proof-if-setting-configured 367,11989
+(defmacro proof-define-assistant-command 375,12258
+(defmacro proof-define-assistant-command-witharg 388,12713
+(defun proof-issue-new-command 408,13535
+(defun proof-cd-sync 448,14758
+(defun proof-electric-terminator-enable 499,16357
+(defun proof-electric-terminator 507,16661
+(defun proof-add-completions 531,17441
+(defun proof-script-complete 554,18264
+(defun pg-copy-span-contents 568,18573
+(defun pg-numth-span-higher-or-lower 582,18997
+(defun pg-control-span-of 608,19743
+(defun pg-move-span-contents 614,19947
+(defun pg-fixup-children-spans 665,22065
+(defun pg-move-region-down 675,22322
+(defun pg-move-region-up 684,22615
+(defun pg-pos-for-event 698,22889
+(defun pg-span-for-event 704,23110
+(defun pg-span-context-menu 708,23254
+(defun pg-toggle-visibility 724,23771
+(defun pg-create-in-span-context-menu 733,24078
+(defun pg-span-undo 757,25010
+(defun pg-goals-buffers-hint 770,25248
+(defun pg-slow-fontify-tracing-hint 774,25430
+(defun pg-response-buffers-hint 778,25601
+(defun pg-jump-to-end-hint 790,26016
+(defun pg-processing-complete-hint 794,26145
+(defun pg-next-error-hint 811,26865
+(defun pg-hint 816,27017
+(defun pg-identifier-under-mouse-query 827,27366
+(defun pg-identifier-near-point-query 838,27690
+(defvar proof-query-identifier-history 867,28613
+(defun proof-query-identifier 870,28700
+(defun pg-identifier-query 881,29056
+(defun proof-imenu-enable 914,30204
+(defvar pg-input-ring 950,31507
+(defvar pg-input-ring-index 953,31564
+(defvar pg-stored-incomplete-input 956,31636
+(defun pg-previous-input 959,31739
+(defun pg-next-input 973,32202
+(defun pg-delete-input 978,32324
+(defun pg-get-old-input 991,32662
+(defun pg-restore-input 1005,33053
+(defun pg-search-start 1016,33343
+(defun pg-regexp-arg 1028,33835
+(defun pg-search-arg 1040,34283
+(defun pg-previous-matching-input-string-position 1054,34700
+(defun pg-previous-matching-input 1081,35865
+(defun pg-next-matching-input 1100,36715
+(defvar pg-matching-input-from-input-string 1108,37098
+(defun pg-previous-matching-input-from-input 1112,37212
+(defun pg-next-matching-input-from-input 1130,37977
+(defun pg-add-to-input-history 1141,38356
+(defun pg-remove-from-input-history 1153,38809
+(defun  pg-clear-input-ring 1164,39189
+(define-key proof-mode-map 1181,39659
+(define-key proof-mode-map 1182,39719
+(defun pg-protected-undo 1184,39791
+(defun pg-protected-undo-1 1214,41085
+(defun next-undo-elt 1245,42522
+(defvar proof-autosend-timer 1272,43478
+(deflocal proof-autosend-modified-tick 1274,43539
+(defun proof-autosend-enable 1278,43661
+(defun proof-autosend-delay 1292,44204
+(defun proof-autosend-loop 1296,44337
+(defun proof-autosend-loop-all 1310,44897
+(defun proof-autosend-loop-next 1334,45677
+
+generic/pg-vars.el,1500
 (defvar proof-assistant-cusgrp 22,389
 (defvar proof-assistant-internals-cusgrp 28,649
 (defvar proof-assistant 34,919
@@ -1153,10 +1166,11 @@ generic/pg-vars.el,1451
 (defvar proof-nesting-depth 215,7790
 (defvar proof-last-theorem-dependencies 222,8025
 (defvar proof-autosend-running 226,8187
-(defcustom proof-general-name 236,8460
-(defcustom proof-general-home-page241,8617
-(defcustom proof-unnamed-theorem-name247,8777
-(defcustom proof-universal-keys253,8961
+(defvar proof-next-command-on-new-line 231,8386
+(defcustom proof-general-name 242,8620
+(defcustom proof-general-home-page247,8777
+(defcustom proof-unnamed-theorem-name253,8937
+(defcustom proof-universal-keys259,9121
 
 generic/pg-xml.el,1177
 (defalias 'pg-xml-error pg-xml-error
18,381
@@ -1275,86 +1289,86 @@ generic/proof-config.el,7744
 (defcustom proof-shell-auto-terminate-commands 805,29809
 (defcustom proof-shell-pre-sync-init-cmd 814,30214
 (defcustom proof-shell-init-cmd 828,30772
-(defcustom proof-shell-init-hook 840,31301
-(defcustom proof-shell-restart-cmd 845,31440
-(defcustom proof-shell-quit-cmd 850,31595
-(defcustom proof-shell-quit-timeout 855,31762
-(defcustom proof-shell-cd-cmd 864,32153
-(defcustom proof-shell-start-silent-cmd 881,32824
-(defcustom proof-shell-stop-silent-cmd 890,33200
-(defcustom proof-shell-silent-threshold 899,33535
-(defcustom  proof-shell-inform-file-processed-cmd 907,33869
-(defcustom  proof-shell-inform-file-retracted-cmd 928,34797
-(defcustom proof-auto-multiple-files 956,36069
-(defcustom proof-cannot-reopen-processed-files 971,36790
-(defcustom proof-shell-require-command-regexp 985,37456
-(defcustom proof-done-advancing-require-function 996,37918
-(defcustom proof-shell-annotated-prompt-regexp 1008,38278
-(defcustom proof-shell-error-regexp 1023,38843
-(defcustom proof-shell-truncate-before-error 1043,39645
-(defcustom pg-next-error-regexp 1057,40184
-(defcustom pg-next-error-filename-regexp 1072,40793
-(defcustom pg-next-error-extract-filename 1096,41826
-(defcustom proof-shell-interrupt-regexp 1103,42069
-(defcustom proof-shell-proof-completed-regexp 1117,42664
-(defcustom proof-shell-clear-response-regexp 1130,43172
-(defcustom proof-shell-clear-goals-regexp 1142,43624
-(defcustom proof-shell-start-goals-regexp 1154,44070
-(defcustom proof-shell-end-goals-regexp 1162,44437
-(defcustom proof-shell-eager-annotation-start 1176,45010
-(defcustom proof-shell-eager-annotation-start-length 1199,46029
-(defcustom proof-shell-eager-annotation-end 1210,46455
-(defcustom proof-shell-strip-output-markup 1226,47130
-(defcustom proof-shell-assumption-regexp 1235,47515
-(defcustom proof-shell-process-file 1245,47919
-(defcustom proof-shell-retract-files-regexp 1271,48995
-(defcustom proof-shell-compute-new-files-list 1284,49483
-(defcustom pg-special-char-regexp 1299,50050
-(defcustom proof-shell-set-elisp-variable-regexp 1304,50194
-(defcustom proof-shell-match-pgip-cmd 1342,51860
-(defcustom proof-shell-issue-pgip-cmd 1356,52342
-(defcustom proof-use-pgip-askprefs 1361,52507
-(defcustom proof-shell-query-dependencies-cmd 1369,52854
-(defcustom proof-shell-theorem-dependency-list-regexp 1376,53114
-(defcustom proof-shell-theorem-dependency-list-split 1392,53774
-(defcustom proof-shell-show-dependency-cmd 1401,54197
-(defcustom proof-shell-trace-output-regexp 1423,55103
-(defcustom proof-shell-thms-output-regexp 1441,55697
-(defcustom proof-tokens-activate-command 1454,56080
-(defcustom proof-tokens-deactivate-command 1461,56320
-(defcustom proof-tokens-extra-modes 1468,56565
-(defcustom proof-shell-unicode 1483,57070
-(defcustom proof-shell-filename-escapes 1492,57460
-(defcustom proof-shell-process-connection-type 1509,58140
-(defcustom proof-shell-strip-crs-from-input 1515,58331
-(defcustom proof-shell-strip-crs-from-output 1527,58814
-(defcustom proof-shell-insert-hook 1535,59182
-(defcustom proof-script-preprocess 1576,61142
-(defcustom proof-shell-handle-delayed-output-hook1582,61293
-(defcustom proof-shell-handle-error-or-interrupt-hook1588,61508
-(defcustom proof-shell-pre-interrupt-hook1606,62254
-(defcustom proof-shell-handle-output-system-specific 1614,62525
-(defcustom proof-state-change-hook 1637,63498
-(defcustom proof-shell-syntax-table-entries 1647,63891
-(defgroup proof-goals 1665,64262
-(defcustom pg-subterm-first-special-char 1670,64383
-(defcustom pg-subterm-anns-use-stack 1678,64695
-(defcustom pg-goals-change-goal 1687,64994
-(defcustom pbp-goal-command 1692,65110
-(defcustom pbp-hyp-command 1697,65266
-(defcustom pg-subterm-help-cmd 1702,65428
-(defcustom pg-goals-error-regexp 1709,65664
-(defcustom proof-shell-result-start 1714,65824
-(defcustom proof-shell-result-end 1720,66058
-(defcustom pg-subterm-start-char 1726,66271
-(defcustom pg-subterm-sep-char 1737,66745
-(defcustom pg-subterm-end-char 1743,66924
-(defcustom pg-topterm-regexp 1749,67081
-(defcustom proof-goals-font-lock-keywords 1764,67681
-(defcustom proof-response-font-lock-keywords 1772,68040
-(defcustom proof-shell-font-lock-keywords 1780,68402
-(defcustom pg-before-fontify-output-hook 1791,68916
-(defcustom pg-after-fontify-output-hook 1799,69277
+(defcustom proof-shell-init-hook 840,31318
+(defcustom proof-shell-restart-cmd 845,31457
+(defcustom proof-shell-quit-cmd 850,31612
+(defcustom proof-shell-quit-timeout 855,31779
+(defcustom proof-shell-cd-cmd 864,32170
+(defcustom proof-shell-start-silent-cmd 881,32841
+(defcustom proof-shell-stop-silent-cmd 890,33217
+(defcustom proof-shell-silent-threshold 899,33552
+(defcustom  proof-shell-inform-file-processed-cmd 907,33886
+(defcustom  proof-shell-inform-file-retracted-cmd 928,34814
+(defcustom proof-auto-multiple-files 956,36086
+(defcustom proof-cannot-reopen-processed-files 971,36807
+(defcustom proof-shell-require-command-regexp 985,37473
+(defcustom proof-done-advancing-require-function 996,37935
+(defcustom proof-shell-annotated-prompt-regexp 1008,38295
+(defcustom proof-shell-error-regexp 1023,38860
+(defcustom proof-shell-truncate-before-error 1043,39662
+(defcustom pg-next-error-regexp 1057,40201
+(defcustom pg-next-error-filename-regexp 1072,40810
+(defcustom pg-next-error-extract-filename 1096,41843
+(defcustom proof-shell-interrupt-regexp 1103,42086
+(defcustom proof-shell-proof-completed-regexp 1117,42681
+(defcustom proof-shell-clear-response-regexp 1130,43189
+(defcustom proof-shell-clear-goals-regexp 1142,43641
+(defcustom proof-shell-start-goals-regexp 1154,44087
+(defcustom proof-shell-end-goals-regexp 1162,44454
+(defcustom proof-shell-eager-annotation-start 1176,45027
+(defcustom proof-shell-eager-annotation-start-length 1199,46046
+(defcustom proof-shell-eager-annotation-end 1210,46472
+(defcustom proof-shell-strip-output-markup 1226,47147
+(defcustom proof-shell-assumption-regexp 1235,47532
+(defcustom proof-shell-process-file 1245,47936
+(defcustom proof-shell-retract-files-regexp 1271,49012
+(defcustom proof-shell-compute-new-files-list 1284,49500
+(defcustom pg-special-char-regexp 1299,50067
+(defcustom proof-shell-set-elisp-variable-regexp 1304,50211
+(defcustom proof-shell-match-pgip-cmd 1342,51877
+(defcustom proof-shell-issue-pgip-cmd 1356,52359
+(defcustom proof-use-pgip-askprefs 1361,52524
+(defcustom proof-shell-query-dependencies-cmd 1369,52871
+(defcustom proof-shell-theorem-dependency-list-regexp 1376,53131
+(defcustom proof-shell-theorem-dependency-list-split 1392,53791
+(defcustom proof-shell-show-dependency-cmd 1401,54214
+(defcustom proof-shell-trace-output-regexp 1423,55120
+(defcustom proof-shell-thms-output-regexp 1441,55714
+(defcustom proof-tokens-activate-command 1454,56097
+(defcustom proof-tokens-deactivate-command 1461,56337
+(defcustom proof-tokens-extra-modes 1468,56582
+(defcustom proof-shell-unicode 1483,57087
+(defcustom proof-shell-filename-escapes 1492,57477
+(defcustom proof-shell-process-connection-type 1509,58157
+(defcustom proof-shell-strip-crs-from-input 1515,58348
+(defcustom proof-shell-strip-crs-from-output 1527,58831
+(defcustom proof-shell-insert-hook 1535,59199
+(defcustom proof-script-preprocess 1576,61159
+(defcustom proof-shell-handle-delayed-output-hook1582,61310
+(defcustom proof-shell-handle-error-or-interrupt-hook1588,61525
+(defcustom proof-shell-pre-interrupt-hook1606,62271
+(defcustom proof-shell-handle-output-system-specific 1614,62542
+(defcustom proof-state-change-hook 1637,63515
+(defcustom proof-shell-syntax-table-entries 1647,63908
+(defgroup proof-goals 1665,64279
+(defcustom pg-subterm-first-special-char 1670,64400
+(defcustom pg-subterm-anns-use-stack 1678,64712
+(defcustom pg-goals-change-goal 1687,65011
+(defcustom pbp-goal-command 1692,65127
+(defcustom pbp-hyp-command 1697,65283
+(defcustom pg-subterm-help-cmd 1702,65445
+(defcustom pg-goals-error-regexp 1709,65681
+(defcustom proof-shell-result-start 1714,65841
+(defcustom proof-shell-result-end 1720,66075
+(defcustom pg-subterm-start-char 1726,66288
+(defcustom pg-subterm-sep-char 1737,66762
+(defcustom pg-subterm-end-char 1743,66941
+(defcustom pg-topterm-regexp 1749,67098
+(defcustom proof-goals-font-lock-keywords 1764,67698
+(defcustom proof-response-font-lock-keywords 1772,68057
+(defcustom proof-shell-font-lock-keywords 1780,68419
+(defcustom pg-before-fontify-output-hook 1791,68933
+(defcustom pg-after-fontify-output-hook 1799,69294
 
 generic/proof-depends.el,917
 (defvar proof-thm-names-of-files 25,639
@@ -1385,7 +1399,7 @@ generic/proof-easy-config.el,192
 (defun proof-easy-config-check-setup 52,2135
 (defmacro proof-easy-config 84,3465
 
-generic/proof-faces.el,1595
+generic/proof-faces.el,1809
 (defgroup proof-faces 29,809
 (defconst pg-defface-window-systems36,989
 (defmacro proof-face-specs 49,1551
@@ -1400,29 +1414,33 @@ generic/proof-faces.el,1595
 (defface proof-debug-message-face134,4111
 (defface proof-boring-face142,4310
 (defface proof-mouse-highlight-face150,4502
-(defface proof-highlight-dependent-face158,4720
-(defface proof-highlight-dependency-face166,4927
-(defface proof-active-area-face174,5124
-(defface proof-script-sticky-error-face182,5436
-(defface proof-script-highlight-error-face190,5665
-(defconst proof-face-compat-doc 202,6010
-(defconst proof-queue-face 203,6090
-(defconst proof-locked-face 204,6158
-(defconst proof-declaration-name-face 205,6228
-(defconst proof-tacticals-name-face 206,6318
-(defconst proof-tactics-name-face 207,6404
-(defconst proof-error-face 208,6486
-(defconst proof-script-sticky-error-face 209,6554
-(defconst proof-script-highlight-error-face 210,6650
-(defconst proof-warning-face 211,6752
-(defconst proof-eager-annotation-face 212,6824
-(defconst proof-debug-message-face 213,6914
-(defconst proof-boring-face 214,6998
-(defconst proof-mouse-highlight-face 215,7068
-(defconst proof-highlight-dependent-face 216,7156
-(defconst proof-highlight-dependency-face 217,7252
-(defconst proof-active-area-face 218,7350
-(defconst proof-script-error-face 219,7430
+(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,449
@@ -1436,372 +1454,381 @@ generic/proof-maths-menu.el,83
 (defun proof-maths-menu-set-global 32,906
 (defun proof-maths-menu-enable 46,1357
 
-generic/proof-menu.el,2074
+generic/proof-menu.el,2168
 (defvar proof-display-some-buffers-count 36,816
 (defun proof-display-some-buffers 38,861
 (defun proof-menu-define-keys 95,2988
-(defun proof-menu-define-main 153,5808
-(defvar proof-menu-favourites 162,5993
-(defvar proof-menu-settings 165,6100
-(defun proof-menu-define-specific 169,6189
-(defun proof-assistant-menu-update 212,7451
-(defvar proof-help-menu226,7884
-(defvar proof-show-hide-menu234,8154
-(defvar proof-buffer-menu245,8578
-(defun proof-keep-response-history 308,10894
-(defconst proof-quick-opts-menu316,11204
-(defun proof-quick-opts-vars 528,19836
-(defun proof-quick-opts-changed-from-defaults-p 560,20776
-(defun proof-quick-opts-changed-from-saved-p 564,20881
-(defun proof-quick-opts-save 575,21232
-(defun proof-quick-opts-reset 580,21400
-(defconst proof-config-menu592,21668
-(defconst proof-advanced-menu599,21847
-(defvar proof-menu617,22531
-(defun proof-main-menu 626,22813
-(defun proof-aux-menu 638,23152
-(defun proof-menu-define-favourites-menu 654,23498
-(defun proof-def-favourite 674,24147
-(defvar proof-make-favourite-cmd-history 701,25140
-(defvar proof-make-favourite-menu-history 704,25225
-(defun proof-save-favourites 707,25311
-(defun proof-del-favourite 712,25459
-(defun proof-read-favourite 729,26015
-(defun proof-add-favourite 753,26789
-(defun proof-menu-define-settings-menu 780,27834
-(defun proof-menu-entry-name 813,28965
-(defun proof-menu-entry-for-setting 823,29315
-(defun proof-settings-vars 842,29847
-(defun proof-settings-changed-from-defaults-p 847,30024
-(defun proof-settings-changed-from-saved-p 851,30130
-(defun proof-settings-save 855,30233
-(defun proof-settings-reset 860,30400
-(defun proof-assistant-invisible-command-ifposs 865,30563
-(defun proof-maybe-askprefs 887,31533
-(defun proof-assistant-settings-cmd 893,31726
-(defun proof-assistant-settings-cmds 901,32010
-(defvar proof-assistant-format-table911,32352
-(defun proof-assistant-format-bool 919,32722
-(defun proof-assistant-format-int 922,32835
-(defun proof-assistant-format-string 925,32927
-(defun proof-assistant-format 928,33025
+(defun proof-menu-define-main 153,5813
+(defvar proof-menu-favourites 162,5998
+(defvar proof-menu-settings 165,6105
+(defun proof-menu-define-specific 169,6194
+(defun proof-assistant-menu-update 212,7456
+(defvar proof-help-menu226,7889
+(defvar proof-show-hide-menu234,8159
+(defvar proof-buffer-menu245,8583
+(defun proof-keep-response-history 308,10899
+(defconst proof-quick-opts-menu316,11209
+(defun proof-quick-opts-vars 534,20115
+(defun proof-quick-opts-changed-from-defaults-p 566,21055
+(defun proof-quick-opts-changed-from-saved-p 570,21160
+(defun proof-set-document-centred 578,21316
+(defun proof-set-non-document-centred 591,21742
+(defun proof-quick-opts-save 610,22453
+(defun proof-quick-opts-reset 615,22621
+(defconst proof-config-menu627,22889
+(defconst proof-advanced-menu634,23068
+(defvar proof-menu652,23752
+(defun proof-main-menu 661,24034
+(defun proof-aux-menu 673,24373
+(defun proof-menu-define-favourites-menu 689,24719
+(defun proof-def-favourite 709,25368
+(defvar proof-make-favourite-cmd-history 736,26361
+(defvar proof-make-favourite-menu-history 739,26446
+(defun proof-save-favourites 742,26532
+(defun proof-del-favourite 747,26680
+(defun proof-read-favourite 764,27236
+(defun proof-add-favourite 788,28010
+(defun proof-menu-define-settings-menu 815,29055
+(defun proof-menu-entry-name 848,30186
+(defun proof-menu-entry-for-setting 858,30536
+(defun proof-settings-vars 877,31068
+(defun proof-settings-changed-from-defaults-p 882,31245
+(defun proof-settings-changed-from-saved-p 886,31351
+(defun proof-settings-save 890,31454
+(defun proof-settings-reset 895,31621
+(defun proof-assistant-invisible-command-ifposs 900,31784
+(defun proof-maybe-askprefs 922,32754
+(defun proof-assistant-settings-cmd 928,32947
+(defun proof-assistant-settings-cmds 936,33231
+(defvar proof-assistant-format-table946,33573
+(defun proof-assistant-format-bool 954,33943
+(defun proof-assistant-format-int 957,34056
+(defun proof-assistant-format-string 960,34148
+(defun proof-assistant-format 963,34246
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 43,1439
 (defun proof-mmm-enable 58,1978
 
-generic/proof-script.el,5425
+generic/proof-script.el,5496
 (deflocal proof-active-buffer-fake-minor-mode 46,1414
 (deflocal proof-script-buffer-file-name 49,1540
 (deflocal pg-script-portions 56,1950
 (defun proof-next-element-count 66,2170
 (defun proof-element-id 72,2412
 (defun proof-next-element-id 76,2581
-(deflocal proof-locked-span 112,3907
-(deflocal proof-queue-span 119,4173
-(deflocal proof-overlay-arrow 128,4659
-(defun proof-span-give-warning 134,4786
-(defun proof-span-read-only 140,4966
-(defun proof-strict-read-only 149,5339
-(defsubst proof-set-queue-endpoints 159,5717
-(defun proof-set-overlay-arrow 163,5858
-(defsubst proof-set-locked-endpoints 174,6196
-(defsubst proof-detach-queue 179,6372
-(defsubst proof-detach-locked 184,6511
-(defsubst proof-set-queue-start 191,6736
-(defsubst proof-set-locked-end 195,6862
-(defsubst proof-set-queue-end 207,7332
-(defun proof-init-segmentation 218,7629
-(defun proof-colour-locked 250,9024
-(defun proof-colour-locked-span 257,9297
-(defun proof-sticky-errors 263,9570
-(defun proof-restart-buffers 276,9986
-(defun proof-script-buffers-with-spans 298,10805
-(defun proof-script-remove-all-spans-and-deactivate 308,11161
-(defun proof-script-clear-queue-spans-on-error 312,11351
-(defun proof-script-delete-spans 338,12368
-(defun proof-script-delete-secondary-spans 343,12567
-(defun proof-unprocessed-begin 356,12856
-(defun proof-script-end 364,13110
-(defun proof-queue-or-locked-end 373,13420
-(defun proof-locked-region-full-p 392,14013
-(defun proof-locked-region-empty-p 401,14285
-(defun proof-only-whitespace-to-locked-region-p 405,14435
-(defun proof-in-locked-region-p 415,14784
-(defun proof-goto-end-of-locked 427,15041
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 444,15800
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 456,16314
-(defun proof-end-of-locked-visible-p 469,16898
-(defvar pg-idioms 488,17491
-(defun pg-clear-script-portions 491,17587
-(defun pg-remove-element 497,17822
-(defun pg-get-element 505,18125
-(defun pg-add-element 515,18440
-(defun pg-set-element-span-invisible 563,20419
-(defun pg-open-invisible-span 567,20579
-(defun pg-make-element-invisible 572,20750
-(defun pg-make-element-visible 577,20961
-(defun pg-toggle-element-span-visibility 582,21155
-(defun pg-toggle-element-visibility 588,21318
-(defun pg-show-all-portions 594,21581
-(defun pg-show-all-proofs 613,22289
-(defun pg-hide-all-proofs 618,22417
-(defun pg-add-proof-element 623,22548
-(defun pg-span-name 638,23319
-(defvar pg-span-context-menu-keymap659,24019
-(defun pg-last-output-displayform 666,24257
-(defun pg-set-span-helphighlights 689,25148
-(defun pg-delete-self-modification-hook 738,26962
-(defun proof-complete-buffer-atomic 749,27235
-(defun proof-register-possibly-new-processed-file790,29147
-(defun proof-query-save-this-buffer-p 836,31021
-(defun proof-inform-prover-file-retracted 841,31246
-(defun proof-auto-retract-dependencies 861,32097
-(defun proof-unregister-buffer-file-name 915,34647
-(defun proof-protected-process-or-retract 961,36472
-(defun proof-deactivate-scripting-auto 988,37642
-(defun proof-deactivate-scripting 997,38000
-(defun proof-activate-scripting 1130,43232
-(defun proof-toggle-active-scripting 1230,47747
-(defun proof-done-advancing 1269,48992
-(defun proof-done-advancing-comment 1348,51977
-(defun proof-done-advancing-save 1382,53353
-(defun proof-make-goalsave1470,56717
-(defun proof-get-name-from-goal 1488,57548
-(defun proof-done-advancing-autosave 1508,58573
-(defun proof-done-advancing-other 1573,61117
-(defun proof-segment-up-to-parser 1602,62046
-(defun proof-script-generic-parse-find-comment-end 1671,64312
-(defun proof-script-generic-parse-cmdend 1680,64726
-(defun proof-script-generic-parse-cmdstart 1731,66622
-(defun proof-script-generic-parse-sexp 1770,68222
-(defun proof-semis-to-vanillas 1782,68688
-(defun proof-script-next-command-advance 1835,70361
-(defun proof-assert-until-point 1854,70860
-(defun proof-assert-electric-terminator 1869,71487
-(defun proof-assert-semis 1904,72872
-(defun proof-retract-before-change 1918,73613
-(defun proof-insert-pbp-command 1938,74209
-(defun proof-insert-sendback-command 1953,74709
-(defun proof-done-retracting 1979,75612
-(defun proof-setup-retract-action 2014,77064
-(defun proof-last-goal-or-goalsave 2025,77601
-(defun proof-retract-target 2049,78513
-(defun proof-retract-until-point-interactive 2133,81977
-(defun proof-retract-until-point 2142,82384
-(define-derived-mode proof-mode 2189,84254
-(defun proof-script-set-visited-file-name 2225,85636
-(defun proof-script-set-buffer-hooks 2247,86649
-(defun proof-script-kill-buffer-fn 2255,87067
-(defun proof-config-done-related 2287,88384
-(defun proof-generic-goal-command-p 2352,90869
-(defun proof-generic-state-preserving-p 2357,91082
-(defun proof-generic-count-undos 2366,91599
-(defun proof-generic-find-and-forget 2397,92727
-(defconst proof-script-important-settings2448,94499
-(defun proof-config-done 2463,95045
-(defun proof-setup-parsing-mechanism 2524,97059
-(defun proof-setup-imenu 2548,98131
-(deflocal proof-segment-up-to-cache 2575,98909
-(deflocal proof-segment-up-to-cache-start 2576,98950
-(deflocal proof-last-edited-low-watermark 2577,98995
-(defun proof-segment-up-to-using-cache 2587,99482
-(defun proof-segment-cache-contents-for 2616,100616
-(defun proof-script-after-change-function 2628,100985
-(defun proof-script-set-after-change-functions 2640,101492
-
-generic/proof-shell.el,3597
+(deflocal proof-locked-span 112,3885
+(deflocal proof-queue-span 119,4151
+(deflocal proof-overlay-arrow 128,4637
+(defun proof-span-give-warning 134,4764
+(defun proof-span-read-only 140,4944
+(defun proof-strict-read-only 149,5317
+(defsubst proof-set-queue-endpoints 159,5695
+(defun proof-set-overlay-arrow 163,5836
+(defsubst proof-set-locked-endpoints 174,6174
+(defsubst proof-detach-queue 179,6350
+(defsubst proof-detach-locked 184,6489
+(defsubst proof-set-queue-start 191,6714
+(defsubst proof-set-locked-end 195,6840
+(defsubst proof-set-queue-end 207,7310
+(defun proof-init-segmentation 218,7607
+(defun proof-colour-locked 248,8858
+(defun proof-colour-locked-span 255,9131
+(defun proof-sticky-errors 261,9404
+(defun proof-restart-buffers 274,9820
+(defun proof-script-buffers-with-spans 296,10639
+(defun proof-script-remove-all-spans-and-deactivate 306,10995
+(defun proof-script-clear-queue-spans-on-error 310,11185
+(defun proof-script-delete-spans 336,12202
+(defun proof-script-delete-secondary-spans 341,12401
+(defun proof-unprocessed-begin 354,12690
+(defun proof-script-end 362,12944
+(defun proof-queue-or-locked-end 371,13254
+(defun proof-locked-region-full-p 390,13847
+(defun proof-locked-region-empty-p 399,14119
+(defun proof-only-whitespace-to-locked-region-p 403,14269
+(defun proof-in-locked-region-p 413,14618
+(defun proof-goto-end-of-locked 425,14875
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 442,15634
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 453,16115
+(defun proof-end-of-locked-visible-p 465,16655
+(defconst pg-idioms 484,17248
+(defconst pg-all-idioms 487,17344
+(defun pg-clear-script-portions 491,17465
+(defun pg-remove-element 497,17700
+(defun pg-get-element 505,18003
+(defun pg-add-element 515,18318
+(defun pg-invisible-prop 563,20297
+(defun pg-set-element-span-invisible 568,20498
+(defun pg-toggle-element-span-visibility 581,21064
+(defun pg-open-invisible-span 586,21225
+(defun pg-make-element-invisible 591,21396
+(defun pg-make-element-visible 596,21607
+(defun pg-toggle-element-visibility 601,21801
+(defun pg-show-all-portions 607,22064
+(defun pg-show-all-proofs 626,22772
+(defun pg-hide-all-proofs 631,22900
+(defun pg-add-proof-element 636,23031
+(defun pg-span-name 651,23818
+(defvar pg-span-context-menu-keymap684,25025
+(defun pg-last-output-displayform 691,25263
+(defun pg-set-span-helphighlights 714,26154
+(defun proof-complete-buffer-atomic 772,28131
+(defun proof-register-possibly-new-processed-file801,29401
+(defun proof-query-save-this-buffer-p 847,31275
+(defun proof-inform-prover-file-retracted 852,31500
+(defun proof-auto-retract-dependencies 872,32351
+(defun proof-unregister-buffer-file-name 926,34901
+(defun proof-protected-process-or-retract 972,36726
+(defun proof-deactivate-scripting-auto 999,37896
+(defun proof-deactivate-scripting 1008,38254
+(defun proof-activate-scripting 1138,43398
+(defun proof-toggle-active-scripting 1239,47918
+(defun proof-done-advancing 1278,49163
+(defun proof-done-advancing-comment 1357,52148
+(defun proof-done-advancing-save 1391,53534
+(defun proof-make-goalsave1479,56898
+(defun proof-get-name-from-goal 1497,57763
+(defun proof-done-advancing-autosave 1517,58788
+(defun proof-done-advancing-other 1581,61284
+(defun proof-segment-up-to-parser 1610,62248
+(defun proof-script-generic-parse-find-comment-end 1679,64514
+(defun proof-script-generic-parse-cmdend 1688,64928
+(defun proof-script-generic-parse-cmdstart 1739,66824
+(defun proof-script-generic-parse-sexp 1778,68424
+(defun proof-semis-to-vanillas 1790,68890
+(defun proof-next-command-new-line 1843,70563
+(defun proof-script-next-command-advance 1848,70769
+(defun proof-assert-until-point 1867,71269
+(defun proof-assert-electric-terminator 1882,71896
+(defun proof-assert-semis 1925,73528
+(defun proof-retract-before-change 1939,74269
+(defun proof-insert-pbp-command 1959,74865
+(defun proof-insert-sendback-command 1974,75368
+(defun proof-done-retracting 2000,76271
+(defun proof-setup-retract-action 2035,77725
+(defun proof-last-goal-or-goalsave 2047,78330
+(defun proof-retract-target 2071,79242
+(defun proof-retract-until-point-interactive 2150,82495
+(defun proof-retract-until-point 2159,82902
+(define-derived-mode proof-mode 2214,84910
+(defun proof-script-set-visited-file-name 2250,86292
+(defun proof-script-set-buffer-hooks 2272,87305
+(defun proof-script-kill-buffer-fn 2280,87723
+(defun proof-config-done-related 2312,89040
+(defun proof-generic-goal-command-p 2377,91525
+(defun proof-generic-state-preserving-p 2382,91738
+(defun proof-generic-count-undos 2391,92255
+(defun proof-generic-find-and-forget 2422,93383
+(defconst proof-script-important-settings2473,95155
+(defun proof-config-done 2488,95701
+(defun proof-setup-parsing-mechanism 2555,97866
+(defun proof-setup-imenu 2579,98938
+(deflocal proof-segment-up-to-cache 2606,99716
+(deflocal proof-segment-up-to-cache-start 2607,99757
+(deflocal proof-last-edited-low-watermark 2608,99802
+(defun proof-segment-up-to-using-cache 2618,100289
+(defun proof-segment-cache-contents-for 2650,101534
+(defun proof-script-after-change-function 2662,101903
+(defun proof-script-set-after-change-functions 2674,102410
+
+generic/proof-shell.el,3598
 (defvar proof-marker 34,744
 (defvar proof-action-list 37,840
-(defsubst proof-shell-invoke-callback 56,1512
-(defvar proof-shell-last-goals-output 70,2004
-(defvar proof-shell-last-response-output 73,2084
-(defvar proof-shell-delayed-output-start 76,2171
-(defvar proof-shell-delayed-output-end 80,2353
-(defvar proof-shell-delayed-output-flags 84,2533
-(defvar proof-shell-interrupt-pending 87,2658
-(defcustom proof-shell-active-scripting-indicator98,2953
-(defun proof-shell-ready-prover 144,4312
-(defsubst proof-shell-live-buffer 158,4851
-(defun proof-shell-available-p 165,5090
-(defun proof-grab-lock 171,5312
-(defun proof-release-lock 181,5741
-(defcustom proof-shell-fiddle-frames 191,5915
-(defun proof-shell-set-text-representation 196,6073
-(defun proof-shell-start 204,6401
-(defvar proof-shell-kill-function-hooks 378,12211
-(defun proof-shell-kill-function 381,12309
-(defun proof-shell-clear-state 434,14204
-(defun proof-shell-exit 450,14679
-(defun proof-shell-bail-out 463,15183
-(defun proof-shell-restart 473,15705
-(defvar proof-shell-urgent-message-marker 514,17077
-(defvar proof-shell-urgent-message-scanner 517,17198
-(defun proof-shell-handle-error-output 521,17383
-(defun proof-shell-handle-error-or-interrupt 547,18245
-(defun proof-shell-error-or-interrupt-action 590,19994
-(defun proof-goals-pos 613,20873
-(defun proof-pbp-focus-on-first-goal 618,21084
-(defsubst proof-shell-string-match-safe 630,21500
-(defun proof-shell-handle-immediate-output 634,21661
-(defun proof-interrupt-process 701,24268
-(defun proof-shell-insert 735,25501
-(defun proof-shell-action-list-item 786,27327
-(defun proof-shell-set-silent 791,27569
-(defun proof-shell-start-silent-item 797,27788
-(defun proof-shell-clear-silent 803,27977
-(defun proof-shell-stop-silent-item 809,28199
-(defsubst proof-shell-should-be-silent 815,28388
-(defsubst proof-shell-insert-action-item 826,28898
-(defsubst proof-shell-slurp-comments 830,29073
-(defun proof-add-to-queue 841,29478
-(defun proof-start-queue 899,31502
-(defun proof-extend-queue 910,31896
-(defun proof-shell-exec-loop 924,32364
-(defun proof-shell-insert-loopback-cmd 992,34667
-(defun proof-shell-process-urgent-message 1017,35831
-(defun proof-shell-process-urgent-message-default 1066,37551
-(defun proof-shell-process-urgent-message-trace 1082,38135
-(defun proof-shell-process-urgent-message-retract 1095,38694
-(defun proof-shell-process-urgent-message-elisp 1116,39542
-(defun proof-shell-process-urgent-message-thmdeps 1131,40037
-(defun proof-shell-strip-eager-annotations 1145,40416
-(defun proof-shell-filter 1161,40916
-(defun proof-shell-filter-first-command 1261,44288
-(defun proof-shell-process-urgent-messages 1276,44831
-(defun proof-shell-filter-manage-output 1326,46397
-(defsubst proof-shell-display-output-as-response 1358,47644
-(defun proof-shell-handle-delayed-output 1364,47939
-(defvar pg-last-tracing-output-time 1459,51398
-(defconst pg-slow-mode-duration 1462,51504
-(defconst pg-fast-tracing-mode-threshold 1465,51586
-(defvar pg-tracing-cleanup-timer 1468,51714
-(defun pg-tracing-tight-loop 1470,51753
-(defun pg-finish-tracing-display 1513,53465
-(defun proof-shell-wait 1531,53829
-(defun proof-done-invisible 1561,55034
-(defun proof-shell-invisible-command 1567,55204
-(defun proof-shell-invisible-cmd-get-result 1613,56739
-(defun proof-shell-invisible-command-invisible-result 1625,57175
-(defun pg-insert-last-output-as-comment 1645,57676
-(define-derived-mode proof-shell-mode 1664,58148
-(defconst proof-shell-important-settings1701,59175
-(defun proof-shell-config-done 1707,59290
-
-generic/proof-site.el,503
+(defsubst proof-shell-invoke-callback 57,1594
+(defvar proof-shell-last-goals-output 71,2086
+(defvar proof-shell-last-response-output 74,2166
+(defvar proof-shell-delayed-output-start 77,2253
+(defvar proof-shell-delayed-output-end 81,2435
+(defvar proof-shell-delayed-output-flags 85,2615
+(defvar proof-shell-interrupt-pending 88,2740
+(defcustom proof-shell-active-scripting-indicator99,3035
+(defun proof-shell-ready-prover 151,4619
+(defsubst proof-shell-live-buffer 165,5158
+(defun proof-shell-available-p 172,5397
+(defun proof-grab-lock 178,5619
+(defun proof-release-lock 188,6048
+(defcustom proof-shell-fiddle-frames 198,6222
+(defun proof-shell-set-text-representation 203,6380
+(defun proof-shell-start 211,6708
+(defvar proof-shell-kill-function-hooks 385,12533
+(defun proof-shell-kill-function 388,12631
+(defun proof-shell-clear-state 441,14526
+(defun proof-shell-exit 457,15001
+(defun proof-shell-bail-out 470,15505
+(defun proof-shell-restart 480,16027
+(defvar proof-shell-urgent-message-marker 521,17399
+(defvar proof-shell-urgent-message-scanner 524,17520
+(defun proof-shell-handle-error-output 528,17705
+(defun proof-shell-handle-error-or-interrupt 554,18567
+(defun proof-shell-error-or-interrupt-action 597,20316
+(defun proof-goals-pos 624,21413
+(defun proof-pbp-focus-on-first-goal 629,21624
+(defsubst proof-shell-string-match-safe 641,22040
+(defun proof-shell-handle-immediate-output 645,22201
+(defun proof-interrupt-process 712,24808
+(defun proof-shell-insert 746,26041
+(defun proof-shell-action-list-item 797,27867
+(defun proof-shell-set-silent 802,28109
+(defun proof-shell-start-silent-item 808,28328
+(defun proof-shell-clear-silent 814,28517
+(defun proof-shell-stop-silent-item 820,28739
+(defsubst proof-shell-should-be-silent 826,28928
+(defsubst proof-shell-insert-action-item 837,29438
+(defsubst proof-shell-slurp-comments 841,29613
+(defun proof-add-to-queue 852,30018
+(defun proof-start-queue 910,32042
+(defun proof-extend-queue 921,32436
+(defun proof-shell-exec-loop 935,32904
+(defun proof-shell-insert-loopback-cmd 1003,35207
+(defun proof-shell-process-urgent-message 1028,36371
+(defun proof-shell-process-urgent-message-default 1077,38091
+(defun proof-shell-process-urgent-message-trace 1093,38675
+(defun proof-shell-process-urgent-message-retract 1106,39234
+(defun proof-shell-process-urgent-message-elisp 1127,40082
+(defun proof-shell-process-urgent-message-thmdeps 1142,40577
+(defun proof-shell-strip-eager-annotations 1156,40956
+(defun proof-shell-filter 1172,41456
+(defun proof-shell-filter-first-command 1272,44828
+(defun proof-shell-process-urgent-messages 1287,45371
+(defun proof-shell-filter-manage-output 1337,46937
+(defsubst proof-shell-display-output-as-response 1369,48184
+(defun proof-shell-handle-delayed-output 1375,48479
+(defvar pg-last-tracing-output-time 1470,51938
+(defconst pg-slow-mode-duration 1473,52044
+(defconst pg-fast-tracing-mode-threshold 1476,52126
+(defvar pg-tracing-cleanup-timer 1479,52254
+(defun pg-tracing-tight-loop 1481,52293
+(defun pg-finish-tracing-display 1524,54005
+(defun proof-shell-wait 1542,54369
+(defun proof-done-invisible 1572,55574
+(defun proof-shell-invisible-command 1578,55744
+(defun proof-shell-invisible-cmd-get-result 1625,57336
+(defun proof-shell-invisible-command-invisible-result 1637,57772
+(defun pg-insert-last-output-as-comment 1657,58273
+(define-derived-mode proof-shell-mode 1676,58745
+(defconst proof-shell-important-settings1713,59772
+(defun proof-shell-config-done 1719,59887
+
+generic/proof-site.el,665
 (defconst proof-assistant-table-default26,771
-(defconst proof-general-short-version59,1824
-(defconst proof-general-version-year 65,2011
-(defgroup proof-general 72,2164
-(defgroup proof-general-internals 77,2272
-(defun proof-home-directory-fn 90,2660
-(defcustom proof-home-directory101,3032
-(defcustom proof-images-directory110,3398
-(defcustom proof-info-directory116,3600
-(defcustom proof-assistant-table145,4577
-(defcustom proof-assistants 180,5690
-(defun proof-ready-for-assistant 209,6846
+(defconst proof-general-short-version59,1766
+(defconst proof-general-version-year 65,1953
+(defgroup proof-general 72,2106
+(defgroup proof-general-internals 77,2214
+(defun proof-home-directory-fn 90,2602
+(defcustom proof-home-directory101,2974
+(defcustom proof-images-directory110,3340
+(defcustom proof-info-directory116,3542
+(defcustom proof-assistant-table145,4519
+(defcustom proof-assistants 182,5687
+(defun proof-ready-for-assistant 211,6841
+(defvar proof-general-configured-provers 263,9133
+(defun proof-chose-prover 333,11656
+(defun proofgeneral 338,11788
+(defun proof-visit-example-file 347,12106
 
 generic/proof-splash.el,991
-(defcustom proof-splash-enable 34,1007
-(defcustom proof-splash-time 39,1159
-(defcustom proof-splash-contents47,1443
-(defconst proof-splash-startup-msg91,3008
-(defconst proof-splash-welcome 100,3386
-(define-derived-mode proof-splash-mode 103,3490
-(define-key proof-splash-mode-map 109,3664
-(define-key proof-splash-mode-map 110,3716
-(defsubst proof-emacs-imagep 115,3843
-(defun proof-get-image 120,3968
-(defvar proof-splash-timeout-conf 142,4768
-(defun proof-splash-centre-spaces 145,4881
-(defun proof-splash-remove-screen 170,5966
-(defun proof-splash-remove-buffer 187,6622
-(defvar proof-splash-seen 198,7010
-(defun proof-splash-insert-contents 201,7112
-(defun proof-splash-display-screen 241,8242
-(defalias 'pg-about pg-about
277,9764
-(defun proof-splash-message 280,9830
-(defun proof-splash-timeout-waiter 293,10274
-(defvar proof-splash-old-frame-title-format 306,10832
-(defun proof-splash-set-frame-titles 308,10882
-(defun proof-splash-unset-frame-titles 317,11197
-
-generic/proof-syntax.el,1237
+(defcustom proof-splash-enable 34,1008
+(defcustom proof-splash-time 39,1160
+(defcustom proof-splash-contents47,1444
+(defconst proof-splash-startup-msg91,3009
+(defconst proof-splash-welcome 100,3387
+(define-derived-mode proof-splash-mode 103,3491
+(define-key proof-splash-mode-map 109,3665
+(define-key proof-splash-mode-map 110,3717
+(defsubst proof-emacs-imagep 115,3844
+(defun proof-get-image 120,3969
+(defvar proof-splash-timeout-conf 142,4769
+(defun proof-splash-centre-spaces 145,4882
+(defun proof-splash-remove-screen 172,6038
+(defun proof-splash-remove-buffer 189,6694
+(defvar proof-splash-seen 200,7082
+(defun proof-splash-insert-contents 203,7184
+(defun proof-splash-display-screen 243,8314
+(defalias 'pg-about pg-about
279,9836
+(defun proof-splash-message 282,9902
+(defun proof-splash-timeout-waiter 295,10346
+(defvar proof-splash-old-frame-title-format 308,10904
+(defun proof-splash-set-frame-titles 310,10954
+(defun proof-splash-unset-frame-titles 319,11269
+
+generic/proof-syntax.el,1278
 (defsubst proof-ids-to-regexp 22,517
 (defsubst proof-anchor-regexp 29,755
 (defconst proof-no-regexp 33,860
 (defsubst proof-regexp-alt 36,951
-(defsubst proof-re-search-forward-region 45,1263
-(defsubst proof-search-forward 58,1761
-(defsubst proof-replace-regexp-in-string 65,2031
-(defsubst proof-re-search-forward 70,2282
-(defsubst proof-re-search-backward 75,2540
-(defsubst proof-re-search-forward-safe 80,2801
-(defsubst proof-string-match 86,3082
-(defsubst proof-string-match-safe 91,3311
-(defsubst proof-stringfn-match 95,3515
-(defsubst proof-looking-at 102,3778
-(defsubst proof-looking-at-safe 107,3965
-(defun proof-buffer-syntactic-context 116,4178
-(defsubst proof-looking-at-syntactic-context-default 137,5040
-(defun proof-looking-at-syntactic-context 146,5395
-(defun proof-inside-comment 155,5857
-(defun proof-inside-string 161,6030
-(defsubst proof-replace-string 171,6229
-(defsubst proof-replace-regexp 176,6433
-(defsubst proof-replace-regexp-nocasefold 181,6642
-(defvar proof-id 191,6930
-(defsubst proof-ids 197,7150
-(defun proof-zap-commas 204,7402
-(defadvice font-lock-fontify-keywords-region230,8288
-(defun proof-format 246,8884
-(defun proof-format-filename 265,9523
-(defun proof-insert 312,10925
+(defsubst proof-regexp-alt-list 45,1263
+(defsubst proof-re-search-forward-region 49,1398
+(defsubst proof-search-forward 62,1896
+(defsubst proof-replace-regexp-in-string 69,2166
+(defsubst proof-re-search-forward 74,2417
+(defsubst proof-re-search-backward 79,2675
+(defsubst proof-re-search-forward-safe 84,2936
+(defsubst proof-string-match 90,3217
+(defsubst proof-string-match-safe 95,3446
+(defsubst proof-stringfn-match 99,3650
+(defsubst proof-looking-at 106,3913
+(defsubst proof-looking-at-safe 111,4100
+(defun proof-buffer-syntactic-context 120,4313
+(defsubst proof-looking-at-syntactic-context-default 141,5175
+(defun proof-looking-at-syntactic-context 150,5530
+(defun proof-inside-comment 159,5992
+(defun proof-inside-string 165,6165
+(defsubst proof-replace-string 175,6364
+(defsubst proof-replace-regexp 180,6568
+(defsubst proof-replace-regexp-nocasefold 185,6777
+(defvar proof-id 195,7065
+(defsubst proof-ids 201,7285
+(defun proof-zap-commas 208,7537
+(defadvice font-lock-fontify-keywords-region234,8423
+(defun proof-format 250,9019
+(defun proof-format-filename 269,9658
+(defun proof-insert 316,11060
 
 generic/proof-toolbar.el,2332
-(defun proof-toolbar-function 33,810
-(defun proof-toolbar-icon 37,957
-(defun proof-toolbar-enabler 41,1104
-(defun proof-toolbar-make-icon 50,1306
-(defun proof-toolbar-make-toolbar-items 59,1614
-(defvar proof-toolbar-map 84,2419
-(defun proof-toolbar-available-p 87,2518
-(defun proof-toolbar-setup 97,2824
-(defun proof-toolbar-enable 118,3681
-(defalias 'proof-toolbar-undo proof-toolbar-undo
151,4739
-(defun proof-toolbar-undo-enable-p 153,4807
-(defalias 'proof-toolbar-delete proof-toolbar-delete
160,4965
-(defun proof-toolbar-delete-enable-p 162,5046
-(defalias 'proof-toolbar-home proof-toolbar-home
170,5228
-(defalias 'proof-toolbar-next proof-toolbar-next
174,5295
-(defun proof-toolbar-next-enable-p 176,5366
-(defalias 'proof-toolbar-goto proof-toolbar-goto
182,5482
-(defun proof-toolbar-goto-enable-p 184,5532
-(defalias 'proof-toolbar-retract proof-toolbar-retract
189,5617
-(defun proof-toolbar-retract-enable-p 191,5674
-(defalias 'proof-toolbar-use proof-toolbar-use
197,5793
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
198,5845
-(defalias 'proof-toolbar-restart proof-toolbar-restart
202,5926
-(defalias 'proof-toolbar-goal proof-toolbar-goal
206,5991
-(defalias 'proof-toolbar-qed proof-toolbar-qed
210,6049
-(defun proof-toolbar-qed-enable-p 212,6098
-(defalias 'proof-toolbar-state proof-toolbar-state
220,6260
-(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
221,6303
-(defalias 'proof-toolbar-context proof-toolbar-context
225,6382
-(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
226,6428
-(defalias 'proof-toolbar-command proof-toolbar-command
230,6509
-(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
231,6565
-(defun proof-toolbar-help 235,6670
-(defalias 'proof-toolbar-find proof-toolbar-find
241,6750
-(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
242,6802
-(defalias 'proof-toolbar-info proof-toolbar-info
246,6877
-(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
247,6932
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
251,7030
-(defun proof-toolbar-visibility-enable-p 253,7090
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
258,7204
-(defun proof-toolbar-interrupt-enable-p 259,7265
-(defun proof-toolbar-scripting-menu 267,7418
+(defun proof-toolbar-function 33,813
+(defun proof-toolbar-icon 37,960
+(defun proof-toolbar-enabler 41,1107
+(defun proof-toolbar-make-icon 50,1309
+(defun proof-toolbar-make-toolbar-items 59,1617
+(defvar proof-toolbar-map 85,2493
+(defun proof-toolbar-available-p 88,2592
+(defun proof-toolbar-setup 98,2898
+(defun proof-toolbar-enable 119,3755
+(defalias 'proof-toolbar-undo proof-toolbar-undo
152,4813
+(defun proof-toolbar-undo-enable-p 154,4881
+(defalias 'proof-toolbar-delete proof-toolbar-delete
161,5039
+(defun proof-toolbar-delete-enable-p 163,5120
+(defalias 'proof-toolbar-home proof-toolbar-home
171,5302
+(defalias 'proof-toolbar-next proof-toolbar-next
175,5369
+(defun proof-toolbar-next-enable-p 177,5440
+(defalias 'proof-toolbar-goto proof-toolbar-goto
183,5556
+(defun proof-toolbar-goto-enable-p 185,5606
+(defalias 'proof-toolbar-retract proof-toolbar-retract
190,5691
+(defun proof-toolbar-retract-enable-p 192,5748
+(defalias 'proof-toolbar-use proof-toolbar-use
198,5867
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
199,5919
+(defalias 'proof-toolbar-restart proof-toolbar-restart
203,6000
+(defalias 'proof-toolbar-goal proof-toolbar-goal
207,6065
+(defalias 'proof-toolbar-qed proof-toolbar-qed
211,6123
+(defun proof-toolbar-qed-enable-p 213,6172
+(defalias 'proof-toolbar-state proof-toolbar-state
221,6334
+(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
222,6377
+(defalias 'proof-toolbar-context proof-toolbar-context
226,6456
+(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
227,6502
+(defalias 'proof-toolbar-command proof-toolbar-command
231,6583
+(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
232,6639
+(defun proof-toolbar-help 236,6744
+(defalias 'proof-toolbar-find proof-toolbar-find
242,6824
+(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
243,6876
+(defalias 'proof-toolbar-info proof-toolbar-info
247,6951
+(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
248,7006
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
252,7104
+(defun proof-toolbar-visibility-enable-p 254,7164
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
259,7278
+(defun proof-toolbar-interrupt-enable-p 260,7339
+(defun proof-toolbar-scripting-menu 268,7492
 
 generic/proof-unicode-tokens.el,497
 (defvar proof-unicode-tokens-initialised 31,827
@@ -1815,7 +1842,7 @@ generic/proof-unicode-tokens.el,497
 (defun proof-unicode-tokens-activate-prover 133,4573
 (defun proof-unicode-tokens-deactivate-prover 140,4819
 
-generic/proof-useropts.el,1676
+generic/proof-useropts.el,1575
 (defgroup proof-user-options 21,559
 (defun proof-set-value 29,738
 (defcustom proof-electric-terminator-enable 62,1861
@@ -1834,66 +1861,64 @@ generic/proof-useropts.el,1676
 (defcustom proof-colour-locked 187,6947
 (defcustom proof-sticky-errors 195,7197
 (defcustom proof-query-file-save-when-activating-scripting202,7414
-(defcustom proof-one-command-per-line218,8134
-(defcustom proof-prog-name-ask225,8358
-(defcustom proof-prog-name-guess231,8518
-(defcustom proof-tidy-response239,8783
-(defcustom proof-keep-response-history253,9246
-(defcustom pg-input-ring-size 263,9634
-(defcustom proof-general-debug 268,9786
-(defcustom proof-use-parser-cache 277,10157
-(defcustom proof-follow-mode 284,10413
-(defcustom proof-auto-action-when-deactivating-scripting 308,11590
-(defcustom proof-script-command-separator 331,12539
-(defcustom proof-rsh-command 339,12831
-(defcustom proof-disappearing-proofs 355,13381
-(defcustom proof-full-annotation 360,13542
-(defcustom proof-minibuffer-messages 369,13912
-(defcustom proof-autosend-enable 377,14221
-(defcustom proof-autosend-delay 383,14401
-(defcustom proof-autosend-all 389,14559
-(defcustom proof-fast-process-buffer 394,14728
+(defcustom proof-prog-name-ask218,8134
+(defcustom proof-prog-name-guess224,8294
+(defcustom proof-tidy-response232,8559
+(defcustom proof-keep-response-history246,9022
+(defcustom pg-input-ring-size 256,9410
+(defcustom proof-general-debug 261,9562
+(defcustom proof-use-parser-cache 270,9933
+(defcustom proof-follow-mode 277,10189
+(defcustom proof-auto-action-when-deactivating-scripting 301,11366
+(defcustom proof-rsh-command 324,12315
+(defcustom proof-disappearing-proofs 340,12865
+(defcustom proof-full-annotation 345,13026
+(defcustom proof-minibuffer-messages 354,13396
+(defcustom proof-autosend-enable 362,13705
+(defcustom proof-autosend-delay 368,13885
+(defcustom proof-autosend-all 374,14043
+(defcustom proof-fast-process-buffer 379,14212
 
 generic/proof-utils.el,1567
-(defmacro proof-with-current-buffer-if-exists 61,1732
-(defmacro proof-with-script-buffer 70,2109
-(defmacro proof-map-buffers 81,2490
-(defmacro proof-sym 86,2675
-(defsubst proof-try-require 91,2836
-(defun proof-save-some-buffers 104,3167
-(defun proof-save-this-buffer 124,3763
-(defun proof-file-truename 137,4127
-(defun proof-files-to-buffers 141,4309
-(defun proof-buffers-in-mode 149,4548
-(defun pg-save-from-death 163,4998
-(defun proof-define-keys 182,5614
-(defun pg-remove-specials 193,5899
-(defun pg-remove-specials-in-string 203,6235
-(defun proof-safe-split-window-vertically 213,6460
-(defun proof-warn-if-unset 219,6658
-(defun proof-get-window-for-buffer 224,6876
-(defun proof-display-and-keep-buffer 275,9195
-(defun proof-clean-buffer 317,10918
-(defun pg-internal-warning 333,11574
-(defun proof-debug 341,11856
-(defun proof-switch-to-buffer 351,12227
-(defun proof-resize-window-tofit 373,13351
-(defun proof-submit-bug-report 468,17199
-(defun proof-deftoggle-fn 503,18556
-(defmacro proof-deftoggle 518,19219
-(defun proof-defintset-fn 525,19595
-(defmacro proof-defintset 541,20299
-(defun proof-defstringset-fn 548,20678
-(defmacro proof-defstringset 561,21304
-(defun proof-escape-keymap-doc 574,21760
-(defmacro proof-defshortcut 578,21914
-(defmacro proof-definvisible 593,22512
-(defun pg-custom-save-vars 620,23441
-(defun pg-custom-reset-vars 636,24085
-(defun proof-locate-executable 649,24422
-(defun pg-current-word-pos 664,24977
-(defsubst proof-shell-strip-output-markup 709,26632
-(defun proof-minibuffer-message 715,26896
+(defmacro proof-with-current-buffer-if-exists 61,1730
+(defmacro proof-with-script-buffer 70,2107
+(defmacro proof-map-buffers 81,2488
+(defmacro proof-sym 86,2673
+(defsubst proof-try-require 91,2834
+(defun proof-save-some-buffers 104,3165
+(defun proof-save-this-buffer 124,3761
+(defun proof-file-truename 137,4125
+(defun proof-files-to-buffers 141,4307
+(defun proof-buffers-in-mode 149,4546
+(defun pg-save-from-death 163,4996
+(defun proof-define-keys 182,5612
+(defun pg-remove-specials 193,5897
+(defun pg-remove-specials-in-string 203,6233
+(defun proof-safe-split-window-vertically 213,6458
+(defun proof-warn-if-unset 219,6656
+(defun proof-get-window-for-buffer 224,6874
+(defun proof-display-and-keep-buffer 273,9184
+(defun proof-clean-buffer 315,10907
+(defun pg-internal-warning 331,11563
+(defun proof-debug 339,11845
+(defun proof-switch-to-buffer 349,12216
+(defun proof-resize-window-tofit 371,13340
+(defun proof-submit-bug-report 466,17188
+(defun proof-deftoggle-fn 501,18545
+(defmacro proof-deftoggle 516,19211
+(defun proof-defintset-fn 527,19724
+(defmacro proof-defintset 543,20428
+(defun proof-defstringset-fn 550,20807
+(defmacro proof-defstringset 563,21433
+(defun proof-escape-keymap-doc 576,21889
+(defmacro proof-defshortcut 580,22043
+(defmacro proof-definvisible 595,22641
+(defun pg-custom-save-vars 622,23570
+(defun pg-custom-reset-vars 638,24214
+(defun proof-locate-executable 651,24551
+(defun pg-current-word-pos 666,25101
+(defsubst proof-shell-strip-output-markup 711,26756
+(defun proof-minibuffer-message 717,27020
 
 lib/bufhist.el,1257
 (defun bufhist-ring-update 38,1391
@@ -2011,11 +2036,11 @@ lib/maths-menu.el,242
 
 lib/pg-dev.el,199
 (defconst pg-dev-lisp-font-lock-keywords52,1588
-(defun pg-loadpath 80,2422
-(defun unload-pg 90,2593
-(defun profile-pg 121,3487
-(defun elp-pack-number 150,4514
-(defun pg-bug-references 159,4714
+(defun pg-loadpath 78,2287
+(defun unload-pg 88,2458
+(defun profile-pg 119,3352
+(defun elp-pack-number 148,4379
+(defun pg-bug-references 157,4579
 
 lib/pg-fontsets.el,209
 (defcustom pg-fontsets-default-fontset 24,722
@@ -2054,7 +2079,7 @@ lib/scomint.el,876
 (defun scomint-output-filter 291,11525
 (defun scomint-interrupt-process 363,14257
 
-lib/span.el,1406
+lib/span.el,1510
 (defalias 'span-start span-start
22,610
 (defalias 'span-end span-end
23,648
 (defalias 'span-set-property span-set-property
24,682
@@ -2092,7 +2117,9 @@ lib/span.el,1406
 (defsubst span-property-safe 206,6951
 (defsubst span-set-start 210,7088
 (defsubst span-set-end 214,7220
-(defun span-add-self-removing-span 222,7380
+(defun span-make-self-removing-span 222,7380
+(defun span-delete-self-modification-hook 232,7748
+(defun span-make-modifying-removing-span 237,7922
 
 lib/texi-docstring-magic.el,584
 (defun texi-docstring-magic-find-face 88,3027
@@ -2205,28 +2232,28 @@ lib/unicode-tokens.el,5900
 (defvar unicode-tokens-mode-map 1073,38906
 (defvar unicode-tokens-display-table1076,39003
 (define-minor-mode unicode-tokens-mode1083,39254
-(defun unicode-tokens-set-font-var 1216,43737
-(defun unicode-tokens-set-font-var-aux 1232,44226
-(defun unicode-tokens-mouse-set-font 1263,45387
-(defsubst unicode-tokens-face-font-sym 1276,45901
-(defun unicode-tokens-set-font-restart 1280,46081
-(defun unicode-tokens-save-fonts 1291,46391
-(defun unicode-tokens-custom-save-faces 1299,46647
-(define-key unicode-tokens-mode-map1316,47103
-(define-key unicode-tokens-mode-map1319,47210
-(defvar unicode-tokens-quail-translation-keymap1323,47300
-(define-key unicode-tokens-quail-translation-keymap1330,47490
-(defun unicode-tokens-quail-delete-last-char 1334,47624
-(define-key unicode-tokens-mode-map 1349,48051
-(define-key unicode-tokens-mode-map 1351,48143
-(define-key unicode-tokens-mode-map1353,48234
-(define-key unicode-tokens-mode-map1355,48340
-(define-key unicode-tokens-mode-map1358,48455
-(define-key unicode-tokens-mode-map1360,48564
-(define-key unicode-tokens-mode-map1362,48672
-(define-key unicode-tokens-mode-map1364,48778
-(defun unicode-tokens-customize-submenu 1372,48902
-(defun unicode-tokens-define-menu 1379,49125
+(defun unicode-tokens-set-font-var 1219,43807
+(defun unicode-tokens-set-font-var-aux 1235,44296
+(defun unicode-tokens-mouse-set-font 1266,45457
+(defsubst unicode-tokens-face-font-sym 1279,45971
+(defun unicode-tokens-set-font-restart 1283,46151
+(defun unicode-tokens-save-fonts 1294,46461
+(defun unicode-tokens-custom-save-faces 1302,46717
+(define-key unicode-tokens-mode-map1319,47173
+(define-key unicode-tokens-mode-map1322,47280
+(defvar unicode-tokens-quail-translation-keymap1326,47370
+(define-key unicode-tokens-quail-translation-keymap1333,47560
+(defun unicode-tokens-quail-delete-last-char 1337,47694
+(define-key unicode-tokens-mode-map 1352,48121
+(define-key unicode-tokens-mode-map 1354,48213
+(define-key unicode-tokens-mode-map1356,48304
+(define-key unicode-tokens-mode-map1358,48410
+(define-key unicode-tokens-mode-map1361,48525
+(define-key unicode-tokens-mode-map1363,48634
+(define-key unicode-tokens-mode-map1365,48742
+(define-key unicode-tokens-mode-map1367,48848
+(defun unicode-tokens-customize-submenu 1375,48972
+(defun unicode-tokens-define-menu 1382,49195
 
 contrib/mmm/mmm-auto.el,343
 (defvar mmm-autoloaded-classes67,2675
@@ -2472,169 +2499,168 @@ contrib/mmm/mmm-vars.el,2668
 (defun mmm-mode-ext-applies 1028,37844
 (defun mmm-get-all-classes 1042,38223
 
-doc/ProofGeneral.texi,6304
-@node Top161,4909
-@node Preface199,6063
-@node News for Version 4.0News for Version 4.0
222,6652
-@node Future243,7447
-@node Credits272,8782
-@node Introducing Proof GeneralIntroducing Proof General
391,12966
-@node Installing Proof GeneralInstalling Proof General
446,14940
-@node Quick start guideQuick start guide
460,15389
-@node Features of Proof GeneralFeatures of Proof General
504,17510
-@node Supported proof assistantsSupported proof assistants
593,21447
-@node Prerequisites for this manualPrerequisites for this manual
642,23338
-@node Organization of this manualOrganization of this manual
686,24957
-@node Basic Script ManagementBasic Script Management
712,25785
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
731,26385
-@node Proof scriptsProof scripts
997,36637
-@node Script buffersScript buffers
1040,38757
-@node Locked queue and editing regionsLocked queue and editing regions
1062,39334
-@node Goal-save sequencesGoal-save sequences
1118,41481
-@node Active scripting bufferActive scripting buffer
1155,42947
-@node Summary of Proof General buffersSummary of Proof General buffers
1224,46367
-@node Script editing commandsScript editing commands
1273,48624
-@node Script processing commandsScript processing commands
1353,51583
-@node Proof assistant commandsProof assistant commands
1480,56886
-@node Toolbar commandsToolbar commands
1655,63075
-@node Interrupting during trace outputInterrupting during trace output
1679,64004
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1719,65934
-@node Document centred workingDocument centred working
1740,66555
-@node Automatic processingAutomatic processing
1809,69148
-@node Visibility of completed proofsVisibility of completed proofs
1838,70157
-@node Switching between proof scriptsSwitching between proof scripts
1893,72086
-@node View of processed files View of processed files 
1930,74058
-@node Retracting across filesRetracting across files
1990,77109
-@node Asserting across filesAsserting across files
2003,77740
-@node Automatic multiple file handlingAutomatic multiple file handling
2016,78306
-@node Escaping script managementEscaping script management
2041,79340
-@node Editing featuresEditing features
2098,81452
-@node Unicode symbols and special layout supportUnicode symbols and special layout support
2168,84231
-@node Maths menuMaths menu
2210,85789
-@node Unicode Tokens modeUnicode Tokens mode
2227,86480
-@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2277,88903
-@node Special layout Special layout 
2307,89864
-@node Moving between Unicode and tokensMoving between Unicode and tokens
2415,93980
-@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2470,96091
-@node Selecting suitable fontsSelecting suitable fonts
2509,97265
-@node Support for other PackagesSupport for other Packages
2574,100253
-@node Syntax highlightingSyntax highlighting
2604,101089
-@node Imenu and SpeedbarImenu and Speedbar
2632,102092
-@node Support for outline modeSupport for outline mode
2678,103748
-@node Support for completionSupport for completion
2703,104877
-@node Support for tagsSupport for tags
2760,107039
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2812,109387
-@node Goals buffer commandsGoals buffer commands
2827,109899
-@node Customizing Proof GeneralCustomizing Proof General
2915,113434
-@node Basic optionsBasic options
2955,115104
-@node How to customizeHow to customize
2979,115874
-@node Display customizationDisplay customization
3026,117841
-@node User optionsUser options
3180,124246
-@node Changing facesChanging faces
3411,132432
-@node Script buffer facesScript buffer faces
3433,133307
-@node Goals and response facesGoals and response faces
3479,134907
-@node Tweaking configuration settingsTweaking configuration settings
3524,136439
-@node Hints and TipsHints and Tips
3581,138965
-@node Adding your own keybindingsAdding your own keybindings
3600,139566
-@node Using file variablesUsing file variables
3664,142180
-@node Using abbreviationsUsing abbreviations
3723,144366
-@node LEGO Proof GeneralLEGO Proof General
3762,145781
-@node LEGO specific commandsLEGO specific commands
3803,147150
-@node LEGO tagsLEGO tags
3823,147605
-@node LEGO customizationsLEGO customizations
3833,147852
-@node Coq Proof GeneralCoq Proof General
3865,148771
-@node Coq-specific commandsCoq-specific commands
3881,149180
-@node Coq-specific variablesCoq-specific variables
3903,149687
-@node Editing multiple proofsEditing multiple proofs
3925,150345
-@node User-loaded tacticsUser-loaded tactics
3949,151453
-@node Holes featureHoles feature
4013,153927
-@node Isabelle Proof GeneralIsabelle Proof General
4040,155214
-@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4066,156090
-@node Isabelle commandsIsabelle commands
4135,158886
-@node Isabelle settingsIsabelle settings
4278,163078
-@node Isabelle customizationsIsabelle customizations
4292,163660
-@node HOL Proof GeneralHOL Proof General
4315,164147
-@node Shell Proof GeneralShell Proof General
4357,165969
-@node Obtaining and InstallingObtaining and Installing
4393,167428
-@node Obtaining Proof GeneralObtaining Proof General
4408,167793
-@node Installing Proof General from tarballInstalling Proof General from tarball
4434,168675
-@node Setting the names of binariesSetting the names of binaries
4458,169465
-@node Notes for syssiesNotes for syssies
4486,170405
-@node Bugs and EnhancementsBugs and Enhancements
4562,173402
-@node References4583,174217
-@node History of Proof GeneralHistory of Proof General
4623,175240
-@node Old News for 3.0Old News for 3.0
4717,179405
-@node Old News for 3.1Old News for 3.1
4787,183099
-@node Old News for 3.2Old News for 3.2
4813,184271
-@node Old News for 3.3Old News for 3.3
4874,187274
-@node Old News for 3.4Old News for 3.4
4893,188171
-@node Old News for 3.5Old News for 3.5
4915,189226
-@node Old News for 3.6Old News for 3.6
4919,189283
-@node Old News for 3.7Old News for 3.7
4924,189383
-@node Function IndexFunction Index
4968,191306
-@node Variable IndexVariable Index
4972,191382
-@node Keystroke IndexKeystroke Index
4976,191462
-@node Concept IndexConcept Index
4980,191528
+doc/ProofGeneral.texi,6240
+@node Top161,4917
+@node Preface199,6071
+@node News for Version 4.0News for Version 4.0
222,6660
+@node Future243,7504
+@node Credits272,8839
+@node Introducing Proof GeneralIntroducing Proof General
392,13042
+@node Installing Proof GeneralInstalling Proof General
447,15016
+@node Quick start guideQuick start guide
461,15465
+@node Features of Proof GeneralFeatures of Proof General
505,17586
+@node Supported proof assistantsSupported proof assistants
594,21523
+@node Prerequisites for this manualPrerequisites for this manual
643,23404
+@node Organization of this manualOrganization of this manual
687,25023
+@node Basic Script ManagementBasic Script Management
713,25851
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
732,26451
+@node Proof scriptsProof scripts
995,36579
+@node Script buffersScript buffers
1038,38699
+@node Locked queue and editing regionsLocked queue and editing regions
1060,39276
+@node Goal-save sequencesGoal-save sequences
1116,41423
+@node Active scripting bufferActive scripting buffer
1153,42889
+@node Summary of Proof General buffersSummary of Proof General buffers
1222,46309
+@node Script editing commandsScript editing commands
1271,48566
+@node Script processing commandsScript processing commands
1351,51525
+@node Proof assistant commandsProof assistant commands
1477,56770
+@node Toolbar commandsToolbar commands
1660,63241
+@node Interrupting during trace outputInterrupting during trace output
1685,64200
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1725,66130
+@node Document centred workingDocument centred working
1746,66751
+@node Automatic processingAutomatic processing
1825,69809
+@node Visibility of completed proofsVisibility of completed proofs
1880,71832
+@node Switching between proof scriptsSwitching between proof scripts
1935,73772
+@node View of processed files View of processed files 
1972,75744
+@node Retracting across filesRetracting across files
2032,78795
+@node Asserting across filesAsserting across files
2045,79426
+@node Automatic multiple file handlingAutomatic multiple file handling
2058,79992
+@node Escaping script managementEscaping script management
2083,81026
+@node Editing featuresEditing features
2140,83138
+@node Unicode symbols and special layout supportUnicode symbols and special layout support
2210,85917
+@node Maths menuMaths menu
2252,87475
+@node Unicode Tokens modeUnicode Tokens mode
2269,88166
+@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2319,90589
+@node Special layout Special layout 
2349,91550
+@node Moving between Unicode and tokensMoving between Unicode and tokens
2457,95666
+@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2512,97777
+@node Selecting suitable fontsSelecting suitable fonts
2551,98951
+@node Support for other PackagesSupport for other Packages
2616,101939
+@node Syntax highlightingSyntax highlighting
2646,102775
+@node Imenu and SpeedbarImenu and Speedbar
2674,103778
+@node Support for outline modeSupport for outline mode
2720,105449
+@node Support for completionSupport for completion
2745,106578
+@node Support for tagsSupport for tags
2802,108740
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2854,111088
+@node Goals buffer commandsGoals buffer commands
2870,111683
+@node Customizing Proof GeneralCustomizing Proof General
2969,115836
+@node Basic optionsBasic options
3009,117506
+@node How to customizeHow to customize
3033,118276
+@node Display customizationDisplay customization
3080,120243
+@node User optionsUser options
3234,126648
+@node Changing facesChanging faces
3454,134430
+@node Script buffer facesScript buffer faces
3476,135305
+@node Goals and response facesGoals and response faces
3522,136905
+@node Tweaking configuration settingsTweaking configuration settings
3567,138437
+@node Hints and TipsHints and Tips
3624,140963
+@node Adding your own keybindingsAdding your own keybindings
3643,141564
+@node Using file variablesUsing file variables
3707,144178
+@node Using abbreviationsUsing abbreviations
3766,146364
+@node LEGO Proof GeneralLEGO Proof General
3805,147779
+@node LEGO specific commandsLEGO specific commands
3846,149148
+@node LEGO tagsLEGO tags
3866,149603
+@node LEGO customizationsLEGO customizations
3876,149850
+@node Coq Proof GeneralCoq Proof General
3908,150769
+@node Coq-specific commandsCoq-specific commands
3922,151080
+@node Editing multiple proofsEditing multiple proofs
3945,151588
+@node User-loaded tacticsUser-loaded tactics
3969,152696
+@node Holes featureHoles feature
4033,155170
+@node Isabelle Proof GeneralIsabelle Proof General
4062,156500
+@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4088,157376
+@node Isabelle commandsIsabelle commands
4157,160177
+@node Isabelle settingsIsabelle settings
4300,164369
+@node Isabelle customizationsIsabelle customizations
4314,164951
+@node HOL Proof GeneralHOL Proof General
4337,165438
+@node Shell Proof GeneralShell Proof General
4379,167260
+@node Obtaining and InstallingObtaining and Installing
4415,168719
+@node Obtaining Proof GeneralObtaining Proof General
4430,169084
+@node Installing Proof General from tarballInstalling Proof General from tarball
4456,169966
+@node Setting the names of binariesSetting the names of binaries
4480,170756
+@node Notes for syssiesNotes for syssies
4508,171696
+@node Bugs and EnhancementsBugs and Enhancements
4584,174693
+@node References4605,175508
+@node History of Proof GeneralHistory of Proof General
4645,176531
+@node Old News for 3.0Old News for 3.0
4739,180696
+@node Old News for 3.1Old News for 3.1
4809,184390
+@node Old News for 3.2Old News for 3.2
4835,185562
+@node Old News for 3.3Old News for 3.3
4896,188565
+@node Old News for 3.4Old News for 3.4
4915,189462
+@node Old News for 3.5Old News for 3.5
4937,190517
+@node Old News for 3.6Old News for 3.6
4941,190574
+@node Old News for 3.7Old News for 3.7
4946,190674
+@node Function IndexFunction Index
4976,192128
+@node Variable IndexVariable Index
4980,192204
+@node Keystroke IndexKeystroke Index
4984,192284
+@node Concept IndexConcept Index
4988,192350
 
 doc/PG-adapting.texi,3770
-@node Top153,4679
-@node Introduction190,5788
-@node Future231,7441
-@node Credits267,9037
-@node Beginning with a New ProverBeginning with a New Prover
277,9329
-@node Overview of adding a new proverOverview of adding a new prover
317,11271
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration
394,14580
-@node Major modes used by Proof GeneralMajor modes used by Proof General
463,17971
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
506,19681
-@node Settings for generic user-level commandsSettings for generic user-level commands
521,20227
-@node Menu configurationMenu configuration
566,21959
-@node Toolbar configurationToolbar configuration
590,22876
-@node Proof Script SettingsProof Script Settings
649,25113
-@node Recognizing commands and commentsRecognizing commands and comments
671,25693
-@node Recognizing proofsRecognizing proofs
808,32146
-@node Recognizing other elementsRecognizing other elements
912,36450
-@node Configuring undo behaviourConfiguring undo behaviour
975,38929
-@node Nested proofsNested proofs
1112,44316
-@node Safe (state-preserving) commandsSafe (state-preserving) commands
1152,45942
-@node Activate scripting hookActivate scripting hook
1175,46895
-@node Automatic multiple filesAutomatic multiple files
1199,47765
-@node Completions1221,48612
-@node Proof Shell SettingsProof Shell Settings
1262,50102
-@node Proof shell commandsProof shell commands
1293,51384
-@node Script input to the shellScript input to the shell
1457,58432
-@node Settings for matching various output from proof processSettings for matching various output from proof process
1525,61502
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1647,66856
-@node Hooks and other settingsHooks and other settings
1887,77610
-@node Goals Buffer SettingsGoals Buffer Settings
1966,80754
-@node Splash Screen SettingsSplash Screen Settings
2040,83744
-@node Global ConstantsGlobal Constants
2066,84499
-@node Handling Multiple FilesHandling Multiple Files
2092,85328
-@node Configuring Editing SyntaxConfiguring Editing Syntax
2244,93132
-@node Configuring Font LockConfiguring Font Lock
2301,95249
-@node Configuring TokensConfiguring Tokens
2377,98956
-@node Writing More Lisp CodeWriting More Lisp Code
2427,101076
-@node Default values for generic settingsDefault values for generic settings
2444,101721
-@node Adding prover-specific configurationsAdding prover-specific configurations
2474,102804
-@node Useful variablesUseful variables
2517,104086
-@node Useful functions and macrosUseful functions and macros
2532,104585
-@node Internals of Proof GeneralInternals of Proof General
2641,108820
-@node Spans2671,109750
-@node Proof General site configurationProof General site configuration
2686,110123
-@node Configuration variable mechanismsConfiguration variable mechanisms
2769,113222
-@node Global variablesGlobal variables
2895,118670
-@node Proof script modeProof script mode
2970,121294
-@node Proof shell modeProof shell mode
3201,131734
-@node Debugging3714,152272
-@node Plans and IdeasPlans and Ideas
3757,153148
-@node Proof by pointing and similar featuresProof by pointing and similar features
3778,153870
-@node Granularity of atomic command sequencesGranularity of atomic command sequences
3816,155528
-@node Browser mode for script files and theoriesBrowser mode for script files and theories
3861,157753
-@node Demonstration InstantiationsDemonstration Instantiations
3891,158784
-@node demoisa-easy.el3907,159215
-@node demoisa.el3969,161407
-@node Function IndexFunction Index
4123,166327
-@node Variable IndexVariable Index
4127,166403
-@node Concept IndexConcept Index
4136,166582
+@node Top153,4678
+@node Introduction190,5787
+@node Future231,7440
+@node Credits267,9036
+@node Beginning with a New ProverBeginning with a New Prover
277,9328
+@node Overview of adding a new proverOverview of adding a new prover
317,11270
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration
396,14573
+@node Major modes used by Proof GeneralMajor modes used by Proof General
465,17964
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
508,19674
+@node Settings for generic user-level commandsSettings for generic user-level commands
523,20220
+@node Menu configurationMenu configuration
568,21952
+@node Toolbar configurationToolbar configuration
592,22869
+@node Proof Script SettingsProof Script Settings
651,25106
+@node Recognizing commands and commentsRecognizing commands and comments
673,25686
+@node Recognizing proofsRecognizing proofs
810,32139
+@node Recognizing other elementsRecognizing other elements
914,36443
+@node Configuring undo behaviourConfiguring undo behaviour
977,38922
+@node Nested proofsNested proofs
1114,44309
+@node Safe (state-preserving) commandsSafe (state-preserving) commands
1154,45935
+@node Activate scripting hookActivate scripting hook
1177,46888
+@node Automatic multiple filesAutomatic multiple files
1201,47758
+@node Completions1223,48605
+@node Proof Shell SettingsProof Shell Settings
1264,50095
+@node Proof shell commandsProof shell commands
1295,51377
+@node Script input to the shellScript input to the shell
1459,58428
+@node Settings for matching various output from proof processSettings for matching various output from proof process
1527,61498
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1649,66852
+@node Hooks and other settingsHooks and other settings
1889,77606
+@node Goals Buffer SettingsGoals Buffer Settings
1968,80750
+@node Splash Screen SettingsSplash Screen Settings
2042,83740
+@node Global ConstantsGlobal Constants
2068,84495
+@node Handling Multiple FilesHandling Multiple Files
2094,85324
+@node Configuring Editing SyntaxConfiguring Editing Syntax
2246,93128
+@node Configuring Font LockConfiguring Font Lock
2303,95245
+@node Configuring TokensConfiguring Tokens
2379,98957
+@node Writing More Lisp CodeWriting More Lisp Code
2429,101077
+@node Default values for generic settingsDefault values for generic settings
2446,101722
+@node Adding prover-specific configurationsAdding prover-specific configurations
2476,102805
+@node Useful variablesUseful variables
2519,104087
+@node Useful functions and macrosUseful functions and macros
2534,104586
+@node Internals of Proof GeneralInternals of Proof General
2644,108898
+@node Spans2674,109828
+@node Proof General site configurationProof General site configuration
2689,110201
+@node Configuration variable mechanismsConfiguration variable mechanisms
2772,113282
+@node Global variablesGlobal variables
2898,118763
+@node Proof script modeProof script mode
2973,121387
+@node Proof shell modeProof shell mode
3223,132713
+@node Debugging3737,153362
+@node Plans and IdeasPlans and Ideas
3780,154238
+@node Proof by pointing and similar featuresProof by pointing and similar features
3801,154960
+@node Granularity of atomic command sequencesGranularity of atomic command sequences
3839,156618
+@node Browser mode for script files and theoriesBrowser mode for script files and theories
3884,158843
+@node Demonstration InstantiationsDemonstration Instantiations
3914,159874
+@node demoisa-easy.el3930,160305
+@node demoisa.el3992,162497
+@node Function IndexFunction Index
4146,167417
+@node Variable IndexVariable Index
4150,167493
+@node Concept IndexConcept Index
4159,167672
 
 generic/proof.el,0
 
diff --git a/etc/README b/etc/README
index 6b622f9b..dc5d7f9e 100644
--- a/etc/README
+++ b/etc/README
@@ -1,9 +1,9 @@
-Files in the PG/etc directory  (NB: some only in devel distrib)
-===============================================================
+Files in the PG/etc directory
+=============================
 
 README                 this file
 
-ProofGeneral.spec      For building the Proof General RPM.
+ProofGeneral.spec      Sample specfile for building the Proof General RPM.
 		       Use "rpm -tb" to build from tarball.
 
 ProofGeneral.menu      Menu file for some Linux versions.  
@@ -12,8 +12,6 @@ ProofGeneral.menu      Menu file for some Linux versions.
 ProofGeneral.desktop   Menu file for some Linux versions.  
 		       Install in /etc/X11/applnk/Applications/
 
-announce	       Announcement
-		       
 lego		       Files for testing: LEGO Proof General
 isa					  Isabelle Proof General
 isar					  Isar PG
@@ -22,15 +20,11 @@ coq					  Coq
 <otherprover>				   .. others, similarly
 
 
-bug-notes.txt	       Test cases for Emacs or PG bugs
 cvs-tips.txt	       Notes on  cvs with PG project
-debugging-tips.txt     Notes on  debugging
+development-tips.txt   Notes on  development
 profiling.txt			 profiling
 
-release-log.txt	        A record of official releases 
-
-testing-log.txt	        Notes on testing 
-test-schedule.txt
-TESTS
+testsuite/	       Test suites (replaced by generic/pg-autotest)
+trac/		       Test cases for reported bugs to check regression
 
 
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index bc6f3671..3fe0fa9b 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -186,8 +186,8 @@ Dead or nil buffers are not represented in the list.
 
 ;;;***
 
-;;;### (autoloads (profile-pg) "pg-dev" "../lib/pg-dev.el" (19564
-;;;;;;  4338))
+;;;### (autoloads (profile-pg) "pg-dev" "../lib/pg-dev.el" (19622
+;;;;;;  2314))
 ;;; Generated autoloads from ../lib/pg-dev.el
 
 (autoload 'profile-pg "pg-dev" "\
@@ -198,7 +198,7 @@ Not documented
 ;;;***
 
 ;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
-;;;;;;  (19121 59721))
+;;;;;;  (19625 55352))
 ;;; Generated autoloads from pg-goals.el
 
 (autoload 'proof-goals-config-done "pg-goals" "\
@@ -232,7 +232,7 @@ Existing XML files are overwritten.
 ;;;***
 
 ;;;### (autoloads (defpacustom proof-defpacustom-fn) "pg-pamacs"
-;;;;;;  "pg-pamacs.el" (19554 65355))
+;;;;;;  "pg-pamacs.el" (19621 61895))
 ;;; Generated autoloads from pg-pamacs.el
 
 (autoload 'proof-defpacustom-fn "pg-pamacs" "\
@@ -279,7 +279,7 @@ Send an <askprefs> message to the prover.
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
 ;;;;;;  pg-response-message pg-response-display-with-face pg-response-maybe-erase
 ;;;;;;  proof-response-config-done proof-response-mode) "pg-response"
-;;;;;;  "pg-response.el" (19562 32774))
+;;;;;;  "pg-response.el" (19574 64296))
 ;;; Generated autoloads from pg-response.el
 
 (autoload 'proof-response-mode "pg-response" "\
@@ -338,11 +338,12 @@ See `pg-next-error-regexp'.
 ;;;### (autoloads (proof-autosend-enable pg-clear-input-ring pg-remove-from-input-history
 ;;;;;;  pg-add-to-input-history pg-next-matching-input-from-input
 ;;;;;;  pg-previous-matching-input-from-input proof-imenu-enable
-;;;;;;  pg-hint pg-next-error-hint pg-processing-complete-hint pg-jump-to-end-hint
-;;;;;;  pg-response-buffers-hint pg-slow-fontify-tracing-hint proof-electric-terminator-enable
+;;;;;;  pg-identifier-near-point-query pg-hint pg-next-error-hint
+;;;;;;  pg-processing-complete-hint pg-jump-to-end-hint pg-response-buffers-hint
+;;;;;;  pg-slow-fontify-tracing-hint proof-electric-terminator-enable
 ;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command
 ;;;;;;  proof-goto-point proof-script-new-command-advance) "pg-user"
-;;;;;;  "pg-user.el" (19570 20547))
+;;;;;;  "pg-user.el" (19633 61674))
 ;;; Generated autoloads from pg-user.el
 
 (autoload 'proof-script-new-command-advance "pg-user" "\
@@ -371,7 +372,8 @@ CMDVAR is a variable holding a function or string.  Automatically has history.
 \(fn FN DOC CMDVAR PROMPT &rest BODY)" nil (quote macro))
 
 (autoload 'proof-electric-terminator-enable "pg-user" "\
-Make sure the modeline is updated to display new value for electric terminator.
+Ensure modeline update to display new value for electric terminator.
+This a function is called by the custom-set property 'proof-set-value.
 
 \(fn)" nil nil)
 
@@ -406,6 +408,13 @@ The function `substitute-command-keys' is called on the argument.
 
 \(fn HINTMSG)" nil nil)
 
+(autoload 'pg-identifier-near-point-query "pg-user" "\
+Query the prover about the identifier near point.
+If the result is successful, we add a span to the buffer which has
+a popup with the information in it.
+
+\(fn)" t nil)
+
 (autoload 'proof-imenu-enable "pg-user" "\
 Add or remove index menu.
 
@@ -507,7 +516,7 @@ Indent current line of proof script, if indentation enabled.
 ;;;***
 
 ;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-set-global)
-;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19550 46151))
+;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19575 41316))
 ;;; Generated autoloads from proof-maths-menu.el
 
 (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
@@ -528,8 +537,8 @@ in future if we have just activated it for this buffer.
 ;;;***
 
 ;;;### (autoloads (proof-aux-menu proof-menu-define-specific proof-menu-define-main
-;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19570
-;;;;;;  20547))
+;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19625
+;;;;;;  55352))
 ;;; Generated autoloads from proof-menu.el
 
 (autoload 'proof-menu-define-keys "proof-menu" "\
@@ -578,7 +587,7 @@ in future if we have just activated it for this buffer.
 ;;;;;;  proof-insert-pbp-command proof-register-possibly-new-processed-file
 ;;;;;;  pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p
 ;;;;;;  proof-unprocessed-begin proof-colour-locked) "proof-script"
-;;;;;;  "proof-script.el" (19564 4338))
+;;;;;;  "proof-script.el" (19633 62018))
 ;;; Generated autoloads from proof-script.el
 
 (autoload 'proof-colour-locked "proof-script" "\
@@ -607,13 +616,14 @@ Non-nil if the locked region is empty.  Works on any buffer.
 Add a daughter help span for SPAN with help message, highlight, actions.
 The daughter span covers the non whitespace content of the main span.
 
-We add the last output (which should be non-empty) to the hover display.
+We add the last output (when non-empty) to the hover display, and
+also as the 'response property on the span.
 
 Optional argument MOUSEFACE means use the given face as a mouse highlight
 face, if it is a face, otherwise, if it is non-nil but not a face,
 do not add a mouse highlight.
 
-Argument FACE means add regular face property FACE to the span.
+Argument FACE means add 'face property FACE to the span.
 
 \(fn SPAN &optional MOUSEFACE FACE)" nil nil)
 
@@ -662,7 +672,7 @@ finish setup which depends on specific proof assistant configuration.
 ;;;;;;  proof-shell-invisible-cmd-get-result proof-shell-invisible-command
 ;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
 ;;;;;;  proof-shell-available-p proof-shell-ready-prover) "proof-shell"
-;;;;;;  "proof-shell.el" (19570 20547))
+;;;;;;  "proof-shell.el" (19633 48731))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload 'proof-shell-ready-prover "proof-shell" "\
@@ -726,13 +736,20 @@ The queue mode is set to 'advancing
 
 (autoload 'proof-shell-wait "proof-shell" "\
 Busy wait for `proof-shell-busy' to become nil, reading from prover.
+
 Needed between sequences of commands to maintain synchronization,
 because Proof General does not allow for the action list to be extended
 in some cases.   Also is considerably faster than leaving the Emacs 
 top-level command loop to read from the prover.
-May be called by `proof-shell-invisible-command'.
 
-\(fn &optional INTERRUPT-ON-INPUT)" nil nil)
+Called by `proof-shell-invisible-command' and `proof-process-buffer'
+when setting `proof-fast-process-buffer' is enabled.
+
+If INTERRUPT-ON-INPUT is non-nil, return if input is received.
+
+If TIMEOUTSECS is a number, time out after that many seconds.
+
+\(fn &optional INTERRUPT-ON-INPUT TIMEOUTSECS)" nil nil)
 
 (autoload 'proof-shell-invisible-command "proof-shell" "\
 Send CMD to the proof process.
@@ -752,7 +769,8 @@ INVISIBLECALLBACK will be invoked after the command has finished,
 if it is set.  It should probably run the hook variables
 `proof-state-change-hook'.
 
-FLAGS are put onto the If NOERROR is set, surpress usual error action.
+FLAGS are additional flags to put onto the `proof-action-list'.
+The flag 'invisible is always added to FLAGS.
 
 \(fn CMD &optional WAIT INVISIBLECALLBACK &rest FLAGS)" nil nil)
 
@@ -785,7 +803,7 @@ processing.
 ;;;***
 
 ;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el"
-;;;;;;  (19570 20548))
+;;;;;;  (19634 16192))
 ;;; Generated autoloads from proof-site.el
 
 (autoload 'proof-ready-for-assistant "proof-site" "\
@@ -797,7 +815,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
 ;;;***
 
 ;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;;  "proof-splash" "proof-splash.el" (19570 20548))
+;;;;;;  "proof-splash" "proof-splash.el" (19628 18525))
 ;;; Generated autoloads from proof-splash.el
 
 (autoload 'proof-splash-display-screen "proof-splash" "\
@@ -816,7 +834,7 @@ Make sure the user gets welcomed one way or another.
 ;;;***
 
 ;;;### (autoloads (proof-format) "proof-syntax" "proof-syntax.el"
-;;;;;;  (19564 4338))
+;;;;;;  (19609 53995))
 ;;; Generated autoloads from proof-syntax.el
 
 (defsubst proof-replace-regexp-in-string (regexp rep string) "\
@@ -832,7 +850,7 @@ may be a string or sexp evaluated to get a string.
 ;;;***
 
 ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;;  "proof-toolbar" "proof-toolbar.el" (19550 46151))
+;;;;;;  "proof-toolbar" "proof-toolbar.el" (19609 20575))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload 'proof-toolbar-setup "proof-toolbar" "\
@@ -879,8 +897,8 @@ is changed.
 
 ;;;***
 
-;;;### (autoloads (proof-debug) "proof-utils" "proof-utils.el" (19554
-;;;;;;  65355))
+;;;### (autoloads (proof-debug) "proof-utils" "proof-utils.el" (19630
+;;;;;;  57223))
 ;;; Generated autoloads from proof-utils.el
 
 (autoload 'proof-debug "proof-utils" "\
@@ -950,7 +968,7 @@ in your emacs font.
 ;;;***
 
 ;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;;  (19570 20548))
+;;;;;;  (19591 34223))
 ;;; Generated autoloads from ../lib/unicode-tokens.el
 
 (autoload 'unicode-tokens-encode-str "unicode-tokens" "\
@@ -964,7 +982,7 @@ Return a unicode encoded version presentation of STR.
 ;;;;;;  "../lib/proof-compat.el" "../lib/span.el" "pg-autotest.el"
 ;;;;;;  "pg-custom.el" "pg-pbrpm.el" "pg-vars.el" "proof-auxmodes.el"
 ;;;;;;  "proof-config.el" "proof-faces.el" "proof-useropts.el" "proof.el")
-;;;;;;  (19570 20593 985026))
+;;;;;;  (19634 16926 377965))
 
 ;;;***