Updated

1 files changed, 650 insertions, 762 deletions

diff --git a/TAGS b/TAGS
index 154cc2e6..050bbc3e 100644
--- a/TAGS
+++ b/TAGS
@@ -38,161 +38,6 @@ coq/coq-db.el,668
 (defconst coq-solve-tactics-face 247,8948
 (defconst coq-cheat-face 251,9112
 
-coq/coq.el,6010
-(defcustom coq-translate-to-v8 48,1381
-(defun coq-build-prog-args 54,1561
-(defcustom coq-compile-file-command 64,1857
-(defcustom coq-use-makefile 72,2176
-(defcustom coq-default-undo-limit 80,2399
-(defconst coq-shell-init-cmd85,2527
-(defcustom coq-prog-env 91,2654
-(defconst coq-shell-restart-cmd 99,2904
-(defvar coq-shell-prompt-pattern101,2958
-(defvar coq-shell-cd 109,3261
-(defvar coq-shell-proof-completed-regexp 113,3421
-(defvar coq-goal-regexp116,3576
-(defun coq-library-directory 123,3690
-(defcustom coq-tags 130,3869
-(defconst coq-interrupt-regexp 135,4019
-(defcustom coq-www-home-page 140,4140
-(defvar coq-outline-regexp147,4308
-(defvar coq-outline-heading-end-regexp 154,4520
-(defvar coq-shell-outline-regexp 156,4574
-(defvar coq-shell-outline-heading-end-regexp 157,4624
-(defconst coq-state-preserving-tactics-regexp163,4789
-(defconst coq-state-changing-commands-regexp165,4889
-(defconst coq-state-preserving-commands-regexp167,4996
-(defconst coq-commands-regexp169,5107
-(defvar coq-retractable-instruct-regexp171,5184
-(defvar coq-non-retractable-instruct-regexp173,5274
-(defun coq-set-undo-limit 207,6151
-(defun build-list-id-from-string 211,6281
-(defun coq-last-prompt-info 223,6779
-(defun coq-last-prompt-info-safe 235,7311
-(defvar coq-last-but-one-statenum 241,7568
-(defvar coq-last-but-one-proofnum 247,7865
-(defvar coq-last-but-one-proofstack 250,7963
-(defsubst coq-get-span-statenum 253,8073
-(defsubst coq-get-span-proofnum 257,8188
-(defsubst coq-get-span-proofstack 261,8303
-(defsubst coq-set-span-statenum 265,8447
-(defsubst coq-get-span-goalcmd 269,8578
-(defsubst coq-set-span-goalcmd 273,8692
-(defsubst coq-set-span-proofnum 277,8822
-(defsubst coq-set-span-proofstack 281,8953
-(defsubst proof-last-locked-span 285,9113
-(defun proof-clone-buffer 291,9346
-(defun proof-store-buffer-win 305,9903
-(defun proof-store-response-win 311,10120
-(defun proof-store-goals-win 315,10247
-(defun coq-set-state-infos 327,10779
-(defun count-not-intersection 365,12761
-(defun coq-find-and-forget 396,14011
-(defvar coq-current-goal 419,15059
-(defun coq-goal-hyp 422,15124
-(defun coq-state-preserving-p 435,15556
-(defconst notation-print-kinds-table449,16057
-(defun coq-PrintScope 453,16224
-(defun coq-guess-or-ask-for-string 471,16773
-(defun coq-ask-do 485,17341
-(defsubst coq-put-into-brackets 494,17726
-(defsubst coq-put-into-quotes 497,17787
-(defun coq-SearchIsos 500,17847
-(defun coq-SearchConstant 508,18088
-(defun coq-Searchregexp 512,18181
-(defun coq-SearchRewrite 518,18324
-(defun coq-SearchAbout 522,18422
-(defun coq-Print 528,18568
-(defun coq-About 533,18693
-(defun coq-LocateConstant 538,18813
-(defun coq-LocateLibrary 543,18916
-(defun coq-LocateNotation 548,19034
-(defun coq-Pwd 556,19231
-(defun coq-Inspect 561,19331
-(defun coq-PrintSection(565,19431
-(defun coq-Print-implicit 569,19524
-(defun coq-Check 574,19675
-(defun coq-Show 579,19783
-(defun coq-Compile 593,20226
-(defun coq-guess-command-line 605,20544
-(defpacustom use-editing-holes 642,22097
-(defun coq-mode-config 651,22400
-(defun coq-shell-mode-config 743,25718
-(defun coq-goals-mode-config 785,27441
-(defun coq-response-config 792,27685
-(defpacustom print-fully-explicit 817,28510
-(defpacustom print-implicit 822,28658
-(defpacustom print-coercions 827,28824
-(defpacustom print-match-wildcards 832,28968
-(defpacustom print-elim-types 837,29148
-(defpacustom printing-depth 842,29314
-(defpacustom undo-depth 847,29475
-(defpacustom time-commands 852,29622
-(defpacustom undo-limit 856,29732
-(defpacustom auto-compile-vos 861,29834
-(defun coq-maybe-compile-buffer 890,30948
-(defun coq-ancestors-of 926,32476
-(defun coq-all-ancestors-of 949,33440
-(defun coq-process-require-command 960,33787
-(defun coq-included-children 965,33914
-(defun coq-process-file 986,34753
-(defun coq-preprocessing 1001,35292
-(defun coq-fake-constant-markup 1015,35727
-(defun coq-create-span-menu 1031,36332
-(defconst module-kinds-table1049,36845
-(defconst modtype-kinds-table1053,36994
-(defun coq-insert-section-or-module 1057,37123
-(defconst reqkinds-kinds-table1078,37973
-(defun coq-insert-requires 1082,38117
-(defun coq-end-Section 1095,38597
-(defun coq-insert-intros 1113,39175
-(defun coq-insert-infoH-hook 1125,39708
-(defun coq-insert-as 1130,39916
-(defun coq-insert-match 1147,40609
-(defun coq-insert-tactic 1176,41779
-(defun coq-insert-tactical 1182,42018
-(defun coq-insert-command 1188,42267
-(defun coq-insert-term 1194,42511
-(define-key coq-keymap 1200,42708
-(define-key coq-keymap 1201,42766
-(define-key coq-keymap 1202,42823
-(define-key coq-keymap 1203,42892
-(define-key coq-keymap 1204,42948
-(define-key coq-keymap 1205,42997
-(define-key coq-keymap 1206,43055
-(define-key coq-keymap 1207,43115
-(define-key coq-keymap 1208,43180
-(define-key coq-keymap 1210,43243
-(define-key coq-keymap 1211,43302
-(define-key coq-keymap 1215,43427
-(define-key coq-keymap 1217,43483
-(define-key coq-keymap 1218,43533
-(define-key coq-keymap 1219,43583
-(define-key coq-keymap 1220,43639
-(define-key coq-keymap 1221,43689
-(define-key coq-keymap 1222,43743
-(define-key coq-keymap 1223,43802
-(define-key coq-goals-mode-map 1226,43863
-(define-key coq-goals-mode-map 1227,43945
-(define-key coq-goals-mode-map 1228,44027
-(define-key coq-goals-mode-map 1229,44114
-(define-key coq-goals-mode-map 1230,44196
-(defvar last-coq-error-location 1239,44498
-(defun coq-get-last-error-location 1247,44882
-(defun coq-highlight-error 1297,47439
-(defvar coq-allow-highlight-error 1328,48635
-(defun coq-decide-highlight-error 1335,48961
-(defun coq-highlight-error-hook 1340,49146
-(defun first-word-of-buffer 1351,49539
-(defun coq-show-first-goal 1359,49742
-(defvar coq-modeline-string2 1376,50437
-(defvar coq-modeline-string1 1377,50481
-(defvar coq-modeline-string0 1378,50524
-(defun coq-build-subgoals-string 1379,50569
-(defun coq-update-minor-mode-alist 1384,50735
-(defun is-not-split-vertic 1410,51806
-(defun optim-resp-windows 1419,52246
-
 coq/coq-indent.el,2223
 (defconst coq-any-command-regexp20,368
 (defconst coq-indent-inner-regexp23,459
@@ -334,15 +179,160 @@ coq/coq-unicode-tokens.el,454
 (defconst coq-control-region-format-regexp 251,6639
 (defconst coq-control-regions253,6722
 
-demoisa/demoisa.el,349
-(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
+coq/coq.el,6009
+(defcustom coq-translate-to-v8 48,1381
+(defun coq-build-prog-args 54,1561
+(defcustom coq-compile-file-command 64,1857
+(defcustom coq-use-makefile 72,2176
+(defcustom coq-default-undo-limit 80,2399
+(defconst coq-shell-init-cmd85,2527
+(defcustom coq-prog-env 91,2654
+(defconst coq-shell-restart-cmd 99,2904
+(defvar coq-shell-prompt-pattern101,2958
+(defvar coq-shell-cd 109,3261
+(defvar coq-shell-proof-completed-regexp 113,3421
+(defvar coq-goal-regexp116,3576
+(defun coq-library-directory 123,3690
+(defcustom coq-tags 130,3869
+(defconst coq-interrupt-regexp 135,4019
+(defcustom coq-www-home-page 140,4140
+(defvar coq-outline-regexp147,4308
+(defvar coq-outline-heading-end-regexp 154,4520
+(defvar coq-shell-outline-regexp 156,4574
+(defvar coq-shell-outline-heading-end-regexp 157,4624
+(defconst coq-state-preserving-tactics-regexp163,4789
+(defconst coq-state-changing-commands-regexp165,4889
+(defconst coq-state-preserving-commands-regexp167,4996
+(defconst coq-commands-regexp169,5107
+(defvar coq-retractable-instruct-regexp171,5184
+(defvar coq-non-retractable-instruct-regexp173,5274
+(defun coq-set-undo-limit 207,6151
+(defun build-list-id-from-string 211,6281
+(defun coq-last-prompt-info 223,6779
+(defun coq-last-prompt-info-safe 235,7311
+(defvar coq-last-but-one-statenum 241,7568
+(defvar coq-last-but-one-proofnum 248,7866
+(defvar coq-last-but-one-proofstack 251,7964
+(defsubst coq-get-span-statenum 254,8074
+(defsubst coq-get-span-proofnum 258,8189
+(defsubst coq-get-span-proofstack 262,8304
+(defsubst coq-set-span-statenum 266,8448
+(defsubst coq-get-span-goalcmd 270,8579
+(defsubst coq-set-span-goalcmd 274,8693
+(defsubst coq-set-span-proofnum 278,8823
+(defsubst coq-set-span-proofstack 282,8954
+(defsubst proof-last-locked-span 286,9114
+(defun proof-clone-buffer 292,9347
+(defun proof-store-buffer-win 306,9904
+(defun proof-store-response-win 312,10121
+(defun proof-store-goals-win 316,10248
+(defun coq-set-state-infos 328,10780
+(defun count-not-intersection 365,12866
+(defun coq-find-and-forget 396,14116
+(defvar coq-current-goal 416,15020
+(defun coq-goal-hyp 419,15085
+(defun coq-state-preserving-p 432,15517
+(defconst notation-print-kinds-table446,16018
+(defun coq-PrintScope 450,16185
+(defun coq-guess-or-ask-for-string 468,16734
+(defun coq-ask-do 482,17302
+(defsubst coq-put-into-brackets 491,17687
+(defsubst coq-put-into-quotes 494,17748
+(defun coq-SearchIsos 497,17808
+(defun coq-SearchConstant 505,18049
+(defun coq-Searchregexp 509,18142
+(defun coq-SearchRewrite 515,18285
+(defun coq-SearchAbout 519,18383
+(defun coq-Print 525,18529
+(defun coq-About 530,18654
+(defun coq-LocateConstant 535,18774
+(defun coq-LocateLibrary 540,18877
+(defun coq-LocateNotation 545,18995
+(defun coq-Pwd 553,19192
+(defun coq-Inspect 558,19292
+(defun coq-PrintSection(562,19392
+(defun coq-Print-implicit 566,19485
+(defun coq-Check 571,19636
+(defun coq-Show 576,19744
+(defun coq-Compile 590,20187
+(defun coq-guess-command-line 602,20505
+(defpacustom use-editing-holes 639,22058
+(defun coq-mode-config 648,22361
+(defun coq-shell-mode-config 740,25664
+(defun coq-goals-mode-config 782,27387
+(defun coq-response-config 789,27631
+(defpacustom print-fully-explicit 814,28456
+(defpacustom print-implicit 819,28604
+(defpacustom print-coercions 824,28770
+(defpacustom print-match-wildcards 829,28914
+(defpacustom print-elim-types 834,29094
+(defpacustom printing-depth 839,29260
+(defpacustom undo-depth 844,29421
+(defpacustom time-commands 849,29568
+(defpacustom undo-limit 853,29678
+(defpacustom auto-compile-vos 858,29780
+(defun coq-maybe-compile-buffer 887,30894
+(defun coq-ancestors-of 923,32422
+(defun coq-all-ancestors-of 946,33386
+(defun coq-process-require-command 957,33733
+(defun coq-included-children 962,33860
+(defun coq-process-file 983,34699
+(defun coq-preprocessing 998,35238
+(defun coq-fake-constant-markup 1012,35673
+(defun coq-create-span-menu 1028,36278
+(defconst module-kinds-table1046,36791
+(defconst modtype-kinds-table1050,36940
+(defun coq-insert-section-or-module 1054,37069
+(defconst reqkinds-kinds-table1075,37919
+(defun coq-insert-requires 1079,38063
+(defun coq-end-Section 1092,38543
+(defun coq-insert-intros 1110,39121
+(defun coq-insert-infoH-hook 1122,39654
+(defun coq-insert-as 1127,39862
+(defun coq-insert-match 1144,40555
+(defun coq-insert-tactic 1173,41725
+(defun coq-insert-tactical 1179,41964
+(defun coq-insert-command 1185,42213
+(defun coq-insert-term 1191,42457
+(define-key coq-keymap 1197,42654
+(define-key coq-keymap 1198,42712
+(define-key coq-keymap 1199,42769
+(define-key coq-keymap 1200,42838
+(define-key coq-keymap 1201,42894
+(define-key coq-keymap 1202,42943
+(define-key coq-keymap 1203,43001
+(define-key coq-keymap 1204,43061
+(define-key coq-keymap 1205,43126
+(define-key coq-keymap 1207,43189
+(define-key coq-keymap 1208,43248
+(define-key coq-keymap 1212,43373
+(define-key coq-keymap 1214,43429
+(define-key coq-keymap 1215,43479
+(define-key coq-keymap 1216,43529
+(define-key coq-keymap 1217,43585
+(define-key coq-keymap 1218,43635
+(define-key coq-keymap 1219,43689
+(define-key coq-keymap 1220,43748
+(define-key coq-goals-mode-map 1223,43809
+(define-key coq-goals-mode-map 1224,43891
+(define-key coq-goals-mode-map 1225,43973
+(define-key coq-goals-mode-map 1226,44060
+(define-key coq-goals-mode-map 1227,44142
+(defvar last-coq-error-location 1236,44444
+(defun coq-get-last-error-location 1244,44828
+(defun coq-highlight-error 1294,47385
+(defvar coq-allow-highlight-error 1325,48581
+(defun coq-decide-highlight-error 1332,48907
+(defun coq-highlight-error-hook 1337,49092
+(defun first-word-of-buffer 1348,49485
+(defun coq-show-first-goal 1356,49688
+(defvar coq-modeline-string2 1373,50383
+(defvar coq-modeline-string1 1374,50427
+(defvar coq-modeline-string0 1375,50470
+(defun coq-build-subgoals-string 1376,50515
+(defun coq-update-minor-mode-alist 1381,50681
+(defun is-not-split-vertic 1407,51752
+(defun optim-resp-windows 1416,52192
 
 hol98/hol98.el,121
 (defvar hol98-keywords 17,419
@@ -385,46 +375,6 @@ isar/isabelle-system.el,1254
 isar/isar-autotest.el,31
 (defvar isar-long-tests 8,187
 
-isar/isar.el,1595
-(defcustom isar-keywords-name 40,919
-(defpgdefault completion-table 56,1430
-(defcustom isar-web-page58,1483
-(defun isar-strip-terminators 72,1833
-(defun isar-markup-ml 85,2210
-(defun isar-mode-config-set-variables 90,2345
-(defun isar-shell-mode-config-set-variables 155,5142
-(defun isar-set-proof-find-theorems-command 236,8276
-(defpacustom use-find-theorems-form 242,8460
-(defun isar-set-undo-commands 247,8626
-(defpacustom use-linear-undo 258,9077
-(defun isar-configure-from-settings 263,9235
-(defun isar-remove-file 271,9379
-(defun isar-shell-compute-new-files-list 283,9683
-(define-derived-mode isar-shell-mode 302,10255
-(define-derived-mode isar-response-mode 307,10382
-(define-derived-mode isar-goals-mode 312,10515
-(define-derived-mode isar-mode 317,10641
-(defpgdefault menu-entries370,12358
-(defun isar-set-command 401,13552
-(defpgdefault help-menu-entries 406,13682
-(defun isar-count-undos 409,13758
-(defun isar-find-and-forget 435,14740
-(defun isar-goal-command-p 471,16092
-(defun isar-global-save-command-p 476,16269
-(defvar isar-current-goal 497,17053
-(defun isar-state-preserving-p 500,17119
-(defvar isar-shell-current-line-width 525,17968
-(defun isar-shell-adjust-line-width 530,18160
-(defsubst isar-string-wrapping 553,18925
-(defsubst isar-positions-of 562,19119
-(defcustom isar-wrap-commands-singly 568,19324
-(defun isar-command-wrapping 574,19520
-(defun isar-preprocessing 582,19834
-(defun isar-mode-config 600,20385
-(defun isar-shell-mode-config 614,21038
-(defun isar-response-mode-config 624,21387
-(defun isar-goals-mode-config 634,21722
-
 isar/isar-find-theorems.el,779
 (defvar isar-find-theorems-data 19,565
 (defun isar-find-theorems-minibuffer 35,1039
@@ -602,21 +552,63 @@ isar/isar-unicode-tokens.el,1363
 (defun isar-init-shortcut-alists 632,16809
 (defconst isar-tokens-customizable-variables653,17472
 
-lclam/lclam.el,524
-(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
+isar/isar.el,1595
+(defcustom isar-keywords-name 39,916
+(defpgdefault completion-table 55,1427
+(defcustom isar-web-page57,1480
+(defun isar-strip-terminators 71,1830
+(defun isar-markup-ml 83,2186
+(defun isar-mode-config-set-variables 88,2321
+(defun isar-shell-mode-config-set-variables 153,5118
+(defun isar-set-proof-find-theorems-command 235,8304
+(defpacustom use-find-theorems-form 241,8488
+(defun isar-set-undo-commands 246,8654
+(defpacustom use-linear-undo 260,9246
+(defun isar-configure-from-settings 265,9406
+(defun isar-remove-file 273,9550
+(defun isar-shell-compute-new-files-list 285,9854
+(define-derived-mode isar-shell-mode 304,10424
+(define-derived-mode isar-response-mode 309,10551
+(define-derived-mode isar-goals-mode 314,10684
+(define-derived-mode isar-mode 319,10810
+(defpgdefault menu-entries371,12525
+(defun isar-set-command 402,13719
+(defpgdefault help-menu-entries 407,13849
+(defun isar-count-undos 410,13925
+(defun isar-find-and-forget 436,14907
+(defun isar-goal-command-p 472,16259
+(defun isar-global-save-command-p 477,16436
+(defvar isar-current-goal 498,17220
+(defun isar-state-preserving-p 501,17286
+(defvar isar-shell-current-line-width 526,18135
+(defun isar-shell-adjust-line-width 531,18327
+(defsubst isar-string-wrapping 554,19092
+(defsubst isar-positions-of 563,19286
+(defcustom isar-wrap-commands-singly 569,19491
+(defun isar-command-wrapping 575,19687
+(defun isar-preprocessing 583,20001
+(defun isar-mode-config 601,20552
+(defun isar-shell-mode-config 615,21205
+(defun isar-response-mode-config 625,21554
+(defun isar-goals-mode-config 635,21889
+
+lego/lego-syntax.el,600
+(defconst lego-keywords-goal 15,358
+(defconst lego-keywords-save 17,401
+(defconst lego-commands19,472
+(defconst lego-keywords31,1030
+(defconst lego-tacticals 36,1207
+(defconst lego-error-regexp 39,1315
+(defvar lego-id 42,1473
+(defvar lego-ids 44,1500
+(defconst lego-arg-list-regexp 48,1696
+(defun lego-decl-defn-regexp 51,1812
+(defconst lego-definiendum-alternative-regexp59,2184
+(defvar lego-font-lock-terms63,2368
+(defconst lego-goal-with-hole-regexp89,3221
+(defconst lego-save-with-hole-regexp94,3443
+(defvar lego-font-lock-keywords-199,3660
+(defun lego-init-syntax-table 110,4122
 
 lego/lego.el,1636
 (defcustom lego-tags 21,535
@@ -660,41 +652,6 @@ lego/lego.el,1636
 (defun lego-shell-mode-config 373,12770
 (defun lego-goals-mode-config 420,14437
 
-lego/lego-syntax.el,600
-(defconst lego-keywords-goal 15,358
-(defconst lego-keywords-save 17,401
-(defconst lego-commands19,472
-(defconst lego-keywords31,1030
-(defconst lego-tacticals 36,1207
-(defconst lego-error-regexp 39,1315
-(defvar lego-id 42,1473
-(defvar lego-ids 44,1500
-(defconst lego-arg-list-regexp 48,1696
-(defun lego-decl-defn-regexp 51,1812
-(defconst lego-definiendum-alternative-regexp59,2184
-(defvar lego-font-lock-terms63,2368
-(defconst lego-goal-with-hole-regexp89,3221
-(defconst lego-save-with-hole-regexp94,3443
-(defvar lego-font-lock-keywords-199,3660
-(defun lego-init-syntax-table 110,4122
-
-phox/phox.el,555
-(defcustom phox-prog-name 32,916
-(defcustom phox-web-page37,1018
-(defcustom phox-doc-dir43,1168
-(defcustom phox-lib-dir49,1315
-(defcustom phox-tags-program55,1458
-(defcustom phox-tags-doc61,1637
-(defcustom phox-etags67,1774
-(defpgdefault menu-entries88,2224
-(defun phox-config 102,2417
-(defun phox-shell-config 146,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 19,619
 (defun phox-prog-flags-modify(21,687
@@ -833,90 +790,22 @@ phox/phox-tags.el,305
 (defun phox-complete-tag(69,2091
 (defvar phox-tags-menu76,2200
 
-plastic/plastic.el,2759
-(defcustom plastic-tags 29,608
-(defcustom plastic-test-all-name 34,740
-(defvar plastic-lit-string41,931
-(defcustom plastic-help-menu-list45,1043
-(defvar plastic-shell-handle-output59,1536
-(defconst plastic-process-config67,1837
-(defconst plastic-pretty-set-width 74,2085
-(defconst plastic-interrupt-regexp 78,2233
-(defcustom plastic-www-home-page 84,2354
-(defcustom plastic-www-latest-release89,2491
-(defcustom plastic-www-refcard95,2661
-(defcustom plastic-library-www-page101,2792
-(defcustom plastic-base111,3007
-(defvar plastic-prog-name119,3178
-(defun plastic-set-default-env-vars 123,3285
-(defvar plastic-shell-cd131,3522
-(defvar plastic-shell-proof-completed-regexp 135,3662
-(defvar plastic-save-command-regexp138,3805
-(defvar plastic-goal-command-regexp140,3901
-(defvar plastic-kill-goal-command143,3998
-(defvar plastic-forget-id-command145,4098
-(defvar plastic-undoable-commands-regexp148,4178
-(defvar plastic-goal-regexp 160,4625
-(defvar plastic-outline-regexp162,4673
-(defvar plastic-outline-heading-end-regexp 168,4851
-(defvar plastic-shell-outline-regexp 170,4907
-(defvar plastic-shell-outline-heading-end-regexp 171,4965
-(defvar plastic-error-occurred173,5036
-(define-derived-mode plastic-shell-mode 182,5353
-(define-derived-mode plastic-mode 188,5535
-(define-derived-mode plastic-goals-mode 204,6052
-(defun plastic-count-undos 213,6397
-(defun plastic-goal-command-p 234,7284
-(defun plastic-find-and-forget 239,7476
-(defun plastic-goal-hyp 278,8887
-(defun plastic-state-preserving-p 289,9136
-(defvar plastic-shell-current-line-width 312,10111
-(defun plastic-shell-adjust-line-width 320,10427
-(defun plastic-mode-config 345,11436
-(defun plastic-show-shell-buffer 434,14695
-(defun plastic-equal-module-filename 440,14798
-(defun plastic-shell-compute-new-files-list 446,15076
-(defun plastic-shell-mode-config 458,15470
-(defun plastic-goals-mode-config 506,17273
-(defun plastic-small-bar 518,17560
-(defun plastic-large-bar 520,17649
-(defun plastic-preprocessing 522,17787
-(defun plastic-all-ctxt 574,19590
-(defun plastic-send-one-undo 581,19759
-(defun plastic-minibuf-cmd 591,20065
-(defun plastic-minibuf 603,20537
-(defun plastic-synchro 610,20743
-(defun plastic-send-minibuf 615,20884
-(defun plastic-had-error 623,21192
-(defun plastic-reset-error 627,21367
-(defun plastic-call-if-no-error 630,21506
-(defun plastic-show-shell 635,21710
-(define-key plastic-keymap 640,21838
-(define-key plastic-keymap 641,21899
-(define-key plastic-keymap 642,21960
-(define-key plastic-keymap 643,22020
-(define-key plastic-keymap 644,22079
-(define-key plastic-keymap 645,22138
-(defalias 'proof-toolbar-command proof-toolbar-command
655,22387
-(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
656,22438
-
-plastic/plastic-syntax.el,648
-(defconst plastic-keywords-goal 18,536
-(defconst plastic-keywords-save 20,582
-(defconst plastic-commands22,656
-(defconst plastic-keywords35,1263
-(defconst plastic-tacticals 40,1446
-(defconst plastic-error-regexp 43,1557
-(defvar plastic-id 46,1690
-(defvar plastic-ids 48,1720
-(defconst plastic-arg-list-regexp 52,1928
-(defun plastic-decl-defn-regexp 55,2047
-(defconst plastic-definiendum-alternative-regexp63,2428
-(defvar plastic-font-lock-terms67,2621
-(defconst plastic-goal-with-hole-regexp89,3331
-(defconst plastic-save-with-hole-regexp94,3557
-(defvar plastic-font-lock-keywords-199,3783
-(defun plastic-init-syntax-table 108,4175
+phox/phox.el,555
+(defcustom phox-prog-name 32,916
+(defcustom phox-web-page37,1018
+(defcustom phox-doc-dir43,1168
+(defcustom phox-lib-dir49,1315
+(defcustom phox-tags-program55,1458
+(defcustom phox-tags-doc61,1637
+(defcustom phox-etags67,1774
+(defpgdefault menu-entries88,2224
+(defun phox-config 102,2417
+(defun phox-shell-config 146,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
 
 generic/pg-assoc.el,81
 (defun proof-associated-buffers 33,973
@@ -1021,25 +910,25 @@ generic/pg-pbrpm.el,1808
 (defun pg-pbrpm-eliminate-id 198,6959
 (defun pg-pbrpm-build-menu 206,7205
 (defun pg-pbrpm-setup-span 269,9525
-(defun pg-pbrpm-run-command 329,11840
-(defun pg-pbrpm-get-pos-info 362,13361
-(defun pg-pbrpm-get-region-info 404,14660
-(defun pg-pbrpm-auto-select-around-point 415,15072
-(defun pg-pbrpm-translate-position 430,15596
-(defun pg-pbrpm-process-click 438,15850
-(defvar pg-pbrpm-remember-region-selected-region 458,16875
-(defvar pg-pbrpm-regions-list 459,16929
-(defun pg-pbrpm-erase-regions-list 461,16965
-(defun pg-pbrpm-filter-regions-list 470,17273
-(defface pg-pbrpm-multiple-selection-face477,17536
-(defface pg-pbrpm-menu-input-face485,17738
-(defun pg-pbrpm-do-remember-region 493,17928
-(defun pg-pbrpm-remember-region-drag-up-hook 514,18776
-(defun pg-pbrpm-remember-region-click-hook 518,18947
-(defun pg-pbrpm-remember-region 523,19132
-(defun pg-pbrpm-process-region 537,19846
-(defun pg-pbrpm-process-regions-list 555,20575
-(defun pg-pbrpm-region-expression 559,20758
+(defun pg-pbrpm-run-command 329,11824
+(defun pg-pbrpm-get-pos-info 362,13345
+(defun pg-pbrpm-get-region-info 404,14644
+(defun pg-pbrpm-auto-select-around-point 415,15056
+(defun pg-pbrpm-translate-position 430,15580
+(defun pg-pbrpm-process-click 438,15834
+(defvar pg-pbrpm-remember-region-selected-region 458,16859
+(defvar pg-pbrpm-regions-list 459,16913
+(defun pg-pbrpm-erase-regions-list 461,16949
+(defun pg-pbrpm-filter-regions-list 470,17257
+(defface pg-pbrpm-multiple-selection-face477,17520
+(defface pg-pbrpm-menu-input-face485,17722
+(defun pg-pbrpm-do-remember-region 493,17912
+(defun pg-pbrpm-remember-region-drag-up-hook 514,18760
+(defun pg-pbrpm-remember-region-click-hook 518,18931
+(defun pg-pbrpm-remember-region 523,19116
+(defun pg-pbrpm-process-region 537,19830
+(defun pg-pbrpm-process-regions-list 555,20559
+(defun pg-pbrpm-region-expression 559,20742
 
 generic/pg-pgip.el,2931
 (defalias 'pg-pgip-debug pg-pgip-debug
38,1032
@@ -1112,38 +1001,38 @@ generic/pg-pgip.el,2931
 (defconst pg-pgip-end-element-regexp 677,22923
 
 generic/pg-response.el,1292
-(deflocal pg-response-eagerly-raise 32,789
-(define-derived-mode proof-response-mode 42,1014
-(define-key proof-response-mode-map 70,1968
-(define-key proof-response-mode-map 71,2039
-(define-key proof-response-mode-map 72,2093
-(defun proof-response-config-done 76,2179
-(defvar pg-response-special-display-regexp 87,2525
-(defconst proof-multiframe-parameters91,2692
-(defun proof-multiple-frames-enable 100,2982
-(defun proof-three-window-enable 110,3310
-(defun proof-select-three-b 113,3373
-(defun proof-display-three-b 128,3842
-(defvar pg-frame-configuration 139,4232
-(defun pg-cache-frame-configuration 143,4379
-(defun proof-layout-windows 147,4550
-(defun proof-delete-other-frames 187,6337
-(defvar pg-response-erase-flag 218,7425
-(defun pg-response-maybe-erase222,7554
-(defun pg-response-display 252,8658
-(defun pg-response-display-with-face 277,9441
-(defun pg-response-clear-displays 305,10287
-(defun pg-response-message 318,10806
-(defun pg-response-warning 324,11041
-(defun proof-next-error 339,11447
-(defun pg-response-has-error-location 417,14256
-(defvar proof-trace-last-fontify-pos 439,15069
-(defun proof-trace-fontify-pos 441,15112
-(defun proof-trace-buffer-display 449,15425
-(defun proof-trace-buffer-finish 460,15769
-(defun pg-thms-buffer-clear 478,16112
-
-generic/pg-user.el,3657
+(deflocal pg-response-eagerly-raise 32,791
+(define-derived-mode proof-response-mode 42,1016
+(define-key proof-response-mode-map 70,1970
+(define-key proof-response-mode-map 71,2041
+(define-key proof-response-mode-map 72,2095
+(defun proof-response-config-done 76,2181
+(defvar pg-response-special-display-regexp 87,2527
+(defconst proof-multiframe-parameters91,2694
+(defun proof-multiple-frames-enable 100,2984
+(defun proof-three-window-enable 110,3312
+(defun proof-select-three-b 113,3375
+(defun proof-display-three-b 128,3866
+(defvar pg-frame-configuration 139,4256
+(defun pg-cache-frame-configuration 143,4403
+(defun proof-layout-windows 147,4574
+(defun proof-delete-other-frames 187,6361
+(defvar pg-response-erase-flag 218,7449
+(defun pg-response-maybe-erase222,7578
+(defun pg-response-display 252,8682
+(defun pg-response-display-with-face 277,9465
+(defun pg-response-clear-displays 305,10311
+(defun pg-response-message 318,10830
+(defun pg-response-warning 324,11065
+(defun proof-next-error 339,11471
+(defun pg-response-has-error-location 417,14280
+(defvar proof-trace-last-fontify-pos 439,15093
+(defun proof-trace-fontify-pos 441,15136
+(defun proof-trace-buffer-display 449,15449
+(defun proof-trace-buffer-finish 460,15793
+(defun pg-thms-buffer-clear 478,16136
+
+generic/pg-user.el,3654
 (defun proof-script-new-command-advance 42,1232
 (defun proof-maybe-follow-locked-end 85,2994
 (defun proof-goto-command-start 112,3870
@@ -1160,76 +1049,76 @@ generic/pg-user.el,3657
 (defun proof-mouse-goto-point 271,9143
 (defvar proof-minibuffer-history 286,9419
 (defun proof-minibuffer-cmd 289,9514
-(defun proof-frob-locked-end 333,11136
-(defmacro proof-if-setting-configured 394,13074
-(defmacro proof-define-assistant-command 402,13343
-(defmacro proof-define-assistant-command-witharg 415,13798
-(defun proof-issue-new-command 435,14620
-(defun proof-cd-sync 475,15843
-(defun proof-electric-terminator-enable 531,17617
-(defun proof-electric-terminator 538,17861
-(defun proof-add-completions 564,18684
-(defun proof-script-complete 589,19573
-(defun pg-copy-span-contents 603,19882
-(defun pg-numth-span-higher-or-lower 620,20440
-(defun pg-control-span-of 646,21186
-(defun pg-move-span-contents 652,21390
-(defun pg-fixup-children-spans 704,23566
-(defun pg-move-region-down 714,23823
-(defun pg-move-region-up 723,24116
-(defun proof-forward-command 753,24944
-(defun proof-backward-command 774,25665
-(defun pg-pos-for-event 796,26009
-(defun pg-span-for-event 802,26230
-(defun pg-span-context-menu 806,26374
-(defun pg-toggle-visibility 821,26822
-(defun pg-create-in-span-context-menu 830,27129
-(defun pg-span-undo 859,28343
-(defun pg-goals-buffers-hint 905,29745
-(defun pg-slow-fontify-tracing-hint 909,29927
-(defun pg-response-buffers-hint 913,30098
-(defun pg-jump-to-end-hint 925,30513
-(defun pg-processing-complete-hint 929,30642
-(defun pg-next-error-hint 946,31362
-(defun pg-hint 951,31514
-(defun pg-identifier-under-mouse-query 967,32104
-(defun pg-identifier-near-point-query 977,32413
-(defvar proof-query-identifier-collection 1005,33310
-(defvar proof-query-identifier-history 1006,33357
-(defun proof-query-identifier 1008,33402
-(defun pg-identifier-query 1019,33721
-(defun proof-imenu-enable 1052,34887
-(defvar pg-input-ring 1088,36209
-(defvar pg-input-ring-index 1091,36266
-(defvar pg-stored-incomplete-input 1094,36338
-(defun pg-previous-input 1097,36441
-(defun pg-next-input 1111,36898
-(defun pg-delete-input 1116,37020
-(defun pg-get-old-input 1129,37358
-(defun pg-restore-input 1143,37749
-(defun pg-search-start 1154,38039
-(defun pg-regexp-arg 1166,38531
-(defun pg-search-arg 1178,38979
-(defun pg-previous-matching-input-string-position 1192,39396
-(defun pg-previous-matching-input 1219,40561
-(defun pg-next-matching-input 1238,41411
-(defvar pg-matching-input-from-input-string 1246,41794
-(defun pg-previous-matching-input-from-input 1250,41908
-(defun pg-next-matching-input-from-input 1268,42673
-(defun pg-add-to-input-history 1279,43052
-(defun pg-remove-from-input-history 1291,43505
-(defun  pg-clear-input-ring 1302,43885
-(define-key proof-mode-map 1319,44355
-(define-key proof-mode-map 1320,44415
-(defun pg-protected-undo 1322,44487
-(defun pg-protected-undo-1 1357,45877
-(defun next-undo-elt 1388,47311
-(defvar proof-autosend-timer 1415,48267
-(deflocal proof-autosend-error-point 1417,48328
-(defun proof-autosend-enable 1421,48452
-(defun proof-autosend-delay 1435,48993
-(defun proof-autosend-loop 1439,49126
-(defun proof-autosend-loop-all 1445,49311
+(defun proof-frob-locked-end 328,10921
+(defmacro proof-if-setting-configured 389,12859
+(defmacro proof-define-assistant-command 397,13128
+(defmacro proof-define-assistant-command-witharg 410,13583
+(defun proof-issue-new-command 430,14405
+(defun proof-cd-sync 470,15628
+(defun proof-electric-terminator-enable 523,17298
+(defun proof-electric-terminator 530,17542
+(defun proof-add-completions 555,18346
+(defun proof-script-complete 580,19235
+(defun pg-copy-span-contents 594,19544
+(defun pg-numth-span-higher-or-lower 611,20102
+(defun pg-control-span-of 637,20848
+(defun pg-move-span-contents 643,21052
+(defun pg-fixup-children-spans 695,23228
+(defun pg-move-region-down 705,23485
+(defun pg-move-region-up 714,23778
+(defun proof-forward-command 744,24606
+(defun proof-backward-command 765,25327
+(defun pg-pos-for-event 787,25671
+(defun pg-span-for-event 793,25892
+(defun pg-span-context-menu 797,26036
+(defun pg-toggle-visibility 812,26484
+(defun pg-create-in-span-context-menu 821,26791
+(defun pg-span-undo 850,28005
+(defun pg-goals-buffers-hint 896,29388
+(defun pg-slow-fontify-tracing-hint 900,29570
+(defun pg-response-buffers-hint 904,29741
+(defun pg-jump-to-end-hint 916,30156
+(defun pg-processing-complete-hint 920,30285
+(defun pg-next-error-hint 937,31005
+(defun pg-hint 942,31157
+(defun pg-identifier-under-mouse-query 958,31747
+(defun pg-identifier-near-point-query 968,32056
+(defvar proof-query-identifier-collection 996,32953
+(defvar proof-query-identifier-history 997,33000
+(defun proof-query-identifier 999,33045
+(defun pg-identifier-query 1010,33364
+(defun proof-imenu-enable 1043,34512
+(defvar pg-input-ring 1079,35815
+(defvar pg-input-ring-index 1082,35872
+(defvar pg-stored-incomplete-input 1085,35944
+(defun pg-previous-input 1088,36047
+(defun pg-next-input 1102,36504
+(defun pg-delete-input 1107,36626
+(defun pg-get-old-input 1120,36964
+(defun pg-restore-input 1134,37355
+(defun pg-search-start 1145,37645
+(defun pg-regexp-arg 1157,38137
+(defun pg-search-arg 1169,38585
+(defun pg-previous-matching-input-string-position 1183,39002
+(defun pg-previous-matching-input 1210,40167
+(defun pg-next-matching-input 1229,41017
+(defvar pg-matching-input-from-input-string 1237,41400
+(defun pg-previous-matching-input-from-input 1241,41514
+(defun pg-next-matching-input-from-input 1259,42279
+(defun pg-add-to-input-history 1270,42658
+(defun pg-remove-from-input-history 1282,43111
+(defun  pg-clear-input-ring 1293,43491
+(define-key proof-mode-map 1310,43961
+(define-key proof-mode-map 1311,44021
+(defun pg-protected-undo 1313,44093
+(defun pg-protected-undo-1 1348,45483
+(defun next-undo-elt 1379,46917
+(defvar proof-autosend-timer 1406,47873
+(deflocal proof-autosend-error-point 1408,47934
+(defun proof-autosend-enable 1412,48058
+(defun proof-autosend-delay 1426,48599
+(defun proof-autosend-loop 1430,48732
+(defun proof-autosend-loop-all 1436,48917
 
 generic/pg-vars.el,1491
 (defvar proof-assistant-cusgrp 22,389
@@ -1547,7 +1436,7 @@ generic/proof-maths-menu.el,83
 (defun proof-maths-menu-set-global 32,906
 (defun proof-maths-menu-enable 46,1357
 
-generic/proof-menu.el,2026
+generic/proof-menu.el,2074
 (defvar proof-display-some-buffers-count 36,816
 (defun proof-display-some-buffers 38,861
 (defun proof-menu-define-keys 95,2988
@@ -1590,137 +1479,136 @@ generic/proof-menu.el,2026
 (defun proof-assistant-invisible-command-ifposs 851,30043
 (defun proof-maybe-askprefs 873,31013
 (defun proof-assistant-settings-cmd 879,31206
-(defvar proof-assistant-format-table896,31861
-(defun proof-assistant-format-bool 904,32231
-(defun proof-assistant-format-int 907,32344
-(defun proof-assistant-format-string 910,32436
-(defun proof-assistant-format 913,32534
+(defun proof-assistant-settings-cmds 887,31490
+(defvar proof-assistant-format-table897,31832
+(defun proof-assistant-format-bool 905,32202
+(defun proof-assistant-format-int 908,32315
+(defun proof-assistant-format-string 911,32407
+(defun proof-assistant-format 914,32505
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 43,1439
 (defun proof-mmm-enable 58,1978
 
-generic/proof-script.el,5504
-(deflocal proof-active-buffer-fake-minor-mode 45,1360
-(deflocal proof-script-buffer-file-name 48,1486
-(deflocal pg-script-portions 55,1896
-(defun proof-next-element-count 65,2116
-(defun proof-element-id 71,2358
-(defun proof-next-element-id 75,2527
-(deflocal proof-locked-span 111,3853
-(deflocal proof-queue-span 118,4119
-(deflocal proof-overlay-arrow 127,4605
-(defun proof-span-give-warning 133,4732
-(defun proof-span-read-only 139,4912
-(defun proof-strict-read-only 148,5285
-(defsubst proof-set-queue-endpoints 158,5663
-(defun proof-set-overlay-arrow 162,5804
-(defsubst proof-set-locked-endpoints 173,6142
-(defsubst proof-detach-queue 178,6318
-(defsubst proof-detach-locked 183,6457
-(defsubst proof-set-queue-start 190,6682
-(defsubst proof-set-locked-end 194,6808
-(defsubst proof-set-queue-end 206,7278
-(defun proof-init-segmentation 217,7575
-(defun proof-colour-locked 249,8970
-(defun proof-colour-locked-span 256,9243
-(defun proof-sticky-errors 262,9516
-(defun proof-restart-buffers 275,9932
-(defun proof-script-buffers-with-spans 297,10751
-(defun proof-script-remove-all-spans-and-deactivate 307,11107
-(defun proof-script-clear-queue-spans-on-error 311,11297
-(defun proof-script-delete-spans 337,12314
-(defun proof-script-delete-secondary-spans 342,12513
-(defun proof-unprocessed-begin 355,12802
-(defun proof-script-end 363,13056
-(defun proof-queue-or-locked-end 372,13366
-(defun proof-locked-region-full-p 391,13959
-(defun proof-locked-region-empty-p 400,14231
-(defun proof-only-whitespace-to-locked-region-p 404,14381
-(defun proof-in-locked-region-p 414,14730
-(defun proof-goto-end-of-locked 426,14987
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 443,15746
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 455,16260
-(defun proof-end-of-locked-visible-p 468,16844
-(defvar pg-idioms 487,17437
-(defun pg-clear-script-portions 490,17533
-(defun pg-remove-element 496,17768
-(defun pg-get-element 504,18071
-(defun pg-add-element 514,18386
-(defun pg-set-element-span-invisible 562,20365
-(defun pg-open-invisible-span 566,20525
-(defun pg-make-element-invisible 571,20696
-(defun pg-make-element-visible 576,20907
-(defun pg-toggle-element-span-visibility 581,21101
-(defun pg-toggle-element-visibility 587,21264
-(defun pg-show-all-portions 593,21527
-(defun pg-show-all-proofs 612,22235
-(defun pg-hide-all-proofs 617,22363
-(defun pg-add-proof-element 622,22494
-(defun pg-span-name 637,23265
-(defvar pg-span-context-menu-keymap658,23965
-(defun pg-last-output-displayform 665,24203
-(defun pg-set-span-helphighlights 688,25094
-(defun pg-delete-self-modification-hook 737,26908
-(defun proof-complete-buffer-atomic 748,27181
-(defun proof-register-possibly-new-processed-file789,29093
-(defun proof-query-save-this-buffer-p 835,30967
-(defun proof-inform-prover-file-retracted 840,31192
-(defun proof-auto-retract-dependencies 860,32043
-(defun proof-unregister-buffer-file-name 914,34593
-(defun proof-protected-process-or-retract 960,36418
-(defun proof-deactivate-scripting-auto 987,37588
-(defun proof-deactivate-scripting 996,37946
-(defun proof-activate-scripting 1129,43178
-(defun proof-toggle-active-scripting 1229,47693
-(defun proof-done-advancing 1268,48938
-(defun proof-done-advancing-comment 1347,51923
-(defun proof-done-advancing-save 1381,53299
-(defun proof-make-goalsave1469,56663
-(defun proof-get-name-from-goal 1487,57494
-(defun proof-done-advancing-autosave 1507,58519
-(defun proof-done-advancing-other 1572,61063
-(defun proof-segment-up-to-parser 1601,61992
-(defun proof-script-generic-parse-find-comment-end 1670,64258
-(defun proof-script-generic-parse-cmdend 1679,64672
-(defun proof-script-generic-parse-cmdstart 1730,66568
-(defun proof-script-generic-parse-sexp 1769,68168
-(defun proof-semis-to-vanillas 1781,68634
-(defun proof-script-next-command-advance 1834,70307
-(defun proof-assert-until-point 1853,70806
-(defun proof-assert-electric-terminator 1868,71433
-(defun proof-assert-semis 1903,72814
-(defun proof-retract-before-change 1917,73555
-(defun proof-inside-comment 1929,73956
-(defun proof-inside-string 1935,74129
-(defun proof-insert-pbp-command 1950,74409
-(defun proof-insert-sendback-command 1965,74909
-(defun proof-done-retracting 1991,75812
-(defun proof-setup-retract-action 2026,77253
-(defun proof-last-goal-or-goalsave 2036,77739
-(defun proof-retract-target 2060,78651
-(defun proof-retract-until-point-interactive 2142,82057
-(defun proof-retract-until-point 2150,82442
-(define-derived-mode proof-mode 2197,84275
-(defun proof-script-set-visited-file-name 2233,85657
-(defun proof-script-set-buffer-hooks 2255,86670
-(defun proof-script-kill-buffer-fn 2263,87088
-(defun proof-config-done-related 2295,88405
-(defun proof-generic-goal-command-p 2366,91050
-(defun proof-generic-state-preserving-p 2371,91263
-(defun proof-generic-count-undos 2380,91780
-(defun proof-generic-find-and-forget 2409,92833
-(defconst proof-script-important-settings2460,94605
-(defun proof-config-done 2475,95151
-(defun proof-setup-parsing-mechanism 2536,97118
-(defun proof-setup-imenu 2560,98197
-(deflocal proof-segment-up-to-cache 2587,98975
-(deflocal proof-segment-up-to-cache-start 2588,99016
-(deflocal proof-last-edited-low-watermark 2589,99061
-(defun proof-segment-up-to-using-cache 2599,99548
-(defun proof-segment-cache-contents-for 2628,100682
-(defun proof-script-after-change-function 2640,101051
-(defun proof-script-set-after-change-functions 2652,101558
+generic/proof-script.el,5425
+(deflocal proof-active-buffer-fake-minor-mode 46,1414
+(deflocal proof-script-buffer-file-name 49,1540
+(deflocal pg-script-portions 56,1950
+(defun proof-next-element-count 66,2170
+(defun proof-element-id 72,2412
+(defun proof-next-element-id 76,2581
+(deflocal proof-locked-span 112,3907
+(deflocal proof-queue-span 119,4173
+(deflocal proof-overlay-arrow 128,4659
+(defun proof-span-give-warning 134,4786
+(defun proof-span-read-only 140,4966
+(defun proof-strict-read-only 149,5339
+(defsubst proof-set-queue-endpoints 159,5717
+(defun proof-set-overlay-arrow 163,5858
+(defsubst proof-set-locked-endpoints 174,6196
+(defsubst proof-detach-queue 179,6372
+(defsubst proof-detach-locked 184,6511
+(defsubst proof-set-queue-start 191,6736
+(defsubst proof-set-locked-end 195,6862
+(defsubst proof-set-queue-end 207,7332
+(defun proof-init-segmentation 218,7629
+(defun proof-colour-locked 250,9024
+(defun proof-colour-locked-span 257,9297
+(defun proof-sticky-errors 263,9570
+(defun proof-restart-buffers 276,9986
+(defun proof-script-buffers-with-spans 298,10805
+(defun proof-script-remove-all-spans-and-deactivate 308,11161
+(defun proof-script-clear-queue-spans-on-error 312,11351
+(defun proof-script-delete-spans 338,12368
+(defun proof-script-delete-secondary-spans 343,12567
+(defun proof-unprocessed-begin 356,12856
+(defun proof-script-end 364,13110
+(defun proof-queue-or-locked-end 373,13420
+(defun proof-locked-region-full-p 392,14013
+(defun proof-locked-region-empty-p 401,14285
+(defun proof-only-whitespace-to-locked-region-p 405,14435
+(defun proof-in-locked-region-p 415,14784
+(defun proof-goto-end-of-locked 427,15041
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 444,15800
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 456,16314
+(defun proof-end-of-locked-visible-p 469,16898
+(defvar pg-idioms 488,17491
+(defun pg-clear-script-portions 491,17587
+(defun pg-remove-element 497,17822
+(defun pg-get-element 505,18125
+(defun pg-add-element 515,18440
+(defun pg-set-element-span-invisible 563,20419
+(defun pg-open-invisible-span 567,20579
+(defun pg-make-element-invisible 572,20750
+(defun pg-make-element-visible 577,20961
+(defun pg-toggle-element-span-visibility 582,21155
+(defun pg-toggle-element-visibility 588,21318
+(defun pg-show-all-portions 594,21581
+(defun pg-show-all-proofs 613,22289
+(defun pg-hide-all-proofs 618,22417
+(defun pg-add-proof-element 623,22548
+(defun pg-span-name 638,23319
+(defvar pg-span-context-menu-keymap659,24019
+(defun pg-last-output-displayform 666,24257
+(defun pg-set-span-helphighlights 689,25148
+(defun pg-delete-self-modification-hook 738,26962
+(defun proof-complete-buffer-atomic 749,27235
+(defun proof-register-possibly-new-processed-file790,29147
+(defun proof-query-save-this-buffer-p 836,31021
+(defun proof-inform-prover-file-retracted 841,31246
+(defun proof-auto-retract-dependencies 861,32097
+(defun proof-unregister-buffer-file-name 915,34647
+(defun proof-protected-process-or-retract 961,36472
+(defun proof-deactivate-scripting-auto 988,37642
+(defun proof-deactivate-scripting 997,38000
+(defun proof-activate-scripting 1130,43232
+(defun proof-toggle-active-scripting 1230,47747
+(defun proof-done-advancing 1269,48992
+(defun proof-done-advancing-comment 1348,51977
+(defun proof-done-advancing-save 1382,53353
+(defun proof-make-goalsave1470,56717
+(defun proof-get-name-from-goal 1488,57548
+(defun proof-done-advancing-autosave 1508,58573
+(defun proof-done-advancing-other 1573,61117
+(defun proof-segment-up-to-parser 1602,62046
+(defun proof-script-generic-parse-find-comment-end 1671,64312
+(defun proof-script-generic-parse-cmdend 1680,64726
+(defun proof-script-generic-parse-cmdstart 1731,66622
+(defun proof-script-generic-parse-sexp 1770,68222
+(defun proof-semis-to-vanillas 1782,68688
+(defun proof-script-next-command-advance 1835,70361
+(defun proof-assert-until-point 1854,70860
+(defun proof-assert-electric-terminator 1869,71487
+(defun proof-assert-semis 1904,72868
+(defun proof-retract-before-change 1918,73609
+(defun proof-insert-pbp-command 1938,74205
+(defun proof-insert-sendback-command 1953,74705
+(defun proof-done-retracting 1979,75608
+(defun proof-setup-retract-action 2014,77049
+(defun proof-last-goal-or-goalsave 2024,77535
+(defun proof-retract-target 2048,78447
+(defun proof-retract-until-point-interactive 2130,81853
+(defun proof-retract-until-point 2138,82238
+(define-derived-mode proof-mode 2185,84071
+(defun proof-script-set-visited-file-name 2221,85453
+(defun proof-script-set-buffer-hooks 2243,86466
+(defun proof-script-kill-buffer-fn 2251,86884
+(defun proof-config-done-related 2283,88201
+(defun proof-generic-goal-command-p 2354,90846
+(defun proof-generic-state-preserving-p 2359,91059
+(defun proof-generic-count-undos 2368,91576
+(defun proof-generic-find-and-forget 2397,92629
+(defconst proof-script-important-settings2448,94401
+(defun proof-config-done 2463,94947
+(defun proof-setup-parsing-mechanism 2524,96914
+(defun proof-setup-imenu 2548,97993
+(deflocal proof-segment-up-to-cache 2575,98771
+(deflocal proof-segment-up-to-cache-start 2576,98812
+(deflocal proof-last-edited-low-watermark 2577,98857
+(defun proof-segment-up-to-using-cache 2587,99344
+(defun proof-segment-cache-contents-for 2616,100478
+(defun proof-script-after-change-function 2628,100847
+(defun proof-script-set-after-change-functions 2640,101354
 
 generic/proof-shell.el,3597
 (defvar proof-marker 34,744
@@ -1743,76 +1631,76 @@ generic/proof-shell.el,3597
 (defun proof-shell-start 204,6401
 (defvar proof-shell-kill-function-hooks 374,12125
 (defun proof-shell-kill-function 377,12223
-(defun proof-shell-clear-state 429,14024
-(defun proof-shell-exit 445,14499
-(defun proof-shell-bail-out 458,15003
-(defun proof-shell-restart 468,15525
-(defvar proof-shell-urgent-message-marker 510,16903
-(defvar proof-shell-urgent-message-scanner 513,17024
-(defun proof-shell-handle-error-output 517,17209
-(defun proof-shell-handle-error-or-interrupt 543,18071
-(defun proof-shell-error-or-interrupt-action 585,19774
-(defun proof-goals-pos 608,20653
-(defun proof-pbp-focus-on-first-goal 613,20864
-(defsubst proof-shell-string-match-safe 625,21280
-(defun proof-shell-handle-immediate-output 629,21441
-(defun proof-interrupt-process 696,24048
-(defun proof-shell-insert 729,25236
-(defun proof-shell-action-list-item 780,27062
-(defun proof-shell-set-silent 785,27304
-(defun proof-shell-start-silent-item 791,27523
-(defun proof-shell-clear-silent 797,27712
-(defun proof-shell-stop-silent-item 803,27934
-(defsubst proof-shell-should-be-silent 809,28123
-(defsubst proof-shell-insert-action-item 820,28633
-(defsubst proof-shell-slurp-comments 824,28808
-(defun proof-add-to-queue 835,29213
-(defun proof-start-queue 893,31237
-(defun proof-extend-queue 904,31631
-(defun proof-shell-exec-loop 918,32099
-(defun proof-shell-insert-loopback-cmd 986,34402
-(defun proof-shell-process-urgent-message 1011,35566
-(defun proof-shell-process-urgent-message-default 1060,37286
-(defun proof-shell-process-urgent-message-trace 1076,37870
-(defun proof-shell-process-urgent-message-retract 1089,38429
-(defun proof-shell-process-urgent-message-elisp 1110,39277
-(defun proof-shell-process-urgent-message-thmdeps 1125,39772
-(defun proof-shell-strip-eager-annotations 1139,40151
-(defun proof-shell-filter 1155,40651
-(defun proof-shell-filter-first-command 1255,44023
-(defun proof-shell-process-urgent-messages 1270,44566
-(defun proof-shell-filter-manage-output 1320,46132
-(defsubst proof-shell-display-output-as-response 1352,47379
-(defun proof-shell-handle-delayed-output 1358,47671
-(defvar pg-last-tracing-output-time 1453,51130
-(defconst pg-slow-mode-duration 1456,51236
-(defconst pg-fast-tracing-mode-threshold 1459,51318
-(defvar pg-tracing-cleanup-timer 1462,51446
-(defun pg-tracing-tight-loop 1464,51485
-(defun pg-finish-tracing-display 1507,53197
-(defun proof-shell-wait 1525,53561
-(defun proof-done-invisible 1555,54766
-(defun proof-shell-invisible-command 1561,54936
-(defun proof-shell-invisible-cmd-get-result 1608,56505
-(defun proof-shell-invisible-command-invisible-result 1620,56941
-(defun pg-insert-last-output-as-comment 1640,57442
-(define-derived-mode proof-shell-mode 1659,57914
-(defconst proof-shell-important-settings1696,58941
-(defun proof-shell-config-done 1702,59056
+(defun proof-shell-clear-state 430,14118
+(defun proof-shell-exit 446,14593
+(defun proof-shell-bail-out 459,15097
+(defun proof-shell-restart 469,15619
+(defvar proof-shell-urgent-message-marker 510,16991
+(defvar proof-shell-urgent-message-scanner 513,17112
+(defun proof-shell-handle-error-output 517,17297
+(defun proof-shell-handle-error-or-interrupt 543,18159
+(defun proof-shell-error-or-interrupt-action 586,19908
+(defun proof-goals-pos 609,20787
+(defun proof-pbp-focus-on-first-goal 614,20998
+(defsubst proof-shell-string-match-safe 626,21414
+(defun proof-shell-handle-immediate-output 630,21575
+(defun proof-interrupt-process 697,24182
+(defun proof-shell-insert 731,25415
+(defun proof-shell-action-list-item 782,27241
+(defun proof-shell-set-silent 787,27483
+(defun proof-shell-start-silent-item 793,27702
+(defun proof-shell-clear-silent 799,27891
+(defun proof-shell-stop-silent-item 805,28113
+(defsubst proof-shell-should-be-silent 811,28302
+(defsubst proof-shell-insert-action-item 822,28812
+(defsubst proof-shell-slurp-comments 826,28987
+(defun proof-add-to-queue 837,29392
+(defun proof-start-queue 895,31416
+(defun proof-extend-queue 906,31810
+(defun proof-shell-exec-loop 920,32278
+(defun proof-shell-insert-loopback-cmd 988,34581
+(defun proof-shell-process-urgent-message 1013,35745
+(defun proof-shell-process-urgent-message-default 1062,37465
+(defun proof-shell-process-urgent-message-trace 1078,38049
+(defun proof-shell-process-urgent-message-retract 1091,38608
+(defun proof-shell-process-urgent-message-elisp 1112,39456
+(defun proof-shell-process-urgent-message-thmdeps 1127,39951
+(defun proof-shell-strip-eager-annotations 1141,40330
+(defun proof-shell-filter 1157,40830
+(defun proof-shell-filter-first-command 1257,44202
+(defun proof-shell-process-urgent-messages 1272,44745
+(defun proof-shell-filter-manage-output 1322,46311
+(defsubst proof-shell-display-output-as-response 1354,47558
+(defun proof-shell-handle-delayed-output 1360,47850
+(defvar pg-last-tracing-output-time 1455,51309
+(defconst pg-slow-mode-duration 1458,51415
+(defconst pg-fast-tracing-mode-threshold 1461,51497
+(defvar pg-tracing-cleanup-timer 1464,51625
+(defun pg-tracing-tight-loop 1466,51664
+(defun pg-finish-tracing-display 1509,53376
+(defun proof-shell-wait 1527,53740
+(defun proof-done-invisible 1557,54945
+(defun proof-shell-invisible-command 1563,55115
+(defun proof-shell-invisible-cmd-get-result 1610,56684
+(defun proof-shell-invisible-command-invisible-result 1622,57120
+(defun pg-insert-last-output-as-comment 1642,57621
+(define-derived-mode proof-shell-mode 1661,58093
+(defconst proof-shell-important-settings1698,59120
+(defun proof-shell-config-done 1704,59235
 
 generic/proof-site.el,503
 (defconst proof-assistant-table-default26,771
-(defconst proof-general-short-version64,2168
-(defconst proof-general-version-year 70,2355
-(defgroup proof-general 77,2508
-(defgroup proof-general-internals 82,2616
-(defun proof-home-directory-fn 95,3004
-(defcustom proof-home-directory106,3376
-(defcustom proof-images-directory115,3742
-(defcustom proof-info-directory121,3944
-(defcustom proof-assistant-table150,4921
-(defcustom proof-assistants 185,6034
-(defun proof-ready-for-assistant 214,7190
+(defconst proof-general-short-version58,1785
+(defconst proof-general-version-year 64,1972
+(defgroup proof-general 71,2125
+(defgroup proof-general-internals 76,2233
+(defun proof-home-directory-fn 89,2621
+(defcustom proof-home-directory100,2993
+(defcustom proof-images-directory109,3359
+(defcustom proof-info-directory115,3561
+(defcustom proof-assistant-table144,4538
+(defcustom proof-assistants 179,5651
+(defun proof-ready-for-assistant 208,6807
 
 generic/proof-splash.el,991
 (defcustom proof-splash-enable 34,1007
@@ -1839,7 +1727,7 @@ generic/proof-splash.el,991
 (defun proof-splash-set-frame-titles 308,10882
 (defun proof-splash-unset-frame-titles 317,11197
 
-generic/proof-syntax.el,1061
+generic/proof-syntax.el,1237
 (defsubst proof-ids-to-regexp 22,517
 (defsubst proof-anchor-regexp 29,755
 (defconst proof-no-regexp 33,860
@@ -1855,17 +1743,21 @@ generic/proof-syntax.el,1061
 (defsubst proof-stringfn-match 95,3515
 (defsubst proof-looking-at 102,3778
 (defsubst proof-looking-at-safe 107,3965
-(defsubst proof-looking-at-syntactic-context-default 111,4110
-(defsubst proof-replace-string 122,4487
-(defsubst proof-replace-regexp 127,4691
-(defsubst proof-replace-regexp-nocasefold 132,4900
-(defvar proof-id 140,5182
-(defsubst proof-ids 146,5402
-(defun proof-zap-commas 153,5654
-(defadvice font-lock-fontify-keywords-region179,6540
-(defun proof-format 195,7136
-(defun proof-format-filename 214,7775
-(defun proof-insert 261,9177
+(defun proof-buffer-syntactic-context 116,4178
+(defsubst proof-looking-at-syntactic-context-default 137,5040
+(defun proof-looking-at-syntactic-context 146,5395
+(defun proof-inside-comment 155,5857
+(defun proof-inside-string 161,6030
+(defsubst proof-replace-string 171,6229
+(defsubst proof-replace-regexp 176,6433
+(defsubst proof-replace-regexp-nocasefold 181,6642
+(defvar proof-id 191,6930
+(defsubst proof-ids 197,7150
+(defun proof-zap-commas 204,7402
+(defadvice font-lock-fontify-keywords-region230,8288
+(defun proof-format 246,8884
+(defun proof-format-filename 265,9523
+(defun proof-insert 312,10925
 
 generic/proof-toolbar.el,2332
 (defun proof-toolbar-function 33,810
@@ -1961,46 +1853,46 @@ generic/proof-useropts.el,1635
 (defcustom proof-autosend-delay 383,14401
 (defcustom proof-fast-process-buffer 389,14559
 
-generic/proof-utils.el,1568
-(defmacro proof-with-current-buffer-if-exists 61,1730
-(defmacro proof-with-script-buffer 70,2107
-(defmacro proof-map-buffers 81,2488
-(defmacro proof-sym 86,2673
-(defsubst proof-try-require 91,2834
-(defun proof-save-some-buffers 104,3165
-(defun proof-save-this-buffer 124,3761
-(defun proof-file-truename 137,4125
-(defun proof-files-to-buffers 141,4307
-(defun proof-buffers-in-mode 149,4546
-(defun pg-save-from-death 163,4996
-(defun proof-define-keys 182,5612
-(defun pg-remove-specials 193,5897
-(defun pg-remove-specials-in-string 203,6233
-(defun proof-warn-if-unset 214,6459
-(defun proof-get-window-for-buffer 219,6677
-(defun proof-display-and-keep-buffer 270,8985
-(defun proof-clean-buffer 312,10708
-(defun pg-internal-warning 328,11364
-(defun proof-debug 336,11646
-(defun proof-switch-to-buffer 346,12017
-(defun proof-resize-window-tofit 368,13141
-(defun proof-submit-bug-report 463,16989
-(defun proof-deftoggle-fn 498,18346
-(defmacro proof-deftoggle 513,19009
-(defun proof-defintset-fn 520,19385
-(defmacro proof-defintset 536,20089
-(defun proof-defstringset-fn 543,20468
-(defmacro proof-defstringset 556,21094
-(defun proof-escape-keymap-doc 569,21550
-(defmacro proof-defshortcut 573,21704
-(defmacro proof-definvisible 588,22302
-(defun pg-custom-save-vars 615,23231
-(defun pg-custom-reset-vars 631,23875
-(defun proof-locate-executable 644,24212
-(defun pg-current-word-pos 659,24767
-(defun proof-looking-at-syntactic-context 706,26483
-(defsubst proof-shell-strip-output-markup 721,27051
-(defun proof-minibuffer-message 727,27315
+generic/proof-utils.el,1567
+(defmacro proof-with-current-buffer-if-exists 61,1732
+(defmacro proof-with-script-buffer 70,2109
+(defmacro proof-map-buffers 81,2490
+(defmacro proof-sym 86,2675
+(defsubst proof-try-require 91,2836
+(defun proof-save-some-buffers 104,3167
+(defun proof-save-this-buffer 124,3763
+(defun proof-file-truename 137,4127
+(defun proof-files-to-buffers 141,4309
+(defun proof-buffers-in-mode 149,4548
+(defun pg-save-from-death 163,4998
+(defun proof-define-keys 182,5614
+(defun pg-remove-specials 193,5899
+(defun pg-remove-specials-in-string 203,6235
+(defun proof-safe-split-window-vertically 213,6460
+(defun proof-warn-if-unset 219,6658
+(defun proof-get-window-for-buffer 224,6876
+(defun proof-display-and-keep-buffer 275,9195
+(defun proof-clean-buffer 317,10918
+(defun pg-internal-warning 333,11574
+(defun proof-debug 341,11856
+(defun proof-switch-to-buffer 351,12227
+(defun proof-resize-window-tofit 373,13351
+(defun proof-submit-bug-report 468,17199
+(defun proof-deftoggle-fn 503,18556
+(defmacro proof-deftoggle 518,19219
+(defun proof-defintset-fn 525,19595
+(defmacro proof-defintset 541,20299
+(defun proof-defstringset-fn 548,20678
+(defmacro proof-defstringset 561,21304
+(defun proof-escape-keymap-doc 574,21760
+(defmacro proof-defshortcut 578,21914
+(defmacro proof-definvisible 593,22512
+(defun pg-custom-save-vars 620,23441
+(defun pg-custom-reset-vars 636,24085
+(defun proof-locate-executable 649,24422
+(defun pg-current-word-pos 664,24977
+(defsubst proof-shell-strip-output-markup 709,26632
+(defun proof-minibuffer-message 715,26896
 
 lib/bufhist.el,1257
 (defun bufhist-ring-update 38,1391
@@ -2131,13 +2023,11 @@ lib/pg-fontsets.el,209
 (defconst pg-fontsets-base-fonts51,1710
 (defun pg-fontsets-make-fontsets 57,1840
 
-lib/proof-compat.el,297
-(defvar proof-running-on-win32 32,975
-(defun pg-custom-undeclare-variable 53,1777
-(defmacro save-selected-frame 85,2548
-(defun proof-buffer-syntactic-context-emulate 95,2925
-(defalias 'proof-buffer-syntactic-contextproof-buffer-syntactic-context
164,5213
-(defmacro declare-function 179,5596
+lib/proof-compat.el,160
+(defvar proof-running-on-win32 32,976
+(defun pg-custom-undeclare-variable 53,1778
+(defmacro save-selected-frame 85,2549
+(defmacro declare-function 147,4461
 
 lib/scomint.el,876
 (defface scomint-highlight-input 19,493
@@ -2287,54 +2177,54 @@ lib/unicode-tokens.el,5900
 (defun unicode-tokens-delete-backward-char 752,27509
 (defun unicode-tokens-delete-char 763,27890
 (defun unicode-tokens-delete-backward-1 774,28244
-(defun unicode-tokens-delete-1 791,28848
-(defun unicode-tokens-prev-token 807,29392
-(defun unicode-tokens-rotate-token-forward 815,29689
-(defun unicode-tokens-rotate-token-backward 842,30579
-(defun unicode-tokens-replace-shortcut-match 847,30781
-(defun unicode-tokens-replace-shortcuts 856,31151
-(defun unicode-tokens-replace-unicode-match 870,31749
-(defun unicode-tokens-replace-unicode 877,32050
-(defun unicode-tokens-copy-token 894,32649
-(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32870
-(defun unicode-tokens-list-tokens 907,33074
-(defun unicode-tokens-list-shortcuts 946,34258
-(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34896
-(defun unicode-tokens-encode-in-temp-buffer 966,34969
-(defun unicode-tokens-encode 984,35625
-(defun unicode-tokens-encode-str 990,35861
-(defun unicode-tokens-copy 994,36023
-(defun unicode-tokens-paste 1003,36429
-(defvar unicode-tokens-highlight-unicode 1022,37150
-(defconst unicode-tokens-unicode-highlight-patterns1025,37242
-(defun unicode-tokens-highlight-unicode 1029,37411
-(defun unicode-tokens-highlight-unicode-setkeywords 1041,37874
-(defun unicode-tokens-initialise 1053,38243
-(defvar unicode-tokens-mode-map 1073,38914
-(defvar unicode-tokens-display-table1076,39011
-(define-minor-mode unicode-tokens-mode1083,39262
-(defun unicode-tokens-set-font-var 1216,43745
-(defun unicode-tokens-set-font-var-aux 1232,44234
-(defun unicode-tokens-mouse-set-font 1263,45395
-(defsubst unicode-tokens-face-font-sym 1276,45909
-(defun unicode-tokens-set-font-restart 1280,46089
-(defun unicode-tokens-save-fonts 1291,46399
-(defun unicode-tokens-custom-save-faces 1299,46655
-(define-key unicode-tokens-mode-map1316,47111
-(define-key unicode-tokens-mode-map1319,47218
-(defvar unicode-tokens-quail-translation-keymap1323,47308
-(define-key unicode-tokens-quail-translation-keymap1330,47498
-(defun unicode-tokens-quail-delete-last-char 1334,47632
-(define-key unicode-tokens-mode-map 1349,48059
-(define-key unicode-tokens-mode-map 1351,48151
-(define-key unicode-tokens-mode-map1353,48242
-(define-key unicode-tokens-mode-map1355,48348
-(define-key unicode-tokens-mode-map1358,48463
-(define-key unicode-tokens-mode-map1360,48572
-(define-key unicode-tokens-mode-map1362,48680
-(define-key unicode-tokens-mode-map1364,48786
-(defun unicode-tokens-customize-submenu 1372,48910
-(defun unicode-tokens-define-menu 1379,49133
+(defun unicode-tokens-delete-1 791,28840
+(defun unicode-tokens-prev-token 807,29384
+(defun unicode-tokens-rotate-token-forward 815,29681
+(defun unicode-tokens-rotate-token-backward 842,30571
+(defun unicode-tokens-replace-shortcut-match 847,30773
+(defun unicode-tokens-replace-shortcuts 856,31143
+(defun unicode-tokens-replace-unicode-match 870,31741
+(defun unicode-tokens-replace-unicode 877,32042
+(defun unicode-tokens-copy-token 894,32641
+(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32862
+(defun unicode-tokens-list-tokens 907,33066
+(defun unicode-tokens-list-shortcuts 946,34250
+(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34888
+(defun unicode-tokens-encode-in-temp-buffer 966,34961
+(defun unicode-tokens-encode 984,35617
+(defun unicode-tokens-encode-str 990,35853
+(defun unicode-tokens-copy 994,36015
+(defun unicode-tokens-paste 1003,36421
+(defvar unicode-tokens-highlight-unicode 1022,37142
+(defconst unicode-tokens-unicode-highlight-patterns1025,37234
+(defun unicode-tokens-highlight-unicode 1029,37403
+(defun unicode-tokens-highlight-unicode-setkeywords 1041,37866
+(defun unicode-tokens-initialise 1053,38235
+(defvar unicode-tokens-mode-map 1073,38906
+(defvar unicode-tokens-display-table1076,39003
+(define-minor-mode unicode-tokens-mode1083,39254
+(defun unicode-tokens-set-font-var 1216,43737
+(defun unicode-tokens-set-font-var-aux 1232,44226
+(defun unicode-tokens-mouse-set-font 1263,45387
+(defsubst unicode-tokens-face-font-sym 1276,45901
+(defun unicode-tokens-set-font-restart 1280,46081
+(defun unicode-tokens-save-fonts 1291,46391
+(defun unicode-tokens-custom-save-faces 1299,46647
+(define-key unicode-tokens-mode-map1316,47103
+(define-key unicode-tokens-mode-map1319,47210
+(defvar unicode-tokens-quail-translation-keymap1323,47300
+(define-key unicode-tokens-quail-translation-keymap1330,47490
+(defun unicode-tokens-quail-delete-last-char 1334,47624
+(define-key unicode-tokens-mode-map 1349,48051
+(define-key unicode-tokens-mode-map 1351,48143
+(define-key unicode-tokens-mode-map1353,48234
+(define-key unicode-tokens-mode-map1355,48340
+(define-key unicode-tokens-mode-map1358,48455
+(define-key unicode-tokens-mode-map1360,48564
+(define-key unicode-tokens-mode-map1362,48672
+(define-key unicode-tokens-mode-map1364,48778
+(defun unicode-tokens-customize-submenu 1372,48902
+(defun unicode-tokens-define-menu 1379,49125
 
 mmm/mmm-auto.el,343
 (defvar mmm-autoloaded-classes67,2676
@@ -2752,8 +2642,6 @@ isar/isar-profiling.el,0
 
 isar/interface-setup.el,0
 
-demoisa/demoisa-easy.el,0
-
 coq/coq-mmm.el,0
 
 coq/coq-autotest.el,0