Updated

author: David Aspinall <da@inf.ed.ac.uk> 2009-09-15 08:40:12 +0000
committer: David Aspinall <da@inf.ed.ac.uk> 2009-09-15 08:40:12 +0000
commit: 5286b54dcbbda5715a59a7fc50cdfb9872706950 (patch)
tree: a830ea13cbed19d7312748b43ce6f194354377ec /TAGS
parent: 815cadebd99cd25dc78be6e2ba3af177c4140ebd (diff)
1 files changed, 1302 insertions, 1270 deletions
diff --git a/TAGS b/TAGS
index cd587396..5482b03d 100644
--- a/TAGS
+++ b/TAGS
@@ -37,146 +37,146 @@ coq/coq-db.el,600
 (defconst coq-solve-tactics-face 236,8599
 
 coq/coq.el,5449
-(defcustom coq-translate-to-v8 48,1389
-(defun coq-build-prog-args 54,1569
-(defcustom coq-compile-file-command 64,1865
-(defcustom coq-use-makefile 72,2184
-(defcustom coq-default-undo-limit 80,2407
-(defconst coq-shell-init-cmd85,2535
-(defcustom coq-prog-env 91,2662
-(defconst coq-shell-restart-cmd 99,2912
-(defvar coq-shell-prompt-pattern101,2966
-(defvar coq-shell-cd 109,3270
-(defvar coq-shell-proof-completed-regexp 113,3430
-(defvar coq-goal-regexp116,3582
-(defun coq-library-directory 123,3696
-(defcustom coq-tags 130,3875
-(defconst coq-interrupt-regexp 135,4025
-(defcustom coq-www-home-page 140,4146
-(defvar coq-outline-regexp147,4314
-(defvar coq-outline-heading-end-regexp 154,4526
-(defvar coq-shell-outline-regexp 156,4580
-(defvar coq-shell-outline-heading-end-regexp 157,4630
-(defconst coq-state-preserving-tactics-regexp163,4795
-(defconst coq-state-changing-commands-regexp165,4895
-(defconst coq-state-preserving-commands-regexp167,5002
-(defconst coq-commands-regexp169,5113
-(defvar coq-retractable-instruct-regexp171,5190
-(defvar coq-non-retractable-instruct-regexp173,5280
-(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 247,7865
-(defvar coq-last-but-one-proofstack 250,7963
-(defun coq-get-span-statenum 253,8073
-(defun coq-get-span-proofnum 258,8188
-(defun coq-get-span-proofstack 263,8303
-(defun coq-set-span-statenum 268,8447
-(defun coq-get-span-goalcmd 273,8578
-(defun coq-set-span-goalcmd 278,8692
-(defun coq-set-span-proofnum 283,8822
-(defun coq-set-span-proofstack 288,8953
-(defun proof-last-locked-span 293,9113
-(defun coq-set-state-infos 308,9716
-(defun count-not-intersection 347,11711
-(defun coq-find-and-forget 378,12961
-(defvar coq-current-goal 397,13848
-(defun coq-goal-hyp 400,13913
-(defun coq-state-preserving-p 413,14345
-(defconst notation-print-kinds-table427,14846
-(defun coq-PrintScope 431,15013
-(defun coq-guess-or-ask-for-string 449,15562
-(defun coq-ask-do 463,16130
-(defun coq-SearchIsos 472,16515
-(defun coq-SearchConstant 478,16748
-(defun coq-SearchRewrite 482,16841
-(defun coq-SearchAbout 486,16939
-(defun coq-Print 490,17031
-(defun coq-About 494,17153
-(defun coq-LocateConstant 498,17270
-(defun coq-LocateLibrary 504,17405
-(defun coq-addquotes 510,17555
-(defun coq-LocateNotation 512,17603
-(defun coq-Pwd 519,17801
-(defun coq-Inspect 525,17933
-(defun coq-PrintSection(529,18033
-(defun coq-Print-implicit 533,18126
-(defun coq-Check 538,18277
-(defun coq-Show 543,18385
-(defun coq-Compile 557,18828
-(defun coq-guess-command-line 569,19146
-(defpacustom use-editing-holes 608,20818
-(defun coq-mode-config 618,21155
-(defun coq-shell-mode-config 722,25039
-(defun coq-goals-mode-config 765,26838
-(defun coq-response-config 772,27082
-(defpacustom print-fully-explicit 797,27907
-(defpacustom print-implicit 802,28055
-(defpacustom print-coercions 807,28221
-(defpacustom print-match-wildcards 812,28365
-(defpacustom print-elim-types 817,28545
-(defpacustom printing-depth 822,28711
-(defpacustom undo-depth 827,28872
-(defpacustom time-commands 832,29019
-(defpacustom undo-limit 836,29129
-(defpacustom auto-compile-vos 841,29231
-(defun coq-maybe-compile-buffer 870,30345
-(defun coq-ancestors-of 906,31873
-(defun coq-all-ancestors-of 929,32837
-(defun coq-process-require-command 940,33184
-(defun coq-included-children 945,33311
-(defun coq-process-file 966,34150
-(defun coq-preprocessing 981,34689
-(defun coq-fake-constant-markup 994,35096
-(defun coq-create-span-menu 1010,35701
-(defconst module-kinds-table1027,36196
-(defconst modtype-kinds-table1031,36345
-(defun coq-insert-section-or-module 1035,36474
-(defconst reqkinds-kinds-table1058,37332
-(defun coq-insert-requires 1063,37477
-(defun coq-end-Section 1079,37980
-(defun coq-insert-intros 1097,38558
-(defun coq-insert-infoH-hook 1110,39090
-(defun coq-insert-as 1115,39242
-(defun coq-insert-match 1133,39985
-(defun coq-insert-tactic 1165,41167
-(defun coq-insert-tactical 1171,41406
-(defun coq-insert-command 1177,41655
-(defun coq-insert-term 1183,41899
-(define-key coq-keymap 1189,42096
-(define-key coq-keymap 1190,42154
-(define-key coq-keymap 1191,42211
-(define-key coq-keymap 1192,42280
-(define-key coq-keymap 1193,42336
-(define-key coq-keymap 1194,42385
-(define-key coq-keymap 1195,42443
-(define-key coq-keymap 1197,42504
-(define-key coq-keymap 1198,42563
-(define-key coq-keymap 1200,42627
-(define-key coq-keymap 1201,42687
-(define-key coq-keymap 1203,42743
-(define-key coq-keymap 1204,42793
-(define-key coq-keymap 1205,42843
-(define-key coq-keymap 1206,42893
-(define-key coq-keymap 1207,42947
-(define-key coq-keymap 1208,43006
-(defvar last-coq-error-location 1216,43137
-(defun coq-get-last-error-location 1225,43536
-(defun coq-highlight-error 1272,45874
-(defvar coq-allow-highlight-error 1307,47161
-(defun coq-decide-highlight-error 1314,47488
-(defun coq-highlight-error-hook 1318,47610
-(defun first-word-of-buffer 1329,48003
-(defun coq-show-first-goal 1337,48206
-(defvar coq-modeline-string2 1354,48901
-(defvar coq-modeline-string1 1355,48945
-(defvar coq-modeline-string0 1356,48988
-(defun coq-build-subgoals-string 1357,49033
-(defun coq-update-minor-mode-alist 1362,49199
-(defun is-not-split-vertic 1388,50270
-(defun optim-resp-windows 1397,50709
+(defcustom coq-translate-to-v8 47,1330
+(defun coq-build-prog-args 53,1510
+(defcustom coq-compile-file-command 63,1806
+(defcustom coq-use-makefile 71,2125
+(defcustom coq-default-undo-limit 79,2348
+(defconst coq-shell-init-cmd84,2476
+(defcustom coq-prog-env 90,2603
+(defconst coq-shell-restart-cmd 98,2853
+(defvar coq-shell-prompt-pattern100,2907
+(defvar coq-shell-cd 108,3211
+(defvar coq-shell-proof-completed-regexp 112,3371
+(defvar coq-goal-regexp115,3523
+(defun coq-library-directory 122,3637
+(defcustom coq-tags 129,3816
+(defconst coq-interrupt-regexp 134,3966
+(defcustom coq-www-home-page 139,4087
+(defvar coq-outline-regexp146,4255
+(defvar coq-outline-heading-end-regexp 153,4467
+(defvar coq-shell-outline-regexp 155,4521
+(defvar coq-shell-outline-heading-end-regexp 156,4571
+(defconst coq-state-preserving-tactics-regexp162,4736
+(defconst coq-state-changing-commands-regexp164,4836
+(defconst coq-state-preserving-commands-regexp166,4943
+(defconst coq-commands-regexp168,5054
+(defvar coq-retractable-instruct-regexp170,5131
+(defvar coq-non-retractable-instruct-regexp172,5221
+(defun coq-set-undo-limit 206,6098
+(defun build-list-id-from-string 210,6228
+(defun coq-last-prompt-info 222,6726
+(defun coq-last-prompt-info-safe 234,7258
+(defvar coq-last-but-one-statenum 240,7515
+(defvar coq-last-but-one-proofnum 246,7812
+(defvar coq-last-but-one-proofstack 249,7910
+(defun coq-get-span-statenum 252,8020
+(defun coq-get-span-proofnum 257,8135
+(defun coq-get-span-proofstack 262,8250
+(defun coq-set-span-statenum 267,8394
+(defun coq-get-span-goalcmd 272,8525
+(defun coq-set-span-goalcmd 277,8639
+(defun coq-set-span-proofnum 282,8769
+(defun coq-set-span-proofstack 287,8900
+(defun proof-last-locked-span 292,9060
+(defun coq-set-state-infos 307,9663
+(defun count-not-intersection 346,11658
+(defun coq-find-and-forget 377,12908
+(defvar coq-current-goal 396,13795
+(defun coq-goal-hyp 399,13860
+(defun coq-state-preserving-p 412,14292
+(defconst notation-print-kinds-table426,14793
+(defun coq-PrintScope 430,14960
+(defun coq-guess-or-ask-for-string 448,15509
+(defun coq-ask-do 462,16077
+(defun coq-SearchIsos 471,16462
+(defun coq-SearchConstant 477,16695
+(defun coq-SearchRewrite 481,16788
+(defun coq-SearchAbout 485,16886
+(defun coq-Print 489,16978
+(defun coq-About 493,17100
+(defun coq-LocateConstant 497,17217
+(defun coq-LocateLibrary 503,17352
+(defun coq-addquotes 509,17502
+(defun coq-LocateNotation 511,17550
+(defun coq-Pwd 518,17748
+(defun coq-Inspect 524,17880
+(defun coq-PrintSection(528,17980
+(defun coq-Print-implicit 532,18073
+(defun coq-Check 537,18224
+(defun coq-Show 542,18332
+(defun coq-Compile 556,18775
+(defun coq-guess-command-line 568,19093
+(defpacustom use-editing-holes 607,20765
+(defun coq-mode-config 617,21102
+(defun coq-shell-mode-config 721,24986
+(defun coq-goals-mode-config 764,26785
+(defun coq-response-config 771,27029
+(defpacustom print-fully-explicit 796,27854
+(defpacustom print-implicit 801,28002
+(defpacustom print-coercions 806,28168
+(defpacustom print-match-wildcards 811,28312
+(defpacustom print-elim-types 816,28492
+(defpacustom printing-depth 821,28658
+(defpacustom undo-depth 826,28819
+(defpacustom time-commands 831,28966
+(defpacustom undo-limit 835,29076
+(defpacustom auto-compile-vos 840,29178
+(defun coq-maybe-compile-buffer 869,30292
+(defun coq-ancestors-of 905,31820
+(defun coq-all-ancestors-of 928,32784
+(defun coq-process-require-command 939,33131
+(defun coq-included-children 944,33258
+(defun coq-process-file 965,34097
+(defun coq-preprocessing 980,34636
+(defun coq-fake-constant-markup 994,35071
+(defun coq-create-span-menu 1010,35676
+(defconst module-kinds-table1027,36171
+(defconst modtype-kinds-table1031,36320
+(defun coq-insert-section-or-module 1035,36449
+(defconst reqkinds-kinds-table1058,37307
+(defun coq-insert-requires 1063,37452
+(defun coq-end-Section 1079,37955
+(defun coq-insert-intros 1097,38533
+(defun coq-insert-infoH-hook 1110,39065
+(defun coq-insert-as 1115,39273
+(defun coq-insert-match 1132,39976
+(defun coq-insert-tactic 1164,41158
+(defun coq-insert-tactical 1170,41397
+(defun coq-insert-command 1176,41646
+(defun coq-insert-term 1182,41890
+(define-key coq-keymap 1188,42087
+(define-key coq-keymap 1189,42145
+(define-key coq-keymap 1190,42202
+(define-key coq-keymap 1191,42271
+(define-key coq-keymap 1192,42327
+(define-key coq-keymap 1193,42376
+(define-key coq-keymap 1194,42434
+(define-key coq-keymap 1196,42495
+(define-key coq-keymap 1197,42554
+(define-key coq-keymap 1199,42618
+(define-key coq-keymap 1200,42678
+(define-key coq-keymap 1202,42734
+(define-key coq-keymap 1203,42784
+(define-key coq-keymap 1204,42834
+(define-key coq-keymap 1205,42884
+(define-key coq-keymap 1206,42938
+(define-key coq-keymap 1207,42997
+(defvar last-coq-error-location 1215,43128
+(defun coq-get-last-error-location 1224,43527
+(defun coq-highlight-error 1272,45907
+(defvar coq-allow-highlight-error 1306,47157
+(defun coq-decide-highlight-error 1313,47483
+(defun coq-highlight-error-hook 1318,47668
+(defun first-word-of-buffer 1329,48061
+(defun coq-show-first-goal 1337,48264
+(defvar coq-modeline-string2 1354,48959
+(defvar coq-modeline-string1 1355,49003
+(defvar coq-modeline-string0 1356,49046
+(defun coq-build-subgoals-string 1357,49091
+(defun coq-update-minor-mode-alist 1362,49257
+(defun is-not-split-vertic 1388,50328
+(defun optim-resp-windows 1397,50767
 
 coq/coq-indent.el,2223
 (defconst coq-any-command-regexp20,368
@@ -232,13 +232,13 @@ coq/coq-indent.el,2223
 (defun coq-indent-region 722,28820
 
 coq/coq-local-vars.el,280
-(defconst coq-local-vars-doc 18,369
-(defun coq-insert-coq-prog-name 76,2897
-(defun coq-read-directory 87,3370
-(defun coq-extract-directories-from-args 111,4473
-(defun coq-ask-prog-args 126,5025
-(defun coq-ask-prog-name 148,6089
-(defun coq-ask-insert-coq-prog-name 166,6844
+(defconst coq-local-vars-doc 20,429
+(defun coq-insert-coq-prog-name 78,2957
+(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,2428
 (defcustom coq-prog-name 18,558
@@ -317,14 +317,14 @@ coq/coq-unicode-tokens.el,454
 (defconst coq-control-regions249,6553
 
 demoisa/demoisa.el,349
-(defcustom isabelledemo-prog-name 54,1805
-(defcustom isabelledemo-web-page59,1927
-(defun demoisa-config 70,2157
-(defun demoisa-shell-config 91,2949
-(define-derived-mode demoisa-mode 116,3878
-(define-derived-mode demoisa-shell-mode 121,4001
-(define-derived-mode demoisa-response-mode 126,4144
-(define-derived-mode demoisa-goals-mode 130,4271
+(defcustom isabelledemo-prog-name 56,1848
+(defcustom isabelledemo-web-page61,1970
+(defun demoisa-config 72,2200
+(defun demoisa-shell-config 93,2992
+(define-derived-mode demoisa-mode 118,3921
+(define-derived-mode demoisa-shell-mode 123,4044
+(define-derived-mode demoisa-response-mode 128,4187
+(define-derived-mode demoisa-goals-mode 132,4314
 
 hol98/hol98.el,121
 (defvar hol98-keywords 17,419
@@ -333,95 +333,95 @@ hol98/hol98.el,121
 (defvar hol98-tacticals 20,499
 
 isar/isabelle-system.el,1291
-(defgroup isabelle 26,776
-(defcustom isabelle-web-page30,904
-(defcustom isa-isabelle-command39,1121
-(defvar isabelle-not-found 57,1803
-(defun isa-set-isabelle-command 60,1918
-(defun isa-shell-command-to-string 83,2936
-(defun isa-getenv 89,3160
-(defcustom isabelle-program-name-override 109,3852
-(defvar isabelle-prog-name 120,4198
-(defun isa-tool-list-logics 123,4308
-(defcustom isabelle-logics-available 130,4547
-(defcustom isabelle-chosen-logic 140,4884
-(defvar isabelle-chosen-logic-prev 156,5468
-(defun isabelle-hack-local-variables-function 159,5588
-(defun isabelle-set-prog-name 171,6027
-(defun isabelle-choose-logic 196,7217
-(defun isa-view-doc 215,7979
-(defun isa-tool-list-docs 224,8244
-(defconst isabelle-verbatim-regexp 242,8967
-(defun isabelle-verbatim 245,9109
-(defcustom isabelle-refresh-logics 252,9270
-(defvar isabelle-docs-menu260,9598
-(defvar isabelle-logics-menu-entries 267,9883
-(defun isabelle-logics-menu-calculate 270,9956
-(defvar isabelle-time-to-refresh-logics 291,10598
-(defun isabelle-logics-menu-refresh 295,10693
-(defun isabelle-menu-bar-update-logics 310,11326
-(defun isabelle-load-isar-keywords 326,11955
-(defun isabelle-create-span-menu 347,12683
-(defun isabelle-xml-sml-escapes 363,13125
-(defun isabelle-process-pgip 366,13226
-
-isar/isar.el,1610
-(defcustom isar-keywords-name 37,884
-(defpgdefault completion-table 54,1402
-(defcustom isar-web-page56,1455
-(defun isar-strip-terminators 70,1805
-(defun isar-markup-ml 83,2182
-(defun isar-mode-config-set-variables 88,2317
-(defun isar-shell-mode-config-set-variables 159,5303
-(defpacustom use-find-theorems-form 240,8437
-(defun isar-set-proof-find-theorems-command 245,8603
-(defpacustom use-linear-undo 251,8787
-(defun isar-set-undo-commands 255,8912
-(defun isar-configure-from-settings 266,9355
-(defun isar-remove-file 274,9502
-(defun isar-shell-compute-new-files-list 284,9857
-(define-derived-mode isar-shell-mode 302,10429
-(define-derived-mode isar-response-mode 307,10552
-(define-derived-mode isar-goals-mode 312,10680
-(define-derived-mode isar-mode 317,10801
-(defpgdefault menu-entries374,12823
-(defalias 'isar-set-command isar-set-command404,13980
-(defpgdefault help-menu-entries 406,14036
-(defun isar-count-undos 409,14112
-(defun isar-find-and-forget 435,15087
-(defun isar-goal-command-p 475,16614
-(defun isar-global-save-command-p 480,16791
-(defvar isar-current-goal 501,17575
-(defun isar-state-preserving-p 504,17641
-(defvar isar-shell-current-line-width 529,18838
-(defun isar-shell-adjust-line-width 534,19030
-(defun isar-string-wrapping 558,19801
-(defun isar-positions-of 567,19998
-(defun isar-command-wrapping 591,20702
-(defcustom isar-wrap-commands-singly 600,21046
-(defun isar-preprocessing 606,21242
-(defun isar-mode-config 625,21869
-(defun isar-shell-mode-config 636,22427
-(defun isar-response-mode-config 646,22776
-(defun isar-goals-mode-config 656,23111
-
-isar/isar-find-theorems.el,778
-(defun isar-find-theorems-minibuffer 18,713
-(defun isar-find-theorems-form 32,1332
-(defvar isar-find-theorems-data 74,3132
-(defvar isar-find-theorems-widget-number 88,3467
-(defvar isar-find-theorems-widget-pattern 91,3565
-(defvar isar-find-theorems-widget-intro 94,3657
-(defvar isar-find-theorems-widget-elim 97,3743
-(defvar isar-find-theorems-widget-dest 100,3827
-(defvar isar-find-theorems-widget-name 103,3911
-(defvar isar-find-theorems-widget-simp 106,3998
-(defun isar-find-theorems-create-searchform111,4144
-(defun isar-find-theorems-create-help 251,8687
-(defun isar-find-theorems-submit-searchform294,10859
-(defun isar-find-theorems-parse-criteria 372,13229
-(defun isar-find-theorems-parse-number 465,16210
-(defun isar-find-theorems-filter-empty 475,16487
+(defgroup isabelle 26,716
+(defcustom isabelle-web-page30,844
+(defcustom isa-isabelle-command39,1061
+(defvar isabelle-not-found 57,1743
+(defun isa-set-isabelle-command 60,1858
+(defun isa-shell-command-to-string 83,2876
+(defun isa-getenv 89,3100
+(defcustom isabelle-program-name-override 109,3792
+(defvar isabelle-prog-name 120,4138
+(defun isa-tool-list-logics 123,4248
+(defcustom isabelle-logics-available 130,4487
+(defcustom isabelle-chosen-logic 140,4824
+(defvar isabelle-chosen-logic-prev 156,5408
+(defun isabelle-hack-local-variables-function 159,5528
+(defun isabelle-set-prog-name 171,5967
+(defun isabelle-choose-logic 196,7157
+(defun isa-view-doc 215,7919
+(defun isa-tool-list-docs 224,8184
+(defconst isabelle-verbatim-regexp 242,8907
+(defun isabelle-verbatim 245,9049
+(defcustom isabelle-refresh-logics 252,9210
+(defvar isabelle-docs-menu260,9538
+(defvar isabelle-logics-menu-entries 267,9823
+(defun isabelle-logics-menu-calculate 270,9896
+(defvar isabelle-time-to-refresh-logics 291,10538
+(defun isabelle-logics-menu-refresh 295,10633
+(defun isabelle-menu-bar-update-logics 310,11266
+(defun isabelle-load-isar-keywords 326,11895
+(defun isabelle-create-span-menu 347,12623
+(defun isabelle-xml-sml-escapes 363,13065
+(defun isabelle-process-pgip 366,13166
+
+isar/isar.el,1616
+(defcustom isar-keywords-name 39,915
+(defpgdefault completion-table 56,1433
+(defcustom isar-web-page58,1486
+(defun isar-strip-terminators 72,1836
+(defun isar-markup-ml 85,2213
+(defun isar-mode-config-set-variables 90,2348
+(defun isar-shell-mode-config-set-variables 162,5389
+(defun isar-set-proof-find-theorems-command 243,8523
+(defpacustom use-find-theorems-form 249,8707
+(defun isar-set-undo-commands 254,8873
+(defpacustom use-linear-undo 265,9324
+(defun isar-configure-from-settings 270,9482
+(defun isar-remove-file 278,9629
+(defun isar-shell-compute-new-files-list 288,9984
+(define-derived-mode isar-shell-mode 307,10564
+(define-derived-mode isar-response-mode 312,10691
+(define-derived-mode isar-goals-mode 317,10824
+(define-derived-mode isar-mode 322,10950
+(defpgdefault menu-entries379,12965
+(defalias 'isar-set-command isar-set-command409,14122
+(defpgdefault help-menu-entries 411,14178
+(defun isar-count-undos 414,14254
+(defun isar-find-and-forget 440,15229
+(defun isar-goal-command-p 480,16756
+(defun isar-global-save-command-p 485,16933
+(defvar isar-current-goal 506,17717
+(defun isar-state-preserving-p 509,17783
+(defvar isar-shell-current-line-width 534,18980
+(defun isar-shell-adjust-line-width 539,19172
+(defsubst isar-string-wrapping 564,19970
+(defsubst isar-positions-of 573,20164
+(defcustom isar-wrap-commands-singly 579,20369
+(defun isar-command-wrapping 585,20565
+(defun isar-preprocessing 593,20879
+(defun isar-mode-config 611,21430
+(defun isar-shell-mode-config 625,22083
+(defun isar-response-mode-config 635,22432
+(defun isar-goals-mode-config 645,22767
+
+isar/isar-find-theorems.el,779
+(defvar isar-find-theorems-data 19,565
+(defun isar-find-theorems-minibuffer 35,1039
+(defun isar-find-theorems-form 49,1658
+(defvar isar-find-theorems-widget-number 92,3532
+(defvar isar-find-theorems-widget-pattern 95,3630
+(defvar isar-find-theorems-widget-intro 98,3722
+(defvar isar-find-theorems-widget-elim 101,3808
+(defvar isar-find-theorems-widget-dest 104,3892
+(defvar isar-find-theorems-widget-name 107,3976
+(defvar isar-find-theorems-widget-simp 110,4063
+(defun isar-find-theorems-create-searchform115,4209
+(defun isar-find-theorems-create-help 255,8752
+(defun isar-find-theorems-submit-searchform298,10924
+(defun isar-find-theorems-parse-criteria 376,13294
+(defun isar-find-theorems-parse-number 469,16275
+(defun isar-find-theorems-filter-empty 479,16552
 
 isar/isar-keywords.el,1052
 (defconst isar-keywords-major13,481
@@ -453,7 +453,7 @@ isar/isar-mmm.el,81
 (defconst isar-start-latex-regexp24,744
 (defconst isar-start-sml-regexp36,1172
 
-isar/isar-syntax.el,3703
+isar/isar-syntax.el,3799
 (defconst isar-script-syntax-table-entries18,424
 (defconst isar-script-syntax-table-alist42,826
 (defun isar-init-syntax-table 51,1109
@@ -469,127 +469,129 @@ isar/isar-syntax.el,3703
 (defconst isar-keywords-local-goal110,2705
 (defconst isar-keywords-proper114,2810
 (defconst isar-keywords-improper119,2929
-(defconst isar-keywords-outline124,3061
-(defconst isar-keywords-fume127,3126
-(defconst isar-keywords-indent-open134,3316
-(defconst isar-keywords-indent-close140,3479
-(defconst isar-keywords-indent-enclose144,3577
-(defun isar-regexp-simple-alt 153,3771
-(defun isar-ids-to-regexp 173,4531
-(defconst isar-ext-first 207,5916
-(defconst isar-ext-rest 208,5983
-(defconst isar-long-id-stuff 210,6055
-(defconst isar-id 211,6129
-(defconst isar-idx 212,6199
-(defconst isar-string 214,6258
-(defconst isar-any-command-regexp216,6318
-(defconst isar-name-regexp220,6452
-(defconst isar-improper-regexp226,6747
-(defconst isar-save-command-regexp230,6895
-(defconst isar-global-save-command-regexp233,6996
-(defconst isar-goal-command-regexp236,7110
-(defconst isar-local-goal-command-regexp239,7218
-(defconst isar-comment-start 242,7331
-(defconst isar-comment-end 243,7366
-(defconst isar-comment-start-regexp 244,7399
-(defconst isar-comment-end-regexp 245,7470
-(defconst isar-string-start-regexp 247,7538
-(defconst isar-string-end-regexp 248,7590
-(defun isar-syntactic-context 250,7641
-(defconst isar-antiq-regexp265,8036
-(defconst isar-nesting-regexp271,8187
-(defun isar-nesting 274,8285
-(defun isar-match-nesting 286,8678
-(defface isabelle-class-name-face298,9009
-(defface isabelle-tfree-name-face306,9192
-(defface isabelle-tvar-name-face314,9381
-(defface isabelle-free-name-face322,9569
-(defface isabelle-bound-name-face330,9753
-(defface isabelle-var-name-face338,9940
-(defconst isabelle-class-name-face 346,10127
-(defconst isabelle-tfree-name-face 347,10189
-(defconst isabelle-tvar-name-face 348,10251
-(defconst isabelle-free-name-face 349,10312
-(defconst isabelle-bound-name-face 350,10373
-(defconst isabelle-var-name-face 351,10435
-(defvar isar-font-lock-keywords-1354,10497
-(defun isar-output-flkprops 372,11505
-(defun isar-output-flk 378,11757
-(defvar isar-output-font-lock-keywords-1381,11866
-(defun isar-strip-output-markup 417,13289
-(defconst isar-shell-font-lock-keywords421,13425
-(defvar isar-goals-font-lock-keywords424,13509
-(defconst isar-linear-undo 458,14188
-(defconst isar-undo 460,14231
-(defun isar-remove 462,14274
-(defun isar-undos 465,14349
-(defun isar-cannot-undo 470,14510
-(defconst isar-undo-commands473,14580
-(defconst isar-theory-start-regexp481,14717
-(defconst isar-end-regexp487,14875
-(defconst isar-undo-fail-regexp491,14976
-(defconst isar-undo-skip-regexp495,15080
-(defconst isar-undo-ignore-regexp498,15201
-(defconst isar-undo-remove-regexp501,15266
-(defconst isar-any-entity-regexp509,15441
-(defconst isar-named-entity-regexp514,15614
-(defconst isar-unnamed-entity-regexp519,15777
-(defconst isar-next-entity-regexps522,15879
-(defconst isar-generic-expression530,16183
-(defconst isar-indent-any-regexp541,16416
-(defconst isar-indent-inner-regexp543,16509
-(defconst isar-indent-enclose-regexp545,16575
-(defconst isar-indent-open-regexp547,16691
-(defconst isar-indent-close-regexp549,16801
-(defconst isar-outline-regexp555,16938
-(defconst isar-outline-heading-end-regexp 559,17091
+(defconst isar-keyword-level-alist124,3061
+(defconst isar-keywords-outline 139,3532
+(defconst isar-keywords-fume142,3608
+(defconst isar-keywords-indent-open149,3798
+(defconst isar-keywords-indent-close155,3961
+(defconst isar-keywords-indent-enclose159,4059
+(defun isar-regexp-simple-alt 168,4253
+(defun isar-ids-to-regexp 188,5013
+(defconst isar-ext-first 222,6398
+(defconst isar-ext-rest 223,6465
+(defconst isar-long-id-stuff 225,6537
+(defconst isar-id 226,6611
+(defconst isar-idx 227,6681
+(defconst isar-string 229,6740
+(defconst isar-any-command-regexp231,6800
+(defconst isar-name-regexp235,6934
+(defconst isar-improper-regexp241,7229
+(defconst isar-save-command-regexp245,7377
+(defconst isar-global-save-command-regexp248,7478
+(defconst isar-goal-command-regexp251,7592
+(defconst isar-local-goal-command-regexp254,7700
+(defconst isar-comment-start 257,7813
+(defconst isar-comment-end 258,7848
+(defconst isar-comment-start-regexp 259,7881
+(defconst isar-comment-end-regexp 260,7952
+(defconst isar-string-start-regexp 262,8020
+(defconst isar-string-end-regexp 263,8072
+(defun isar-syntactic-context 265,8123
+(defconst isar-antiq-regexp280,8518
+(defconst isar-nesting-regexp286,8669
+(defun isar-nesting 289,8767
+(defun isar-match-nesting 301,9160
+(defface isabelle-class-name-face313,9491
+(defface isabelle-tfree-name-face321,9674
+(defface isabelle-tvar-name-face329,9863
+(defface isabelle-free-name-face337,10051
+(defface isabelle-bound-name-face345,10235
+(defface isabelle-var-name-face353,10422
+(defconst isabelle-class-name-face 361,10609
+(defconst isabelle-tfree-name-face 362,10671
+(defconst isabelle-tvar-name-face 363,10733
+(defconst isabelle-free-name-face 364,10794
+(defconst isabelle-bound-name-face 365,10855
+(defconst isabelle-var-name-face 366,10917
+(defvar isar-font-lock-keywords-1369,10979
+(defun isar-output-flkprops 387,11987
+(defun isar-output-flk 393,12239
+(defvar isar-output-font-lock-keywords-1396,12348
+(defun isar-strip-output-markup 432,13771
+(defconst isar-shell-font-lock-keywords436,13907
+(defvar isar-goals-font-lock-keywords439,13991
+(defconst isar-linear-undo 473,14670
+(defconst isar-undo 475,14713
+(defun isar-remove 477,14756
+(defun isar-undos 480,14831
+(defun isar-cannot-undo 485,14992
+(defconst isar-undo-commands488,15062
+(defconst isar-theory-start-regexp496,15199
+(defconst isar-end-regexp502,15357
+(defconst isar-undo-fail-regexp506,15458
+(defconst isar-undo-skip-regexp510,15562
+(defconst isar-undo-ignore-regexp513,15683
+(defconst isar-undo-remove-regexp516,15748
+(defconst isar-any-entity-regexp524,15923
+(defconst isar-named-entity-regexp529,16096
+(defconst isar-unnamed-entity-regexp534,16259
+(defconst isar-next-entity-regexps537,16361
+(defconst isar-generic-expression545,16665
+(defconst isar-indent-any-regexp556,16898
+(defconst isar-indent-inner-regexp558,16991
+(defconst isar-indent-enclose-regexp560,17057
+(defconst isar-indent-open-regexp562,17173
+(defconst isar-indent-close-regexp564,17283
+(defconst isar-outline-regexp570,17420
+(defconst isar-outline-heading-end-regexp 574,17573
+(defconst isar-outline-heading-alist 576,17622
 
 isar/isar-unicode-tokens.el,1289
-(defgroup isabelle-tokens 26,636
-(defun isar-set-and-restart-tokens 31,776
-(defconst isar-control-region-format-regexp44,1129
-(defconst isar-control-char-format-regexp47,1223
-(defconst isar-control-char-format	50,1318
-(defconst isar-control-region-format-start 51,1367
-(defconst isar-control-region-format-end 52,1421
-(defcustom isar-control-characters55,1477
-(defcustom isar-control-regions68,1849
-(defconst isar-token-format 92,2565
-(defconst isar-token-variant-format-regexp96,2716
-(defcustom isar-greek-letters-tokens99,2830
-(defcustom isar-misc-letters-tokens139,3688
-(defcustom isar-symbols-tokens151,4006
-(defcustom isar-extended-symbols-tokens357,8817
-(defun isar-try-char 426,10472
-(defcustom isar-symbols-tokens-fallbacks430,10616
-(defcustom isar-bold-nums-tokens457,11546
-(defun isar-map-letters 473,11935
-(defconst isar-script-letters-tokens479,12083
-(defconst isar-roman-letters-tokens484,12221
-(defconst isar-fraktur-letters-tokens489,12357
-(defcustom isar-token-symbol-map 494,12499
-(defcustom isar-user-tokens 510,12968
-(defun isar-init-token-symbol-map 517,13205
-(defcustom isar-symbol-shortcuts540,13760
-(defcustom isar-shortcut-alist 613,15986
-(defun isar-init-shortcut-alists 621,16245
-(defconst isar-tokens-customizable-variables642,16908
+(defgroup isabelle-tokens 25,672
+(defun isar-set-and-restart-tokens 30,812
+(defconst isar-control-region-format-regexp43,1165
+(defconst isar-control-char-format-regexp46,1259
+(defconst isar-control-char-format	49,1354
+(defconst isar-control-region-format-start 50,1403
+(defconst isar-control-region-format-end 51,1457
+(defcustom isar-control-characters54,1513
+(defcustom isar-control-regions67,1885
+(defconst isar-token-format 91,2601
+(defconst isar-token-variant-format-regexp95,2752
+(defcustom isar-greek-letters-tokens98,2866
+(defcustom isar-misc-letters-tokens138,3724
+(defcustom isar-symbols-tokens150,4042
+(defcustom isar-extended-symbols-tokens356,8853
+(defun isar-try-char 425,10508
+(defcustom isar-symbols-tokens-fallbacks429,10652
+(defcustom isar-bold-nums-tokens456,11582
+(defun isar-map-letters 472,11971
+(defconst isar-script-letters-tokens478,12119
+(defconst isar-roman-letters-tokens483,12257
+(defconst isar-fraktur-letters-tokens488,12393
+(defcustom isar-token-symbol-map 493,12535
+(defcustom isar-user-tokens 509,13004
+(defun isar-init-token-symbol-map 516,13241
+(defcustom isar-symbol-shortcuts539,13796
+(defcustom isar-shortcut-alist 612,16023
+(defun isar-init-shortcut-alists 620,16282
+(defconst isar-tokens-customizable-variables641,16945
 
 lclam/lclam.el,524
-(defcustom lclam-prog-name 15,373
-(defcustom lclam-web-page21,521
-(defun lclam-config 32,751
-(defun lclam-shell-config 54,1542
-(define-derived-mode lclam-proofscript-mode 73,2157
-(define-derived-mode lclam-shell-mode 78,2280
-(define-derived-mode lclam-response-mode 83,2414
-(define-derived-mode lclam-goals-mode 87,2537
-(defun lclam-mode 95,2765
-(define-derived-mode thy-mode 132,3611
-(defvar thy-mode-map 135,3709
-(defun thy-add-menus 137,3736
-(defun process-thy-file 176,5217
-(defun update-thy-only 182,5418
+(defcustom lclam-prog-name 18,431
+(defcustom lclam-web-page24,579
+(defun lclam-config 35,809
+(defun lclam-shell-config 57,1600
+(define-derived-mode lclam-proofscript-mode 76,2215
+(define-derived-mode lclam-shell-mode 81,2338
+(define-derived-mode lclam-response-mode 86,2472
+(define-derived-mode lclam-goals-mode 90,2595
+(defun lclam-mode 98,2823
+(define-derived-mode thy-mode 135,3669
+(defvar thy-mode-map 138,3767
+(defun thy-add-menus 140,3794
+(defun process-thy-file 179,5275
+(defun update-thy-only 185,5476
 
 lego/lego.el,1636
 (defcustom lego-tags 21,534
@@ -619,19 +621,19 @@ lego/lego.el,1636
 (defvar lego-shell-outline-heading-end-regexp 138,4218
 (define-derived-mode lego-shell-mode 144,4497
 (define-derived-mode lego-mode 151,4658
-(define-derived-mode lego-goals-mode 162,4953
-(defun lego-count-undos 173,5379
-(defun lego-goal-command-p 193,6197
-(defun lego-find-and-forget 198,6368
-(defun lego-goal-hyp 240,8184
-(defun lego-state-preserving-p 249,8381
-(defvar lego-shell-current-line-width 265,9084
-(defun lego-shell-adjust-line-width 273,9391
-(defun lego-mode-config 292,10128
-(defun lego-equal-module-filename 360,12177
-(defun lego-shell-compute-new-files-list 366,12452
-(defun lego-shell-mode-config 376,12835
-(defun lego-goals-mode-config 422,14488
+(define-derived-mode lego-goals-mode 162,4968
+(defun lego-count-undos 173,5394
+(defun lego-goal-command-p 193,6212
+(defun lego-find-and-forget 198,6383
+(defun lego-goal-hyp 240,8199
+(defun lego-state-preserving-p 249,8396
+(defvar lego-shell-current-line-width 265,9099
+(defun lego-shell-adjust-line-width 273,9406
+(defun lego-mode-config 292,10143
+(defun lego-equal-module-filename 360,12192
+(defun lego-shell-compute-new-files-list 366,12467
+(defun lego-shell-mode-config 376,12850
+(defun lego-goals-mode-config 423,14517
 
 lego/lego-syntax.el,600
 (defconst lego-keywords-goal 15,358
@@ -651,60 +653,84 @@ lego/lego-syntax.el,600
 (defvar lego-font-lock-keywords-199,3660
 (defun lego-init-syntax-table 110,4122
 
-phox/phox.el,597
+phox/phox.el,555
 (defcustom phox-prog-name 32,916
-(defcustom phox-sym-lock-enabled 37,1018
-(defcustom phox-web-page43,1127
-(defcustom phox-doc-dir49,1277
-(defcustom phox-lib-dir55,1424
-(defcustom phox-tags-program61,1567
-(defcustom phox-tags-doc67,1746
-(defcustom phox-etags73,1883
-(defpgdefault menu-entries94,2333
-(defun phox-config 108,2526
-(defun phox-shell-config 152,4450
-(define-derived-mode phox-mode 176,5312
-(define-derived-mode phox-shell-mode 192,5775
-(define-derived-mode phox-response-mode 197,5903
-(define-derived-mode phox-goals-mode 207,6264
-(defpgdefault completion-table230,7050
+(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,4341
+(define-derived-mode phox-mode 170,5203
+(define-derived-mode phox-shell-mode 186,5666
+(define-derived-mode phox-response-mode 191,5794
+(define-derived-mode phox-goals-mode 201,6155
+(defpgdefault completion-table224,6941
 
 phox/phox-extraction.el,383
-(defvar phox-prog-orig 17,605
-(defun phox-prog-flags-modify(19,673
-(defun phox-prog-flags-extract(48,1474
-(defun phox-prog-flags-erase(59,1764
-(defun phox-toggle-extraction(67,1960
-(defun phox-compile-theorem(79,2362
-(defun phox-compile-theorem-on-cursor(85,2587
-(defun phox-output 101,3065
-(defun phox-output-theorem 111,3277
-(defun phox-output-theorem-on-cursor(118,3576
-
-phox/phox-font.el,123
-(defconst phox-font-lock-keywords6,282
-(defconst phox-sym-lock-keywords-table65,2399
-(defun phox-sym-lock-start 88,2973
-
-phox/phox-fun.el,678
-(defun phox-init-syntax-table 67,2384
-(defvar phox-top-keywords83,2856
-(defvar phox-proof-keywords131,3311
-(defun phox-find-and-forget 172,3661
-(defun phox-assert-next-command-interactive 251,6059
-(defun phox-depend-theorem(269,6863
-(defun phox-eshow-extlist(278,7152
-(defun phox-flag-name(292,7749
-(defun phox-path(303,8051
-(defun phox-print-expression(314,8287
-(defun phox-print-sort-expression(327,8743
-(defun phox-priority-symbols-list(338,9055
-(defun phox-search-string(350,9427
-(defun phox-constraints(365,9952
-(defun phox-goals(376,10208
-(defvar phox-state-menu388,10417
-(defun phox-delete-symbol(413,11407
-(defun phox-delete-symbol-on-cursor(419,11615
+(defvar phox-prog-orig 19,619
+(defun phox-prog-flags-modify(21,687
+(defun phox-prog-flags-extract(50,1488
+(defun phox-prog-flags-erase(61,1778
+(defun phox-toggle-extraction(69,1974
+(defun phox-compile-theorem(81,2376
+(defun phox-compile-theorem-on-cursor(87,2601
+(defun phox-output 103,3079
+(defun phox-output-theorem 113,3291
+(defun phox-output-theorem-on-cursor(120,3590
+
+phox/phox-font.el,231
+(defvar phox-sym-lock-enabled 1,0
+(defvar phox-sym-lock-color 2,60
+(defvar phox-sym-lock-keywords 3,118
+(defconst phox-font-lock-keywords11,511
+(defconst phox-sym-lock-keywords-table70,2628
+(defun phox-sym-lock-start 93,3202
+
+phox/phox-fun.el,1659
+(defconst phox-forget-id-command 11,186
+(defconst phox-forget-proof-command 12,232
+(defconst phox-forget-new-elim-command 13,287
+(defconst phox-forget-new-intro-command 14,345
+(defconst phox-forget-new-equation-command 15,405
+(defconst phox-forget-close-def-command 16,471
+(defconst phox-comments-regexp 18,597
+(defconst phox-strict-comments-regexp 20,776
+(defconst phox-ident-regexp 21,941
+(defconst phox-inductive-option 22,1027
+(defconst phox-spaces-regexp 23,1079
+(defconst phox-sy-definition-regexp 24,1122
+(defconst phox-sy-inductive-regexp 28,1309
+(defconst phox-inductive-regexp 34,1522
+(defconst phox-data-regexp 40,1673
+(defconst phox-definition-regexp 46,1827
+(defconst phox-prove-claim-regexp 50,1971
+(defconst phox-new-elim-regexp 54,2077
+(defconst phox-new-intro-regexp 57,2196
+(defconst phox-new-rewrite-regexp 60,2317
+(defconst phox-new-equation-regexp 63,2442
+(defconst phox-close-def-regexp 66,2569
+(defun phox-init-syntax-table 71,2706
+(defvar phox-top-keywords87,3178
+(defvar phox-proof-keywords135,3633
+(defun phox-find-and-forget 176,3983
+(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive255,6381
+(defun phox-depend-theorem(274,7347
+(defun phox-eshow-extlist(283,7636
+(defun phox-flag-name(297,8233
+(defun phox-path(308,8535
+(defun phox-print-expression(319,8771
+(defun phox-print-sort-expression(332,9227
+(defun phox-priority-symbols-list(343,9539
+(defun phox-search-string(355,9911
+(defun phox-constraints(370,10436
+(defun phox-goals(381,10692
+(defvar phox-state-menu393,10901
+(defun phox-delete-symbol(418,11891
+(defun phox-delete-symbol-on-cursor(424,12099
 
 phox/phox-lang.el,323
 (defvar phox-lang9,306
@@ -718,64 +744,69 @@ phox/phox-lang.el,323
 (defun phox-lang-prove 52,1488
 (defun phox-lang-let 57,1622
 
-phox/phox-outline.el,70
-(defun phox-outline-level(34,1143
-(defun phox-setup-outline 48,1617
-
-phox/phox-pbrpm.el,512
-(defun phox-pbrpm-left-paren-p 27,1188
-(defun phox-pbrpm-right-paren-p 34,1391
-(defun phox-pbrpm-menu-from-string 42,1595
-(defun phox-pbrpm-rename-in-cmd 51,1927
-(defun phox-pbrpm-get-region-name 84,3175
-(defun  phox-pbrpm-escape-string 87,3302
-(defun phox-pbrpm-generate-menu 91,3437
-(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu298,10917
-(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p299,10981
-(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p300,11043
-
-phox/phox-sym-lock.el,1353
-(defvar phox-sym-lock-sym-count 36,1642
-(defvar phox-sym-lock-ext-start 39,1712
-(defvar phox-sym-lock-ext-end 41,1834
-(defvar phox-sym-lock-font-size 44,1953
-(defvar phox-sym-lock-keywords 49,2143
-(defvar phox-sym-lock-enabled 54,2319
-(defvar phox-sym-lock-color 59,2481
-(defvar phox-sym-lock-mouse-face 64,2699
-(defvar phox-sym-lock-mouse-face-enabled 69,2889
-(defconst phox-sym-lock-with-mule 74,3079
-(defun phox-sym-lock-gen-symbol 77,3163
-(defun phox-sym-lock-make-symbols-atomic 85,3465
-(defun phox-sym-lock-compute-font-size 112,4406
-(defvar phox-sym-lock-font-name150,5825
-(defun phox-sym-lock-set-foreground 192,7304
-(defun phox-sym-lock-translate-char 206,7913
-(defun phox-sym-lock-translate-char-or-string 214,8181
-(defun phox-sym-lock-remap-face 221,8408
-(defvar phox-sym-lock-clear-face241,9398
-(defun phox-sym-lock 253,9819
-(defun phox-sym-lock-rec 262,10223
-(defun phox-sym-lock-atom-face 268,10368
-(defun phox-sym-lock-pre-idle-hook-first 273,10664
-(defun phox-sym-lock-pre-idle-hook-last 281,11022
-(defun phox-sym-lock-enable 290,11397
-(defun phox-sym-lock-disable 303,11810
-(defun phox-sym-lock-mouse-face-enable 316,12228
-(defun phox-sym-lock-mouse-face-disable 323,12443
-(defun phox-sym-lock-font-lock-hook 330,12662
-(defun font-lock-set-defaults 345,13353
-(defun phox-sym-lock-patch-keywords 356,13717
+phox/phox-outline.el,254
+(defconst phox-outline-title-regexp 20,745
+(defconst phox-outline-section-regexp 21,810
+(defconst phox-outline-save-regexp 22,866
+(defconst phox-outline-heading-end-regexp 39,1409
+(defun phox-outline-level(45,1584
+(defun phox-setup-outline 59,2058
+
+phox/phox-pbrpm.el,513
+(defun phox-pbrpm-left-paren-p 39,1671
+(defun phox-pbrpm-right-paren-p 46,1874
+(defun phox-pbrpm-menu-from-string 54,2078
+(defun phox-pbrpm-rename-in-cmd 63,2410
+(defun phox-pbrpm-get-region-name 96,3658
+(defun  phox-pbrpm-escape-string 99,3785
+(defun phox-pbrpm-generate-menu 103,3920
+(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu310,11400
+(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p311,11464
+(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p312,11526
+
+phox/phox-sym-lock.el,1398
+(defcustom phox-sym-lock-enabled 19,871
+(defvar phox-sym-lock-sym-count 59,2452
+(defvar phox-sym-lock-ext-start 62,2522
+(defvar phox-sym-lock-ext-end 64,2644
+(defvar phox-sym-lock-font-size 67,2763
+(defvar phox-sym-lock-keywords 72,2953
+(defvar phox-sym-lock-enabled 77,3129
+(defvar phox-sym-lock-color 82,3291
+(defvar phox-sym-lock-mouse-face 87,3509
+(defvar phox-sym-lock-mouse-face-enabled 92,3699
+(defconst phox-sym-lock-with-mule 97,3889
+(defun phox-sym-lock-gen-symbol 100,3973
+(defun phox-sym-lock-make-symbols-atomic 108,4275
+(defun phox-sym-lock-compute-font-size 135,5216
+(defvar phox-sym-lock-font-name173,6635
+(defun phox-sym-lock-set-foreground 216,8233
+(defun phox-sym-lock-translate-char 230,8842
+(defun phox-sym-lock-translate-char-or-string 239,9159
+(defun phox-sym-lock-remap-face 246,9387
+(defvar phox-sym-lock-clear-face266,10375
+(defun phox-sym-lock 278,10794
+(defun phox-sym-lock-rec 287,11198
+(defun phox-sym-lock-atom-face 293,11343
+(defun phox-sym-lock-pre-idle-hook-first 298,11639
+(defun phox-sym-lock-pre-idle-hook-last 308,12044
+(defun phox-sym-lock-enable 317,12419
+(defun phox-sym-lock-disable 330,12830
+(defun phox-sym-lock-mouse-face-enable 343,13246
+(defun phox-sym-lock-mouse-face-disable 350,13461
+(defun phox-sym-lock-font-lock-hook 357,13680
+(defun font-lock-set-defaults 372,14371
+(defun phox-sym-lock-patch-keywords 384,14798
 
 phox/phox-tags.el,305
-(defun phox-tags-add-table(21,766
-(defun phox-tags-reset-table(30,1161
-(defun phox-tags-add-doc-table(35,1271
-(defun phox-tags-add-lib-table(41,1420
-(defun phox-tags-add-local-table(47,1555
-(defun phox-tags-create-local-table(53,1738
-(defun phox-complete-tag(64,1988
-(defvar phox-tags-menu71,2097
+(defun phox-tags-add-table(26,869
+(defun phox-tags-reset-table(35,1264
+(defun phox-tags-add-doc-table(40,1374
+(defun phox-tags-add-lib-table(46,1523
+(defun phox-tags-add-local-table(52,1658
+(defun phox-tags-create-local-table(58,1841
+(defun phox-complete-tag(69,2091
+(defvar phox-tags-menu76,2200
 
 plastic/plastic.el,2759
 (defcustom plastic-tags 29,608
@@ -825,24 +856,24 @@ plastic/plastic.el,2759
 (defun plastic-small-bar 517,17561
 (defun plastic-large-bar 519,17650
 (defun plastic-preprocessing 521,17788
-(defun plastic-all-ctxt 572,19569
-(defun plastic-send-one-undo 579,19738
-(defun plastic-minibuf-cmd 589,20044
-(defun plastic-minibuf 601,20516
-(defun plastic-synchro 608,20722
-(defun plastic-send-minibuf 613,20863
-(defun plastic-had-error 621,21171
-(defun plastic-reset-error 625,21346
-(defun plastic-call-if-no-error 628,21485
-(defun plastic-show-shell 633,21689
-(define-key plastic-keymap 638,21817
-(define-key plastic-keymap 639,21878
-(define-key plastic-keymap 640,21939
-(define-key plastic-keymap 641,21999
-(define-key plastic-keymap 642,22058
-(define-key plastic-keymap 643,22117
-(defalias 'proof-toolbar-command proof-toolbar-command653,22366
-(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd654,22417
+(defun plastic-all-ctxt 573,19591
+(defun plastic-send-one-undo 580,19760
+(defun plastic-minibuf-cmd 590,20066
+(defun plastic-minibuf 602,20538
+(defun plastic-synchro 609,20744
+(defun plastic-send-minibuf 614,20885
+(defun plastic-had-error 622,21193
+(defun plastic-reset-error 626,21368
+(defun plastic-call-if-no-error 629,21507
+(defun plastic-show-shell 634,21711
+(define-key plastic-keymap 639,21839
+(define-key plastic-keymap 640,21900
+(define-key plastic-keymap 641,21961
+(define-key plastic-keymap 642,22021
+(define-key plastic-keymap 643,22080
+(define-key plastic-keymap 644,22139
+(defalias 'proof-toolbar-command proof-toolbar-command654,22388
+(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd655,22439
 
 plastic/plastic-syntax.el,648
 (defconst plastic-keywords-goal 18,536
@@ -905,118 +936,118 @@ generic/pg-goals.el,285
 (defun pg-goals-display 77,2204
 (defun pg-goals-button-action 118,3508
 
-generic/pg-pbrpm.el,1805
-(defvar pg-pbrpm-use-buffer-menu 31,742
-(defvar pg-pbrpm-start-goal-regexp 34,864
-(defvar pg-pbrpm-start-goal-regexp-par-num 38,1021
-(defvar pg-pbrpm-end-goal-regexp 41,1144
-(defvar pg-pbrpm-start-hyp-regexp 45,1296
-(defvar pg-pbrpm-start-hyp-regexp-par-num 49,1457
-(defvar pg-pbrpm-start-concl-regexp 53,1664
-(defvar pg-pbrpm-auto-select-regexp 57,1828
-(defvar pg-pbrpm-buffer-menu 64,1989
-(defvar pg-pbrpm-spans 65,2023
-(defvar pg-pbrpm-goal-description 66,2051
-(defvar pg-pbrpm-windows-dialog-bug 67,2090
-(defvar pbrpm-menu-desc 68,2131
-(defun pg-pbrpm-erase-buffer-menu 70,2161
-(defun pg-pbrpm-menu-change-hook 77,2345
-(defun pg-pbrpm-create-reset-buffer-menu 95,2920
-(defun pg-pbrpm-analyse-goal-buffer 114,3762
-(defun pg-pbrpm-button-action 174,6160
-(defun pg-pbrpm-exists 181,6386
-(defun pg-pbrpm-eliminate-id 185,6498
-(defun pg-pbrpm-build-menu 193,6744
-(defun pg-pbrpm-setup-span 256,9064
-(defun pg-pbrpm-run-command 316,11379
-(defun pg-pbrpm-get-pos-info 345,12689
-(defun pg-pbrpm-get-region-info 387,13988
-(defun pg-pbrpm-auto-select-around-point 398,14400
-(defun pg-pbrpm-translate-position 413,14924
-(defun pg-pbrpm-process-click 421,15181
-(defvar pg-pbrpm-remember-region-selected-region 441,16206
-(defvar pg-pbrpm-regions-list 442,16260
-(defun pg-pbrpm-erase-regions-list 444,16296
-(defun pg-pbrpm-filter-regions-list 453,16604
-(defface pg-pbrpm-multiple-selection-face460,16867
-(defface pg-pbrpm-menu-input-face468,17069
-(defun pg-pbrpm-do-remember-region 476,17259
-(defun pg-pbrpm-remember-region-drag-up-hook 497,18107
-(defun pg-pbrpm-remember-region-click-hook 501,18278
-(defun pg-pbrpm-remember-region 506,18463
-(defun pg-pbrpm-process-region 520,19177
-(defun pg-pbrpm-process-regions-list 538,19906
-(defun pg-pbrpm-region-expression 542,20089
+generic/pg-pbrpm.el,1808
+(defvar pg-pbrpm-use-buffer-menu 41,1185
+(defvar pg-pbrpm-start-goal-regexp 44,1307
+(defvar pg-pbrpm-start-goal-regexp-par-num 48,1464
+(defvar pg-pbrpm-end-goal-regexp 51,1587
+(defvar pg-pbrpm-start-hyp-regexp 55,1739
+(defvar pg-pbrpm-start-hyp-regexp-par-num 59,1900
+(defvar pg-pbrpm-start-concl-regexp 63,2107
+(defvar pg-pbrpm-auto-select-regexp 67,2271
+(defvar pg-pbrpm-buffer-menu 74,2432
+(defvar pg-pbrpm-spans 75,2466
+(defvar pg-pbrpm-goal-description 76,2494
+(defvar pg-pbrpm-windows-dialog-bug 77,2533
+(defvar pbrpm-menu-desc 78,2574
+(defun pg-pbrpm-erase-buffer-menu 80,2604
+(defun pg-pbrpm-menu-change-hook 87,2788
+(defun pg-pbrpm-create-reset-buffer-menu 105,3363
+(defun pg-pbrpm-analyse-goal-buffer 124,4205
+(defun pg-pbrpm-button-action 184,6603
+(defun pg-pbrpm-exists 191,6829
+(defun pg-pbrpm-eliminate-id 195,6941
+(defun pg-pbrpm-build-menu 203,7187
+(defun pg-pbrpm-setup-span 266,9507
+(defun pg-pbrpm-run-command 326,11822
+(defun pg-pbrpm-get-pos-info 356,13149
+(defun pg-pbrpm-get-region-info 398,14448
+(defun pg-pbrpm-auto-select-around-point 409,14860
+(defun pg-pbrpm-translate-position 424,15384
+(defun pg-pbrpm-process-click 432,15641
+(defvar pg-pbrpm-remember-region-selected-region 452,16666
+(defvar pg-pbrpm-regions-list 453,16720
+(defun pg-pbrpm-erase-regions-list 455,16756
+(defun pg-pbrpm-filter-regions-list 464,17064
+(defface pg-pbrpm-multiple-selection-face471,17327
+(defface pg-pbrpm-menu-input-face479,17529
+(defun pg-pbrpm-do-remember-region 487,17719
+(defun pg-pbrpm-remember-region-drag-up-hook 508,18567
+(defun pg-pbrpm-remember-region-click-hook 512,18738
+(defun pg-pbrpm-remember-region 517,18923
+(defun pg-pbrpm-process-region 531,19637
+(defun pg-pbrpm-process-regions-list 549,20366
+(defun pg-pbrpm-region-expression 553,20549
 
 generic/pg-pgip.el,2931
-(defalias 'pg-pgip-debug pg-pgip-debug39,1033
-(defalias 'pg-pgip-error pg-pgip-error40,1074
-(defalias 'pg-pgip-warning pg-pgip-warning41,1109
-(defconst pg-pgip-version-supported 43,1159
-(defun pg-pgip-process-packet 47,1265
-(defvar pg-pgip-last-seen-id 57,1833
-(defvar pg-pgip-last-seen-seq 58,1867
-(defun pg-pgip-process-pgip 60,1903
-(defun pg-pgip-process-msg 79,2834
-(defvar pg-pgip-post-process-functions93,3404
-(defun pg-pgip-post-process 103,3892
-(defun pg-pgip-process-askpgip 119,4502
-(defun pg-pgip-process-usespgip 125,4706
-(defun pg-pgip-process-usespgml 129,4870
-(defun pg-pgip-process-pgmlconfig 133,5034
-(defun pg-pgip-process-proverinfo 149,5651
-(defun pg-pgip-process-hasprefs 166,6316
-(defun pg-pgip-haspref 180,6948
-(defun pg-pgip-process-prefval 197,7650
-(defun pg-pgip-process-guiconfig 224,8358
-(defvar proof-assistant-idtables 231,8475
-(defun pg-pgip-process-ids 234,8592
-(defun pg-complete-idtable-symbol 260,9664
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids265,9756
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids266,9812
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids267,9868
-(defun pg-pgip-process-idvalue 270,9926
-(defun pg-pgip-process-menuadd 282,10272
-(defun pg-pgip-process-menudel 285,10315
-(defun pg-pgip-process-ready 294,10547
-(defun pg-pgip-process-cleardisplay 297,10588
-(defun pg-pgip-process-proofstate 311,11045
-(defun pg-pgip-process-normalresponse 315,11122
-(defun pg-pgip-process-errorresponse 319,11252
-(defun pg-pgip-process-scriptinsert 323,11381
-(defun pg-pgip-process-metainforesponse 328,11515
-(defun pg-pgip-file-of-url 337,11755
-(defun pg-pgip-process-informfileloaded 342,11890
-(defun pg-pgip-process-informfileretracted 348,12122
-(defun pg-pgip-process-brokerstatus 361,12569
-(defun pg-pgip-process-proveravailmsg 364,12617
-(defun pg-pgip-process-newprovermsg 367,12667
-(defun pg-pgip-process-proverstatusmsg 370,12715
-(defvar pg-pgip-srcids 379,12961
-(defun pg-pgip-process-newfile 383,13068
-(defun pg-pgip-process-filestatus 399,13650
-(defun pg-pgip-process-newobj 419,14304
-(defun pg-pgip-process-delobj 422,14346
-(defun pg-pgip-process-objectstatus 425,14388
-(defun pg-pgip-process-parsescript 439,14740
-(defun pg-pgip-get-pgiptype 462,15614
-(defun pg-pgip-default-for 482,16406
-(defun pg-pgip-subst-for 495,16801
-(defun pg-pgip-interpret-value 507,17144
-(defun pg-pgip-interpret-choice 525,17825
-(defun pg-pgip-string-of-command 556,18842
-(defconst pg-pgip-id573,19603
-(defvar pg-pgip-refseq 579,19883
-(defvar pg-pgip-refid 581,19980
-(defvar pg-pgip-seq 584,20072
-(defun pg-pgip-assemble-packet 586,20136
-(defun pg-pgip-issue 604,20947
-(defun pg-pgip-maybe-askpgip 621,21559
-(defun pg-pgip-askprefs 627,21750
-(defun pg-pgip-askids 631,21864
-(defun pg-pgip-reset 644,22152
-(defconst pg-pgip-start-element-regexp 675,22850
-(defconst pg-pgip-end-element-regexp 676,22902
+(defalias 'pg-pgip-debug pg-pgip-debug38,1032
+(defalias 'pg-pgip-error pg-pgip-error39,1073
+(defalias 'pg-pgip-warning pg-pgip-warning40,1108
+(defconst pg-pgip-version-supported 42,1158
+(defun pg-pgip-process-packet 46,1264
+(defvar pg-pgip-last-seen-id 56,1832
+(defvar pg-pgip-last-seen-seq 57,1866
+(defun pg-pgip-process-pgip 59,1902
+(defun pg-pgip-process-msg 78,2833
+(defvar pg-pgip-post-process-functions92,3403
+(defun pg-pgip-post-process 102,3891
+(defun pg-pgip-process-askpgip 118,4501
+(defun pg-pgip-process-usespgip 124,4705
+(defun pg-pgip-process-usespgml 128,4869
+(defun pg-pgip-process-pgmlconfig 132,5033
+(defun pg-pgip-process-proverinfo 148,5650
+(defun pg-pgip-process-hasprefs 165,6315
+(defun pg-pgip-haspref 179,6947
+(defun pg-pgip-process-prefval 196,7649
+(defun pg-pgip-process-guiconfig 223,8357
+(defvar proof-assistant-idtables 230,8474
+(defun pg-pgip-process-ids 233,8591
+(defun pg-complete-idtable-symbol 259,9663
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids264,9755
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids265,9811
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids266,9867
+(defun pg-pgip-process-idvalue 269,9925
+(defun pg-pgip-process-menuadd 281,10271
+(defun pg-pgip-process-menudel 284,10314
+(defun pg-pgip-process-ready 293,10546
+(defun pg-pgip-process-cleardisplay 296,10587
+(defun pg-pgip-process-proofstate 310,11044
+(defun pg-pgip-process-normalresponse 314,11121
+(defun pg-pgip-process-errorresponse 318,11251
+(defun pg-pgip-process-scriptinsert 322,11380
+(defun pg-pgip-process-metainforesponse 327,11514
+(defun pg-pgip-file-of-url 336,11754
+(defun pg-pgip-process-informfileloaded 341,11889
+(defun pg-pgip-process-informfileretracted 347,12121
+(defun pg-pgip-process-brokerstatus 360,12568
+(defun pg-pgip-process-proveravailmsg 363,12616
+(defun pg-pgip-process-newprovermsg 366,12666
+(defun pg-pgip-process-proverstatusmsg 369,12714
+(defvar pg-pgip-srcids 378,12960
+(defun pg-pgip-process-newfile 382,13067
+(defun pg-pgip-process-filestatus 398,13649
+(defun pg-pgip-process-newobj 418,14303
+(defun pg-pgip-process-delobj 421,14345
+(defun pg-pgip-process-objectstatus 424,14387
+(defun pg-pgip-process-parsescript 438,14739
+(defun pg-pgip-get-pgiptype 461,15613
+(defun pg-pgip-default-for 481,16405
+(defun pg-pgip-subst-for 494,16800
+(defun pg-pgip-interpret-value 506,17143
+(defun pg-pgip-interpret-choice 524,17824
+(defun pg-pgip-string-of-command 555,18841
+(defconst pg-pgip-id572,19602
+(defvar pg-pgip-refseq 578,19882
+(defvar pg-pgip-refid 580,19979
+(defvar pg-pgip-seq 583,20071
+(defun pg-pgip-assemble-packet 585,20135
+(defun pg-pgip-issue 603,20946
+(defun pg-pgip-maybe-askpgip 620,21558
+(defun pg-pgip-askprefs 626,21749
+(defun pg-pgip-askids 630,21863
+(defun pg-pgip-reset 643,22151
+(defconst pg-pgip-start-element-regexp 674,22849
+(defconst pg-pgip-end-element-regexp 675,22901
 
 generic/pg-response.el,1291
 (deflocal pg-response-eagerly-raise 32,787
@@ -1057,87 +1088,85 @@ generic/pg-thymodes.el,152
 (defun pg-modesym 82,2548
 (defun pg-modesymval 86,2662
 
-generic/pg-user.el,3435
-(defun proof-script-next-command-advance 35,887
-(defun proof-script-new-command-advance 48,1366
-(defun proof-maybe-follow-locked-end 91,3108
-(defun proof-goto-command-start 118,3937
-(defun proof-goto-command-end 141,4877
-(defun proof-goto-point 164,5402
-(defun proof-assert-next-command-interactive 178,5836
-(defun proof-assert-until-point-interactive 191,6361
-(defun proof-process-buffer 197,6591
-(defun proof-undo-last-successful-command 212,6968
-(defun proof-undo-and-delete-last-successful-command 217,7130
-(defun proof-undo-last-successful-command-1 230,7684
-(defun proof-retract-buffer 247,8296
-(defun proof-retract-current-goal 256,8580
-(defun proof-mouse-goto-point 275,9100
-(defvar proof-minibuffer-history 290,9376
-(defun proof-minibuffer-cmd 293,9471
-(defun proof-frob-locked-end 337,11093
-(defmacro proof-if-setting-configured 398,13017
-(defmacro proof-define-assistant-command 406,13286
-(defmacro proof-define-assistant-command-witharg 419,13741
-(defun proof-issue-new-command 439,14563
-(defun proof-cd-sync 485,16060
-(defun proof-electric-terminator-enable 539,17780
-(defun proof-process-electric-terminator 547,18070
-(defun proof-electric-terminator 582,19409
-(defun proof-add-completions 604,20055
-(defun proof-script-complete 629,20962
-(defun pg-copy-span-contents 643,21271
-(defun pg-numth-span-higher-or-lower 660,21829
-(defun pg-control-span-of 686,22575
-(defun pg-move-span-contents 692,22779
-(defun pg-fixup-children-spans 744,24955
-(defun pg-move-region-down 754,25212
-(defun pg-move-region-up 763,25505
-(defun proof-forward-command 793,26333
-(defun proof-backward-command 814,27054
-(defun pg-pos-for-event 836,27398
-(defun pg-span-for-event 842,27619
-(defun pg-span-context-menu 846,27763
-(defun pg-toggle-visibility 861,28218
-(defun pg-create-in-span-context-menu 871,28540
-(defun pg-span-undo 901,29749
-(defun pg-goals-buffers-hint 947,31151
-(defun pg-slow-fontify-tracing-hint 951,31333
-(defun pg-response-buffers-hint 955,31504
-(defun pg-jump-to-end-hint 965,31866
-(defun pg-processing-complete-hint 969,31995
-(defun pg-next-error-hint 986,32694
-(defun pg-hint 991,32846
-(defun pg-identifier-under-mouse-query 1007,33436
-(defun pg-identifier-near-point-query 1016,33679
-(defvar proof-query-identifier-collection 1041,34395
-(defvar proof-query-identifier-history 1042,34442
-(defun proof-query-identifier 1044,34487
-(defun pg-identifier-query 1054,34756
-(defun proof-imenu-enable 1085,35834
-(defvar pg-input-ring 1116,36895
-(defvar pg-input-ring-index 1119,36952
-(defvar pg-stored-incomplete-input 1122,37024
-(defun pg-previous-input 1125,37127
-(defun pg-next-input 1139,37584
-(defun pg-delete-input 1144,37706
-(defun pg-get-old-input 1157,38044
-(defun pg-restore-input 1171,38435
-(defun pg-search-start 1182,38725
-(defun pg-regexp-arg 1194,39217
-(defun pg-search-arg 1206,39665
-(defun pg-previous-matching-input-string-position 1220,40082
-(defun pg-previous-matching-input 1247,41247
-(defun pg-next-matching-input 1266,42097
-(defvar pg-matching-input-from-input-string 1274,42480
-(defun pg-previous-matching-input-from-input 1278,42594
-(defun pg-next-matching-input-from-input 1296,43359
-(defun pg-add-to-input-history 1307,43738
-(defun pg-remove-from-input-history 1319,44191
-(defun  pg-clear-input-ring 1330,44571
-(define-key proof-mode-map 1344,44921
-(define-key proof-mode-map 1345,44981
-(defun pg-protected-undo 1347,45053
+generic/pg-user.el,3331
+(defun proof-script-new-command-advance 41,1156
+(defun proof-maybe-follow-locked-end 84,2897
+(defun proof-goto-command-start 111,3726
+(defun proof-goto-command-end 134,4666
+(defun proof-goto-point 157,5191
+(defun proof-assert-next-command-interactive 171,5625
+(defun proof-assert-until-point-interactive 184,6150
+(defun proof-process-buffer 190,6380
+(defun proof-undo-last-successful-command 205,6757
+(defun proof-undo-and-delete-last-successful-command 210,6919
+(defun proof-undo-last-successful-command-1 223,7473
+(defun proof-retract-buffer 240,8085
+(defun proof-retract-current-goal 249,8369
+(defun proof-mouse-goto-point 268,8889
+(defvar proof-minibuffer-history 283,9165
+(defun proof-minibuffer-cmd 286,9260
+(defun proof-frob-locked-end 330,10882
+(defmacro proof-if-setting-configured 391,12806
+(defmacro proof-define-assistant-command 399,13075
+(defmacro proof-define-assistant-command-witharg 412,13530
+(defun proof-issue-new-command 432,14352
+(defun proof-cd-sync 478,15849
+(defun proof-electric-terminator-enable 532,17569
+(defun proof-electric-terminator 540,17859
+(defun proof-add-completions 562,18504
+(defun proof-script-complete 587,19411
+(defun pg-copy-span-contents 601,19720
+(defun pg-numth-span-higher-or-lower 618,20278
+(defun pg-control-span-of 644,21024
+(defun pg-move-span-contents 650,21228
+(defun pg-fixup-children-spans 702,23404
+(defun pg-move-region-down 712,23661
+(defun pg-move-region-up 721,23954
+(defun proof-forward-command 751,24782
+(defun proof-backward-command 772,25503
+(defun pg-pos-for-event 794,25847
+(defun pg-span-for-event 800,26068
+(defun pg-span-context-menu 804,26212
+(defun pg-toggle-visibility 819,26667
+(defun pg-create-in-span-context-menu 829,26989
+(defun pg-span-undo 859,28198
+(defun pg-goals-buffers-hint 905,29600
+(defun pg-slow-fontify-tracing-hint 909,29782
+(defun pg-response-buffers-hint 913,29953
+(defun pg-jump-to-end-hint 923,30315
+(defun pg-processing-complete-hint 927,30444
+(defun pg-next-error-hint 944,31143
+(defun pg-hint 949,31295
+(defun pg-identifier-under-mouse-query 965,31885
+(defun pg-identifier-near-point-query 974,32128
+(defvar proof-query-identifier-collection 999,32844
+(defvar proof-query-identifier-history 1000,32891
+(defun proof-query-identifier 1002,32936
+(defun pg-identifier-query 1012,33205
+(defun proof-imenu-enable 1043,34283
+(defvar pg-input-ring 1079,35605
+(defvar pg-input-ring-index 1082,35662
+(defvar pg-stored-incomplete-input 1085,35734
+(defun pg-previous-input 1088,35837
+(defun pg-next-input 1102,36294
+(defun pg-delete-input 1107,36416
+(defun pg-get-old-input 1120,36754
+(defun pg-restore-input 1134,37145
+(defun pg-search-start 1145,37435
+(defun pg-regexp-arg 1157,37927
+(defun pg-search-arg 1169,38375
+(defun pg-previous-matching-input-string-position 1183,38792
+(defun pg-previous-matching-input 1210,39957
+(defun pg-next-matching-input 1229,40807
+(defvar pg-matching-input-from-input-string 1237,41190
+(defun pg-previous-matching-input-from-input 1241,41304
+(defun pg-next-matching-input-from-input 1259,42069
+(defun pg-add-to-input-history 1270,42448
+(defun pg-remove-from-input-history 1282,42901
+(defun  pg-clear-input-ring 1293,43281
+(define-key proof-mode-map 1307,43631
+(define-key proof-mode-map 1308,43691
+(defun pg-protected-undo 1310,43763
 
 generic/pg-vars.el,1452
 (defvar proof-assistant-cusgrp 22,382
@@ -1210,14 +1239,14 @@ generic/pg-xml.el,1177
 (defun pg-pgip-get-pgmltext 223,7251
 
 generic/proof-autoloads.el,45
-(defsubst proof-shell-live-buffer 636,20899
+(defsubst proof-shell-live-buffer 636,21159
 
 generic/proof-auxmodes.el,149
 (defun proof-mmm-support-available 20,489
 (defun proof-maths-menu-support-available 44,1100
 (defun proof-unicode-tokens-support-available 58,1517
 
-generic/proof-config.el,7858
+generic/proof-config.el,7905
 (defgroup prover-config 80,2633
 (defcustom proof-guess-command-line 98,3483
 (defcustom proof-assistant-home-page 113,3978
@@ -1271,109 +1300,110 @@ generic/proof-config.el,7858
 (defcustom pg-topterm-goalhyplit-fn 640,24872
 (defcustom proof-kill-goal-command 652,25407
 (defcustom proof-undo-n-times-cmd 666,25911
-(defcustom proof-nested-goals-history-p 680,26459
-(defcustom proof-arbitrary-undo-positions 689,26796
-(defcustom proof-state-preserving-p 703,27376
-(defcustom proof-activate-scripting-hook 713,27848
-(defcustom proof-deactivate-scripting-hook 732,28629
-(defcustom proof-script-evaluate-elisp-comment-regexp 741,28959
-(defcustom proof-indent 759,29545
-(defcustom proof-indent-hang 764,29652
-(defcustom proof-indent-enclose-offset 769,29778
-(defcustom proof-indent-open-offset 774,29920
-(defcustom proof-indent-close-offset 779,30057
-(defcustom proof-indent-any-regexp 784,30195
-(defcustom proof-indent-inner-regexp 789,30355
-(defcustom proof-indent-enclose-regexp 794,30509
-(defcustom proof-indent-open-regexp 799,30663
-(defcustom proof-indent-close-regexp 804,30815
-(defcustom proof-script-font-lock-keywords 810,30969
-(defcustom proof-script-syntax-table-entries 818,31321
-(defcustom proof-script-span-context-menu-extensions 836,31717
-(defgroup proof-shell 862,32475
-(defcustom proof-prog-name 872,32645
-(defcustom proof-shell-auto-terminate-commands 883,33065
-(defcustom proof-shell-pre-sync-init-cmd 892,33466
-(defcustom proof-shell-init-cmd 906,34024
-(defcustom proof-shell-init-hook 918,34553
-(defcustom proof-shell-restart-cmd 923,34692
-(defcustom proof-shell-quit-cmd 928,34847
-(defcustom proof-shell-quit-timeout 933,35014
-(defcustom proof-shell-cd-cmd 943,35464
-(defcustom proof-shell-start-silent-cmd 960,36135
-(defcustom proof-shell-stop-silent-cmd 969,36511
-(defcustom proof-shell-silent-threshold 978,36846
-(defcustom  proof-shell-inform-file-processed-cmd 986,37180
-(defcustom  proof-shell-inform-file-retracted-cmd 1007,38108
-(defcustom proof-auto-multiple-files 1035,39380
-(defcustom proof-cannot-reopen-processed-files 1050,40101
-(defcustom proof-shell-require-command-regexp 1064,40767
-(defcustom proof-done-advancing-require-function 1075,41229
-(defcustom proof-shell-annotated-prompt-regexp 1087,41589
-(defcustom proof-shell-error-regexp 1102,42154
-(defcustom proof-shell-truncate-before-error 1122,42956
-(defcustom pg-next-error-regexp 1136,43495
-(defcustom pg-next-error-filename-regexp 1151,44104
-(defcustom pg-next-error-extract-filename 1175,45137
-(defcustom proof-shell-interrupt-regexp 1182,45380
-(defcustom proof-shell-proof-completed-regexp 1196,45975
-(defcustom proof-shell-clear-response-regexp 1209,46483
-(defcustom proof-shell-clear-goals-regexp 1221,46935
-(defcustom proof-shell-start-goals-regexp 1233,47381
-(defcustom proof-shell-end-goals-regexp 1241,47748
-(defcustom proof-shell-eager-annotation-start 1255,48323
-(defcustom proof-shell-eager-annotation-start-length 1278,49342
-(defcustom proof-shell-eager-annotation-end 1289,49768
-(defcustom proof-shell-strip-output-markup 1305,50443
-(defcustom proof-shell-assumption-regexp 1314,50828
-(defcustom proof-shell-process-file 1324,51232
-(defcustom proof-shell-retract-files-regexp 1350,52310
-(defcustom proof-shell-compute-new-files-list 1363,52798
-(defcustom pg-special-char-regexp 1378,53367
-(defcustom proof-shell-set-elisp-variable-regexp 1383,53511
-(defcustom proof-shell-match-pgip-cmd 1421,55177
-(defcustom proof-shell-issue-pgip-cmd 1435,55659
-(defcustom proof-use-pgip-askprefs 1440,55824
-(defcustom proof-shell-query-dependencies-cmd 1448,56171
-(defcustom proof-shell-theorem-dependency-list-regexp 1455,56431
-(defcustom proof-shell-theorem-dependency-list-split 1471,57091
-(defcustom proof-shell-show-dependency-cmd 1480,57514
-(defcustom proof-shell-trace-output-regexp 1502,58420
-(defcustom proof-shell-thms-output-regexp 1520,59015
-(defcustom proof-tokens-activate-command 1533,59398
-(defcustom proof-tokens-deactivate-command 1540,59638
-(defcustom proof-tokens-extra-modes 1547,59883
-(defcustom proof-shell-unicode 1562,60388
-(defcustom proof-shell-filename-escapes 1571,60778
-(defcustom proof-shell-process-connection-type1588,61458
-(defcustom proof-shell-strip-crs-from-input 1611,62462
-(defcustom proof-shell-strip-crs-from-output 1623,62945
-(defcustom proof-shell-insert-hook 1631,63313
-(defcustom proof-shell-handle-delayed-output-hook1669,65173
-(defcustom proof-shell-handle-error-or-interrupt-hook1675,65388
-(defcustom proof-shell-pre-interrupt-hook1693,66134
-(defcustom proof-shell-handle-output-system-specific 1701,66405
-(defcustom proof-state-change-hook 1724,67381
-(defcustom proof-shell-syntax-table-entries 1734,67774
-(defgroup proof-goals 1752,68145
-(defcustom pg-subterm-first-special-char 1757,68266
-(defcustom pg-subterm-anns-use-stack 1765,68578
-(defcustom pg-goals-change-goal 1774,68877
-(defcustom pbp-goal-command 1779,68993
-(defcustom pbp-hyp-command 1784,69149
-(defcustom pg-subterm-help-cmd 1789,69311
-(defcustom pg-goals-error-regexp 1796,69547
-(defcustom proof-shell-result-start 1801,69707
-(defcustom proof-shell-result-end 1807,69941
-(defcustom pg-subterm-start-char 1813,70154
-(defcustom pg-subterm-sep-char 1827,70739
-(defcustom pg-subterm-end-char 1833,70918
-(defcustom pg-topterm-regexp 1839,71075
-(defcustom proof-goals-font-lock-keywords 1854,71675
-(defcustom proof-response-font-lock-keywords 1862,72034
-(defcustom proof-shell-font-lock-keywords 1870,72396
-(defcustom pg-before-fontify-output-hook 1881,72911
-(defcustom pg-after-fontify-output-hook 1889,73272
+(defcustom proof-nested-goals-history-p 680,26448
+(defcustom proof-arbitrary-undo-positions 689,26785
+(defcustom proof-state-preserving-p 703,27365
+(defcustom proof-activate-scripting-hook 713,27837
+(defcustom proof-deactivate-scripting-hook 732,28618
+(defcustom proof-script-evaluate-elisp-comment-regexp 741,28948
+(defcustom proof-indent 759,29534
+(defcustom proof-indent-hang 764,29641
+(defcustom proof-indent-enclose-offset 769,29767
+(defcustom proof-indent-open-offset 774,29909
+(defcustom proof-indent-close-offset 779,30046
+(defcustom proof-indent-any-regexp 784,30184
+(defcustom proof-indent-inner-regexp 789,30344
+(defcustom proof-indent-enclose-regexp 794,30498
+(defcustom proof-indent-open-regexp 799,30652
+(defcustom proof-indent-close-regexp 804,30804
+(defcustom proof-script-font-lock-keywords 810,30958
+(defcustom proof-script-syntax-table-entries 818,31310
+(defcustom proof-script-span-context-menu-extensions 836,31706
+(defgroup proof-shell 862,32464
+(defcustom proof-prog-name 872,32634
+(defcustom proof-shell-auto-terminate-commands 883,33054
+(defcustom proof-shell-pre-sync-init-cmd 892,33455
+(defcustom proof-shell-init-cmd 906,34013
+(defcustom proof-shell-init-hook 918,34542
+(defcustom proof-shell-restart-cmd 923,34681
+(defcustom proof-shell-quit-cmd 928,34836
+(defcustom proof-shell-quit-timeout 933,35003
+(defcustom proof-shell-cd-cmd 943,35453
+(defcustom proof-shell-start-silent-cmd 960,36124
+(defcustom proof-shell-stop-silent-cmd 969,36500
+(defcustom proof-shell-silent-threshold 978,36835
+(defcustom  proof-shell-inform-file-processed-cmd 986,37169
+(defcustom  proof-shell-inform-file-retracted-cmd 1007,38097
+(defcustom proof-auto-multiple-files 1035,39369
+(defcustom proof-cannot-reopen-processed-files 1050,40090
+(defcustom proof-shell-require-command-regexp 1064,40756
+(defcustom proof-done-advancing-require-function 1075,41218
+(defcustom proof-shell-annotated-prompt-regexp 1087,41578
+(defcustom proof-shell-error-regexp 1102,42143
+(defcustom proof-shell-truncate-before-error 1122,42945
+(defcustom pg-next-error-regexp 1136,43484
+(defcustom pg-next-error-filename-regexp 1151,44093
+(defcustom pg-next-error-extract-filename 1175,45126
+(defcustom proof-shell-interrupt-regexp 1182,45369
+(defcustom proof-shell-proof-completed-regexp 1196,45964
+(defcustom proof-shell-clear-response-regexp 1209,46472
+(defcustom proof-shell-clear-goals-regexp 1221,46924
+(defcustom proof-shell-start-goals-regexp 1233,47370
+(defcustom proof-shell-end-goals-regexp 1241,47737
+(defcustom proof-shell-eager-annotation-start 1255,48312
+(defcustom proof-shell-eager-annotation-start-length 1278,49331
+(defcustom proof-shell-eager-annotation-end 1289,49757
+(defcustom proof-shell-strip-output-markup 1305,50432
+(defcustom proof-shell-assumption-regexp 1314,50817
+(defcustom proof-shell-process-file 1324,51221
+(defcustom proof-shell-retract-files-regexp 1350,52299
+(defcustom proof-shell-compute-new-files-list 1363,52787
+(defcustom pg-special-char-regexp 1378,53356
+(defcustom proof-shell-set-elisp-variable-regexp 1383,53500
+(defcustom proof-shell-match-pgip-cmd 1421,55166
+(defcustom proof-shell-issue-pgip-cmd 1435,55648
+(defcustom proof-use-pgip-askprefs 1440,55813
+(defcustom proof-shell-query-dependencies-cmd 1448,56160
+(defcustom proof-shell-theorem-dependency-list-regexp 1455,56420
+(defcustom proof-shell-theorem-dependency-list-split 1471,57080
+(defcustom proof-shell-show-dependency-cmd 1480,57503
+(defcustom proof-shell-trace-output-regexp 1502,58409
+(defcustom proof-shell-thms-output-regexp 1520,59004
+(defcustom proof-tokens-activate-command 1533,59387
+(defcustom proof-tokens-deactivate-command 1540,59627
+(defcustom proof-tokens-extra-modes 1547,59872
+(defcustom proof-shell-unicode 1562,60377
+(defcustom proof-shell-filename-escapes 1571,60767
+(defcustom proof-shell-process-connection-type1588,61447
+(defcustom proof-shell-strip-crs-from-input 1611,62451
+(defcustom proof-shell-strip-crs-from-output 1623,62934
+(defcustom proof-shell-insert-hook 1631,63302
+(defcustom proof-script-preprocess 1672,65262
+(defcustom proof-shell-handle-delayed-output-hook1678,65413
+(defcustom proof-shell-handle-error-or-interrupt-hook1684,65628
+(defcustom proof-shell-pre-interrupt-hook1702,66374
+(defcustom proof-shell-handle-output-system-specific 1710,66645
+(defcustom proof-state-change-hook 1733,67621
+(defcustom proof-shell-syntax-table-entries 1743,68014
+(defgroup proof-goals 1761,68385
+(defcustom pg-subterm-first-special-char 1766,68506
+(defcustom pg-subterm-anns-use-stack 1774,68818
+(defcustom pg-goals-change-goal 1783,69117
+(defcustom pbp-goal-command 1788,69233
+(defcustom pbp-hyp-command 1793,69389
+(defcustom pg-subterm-help-cmd 1798,69551
+(defcustom pg-goals-error-regexp 1805,69787
+(defcustom proof-shell-result-start 1810,69947
+(defcustom proof-shell-result-end 1816,70181
+(defcustom pg-subterm-start-char 1822,70394
+(defcustom pg-subterm-sep-char 1836,70979
+(defcustom pg-subterm-end-char 1842,71158
+(defcustom pg-topterm-regexp 1848,71315
+(defcustom proof-goals-font-lock-keywords 1863,71915
+(defcustom proof-response-font-lock-keywords 1871,72274
+(defcustom proof-shell-font-lock-keywords 1879,72636
+(defcustom pg-before-fontify-output-hook 1890,73151
+(defcustom pg-after-fontify-output-hook 1898,73512
 
 generic/proof-depends.el,824
 (defvar proof-thm-names-of-files 23,622
@@ -1447,64 +1477,63 @@ generic/proof-indent.el,219
 (defun proof-indent-line 76,2611
 
 generic/proof-maths-menu.el,83
-(defun proof-maths-menu-set-global 30,936
-(defun proof-maths-menu-enable 44,1387
-
-generic/proof-menu.el,2073
-(defvar proof-display-some-buffers-count 29,665
-(defun proof-display-some-buffers 31,710
-(defun proof-menu-define-keys 90,2906
-(defun proof-menu-define-main 149,5772
-(defvar proof-menu-favourites 158,5957
-(defvar proof-menu-settings 161,6064
-(defun proof-menu-define-specific 165,6153
-(defun proof-assistant-menu-update 208,7414
-(defvar proof-help-menu222,7847
-(defvar proof-show-hide-menu230,8117
-(defvar proof-buffer-menu239,8430
-(defun proof-retract-on-edit-toggle 302,10740
-(defun proof-keep-response-history 309,10916
-(defconst proof-quick-opts-menu317,11226
-(defun proof-quick-opts-vars 486,18144
-(defun proof-quick-opts-changed-from-defaults-p 515,19004
-(defun proof-quick-opts-changed-from-saved-p 519,19109
-(defun proof-quick-opts-save 530,19460
-(defun proof-quick-opts-reset 535,19628
-(defconst proof-config-menu547,19896
-(defconst proof-advanced-menu554,20075
-(defvar proof-menu567,20510
-(defun proof-main-menu 576,20792
-(defun proof-aux-menu 587,21058
-(defun proof-menu-define-favourites-menu 603,21404
-(defun proof-def-favourite 623,22053
-(defvar proof-make-favourite-cmd-history 646,23027
-(defvar proof-make-favourite-menu-history 649,23112
-(defun proof-save-favourites 652,23198
-(defun proof-del-favourite 657,23346
-(defun proof-read-favourite 674,23902
-(defun proof-add-favourite 698,24678
-(defun proof-menu-define-settings-menu 725,25723
-(defun proof-menu-entry-name 758,26844
-(defun proof-menu-entry-for-setting 768,27194
-(defun proof-settings-vars 787,27726
-(defun proof-settings-changed-from-defaults-p 792,27903
-(defun proof-settings-changed-from-saved-p 796,28009
-(defun proof-settings-save 800,28112
-(defun proof-settings-reset 805,28279
-(defun proof-assistant-invisible-command-ifposs 810,28442
-(defun proof-maybe-askprefs 832,29412
-(defun proof-assistant-settings-cmd 838,29604
-(defvar proof-assistant-format-table855,30259
-(defun proof-assistant-format-bool 863,30627
-(defun proof-assistant-format-int 866,30740
-(defun proof-assistant-format-string 869,30832
-(defun proof-assistant-format 872,30930
+(defun proof-maths-menu-set-global 30,942
+(defun proof-maths-menu-enable 44,1393
+
+generic/proof-menu.el,2026
+(defvar proof-display-some-buffers-count 35,801
+(defun proof-display-some-buffers 37,846
+(defun proof-menu-define-keys 94,2986
+(defun proof-menu-define-main 153,5852
+(defvar proof-menu-favourites 162,6037
+(defvar proof-menu-settings 165,6144
+(defun proof-menu-define-specific 169,6233
+(defun proof-assistant-menu-update 212,7494
+(defvar proof-help-menu226,7927
+(defvar proof-show-hide-menu234,8197
+(defvar proof-buffer-menu243,8510
+(defun proof-keep-response-history 305,10779
+(defconst proof-quick-opts-menu313,11089
+(defun proof-quick-opts-vars 496,18562
+(defun proof-quick-opts-changed-from-defaults-p 525,19422
+(defun proof-quick-opts-changed-from-saved-p 529,19527
+(defun proof-quick-opts-save 540,19878
+(defun proof-quick-opts-reset 545,20046
+(defconst proof-config-menu557,20314
+(defconst proof-advanced-menu564,20493
+(defvar proof-menu577,20928
+(defun proof-main-menu 586,21210
+(defun proof-aux-menu 597,21476
+(defun proof-menu-define-favourites-menu 613,21822
+(defun proof-def-favourite 633,22471
+(defvar proof-make-favourite-cmd-history 656,23445
+(defvar proof-make-favourite-menu-history 659,23530
+(defun proof-save-favourites 662,23616
+(defun proof-del-favourite 667,23764
+(defun proof-read-favourite 684,24320
+(defun proof-add-favourite 708,25096
+(defun proof-menu-define-settings-menu 735,26141
+(defun proof-menu-entry-name 768,27262
+(defun proof-menu-entry-for-setting 778,27612
+(defun proof-settings-vars 797,28144
+(defun proof-settings-changed-from-defaults-p 802,28321
+(defun proof-settings-changed-from-saved-p 806,28427
+(defun proof-settings-save 810,28530
+(defun proof-settings-reset 815,28697
+(defun proof-assistant-invisible-command-ifposs 820,28860
+(defun proof-maybe-askprefs 842,29830
+(defun proof-assistant-settings-cmd 848,30022
+(defvar proof-assistant-format-table865,30677
+(defun proof-assistant-format-bool 873,31045
+(defun proof-assistant-format-int 876,31158
+(defun proof-assistant-format-string 879,31250
+(defun proof-assistant-format 882,31348
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 39,1466
 (defun proof-mmm-enable 54,2005
 
-generic/proof-script.el,5381
+generic/proof-script.el,5552
 (deflocal proof-active-buffer-fake-minor-mode 44,1308
 (deflocal proof-script-buffer-file-name 47,1434
 (deflocal pg-script-portions 54,1844
@@ -1515,196 +1544,197 @@ generic/proof-script.el,5381
 (deflocal proof-queue-span 116,3995
 (deflocal proof-overlay-arrow 125,4481
 (defun proof-span-give-warning 131,4608
-(defun proof-span-read-only 136,4757
-(defun proof-strict-read-only 145,5130
-(defsubst proof-set-queue-endpoints 155,5508
-(defun proof-set-overlay-arrow 159,5649
-(defsubst proof-set-locked-endpoints 170,5987
-(defsubst proof-detach-queue 175,6163
-(defsubst proof-detach-locked 180,6302
-(defsubst proof-set-queue-start 187,6527
-(defsubst proof-set-locked-end 191,6653
-(defsubst proof-set-queue-end 203,7123
-(defun proof-init-segmentation 214,7420
-(defun proof-colour-locked 247,8882
-(defun proof-restart-buffers 258,9314
-(defun proof-script-buffers-with-spans 279,10065
-(defun proof-script-remove-all-spans-and-deactivate 289,10421
-(defun proof-script-clear-queue-spans 293,10611
-(defun proof-script-delete-spans 304,11001
-(defun proof-unprocessed-begin 320,11453
-(defun proof-script-end 328,11707
-(defun proof-queue-or-locked-end 337,12010
-(defun proof-locked-end 352,12688
-(defun proof-locked-region-full-p 366,12969
-(defun proof-locked-region-empty-p 375,13241
-(defun proof-only-whitespace-to-locked-region-p 379,13391
-(defun proof-in-locked-region-p 389,13718
-(defun proof-goto-end-of-locked 401,13975
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 418,14734
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 429,15215
-(defun proof-end-of-locked-visible-p 443,15828
-(defvar pg-idioms 461,16446
-(defvar pg-visibility-specs 464,16542
-(defconst pg-default-invisibility-spec469,16749
-(defun pg-clear-script-portions 472,16818
-(defun pg-remove-script-element 479,17092
-(defsubst pg-visname 484,17281
-(defun pg-add-element 488,17426
-(defun pg-open-invisible-span 524,19119
-(defun pg-remove-element 535,19482
-(defun pg-make-element-invisible 542,19752
-(defun pg-make-element-visible 548,19996
-(defun pg-toggle-element-visibility 552,20139
-(defun pg-redisplay-for-gnuemacs 559,20426
-(defun pg-show-all-portions 563,20573
-(defun pg-show-all-proofs 583,21291
-(defun pg-hide-all-proofs 588,21419
-(defun pg-add-proof-element 593,21550
-(defun pg-span-name 607,22208
-(defvar pg-span-context-menu-keymap628,22908
-(defun pg-last-output-displayform 635,23146
-(defun pg-set-span-helphighlights 650,23709
-(defun proof-complete-buffer-atomic 690,25153
-(defun proof-register-possibly-new-processed-file732,27073
-(defun proof-inform-prover-file-retracted 778,28910
-(defun proof-auto-retract-dependencies 798,29761
-(defun proof-unregister-buffer-file-name 852,32311
-(defun proof-protected-process-or-retract 898,34136
-(defun proof-deactivate-scripting-auto 925,35306
-(defun proof-deactivate-scripting 934,35664
-(defun proof-activate-scripting 1067,40920
-(defun proof-toggle-active-scripting 1182,46038
-(defun proof-done-advancing 1221,47283
-(defun proof-done-advancing-comment 1300,50268
-(defun proof-done-advancing-save 1334,51644
-(defun proof-make-goalsave 1419,54856
-(defun proof-get-name-from-goal 1437,55688
-(defun proof-done-advancing-autosave 1457,56713
-(defun proof-done-advancing-other 1522,59257
-(defun proof-segment-up-to-parser 1550,60210
-(defun proof-script-generic-parse-find-comment-end 1614,62293
-(defun proof-script-generic-parse-cmdend 1623,62707
-(defun proof-script-generic-parse-cmdstart 1648,63594
-(defun proof-script-generic-parse-sexp 1711,66287
-(defun proof-cmdstart-add-segment-for-cmd 1735,67219
-(defun proof-segment-up-to-cmdstart 1787,69432
-(defun proof-segment-up-to-cmdend 1848,71792
-(defun proof-semis-to-vanillas 1920,74471
-(defun proof-assert-until-point 1952,75570
-(defun proof-assert-semis 1967,76163
-(defun proof-retract-before-change 1975,76508
-(defun proof-inside-comment 1984,76826
-(defun proof-insert-pbp-command 1998,77061
-(defun proof-insert-sendback-command 2012,77540
-(defun proof-done-retracting 2038,78443
-(defun proof-setup-retract-action 2073,79884
-(defun proof-last-goal-or-goalsave 2083,80367
-(defun proof-retract-target 2107,81272
-(defun proof-retract-until-point-interactive 2188,84642
-(defun proof-retract-until-point 2196,85027
-(define-derived-mode proof-mode 2243,86862
-(defun proof-script-set-visited-file-name 2280,88230
-(defun proof-script-set-buffer-hooks 2302,89243
-(defun proof-script-kill-buffer-fn 2310,89661
-(defun proof-config-done-related 2342,90978
-(defun proof-generic-goal-command-p 2410,93501
-(defun proof-generic-state-preserving-p 2415,93714
-(defun proof-generic-count-undos 2424,94231
-(defun proof-generic-find-and-forget 2453,95269
-(defconst proof-script-important-settings2506,97108
-(defun proof-config-done 2521,97654
-(defun proof-setup-parsing-mechanism 2589,99932
-(defun proof-setup-imenu 2633,101785
-(deflocal proof-segment-up-to-cache 2657,102559
-(deflocal proof-segment-up-to-cache-start 2658,102600
-(deflocal proof-last-edited-low-watermark 2659,102645
-(defun proof-segment-up-to-using-cache 2669,103132
-(defun proof-segment-cache-contents-for 2698,104280
-(defun proof-script-after-change-function 2710,104649
-(defun proof-script-set-after-change-functions 2722,105156
-
-generic/proof-shell.el,3834
+(defun proof-span-read-only 137,4788
+(defun proof-strict-read-only 146,5161
+(defsubst proof-set-queue-endpoints 156,5539
+(defun proof-set-overlay-arrow 160,5680
+(defsubst proof-set-locked-endpoints 171,6018
+(defsubst proof-detach-queue 176,6194
+(defsubst proof-detach-locked 181,6333
+(defsubst proof-set-queue-start 188,6558
+(defsubst proof-set-locked-end 192,6684
+(defsubst proof-set-queue-end 204,7154
+(defun proof-init-segmentation 215,7451
+(defun proof-colour-locked 248,8913
+(defun proof-restart-buffers 259,9345
+(defun proof-script-buffers-with-spans 281,10164
+(defun proof-script-remove-all-spans-and-deactivate 291,10520
+(defun proof-script-clear-queue-spans-on-error 295,10710
+(defun proof-script-delete-spans 311,11287
+(defun proof-script-delete-secondary-spans 316,11486
+(defun proof-unprocessed-begin 328,11774
+(defun proof-script-end 336,12028
+(defun proof-queue-or-locked-end 345,12331
+(defun proof-locked-end 360,13009
+(defun proof-locked-region-full-p 374,13290
+(defun proof-locked-region-empty-p 383,13562
+(defun proof-only-whitespace-to-locked-region-p 387,13712
+(defun proof-in-locked-region-p 397,14039
+(defun proof-goto-end-of-locked 409,14296
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 426,15055
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 437,15536
+(defun proof-end-of-locked-visible-p 451,16149
+(defvar pg-idioms 469,16767
+(defvar pg-visibility-specs 472,16863
+(defconst pg-default-invisibility-spec477,17070
+(defun pg-clear-script-portions 480,17139
+(defun pg-remove-script-element 487,17413
+(defsubst pg-visname 492,17602
+(defun pg-add-element 496,17747
+(defun pg-open-invisible-span 532,19440
+(defun pg-remove-element 543,19803
+(defun pg-make-element-invisible 550,20073
+(defun pg-make-element-visible 556,20317
+(defun pg-toggle-element-visibility 560,20460
+(defun pg-redisplay-for-gnuemacs 567,20747
+(defun pg-show-all-portions 571,20894
+(defun pg-show-all-proofs 591,21612
+(defun pg-hide-all-proofs 596,21740
+(defun pg-add-proof-element 601,21871
+(defun pg-span-name 616,22592
+(defvar pg-span-context-menu-keymap637,23292
+(defun pg-last-output-displayform 644,23530
+(defun pg-set-span-helphighlights 659,24093
+(defun proof-complete-buffer-atomic 706,25796
+(defun proof-register-possibly-new-processed-file748,27716
+(defun proof-inform-prover-file-retracted 794,29553
+(defun proof-auto-retract-dependencies 814,30404
+(defun proof-unregister-buffer-file-name 868,32954
+(defun proof-protected-process-or-retract 914,34779
+(defun proof-deactivate-scripting-auto 941,35949
+(defun proof-deactivate-scripting 950,36307
+(defun proof-activate-scripting 1083,41563
+(defun proof-toggle-active-scripting 1198,46681
+(defun proof-done-advancing 1237,47926
+(defun proof-done-advancing-comment 1316,50911
+(defun proof-done-advancing-save 1350,52287
+(defun proof-make-goalsave 1438,55652
+(defun proof-get-name-from-goal 1456,56484
+(defun proof-done-advancing-autosave 1476,57509
+(defun proof-done-advancing-other 1541,60053
+(defun proof-segment-up-to-parser 1569,61006
+(defun proof-script-generic-parse-find-comment-end 1639,63281
+(defun proof-script-generic-parse-cmdend 1648,63695
+(defun proof-script-generic-parse-cmdstart 1673,64582
+(defun proof-script-generic-parse-sexp 1736,67275
+(defun proof-cmdstart-add-segment-for-cmd 1760,68207
+(defun proof-segment-up-to-cmdstart 1812,70420
+(defun proof-segment-up-to-cmdend 1873,72780
+(defun proof-semis-to-vanillas 1945,75459
+(defun proof-script-next-command-advance 1994,76981
+(defun proof-assert-until-point 2013,77480
+(defun proof-assert-electric-terminator 2028,78073
+(defun proof-assert-semis 2062,79415
+(defun proof-retract-before-change 2075,80054
+(defun proof-inside-comment 2084,80372
+(defun proof-insert-pbp-command 2099,80655
+(defun proof-insert-sendback-command 2114,81149
+(defun proof-done-retracting 2140,82052
+(defun proof-setup-retract-action 2175,83493
+(defun proof-last-goal-or-goalsave 2185,83979
+(defun proof-retract-target 2209,84884
+(defun proof-retract-until-point-interactive 2292,88398
+(defun proof-retract-until-point 2300,88783
+(define-derived-mode proof-mode 2347,90618
+(defun proof-script-set-visited-file-name 2384,91986
+(defun proof-script-set-buffer-hooks 2406,92999
+(defun proof-script-kill-buffer-fn 2414,93417
+(defun proof-config-done-related 2446,94734
+(defun proof-generic-goal-command-p 2514,97257
+(defun proof-generic-state-preserving-p 2519,97470
+(defun proof-generic-count-undos 2528,97987
+(defun proof-generic-find-and-forget 2557,99025
+(defconst proof-script-important-settings2610,100864
+(defun proof-config-done 2625,101410
+(defun proof-setup-parsing-mechanism 2693,103688
+(defun proof-setup-imenu 2737,105541
+(deflocal proof-segment-up-to-cache 2761,106315
+(deflocal proof-segment-up-to-cache-start 2762,106356
+(deflocal proof-last-edited-low-watermark 2763,106401
+(defun proof-segment-up-to-using-cache 2773,106888
+(defun proof-segment-cache-contents-for 2802,108036
+(defun proof-script-after-change-function 2814,108405
+(defun proof-script-set-after-change-functions 2826,108912
+
+generic/proof-shell.el,3745
 (defvar proof-marker 35,808
 (defvar proof-action-list 38,904
-(defvar proof-shell-last-goals-output 63,1842
-(defvar proof-shell-last-response-output 66,1922
-(defvar proof-shell-delayed-output-start 69,2009
-(defvar proof-shell-delayed-output-end 73,2191
-(defvar proof-shell-delayed-output-flags 77,2371
-(defcustom proof-shell-active-scripting-indicator86,2567
-(defun proof-shell-ready-prover 134,3881
-(defsubst proof-shell-live-buffer 148,4420
-(defun proof-shell-available-p 155,4659
-(defun proof-grab-lock 161,4881
-(defun proof-release-lock 172,5379
-(defcustom proof-shell-fiddle-frames 184,5599
-(defun proof-shell-set-text-representation 190,5821
-(defun proof-shell-start 201,6282
-(defvar proof-shell-kill-function-hooks 386,12548
-(defun proof-shell-kill-function 389,12646
-(defun proof-shell-clear-state 478,16450
-(defun proof-shell-exit 493,16893
-(defun proof-shell-bail-out 505,17338
-(defun proof-shell-restart 514,17815
-(defvar proof-shell-urgent-message-marker 556,19193
-(defvar proof-shell-urgent-message-scanner 559,19314
-(defun proof-shell-handle-error-output 562,19440
-(defsubst proof-shell-strip-output-markup 583,20202
-(defun proof-shell-handle-error-or-interrupt 596,20568
-(defun proof-shell-error-or-interrupt-action 632,22037
-(defun proof-goals-pos 654,22816
-(defun proof-pbp-focus-on-first-goal 659,23027
-(defsubst proof-shell-string-match-safe 671,23443
-(defun proof-shell-handle-immediate-output 675,23604
-(defvar proof-shell-expecting-output 742,26168
-(defvar proof-shell-interrupt-pending 746,26327
-(defun proof-interrupt-process 751,26551
-(defun proof-shell-insert 789,27984
-(defun proof-shell-action-list-item 840,29727
-(defun proof-shell-set-silent 846,29972
-(defun proof-shell-start-silent-item 852,30191
-(defun proof-shell-clear-silent 858,30380
-(defun proof-shell-stop-silent-item 864,30602
-(defun proof-shell-should-be-silent 871,30871
-(defsubst proof-shell-invoke-callback 885,31458
-(defsubst proof-shell-insert-action-item 891,31668
-(defun proof-append-alist 895,31843
-(defun proof-start-queue 953,33968
-(defun proof-extend-queue 964,34317
-(defun proof-shell-exec-loop 973,34696
-(defun proof-shell-insert-loopback-cmd 1050,37302
-(defun proof-shell-process-urgent-message 1075,38448
-(defun proof-shell-process-urgent-message-default 1124,40169
-(defun proof-shell-process-urgent-message-trace 1141,40801
-(defun proof-shell-process-urgent-message-retract 1154,41361
-(defun proof-shell-process-urgent-message-elisp 1175,42209
-(defun proof-shell-process-urgent-message-thmdeps 1190,42704
-(defun proof-shell-message 1204,43084
-(defun proof-shell-strip-eager-annotations 1211,43336
-(defvar proof-shell-minibuffer-urgent-interactive-input-history 1226,43869
-(defun proof-shell-minibuffer-urgent-interactive-input 1228,43939
-(defun proof-shell-filter 1244,44406
-(defun proof-shell-filter-first-command 1345,47815
-(defun proof-shell-process-urgent-messages 1360,48358
-(defun proof-shell-filter-manage-output 1427,50823
-(defsubst proof-shell-display-output-as-response 1460,52126
-(defun proof-shell-handle-delayed-output 1466,52418
-(defvar pg-last-tracing-output-time 1563,55885
-(defconst pg-slow-mode-duration 1566,55991
-(defconst pg-fast-tracing-mode-threshold 1569,56073
-(defvar pg-tracing-cleanup-timer 1572,56201
-(defun pg-tracing-tight-loop 1574,56240
-(defun pg-finish-tracing-display 1617,57952
-(defun proof-shell-wait 1635,58316
-(defun proof-done-invisible 1654,59224
-(defun proof-shell-invisible-command 1660,59394
-(defun proof-shell-invisible-cmd-get-result 1707,60938
-(defun proof-shell-invisible-command-invisible-result 1719,61374
-(defun pg-insert-last-output-as-comment 1739,61875
-(define-derived-mode proof-shell-mode 1758,62347
-(defconst proof-shell-important-settings1800,63740
-(defun proof-shell-config-done 1806,63855
+(defvar proof-shell-last-goals-output 63,1832
+(defvar proof-shell-last-response-output 66,1912
+(defvar proof-shell-delayed-output-start 69,1999
+(defvar proof-shell-delayed-output-end 73,2181
+(defvar proof-shell-delayed-output-flags 77,2361
+(defcustom proof-shell-active-scripting-indicator86,2557
+(defun proof-shell-ready-prover 134,3909
+(defsubst proof-shell-live-buffer 148,4448
+(defun proof-shell-available-p 155,4687
+(defun proof-grab-lock 161,4909
+(defun proof-release-lock 172,5407
+(defcustom proof-shell-fiddle-frames 184,5627
+(defun proof-shell-set-text-representation 190,5849
+(defun proof-shell-start 201,6310
+(defvar proof-shell-kill-function-hooks 387,12598
+(defun proof-shell-kill-function 390,12696
+(defun proof-shell-clear-state 479,16500
+(defun proof-shell-exit 494,16943
+(defun proof-shell-bail-out 506,17388
+(defun proof-shell-restart 515,17865
+(defvar proof-shell-urgent-message-marker 557,19243
+(defvar proof-shell-urgent-message-scanner 560,19364
+(defun proof-shell-handle-error-output 563,19490
+(defun proof-shell-handle-error-or-interrupt 589,20352
+(defun proof-shell-error-or-interrupt-action 624,21773
+(defun proof-goals-pos 638,22301
+(defun proof-pbp-focus-on-first-goal 643,22512
+(defsubst proof-shell-string-match-safe 655,22928
+(defun proof-shell-handle-immediate-output 659,23089
+(defvar proof-shell-expecting-output 726,25671
+(defvar proof-shell-interrupt-pending 730,25830
+(defun proof-interrupt-process 735,26054
+(defun proof-shell-insert 773,27487
+(defun proof-shell-action-list-item 826,29355
+(defun proof-shell-set-silent 831,29606
+(defun proof-shell-start-silent-item 837,29825
+(defun proof-shell-clear-silent 843,30014
+(defun proof-shell-stop-silent-item 849,30236
+(defsubst proof-shell-should-be-silent 855,30425
+(defsubst proof-shell-invoke-callback 867,30928
+(defsubst proof-shell-insert-action-item 873,31138
+(defun proof-add-to-queue 877,31313
+(defun proof-start-queue 934,33535
+(defun proof-extend-queue 945,33899
+(defun proof-shell-exec-loop 954,34281
+(defun proof-shell-insert-loopback-cmd 1034,37057
+(defun proof-shell-process-urgent-message 1059,38203
+(defun proof-shell-process-urgent-message-default 1108,39924
+(defun proof-shell-process-urgent-message-trace 1124,40511
+(defun proof-shell-process-urgent-message-retract 1137,41071
+(defun proof-shell-process-urgent-message-elisp 1158,41919
+(defun proof-shell-process-urgent-message-thmdeps 1173,42414
+(defun proof-shell-strip-eager-annotations 1187,42794
+(defvar proof-shell-minibuffer-urgent-interactive-input-history 1202,43327
+(defun proof-shell-minibuffer-urgent-interactive-input 1204,43397
+(defun proof-shell-filter 1220,43871
+(defun proof-shell-filter-first-command 1321,47280
+(defun proof-shell-process-urgent-messages 1336,47823
+(defun proof-shell-filter-manage-output 1400,50123
+(defsubst proof-shell-display-output-as-response 1433,51426
+(defun proof-shell-handle-delayed-output 1439,51718
+(defvar pg-last-tracing-output-time 1534,55183
+(defconst pg-slow-mode-duration 1537,55289
+(defconst pg-fast-tracing-mode-threshold 1540,55371
+(defvar pg-tracing-cleanup-timer 1543,55499
+(defun pg-tracing-tight-loop 1545,55538
+(defun pg-finish-tracing-display 1588,57250
+(defun proof-shell-wait 1606,57614
+(defun proof-done-invisible 1625,58522
+(defun proof-shell-invisible-command 1631,58692
+(defun proof-shell-invisible-cmd-get-result 1678,60236
+(defun proof-shell-invisible-command-invisible-result 1690,60672
+(defun pg-insert-last-output-as-comment 1710,61173
+(define-derived-mode proof-shell-mode 1729,61645
+(defconst proof-shell-important-settings1766,62676
+(defun proof-shell-config-done 1772,62791
 
 generic/proof-site.el,503
 (defconst proof-assistant-table-default22,725
@@ -1826,91 +1856,93 @@ generic/proof-unicode-tokens.el,497
 (defun proof-unicode-tokens-deactivate-prover 138,4803
 
 generic/proof-useropts.el,1510
-(defgroup proof-user-options 21,552
-(defun proof-set-value 29,731
-(defcustom proof-electric-terminator-enable 62,1854
-(defcustom proof-toolbar-enable 74,2386
-(defcustom proof-imenu-enable 80,2559
-(defcustom pg-show-hints 86,2730
-(defcustom proof-shell-quiet-errors 91,2863
-(defcustom proof-trace-output-slow-catchup 98,3136
-(defcustom proof-strict-state-preserving 108,3633
-(defcustom proof-strict-read-only 121,4242
-(defcustom proof-allow-undo-in-read-only 133,4752
-(defcustom proof-three-window-enable 140,5034
-(defcustom proof-multiple-frames-enable 159,5784
-(defcustom proof-delete-empty-windows 168,6117
-(defcustom proof-shrink-windows-tofit 179,6648
-(defcustom proof-auto-raise-buffers 186,6920
-(defcustom proof-colour-locked 193,7155
-(defcustom proof-query-file-save-when-activating-scripting201,7405
-(defcustom proof-one-command-per-line217,8125
-(defcustom proof-prog-name-ask224,8349
-(defcustom proof-prog-name-guess230,8509
-(defcustom proof-tidy-response238,8774
-(defcustom proof-keep-response-history252,9237
-(defcustom pg-input-ring-size 262,9625
-(defcustom proof-general-debug 267,9777
-(defcustom proof-use-parser-cache 278,10186
-(defcustom proof-follow-mode 288,10483
-(defcustom proof-auto-action-when-deactivating-scripting 312,11660
-(defcustom proof-script-command-separator 335,12609
-(defcustom proof-rsh-command 343,12901
-(defcustom proof-disappearing-proofs 359,13451
-(defcustom proof-full-annotation 364,13612
-(defcustom proof-minibuffer-messages 373,13984
-
-generic/proof-utils.el,1938
-(defmacro deflocal 65,1980
-(defmacro proof-with-current-buffer-if-exists 72,2218
-(deflocal proof-buffer-type 78,2428
-(defmacro proof-with-script-buffer 84,2708
-(defmacro proof-map-buffers 95,3089
-(defmacro proof-sym 100,3274
-(defsubst proof-try-require 105,3435
-(defun proof-save-some-buffers 118,3766
-(defmacro proof-ass-sym 167,5367
-(defmacro proof-ass-symv 173,5626
-(defmacro proof-ass 179,5884
-(defun proof-defpgcustom-fn 185,6136
-(defun undefpgcustom 206,7006
-(defmacro defpgcustom 212,7230
-(defun proof-defpgdefault-fn 223,7641
-(defmacro defpgdefault 237,8099
-(defmacro defpgfun 248,8461
-(defun proof-defpacustom-fn 262,8861
-(defmacro defpacustom 328,11142
-(defmacro proof-eval-when-ready-for-assistant 349,12089
-(defun proof-file-truename 362,12480
-(defun proof-files-to-buffers 366,12663
-(defun proof-buffers-in-mode 374,12903
-(defun pg-save-from-death 388,13353
-(defun proof-define-keys 407,13970
-(defun pg-remove-specials 418,14255
-(defun pg-remove-specials-in-string 428,14591
-(defun proof-warn-if-unset 439,14817
-(defun proof-get-window-for-buffer 444,15035
-(defun proof-display-and-keep-buffer 495,17343
-(defun proof-clean-buffer 537,19066
-(defun pg-internal-warning 553,19722
-(defun proof-debug 560,19989
-(defun proof-switch-to-buffer 568,20338
-(defun proof-resize-window-tofit 590,21462
-(defun proof-submit-bug-report 684,25308
-(defun proof-deftoggle-fn 719,26665
-(defmacro proof-deftoggle 734,27318
-(defun proof-defintset-fn 741,27692
-(defmacro proof-defintset 757,28396
-(defun proof-defstringset-fn 764,28773
-(defmacro proof-defstringset 777,29399
-(defun proof-escape-keymap-doc 790,29855
-(defmacro proof-defshortcut 794,29995
-(defmacro proof-definvisible 809,30593
-(defun pg-custom-save-vars 836,31520
-(defun pg-custom-reset-vars 852,32164
-(defun proof-locate-executable 865,32501
-(defun pg-current-word-pos 880,33056
-(defun proof-looking-at-syntactic-context 927,34772
+(defgroup proof-user-options 21,553
+(defun proof-set-value 29,732
+(defcustom proof-electric-terminator-enable 62,1855
+(defcustom proof-toolbar-enable 74,2387
+(defcustom proof-imenu-enable 80,2560
+(defcustom pg-show-hints 86,2731
+(defcustom proof-shell-quiet-errors 91,2864
+(defcustom proof-trace-output-slow-catchup 98,3135
+(defcustom proof-strict-state-preserving 108,3632
+(defcustom proof-strict-read-only 121,4241
+(defcustom proof-allow-undo-in-read-only 134,4820
+(defcustom proof-three-window-enable 141,5102
+(defcustom proof-multiple-frames-enable 160,5852
+(defcustom proof-delete-empty-windows 169,6185
+(defcustom proof-shrink-windows-tofit 180,6716
+(defcustom proof-auto-raise-buffers 187,6988
+(defcustom proof-colour-locked 194,7223
+(defcustom proof-query-file-save-when-activating-scripting202,7473
+(defcustom proof-one-command-per-line218,8193
+(defcustom proof-prog-name-ask225,8417
+(defcustom proof-prog-name-guess231,8577
+(defcustom proof-tidy-response239,8842
+(defcustom proof-keep-response-history253,9305
+(defcustom pg-input-ring-size 263,9693
+(defcustom proof-general-debug 268,9845
+(defcustom proof-use-parser-cache 279,10254
+(defcustom proof-follow-mode 289,10551
+(defcustom proof-auto-action-when-deactivating-scripting 313,11728
+(defcustom proof-script-command-separator 336,12677
+(defcustom proof-rsh-command 344,12969
+(defcustom proof-disappearing-proofs 360,13519
+(defcustom proof-full-annotation 365,13680
+(defcustom proof-minibuffer-messages 374,14052
+
+generic/proof-utils.el,2033
+(defmacro deflocal 61,1871
+(defmacro proof-with-current-buffer-if-exists 68,2109
+(deflocal proof-buffer-type 74,2319
+(defmacro proof-with-script-buffer 80,2599
+(defmacro proof-map-buffers 91,2980
+(defmacro proof-sym 96,3165
+(defsubst proof-try-require 101,3326
+(defun proof-save-some-buffers 114,3657
+(defmacro proof-ass-sym 163,5258
+(defmacro proof-ass-symv 169,5517
+(defmacro proof-ass 175,5775
+(defun proof-defpgcustom-fn 181,6027
+(defun undefpgcustom 202,6897
+(defmacro defpgcustom 208,7121
+(defun proof-defpgdefault-fn 219,7532
+(defmacro defpgdefault 233,7990
+(defmacro defpgfun 244,8352
+(defun proof-defpacustom-fn 258,8752
+(defmacro defpacustom 324,11033
+(defmacro proof-eval-when-ready-for-assistant 345,11980
+(defun proof-file-truename 358,12371
+(defun proof-files-to-buffers 362,12554
+(defun proof-buffers-in-mode 370,12794
+(defun pg-save-from-death 384,13244
+(defun proof-define-keys 403,13861
+(defun pg-remove-specials 414,14146
+(defun pg-remove-specials-in-string 424,14482
+(defun proof-warn-if-unset 435,14708
+(defun proof-get-window-for-buffer 440,14926
+(defun proof-display-and-keep-buffer 491,17234
+(defun proof-clean-buffer 533,18957
+(defun pg-internal-warning 549,19613
+(defun proof-debug 556,19880
+(defun proof-switch-to-buffer 566,20252
+(defun proof-resize-window-tofit 588,21376
+(defun proof-submit-bug-report 683,25224
+(defun proof-deftoggle-fn 718,26581
+(defmacro proof-deftoggle 733,27234
+(defun proof-defintset-fn 740,27608
+(defmacro proof-defintset 756,28312
+(defun proof-defstringset-fn 763,28689
+(defmacro proof-defstringset 776,29315
+(defun proof-escape-keymap-doc 789,29771
+(defmacro proof-defshortcut 793,29911
+(defmacro proof-definvisible 808,30509
+(defun pg-custom-save-vars 835,31436
+(defun pg-custom-reset-vars 851,32080
+(defun proof-locate-executable 864,32417
+(defun pg-current-word-pos 879,32972
+(defun proof-looking-at-syntactic-context 926,34688
+(defsubst proof-shell-strip-output-markup 941,35257
+(defun proof-minibuffer-message 947,35521
 
 lib/bufhist.el,1106
 (defun bufhist-ring-update 36,1305
@@ -2023,11 +2055,12 @@ lib/maths-menu.el,242
 (defvar maths-menu-mode-map344,12882
 (define-minor-mode maths-menu-mode352,13101
 
-lib/pg-dev.el,138
-(defconst pg-dev-lisp-font-lock-keywords52,1591
-(defun unload-pg 79,2385
-(defun profile-pg 107,3248
-(defun pg-bug-references 124,3674
+lib/pg-dev.el,166
+(defconst pg-dev-lisp-font-lock-keywords52,1582
+(defun pg-loadpath 80,2416
+(defun unload-pg 90,2587
+(defun profile-pg 118,3450
+(defun pg-bug-references 139,4117
 
 lib/pg-fontsets.el,210
 (defcustom pg-fontsets-default-fontset 28,780
@@ -2068,7 +2101,7 @@ lib/scomint.el,876
 (defun scomint-output-filter 288,11418
 (defun scomint-interrupt-process 360,14150
 
-lib/span.el,1354
+lib/span.el,1315
 (defalias 'span-start span-start22,609
 (defalias 'span-end span-end23,647
 (defalias 'span-set-property span-set-property24,681
@@ -2080,32 +2113,31 @@ lib/span.el,1354
 (defun span-read-only-hook 31,925
 (defsubst span-read-only 36,1115
 (defsubst span-read-write 43,1425
-(defsubst span-give-warning 48,1595
-(defsubst span-write-warning 53,1741
-(defsubst span-lt 65,2307
-(defsubst spans-at-point-prop 70,2451
-(defsubst spans-at-region-prop 79,2642
-(defsubst span-at 89,2908
-(defsubst span-delete 93,3034
-(defsubst span-mapcar-spans 100,3256
-(defsubst span-mapc-spans 104,3431
-(defun span-at-before 108,3602
-(defsubst prev-span 125,4326
-(defsubst next-span 131,4479
-(defsubst span-live-p 137,4693
-(defsubst span-raise 143,4859
-(defsubst span-string 147,4992
-(defsubst set-span-properties 152,5152
-(defsubst span-find-span 158,5346
-(defsubst span-at-event 166,5658
-(defun fold-spans 172,5855
-(defsubst span-detached-p 186,6388
-(defsubst set-span-face 190,6504
-(defsubst set-span-keymap 194,6602
-(defsubst span-delete-spans 202,6771
-(defsubst span-property-safe 206,6933
-(defsubst span-set-start 210,7070
-(defsubst span-set-end 214,7202
+(defsubst span-write-warning 48,1595
+(defsubst span-lt 59,2119
+(defsubst spans-at-point-prop 64,2263
+(defsubst spans-at-region-prop 73,2454
+(defsubst span-at 83,2720
+(defsubst span-delete 87,2846
+(defsubst span-mapcar-spans 94,3068
+(defsubst span-mapc-spans 98,3243
+(defun span-at-before 102,3414
+(defsubst prev-span 119,4138
+(defsubst next-span 125,4291
+(defsubst span-live-p 131,4505
+(defsubst span-raise 137,4671
+(defsubst span-string 141,4804
+(defsubst set-span-properties 146,4964
+(defsubst span-find-span 152,5158
+(defsubst span-at-event 160,5470
+(defun fold-spans 166,5667
+(defsubst span-detached-p 180,6200
+(defsubst set-span-face 184,6316
+(defsubst set-span-keymap 188,6414
+(defsubst span-delete-spans 196,6583
+(defsubst span-property-safe 200,6745
+(defsubst span-set-start 204,6882
+(defsubst span-set-end 208,7014
 
 lib/texi-docstring-magic.el,584
 (defun texi-docstring-magic-find-face 88,3027
@@ -2154,79 +2186,79 @@ lib/unicode-tokens.el,5231
 (defface unicode-tokens-script-font-face270,9589
 (defface unicode-tokens-fraktur-font-face275,9733
 (defface unicode-tokens-serif-font-face280,9858
-(defface unicode-tokens-sans-font-face285,9985
-(defface unicode-tokens-highlight-face290,10107
-(defconst unicode-tokens-fonts299,10469
-(defconst unicode-tokens-fontsymb-properties308,10686
-(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map334,12132
-(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist352,12684
-(defconst unicode-tokens-font-lock-extra-managed-props365,13015
-(defun unicode-tokens-font-lock-keywords 369,13169
-(defun unicode-tokens-calculate-token-match 402,14540
-(defun unicode-tokens-usable-composition 432,15578
-(defun unicode-tokens-help-echo 445,15957
-(defvar unicode-tokens-show-symbols 449,16121
-(defun unicode-tokens-interpret-composition 452,16235
-(defun unicode-tokens-font-lock-compose-symbol 470,16747
-(defun unicode-tokens-prepend-text-properties-in-match 500,17994
-(defun unicode-tokens-prepend-text-property 514,18572
-(defun unicode-tokens-show-symbols 539,19717
-(defun unicode-tokens-symbs-to-props 547,20027
-(defvar unicode-tokens-show-controls 567,20726
-(defun unicode-tokens-show-controls 570,20817
-(defun unicode-tokens-control-char 583,21402
-(defun unicode-tokens-control-region 592,21841
-(defun unicode-tokens-control-font-lock-keywords 603,22388
-(defvar unicode-tokens-use-shortcuts 614,22712
-(defun unicode-tokens-use-shortcuts 617,22815
-(defun unicode-tokens-map-ordering 635,23421
-(defun unicode-tokens-quail-define-rules 644,23774
-(defun unicode-tokens-insert-token 667,24451
-(defun unicode-tokens-annotate-region 676,24755
-(defun unicode-tokens-insert-control 700,25593
-(defun unicode-tokens-insert-uchar-as-token 710,26042
-(defun unicode-tokens-delete-token-near-point 716,26263
-(defun unicode-tokens-prev-token 730,26825
-(defun unicode-tokens-rotate-token-forward 738,27122
-(defun unicode-tokens-rotate-token-backward 765,28012
-(defun unicode-tokens-replace-shortcut-match 770,28214
-(defun unicode-tokens-replace-shortcuts 779,28584
-(defun unicode-tokens-replace-unicode-match 793,29182
-(defun unicode-tokens-replace-unicode 800,29483
-(defun unicode-tokens-copy-token 817,30082
-(define-button-type 'unicode-tokens-listunicode-tokens-list824,30303
-(defun unicode-tokens-list-tokens 830,30507
-(defun unicode-tokens-list-shortcuts 869,31691
-(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars887,32329
-(defun unicode-tokens-encode-in-temp-buffer 889,32402
-(defun unicode-tokens-encode 907,33058
-(defun unicode-tokens-encode-str 913,33294
-(defun unicode-tokens-copy 917,33456
-(defun unicode-tokens-paste 926,33862
-(defvar unicode-tokens-highlight-unicode 945,34583
-(defconst unicode-tokens-unicode-highlight-patterns948,34675
-(defun unicode-tokens-highlight-unicode 952,34844
-(defun unicode-tokens-highlight-unicode-setkeywords 964,35307
-(defun unicode-tokens-initialise 976,35676
-(defvar unicode-tokens-mode-map 996,36347
-(define-minor-mode unicode-tokens-mode999,36444
-(defun unicode-tokens-set-font-var 1126,40688
-(defun unicode-tokens-set-font-var-aux 1142,41179
-(defun unicode-tokens-mouse-set-font 1167,42221
-(defsubst unicode-tokens-face-font-sym 1180,42735
-(defun unicode-tokens-set-font-restart 1184,42915
-(defun unicode-tokens-save-fonts 1195,43225
-(defun unicode-tokens-custom-save-faces 1203,43481
-(define-key unicode-tokens-mode-map 1220,43937
-(define-key unicode-tokens-mode-map 1222,44029
-(define-key unicode-tokens-mode-map1224,44120
-(define-key unicode-tokens-mode-map1226,44226
-(define-key unicode-tokens-mode-map1229,44341
-(define-key unicode-tokens-mode-map1231,44450
-(define-key unicode-tokens-mode-map1233,44558
-(define-key unicode-tokens-mode-map1235,44664
-(defun unicode-tokens-customize-submenu 1243,44788
-(defun unicode-tokens-define-menu 1250,45011
+(defface unicode-tokens-sans-font-face285,9995
+(defface unicode-tokens-highlight-face290,10117
+(defconst unicode-tokens-fonts299,10479
+(defconst unicode-tokens-fontsymb-properties308,10696
+(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map334,12142
+(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist352,12694
+(defconst unicode-tokens-font-lock-extra-managed-props365,13025
+(defun unicode-tokens-font-lock-keywords 369,13179
+(defun unicode-tokens-calculate-token-match 402,14550
+(defun unicode-tokens-usable-composition 432,15588
+(defun unicode-tokens-help-echo 445,15967
+(defvar unicode-tokens-show-symbols 449,16131
+(defun unicode-tokens-interpret-composition 452,16245
+(defun unicode-tokens-font-lock-compose-symbol 470,16757
+(defun unicode-tokens-prepend-text-properties-in-match 500,18004
+(defun unicode-tokens-prepend-text-property 514,18582
+(defun unicode-tokens-show-symbols 539,19727
+(defun unicode-tokens-symbs-to-props 547,20037
+(defvar unicode-tokens-show-controls 567,20736
+(defun unicode-tokens-show-controls 570,20827
+(defun unicode-tokens-control-char 583,21412
+(defun unicode-tokens-control-region 592,21851
+(defun unicode-tokens-control-font-lock-keywords 603,22398
+(defvar unicode-tokens-use-shortcuts 614,22722
+(defun unicode-tokens-use-shortcuts 617,22825
+(defun unicode-tokens-map-ordering 635,23431
+(defun unicode-tokens-quail-define-rules 644,23784
+(defun unicode-tokens-insert-token 667,24461
+(defun unicode-tokens-annotate-region 676,24765
+(defun unicode-tokens-insert-control 700,25603
+(defun unicode-tokens-insert-uchar-as-token 710,26052
+(defun unicode-tokens-delete-token-near-point 716,26273
+(defun unicode-tokens-prev-token 730,26835
+(defun unicode-tokens-rotate-token-forward 738,27132
+(defun unicode-tokens-rotate-token-backward 765,28022
+(defun unicode-tokens-replace-shortcut-match 770,28224
+(defun unicode-tokens-replace-shortcuts 779,28594
+(defun unicode-tokens-replace-unicode-match 793,29192
+(defun unicode-tokens-replace-unicode 800,29493
+(defun unicode-tokens-copy-token 817,30092
+(define-button-type 'unicode-tokens-listunicode-tokens-list824,30313
+(defun unicode-tokens-list-tokens 830,30517
+(defun unicode-tokens-list-shortcuts 869,31701
+(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars887,32339
+(defun unicode-tokens-encode-in-temp-buffer 889,32412
+(defun unicode-tokens-encode 907,33068
+(defun unicode-tokens-encode-str 913,33304
+(defun unicode-tokens-copy 917,33466
+(defun unicode-tokens-paste 926,33872
+(defvar unicode-tokens-highlight-unicode 945,34593
+(defconst unicode-tokens-unicode-highlight-patterns948,34685
+(defun unicode-tokens-highlight-unicode 952,34854
+(defun unicode-tokens-highlight-unicode-setkeywords 964,35317
+(defun unicode-tokens-initialise 976,35686
+(defvar unicode-tokens-mode-map 996,36357
+(define-minor-mode unicode-tokens-mode999,36454
+(defun unicode-tokens-set-font-var 1126,40698
+(defun unicode-tokens-set-font-var-aux 1142,41189
+(defun unicode-tokens-mouse-set-font 1167,42231
+(defsubst unicode-tokens-face-font-sym 1180,42745
+(defun unicode-tokens-set-font-restart 1184,42925
+(defun unicode-tokens-save-fonts 1195,43235
+(defun unicode-tokens-custom-save-faces 1203,43491
+(define-key unicode-tokens-mode-map 1220,43947
+(define-key unicode-tokens-mode-map 1222,44039
+(define-key unicode-tokens-mode-map1224,44130
+(define-key unicode-tokens-mode-map1226,44236
+(define-key unicode-tokens-mode-map1229,44351
+(define-key unicode-tokens-mode-map1231,44460
+(define-key unicode-tokens-mode-map1233,44568
+(define-key unicode-tokens-mode-map1235,44674
+(defun unicode-tokens-customize-submenu 1243,44798
+(defun unicode-tokens-define-menu 1250,45021
 
 mmm/mmm-auto.el,343
 (defvar mmm-autoloaded-classes67,2676
@@ -2583,49 +2615,49 @@ doc/PG-adapting.texi,3772
 @node Proof Script SettingsProof Script Settings651,25120
 @node Recognizing commands and commentsRecognizing commands and comments673,25700
 @node Recognizing proofsRecognizing proofs810,32137
-@node Recognizing other elementsRecognizing other elements919,36812
-@node Configuring undo behaviourConfiguring undo behaviour1045,42344
-@node Nested proofsNested proofs1182,47733
-@node Safe (state-preserving) commandsSafe (state-preserving) commands1222,49359
-@node Activate scripting hookActivate scripting hook1245,50312
-@node Automatic multiple filesAutomatic multiple files1269,51182
-@node Completions1291,52029
-@node Proof Shell SettingsProof Shell Settings1332,53519
-@node Proof shell commandsProof shell commands1363,54801
-@node Script input to the shellScript input to the shell1527,61845
-@node Settings for matching various output from proof processSettings for matching various output from proof process1592,64803
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1706,69781
-@node Hooks and other settingsHooks and other settings1921,79658
-@node Goals Buffer SettingsGoals Buffer Settings2002,83045
-@node Splash Screen SettingsSplash Screen Settings2079,86151
-@node Global ConstantsGlobal Constants2105,86906
-@node Handling Multiple FilesHandling Multiple Files2131,87747
-@node Configuring Editing SyntaxConfiguring Editing Syntax2283,95530
-@node Configuring Font LockConfiguring Font Lock2340,97647
-@node Configuring TokensConfiguring Tokens2412,101141
-@node Writing More Lisp CodeWriting More Lisp Code2462,103261
-@node Default values for generic settingsDefault values for generic settings2479,103906
-@node Adding prover-specific configurationsAdding prover-specific configurations2509,104989
-@node Useful variablesUseful variables2552,106271
-@node Useful functions and macrosUseful functions and macros2567,106770
-@node Internals of Proof GeneralInternals of Proof General2676,110993
-@node Spans2704,111889
-@node Proof General site configurationProof General site configuration2716,112211
-@node Configuration variable mechanismsConfiguration variable mechanisms2796,115256
-@node Global variablesGlobal variables2917,120700
-@node Proof script modeProof script mode2987,123248
-@node Proof shell modeProof shell mode3225,133855
-@node Debugging3661,151085
-@node Plans and IdeasPlans and Ideas3704,151961
-@node Proof by pointing and similar featuresProof by pointing and similar features3725,152683
-@node Granularity of atomic command sequencesGranularity of atomic command sequences3763,154341
-@node Browser mode for script files and theoriesBrowser mode for script files and theories3808,156566
-@node Demonstration InstantiationsDemonstration Instantiations3838,157597
-@node demoisa-easy.el3854,158028
-@node demoisa.el3916,160220
-@node Function IndexFunction Index4070,165160
-@node Variable IndexVariable Index4074,165236
-@node Concept IndexConcept Index4083,165415
+@node Recognizing other elementsRecognizing other elements919,36811
+@node Configuring undo behaviourConfiguring undo behaviour1045,42343
+@node Nested proofsNested proofs1182,47732
+@node Safe (state-preserving) commandsSafe (state-preserving) commands1222,49358
+@node Activate scripting hookActivate scripting hook1245,50311
+@node Automatic multiple filesAutomatic multiple files1269,51181
+@node Completions1291,52028
+@node Proof Shell SettingsProof Shell Settings1332,53518
+@node Proof shell commandsProof shell commands1363,54800
+@node Script input to the shellScript input to the shell1527,61844
+@node Settings for matching various output from proof processSettings for matching various output from proof process1592,64802
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1706,69780
+@node Hooks and other settingsHooks and other settings1921,79657
+@node Goals Buffer SettingsGoals Buffer Settings2002,83044
+@node Splash Screen SettingsSplash Screen Settings2079,86150
+@node Global ConstantsGlobal Constants2105,86905
+@node Handling Multiple FilesHandling Multiple Files2131,87746
+@node Configuring Editing SyntaxConfiguring Editing Syntax2283,95529
+@node Configuring Font LockConfiguring Font Lock2340,97646
+@node Configuring TokensConfiguring Tokens2412,101140
+@node Writing More Lisp CodeWriting More Lisp Code2462,103260
+@node Default values for generic settingsDefault values for generic settings2479,103905
+@node Adding prover-specific configurationsAdding prover-specific configurations2509,104988
+@node Useful variablesUseful variables2552,106270
+@node Useful functions and macrosUseful functions and macros2567,106769
+@node Internals of Proof GeneralInternals of Proof General2676,110992
+@node Spans2704,111888
+@node Proof General site configurationProof General site configuration2716,112210
+@node Configuration variable mechanismsConfiguration variable mechanisms2796,115255
+@node Global variablesGlobal variables2917,120699
+@node Proof script modeProof script mode2987,123247
+@node Proof shell modeProof shell mode3225,133854
+@node Debugging3661,151084
+@node Plans and IdeasPlans and Ideas3704,151960
+@node Proof by pointing and similar featuresProof by pointing and similar features3725,152682
+@node Granularity of atomic command sequencesGranularity of atomic command sequences3763,154340
+@node Browser mode for script files and theoriesBrowser mode for script files and theories3808,156565
+@node Demonstration InstantiationsDemonstration Instantiations3838,157596
+@node demoisa-easy.el3854,158027
+@node demoisa.el3916,160219
+@node Function IndexFunction Index4070,165159
+@node Variable IndexVariable Index4074,165235
+@node Concept IndexConcept Index4083,165414
 
 generic/proof.el,0
author	David Aspinall <da@inf.ed.ac.uk>	2009-09-15 08:40:12 +0000
committer	David Aspinall <da@inf.ed.ac.uk>	2009-09-15 08:40:12 +0000
commit	5286b54dcbbda5715a59a7fc50cdfb9872706950 (patch)
tree	a830ea13cbed19d7312748b43ce6f194354377ec /TAGS
parent	815cadebd99cd25dc78be6e2ba3af177c4140ebd (diff)