diff options
Diffstat (limited to 'TAGS')
| -rw-r--r-- | TAGS | 3739 |
1 files changed, 1884 insertions, 1855 deletions
@@ -1,188 +1,190 @@ -coq/coq-abbrev.el,468 +coq/coq-abbrev.el,504 (defun holes-show-doc 10,310 (defun coq-local-vars-list-show-doc 14,387 (defconst coq-tactics-menu 19,487 -(defconst coq-tactics-abbrev-table 24,636 -(defconst coq-tacticals-menu 27,724 -(defconst coq-tacticals-abbrev-table 32,879 -(defconst coq-commands-menu 36,972 -(defconst coq-commands-abbrev-table 42,1189 -(defconst coq-terms-menu 45,1279 -(defconst coq-terms-abbrev-table 50,1419 -(defpgdefault menu-entries 72,2197 -(defpgdefault help-menu-entries153,5618 +(defconst coq-tactics-abbrev-table 24,666 +(defconst coq-tacticals-menu 27,784 +(defconst coq-tacticals-abbrev-table 31,894 +(defconst coq-commands-menu 35,987 +(defconst coq-commands-abbrev-table 41,1204 +(defconst coq-terms-menu 44,1294 +(defconst coq-terms-abbrev-table 49,1434 +(defun coq-install-abbrevs 56,1629 +(defpgdefault menu-entries 75,2310 +(defpgdefault help-menu-entries156,5731 coq/coq-db.el,559 -(defconst coq-syntax-db 22,519 -(defvar coq-user-tactics-db58,1892 -(defun coq-insert-from-db 68,2241 -(defun coq-build-regexp-list-from-db 86,3022 -(defun max-length-db 108,4075 -(defun coq-build-menu-from-db-internal 120,4350 -(defun coq-build-title-menu 155,5974 -(defun coq-sort-menu-entries 164,6342 -(defun coq-build-menu-from-db 167,6462 -(defun coq-build-abbrev-table-from-db 187,7233 -(defun filter-state-preserving 203,7787 -(defun filter-state-changing 208,7941 -(defface coq-solve-tactics-face 215,8162 -(defconst coq-solve-tactics-face 223,8424 - -coq/coq.el,6050 -(defcustom coq-translate-to-v8 34,982 -(defcustom coq-compile-file-command 49,1471 -(defcustom coq-default-undo-limit 59,1840 -(defconst coq-shell-init-cmd 64,1968 -(defvar coq-utf-safe 73,2184 -(defcustom coq-prog-env 82,2600 -(defconst coq-shell-restart-cmd 90,2852 -(defvar coq-shell-prompt-pattern 97,3112 -(defvar coq-shell-cd 105,3441 -(defvar coq-shell-abort-goal-regexp 109,3596 -(defvar coq-shell-proof-completed-regexp 112,3722 -(defvar coq-goal-regexp115,3853 -(defun coq-library-directory 124,4042 -(defcustom coq-tags 131,4222 -(defconst coq-interrupt-regexp 136,4372 -(defcustom coq-www-home-page 141,4493 -(defvar coq-outline-regexp151,4664 -(defvar coq-outline-heading-end-regexp 158,4878 -(defvar coq-shell-outline-regexp 160,4932 -(defvar coq-shell-outline-heading-end-regexp 161,4982 -(defconst coq-kill-goal-command 166,5092 -(defconst coq-forget-id-command 167,5135 -(defconst coq-back-n-command 168,5182 -(defconst coq-state-preserving-tactics-regexp 172,5326 -(defconst coq-state-changing-commands-regexp174,5427 -(defconst coq-state-preserving-commands-regexp 176,5534 -(defconst coq-commands-regexp 178,5646 -(defvar coq-retractable-instruct-regexp 180,5724 -(defvar coq-non-retractable-instruct-regexp 182,5815 -(defvar coq-keywords-section186,5955 -(defvar coq-section-regexp 189,6049 -(defun coq-set-undo-limit 223,7149 -(defconst coq-keywords-decl-defn-regexp234,7588 -(defun coq-proof-mode-p 238,7738 -(defun coq-is-comment-or-proverprocp 249,8148 -(defun coq-is-goalsave-p 251,8252 -(defun coq-is-module-equal-p 252,8327 -(defun coq-is-def-p 255,8523 -(defun coq-is-decl-defn-p 257,8631 -(defun coq-state-preserving-command-p 262,8798 -(defun coq-command-p 265,8932 -(defun coq-state-preserving-tactic-p 268,9032 -(defun coq-state-changing-tactic-p 273,9180 -(defun coq-state-changing-command-p 280,9414 -(defun coq-section-or-module-start-p 287,9760 -(defun build-list-id-from-string 296,10001 -(defun coq-last-prompt-info 309,10531 -(defun coq-last-prompt-info-safe 321,11072 -(defvar coq-last-but-one-statenum 331,11587 -(defvar coq-last-but-one-proofnum 333,11654 -(defvar coq-last-but-one-proofstack 335,11717 -(defun coq-get-span-statenum 337,11759 -(defun coq-get-span-proofnum 342,11874 -(defun coq-get-span-proofstack 347,11989 -(defun coq-set-span-statenum 352,12133 -(defun coq-get-span-goalcmd 357,12264 -(defun coq-set-span-goalcmd 362,12378 -(defun coq-set-span-proofnum 367,12508 -(defun coq-set-span-proofstack 372,12639 -(defun proof-last-locked-span 377,12799 -(defun coq-set-state-infos 392,13403 -(defun count-not-intersection 432,15482 -(defun coq-find-and-forget-v81 463,16736 -(defun coq-find-and-forget-v80 491,17868 -(defun coq-find-and-forget 586,22567 -(defvar coq-current-goal 599,23107 -(defun coq-goal-hyp 602,23172 -(defun coq-state-preserving-p 615,23605 -(defconst notation-print-kinds-table 630,24111 -(defun coq-PrintScope 634,24279 -(defun coq-guess-or-ask-for-string 653,24835 -(defun coq-ask-do 664,25220 -(defun coq-SearchIsos 673,25608 -(defun coq-SearchConstant 679,25841 -(defun coq-SearchRewrite 683,25934 -(defun coq-SearchAbout 687,26032 -(defun coq-Print 691,26124 -(defun coq-About 695,26246 -(defun coq-LocateConstant 699,26363 -(defun coq-LocateLibrary 705,26498 -(defun coq-addquotes 711,26648 -(defun coq-LocateNotation 713,26696 -(defun coq-Pwd 720,26895 -(defun coq-Inspect 726,27027 -(defun coq-PrintSection(730,27127 -(defun coq-Print-implicit 734,27221 -(defun coq-Check 739,27373 -(defun coq-Show 744,27483 -(defun coq-Compile 758,27928 -(defun coq-guess-command-line 772,28248 -(defun coq-pre-shell-start 794,29096 -(defun coq-mode-config 804,29545 -(defun coq-hybrid-ouput-goals-response-p 920,33755 -(defun coq-hybrid-ouput-goals-response 926,34013 -(defun coq-shell-mode-config 948,34925 -(defun coq-goals-mode-config 992,36996 -(defun coq-response-config 999,37228 -(defun coq-maybe-compile-buffer 1019,37934 -(defun coq-ancestors-of 1056,39468 -(defun coq-all-ancestors-of 1079,40435 -(defconst coq-require-command-regexp 1091,40828 -(defun coq-process-require-command 1096,41037 -(defun coq-included-children 1101,41164 -(defun coq-process-file 1122,42003 -(defpacustom print-fully-explicit 1147,42918 -(defpacustom print-implicit 1152,43067 -(defpacustom print-coercions 1157,43234 -(defpacustom print-match-wildcards 1162,43379 -(defpacustom print-elim-types 1167,43560 -(defpacustom printing-depth 1172,43727 -(defpacustom time-commands 1177,43889 -(defpacustom auto-compile-vos 1181,44000 -(defun coq-preprocessing 1201,44670 -(defun coq-fake-constant-markup 1216,45089 -(defun coq-create-span-menu 1238,45896 -(defconst module-kinds-table 1265,46698 -(defconst modtype-kinds-table1269,46848 -(defun coq-insert-section-or-module 1273,46977 -(defconst reqkinds-kinds-table1296,47837 -(defun coq-insert-requires 1301,47982 -(defun coq-end-Section 1317,48488 -(defun coq-insert-intros 1335,49072 -(defun coq-insert-match 1347,49596 -(defun coq-insert-tactic 1379,50774 -(defun coq-insert-tactical 1385,51013 -(defun coq-insert-command 1391,51262 -(defun coq-insert-term 1397,51506 -(define-key coq-keymap 1404,51704 -(define-key coq-keymap 1405,51762 -(define-key coq-keymap 1406,51819 -(define-key coq-keymap 1407,51888 -(define-key coq-keymap 1408,51944 -(define-key coq-keymap 1409,51993 -(define-key coq-keymap 1410,52051 -(define-key coq-keymap 1412,52112 -(define-key coq-keymap 1413,52171 -(define-key coq-keymap 1415,52235 -(define-key coq-keymap 1416,52295 -(define-key coq-keymap 1418,52351 -(define-key coq-keymap 1419,52401 -(define-key coq-keymap 1420,52451 -(define-key coq-keymap 1421,52501 -(define-key coq-keymap 1422,52555 -(define-key coq-keymap 1423,52614 -(defvar last-coq-error-location 1433,52797 -(defun coq-get-last-error-location 1442,53196 -(defun coq-highlight-error 1475,54593 -(defun coq-decide-highlight-error 1544,57278 -(defun coq-highlight-error-hook 1549,57440 -(defun first-word-of-buffer 1560,57833 -(defun coq-show-first-goal 1569,58064 -(defun is-not-split-vertic 1594,58953 -(defun optim-resp-windows 1603,59392 +(defconst coq-syntax-db 22,533 +(defvar coq-user-tactics-db58,1906 +(defun coq-insert-from-db 68,2255 +(defun coq-build-regexp-list-from-db 86,3036 +(defun max-length-db 108,4089 +(defun coq-build-menu-from-db-internal 120,4364 +(defun coq-build-title-menu 155,5988 +(defun coq-sort-menu-entries 164,6356 +(defun coq-build-menu-from-db 170,6486 +(defun coq-build-abbrev-table-from-db 192,7247 +(defun filter-state-preserving 209,7805 +(defun filter-state-changing 214,7959 +(defface coq-solve-tactics-face 221,8180 +(defconst coq-solve-tactics-face 229,8442 + +coq/coq.el,6096 +(defcustom coq-translate-to-v8 37,1089 +(defun coq-build-prog-args 43,1269 +(defcustom coq-compile-file-command 56,1651 +(defcustom coq-default-undo-limit 66,2020 +(defconst coq-shell-init-cmd 71,2148 +(defvar coq-utf-safe 80,2364 +(defcustom coq-prog-env 89,2780 +(defconst coq-shell-restart-cmd 97,3032 +(defvar coq-shell-prompt-pattern 104,3292 +(defvar coq-shell-cd 112,3621 +(defvar coq-shell-abort-goal-regexp 116,3776 +(defvar coq-shell-proof-completed-regexp 119,3902 +(defvar coq-goal-regexp122,4054 +(defun coq-library-directory 131,4243 +(defcustom coq-tags 138,4423 +(defconst coq-interrupt-regexp 143,4573 +(defcustom coq-www-home-page 148,4694 +(defvar coq-outline-regexp158,4865 +(defvar coq-outline-heading-end-regexp 165,5079 +(defvar coq-shell-outline-regexp 167,5133 +(defvar coq-shell-outline-heading-end-regexp 168,5183 +(defconst coq-kill-goal-command 173,5293 +(defconst coq-forget-id-command 174,5336 +(defconst coq-back-n-command 175,5383 +(defconst coq-state-preserving-tactics-regexp 179,5527 +(defconst coq-state-changing-commands-regexp181,5628 +(defconst coq-state-preserving-commands-regexp 183,5735 +(defconst coq-commands-regexp 185,5847 +(defvar coq-retractable-instruct-regexp 187,5925 +(defvar coq-non-retractable-instruct-regexp 189,6016 +(defvar coq-keywords-section193,6156 +(defvar coq-section-regexp 196,6250 +(defun coq-set-undo-limit 230,7350 +(defconst coq-keywords-decl-defn-regexp241,7789 +(defun coq-proof-mode-p 245,7939 +(defun coq-is-comment-or-proverprocp 256,8347 +(defun coq-is-goalsave-p 258,8451 +(defun coq-is-module-equal-p 259,8526 +(defun coq-is-def-p 262,8722 +(defun coq-is-decl-defn-p 264,8830 +(defun coq-state-preserving-command-p 269,8997 +(defun coq-command-p 272,9131 +(defun coq-state-preserving-tactic-p 275,9231 +(defun coq-state-changing-tactic-p 280,9379 +(defun coq-state-changing-command-p 287,9613 +(defun coq-section-or-module-start-p 294,9959 +(defun build-list-id-from-string 303,10200 +(defun coq-last-prompt-info 316,10730 +(defun coq-last-prompt-info-safe 328,11271 +(defvar coq-last-but-one-statenum 338,11786 +(defvar coq-last-but-one-proofnum 340,11853 +(defvar coq-last-but-one-proofstack 342,11916 +(defun coq-get-span-statenum 344,11958 +(defun coq-get-span-proofnum 349,12073 +(defun coq-get-span-proofstack 354,12188 +(defun coq-set-span-statenum 359,12332 +(defun coq-get-span-goalcmd 364,12463 +(defun coq-set-span-goalcmd 369,12577 +(defun coq-set-span-proofnum 374,12707 +(defun coq-set-span-proofstack 379,12838 +(defun proof-last-locked-span 384,12998 +(defun coq-set-state-infos 399,13602 +(defun count-not-intersection 439,15681 +(defun coq-find-and-forget-v81 470,16935 +(defun coq-find-and-forget-v80 498,18067 +(defun coq-find-and-forget 593,22766 +(defvar coq-current-goal 606,23306 +(defun coq-goal-hyp 609,23371 +(defun coq-state-preserving-p 622,23804 +(defconst notation-print-kinds-table 637,24310 +(defun coq-PrintScope 641,24478 +(defun coq-guess-or-ask-for-string 660,25034 +(defun coq-ask-do 671,25419 +(defun coq-SearchIsos 680,25807 +(defun coq-SearchConstant 686,26040 +(defun coq-SearchRewrite 690,26133 +(defun coq-SearchAbout 694,26231 +(defun coq-Print 698,26323 +(defun coq-About 702,26445 +(defun coq-LocateConstant 706,26562 +(defun coq-LocateLibrary 712,26697 +(defun coq-addquotes 718,26847 +(defun coq-LocateNotation 720,26895 +(defun coq-Pwd 727,27094 +(defun coq-Inspect 733,27226 +(defun coq-PrintSection(737,27326 +(defun coq-Print-implicit 741,27419 +(defun coq-Check 746,27570 +(defun coq-Show 751,27678 +(defun coq-Compile 765,28121 +(defun coq-guess-command-line 779,28441 +(defun coq-mode-config 800,29294 +(defun coq-hybrid-ouput-goals-response-p 913,33418 +(defun coq-hybrid-ouput-goals-response 919,33676 +(defun coq-shell-mode-config 941,34588 +(defun coq-goals-mode-config 985,36659 +(defun coq-response-config 992,36891 +(defun coq-maybe-compile-buffer 1012,37597 +(defun coq-ancestors-of 1049,39131 +(defun coq-all-ancestors-of 1072,40098 +(defconst coq-require-command-regexp 1084,40491 +(defun coq-process-require-command 1089,40700 +(defun coq-included-children 1094,40827 +(defun coq-process-file 1115,41666 +(defpacustom print-fully-explicit 1140,42581 +(defpacustom print-implicit 1145,42730 +(defpacustom print-coercions 1150,42897 +(defpacustom print-match-wildcards 1155,43042 +(defpacustom print-elim-types 1160,43223 +(defpacustom printing-depth 1165,43390 +(defpacustom time-commands 1170,43552 +(defpacustom auto-compile-vos 1174,43663 +(defun coq-preprocessing 1195,44405 +(defun coq-fake-constant-markup 1210,44824 +(defun coq-create-span-menu 1232,45631 +(defconst module-kinds-table 1259,46433 +(defconst modtype-kinds-table1263,46583 +(defun coq-insert-section-or-module 1267,46712 +(defconst reqkinds-kinds-table1290,47572 +(defun coq-insert-requires 1295,47717 +(defun coq-end-Section 1311,48223 +(defun coq-insert-intros 1329,48807 +(defun coq-insert-match 1341,49331 +(defun coq-insert-tactic 1373,50509 +(defun coq-insert-tactical 1379,50748 +(defun coq-insert-command 1385,50997 +(defun coq-insert-term 1391,51241 +(define-key coq-keymap 1398,51439 +(define-key coq-keymap 1399,51497 +(define-key coq-keymap 1400,51554 +(define-key coq-keymap 1401,51623 +(define-key coq-keymap 1402,51679 +(define-key coq-keymap 1403,51728 +(define-key coq-keymap 1404,51786 +(define-key coq-keymap 1406,51847 +(define-key coq-keymap 1407,51906 +(define-key coq-keymap 1409,51970 +(define-key coq-keymap 1410,52030 +(define-key coq-keymap 1412,52086 +(define-key coq-keymap 1413,52136 +(define-key coq-keymap 1414,52186 +(define-key coq-keymap 1415,52236 +(define-key coq-keymap 1416,52290 +(define-key coq-keymap 1417,52349 +(defvar last-coq-error-location 1427,52532 +(defun coq-get-last-error-location 1436,52931 +(defun coq-highlight-error 1469,54328 +(defvar coq-allow-highlight-error 1534,56883 +(defun coq-decide-highlight-error 1540,57149 +(defun coq-highlight-error-hook 1545,57311 +(defun first-word-of-buffer 1556,57704 +(defun coq-show-first-goal 1565,57935 +(defun is-not-split-vertic 1590,58824 +(defun optim-resp-windows 1599,59263 coq/coq-indent.el,2241 (defconst coq-any-command-regexp11,262 @@ -247,8 +249,72 @@ coq/coq-local-vars.el,279 (defun coq-ask-prog-name 133,5426 (defun coq-ask-insert-coq-prog-name 148,6067 -coq/coq-syntax.el,33 -(defcustom coq-prog-name 12,355 +coq/coq-syntax.el,2572 +(defcustom coq-prog-name 12,357 +(defvar coq-version-is-V8 33,1303 +(defvar coq-version-is-V8-0 35,1382 +(defvar coq-version-is-V8-1 42,1760 +(defun coq-determine-version 51,2193 +(defcustom coq-user-tactics-db 96,4053 +(defcustom coq-user-commands-db 113,4566 +(defcustom coq-user-tacticals-db 129,5085 +(defcustom coq-user-solve-tactics-db 145,5606 +(defcustom coq-user-reserved-db 163,6127 +(defvar coq-tactics-db181,6658 +(defvar coq-solve-tactics-db336,14726 +(defvar coq-tacticals-db359,15524 +(defvar coq-decl-db384,16460 +(defvar coq-defn-db406,17678 +(defvar coq-goal-starters-db459,21664 +(defvar coq-commands-db485,23155 +(defvar coq-terms-db611,32442 +(defun coq-count-match 675,35094 +(defun coq-goal-command-str-v80-p 694,35957 +(defun coq-module-opening-p 717,36830 +(defun coq-section-command-p 728,37246 +(defun coq-goal-command-str-v81-p 732,37343 +(defun coq-goal-command-p-v81 747,38012 +(defun coq-goal-command-str-p 757,38352 +(defun coq-goal-command-p 767,38718 +(defvar coq-keywords-save-strict775,39030 +(defvar coq-keywords-save784,39143 +(defun coq-save-command-p 788,39221 +(defvar coq-keywords-kill-goal 797,39515 +(defvar coq-keywords-state-changing-misc-commands801,39606 +(defvar coq-keywords-goal804,39731 +(defvar coq-keywords-decl807,39814 +(defvar coq-keywords-defn810,39888 +(defvar coq-keywords-state-changing-commands814,39963 +(defvar coq-keywords-state-preserving-commands823,40224 +(defvar coq-keywords-commands828,40440 +(defvar coq-solve-tactics833,40589 +(defvar coq-tacticals837,40710 +(defvar coq-reserved843,40887 +(defvar coq-state-changing-tactics854,41216 +(defvar coq-state-preserving-tactics857,41325 +(defvar coq-tactics861,41439 +(defvar coq-retractable-instruct864,41528 +(defvar coq-non-retractable-instruct867,41638 +(defvar coq-keywords871,41766 +(defvar coq-symbols878,41934 +(defvar coq-error-regexp 897,42147 +(defvar coq-id 900,42375 +(defvar coq-id-shy 901,42400 +(defvar coq-ids 903,42454 +(defun coq-first-abstr-regexp 905,42495 +(defvar coq-font-lock-terms908,42591 +(defconst coq-save-command-regexp-strict926,43552 +(defconst coq-save-command-regexp930,43719 +(defconst coq-save-with-hole-regexp934,43872 +(defconst coq-goal-command-regexp938,44031 +(defconst coq-goal-with-hole-regexp941,44131 +(defconst coq-decl-with-hole-regexp945,44264 +(defconst coq-defn-with-hole-regexp949,44397 +(defconst coq-with-with-hole-regexp959,44686 +(defvar coq-font-lock-keywords-1965,44979 +(defvar coq-font-lock-keywords 989,46243 +(defun coq-init-syntax-table 991,46301 +(defconst coq-generic-expression1020,47200 coq/x-symbol-coq.el,1746 (defvar x-symbol-coq-required-fonts 16,384 @@ -289,85 +355,82 @@ coq/x-symbol-coq.el,1746 (defvar x-symbol-coq-table468,14023 (defcustom x-symbol-coq-auto-style475,14184 -demoisa/demoisa.el,390 +demoisa/demoisa.el,349 (defcustom isabelledemo-prog-name 54,1809 (defcustom isabelledemo-web-page59,1931 (defun demoisa-config 70,2161 -(defun demoisa-shell-config 90,2910 -(define-derived-mode demoisa-mode 119,3994 -(define-derived-mode demoisa-shell-mode 124,4117 -(define-derived-mode demoisa-response-mode 129,4260 -(define-derived-mode demoisa-goals-mode 133,4387 -(defun demoisa-pre-shell-start 152,5169 - -isar/isabelle-system.el,1446 -(defgroup isabelle 19,596 -(defcustom isabelle-web-page23,724 -(defcustom isa-isatool-command34,1019 -(defvar isatool-not-found 61,1964 -(defun isa-set-isatool-command 64,2077 -(defun isa-shell-command-to-string 84,2938 -(defun isa-getenv 90,3162 -(defcustom isabelle-program-name 109,3819 -(defvar isabelle-prog-name 135,4767 -(defun isabelle-command-line 138,4894 -(defun isabelle-choose-logic 162,5851 -(defun isa-tool-list-logics 184,6823 -(defun isa-view-doc 191,7061 -(defun isa-tool-list-docs 199,7286 -(defconst isabelle-verbatim-regexp 226,8319 -(defun isabelle-verbatim 229,8460 -(defcustom isabelle-refresh-logics 236,8616 -(defcustom isabelle-logics-available 244,8943 -(defcustom isabelle-chosen-logic 252,9243 -(defconst isabelle-docs-menu 265,9711 -(defun isabelle-logics-menu-calculate 275,10104 -(defvar isabelle-time-to-refresh-logics 291,10613 -(defun isabelle-logics-menu-refresh 294,10706 -(defun isabelle-logics-menu-filter 311,11405 -(defun isabelle-menu-bar-update-logics 317,11615 -(defvar isabelle-logics-menu-entries 328,11971 -(defvar isabelle-logics-menu 330,12043 -(defun isabelle-load-isar-keywords 343,12661 -(defpgdefault menu-entries364,13402 -(defpgdefault help-menu-entries 367,13454 -(defpgdefault x-symbol-language 375,13648 -(defun isabelle-convert-idmarkup-to-subterm 398,14263 -(defun isabelle-create-span-menu 422,15275 -(defun isabelle-xml-sml-escapes 438,15720 -(defun isabelle-process-pgip 441,15821 - -isar/isar.el,1243 -(defcustom isar-keywords-name 28,580 -(defpgdefault completion-table 45,1104 -(defcustom isar-web-page47,1157 -(defun isar-strip-terminators 61,1494 -(defun isar-markup-ml 74,1871 -(defun isar-mode-config-set-variables 79,2006 -(defun isar-shell-mode-config-set-variables 144,5021 -(defun isar-remove-file 242,9190 -(defun isar-shell-compute-new-files-list 252,9553 -(defun isar-activate-scripting 263,10019 -(define-derived-mode isar-shell-mode 272,10189 -(define-derived-mode isar-response-mode 277,10312 -(define-derived-mode isar-goals-mode 282,10494 -(define-derived-mode isar-mode 287,10669 -(defpgdefault menu-entries341,12646 -(defun isar-count-undos 371,13885 -(defun isar-find-and-forget 398,15010 -(defun isar-goal-command-p 439,16593 -(defun isar-global-save-command-p 444,16765 -(defvar isar-current-goal 465,17610 -(defun isar-state-preserving-p 468,17676 -(defvar isar-shell-current-line-width 493,18835 -(defun isar-shell-adjust-line-width 499,19053 -(defun isar-pre-shell-start 519,19938 -(defun isar-preprocessing 531,20281 -(defun isar-mode-config 554,21547 -(defun isar-shell-mode-config 566,22117 -(defun isar-response-mode-config 577,22487 -(defun isar-goals-mode-config 586,22744 -(defun isar-goalhyplit-test 597,23090 +(defun demoisa-shell-config 91,2953 +(define-derived-mode demoisa-mode 117,3930 +(define-derived-mode demoisa-shell-mode 122,4053 +(define-derived-mode demoisa-response-mode 127,4196 +(define-derived-mode demoisa-goals-mode 131,4323 + +isar/isabelle-system.el,1400 +(defgroup isabelle 24,731 +(defcustom isabelle-web-page28,859 +(defcustom isa-isatool-command39,1154 +(defvar isatool-not-found 66,2097 +(defun isa-set-isatool-command 69,2210 +(defun isa-shell-command-to-string 89,3071 +(defun isa-getenv 95,3295 +(defcustom isabelle-program-name114,3956 +(defvar isabelle-prog-name 140,4886 +(defun isabelle-command-line 143,5013 +(defun isabelle-choose-logic 167,5971 +(defun isa-tool-list-logics 189,6937 +(defun isa-view-doc 196,7174 +(defun isa-tool-list-docs 204,7399 +(defconst isabelle-verbatim-regexp 231,8431 +(defun isabelle-verbatim 234,8573 +(defcustom isabelle-refresh-logics 241,8734 +(defcustom isabelle-logics-available 249,9061 +(defcustom isabelle-chosen-logic 257,9361 +(defconst isabelle-docs-menu270,9829 +(defun isabelle-logics-menu-calculate 280,10221 +(defvar isabelle-time-to-refresh-logics 296,10728 +(defun isabelle-logics-menu-refresh 299,10822 +(defun isabelle-logics-menu-filter 316,11519 +(defun isabelle-menu-bar-update-logics 322,11729 +(defvar isabelle-logics-menu-entries 333,12068 +(defvar isabelle-logics-menu335,12140 +(defun isabelle-load-isar-keywords 348,12752 +(defpgdefault menu-entries369,13493 +(defpgdefault help-menu-entries 372,13545 +(defun isabelle-convert-idmarkup-to-subterm 400,14297 +(defun isabelle-create-span-menu 424,15308 +(defun isabelle-xml-sml-escapes 440,15750 +(defun isabelle-process-pgip 443,15851 + +isar/isar.el,1204 +(defcustom isar-keywords-name 30,707 +(defpgdefault completion-table 47,1230 +(defcustom isar-web-page49,1283 +(defun isar-strip-terminators 63,1615 +(defun isar-markup-ml 76,1992 +(defun isar-mode-config-set-variables 81,2127 +(defun isar-shell-mode-config-set-variables 146,5142 +(defun isar-remove-file 244,9291 +(defun isar-shell-compute-new-files-list 254,9654 +(defun isar-activate-scripting 265,10120 +(define-derived-mode isar-shell-mode 274,10290 +(define-derived-mode isar-response-mode 279,10413 +(define-derived-mode isar-goals-mode 284,10595 +(define-derived-mode isar-mode 289,10770 +(defpgdefault menu-entries343,12742 +(defun isar-count-undos 373,13981 +(defun isar-find-and-forget 400,15095 +(defun isar-goal-command-p 439,16675 +(defun isar-global-save-command-p 444,16852 +(defvar isar-current-goal 465,17713 +(defun isar-state-preserving-p 468,17779 +(defvar isar-shell-current-line-width 492,18916 +(defun isar-shell-adjust-line-width 497,19108 +(defun isar-preprocessing 520,19999 +(defun isar-mode-config 543,21266 +(defun isar-shell-mode-config 554,21767 +(defun isar-response-mode-config 565,22126 +(defun isar-goals-mode-config 574,22376 +(defun isar-goalhyplit-test 585,22715 isar/isar-find-theorems.el,778 (defun isar-find-theorems-minibuffer 18,715 @@ -417,148 +480,147 @@ isar/isar-mmm.el,83 (defconst isar-start-latex-regexp 23,697 (defconst isar-start-sml-regexp 35,1130 -isar/isar-syntax.el,3471 +isar/isar-syntax.el,3470 (defconst isar-script-syntax-table-entries18,433 -(defconst isar-script-syntax-table-alist59,1469 -(defun isar-init-syntax-table 68,1759 -(defun isar-init-output-syntax-table 76,2006 -(defconst isar-keyword-begin 92,2453 -(defconst isar-keyword-end 93,2491 -(defconst isar-keywords-theory-enclose95,2526 -(defconst isar-keywords-theory100,2671 -(defconst isar-keywords-save105,2816 -(defconst isar-keywords-proof-enclose110,2945 -(defconst isar-keywords-proof116,3127 -(defconst isar-keywords-proof-context123,3332 -(defconst isar-keywords-local-goal127,3446 -(defconst isar-keywords-proper131,3558 -(defconst isar-keywords-improper136,3691 -(defconst isar-keywords-outline141,3837 -(defconst isar-keywords-fume144,3902 -(defconst isar-keywords-indent-open151,4120 -(defconst isar-keywords-indent-close157,4304 -(defconst isar-keywords-indent-enclose161,4409 -(defun isar-regexp-simple-alt 170,4624 -(defun isar-ids-to-regexp 190,5384 -(defconst isar-ext-first 224,6790 -(defconst isar-ext-rest 225,6857 -(defconst isar-long-id-stuff 227,6929 -(defconst isar-id 228,7003 -(defconst isar-idx 229,7073 -(defconst isar-string 231,7132 -(defconst isar-any-command-regexp233,7192 -(defconst isar-name-regexp237,7326 -(defconst isar-improper-regexp243,7621 -(defconst isar-save-command-regexp247,7769 -(defconst isar-global-save-command-regexp250,7870 -(defconst isar-goal-command-regexp253,7984 -(defconst isar-local-goal-command-regexp256,8092 -(defconst isar-comment-start 259,8205 -(defconst isar-comment-end 260,8240 -(defconst isar-comment-start-regexp 261,8273 -(defconst isar-comment-end-regexp 262,8344 -(defconst isar-string-start-regexp 264,8412 -(defconst isar-string-end-regexp 265,8464 -(defconst isar-antiq-regexp274,8717 -(defconst isar-nesting-regexp281,8878 -(defun isar-nesting 284,8976 -(defun isar-match-nesting 296,9397 -(defface isabelle-class-name-face308,9728 -(defface isabelle-tfree-name-face318,10003 -(defface isabelle-tvar-name-face328,10284 -(defface isabelle-free-name-face338,10564 -(defface isabelle-bound-name-face348,10840 -(defface isabelle-var-name-face358,11119 -(defconst isabelle-class-name-face 368,11398 -(defconst isabelle-tfree-name-face 369,11460 -(defconst isabelle-tvar-name-face 370,11522 -(defconst isabelle-free-name-face 371,11583 -(defconst isabelle-bound-name-face 372,11644 -(defconst isabelle-var-name-face 373,11706 -(defconst isar-font-lock-local376,11768 -(defvar isar-font-lock-keywords-1381,11934 -(defvar isar-output-font-lock-keywords-1395,12800 -(defvar isar-goals-font-lock-keywords422,14424 -(defconst isar-undo 456,15103 -(defun isar-remove 458,15165 -(defun isar-undos 461,15240 -(defun isar-cannot-undo 465,15346 -(defconst isar-theory-start-regexp468,15416 -(defconst isar-end-regexp474,15581 -(defconst isar-undo-fail-regexp478,15682 -(defconst isar-undo-skip-regexp482,15786 -(defconst isar-undo-ignore-regexp485,15907 -(defconst isar-undo-remove-regexp488,15972 -(defconst isar-any-entity-regexp496,16147 -(defconst isar-named-entity-regexp501,16334 -(defconst isar-unnamed-entity-regexp506,16511 -(defconst isar-next-entity-regexps509,16613 -(defconst isar-generic-expression517,16924 -(defconst isar-indent-any-regexp528,17241 -(defconst isar-indent-inner-regexp530,17334 -(defconst isar-indent-enclose-regexp532,17400 -(defconst isar-indent-open-regexp534,17516 -(defconst isar-indent-close-regexp536,17626 -(defconst isar-outline-regexp542,17763 -(defconst isar-outline-heading-end-regexp 546,17916 - -isar/x-symbol-isabelle.el,1922 -(defvar x-symbol-isabelle-required-fonts 20,624 -(defvar x-symbol-isabelle-name 28,1028 -(defvar x-symbol-isabelle-modeline-name 29,1078 -(defcustom x-symbol-isabelle-header-groups-alist 31,1126 -(defcustom x-symbol-isabelle-electric-ignore 38,1354 -(defvar x-symbol-isabelle-required-fonts 46,1610 -(defvar x-symbol-isabelle-extra-menu-items 49,1719 -(defvar x-symbol-isabelle-token-grammar53,1817 -(defun x-symbol-isabelle-token-list 60,2023 -(defvar x-symbol-isabelle-user-table 63,2112 -(defvar x-symbol-isabelle-generated-data 66,2233 -(defvar x-symbol-isabelle-master-directory 74,2476 -(defvar x-symbol-isabelle-image-searchpath 75,2529 -(defvar x-symbol-isabelle-image-cached-dirs 76,2581 -(defvar x-symbol-isabelle-image-file-truename-alist 77,2651 -(defvar x-symbol-isabelle-image-keywords 78,2708 -(defcustom x-symbol-isabelle-subscript-matcher 88,3052 -(defcustom x-symbol-isabelle-font-lock-regexp 94,3299 -(defcustom x-symbol-isabelle-font-lock-limit-regexp 99,3483 -(defcustom x-symbol-isabelle-font-lock-contents-regexp 105,3715 -(defcustom x-symbol-isabelle-single-char-regexp 115,4107 -(defun x-symbol-isabelle-subscript-matcher 121,4385 -(defun isabelle-match-subscript 163,6057 -(defvar x-symbol-isabelle-font-lock-keywords172,6452 -(defvar x-symbol-isabelle-font-lock-allowed-faces 179,6720 -(defcustom x-symbol-isabelle-class-alist186,6952 -(defcustom x-symbol-isabelle-class-face-alist 197,7377 -(defvar x-symbol-isabelle-case-insensitive 212,7905 -(defvar x-symbol-isabelle-token-shape 213,7953 -(defvar x-symbol-isabelle-input-token-ignore 214,7996 -(defvar x-symbol-isabelle-token-list 215,8046 -(defvar x-symbol-isabelle-symbol-table 217,8095 -(defvar x-symbol-isabelle-xsymbol-table 317,10831 -(defun x-symbol-isabelle-prepare-table 463,15265 -(defvar x-symbol-isabelle-table471,15465 -(defcustom x-symbol-isabelle-auto-style485,15818 -(defcustom x-symbol-isabelle-auto-coding-alist 499,16328 - -lclam/lclam.el,563 +(defconst isar-script-syntax-table-alist59,1464 +(defun isar-init-syntax-table 68,1754 +(defun isar-init-output-syntax-table 76,2001 +(defconst isar-keyword-begin 92,2448 +(defconst isar-keyword-end 93,2486 +(defconst isar-keywords-theory-enclose95,2521 +(defconst isar-keywords-theory100,2666 +(defconst isar-keywords-save105,2811 +(defconst isar-keywords-proof-enclose110,2940 +(defconst isar-keywords-proof116,3122 +(defconst isar-keywords-proof-context123,3327 +(defconst isar-keywords-local-goal127,3441 +(defconst isar-keywords-proper131,3553 +(defconst isar-keywords-improper136,3686 +(defconst isar-keywords-outline141,3832 +(defconst isar-keywords-fume144,3897 +(defconst isar-keywords-indent-open151,4115 +(defconst isar-keywords-indent-close157,4299 +(defconst isar-keywords-indent-enclose161,4404 +(defun isar-regexp-simple-alt 170,4619 +(defun isar-ids-to-regexp 190,5379 +(defconst isar-ext-first 224,6785 +(defconst isar-ext-rest 225,6852 +(defconst isar-long-id-stuff 227,6924 +(defconst isar-id 228,6998 +(defconst isar-idx 229,7068 +(defconst isar-string 231,7127 +(defconst isar-any-command-regexp233,7187 +(defconst isar-name-regexp237,7321 +(defconst isar-improper-regexp243,7616 +(defconst isar-save-command-regexp247,7764 +(defconst isar-global-save-command-regexp250,7865 +(defconst isar-goal-command-regexp253,7979 +(defconst isar-local-goal-command-regexp256,8087 +(defconst isar-comment-start 259,8200 +(defconst isar-comment-end 260,8235 +(defconst isar-comment-start-regexp 261,8268 +(defconst isar-comment-end-regexp 262,8339 +(defconst isar-string-start-regexp 264,8407 +(defconst isar-string-end-regexp 265,8459 +(defconst isar-antiq-regexp274,8712 +(defconst isar-nesting-regexp281,8873 +(defun isar-nesting 284,8971 +(defun isar-match-nesting 296,9392 +(defface isabelle-class-name-face308,9723 +(defface isabelle-tfree-name-face318,9998 +(defface isabelle-tvar-name-face328,10279 +(defface isabelle-free-name-face338,10559 +(defface isabelle-bound-name-face348,10835 +(defface isabelle-var-name-face358,11114 +(defconst isabelle-class-name-face 368,11393 +(defconst isabelle-tfree-name-face 369,11455 +(defconst isabelle-tvar-name-face 370,11517 +(defconst isabelle-free-name-face 371,11578 +(defconst isabelle-bound-name-face 372,11639 +(defconst isabelle-var-name-face 373,11701 +(defconst isar-font-lock-local376,11763 +(defvar isar-font-lock-keywords-1381,11931 +(defvar isar-output-font-lock-keywords-1395,12797 +(defvar isar-goals-font-lock-keywords422,14421 +(defconst isar-undo 456,15100 +(defun isar-remove 458,15162 +(defun isar-undos 461,15237 +(defun isar-cannot-undo 465,15343 +(defconst isar-theory-start-regexp468,15413 +(defconst isar-end-regexp474,15578 +(defconst isar-undo-fail-regexp478,15679 +(defconst isar-undo-skip-regexp482,15783 +(defconst isar-undo-ignore-regexp485,15904 +(defconst isar-undo-remove-regexp488,15969 +(defconst isar-any-entity-regexp496,16144 +(defconst isar-named-entity-regexp501,16331 +(defconst isar-unnamed-entity-regexp506,16508 +(defconst isar-next-entity-regexps509,16610 +(defconst isar-generic-expression517,16921 +(defconst isar-indent-any-regexp528,17238 +(defconst isar-indent-inner-regexp530,17331 +(defconst isar-indent-enclose-regexp532,17397 +(defconst isar-indent-open-regexp534,17513 +(defconst isar-indent-close-regexp536,17623 +(defconst isar-outline-regexp542,17760 +(defconst isar-outline-heading-end-regexp 546,17913 + +isar/x-symbol-isar.el,1774 +(defvar x-symbol-isar-required-fonts 12,429 +(defvar x-symbol-isar-name 20,829 +(defvar x-symbol-isar-modeline-name 21,875 +(defcustom x-symbol-isar-header-groups-alist 23,919 +(defcustom x-symbol-isar-electric-ignore 30,1139 +(defvar x-symbol-isar-required-fonts 38,1387 +(defvar x-symbol-isar-extra-menu-items 41,1492 +(defvar x-symbol-isar-token-grammar45,1586 +(defun x-symbol-isar-token-list 52,1784 +(defvar x-symbol-isar-user-table 55,1869 +(defvar x-symbol-isar-generated-data 58,1982 +(defvar x-symbol-isar-master-directory 66,2221 +(defvar x-symbol-isar-image-searchpath 67,2270 +(defvar x-symbol-isar-image-cached-dirs 68,2318 +(defvar x-symbol-isar-image-file-truename-alist 69,2384 +(defvar x-symbol-isar-image-keywords 70,2437 +(defcustom x-symbol-isar-subscript-matcher 80,2777 +(defcustom x-symbol-isar-font-lock-regexp 86,3012 +(defcustom x-symbol-isar-font-lock-limit-regexp 91,3188 +(defcustom x-symbol-isar-font-lock-contents-regexp 97,3412 +(defcustom x-symbol-isar-single-char-regexp 107,3796 +(defun x-symbol-isar-subscript-matcher 113,4066 +(defun isabelle-match-subscript 155,5718 +(defvar x-symbol-isar-font-lock-keywords164,6101 +(defvar x-symbol-isar-font-lock-allowed-faces 171,6361 +(defcustom x-symbol-isar-class-alist178,6589 +(defcustom x-symbol-isar-class-face-alist 189,7010 +(defvar x-symbol-isar-case-insensitive 204,7530 +(defvar x-symbol-isar-token-shape 205,7574 +(defvar x-symbol-isar-input-token-ignore 206,7613 +(defvar x-symbol-isar-token-list 207,7659 +(defvar x-symbol-isar-symbol-table 209,7704 +(defvar x-symbol-isar-xsymbol-table 309,10436 +(defun x-symbol-isar-prepare-table 455,14866 +(defvar x-symbol-isar-table463,15062 +(defcustom x-symbol-isar-auto-style477,15395 +(defcustom x-symbol-isar-auto-coding-alist 491,15897 + +lclam/lclam.el,524 (defcustom lclam-prog-name 15,385 (defcustom lclam-web-page21,533 (defun lclam-config 32,763 -(defun lclam-shell-config 52,1477 -(define-derived-mode lclam-proofscript-mode 72,2136 -(define-derived-mode lclam-shell-mode 77,2259 -(define-derived-mode lclam-response-mode 82,2393 -(define-derived-mode lclam-goals-mode 86,2516 -(defun lclam-mode 94,2744 -(defun lclam-pre-shell-start 107,3027 -(define-derived-mode thy-mode 141,3970 -(defvar thy-mode-map 144,4068 -(defun thy-add-menus 146,4095 -(defun process-thy-file 186,6009 -(defun update-thy-only 192,6210 - -lego/lego.el,1766 +(defun lclam-shell-config 54,1557 +(define-derived-mode lclam-proofscript-mode 74,2216 +(define-derived-mode lclam-shell-mode 79,2339 +(define-derived-mode lclam-response-mode 84,2473 +(define-derived-mode lclam-goals-mode 88,2596 +(defun lclam-mode 96,2824 +(define-derived-mode thy-mode 133,3635 +(defvar thy-mode-map 136,3733 +(defun thy-add-menus 138,3760 +(defun process-thy-file 178,5674 +(defun update-thy-only 184,5875 + +lego/lego.el,1727 (defcustom lego-tags 19,493 (defcustom lego-test-all-name 24,629 (defpgdefault help-menu-entries30,787 @@ -591,17 +653,16 @@ lego/lego.el,1766 (define-derived-mode lego-goals-mode 167,5271 (defun lego-count-undos 178,5697 (defun lego-goal-command-p 198,6516 -(defun lego-find-and-forget 203,6686 -(defun lego-goal-hyp 245,8522 -(defun lego-state-preserving-p 254,8720 -(defvar lego-shell-current-line-width 270,9423 -(defun lego-shell-adjust-line-width 278,9730 -(defun lego-pre-shell-start 297,10469 -(defun lego-mode-config 304,10666 -(defun lego-equal-module-filename 373,12764 -(defun lego-shell-compute-new-files-list 379,13039 -(defun lego-shell-mode-config 393,13565 -(defun lego-goals-mode-config 442,15501 +(defun lego-find-and-forget 203,6687 +(defun lego-goal-hyp 245,8523 +(defun lego-state-preserving-p 254,8721 +(defvar lego-shell-current-line-width 270,9424 +(defun lego-shell-adjust-line-width 278,9731 +(defun lego-mode-config 297,10470 +(defun lego-equal-module-filename 365,12497 +(defun lego-shell-compute-new-files-list 371,12772 +(defun lego-shell-mode-config 385,13298 +(defun lego-goals-mode-config 434,15234 lego/lego-syntax.el,600 (defconst lego-keywords-goal 15,358 @@ -621,25 +682,24 @@ lego/lego-syntax.el,600 (defvar lego-font-lock-keywords-199,3667 (defun lego-init-syntax-table 110,4134 -phox/phox.el,682 -(defcustom phox-prog-name 31,931 -(defcustom phox-sym-lock-enabled 36,1033 -(defcustom phox-web-page42,1140 -(defcustom phox-doc-dir 48,1290 -(defcustom phox-lib-dir 54,1438 -(defcustom phox-tags-program 60,1582 -(defcustom phox-tags-doc 66,1762 -(defcustom phox-etags 72,1900 -(defpgdefault menu-entries93,2352 -(defun phox-config 107,2545 -(defun phox-shell-config 153,4582 -(define-derived-mode phox-mode 178,5511 -(define-derived-mode phox-shell-mode 198,6123 -(define-derived-mode phox-response-mode 203,6251 -(define-derived-mode phox-goals-mode 215,6678 -(defun phox-pre-shell-start 243,7750 -(defpgdefault completion-table257,8264 -(defpgdefault x-symbol-language 265,8369 +phox/phox.el,644 +(defcustom phox-prog-name 31,907 +(defcustom phox-sym-lock-enabled 36,1009 +(defcustom phox-web-page42,1116 +(defcustom phox-doc-dir 48,1266 +(defcustom phox-lib-dir 54,1414 +(defcustom phox-tags-program 60,1558 +(defcustom phox-tags-doc 66,1738 +(defcustom phox-etags 72,1876 +(defpgdefault menu-entries93,2328 +(defun phox-config 107,2521 +(defun phox-shell-config 153,4558 +(define-derived-mode phox-mode 178,5487 +(define-derived-mode phox-shell-mode 198,6099 +(define-derived-mode phox-response-mode 203,6227 +(define-derived-mode phox-goals-mode 215,6654 +(defpgdefault completion-table240,7522 +(defpgdefault x-symbol-language 248,7627 phox/phox-extraction.el,382 (defvar phox-prog-orig 11,480 @@ -655,8 +715,8 @@ phox/phox-extraction.el,382 phox/phox-font.el,123 (defconst phox-font-lock-keywords6,282 -(defconst phox-sym-lock-keywords-table65,2406 -(defun phox-sym-lock-start 88,2980 +(defconst phox-sym-lock-keywords-table65,2401 +(defun phox-sym-lock-start 88,2975 phox/phox-fun.el,679 (defun phox-init-syntax-table 67,2392 @@ -706,153 +766,152 @@ phox/phox-pbrpm.el,512 (defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p289,10739 phox/phox-sym-lock.el,1353 -(defvar phox-sym-lock-sym-count 35,1696 -(defvar phox-sym-lock-ext-start 38,1766 -(defvar phox-sym-lock-ext-end 40,1888 -(defvar phox-sym-lock-font-size 43,2007 -(defvar phox-sym-lock-keywords 48,2197 -(defvar phox-sym-lock-enabled 53,2373 -(defvar phox-sym-lock-color 58,2535 -(defvar phox-sym-lock-mouse-face 63,2753 -(defvar phox-sym-lock-mouse-face-enabled 68,2943 -(defconst phox-sym-lock-with-mule 73,3133 -(defun phox-sym-lock-gen-symbol 76,3217 -(defun phox-sym-lock-make-symbols-atomic 84,3520 -(defun phox-sym-lock-compute-font-size 111,4462 -(defvar phox-sym-lock-font-name149,5882 -(defun phox-sym-lock-set-foreground 187,7167 -(defun phox-sym-lock-translate-char 201,7776 -(defun phox-sym-lock-translate-char-or-string 209,8044 -(defun phox-sym-lock-remap-face 216,8271 -(defvar phox-sym-lock-clear-face236,9261 -(defun phox-sym-lock 248,9683 -(defun phox-sym-lock-rec 257,10087 -(defun phox-sym-lock-atom-face 263,10240 -(defun phox-sym-lock-pre-idle-hook-first 268,10536 -(defun phox-sym-lock-pre-idle-hook-last 276,10894 -(defun phox-sym-lock-enable 285,11269 -(defun phox-sym-lock-disable 298,11682 -(defun phox-sym-lock-mouse-face-enable 311,12100 -(defun phox-sym-lock-mouse-face-disable 318,12315 -(defun phox-sym-lock-font-lock-hook 325,12534 -(defun font-lock-set-defaults 340,13227 -(defun phox-sym-lock-patch-keywords 351,13605 +(defvar phox-sym-lock-sym-count 34,1618 +(defvar phox-sym-lock-ext-start 37,1688 +(defvar phox-sym-lock-ext-end 39,1810 +(defvar phox-sym-lock-font-size 42,1929 +(defvar phox-sym-lock-keywords 47,2119 +(defvar phox-sym-lock-enabled 52,2295 +(defvar phox-sym-lock-color 57,2457 +(defvar phox-sym-lock-mouse-face 62,2675 +(defvar phox-sym-lock-mouse-face-enabled 67,2865 +(defconst phox-sym-lock-with-mule 72,3055 +(defun phox-sym-lock-gen-symbol 75,3139 +(defun phox-sym-lock-make-symbols-atomic 83,3442 +(defun phox-sym-lock-compute-font-size 110,4384 +(defvar phox-sym-lock-font-name148,5804 +(defun phox-sym-lock-set-foreground 186,7089 +(defun phox-sym-lock-translate-char 200,7698 +(defun phox-sym-lock-translate-char-or-string 208,7966 +(defun phox-sym-lock-remap-face 215,8193 +(defvar phox-sym-lock-clear-face235,9183 +(defun phox-sym-lock 247,9605 +(defun phox-sym-lock-rec 256,10009 +(defun phox-sym-lock-atom-face 262,10162 +(defun phox-sym-lock-pre-idle-hook-first 267,10458 +(defun phox-sym-lock-pre-idle-hook-last 275,10816 +(defun phox-sym-lock-enable 284,11191 +(defun phox-sym-lock-disable 297,11604 +(defun phox-sym-lock-mouse-face-enable 310,12022 +(defun phox-sym-lock-mouse-face-disable 317,12237 +(defun phox-sym-lock-font-lock-hook 324,12456 +(defun font-lock-set-defaults 339,13149 +(defun phox-sym-lock-patch-keywords 350,13527 phox/phox-tags.el,305 (defun phox-tags-add-table(21,766 -(defun phox-tags-reset-table(38,1359 -(defun phox-tags-add-doc-table(48,1629 -(defun phox-tags-add-lib-table(54,1778 -(defun phox-tags-add-local-table(60,1914 -(defun phox-tags-create-local-table(66,2097 -(defun phox-complete-tag(77,2349 -(defvar phox-tags-menu96,2904 +(defun phox-tags-reset-table(38,1354 +(defun phox-tags-add-doc-table(48,1619 +(defun phox-tags-add-lib-table(54,1768 +(defun phox-tags-add-local-table(60,1904 +(defun phox-tags-create-local-table(66,2087 +(defun phox-complete-tag(77,2339 +(defvar phox-tags-menu96,2889 phox/x-symbol-phox.el,1609 -(defvar x-symbol-phox-required-fonts 14,449 -(defcustom x-symbol-phox-header-groups-alist 29,1056 -(defcustom x-symbol-phox-electric-ignore 36,1276 -(defvar x-symbol-phox-required-fonts 43,1492 -(defvar x-symbol-phox-extra-menu-items 46,1593 -(defvar x-symbol-phox-token-grammar49,1682 -(defvar x-symbol-phox-input-token-grammar63,2473 -(defun x-symbol-phox-default-token-list 69,2728 -(defvar x-symbol-phox-user-table 81,3046 -(defvar x-symbol-phox-generated-data 84,3155 -(defvar x-symbol-phox-master-directory 92,3394 -(defvar x-symbol-phox-image-searchpath 93,3443 -(defvar x-symbol-phox-image-cached-dirs 94,3491 -(defvar x-symbol-phox-image-file-truename-alist 95,3557 -(defvar x-symbol-phox-image-keywords 96,3610 -(defcustom x-symbol-phox-class-alist103,3831 -(defcustom x-symbol-phox-class-face-alist 114,4213 -(defvar x-symbol-phox-font-lock-keywords 124,4526 -(defvar x-symbol-phox-font-lock-allowed-faces 126,4573 -(defvar x-symbol-phox-case-insensitive 132,4798 -(defvar x-symbol-phox-token-shape 133,4842 -(defvar x-symbol-phox-input-token-ignore 134,4881 -(defvar x-symbol-phox-token-list 141,5120 -(defvar x-symbol-phox-xsymb0-table 143,5165 -(defun x-symbol-phox-prepare-table 164,5624 -(defvar x-symbol-phox-table172,5800 -(defcustom x-symbol-phox-auto-style183,6118 -(defvar x-symbol-phox-menu-alist 209,7068 -(defvar x-symbol-phox-grid-alist 211,7158 -(defvar x-symbol-phox-decode-atree 214,7249 -(defvar x-symbol-phox-decode-alist 216,7342 -(defvar x-symbol-phox-encode-alist 218,7439 -(defvar x-symbol-phox-nomule-decode-exec 222,7596 -(defvar x-symbol-phox-nomule-encode-exec 224,7696 - -plastic/plastic.el,2907 -(defcustom plastic-tags 28,805 -(defcustom plastic-test-all-name 33,937 -(defvar plastic-lit-string 39,1110 -(defcustom plastic-help-menu-list43,1223 -(defvar plastic-shell-process-output57,1717 -(defconst plastic-process-config 65,2043 -(defconst plastic-pretty-set-width 72,2293 -(defconst plastic-interrupt-regexp 76,2442 -(defcustom plastic-www-home-page 82,2563 -(defcustom plastic-www-latest-release87,2700 -(defcustom plastic-www-refcard93,2873 -(defcustom plastic-library-www-page99,3004 -(defcustom plastic-base 109,3219 -(defvar plastic-prog-name 117,3391 -(defun plastic-set-default-env-vars 121,3499 -(defvar plastic-shell-prompt-pattern 129,3737 -(defvar plastic-shell-cd 132,3862 -(defvar plastic-shell-abort-goal-regexp 136,4004 -(defvar plastic-shell-proof-completed-regexp 140,4172 -(defvar plastic-save-command-regexp143,4315 -(defvar plastic-goal-command-regexp145,4411 -(defvar plastic-kill-goal-command 148,4508 -(defvar plastic-forget-id-command 150,4609 -(defvar plastic-undoable-commands-regexp153,4690 -(defvar plastic-goal-regexp 165,5137 -(defvar plastic-outline-regexp167,5185 -(defvar plastic-outline-heading-end-regexp 173,5364 -(defvar plastic-shell-outline-regexp 175,5420 -(defvar plastic-shell-outline-heading-end-regexp 176,5478 -(defvar plastic-error-occurred 178,5549 -(define-derived-mode plastic-shell-mode 187,5881 -(define-derived-mode plastic-mode 193,6063 -(define-derived-mode plastic-goals-mode 207,6516 -(defun plastic-count-undos 216,6861 -(defun plastic-goal-command-p 236,7737 -(defun plastic-find-and-forget 241,7930 -(defun plastic-goal-hyp 276,9278 -(defun plastic-state-preserving-p 287,9528 -(defvar plastic-shell-current-line-width 309,10456 -(defun plastic-shell-adjust-line-width 317,10772 -(defun plastic-pre-shell-start 338,11653 -(defun plastic-mode-config 353,12219 -(defun plastic-show-shell-buffer 450,15864 -(defun plastic-equal-module-filename 456,15967 -(defun plastic-shell-compute-new-files-list 462,16245 -(defun plastic-shell-mode-config 478,16782 -(defun plastic-goals-mode-config 529,18975 -(defun plastic-small-bar 541,19257 -(defun plastic-large-bar 543,19346 -(defun plastic-preprocessing 545,19484 -(defun plastic-all-ctxt 596,21312 -(defun plastic-send-one-undo 603,21490 -(defun plastic-minibuf-cmd 613,21818 -(defun plastic-minibuf 625,22297 -(defun plastic-synchro 632,22503 -(defun plastic-send-minibuf 637,22644 -(defun plastic-had-error 645,22973 -(defun plastic-reset-error 649,23148 -(defun plastic-call-if-no-error 652,23287 -(defun plastic-show-shell 657,23491 -(define-key plastic-keymap 666,23753 -(define-key plastic-keymap 667,23814 -(define-key plastic-keymap 668,23875 -(define-key plastic-keymap 669,23935 -(define-key plastic-keymap 670,23994 -(define-key plastic-keymap 671,24053 -(defalias 'proof-toolbar-command proof-toolbar-command681,24303 -(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd682,24354 +(defvar x-symbol-phox-required-fonts 16,473 +(defcustom x-symbol-phox-header-groups-alist 31,1080 +(defcustom x-symbol-phox-electric-ignore 38,1300 +(defvar x-symbol-phox-required-fonts 45,1516 +(defvar x-symbol-phox-extra-menu-items 48,1617 +(defvar x-symbol-phox-token-grammar51,1706 +(defvar x-symbol-phox-input-token-grammar65,2497 +(defun x-symbol-phox-default-token-list 71,2752 +(defvar x-symbol-phox-user-table 83,3070 +(defvar x-symbol-phox-generated-data 86,3179 +(defvar x-symbol-phox-master-directory 94,3418 +(defvar x-symbol-phox-image-searchpath 95,3467 +(defvar x-symbol-phox-image-cached-dirs 96,3515 +(defvar x-symbol-phox-image-file-truename-alist 97,3581 +(defvar x-symbol-phox-image-keywords 98,3634 +(defcustom x-symbol-phox-class-alist105,3855 +(defcustom x-symbol-phox-class-face-alist 116,4237 +(defvar x-symbol-phox-font-lock-keywords 126,4550 +(defvar x-symbol-phox-font-lock-allowed-faces 128,4597 +(defvar x-symbol-phox-case-insensitive 134,4822 +(defvar x-symbol-phox-token-shape 135,4866 +(defvar x-symbol-phox-input-token-ignore 136,4905 +(defvar x-symbol-phox-token-list 143,5144 +(defvar x-symbol-phox-xsymb0-table 145,5189 +(defun x-symbol-phox-prepare-table 166,5648 +(defvar x-symbol-phox-table174,5824 +(defcustom x-symbol-phox-auto-style185,6142 +(defvar x-symbol-phox-menu-alist 211,7092 +(defvar x-symbol-phox-grid-alist 213,7182 +(defvar x-symbol-phox-decode-atree 216,7273 +(defvar x-symbol-phox-decode-alist 218,7366 +(defvar x-symbol-phox-encode-alist 220,7463 +(defvar x-symbol-phox-nomule-decode-exec 224,7620 +(defvar x-symbol-phox-nomule-encode-exec 226,7720 + +plastic/plastic.el,2866 +(defcustom plastic-tags 29,821 +(defcustom plastic-test-all-name 34,953 +(defvar plastic-lit-string 41,1144 +(defcustom plastic-help-menu-list45,1258 +(defvar plastic-shell-process-output59,1752 +(defconst plastic-process-config 67,2078 +(defconst plastic-pretty-set-width 74,2328 +(defconst plastic-interrupt-regexp 78,2477 +(defcustom plastic-www-home-page 84,2598 +(defcustom plastic-www-latest-release89,2735 +(defcustom plastic-www-refcard95,2908 +(defcustom plastic-library-www-page101,3039 +(defcustom plastic-base 111,3254 +(defvar plastic-prog-name 119,3426 +(defun plastic-set-default-env-vars 123,3534 +(defvar plastic-shell-prompt-pattern 131,3772 +(defvar plastic-shell-cd 134,3897 +(defvar plastic-shell-abort-goal-regexp 138,4039 +(defvar plastic-shell-proof-completed-regexp 142,4207 +(defvar plastic-save-command-regexp145,4350 +(defvar plastic-goal-command-regexp147,4446 +(defvar plastic-kill-goal-command 150,4543 +(defvar plastic-forget-id-command 152,4644 +(defvar plastic-undoable-commands-regexp155,4725 +(defvar plastic-goal-regexp 167,5172 +(defvar plastic-outline-regexp169,5220 +(defvar plastic-outline-heading-end-regexp 175,5399 +(defvar plastic-shell-outline-regexp 177,5455 +(defvar plastic-shell-outline-heading-end-regexp 178,5513 +(defvar plastic-error-occurred 180,5584 +(define-derived-mode plastic-shell-mode 189,5916 +(define-derived-mode plastic-mode 195,6098 +(define-derived-mode plastic-goals-mode 209,6551 +(defun plastic-count-undos 218,6896 +(defun plastic-goal-command-p 238,7772 +(defun plastic-find-and-forget 243,7965 +(defun plastic-goal-hyp 278,9313 +(defun plastic-state-preserving-p 289,9563 +(defvar plastic-shell-current-line-width 312,10456 +(defun plastic-shell-adjust-line-width 320,10772 +(defun plastic-mode-config 347,11867 +(defun plastic-show-shell-buffer 436,15108 +(defun plastic-equal-module-filename 442,15211 +(defun plastic-shell-compute-new-files-list 448,15489 +(defun plastic-shell-mode-config 464,16026 +(defun plastic-goals-mode-config 515,18219 +(defun plastic-small-bar 527,18501 +(defun plastic-large-bar 529,18590 +(defun plastic-preprocessing 531,18728 +(defun plastic-all-ctxt 582,20556 +(defun plastic-send-one-undo 589,20734 +(defun plastic-minibuf-cmd 599,21062 +(defun plastic-minibuf 611,21541 +(defun plastic-synchro 618,21747 +(defun plastic-send-minibuf 623,21888 +(defun plastic-had-error 631,22217 +(defun plastic-reset-error 635,22392 +(defun plastic-call-if-no-error 638,22531 +(defun plastic-show-shell 643,22735 +(define-key plastic-keymap 652,22997 +(define-key plastic-keymap 653,23058 +(define-key plastic-keymap 654,23119 +(define-key plastic-keymap 655,23179 +(define-key plastic-keymap 656,23238 +(define-key plastic-keymap 657,23297 +(defalias 'proof-toolbar-command proof-toolbar-command667,23547 +(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd668,23598 plastic/plastic-syntax.el,648 (defconst plastic-keywords-goal 18,537 @@ -1092,163 +1151,168 @@ twelf/twelf-old.el,6958 (defun twelf-server-remove-menu 2651,107274 (defun twelf-server-reset-menu 2655,107386 -generic/pg-assoc.el,329 -(define-derived-mode proof-universal-keys-only-mode 20,563 -(defun proof-associated-buffers 32,987 -(defun proof-associated-windows 41,1184 -(defun pg-assoc-strip-subterm-markup 58,1665 -(defvar pg-assoc-ann-regexp 84,2598 -(defun pg-assoc-strip-subterm-markup-buf 87,2693 -(defun pg-assoc-strip-subterm-markup-buf-old 110,3412 - -generic/pg-autotest.el,442 -(defvar pg-autotest-success 21,538 -(defun pg-autotest-find-file 25,622 -(defun pg-autotest-find-file-restart 32,893 -(defmacro pg-autotest 45,1341 -(defun pg-autotest-script-wholefile 59,1689 -(defun pg-autotest-retract-file 76,2302 -(defun pg-autotest-assert-processed 82,2438 -(defun pg-autotest-assert-unprocessed 89,2684 -(defun pg-autotest-message 96,2931 -(defun pg-autotest-quit-prover 103,3124 -(defun pg-autotest-finished 109,3306 - -generic/pg-goals.el,704 -(define-derived-mode proof-goals-mode 29,669 -(define-key proof-goals-mode-map 50,1432 -(define-key proof-goals-mode-map 53,1515 -(define-key proof-goals-mode-map 54,1585 -(define-key proof-goals-mode-map 62,2175 -(define-key proof-goals-mode-map 64,2248 -(define-key proof-goals-mode-map 65,2316 -(define-key proof-goals-mode-map 71,2750 -(defun proof-goals-config-done 86,3014 -(defun pg-goals-display 96,3302 -(defun pg-goals-analyse-structure 152,5455 -(defun pg-goals-make-top-span 279,10502 -(defun pg-goals-yank-subterm 319,12006 -(defun pg-goals-button-action 346,12906 -(defun proof-expand-path 367,13879 -(defun pg-goals-construct-command 376,14123 -(defun pg-goals-get-subterm-help 405,15148 - -generic/pg-metadata.el,128 -(defcustom pg-metadata-default-directory 23,628 -(defface proof-preparsed-span 28,802 -(defun pg-metadata-filename-for 39,1065 - -generic/pg-pbrpm.el,1781 -(defvar pg-pbrpm-use-buffer-menu 13,309 -(defvar pg-pbrpm-buffer-menu 15,428 -(defvar pg-pbrpm-spans 16,462 -(defvar pg-pbrpm-goal-description 17,490 -(defvar pg-pbrpm-windows-dialog-bug 18,529 -(defun pg-pbrpm-erase-buffer-menu 20,571 -(defun pg-pbrpm-menu-change-hook 27,755 -(defun pg-pbrpm-create-reset-buffer-menu 45,1332 -(defun pg-pbrpm-analyse-goal-buffer 59,1946 -(defun pg-pbrpm-button-action 120,4366 -(defun pg-pbrpm-exists 127,4592 -(defun pg-pbrpm-eliminate-id 131,4704 -(defun pg-pbrpm-build-menu 139,4952 -(defun pg-pbrpm-setup-span 199,7269 -(defun pg-pbrpm-run-command 259,9600 -(defun pg-pbrpm-get-pos-info 288,10911 -(defun pg-pbrpm-get-region-info 324,12053 -(defun auto-select-arround-pos 334,12378 -(defun pg-pbrpm-translate-position 346,12822 -(defun pg-pbrpm-process-click 352,13046 -(defvar pg-pbrpm-remember-region-selected-region 372,14053 -(defvar pg-pbrpm-regions-list 373,14107 -(defun pg-pbrpm-erase-regions-list 375,14143 -(defun pg-pbrpm-filter-regions-list 384,14452 -(defface pg-pbrpm-multiple-selection-face391,14715 -(defface pg-pbrpm-menu-input-face399,14920 -(defun pg-pbrpm-do-remember-region 407,15113 -(defun pg-pbrpm-remember-region-drag-up-hook 428,15964 -(defun pg-pbrpm-remember-region-click-hook 432,16135 -(defun pg-pbrpm-remember-region 437,16320 -(defun pg-pbrpm-process-region 451,17035 -(defun pg-pbrpm-process-regions-list 468,17761 -(defun pg-pbrpm-region-expression 472,17944 -(define-key proof-goals-mode-map 497,18906 -(define-key proof-goals-mode-map 498,18976 -(define-key proof-goals-mode-map 499,19053 -(define-key pg-span-context-menu-keymap 500,19133 -(define-key pg-span-context-menu-keymap 501,19210 -(define-key proof-mode-map 502,19293 -(define-key proof-mode-map 503,19357 -(define-key proof-mode-map 504,19428 - -generic/pg-pgip.el,2889 -(defalias 'pg-pgip-debug pg-pgip-debug29,883 -(defalias 'pg-pgip-error pg-pgip-error30,924 -(defalias 'pg-pgip-warning pg-pgip-warning31,959 -(defconst pg-pgip-version-supported 33,1009 -(defun pg-pgip-process-packet 37,1115 -(defvar pg-pgip-last-seen-id 47,1688 -(defvar pg-pgip-last-seen-seq 48,1722 -(defun pg-pgip-process-pgip 50,1758 -(defun pg-pgip-process-msg 69,2689 -(defvar pg-pgip-post-process-functions83,3259 -(defun pg-pgip-post-process 93,3746 -(defun pg-pgip-process-askpgip 109,4357 -(defun pg-pgip-process-usespgip 114,4516 -(defun pg-pgip-process-usespgml 118,4680 -(defun pg-pgip-process-pgmlconfig 122,4844 -(defun pg-pgip-process-proverinfo 138,5463 -(defun pg-pgip-process-hasprefs 155,6128 -(defun pg-pgip-haspref 169,6760 -(defun pg-pgip-process-prefval 188,7539 -(defun pg-pgip-process-guiconfig 215,8248 -(defvar proof-assistant-idtables 222,8365 -(defun pg-pgip-process-ids 225,8482 -(defun pg-complete-idtable-symbol 251,9561 -(defalias 'pg-pgip-process-setids pg-pgip-process-setids256,9653 -(defalias 'pg-pgip-process-addids pg-pgip-process-addids257,9709 -(defalias 'pg-pgip-process-delids pg-pgip-process-delids258,9765 -(defun pg-pgip-process-idvalue 261,9823 -(defun pg-pgip-process-menuadd 273,10160 -(defun pg-pgip-process-menudel 276,10203 -(defun pg-pgip-process-ready 285,10436 -(defun pg-pgip-process-cleardisplay 288,10477 -(defun pg-pgip-process-proofstate 302,10954 -(defun pg-pgip-process-normalresponse 306,11031 -(defun pg-pgip-process-errorresponse 310,11155 -(defun pg-pgip-process-scriptinsert 314,11278 -(defun pg-pgip-process-metainforesponse 319,11412 -(defun pg-pgip-process-informfileloaded 328,11653 -(defun pg-pgip-process-informfileretracted 334,11920 -(defun pg-pgip-process-brokerstatus 347,12397 -(defun pg-pgip-process-proveravailmsg 350,12445 -(defun pg-pgip-process-newprovermsg 353,12495 -(defun pg-pgip-process-proverstatusmsg 356,12543 -(defvar pg-pgip-srcids 365,12790 -(defun pg-pgip-process-newfile 369,12897 -(defun pg-pgip-process-filestatus 385,13485 -(defun pg-pgip-process-newobj 405,14140 -(defun pg-pgip-process-delobj 408,14182 -(defun pg-pgip-process-objectstatus 411,14224 -(defun pg-pgip-process-parsescript 425,14580 -(defun pg-pgip-get-pgiptype 448,15455 -(defun pg-pgip-default-for 468,16252 -(defun pg-pgip-subst-for 481,16647 -(defun pg-pgip-interpret-value 493,16990 -(defun pg-pgip-interpret-choice 511,17676 -(defun pg-pgip-string-of-command 542,18696 -(defconst pg-pgip-id559,19457 -(defvar pg-pgip-refseq 565,19737 -(defvar pg-pgip-refid 567,19835 -(defvar pg-pgip-seq 570,19929 -(defun pg-pgip-assemble-packet 572,19993 -(defun pg-pgip-issue 590,20808 -(defun pg-pgip-maybe-askpgip 607,21421 -(defun pg-pgip-askprefs 613,21612 -(defun pg-pgip-askids 617,21726 -(defun pg-pgip-reset 630,22017 -(defconst pg-pgip-start-element-regexp 661,22715 -(defconst pg-pgip-end-element-regexp 662,22767 +generic/pg-assoc.el,354 +(defun proof-associated-buffers 35,1072 +(defun proof-associated-windows 44,1269 +(defun pg-assoc-strip-subterm-markup 61,1750 +(defvar pg-assoc-ann-regexp 87,2683 +(defun pg-assoc-strip-subterm-markup-buf 90,2778 +(defun pg-assoc-strip-subterm-markup-buf-old 113,3497 +(defun pg-assoc-make-top-span 142,4352 +(defun pg-assoc-analyse-structure 171,5571 + +generic/pg-autotest.el,443 +(defvar pg-autotest-success 26,573 +(defun pg-autotest-find-file 30,657 +(defun pg-autotest-find-file-restart 37,937 +(defmacro pg-autotest 50,1385 +(defun pg-autotest-script-wholefile 64,1732 +(defun pg-autotest-retract-file 81,2345 +(defun pg-autotest-assert-processed 87,2481 +(defun pg-autotest-assert-unprocessed 94,2735 +(defun pg-autotest-message 101,2995 +(defun pg-autotest-quit-prover 108,3188 +(defun pg-autotest-finished 114,3369 + +generic/pg-custom.el,673 +(defpgcustom x-symbol-enable 32,1033 +(defpgcustom x-symbol-language 41,1383 +(defpgcustom maths-menu-enable 46,1605 +(defpgcustom mmm-enable 52,1785 +(defpgcustom script-indent 61,2139 +(defpgcustom toolbar-entries 66,2276 +(defpgcustom prog-args 84,2996 +(defpgcustom prog-env 97,3571 +(defpgcustom favourites 106,3997 +(defpgcustom menu-entries 111,4186 +(defpgcustom help-menu-entries 118,4422 +(defpgcustom keymap 125,4685 +(defpgcustom completion-table 130,4857 +(defpgcustom tags-program 141,5231 +(defconst proof-mode-for-shell 151,5403 +(defconst proof-mode-for-response 155,5533 +(defconst proof-mode-for-goals 159,5701 +(defconst proof-mode-for-script 163,5829 + +generic/pg-goals.el,363 +(define-derived-mode proof-goals-mode 33,663 +(define-key proof-goals-mode-map 63,1542 +(defun proof-goals-config-done 93,3010 +(defun pg-goals-display 103,3298 +(defun pg-goals-yank-subterm 169,5735 +(defun pg-goals-button-action 196,6635 +(defun proof-expand-path 217,7607 +(defun pg-goals-construct-command 226,7849 +(defun pg-goals-get-subterm-help 255,8870 + +generic/pg-metadata.el,127 +(defcustom pg-metadata-default-directory 26,647 +(defface proof-preparsed-span31,821 +(defun pg-metadata-filename-for 42,1083 + +generic/pg-pbrpm.el,1433 +(defvar pg-pbrpm-use-buffer-menu 10,270 +(defvar pg-pbrpm-buffer-menu 12,391 +(defvar pg-pbrpm-spans 13,425 +(defvar pg-pbrpm-goal-description 14,453 +(defvar pg-pbrpm-windows-dialog-bug 15,492 +(defun pg-pbrpm-erase-buffer-menu 17,534 +(defun pg-pbrpm-menu-change-hook 24,718 +(defun pg-pbrpm-create-reset-buffer-menu 42,1294 +(defun pg-pbrpm-analyse-goal-buffer 57,1923 +(defun pg-pbrpm-button-action 117,4333 +(defun pg-pbrpm-exists 124,4559 +(defun pg-pbrpm-eliminate-id 128,4671 +(defun pg-pbrpm-build-menu 136,4917 +(defun pg-pbrpm-setup-span 196,7229 +(defun pg-pbrpm-run-command 256,9546 +(defun pg-pbrpm-get-pos-info 285,10856 +(defun pg-pbrpm-get-region-info 321,11993 +(defun auto-select-arround-pos 331,12318 +(defun pg-pbrpm-translate-position 343,12762 +(defun pg-pbrpm-process-click 349,12985 +(defvar pg-pbrpm-remember-region-selected-region 369,13990 +(defvar pg-pbrpm-regions-list 370,14044 +(defun pg-pbrpm-erase-regions-list 372,14080 +(defun pg-pbrpm-filter-regions-list 381,14388 +(defface pg-pbrpm-multiple-selection-face388,14651 +(defface pg-pbrpm-menu-input-face396,14853 +(defun pg-pbrpm-do-remember-region 404,15043 +(defun pg-pbrpm-remember-region-drag-up-hook 425,15891 +(defun pg-pbrpm-remember-region-click-hook 429,16062 +(defun pg-pbrpm-remember-region 434,16247 +(defun pg-pbrpm-process-region 448,16962 +(defun pg-pbrpm-process-regions-list 465,17687 +(defun pg-pbrpm-region-expression 469,17870 + +generic/pg-pgip.el,2890 +(defalias 'pg-pgip-debug pg-pgip-debug35,939 +(defalias 'pg-pgip-error pg-pgip-error36,980 +(defalias 'pg-pgip-warning pg-pgip-warning37,1015 +(defconst pg-pgip-version-supported 39,1065 +(defun pg-pgip-process-packet 43,1171 +(defvar pg-pgip-last-seen-id 53,1743 +(defvar pg-pgip-last-seen-seq 54,1777 +(defun pg-pgip-process-pgip 56,1813 +(defun pg-pgip-process-msg 75,2744 +(defvar pg-pgip-post-process-functions89,3311 +(defun pg-pgip-post-process 99,3799 +(defun pg-pgip-process-askpgip 115,4410 +(defun pg-pgip-process-usespgip 120,4569 +(defun pg-pgip-process-usespgml 124,4733 +(defun pg-pgip-process-pgmlconfig 128,4897 +(defun pg-pgip-process-proverinfo 144,5514 +(defun pg-pgip-process-hasprefs 161,6179 +(defun pg-pgip-haspref 175,6811 +(defun pg-pgip-process-prefval 194,7587 +(defun pg-pgip-process-guiconfig 221,8296 +(defvar proof-assistant-idtables 228,8413 +(defun pg-pgip-process-ids 231,8530 +(defun pg-complete-idtable-symbol 257,9606 +(defalias 'pg-pgip-process-setids pg-pgip-process-setids262,9698 +(defalias 'pg-pgip-process-addids pg-pgip-process-addids263,9754 +(defalias 'pg-pgip-process-delids pg-pgip-process-delids264,9810 +(defun pg-pgip-process-idvalue 267,9868 +(defun pg-pgip-process-menuadd 279,10204 +(defun pg-pgip-process-menudel 282,10247 +(defun pg-pgip-process-ready 291,10480 +(defun pg-pgip-process-cleardisplay 294,10521 +(defun pg-pgip-process-proofstate 308,10978 +(defun pg-pgip-process-normalresponse 312,11055 +(defun pg-pgip-process-errorresponse 316,11179 +(defun pg-pgip-process-scriptinsert 320,11302 +(defun pg-pgip-process-metainforesponse 325,11436 +(defun pg-pgip-process-informfileloaded 334,11677 +(defun pg-pgip-process-informfileretracted 340,11943 +(defun pg-pgip-process-brokerstatus 353,12420 +(defun pg-pgip-process-proveravailmsg 356,12468 +(defun pg-pgip-process-newprovermsg 359,12518 +(defun pg-pgip-process-proverstatusmsg 362,12566 +(defvar pg-pgip-srcids 371,12813 +(defun pg-pgip-process-newfile 375,12920 +(defun pg-pgip-process-filestatus 391,13508 +(defun pg-pgip-process-newobj 411,14163 +(defun pg-pgip-process-delobj 414,14205 +(defun pg-pgip-process-objectstatus 417,14247 +(defun pg-pgip-process-parsescript 431,14602 +(defun pg-pgip-get-pgiptype 454,15477 +(defun pg-pgip-default-for 474,16270 +(defun pg-pgip-subst-for 487,16665 +(defun pg-pgip-interpret-value 499,17008 +(defun pg-pgip-interpret-choice 517,17693 +(defun pg-pgip-string-of-command 548,18710 +(defconst pg-pgip-id565,19471 +(defvar pg-pgip-refseq 571,19751 +(defvar pg-pgip-refid 573,19848 +(defvar pg-pgip-seq 576,19940 +(defun pg-pgip-assemble-packet 578,20004 +(defun pg-pgip-issue 596,20816 +(defun pg-pgip-maybe-askpgip 613,21428 +(defun pg-pgip-askprefs 619,21619 +(defun pg-pgip-askids 623,21733 +(defun pg-pgip-reset 636,22021 +(defconst pg-pgip-start-element-regexp 667,22719 +(defconst pg-pgip-end-element-regexp 668,22771 generic/pg-pgip-old.el,456 (defun pg-pgip-process-oldhaspref 18,633 @@ -1263,373 +1327,352 @@ generic/pg-pgip-old.el,456 (defun pg-pgip-old-get-type 131,4423 (defun pg-pgip-old-pgiptype 138,4639 -generic/pg-response.el,1188 -(define-derived-mode proof-response-mode 25,617 -(defun proof-response-config-done 50,1658 -(defvar proof-shell-special-display-regexp 71,2433 -(defconst proof-multiframe-specifiers 79,2838 -(defun proof-map-multiple-frame-specifiers 88,3202 -(defconst proof-multiframe-parameters98,3664 -(defun proof-multiple-frames-enable 107,3963 -(defun proof-three-window-enable 129,4683 -(defun proof-select-three-b 133,4747 -(defun proof-display-three-b 148,5216 -(defvar pg-frame-configuration 162,5710 -(defun pg-cache-frame-configuration 166,5857 -(defun proof-layout-windows 170,6028 -(defun proof-delete-other-frames 211,7841 -(defvar pg-response-erase-flag 242,8936 -(defun proof-shell-maybe-erase-response245,9051 -(defun pg-response-display 276,10253 -(defun pg-response-display-with-face 294,11107 -(defun pg-response-clear-displays 332,12464 -(defvar pg-response-next-error 350,13043 -(defun proof-next-error 354,13165 -(defun pg-response-has-error-location 434,16105 -(defvar proof-trace-last-fontify-pos 457,16938 -(defun proof-trace-fontify-pos 459,16981 -(defun proof-trace-buffer-display 467,17295 -(defun proof-trace-buffer-finish 491,18268 -(defun pg-thms-buffer-clear 512,18847 +generic/pg-response.el,1222 +(defvar pg-response-next-error 31,694 +(deflocal pg-response-eagerly-raise 34,801 +(define-derived-mode proof-response-mode 44,1026 +(defun proof-response-config-done 68,2027 +(defvar pg-response-special-display-regexp 89,2802 +(defconst proof-multiframe-specifiers97,3208 +(defun proof-map-multiple-frame-specifiers 106,3565 +(defconst proof-multiframe-parameters117,4087 +(defun proof-multiple-frames-enable 126,4386 +(defun proof-three-window-enable 144,5030 +(defun proof-select-three-b 148,5094 +(defun proof-display-three-b 163,5563 +(defvar pg-frame-configuration 177,6055 +(defun pg-cache-frame-configuration 181,6202 +(defun proof-layout-windows 185,6373 +(defun proof-delete-other-frames 226,8196 +(defvar pg-response-erase-flag 257,9286 +(defun pg-response-maybe-erase261,9415 +(defun pg-response-display 292,10600 +(defun pg-response-display-with-face 310,11433 +(defun pg-response-clear-displays 347,12731 +(defun proof-next-error 366,13318 +(defun pg-response-has-error-location 447,16234 +(defvar proof-trace-last-fontify-pos 470,17067 +(defun proof-trace-fontify-pos 472,17110 +(defun proof-trace-buffer-display 480,17423 +(defun proof-trace-buffer-finish 504,18423 +(defun pg-thms-buffer-clear 525,19003 generic/pg-thymodes.el,152 -(defmacro pg-defthymode 19,466 -(defmacro pg-do-unless-null 67,2277 -(defun pg-symval 72,2364 -(defun pg-modesym 78,2520 -(defun pg-modesymval 82,2634 - -generic/pg-user.el,2335 -(defmacro proof-maybe-save-point 21,410 -(defun proof-maybe-follow-locked-end 29,612 -(defun proof-assert-next-command-interactive 43,977 -(defun proof-process-buffer 53,1348 -(defun proof-undo-last-successful-command 67,1665 -(defun proof-undo-and-delete-last-successful-command 72,1827 -(defun proof-undo-last-successful-command-1 94,2799 -(defun proof-retract-buffer 110,3364 -(defun proof-retract-current-goal 119,3644 -(defun proof-interrupt-process 137,4135 -(defun proof-goto-command-start 164,5120 -(defun proof-goto-command-end 187,6062 -(defun proof-mouse-goto-point 212,6842 -(defun proof-mouse-track-insert 227,7416 -(defvar proof-minibuffer-history 262,8526 -(defun proof-minibuffer-cmd 265,8620 -(defun proof-frob-locked-end 313,10426 -(defmacro proof-if-setting-configured 406,13340 -(defmacro proof-define-assistant-command 414,13610 -(defmacro proof-define-assistant-command-witharg 427,14076 -(defun proof-issue-new-command 447,14901 -(defun proof-cd-sync 492,16400 -(deflocal proof-electric-terminator 543,17869 -(defun proof-electric-terminator-enable 553,18216 -(defun proof-electric-term-incomment-fn 564,18703 -(defun proof-process-electric-terminator 584,19459 -(defun proof-electric-terminator 611,20610 -(defun proof-add-completions 633,21248 -(defun proof-script-complete 653,22005 -(defun pg-insert-last-output-as-comment 681,22596 -(defun pg-copy-span-contents 712,23824 -(defun pg-numth-span-higher-or-lower 729,24384 -(defun pg-control-span-of 755,25131 -(defun pg-move-span-contents 761,25335 -(defun pg-fixup-children-span 815,27559 -(defun pg-move-region-down 822,27762 -(defun pg-move-region-up 831,28056 -(defun proof-forward-command 861,28896 -(defun proof-backward-command 882,29618 -(defvar pg-span-context-menu-keymap898,29862 -(defun pg-span-for-event 914,30289 -(defun pg-span-context-menu 925,30673 -(defun pg-toggle-visibility 940,31133 -(defun pg-create-in-span-context-menu 950,31455 -(defun pg-span-undo 983,32807 -(defun pg-goals-buffers-hint 1029,34217 -(defun pg-slow-fontify-tracing-hint 1032,34384 -(defun pg-response-buffers-hint 1035,34540 -(defun pg-jump-to-end-hint 1044,34889 -(defun pg-processing-complete-hint 1047,35005 -(defun pg-next-error-hint 1063,35691 -(defun pg-hint 1067,35828 -(defun pg-identifier-under-mouse-query 1086,36504 -(defun proof-imenu-enable 1131,38131 - -generic/pg-xhtml.el,392 -(defvar pg-xhtml-dir 17,423 -(defun pg-xhtml-dir 20,489 -(defvar pg-xhtml-file-count 32,856 -(defun pg-xhtml-next-file 35,928 -(defvar pg-xhtml-header 47,1159 -(defmacro pg-xhtml-write-tempfile 53,1400 -(defun pg-xhtml-cleanup-tempdir 71,1996 -(defvar pg-mozilla-prog-name 75,2127 -(defun pg-xhtml-display-file-mozilla 79,2235 -(defalias 'pg-xhtml-display-file pg-xhtml-display-file84,2408 - -generic/pg-xml.el,1096 -(defun pg-xml-parse-string 40,1169 -(defun pg-xml-parse-buffer 51,1503 -(defun pg-xml-get-attr 73,2236 -(defun pg-xml-child-elts 81,2540 -(defun pg-xml-child-elt 86,2745 -(defun pg-xml-get-child 94,3028 -(defun pg-xml-get-text-content 104,3400 -(defmacro pg-xml-attr 115,3750 -(defmacro pg-xml-node 117,3812 -(defconst pg-xml-header 120,3905 -(defun pg-xml-string-of 124,3982 -(defun pg-xml-output-internal 135,4354 -(defun pg-xml-cdata 169,5504 -(defun pg-pgip-get-icon 177,5697 -(defsubst pg-pgip-get-name 181,5845 -(defsubst pg-pgip-get-version 184,5962 -(defsubst pg-pgip-get-descr 187,6085 -(defsubst pg-pgip-get-thmname 190,6204 -(defsubst pg-pgip-get-thyname 193,6327 -(defsubst pg-pgip-get-url 196,6450 -(defsubst pg-pgip-get-srcid 199,6565 -(defsubst pg-pgip-get-proverid 202,6684 -(defsubst pg-pgip-get-symname 205,6809 -(defsubst pg-pgip-get-prefcat 208,6929 -(defsubst pg-pgip-get-default 211,7057 -(defsubst pg-pgip-get-objtype 214,7180 -(defsubst pg-pgip-get-value 217,7303 -(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext220,7373 -(defun pg-pgip-get-pgmltext 222,7432 +(defmacro pg-defthymode 23,499 +(defmacro pg-do-unless-null 71,2307 +(defun pg-symval 76,2394 +(defun pg-modesym 82,2549 +(defun pg-modesymval 86,2663 + +generic/pg-user.el,2336 +(defmacro proof-maybe-save-point 22,441 +(defun proof-maybe-follow-locked-end 30,643 +(defun proof-assert-next-command-interactive 44,1008 +(defun proof-process-buffer 54,1379 +(defun proof-undo-last-successful-command 68,1696 +(defun proof-undo-and-delete-last-successful-command 73,1858 +(defun proof-undo-last-successful-command-1 95,2829 +(defun proof-retract-buffer 111,3394 +(defun proof-retract-current-goal 120,3674 +(defun proof-interrupt-process 138,4165 +(defun proof-goto-command-start 165,5146 +(defun proof-goto-command-end 188,6086 +(defun proof-mouse-goto-point 213,6864 +(defun proof-mouse-track-insert 228,7435 +(defvar proof-minibuffer-history 263,8543 +(defun proof-minibuffer-cmd 266,8638 +(defun proof-frob-locked-end 314,10436 +(defmacro proof-if-setting-configured 407,13352 +(defmacro proof-define-assistant-command 415,13621 +(defmacro proof-define-assistant-command-witharg 428,14084 +(defun proof-issue-new-command 448,14907 +(defun proof-cd-sync 493,16402 +(deflocal proof-electric-terminator 544,17867 +(defun proof-electric-terminator-enable 554,18214 +(defun proof-electric-term-incomment-fn 565,18700 +(defun proof-process-electric-terminator 585,19451 +(defun proof-electric-terminator 612,20599 +(defun proof-add-completions 634,21234 +(defun proof-script-complete 654,21988 +(defun pg-insert-last-output-as-comment 682,22579 +(defun pg-copy-span-contents 713,23805 +(defun pg-numth-span-higher-or-lower 730,24363 +(defun pg-control-span-of 756,25109 +(defun pg-move-span-contents 762,25313 +(defun pg-fixup-children-span 816,27536 +(defun pg-move-region-down 823,27739 +(defun pg-move-region-up 832,28032 +(defun proof-forward-command 862,28870 +(defun proof-backward-command 883,29591 +(defvar pg-span-context-menu-keymap899,29835 +(defun pg-span-for-event 915,30257 +(defun pg-span-context-menu 926,30635 +(defun pg-toggle-visibility 941,31090 +(defun pg-create-in-span-context-menu 951,31412 +(defun pg-span-undo 984,32756 +(defun pg-goals-buffers-hint 1030,34166 +(defun pg-slow-fontify-tracing-hint 1033,34333 +(defun pg-response-buffers-hint 1036,34489 +(defun pg-jump-to-end-hint 1045,34836 +(defun pg-processing-complete-hint 1048,34952 +(defun pg-next-error-hint 1064,35636 +(defun pg-hint 1068,35773 +(defun pg-identifier-under-mouse-query 1087,36443 +(defun proof-imenu-enable 1132,38065 + +generic/pg-xhtml.el,390 +(defvar pg-xhtml-dir 24,472 +(defun pg-xhtml-dir 27,538 +(defvar pg-xhtml-file-count 39,905 +(defun pg-xhtml-next-file 42,977 +(defvar pg-xhtml-header54,1207 +(defmacro pg-xhtml-write-tempfile 60,1447 +(defun pg-xhtml-cleanup-tempdir 78,2042 +(defvar pg-mozilla-prog-name82,2173 +(defun pg-xhtml-display-file-mozilla 86,2280 +(defalias 'pg-xhtml-display-file pg-xhtml-display-file91,2449 + +generic/pg-xml.el,1095 +(defun pg-xml-parse-string 40,1165 +(defun pg-xml-parse-buffer 51,1498 +(defun pg-xml-get-attr 73,2231 +(defun pg-xml-child-elts 81,2534 +(defun pg-xml-child-elt 86,2739 +(defun pg-xml-get-child 94,3021 +(defun pg-xml-get-text-content 104,3393 +(defmacro pg-xml-attr 115,3743 +(defmacro pg-xml-node 117,3805 +(defconst pg-xml-header120,3897 +(defun pg-xml-string-of 124,3973 +(defun pg-xml-output-internal 135,4344 +(defun pg-xml-cdata 169,5494 +(defun pg-pgip-get-icon 177,5687 +(defsubst pg-pgip-get-name 181,5835 +(defsubst pg-pgip-get-version 184,5952 +(defsubst pg-pgip-get-descr 187,6075 +(defsubst pg-pgip-get-thmname 190,6194 +(defsubst pg-pgip-get-thyname 193,6317 +(defsubst pg-pgip-get-url 196,6440 +(defsubst pg-pgip-get-srcid 199,6555 +(defsubst pg-pgip-get-proverid 202,6674 +(defsubst pg-pgip-get-symname 205,6799 +(defsubst pg-pgip-get-prefcat 208,6919 +(defsubst pg-pgip-get-default 211,7047 +(defsubst pg-pgip-get-objtype 214,7170 +(defsubst pg-pgip-get-value 217,7293 +(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext220,7363 +(defun pg-pgip-get-pgmltext 222,7422 generic/proof-autoloads.el,57 -(defalias (quote proof-x-symbol-decode-region)421,14247 - -generic/proof-config.el,11099 -(defgroup proof-user-options 84,3173 -(defcustom proof-electric-terminator-enable 89,3287 -(defcustom proof-toolbar-enable 101,3821 -(defcustom proof-imenu-enable 107,3994 -(defpgcustom x-symbol-enable 113,4165 -(defpgcustom maths-menu-enable 122,4515 -(defpgcustom mmm-enable 128,4695 -(defcustom pg-show-hints 137,5049 -(defcustom proof-output-fontify-enable 142,5184 -(defcustom proof-trace-output-slow-catchup 152,5566 -(defcustom proof-strict-state-preserving 162,6064 -(defcustom proof-strict-read-only 175,6673 -(defcustom proof-three-window-enable 185,7023 -(defcustom proof-multiple-frames-enable 204,7778 -(defcustom proof-delete-empty-windows 213,8114 -(defcustom proof-shrink-windows-tofit 224,8645 -(defcustom proof-toolbar-use-button-enablers 231,8917 -(defcustom proof-query-file-save-when-activating-scripting 254,9789 -(defpgcustom script-indent 270,10512 -(defcustom proof-one-command-per-line 276,10700 -(defcustom proof-prog-name-ask 284,10920 -(defcustom proof-prog-name-guess 290,11081 -(defcustom proof-tidy-response298,11341 -(defcustom proof-keep-response-history312,11808 -(defcustom proof-general-debug 322,12195 -(defcustom proof-experimental-features 331,12568 -(defcustom proof-follow-mode 349,13330 -(defcustom proof-auto-action-when-deactivating-scripting 375,14525 -(defcustom proof-script-command-separator 398,15476 -(defcustom proof-rsh-command 406,15769 -(defcustom proof-disappearing-proofs 422,16320 -(defgroup proof-faces 449,16970 -(defface proof-queue-face 454,17076 -(defface proof-locked-face462,17356 -(defface proof-declaration-name-face475,17859 -(defconst proof-declaration-name-face 487,18252 -(defface proof-tacticals-name-face492,18488 -(defconst proof-tacticals-name-face 501,18750 -(defface proof-tactics-name-face506,18980 -(defconst proof-tactics-name-face 515,19245 -(defface proof-error-face 520,19469 -(defface proof-warning-face528,19676 -(defconst proof-warning-face 537,19933 -(defface proof-eager-annotation-face539,19984 -(defface proof-debug-message-face547,20202 -(defface proof-boring-face555,20401 -(defface proof-mouse-highlight-face563,20593 -(defface proof-highlight-dependent-face571,20789 -(defface proof-highlight-dependency-face579,20998 -(defface proof-active-area-face 587,21195 -(defgroup prover-config 604,21471 -(defcustom proof-mode-for-shell 638,22590 -(defcustom proof-mode-for-response 645,22837 -(defcustom proof-mode-for-goals 652,23120 -(defcustom proof-mode-for-script 659,23375 -(defcustom proof-guess-command-line 670,23809 -(defcustom proof-assistant-home-page 685,24306 -(defcustom proof-context-command 691,24476 -(defcustom proof-info-command 696,24610 -(defcustom proof-showproof-command 703,24882 -(defcustom proof-goal-command 708,25018 -(defcustom proof-save-command 716,25316 -(defcustom proof-find-theorems-command 724,25626 -(defconst proof-toolbar-entries-default731,25935 -(defpgcustom toolbar-entries 765,27853 -(defcustom proof-assistant-true-value 783,28574 -(defcustom proof-assistant-false-value 789,28764 -(defcustom proof-assistant-format-int-fn 795,28958 -(defcustom proof-assistant-format-string-fn 802,29207 -(defcustom proof-assistant-setting-format 809,29474 -(defgroup proof-script 831,30169 -(defcustom proof-terminal-char 836,30299 -(defcustom proof-script-sexp-commands 846,30703 -(defcustom proof-script-command-end-regexp 857,31173 -(defcustom proof-script-command-start-regexp 875,31992 -(defcustom proof-script-use-old-parser 886,32454 -(defcustom proof-script-integral-proofs 898,32943 -(defcustom proof-script-fly-past-comments 913,33599 -(defcustom proof-script-parse-function 920,33916 -(defcustom proof-script-comment-start 938,34562 -(defcustom proof-script-comment-start-regexp 949,34997 -(defcustom proof-script-comment-end 957,35314 -(defcustom proof-script-comment-end-regexp 969,35732 -(defcustom pg-insert-output-as-comment-fn 977,36043 -(defcustom proof-string-start-regexp 983,36295 -(defcustom proof-string-end-regexp 988,36460 -(defcustom proof-case-fold-search 993,36621 -(defcustom proof-save-command-regexp 1002,37037 -(defcustom proof-save-with-hole-regexp 1007,37148 -(defcustom proof-save-with-hole-result 1019,37600 -(defcustom proof-goal-command-regexp 1030,38064 -(defcustom proof-goal-with-hole-regexp 1039,38456 -(defcustom proof-goal-with-hole-result 1051,38900 -(defcustom proof-non-undoables-regexp 1061,39299 -(defcustom proof-nested-undo-regexp 1072,39755 -(defcustom proof-ignore-for-undo-count 1088,40467 -(defcustom proof-script-next-entity-regexps 1096,40770 -(defcustom proof-script-find-next-entity-fn1140,42504 -(defcustom proof-script-imenu-generic-expression 1160,43334 -(defcustom proof-goal-command-p 1178,44189 -(defcustom proof-really-save-command-p 1205,45630 -(defcustom proof-completed-proof-behaviour 1217,46091 -(defcustom proof-count-undos-fn 1245,47451 -(defconst proof-no-command 1280,49052 -(defcustom proof-find-and-forget-fn 1285,49256 -(defcustom proof-forget-id-command 1302,49967 -(defcustom pg-topterm-goalhyplit-fn 1312,50325 -(defcustom proof-kill-goal-command 1324,50881 -(defcustom proof-undo-n-times-cmd 1338,51391 -(defcustom proof-nested-goals-history-p 1352,51940 -(defcustom proof-state-preserving-p 1361,52278 -(defcustom proof-activate-scripting-hook 1371,52748 -(defcustom proof-deactivate-scripting-hook 1390,53526 -(defcustom proof-indent 1403,53891 -(defcustom proof-indent-hang 1408,53998 -(defcustom proof-indent-enclose-offset 1413,54124 -(defcustom proof-indent-open-offset 1418,54266 -(defcustom proof-indent-close-offset 1423,54403 -(defcustom proof-indent-any-regexp 1428,54541 -(defcustom proof-indent-inner-regexp 1433,54701 -(defcustom proof-indent-enclose-regexp 1438,54855 -(defcustom proof-indent-open-regexp 1443,55009 -(defcustom proof-indent-close-regexp 1448,55161 -(defcustom proof-script-font-lock-keywords 1454,55315 -(defcustom proof-script-syntax-table-entries 1462,55638 -(defcustom proof-script-span-context-menu-extensions 1480,56035 -(defgroup proof-shell 1506,56824 -(defcustom proof-prog-name 1516,56995 -(defpgcustom prog-args 1529,57630 -(defpgcustom prog-env 1542,58205 -(defcustom proof-shell-auto-terminate-commands 1551,58631 -(defcustom proof-shell-pre-sync-init-cmd 1560,59028 -(defcustom proof-shell-init-cmd 1574,59587 -(defcustom proof-shell-restart-cmd 1585,60057 -(defcustom proof-shell-quit-cmd 1590,60212 -(defcustom proof-shell-quit-timeout 1595,60379 -(defcustom proof-shell-cd-cmd 1605,60827 -(defcustom proof-shell-start-silent-cmd 1622,61494 -(defcustom proof-shell-stop-silent-cmd 1631,61870 -(defcustom proof-shell-silent-threshold 1640,62207 -(defcustom proof-shell-inform-file-processed-cmd 1648,62541 -(defcustom proof-shell-inform-file-retracted-cmd 1669,63464 -(defcustom proof-auto-multiple-files 1697,64735 -(defcustom proof-cannot-reopen-processed-files 1712,65456 -(defcustom proof-shell-require-command-regexp 1726,66123 -(defcustom proof-done-advancing-require-function 1737,66585 -(defcustom proof-shell-quiet-errors 1743,66825 -(defcustom proof-shell-prompt-pattern 1756,67159 -(defcustom proof-shell-wakeup-char 1766,67581 -(defcustom proof-shell-annotated-prompt-regexp 1772,67812 -(defcustom proof-shell-abort-goal-regexp 1788,68452 -(defcustom proof-shell-error-regexp 1793,68587 -(defcustom proof-shell-truncate-before-error 1813,69381 -(defcustom pg-next-error-regexp 1827,69924 -(defcustom pg-next-error-filename-regexp 1842,70534 -(defcustom pg-next-error-extract-filename 1866,71572 -(defcustom proof-shell-interrupt-regexp 1873,71815 -(defcustom proof-shell-proof-completed-regexp 1887,72407 -(defcustom proof-shell-clear-response-regexp 1900,72915 -(defcustom proof-shell-clear-goals-regexp 1907,73214 -(defcustom proof-shell-start-goals-regexp 1914,73507 -(defcustom proof-shell-end-goals-regexp 1922,73874 -(defcustom proof-shell-eager-annotation-start 1928,74116 -(defcustom proof-shell-eager-annotation-start-length 1946,74854 -(defcustom proof-shell-eager-annotation-end 1957,75281 -(defcustom proof-shell-assumption-regexp 1973,75957 -(defcustom proof-shell-process-file 1983,76372 -(defcustom proof-shell-retract-files-regexp 2005,77324 -(defcustom proof-shell-compute-new-files-list 2014,77660 -(defcustom pg-use-specials-for-fontify 2026,78205 -(defcustom pg-special-char-regexp 2034,78553 -(defcustom proof-shell-set-elisp-variable-regexp 2040,78698 -(defcustom proof-shell-match-pgip-cmd 2073,80212 -(defcustom proof-shell-issue-pgip-cmd 2082,80542 -(defcustom proof-shell-query-dependencies-cmd 2091,80898 -(defcustom proof-shell-theorem-dependency-list-regexp 2098,81158 -(defcustom proof-shell-theorem-dependency-list-split 2114,81818 -(defcustom proof-shell-show-dependency-cmd 2123,82243 -(defcustom proof-shell-identifier-under-mouse-cmd 2130,82512 -(defcustom proof-shell-trace-output-regexp 2153,83593 -(defcustom proof-shell-thms-output-regexp 2169,84137 -(defcustom proof-shell-unicode 2182,84523 -(defcustom proof-shell-filename-escapes 2190,84851 -(defcustom proof-shell-process-connection-type 2207,85531 -(defcustom proof-shell-strip-crs-from-input 2230,86578 -(defcustom proof-shell-strip-crs-from-output 2242,87067 -(defcustom proof-shell-insert-hook 2250,87435 -(defcustom proof-pre-shell-start-hook 2290,89399 -(defcustom proof-shell-handle-delayed-output-hook2306,89871 -(defcustom proof-shell-handle-error-or-interrupt-hook2312,90086 -(defcustom proof-shell-pre-interrupt-hook2330,90835 -(defcustom proof-shell-process-output-system-specific 2338,91107 -(defcustom proof-state-change-hook 2357,91972 -(defcustom proof-shell-font-lock-keywords 2368,92354 -(defcustom proof-shell-syntax-table-entries 2376,92682 -(defgroup proof-goals 2394,93054 -(defcustom pg-subterm-first-special-char 2399,93175 -(defcustom pg-subterm-anns-use-stack 2407,93487 -(defcustom pg-goals-change-goal 2416,93791 -(defcustom pbp-goal-command 2421,93906 -(defcustom pbp-hyp-command 2426,94062 -(defcustom pg-subterm-help-cmd 2431,94224 -(defcustom pg-goals-error-regexp 2438,94460 -(defcustom proof-shell-result-start 2443,94620 -(defcustom proof-shell-result-end 2449,94854 -(defcustom pg-subterm-start-char 2455,95067 -(defcustom pg-subterm-sep-char 2469,95649 -(defcustom pg-subterm-end-char 2475,95828 -(defcustom pg-topterm-regexp 2481,95985 -(defcustom proof-goals-font-lock-keywords 2498,96588 -(defcustom proof-resp-font-lock-keywords 2512,97267 -(defcustom pg-before-fontify-output-hook 2524,97845 -(defcustom pg-after-fontify-output-hook 2532,98205 -(defgroup proof-x-symbol 2544,98459 -(defcustom proof-xsym-extra-modes 2549,98587 -(defcustom proof-xsym-font-lock-keywords 2562,99216 -(defcustom proof-xsym-activate-command 2570,99593 -(defcustom proof-xsym-deactivate-command 2577,99829 -(defpgcustom favourites 2594,100296 -(defpgcustom menu-entries 2599,100486 -(defpgcustom help-menu-entries 2606,100723 -(defpgcustom keymap 2613,100986 -(defpgcustom completion-table 2618,101157 -(defpgcustom tags-program 2628,101522 -(defcustom proof-general-name 2640,101695 -(defcustom proof-general-home-page2645,101852 -(defcustom proof-unnamed-theorem-name2651,102011 -(defcustom proof-universal-keys2657,102195 +(defalias (quote proof-x-symbol-decode-region)452,14953 + +generic/proof-config.el,10171 +(defgroup proof-user-options 88,3165 +(defcustom proof-electric-terminator-enable 93,3279 +(defcustom proof-toolbar-enable 105,3811 +(defcustom proof-imenu-enable 111,3984 +(defcustom pg-show-hints 117,4155 +(defcustom proof-output-fontify-enable 122,4290 +(defcustom proof-trace-output-slow-catchup 132,4673 +(defcustom proof-strict-state-preserving 142,5170 +(defcustom proof-strict-read-only 155,5779 +(defcustom proof-three-window-enable 165,6129 +(defcustom proof-multiple-frames-enable 184,6879 +(defcustom proof-delete-empty-windows 193,7212 +(defcustom proof-shrink-windows-tofit 204,7743 +(defcustom proof-toolbar-use-button-enablers211,8015 +(defcustom proof-query-file-save-when-activating-scripting234,8883 +(defcustom proof-one-command-per-line253,9656 +(defcustom proof-prog-name-ask261,9875 +(defcustom proof-prog-name-guess267,10035 +(defcustom proof-tidy-response275,10294 +(defcustom proof-keep-response-history289,10757 +(defcustom proof-general-debug 299,11145 +(defcustom proof-experimental-features308,11516 +(defcustom proof-follow-mode 326,12275 +(defcustom proof-auto-action-when-deactivating-scripting 350,13455 +(defcustom proof-script-command-separator 373,14404 +(defcustom proof-rsh-command 381,14696 +(defcustom proof-disappearing-proofs 397,15246 +(defgroup proof-faces 424,15892 +(defface proof-queue-face429,15998 +(defface proof-locked-face437,16276 +(defface proof-declaration-name-face450,16779 +(defface proof-tacticals-name-face459,17065 +(defface proof-tactics-name-face468,17327 +(defface proof-error-face477,17592 +(defface proof-warning-face485,17798 +(defface proof-eager-annotation-face494,18055 +(defface proof-debug-message-face502,18273 +(defface proof-boring-face510,18472 +(defface proof-mouse-highlight-face518,18664 +(defface proof-highlight-dependent-face526,18860 +(defface proof-highlight-dependency-face534,19069 +(defface proof-active-area-face542,19266 +(defgroup prover-config 559,19541 +(defcustom proof-guess-command-line 601,20852 +(defcustom proof-assistant-home-page 616,21347 +(defcustom proof-context-command 622,21517 +(defcustom proof-info-command 627,21651 +(defcustom proof-showproof-command 634,21922 +(defcustom proof-goal-command 639,22058 +(defcustom proof-save-command 647,22355 +(defcustom proof-find-theorems-command 655,22664 +(defconst proof-toolbar-entries-default662,22974 +(defcustom proof-assistant-true-value 696,24887 +(defcustom proof-assistant-false-value 702,25077 +(defcustom proof-assistant-format-int-fn 708,25271 +(defcustom proof-assistant-format-string-fn 715,25520 +(defcustom proof-assistant-setting-format 722,25787 +(defgroup proof-script 744,26482 +(defcustom proof-terminal-char 749,26612 +(defcustom proof-script-sexp-commands 759,26999 +(defcustom proof-script-command-end-regexp 770,27456 +(defcustom proof-script-command-start-regexp 788,28275 +(defcustom proof-script-use-old-parser 799,28736 +(defcustom proof-script-integral-proofs 811,29222 +(defcustom proof-script-fly-past-comments 826,29878 +(defcustom proof-script-parse-function 831,30049 +(defcustom proof-script-comment-start 849,30692 +(defcustom proof-script-comment-start-regexp 860,31129 +(defcustom proof-script-comment-end 868,31446 +(defcustom proof-script-comment-end-regexp 880,31868 +(defcustom pg-insert-output-as-comment-fn 888,32179 +(defcustom proof-string-start-regexp 894,32431 +(defcustom proof-string-end-regexp 899,32596 +(defcustom proof-case-fold-search 904,32757 +(defcustom proof-save-command-regexp 913,33167 +(defcustom proof-save-with-hole-regexp 918,33277 +(defcustom proof-save-with-hole-result 930,33731 +(defcustom proof-goal-command-regexp 940,34182 +(defcustom proof-goal-with-hole-regexp 949,34570 +(defcustom proof-goal-with-hole-result 961,35011 +(defcustom proof-non-undoables-regexp 970,35398 +(defcustom proof-nested-undo-regexp 981,35853 +(defcustom proof-ignore-for-undo-count 997,36565 +(defcustom proof-script-next-entity-regexps 1005,36868 +(defcustom proof-script-find-next-entity-fn1049,38603 +(defcustom proof-script-imenu-generic-expression 1069,39441 +(defcustom proof-goal-command-p 1087,40294 +(defcustom proof-really-save-command-p 1114,41731 +(defcustom proof-completed-proof-behaviour 1126,42193 +(defcustom proof-count-undos-fn 1154,43549 +(defconst proof-no-command 1166,44098 +(defcustom proof-find-and-forget-fn 1171,44303 +(defcustom proof-forget-id-command 1188,45015 +(defcustom pg-topterm-goalhyplit-fn 1198,45373 +(defcustom proof-kill-goal-command 1210,45908 +(defcustom proof-undo-n-times-cmd 1224,46409 +(defcustom proof-nested-goals-history-p 1238,46957 +(defcustom proof-state-preserving-p 1247,47294 +(defcustom proof-activate-scripting-hook 1257,47764 +(defcustom proof-deactivate-scripting-hook 1276,48543 +(defcustom proof-indent 1289,48908 +(defcustom proof-indent-hang 1294,49015 +(defcustom proof-indent-enclose-offset 1299,49141 +(defcustom proof-indent-open-offset 1304,49283 +(defcustom proof-indent-close-offset 1309,49420 +(defcustom proof-indent-any-regexp 1314,49558 +(defcustom proof-indent-inner-regexp 1319,49718 +(defcustom proof-indent-enclose-regexp 1324,49872 +(defcustom proof-indent-open-regexp 1329,50026 +(defcustom proof-indent-close-regexp 1334,50178 +(defcustom proof-script-font-lock-keywords 1340,50332 +(defcustom proof-script-syntax-table-entries 1348,50661 +(defcustom proof-script-span-context-menu-extensions 1366,51058 +(defgroup proof-shell 1392,51818 +(defcustom proof-prog-name 1402,51989 +(defcustom proof-shell-auto-terminate-commands 1413,52407 +(defcustom proof-shell-pre-sync-init-cmd 1422,52804 +(defcustom proof-shell-init-cmd 1436,53362 +(defcustom proof-shell-restart-cmd 1447,53831 +(defcustom proof-shell-quit-cmd 1452,53986 +(defcustom proof-shell-quit-timeout 1457,54153 +(defcustom proof-shell-cd-cmd 1467,54601 +(defcustom proof-shell-start-silent-cmd 1484,55266 +(defcustom proof-shell-stop-silent-cmd 1493,55640 +(defcustom proof-shell-silent-threshold 1502,55973 +(defcustom proof-shell-inform-file-processed-cmd 1510,56307 +(defcustom proof-shell-inform-file-retracted-cmd 1531,57229 +(defcustom proof-auto-multiple-files 1559,58495 +(defcustom proof-cannot-reopen-processed-files 1574,59216 +(defcustom proof-shell-require-command-regexp 1588,59882 +(defcustom proof-done-advancing-require-function 1599,60344 +(defcustom proof-shell-quiet-errors 1605,60579 +(defcustom proof-shell-prompt-pattern 1618,60913 +(defcustom proof-shell-wakeup-char 1628,61334 +(defcustom proof-shell-annotated-prompt-regexp 1634,61565 +(defcustom proof-shell-abort-goal-regexp 1650,62199 +(defcustom proof-shell-error-regexp 1655,62334 +(defcustom proof-shell-truncate-before-error 1675,63128 +(defcustom pg-next-error-regexp 1689,63671 +(defcustom pg-next-error-filename-regexp 1704,64280 +(defcustom pg-next-error-extract-filename 1728,65313 +(defcustom proof-shell-interrupt-regexp 1735,65556 +(defcustom proof-shell-proof-completed-regexp 1749,66147 +(defcustom proof-shell-clear-response-regexp 1762,66655 +(defcustom proof-shell-clear-goals-regexp 1769,66954 +(defcustom proof-shell-start-goals-regexp 1776,67247 +(defcustom proof-shell-end-goals-regexp 1784,67614 +(defcustom proof-shell-eager-annotation-start 1790,67856 +(defcustom proof-shell-eager-annotation-start-length 1808,68591 +(defcustom proof-shell-eager-annotation-end 1819,69017 +(defcustom proof-shell-assumption-regexp 1835,69692 +(defcustom proof-shell-process-file 1845,70095 +(defcustom proof-shell-retract-files-regexp 1867,71051 +(defcustom proof-shell-compute-new-files-list 1876,71387 +(defcustom pg-use-specials-for-fontify 1888,71935 +(defcustom pg-special-char-regexp 1896,72283 +(defcustom proof-shell-set-elisp-variable-regexp 1902,72428 +(defcustom proof-shell-match-pgip-cmd 1935,73939 +(defcustom proof-shell-issue-pgip-cmd 1944,74268 +(defcustom proof-shell-query-dependencies-cmd 1953,74624 +(defcustom proof-shell-theorem-dependency-list-regexp 1960,74884 +(defcustom proof-shell-theorem-dependency-list-split 1976,75544 +(defcustom proof-shell-show-dependency-cmd 1985,75967 +(defcustom proof-shell-identifier-under-mouse-cmd 1992,76236 +(defcustom proof-shell-trace-output-regexp 2015,77317 +(defcustom proof-shell-thms-output-regexp 2029,77775 +(defcustom proof-shell-unicode 2042,78161 +(defcustom proof-shell-filename-escapes 2050,78481 +(defcustom proof-shell-process-connection-type2067,79161 +(defcustom proof-shell-strip-crs-from-input 2090,80207 +(defcustom proof-shell-strip-crs-from-output 2102,80692 +(defcustom proof-shell-insert-hook 2110,81060 +(defcustom proof-shell-handle-delayed-output-hook2150,83017 +(defcustom proof-shell-handle-error-or-interrupt-hook2156,83232 +(defcustom proof-shell-pre-interrupt-hook2174,83981 +(defcustom proof-shell-process-output-system-specific 2182,84253 +(defcustom proof-state-change-hook 2201,85117 +(defcustom proof-shell-font-lock-keywords 2212,85499 +(defcustom proof-shell-syntax-table-entries 2220,85831 +(defgroup proof-goals 2238,86203 +(defcustom pg-subterm-first-special-char 2243,86324 +(defcustom pg-subterm-anns-use-stack 2251,86636 +(defcustom pg-goals-change-goal 2260,86935 +(defcustom pbp-goal-command 2265,87051 +(defcustom pbp-hyp-command 2270,87207 +(defcustom pg-subterm-help-cmd 2275,87369 +(defcustom pg-goals-error-regexp 2282,87605 +(defcustom proof-shell-result-start 2287,87765 +(defcustom proof-shell-result-end 2293,87999 +(defcustom pg-subterm-start-char 2299,88212 +(defcustom pg-subterm-sep-char 2313,88792 +(defcustom pg-subterm-end-char 2319,88971 +(defcustom pg-topterm-regexp 2325,89128 +(defcustom proof-goals-font-lock-keywords 2342,89730 +(defcustom proof-resp-font-lock-keywords 2356,90415 +(defcustom pg-before-fontify-output-hook 2368,90995 +(defcustom pg-after-fontify-output-hook 2376,91355 +(defgroup proof-x-symbol 2388,91635 +(defcustom proof-xsym-extra-modes 2393,91763 +(defcustom proof-xsym-font-lock-keywords 2406,92391 +(defcustom proof-xsym-activate-command 2414,92768 +(defcustom proof-xsym-deactivate-command 2421,93003 +(defcustom proof-general-name 2438,93288 +(defcustom proof-general-home-page2443,93445 +(defcustom proof-unnamed-theorem-name2449,93605 +(defcustom proof-universal-keys2455,93789 generic/proof-depends.el,824 (defvar proof-thm-names-of-files 19,540 @@ -1638,520 +1681,505 @@ generic/proof-depends.el,824 (defun proof-depends-module-of 44,1570 (defun proof-depends-names-in-same-file 52,1864 (defun proof-depends-process-dependencies 71,2484 -(defun proof-dependency-in-span-context-menu 124,4226 -(defun proof-dep-alldeps-menu 147,5129 -(defun proof-dep-make-alldeps-menu 153,5356 -(defun proof-dep-split-deps 171,5852 -(defun proof-dep-make-submenu 192,6551 -(defun proof-make-highlight-depts-menu 202,6904 -(defun proof-goto-dependency 212,7208 -(defun proof-show-dependency 218,7431 -(defconst pg-dep-span-priority 225,7721 -(defconst pg-ordinary-span-priority 226,7757 -(defun proof-highlight-depcs 228,7799 -(defun proof-highlight-depts 238,8229 -(defun proof-dep-unhighlight 249,8703 +(defun proof-dependency-in-span-context-menu 124,4231 +(defun proof-dep-alldeps-menu 147,5134 +(defun proof-dep-make-alldeps-menu 153,5361 +(defun proof-dep-split-deps 171,5857 +(defun proof-dep-make-submenu 192,6556 +(defun proof-make-highlight-depts-menu 202,6909 +(defun proof-goto-dependency 212,7213 +(defun proof-show-dependency 218,7436 +(defconst pg-dep-span-priority 225,7726 +(defconst pg-ordinary-span-priority 226,7762 +(defun proof-highlight-depcs 228,7804 +(defun proof-highlight-depts 238,8234 +(defun proof-dep-unhighlight 249,8708 generic/proof-easy-config.el,192 -(defconst proof-easy-config-derived-modes-table15,492 -(defun proof-easy-config-define-derived-modes 22,898 -(defun proof-easy-config-check-setup 59,2510 -(defmacro proof-easy-config 91,3835 - -generic/proof.el,543 -(deflocal proof-buffer-type 35,900 -(defvar proof-shell-busy 38,1013 -(defvar proof-included-files-list 43,1169 -(defvar proof-script-buffer 66,2185 -(defvar proof-previous-script-buffer 70,2325 -(defvar proof-shell-buffer 75,2579 -(defvar proof-goals-buffer 78,2665 -(defvar proof-response-buffer 81,2720 -(defvar proof-trace-buffer 84,2781 -(defvar proof-thms-buffer 88,2935 -(defvar proof-shell-error-or-interrupt-seen 92,3090 -(defvar proof-shell-proof-completed 97,3315 -(defvar proof-terminal-string 109,3860 -(defun unload-pg 123,4064 - -generic/proof-indent.el,219 -(defun proof-indent-indent 13,353 -(defun proof-indent-offset 22,619 -(defun proof-indent-inner-p 39,1219 -(defun proof-indent-goto-prev 48,1526 -(defun proof-indent-calculate 55,1859 -(defun proof-indent-line 74,2575 +(defconst proof-easy-config-derived-modes-table14,475 +(defun proof-easy-config-define-derived-modes 21,881 +(defun proof-easy-config-check-setup 54,2291 +(defmacro proof-easy-config 86,3616 + +generic/proof.el,516 +(deflocal proof-buffer-type 35,973 +(defvar proof-shell-busy 38,1086 +(defvar proof-included-files-list 43,1242 +(defvar proof-script-buffer 66,2256 +(defvar proof-previous-script-buffer 70,2396 +(defvar proof-shell-buffer 75,2650 +(defvar proof-goals-buffer 78,2736 +(defvar proof-response-buffer 81,2791 +(defvar proof-trace-buffer 84,2852 +(defvar proof-thms-buffer 88,3006 +(defvar proof-shell-error-or-interrupt-seen 92,3161 +(defvar proof-shell-proof-completed 97,3385 +(defvar proof-terminal-string 109,3930 + +generic/proof-indent.el,218 +(defun proof-indent-indent 9,226 +(defun proof-indent-offset 18,492 +(defun proof-indent-inner-p 35,1092 +(defun proof-indent-goto-prev 44,1399 +(defun proof-indent-calculate 51,1732 +(defun proof-indent-line 70,2448 generic/proof-maths-menu.el,134 -(defun proof-maths-menu-support-available 24,782 -(defun proof-maths-menu-set-global 37,1275 -(defun proof-maths-menu-enable 51,1731 - -generic/proof-menu.el,2787 -(defvar proof-display-some-buffers-count 21,543 -(defun proof-display-some-buffers 23,588 -(defun proof-menu-define-keys 82,2790 -(define-key map 85,2938 -(define-key map 86,2990 -(define-key map 87,3041 -(define-key map 88,3094 -(define-key map 89,3148 -(define-key map 90,3210 -(define-key map 91,3270 -(define-key map 92,3332 -(define-key map 95,3505 -(define-key map 99,3742 -(define-key map 100,3796 -(define-key map 101,3861 -(define-key map 102,3935 -(define-key map 105,4116 -(define-key map 106,4182 -(define-key map 109,4388 -(define-key map 110,4454 -(define-key map 112,4569 -(define-key map 113,4632 -(define-key map 115,4717 -(define-key map 122,5043 -(define-key map 123,5102 -(defun proof-menu-define-main 143,5692 -(defun proof-menu-define-specific 153,5893 -(defun proof-assistant-menu-update 188,6911 -(defvar proof-help-menu205,7519 -(defvar proof-show-hide-menu213,7797 -(defvar proof-buffer-menu222,8110 -(defun proof-keep-response-history 277,10207 -(defconst proof-quick-opts-menu285,10517 -(defun proof-quick-opts-vars 412,15579 -(defun proof-quick-opts-changed-from-defaults-p 437,16330 -(defun proof-quick-opts-changed-from-saved-p 441,16435 -(defun proof-quick-opts-save 452,16787 -(defun proof-quick-opts-reset 457,16955 -(defconst proof-config-menu469,17223 -(defconst proof-advanced-menu476,17402 -(defvar proof-menu 489,17837 -(defvar proof-main-menu498,18121 -(defvar proof-aux-menu508,18347 -(defvar proof-menu-favourites 524,18669 -(defun proof-menu-define-favourites-menu 527,18776 -(defmacro proof-defshortcut 548,19447 -(defmacro proof-definvisible 564,20102 -(defun proof-def-favourite 585,20927 -(defvar proof-make-favourite-cmd-history 608,21902 -(defvar proof-make-favourite-menu-history 611,21987 -(defun proof-save-favourites 614,22073 -(defun proof-del-favourite 619,22221 -(defun proof-read-favourite 636,22782 -(defun proof-add-favourite 661,23585 -(defvar proof-assistant-settings 688,24636 -(defvar proof-menu-settings 695,24999 -(defun proof-menu-define-settings-menu 698,25073 -(defun proof-menu-entry-name 718,25817 -(defun proof-menu-entry-for-setting 730,26289 -(defun proof-settings-vars 748,26779 -(defun proof-settings-changed-from-defaults-p 753,26956 -(defun proof-settings-changed-from-saved-p 757,27062 -(defun proof-settings-save 761,27165 -(defun proof-settings-reset 766,27332 -(defun proof-defpacustom-fn 774,27578 -(defmacro defpacustom 850,30462 -(defun proof-assistant-invisible-command-ifposs 861,31103 -(defun proof-maybe-askprefs 883,32078 -(defun proof-assistant-settings-cmd 890,32282 -(defun proof-assistant-format 907,32942 -(defvar proof-assistant-format-table 931,34001 -(defun proof-assistant-format-bool 939,34370 -(defun proof-assistant-format-int 942,34483 -(defun proof-assistant-format-string 945,34575 +(defun proof-maths-menu-support-available 25,858 +(defun proof-maths-menu-set-global 36,1287 +(defun proof-maths-menu-enable 50,1743 + +generic/proof-menu.el,2146 +(defvar proof-display-some-buffers-count 21,508 +(defun proof-display-some-buffers 23,553 +(defun proof-menu-define-keys 82,2755 +(defun proof-menu-define-main 144,5730 +(defun proof-menu-define-specific 154,5933 +(defun proof-assistant-menu-update 192,6959 +(defvar proof-help-menu208,7542 +(defvar proof-show-hide-menu216,7820 +(defvar proof-buffer-menu225,8133 +(defun proof-keep-response-history 280,10230 +(defconst proof-quick-opts-menu288,10540 +(defun proof-quick-opts-vars 415,15605 +(defun proof-quick-opts-changed-from-defaults-p 440,16356 +(defun proof-quick-opts-changed-from-saved-p 444,16461 +(defun proof-quick-opts-save 455,16813 +(defun proof-quick-opts-reset 460,16981 +(defconst proof-config-menu472,17249 +(defconst proof-advanced-menu479,17428 +(defvar proof-menu 492,17863 +(defun proof-main-menu 501,18147 +(defun proof-aux-menu 512,18413 +(defvar proof-menu-favourites 529,18791 +(defun proof-menu-define-favourites-menu 532,18898 +(defun proof-def-favourite 552,19554 +(defvar proof-make-favourite-cmd-history 575,20529 +(defvar proof-make-favourite-menu-history 578,20614 +(defun proof-save-favourites 581,20700 +(defun proof-del-favourite 586,20848 +(defun proof-read-favourite 603,21409 +(defun proof-add-favourite 628,22212 +(defvar proof-assistant-settings 655,23263 +(defvar proof-menu-settings 662,23626 +(defun proof-menu-define-settings-menu 665,23700 +(defun proof-menu-entry-name 685,24444 +(defun proof-menu-entry-for-setting 697,24916 +(defun proof-settings-vars 715,25406 +(defun proof-settings-changed-from-defaults-p 720,25583 +(defun proof-settings-changed-from-saved-p 724,25689 +(defun proof-settings-save 728,25792 +(defun proof-settings-reset 733,25959 +(defun proof-defpacustom-fn 741,26205 +(defmacro defpacustom 817,29089 +(defun proof-assistant-invisible-command-ifposs 828,29730 +(defun proof-maybe-askprefs 850,30705 +(defun proof-assistant-settings-cmd 857,30909 +(defun proof-assistant-format 874,31569 +(defvar proof-assistant-format-table 898,32628 +(defun proof-assistant-format-bool 906,32997 +(defun proof-assistant-format-int 909,33110 +(defun proof-assistant-format-string 912,33202 generic/proof-mmm.el,113 -(defun proof-mmm-support-available 27,933 -(defun proof-mmm-set-global 53,1833 -(defun proof-mmm-enable 68,2374 - -generic/proof-script.el,5105 -(defvar proof-last-theorem-dependencies 41,1047 -(defvar proof-nesting-depth 45,1209 -(defvar proof-element-counters 52,1440 -(deflocal proof-active-buffer-fake-minor-mode 58,1580 -(deflocal proof-script-buffer-file-name 61,1706 -(defun proof-next-element-count 75,2230 -(defun proof-element-id 84,2557 -(defun proof-next-element-id 88,2726 -(deflocal proof-script-last-entity 102,3042 -(defun proof-script-find-next-entity 109,3322 -(deflocal proof-locked-span 185,6064 -(deflocal proof-queue-span 192,6330 -(defun proof-span-read-only 204,6844 -(defun proof-strict-read-only 211,7101 -(defsubst proof-set-queue-endpoints 226,7771 -(defsubst proof-set-locked-endpoints 230,7912 -(defsubst proof-detach-queue 234,8056 -(defsubst proof-detach-locked 238,8188 -(defsubst proof-set-queue-start 242,8324 -(defsubst proof-set-locked-end 246,8450 -(defsubst proof-set-queue-end 261,9029 -(defun proof-init-segmentation 271,9285 -(defun proof-restart-buffers 303,10656 -(defun proof-script-buffers-with-spans 325,11578 -(defun proof-script-remove-all-spans-and-deactivate 335,11934 -(defun proof-script-clear-queue-spans 339,12122 -(defun proof-unprocessed-begin 357,12663 -(defun proof-script-end 365,12917 -(defun proof-queue-or-locked-end 374,13218 -(defun proof-locked-end 388,13881 -(defun proof-locked-region-full-p 404,14251 -(defun proof-locked-region-empty-p 412,14508 -(defun proof-only-whitespace-to-locked-region-p 416,14658 -(defun proof-in-locked-region-p 429,15294 -(defun proof-goto-end-of-locked 441,15557 -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 458,16316 -(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 469,16797 -(defun proof-end-of-locked-visible-p 483,17450 -(defun proof-goto-end-of-queue-or-locked-if-not-visible 492,17901 -(defvar pg-idioms 511,18551 -(defvar pg-visibility-specs 514,18647 -(deflocal pg-script-portions 519,18854 -(defun pg-clear-script-portions 522,18976 -(defun pg-add-script-element 536,19505 -(defun pg-remove-script-element 539,19581 -(defsubst pg-visname 547,19859 -(defun pg-add-element 551,20004 -(defun pg-open-invisible-span 585,21633 -(defun pg-remove-element 596,21996 -(defun pg-make-element-invisible 603,22266 -(defun pg-make-element-visible 609,22523 -(defun pg-toggle-element-visibility 614,22702 -(defun pg-redisplay-for-gnuemacs 622,23032 -(defun pg-show-all-portions 629,23303 -(defun pg-show-all-proofs 647,23974 -(defun pg-hide-all-proofs 652,24102 -(defun pg-add-proof-element 657,24233 -(defun pg-span-name 671,24853 -(defun pg-set-span-helphighlights 692,25560 -(defun proof-complete-buffer-atomic 717,26384 -(defun proof-register-possibly-new-processed-file 758,28299 -(defun proof-inform-prover-file-retracted 809,30427 -(defun proof-auto-retract-dependencies 828,31213 -(defun proof-unregister-buffer-file-name 882,33753 -(defun proof-protected-process-or-retract 928,35576 -(defun proof-deactivate-scripting-auto 955,36746 -(defun proof-deactivate-scripting 964,37104 -(defun proof-activate-scripting 1101,42509 -(defun proof-toggle-active-scripting 1229,48263 -(defun proof-done-advancing 1270,49624 -(defun proof-done-advancing-comment 1356,52991 -(defun proof-done-advancing-save 1375,53733 -(defun proof-make-goalsave 1468,57348 -(defun proof-get-name-from-goal 1483,58091 -(defun proof-done-advancing-autosave 1502,59117 -(defun proof-done-advancing-other 1567,61663 -(defun proof-segment-up-to-parser 1595,62622 -(defun proof-script-generic-parse-find-comment-end 1658,64698 -(defun proof-script-generic-parse-cmdend 1667,65114 -(defun proof-script-generic-parse-cmdstart 1692,66009 -(defun proof-script-generic-parse-sexp 1755,68717 -(defun proof-cmdstart-add-segment-for-cmd 1779,69653 -(defun proof-segment-up-to-cmdstart 1831,71852 -(defun proof-segment-up-to-cmdend 1892,74212 -(defun proof-semis-to-vanillas 1963,76859 -(defun proof-script-new-command-advance 2002,78185 -(defun proof-script-next-command-advance 2044,79926 -(defun proof-assert-until-point-interactive 2056,80367 -(defun proof-assert-until-point 2082,81489 -(defun proof-assert-next-command2135,83921 -(defun proof-goto-point 2183,86184 -(defun proof-insert-pbp-command 2200,86710 -(defun proof-done-retracting 2233,87823 -(defun proof-setup-retract-action 2260,88934 -(defun proof-last-goal-or-goalsave 2270,89417 -(defun proof-retract-target 2293,90257 -(defun proof-retract-until-point-interactive 2378,93898 -(defun proof-retract-until-point 2386,94283 -(define-derived-mode proof-mode 2431,96144 -(defun proof-script-set-visited-file-name 2480,98111 -(defun proof-script-set-buffer-hooks 2504,99113 -(defun proof-script-kill-buffer-fn 2514,99609 -(defun proof-config-done-related 2558,101431 -(defun proof-generic-goal-command-p 2630,103999 -(defun proof-generic-state-preserving-p 2635,104211 -(defun proof-generic-count-undos 2644,104728 -(defun proof-generic-find-and-forget 2673,105758 -(defconst proof-script-important-settings2724,107583 -(defun proof-config-done 2737,108120 -(defun proof-setup-parsing-mechanism 2834,111668 -(defun proof-setup-imenu 2878,113521 -(defun proof-setup-func-menu 2895,114126 - -generic/proof-shell.el,3390 -(defvar proof-shell-last-output 19,457 -(defvar proof-marker 63,1713 -(defvar proof-action-list 66,1810 -(defvar proof-shell-silent 74,1986 -(defvar proof-shell-last-prompt 88,2469 -(defvar proof-shell-last-output-kind 93,2699 -(defvar proof-shell-delayed-output 114,3521 -(defvar proof-shell-delayed-output-kind 117,3642 -(defcustom proof-shell-active-scripting-indicator126,3845 -(defun proof-shell-ready-prover 179,5321 -(defun proof-shell-live-buffer 193,5861 -(defun proof-shell-available-p 200,6096 -(defun proof-grab-lock 206,6319 -(defun proof-release-lock 223,7036 -(defcustom proof-shell-fiddle-frames 243,7592 -(deflocal proof-eagerly-raise 250,7833 -(defun proof-shell-set-text-representation 253,7939 -(defun proof-shell-start 266,8494 -(defvar proof-shell-kill-function-hooks 485,16486 -(defun proof-shell-kill-function 488,16584 -(defun proof-shell-clear-state 577,20387 -(defun proof-shell-exit 592,20830 -(defun proof-shell-bail-out 604,21275 -(defun proof-shell-restart 613,21752 -(defvar proof-shell-no-response-display 655,23136 -(defvar proof-shell-urgent-message-marker 658,23240 -(defvar proof-shell-urgent-message-scanner 661,23361 -(defun proof-shell-handle-output 665,23488 -(defun proof-shell-handle-delayed-output 730,26341 -(defvar proof-shell-no-error-display 765,27763 -(defun proof-shell-handle-error 771,27969 -(defun proof-shell-handle-interrupt 789,28805 -(defun proof-shell-error-or-interrupt-action 803,29427 -(defun proof-goals-pos 830,30632 -(defun proof-pbp-focus-on-first-goal 835,30837 -(defsubst proof-shell-string-match-safe 847,31372 -(defun proof-shell-process-output 852,31540 -(defvar proof-shell-insert-space-fudge 963,36180 -(defun proof-shell-insert 972,36489 -(defun proof-shell-command-queue-item 1046,39401 -(defun proof-shell-set-silent 1051,39558 -(defun proof-shell-start-silent-item 1057,39777 -(defun proof-shell-clear-silent 1063,39969 -(defun proof-shell-stop-silent-item 1069,40191 -(defun proof-shell-should-be-silent 1076,40463 -(defun proof-append-alist 1089,41019 -(defun proof-start-queue 1148,43256 -(defun proof-extend-queue 1159,43605 -(defun proof-shell-exec-loop 1170,43986 -(defun proof-shell-insert-loopback-cmd 1235,46574 -(defun proof-shell-message 1263,47900 -(defun proof-shell-process-urgent-message 1269,48116 -(defvar proof-shell-minibuffer-urgent-interactive-input-history 1481,57074 -(defun proof-shell-minibuffer-urgent-interactive-input 1483,57144 -(defun proof-shell-process-urgent-messages 1495,57514 -(defun proof-shell-filter 1568,60685 -(defun proof-shell-filter-process-output 1727,67274 -(defvar pg-last-tracing-output-time 1780,69328 -(defvar pg-tracing-slow-mode 1783,69434 -(defconst pg-slow-mode-duration 1786,69523 -(defconst pg-fast-tracing-mode-threshold 1789,69605 -(defvar pg-tracing-cleanup-timer 1792,69733 -(defun pg-tracing-tight-loop 1794,69772 -(defun pg-finish-tracing-display 1837,71490 -(defun proof-shell-dont-show-annotations 1850,71796 -(defun proof-shell-show-annotations 1866,72331 -(defun proof-shell-wait 1887,72828 -(defun proof-done-invisible 1907,73738 -(defun proof-shell-invisible-command 1950,75461 -(defun proof-shell-invisible-cmd-get-result 1983,76711 -(defun proof-shell-invisible-command-invisible-result 2000,77392 -(define-derived-mode proof-shell-mode 2020,77896 -(defconst proof-shell-important-settings2091,80567 -(defun proof-shell-config-done 2096,80667 - -generic/proof-site.el,719 -(defgroup proof-general 20,594 -(defgroup proof-general-internals 32,994 -(defun proof-home-directory-fn 43,1234 -(defcustom proof-home-directory54,1604 -(defcustom proof-images-directory63,1970 -(defcustom proof-info-directory69,2171 -(defcustom proof-assistant-table98,3420 -(defun proof-string-to-list 160,5417 -(defcustom proof-assistants 176,5908 -(defun proof-ready-for-assistant 212,7321 -(defconst proof-general-version 325,11540 -(defconst proof-general-short-version 328,11681 -(defconst proof-general-version-year 333,11841 -(defcustom proof-assistant-cusgrp 347,12309 -(defcustom proof-assistant-internals-cusgrp 355,12612 -(defcustom proof-assistant 363,12924 -(defcustom proof-assistant-symbol 371,13193 - -generic/proof-splash.el,727 -(defcustom proof-splash-enable 16,433 -(defcustom proof-splash-time 21,585 -(defcustom proof-splash-contents29,870 -(defconst proof-splash-startup-msg 58,1985 -(defconst proof-splash-welcome 67,2364 -(defun proof-get-image 85,2900 -(defvar proof-splash-timeout-conf 125,4263 -(defun proof-splash-centre-spaces 128,4376 -(defun proof-splash-remove-screen 156,5545 -(defun proof-splash-remove-buffer 176,6271 -(defvar proof-splash-seen 192,6935 -(defun proof-splash-display-screen 196,7052 -(defun proof-splash-message 271,10211 -(defun proof-splash-timeout-waiter 281,10574 -(defvar proof-splash-old-frame-title-format 298,11313 -(defun proof-splash-set-frame-titles 300,11363 -(defun proof-splash-unset-frame-titles 309,11679 - -generic/proof-syntax.el,972 -(defun proof-ids-to-regexp 16,445 -(defun proof-anchor-regexp 22,701 -(defconst proof-no-regexp26,803 -(defun proof-regexp-alt 31,898 -(defun proof-regexp-region 40,1184 -(defun proof-re-search-forward-region 49,1607 -(defun proof-search-forward 62,2102 -(defun proof-replace-regexp-in-string 68,2354 -(defun proof-re-search-forward 74,2608 -(defun proof-re-search-backward 80,2869 -(defun proof-string-match 86,3133 -(defun proof-string-match-safe 92,3365 -(defun proof-stringfn-match 96,3570 -(defun proof-looking-at 103,3830 -(defun proof-looking-at-safe 109,4020 -(defun proof-looking-at-syntactic-context 113,4160 -(defun proof-replace-string 125,4523 -(defun proof-replace-regexp 130,4724 -(defun proof-replace-regexp-nocasefold 135,4930 -(defvar proof-id 143,5209 -(defun proof-ids 149,5429 -(defun proof-zap-commas 162,5990 -(defun proof-format 180,6559 -(defun proof-format-filename 199,7198 -(defun proof-insert 248,8676 -(defun proof-splice-separator 284,9685 - -generic/proof-toolbar.el,2877 -(defun proof-toolbar-function 49,1595 -(defun proof-toolbar-icon 52,1692 -(defun proof-toolbar-enabler 55,1793 -(defun proof-toolbar-function-with-enabler 58,1901 -(defun proof-toolbar-make-icon 65,2074 -(defun proof-toolbar-make-toolbar-item 83,2674 -(defvar proof-toolbar 122,4055 -(deflocal proof-toolbar-itimer 126,4184 -(defun proof-toolbar-setup 130,4294 -(defun proof-toolbar-build 174,5861 -(defalias 'proof-toolbar-enable proof-toolbar-enable239,8074 -(defun proof-toolbar-setup-refresh 248,8313 -(defun proof-toolbar-disable-refresh 269,9083 -(deflocal proof-toolbar-refresh-flag 276,9405 -(defun proof-toolbar-refresh 282,9676 -(defvar proof-toolbar-enablers286,9821 -(defvar proof-toolbar-enablers-last-state292,9997 -(defun proof-toolbar-really-refresh 296,10088 -(defun proof-toolbar-undo-enable-p 349,11918 -(defalias 'proof-toolbar-undo proof-toolbar-undo354,12066 -(defun proof-toolbar-delete-enable-p 360,12185 -(defalias 'proof-toolbar-delete proof-toolbar-delete366,12359 -(defun proof-toolbar-lockedend-enable-p 373,12495 -(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend376,12545 -(defun proof-toolbar-next-enable-p 385,12633 -(defalias 'proof-toolbar-next proof-toolbar-next389,12740 -(defun proof-toolbar-goto-enable-p 396,12834 -(defalias 'proof-toolbar-goto proof-toolbar-goto399,12907 -(defun proof-toolbar-retract-enable-p 406,12983 -(defalias 'proof-toolbar-retract proof-toolbar-retract410,13094 -(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p417,13173 -(defalias 'proof-toolbar-use proof-toolbar-use418,13241 -(defun proof-toolbar-restart-enable-p 424,13319 -(defalias 'proof-toolbar-restart proof-toolbar-restart429,13480 -(defun proof-toolbar-goal-enable-p 435,13558 -(defalias 'proof-toolbar-goal proof-toolbar-goal442,13791 -(defun proof-toolbar-qed-enable-p 449,13863 -(defalias 'proof-toolbar-qed proof-toolbar-qed455,14015 -(defun proof-toolbar-state-enable-p 461,14087 -(defalias 'proof-toolbar-state proof-toolbar-state464,14158 -(defun proof-toolbar-context-enable-p 470,14227 -(defalias 'proof-toolbar-context proof-toolbar-context473,14300 -(defun proof-toolbar-info-enable-p 481,14460 -(defalias 'proof-toolbar-info proof-toolbar-info484,14504 -(defun proof-toolbar-command-enable-p 490,14573 -(defalias 'proof-toolbar-command proof-toolbar-command493,14644 -(defun proof-toolbar-help-enable-p 499,14724 -(defun proof-toolbar-help 502,14769 -(defun proof-toolbar-find-enable-p 510,14863 -(defalias 'proof-toolbar-find proof-toolbar-find513,14932 -(defun proof-toolbar-visibility-enable-p 519,15030 -(defalias 'proof-toolbar-visibility proof-toolbar-visibility522,15130 -(defun proof-toolbar-interrupt-enable-p 528,15218 -(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt531,15282 -(defun proof-toolbar-make-menu-item 540,15471 -(defconst proof-toolbar-scripting-menu562,16159 - -generic/proof-utils.el,2102 -(defmacro deflocal 19,531 -(defmacro proof-with-current-buffer-if-exists 26,769 -(defmacro proof-with-script-buffer 35,1146 -(defmacro proof-map-buffers 46,1533 -(defmacro proof-sym 51,1718 -(defun proof-try-require 56,1879 -(defmacro proof-face-specs 63,2073 -(defun proof-save-some-buffers 85,2728 -(defun proof-set-value 109,3419 -(defun proof-ass-symv 169,5596 -(defmacro proof-ass-sym 174,5783 -(defun proof-defpgcustom-fn 178,5922 -(defun undefpgcustom 203,7006 -(defmacro defpgcustom 209,7230 -(defmacro proof-ass 218,7647 -(defun proof-defpgdefault-fn 223,7823 -(defmacro defpgdefault 237,8282 -(defmacro defpgfun 248,8644 -(defun proof-file-truename 263,8938 -(defun proof-file-to-buffer 267,9121 -(defun proof-files-to-buffers 278,9450 -(defun proof-buffers-in-mode 285,9733 -(defun pg-save-from-death 299,10184 -(defun proof-define-keys 318,10802 -(deflocal proof-font-lock-keywords 347,11803 -(deflocal proof-font-lock-keywords-case-fold-search 353,12068 -(defun proof-font-lock-configure-defaults 356,12191 -(defun proof-font-lock-clear-font-lock-vars 404,14504 -(defun proof-font-lock-set-font-lock-vars 415,14877 -(defun proof-fontify-region 422,15090 -(defun pg-remove-specials 480,17318 -(defun pg-remove-specials-in-string 490,17657 -(defun proof-fontify-buffer 497,17844 -(defun proof-warn-if-unset 510,18085 -(defun proof-get-window-for-buffer 515,18303 -(defun proof-display-and-keep-buffer 566,20617 -(defun proof-clean-buffer 598,21926 -(defun proof-message 613,22547 -(defun proof-warning 618,22760 -(defun pg-internal-warning 624,23042 -(defun proof-debug 632,23361 -(defun proof-switch-to-buffer 647,24032 -(defun proof-resize-window-tofit 680,25724 -(defun proof-submit-bug-report 780,29736 -(defun proof-deftoggle-fn 816,31124 -(defmacro proof-deftoggle 831,31779 -(defun proof-defintset-fn 838,32153 -(defmacro proof-defintset 854,32861 -(defun proof-defstringset-fn 861,33238 -(defmacro proof-defstringset 874,33865 -(defun pg-custom-save-vars 888,34330 -(defun pg-custom-reset-vars 906,35056 -(defun proof-locate-executable 919,35393 -(defconst proof-extra-fls948,36574 - -generic/proof-x-symbol.el,653 -(defpgcustom x-symbol-language 52,2063 -(defvar proof-x-symbol-initialized 57,2285 -(defun proof-x-symbol-tokenlang-file 60,2380 -(defun proof-x-symbol-support-maybe-available 66,2562 -(defun proof-x-symbol-initialize 86,3312 -(defun proof-x-symbol-enable 177,6973 -(defun proof-x-symbol-refresh-output-buffers 207,8290 -(defun proof-x-symbol-mode-associated-buffers 222,9044 -(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region244,9748 -(defun proof-x-symbol-encode-shell-input 246,9814 -(defun proof-x-symbol-set-language 263,10405 -(defun proof-x-symbol-shell-config 268,10576 -(defun proof-x-symbol-config-output-buffer 316,12743 +(defun proof-mmm-support-available 30,995 +(defun proof-mmm-set-global 54,1843 +(defun proof-mmm-enable 69,2384 + +generic/proof-script.el,5103 +(defvar proof-last-theorem-dependencies 36,964 +(defvar proof-nesting-depth 40,1126 +(defvar proof-element-counters 47,1357 +(deflocal proof-active-buffer-fake-minor-mode 53,1497 +(deflocal proof-script-buffer-file-name 56,1623 +(defun proof-next-element-count 70,2147 +(defun proof-element-id 79,2474 +(defun proof-next-element-id 83,2643 +(deflocal proof-script-last-entity 97,2960 +(defun proof-script-find-next-entity 104,3240 +(deflocal proof-locked-span 180,5982 +(deflocal proof-queue-span 187,6248 +(defun proof-span-read-only 199,6762 +(defun proof-strict-read-only 206,7019 +(defsubst proof-set-queue-endpoints 221,7689 +(defsubst proof-set-locked-endpoints 225,7830 +(defsubst proof-detach-queue 229,7974 +(defsubst proof-detach-locked 233,8106 +(defsubst proof-set-queue-start 237,8242 +(defsubst proof-set-locked-end 241,8368 +(defsubst proof-set-queue-end 256,8947 +(defun proof-init-segmentation 266,9203 +(defun proof-restart-buffers 298,10574 +(defun proof-script-buffers-with-spans 320,11506 +(defun proof-script-remove-all-spans-and-deactivate 330,11862 +(defun proof-script-clear-queue-spans 334,12050 +(defun proof-unprocessed-begin 352,12596 +(defun proof-script-end 360,12850 +(defun proof-queue-or-locked-end 369,13151 +(defun proof-locked-end 383,13814 +(defun proof-locked-region-full-p 399,14184 +(defun proof-locked-region-empty-p 407,14441 +(defun proof-only-whitespace-to-locked-region-p 411,14591 +(defun proof-in-locked-region-p 424,15227 +(defun proof-goto-end-of-locked 436,15490 +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 453,16249 +(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 464,16730 +(defun proof-end-of-locked-visible-p 478,17383 +(defun proof-goto-end-of-queue-or-locked-if-not-visible 487,17834 +(defvar pg-idioms 506,18484 +(defvar pg-visibility-specs 509,18580 +(deflocal pg-script-portions 514,18787 +(defun pg-clear-script-portions 517,18909 +(defun pg-add-script-element 531,19438 +(defun pg-remove-script-element 534,19514 +(defsubst pg-visname 542,19792 +(defun pg-add-element 546,19937 +(defun pg-open-invisible-span 580,21566 +(defun pg-remove-element 591,21929 +(defun pg-make-element-invisible 598,22199 +(defun pg-make-element-visible 604,22456 +(defun pg-toggle-element-visibility 609,22635 +(defun pg-redisplay-for-gnuemacs 617,22965 +(defun pg-show-all-portions 624,23236 +(defun pg-show-all-proofs 642,23907 +(defun pg-hide-all-proofs 647,24035 +(defun pg-add-proof-element 652,24166 +(defun pg-span-name 666,24786 +(defun pg-set-span-helphighlights 687,25493 +(defun proof-complete-buffer-atomic 712,26317 +(defun proof-register-possibly-new-processed-file 753,28232 +(defun proof-inform-prover-file-retracted 804,30360 +(defun proof-auto-retract-dependencies 823,31146 +(defun proof-unregister-buffer-file-name 877,33686 +(defun proof-protected-process-or-retract 923,35509 +(defun proof-deactivate-scripting-auto 950,36679 +(defun proof-deactivate-scripting 959,37037 +(defun proof-activate-scripting 1096,42442 +(defun proof-toggle-active-scripting 1224,48196 +(defun proof-done-advancing 1265,49557 +(defun proof-done-advancing-comment 1351,52924 +(defun proof-done-advancing-save 1370,53666 +(defun proof-make-goalsave 1463,57281 +(defun proof-get-name-from-goal 1478,58024 +(defun proof-done-advancing-autosave 1497,59050 +(defun proof-done-advancing-other 1562,61596 +(defun proof-segment-up-to-parser 1590,62555 +(defun proof-script-generic-parse-find-comment-end 1653,64631 +(defun proof-script-generic-parse-cmdend 1662,65047 +(defun proof-script-generic-parse-cmdstart 1687,65942 +(defun proof-script-generic-parse-sexp 1750,68650 +(defun proof-cmdstart-add-segment-for-cmd 1774,69586 +(defun proof-segment-up-to-cmdstart 1826,71785 +(defun proof-segment-up-to-cmdend 1887,74145 +(defun proof-semis-to-vanillas 1958,76792 +(defun proof-script-new-command-advance 1997,78118 +(defun proof-script-next-command-advance 2039,79859 +(defun proof-assert-until-point-interactive 2051,80300 +(defun proof-assert-until-point 2077,81422 +(defun proof-assert-next-command2130,83854 +(defun proof-goto-point 2178,86117 +(defun proof-insert-pbp-command 2195,86643 +(defun proof-done-retracting 2228,87756 +(defun proof-setup-retract-action 2255,88877 +(defun proof-last-goal-or-goalsave 2265,89360 +(defun proof-retract-target 2288,90200 +(defun proof-retract-until-point-interactive 2373,93841 +(defun proof-retract-until-point 2381,94226 +(define-derived-mode proof-mode 2424,95975 +(defun proof-script-set-visited-file-name 2469,97736 +(defun proof-script-set-buffer-hooks 2493,98738 +(defun proof-script-kill-buffer-fn 2501,99156 +(defun proof-config-done-related 2545,100978 +(defun proof-generic-goal-command-p 2617,103546 +(defun proof-generic-state-preserving-p 2622,103758 +(defun proof-generic-count-undos 2631,104275 +(defun proof-generic-find-and-forget 2660,105305 +(defconst proof-script-important-settings2711,107130 +(defun proof-config-done 2726,107683 +(defun proof-setup-parsing-mechanism 2819,111086 +(defun proof-setup-imenu 2863,112939 +(defun proof-setup-func-menu 2880,113544 + +generic/proof-shell.el,3350 +(defvar proof-shell-last-output 27,613 +(defvar proof-marker 63,1714 +(defvar proof-action-list 66,1811 +(defvar proof-shell-silent 74,1987 +(defvar proof-shell-last-prompt 88,2470 +(defvar proof-shell-last-output-kind 93,2700 +(defvar proof-shell-delayed-output 114,3522 +(defvar proof-shell-delayed-output-kind 117,3643 +(defcustom proof-shell-active-scripting-indicator126,3846 +(defun proof-shell-ready-prover 179,5317 +(defun proof-shell-live-buffer 193,5857 +(defun proof-shell-available-p 200,6092 +(defun proof-grab-lock 206,6315 +(defun proof-release-lock 223,7027 +(defcustom proof-shell-fiddle-frames 243,7578 +(defun proof-shell-set-text-representation 250,7819 +(defun proof-shell-start 263,8374 +(defvar proof-shell-kill-function-hooks 472,15899 +(defun proof-shell-kill-function 475,15997 +(defun proof-shell-clear-state 564,19800 +(defun proof-shell-exit 579,20243 +(defun proof-shell-bail-out 591,20688 +(defun proof-shell-restart 600,21165 +(defvar proof-shell-no-response-display 642,22549 +(defvar proof-shell-urgent-message-marker 645,22653 +(defvar proof-shell-urgent-message-scanner 648,22774 +(defun proof-shell-handle-output 652,22901 +(defun proof-shell-handle-delayed-output 712,25542 +(defvar proof-shell-no-error-display 740,26585 +(defun proof-shell-handle-error 746,26789 +(defun proof-shell-handle-interrupt 764,27625 +(defun proof-shell-error-or-interrupt-action 778,28238 +(defun proof-goals-pos 803,29383 +(defun proof-pbp-focus-on-first-goal 808,29588 +(defsubst proof-shell-string-match-safe 820,30118 +(defun proof-shell-process-output 825,30286 +(defvar proof-shell-insert-space-fudge 936,34926 +(defun proof-shell-insert 946,35245 +(defun proof-shell-command-queue-item 1020,38157 +(defun proof-shell-set-silent 1025,38314 +(defun proof-shell-start-silent-item 1031,38533 +(defun proof-shell-clear-silent 1037,38725 +(defun proof-shell-stop-silent-item 1043,38947 +(defun proof-shell-should-be-silent 1050,39219 +(defun proof-append-alist 1063,39775 +(defun proof-start-queue 1122,42012 +(defun proof-extend-queue 1133,42361 +(defun proof-shell-exec-loop 1144,42742 +(defun proof-shell-insert-loopback-cmd 1209,45330 +(defun proof-shell-message 1237,46656 +(defun proof-shell-process-urgent-message 1243,46872 +(defvar proof-shell-minibuffer-urgent-interactive-input-history 1455,55812 +(defun proof-shell-minibuffer-urgent-interactive-input 1457,55882 +(defun proof-shell-process-urgent-messages 1469,56252 +(defun proof-shell-filter 1542,59423 +(defun proof-shell-filter-process-output 1701,66012 +(defvar pg-last-tracing-output-time 1754,68066 +(defvar pg-tracing-slow-mode 1757,68172 +(defconst pg-slow-mode-duration 1760,68261 +(defconst pg-fast-tracing-mode-threshold 1763,68343 +(defvar pg-tracing-cleanup-timer 1766,68471 +(defun pg-tracing-tight-loop 1768,68510 +(defun pg-finish-tracing-display 1811,70228 +(defun proof-shell-dont-show-annotations 1824,70534 +(defun proof-shell-show-annotations 1840,71069 +(defun proof-shell-wait 1861,71566 +(defun proof-done-invisible 1881,72476 +(defun proof-shell-invisible-command 1924,74199 +(defun proof-shell-invisible-cmd-get-result 1957,75449 +(defun proof-shell-invisible-command-invisible-result 1974,76130 +(define-derived-mode proof-shell-mode 1993,76560 +(defconst proof-shell-important-settings2063,79226 +(defun proof-shell-config-done 2069,79341 + +generic/proof-site.el,827 +(defconst proof-general-short-version 50,1694 +(defconst proof-general-version-year 56,1882 +(defgroup proof-general 63,2035 +(defgroup proof-general-internals 68,2143 +(defun proof-home-directory-fn 81,2531 +(defcustom proof-home-directory92,2902 +(defcustom proof-images-directory101,3269 +(defcustom proof-info-directory107,3471 +(defconst proof-assistant-table-default136,4685 +(defcustom proof-assistant-table164,5782 +(defcustom proof-assistants 199,6898 +(defvar proof-assistant-cusgrp 229,8076 +(defvar proof-assistant-internals-cusgrp 235,8338 +(defvar proof-assistant 241,8609 +(defvar proof-assistant-symbol 246,8831 +(defvar proof-ready-for-assistant-hook 255,9222 +(defvar proof-ready-for-assistant-flag 260,9422 +(defun proof-ready-for-assistant 266,9622 +(defmacro proof-eval-when-ready-for-assistant 324,12080 + +generic/proof-splash.el,726 +(defcustom proof-splash-enable 14,379 +(defcustom proof-splash-time 19,531 +(defcustom proof-splash-contents27,816 +(defconst proof-splash-startup-msg 53,1776 +(defconst proof-splash-welcome 62,2155 +(defun proof-get-image 81,2702 +(defvar proof-splash-timeout-conf 120,4053 +(defun proof-splash-centre-spaces 123,4166 +(defun proof-splash-remove-screen 151,5336 +(defun proof-splash-remove-buffer 171,6057 +(defvar proof-splash-seen 187,6721 +(defun proof-splash-display-screen 191,6838 +(defun proof-splash-message 266,9992 +(defun proof-splash-timeout-waiter 277,10388 +(defvar proof-splash-old-frame-title-format 293,11084 +(defun proof-splash-set-frame-titles 295,11134 +(defun proof-splash-unset-frame-titles 304,11450 + +generic/proof-syntax.el,981 +(defun proof-ids-to-regexp 15,421 +(defun proof-anchor-regexp 21,677 +(defconst proof-no-regexp25,779 +(defun proof-regexp-alt 30,874 +(defun proof-regexp-region 39,1160 +(defun proof-re-search-forward-region 48,1583 +(defun proof-search-forward 61,2078 +(defun proof-replace-regexp-in-string 67,2330 +(defun proof-re-search-forward 73,2584 +(defun proof-re-search-backward 79,2845 +(defun proof-string-match 85,3109 +(defun proof-string-match-safe 91,3341 +(defun proof-stringfn-match 95,3546 +(defun proof-looking-at 102,3806 +(defun proof-looking-at-safe 108,3996 +(defun proof-looking-at-syntactic-context 112,4136 +(defsubst proof-replace-string 124,4499 +(defsubst proof-replace-regexp 129,4703 +(defsubst proof-replace-regexp-nocasefold 134,4912 +(defvar proof-id 142,5194 +(defun proof-ids 148,5414 +(defun proof-zap-commas 161,5975 +(defun proof-format 179,6544 +(defun proof-format-filename 198,7183 +(defun proof-insert 247,8661 +(defun proof-splice-separator 283,9670 + +generic/proof-toolbar.el,2874 +(defun proof-toolbar-function 38,1281 +(defun proof-toolbar-icon 41,1378 +(defun proof-toolbar-enabler 44,1479 +(defun proof-toolbar-function-with-enabler 47,1587 +(defun proof-toolbar-make-icon 54,1760 +(defun proof-toolbar-make-toolbar-item 72,2360 +(defvar proof-toolbar 111,3736 +(deflocal proof-toolbar-itimer 115,3865 +(defun proof-toolbar-setup 119,3975 +(defun proof-toolbar-build 162,5518 +(defalias 'proof-toolbar-enable proof-toolbar-enable227,7728 +(defun proof-toolbar-setup-refresh 238,8032 +(defun proof-toolbar-disable-refresh 259,8802 +(deflocal proof-toolbar-refresh-flag 266,9124 +(defun proof-toolbar-refresh 272,9395 +(defvar proof-toolbar-enablers276,9540 +(defvar proof-toolbar-enablers-last-state282,9722 +(defun proof-toolbar-really-refresh 286,9813 +(defun proof-toolbar-undo-enable-p 339,11643 +(defalias 'proof-toolbar-undo proof-toolbar-undo344,11791 +(defun proof-toolbar-delete-enable-p 350,11910 +(defalias 'proof-toolbar-delete proof-toolbar-delete356,12084 +(defun proof-toolbar-lockedend-enable-p 363,12220 +(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend366,12270 +(defun proof-toolbar-next-enable-p 375,12358 +(defalias 'proof-toolbar-next proof-toolbar-next379,12465 +(defun proof-toolbar-goto-enable-p 386,12559 +(defalias 'proof-toolbar-goto proof-toolbar-goto389,12632 +(defun proof-toolbar-retract-enable-p 396,12708 +(defalias 'proof-toolbar-retract proof-toolbar-retract400,12819 +(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p407,12898 +(defalias 'proof-toolbar-use proof-toolbar-use408,12966 +(defun proof-toolbar-restart-enable-p 414,13044 +(defalias 'proof-toolbar-restart proof-toolbar-restart419,13205 +(defun proof-toolbar-goal-enable-p 425,13283 +(defalias 'proof-toolbar-goal proof-toolbar-goal432,13516 +(defun proof-toolbar-qed-enable-p 439,13588 +(defalias 'proof-toolbar-qed proof-toolbar-qed445,13740 +(defun proof-toolbar-state-enable-p 451,13812 +(defalias 'proof-toolbar-state proof-toolbar-state454,13883 +(defun proof-toolbar-context-enable-p 460,13952 +(defalias 'proof-toolbar-context proof-toolbar-context463,14025 +(defun proof-toolbar-info-enable-p 471,14185 +(defalias 'proof-toolbar-info proof-toolbar-info474,14229 +(defun proof-toolbar-command-enable-p 480,14298 +(defalias 'proof-toolbar-command proof-toolbar-command483,14369 +(defun proof-toolbar-help-enable-p 489,14449 +(defun proof-toolbar-help 492,14494 +(defun proof-toolbar-find-enable-p 500,14588 +(defalias 'proof-toolbar-find proof-toolbar-find503,14657 +(defun proof-toolbar-visibility-enable-p 509,14755 +(defalias 'proof-toolbar-visibility proof-toolbar-visibility512,14855 +(defun proof-toolbar-interrupt-enable-p 518,14943 +(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt521,15007 +(defun proof-toolbar-make-menu-item 530,15196 +(defun proof-toolbar-scripting-menu 553,15896 + +generic/proof-utils.el,2153 +(defmacro deflocal 26,852 +(defmacro proof-with-current-buffer-if-exists 33,1090 +(defmacro proof-with-script-buffer 42,1467 +(defmacro proof-map-buffers 53,1854 +(defmacro proof-sym 58,2039 +(defsubst proof-try-require 63,2200 +(defmacro proof-face-specs 70,2397 +(defun proof-save-some-buffers 92,3051 +(defun proof-set-value 116,3742 +(defsubst proof-ass-symv 176,5912 +(defmacro proof-ass-sym 183,6213 +(defmacro proof-ass 188,6423 +(defun proof-defpgcustom-fn 193,6587 +(defun undefpgcustom 214,7458 +(defmacro defpgcustom 220,7682 +(defun proof-defpgdefault-fn 231,8100 +(defmacro defpgdefault 245,8558 +(defmacro defpgfun 256,8920 +(defun proof-file-truename 271,9214 +(defun proof-file-to-buffer 275,9397 +(defun proof-files-to-buffers 286,9726 +(defun proof-buffers-in-mode 293,10009 +(defun pg-save-from-death 307,10459 +(defun proof-define-keys 326,11076 +(deflocal proof-font-lock-keywords 355,12075 +(deflocal proof-font-lock-keywords-case-fold-search 361,12340 +(defun proof-font-lock-configure-defaults 364,12463 +(defun proof-font-lock-clear-font-lock-vars 412,14768 +(defun proof-font-lock-set-font-lock-vars 423,15141 +(defun proof-fontify-region 430,15351 +(defun pg-remove-specials 488,17569 +(defun pg-remove-specials-in-string 498,17907 +(defun proof-fontify-buffer 505,18094 +(defun proof-warn-if-unset 518,18335 +(defun proof-get-window-for-buffer 523,18553 +(defun proof-display-and-keep-buffer 574,20861 +(defun proof-clean-buffer 606,22168 +(defun proof-message 621,22789 +(defun proof-warning 626,23002 +(defun pg-internal-warning 632,23284 +(defun proof-debug 640,23603 +(defun proof-switch-to-buffer 655,24274 +(defun proof-resize-window-tofit 688,25963 +(defun proof-submit-bug-report 788,29975 +(defun proof-deftoggle-fn 824,31354 +(defmacro proof-deftoggle 839,32007 +(defun proof-defintset-fn 846,32381 +(defmacro proof-defintset 862,33085 +(defun proof-defstringset-fn 869,33462 +(defmacro proof-defstringset 882,34088 +(defmacro proof-defshortcut 896,34545 +(defmacro proof-definvisible 911,35184 +(defun pg-custom-save-vars 939,36161 +(defun pg-custom-reset-vars 957,36884 +(defun proof-locate-executable 970,37221 + +generic/proof-x-symbol.el,612 +(defvar proof-x-symbol-initialized 52,2072 +(defun proof-x-symbol-tokenlang-file 55,2167 +(defun proof-x-symbol-support-maybe-available 61,2349 +(defun proof-x-symbol-initialize 81,3078 +(defun proof-x-symbol-enable 164,6345 +(defun proof-x-symbol-refresh-output-buffers 196,7771 +(defun proof-x-symbol-mode-associated-buffers 211,8516 +(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region233,9220 +(defun proof-x-symbol-encode-shell-input 235,9286 +(defun proof-x-symbol-set-language 252,9877 +(defun proof-x-symbol-shell-config 257,10048 +(defun proof-x-symbol-config-output-buffer 305,12215 + +generic/test-compile.el,21 +(defconst bar 8,139 + +generic/test-mac.el,21 +(defvar testme 3,26 + +generic/test-req2.el,48 +(define-derived-mode proof-response-mode 8,138 lib/bufhist.el,1099 (defun bufhist-ring-update 32,1226 @@ -2217,34 +2245,34 @@ lib/holes.el,2447 (defun holes-clear-hole-at 425,13013 (defun holes-map-holes 434,13272 (defun holes-mapcar-holes 442,13455 -(defun holes-clear-all-buffer-holes 448,13622 -(defun holes-next 459,13922 -(defun holes-next-after-active-hole 466,14173 -(defun holes-set-active-hole-next 474,14392 -(defun holes-replace-segment 496,14945 -(defun holes-replace 506,15299 -(defun holes-replace-active-hole 537,16494 -(defun holes-replace-update-active-hole 546,16795 -(defun holes-delete-update-active-hole 567,17485 -(defun holes-set-make-active-hole 574,17699 -(defun holes-mouse-replace-active-hole 621,19327 -(defun holes-destroy-hole 641,19866 -(defun holes-hole-at-event 658,20277 -(defun holes-mouse-destroy-hole 663,20390 -(defun holes-mouse-forget-hole 673,20630 -(defun holes-mouse-set-make-active-hole 689,20940 -(defun holes-mouse-set-active-hole 711,21501 -(defun holes-set-point-next-hole-destroy 723,21765 -(defvar hole-map739,22215 -(defvar holes-mode-map755,22835 -(defun holes-replace-string-by-holes-backward 792,24300 -(defun holes-skeleton-end-hook 810,25001 -(defconst holes-jump-doc 819,25410 -(defun holes-replace-string-by-holes-backward-jump 826,25617 -(defun holes-abbrev-complete 843,26248 -(defun holes-insert-and-expand 852,26555 -(defvar holes-mode 863,26987 -(defun holes-mode 869,27183 +(defun holes-clear-all-buffer-holes 448,13627 +(defun holes-next 459,13927 +(defun holes-next-after-active-hole 466,14178 +(defun holes-set-active-hole-next 474,14397 +(defun holes-replace-segment 496,14950 +(defun holes-replace 506,15304 +(defun holes-replace-active-hole 537,16499 +(defun holes-replace-update-active-hole 546,16800 +(defun holes-delete-update-active-hole 567,17490 +(defun holes-set-make-active-hole 574,17704 +(defun holes-mouse-replace-active-hole 621,19332 +(defun holes-destroy-hole 641,19871 +(defun holes-hole-at-event 658,20282 +(defun holes-mouse-destroy-hole 663,20395 +(defun holes-mouse-forget-hole 673,20635 +(defun holes-mouse-set-make-active-hole 689,20945 +(defun holes-mouse-set-active-hole 711,21506 +(defun holes-set-point-next-hole-destroy 723,21770 +(defvar hole-map739,22220 +(defvar holes-mode-map755,22840 +(defun holes-replace-string-by-holes-backward 792,24305 +(defun holes-skeleton-end-hook 810,25006 +(defconst holes-jump-doc 819,25444 +(defun holes-replace-string-by-holes-backward-jump 826,25651 +(defun holes-abbrev-complete 843,26282 +(defun holes-insert-and-expand 852,26589 +(defvar holes-mode 863,27021 +(defun holes-mode 869,27217 lib/local-vars-list.el,372 (defconst local-vars-list-doc 25,759 @@ -2263,78 +2291,77 @@ lib/maths-menu.el,153 (defvar maths-menu-mode-map312,11648 (define-minor-mode maths-menu-mode337,12521 -lib/proof-compat.el,1003 -(defvar proof-running-on-XEmacs 25,818 -(defvar proof-running-on-Emacs21 27,940 -(defvar proof-running-on-win32 31,1187 -(defun pg-custom-undeclare-variable 43,1621 -(defun pg-window-system 118,4103 -(defconst pg-defface-window-systems 127,4474 -(defun subst-char-in-string 151,5191 -(defun replace-regexp-in-string 165,5745 -(defconst menuvisiblep 227,8458 -(defun set-window-text-height 244,9077 -(defmacro save-selected-frame 270,10027 -(defun warn 309,11329 -(defun redraw-modeline 316,11584 -(defun replace-in-string 331,12151 -(defun proof-buffer-syntactic-context-emulate 380,13669 -(defvar read-shell-command-map413,14976 -(defun read-shell-command 431,15678 -(defun remassq 443,16159 -(defun remassoc 455,16548 -(defun frames-of-buffer 468,16993 -(defmacro with-selected-window 507,18255 -(defun pg-pop-to-buffer 550,19644 -(defun process-live-p 601,21496 -(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context618,21999 -(defun select-buffers-tab-buffers-by-mode 662,23347 - -lib/span.el,132 -(defsubst delete-spans 24,499 -(defsubst span-property-safe 28,653 -(defsubst set-span-start 32,792 -(defsubst set-span-end 36,924 - -lib/span-extent.el,968 -(defsubst make-span 12,367 -(defsubst detach-span 16,489 -(defsubst set-span-endpoints 20,576 -(defsubst set-span-property 24,709 +lib/pg-dev.el,75 +(defconst pg-dev-lisp-font-lock-keywords35,1049 +(defun unload-pg 69,1986 + +lib/proof-compat.el,795 +(defvar proof-running-on-win32 26,856 +(defconst pg-defface-window-systems 34,1235 +(defun pg-custom-undeclare-variable 56,2062 +(defun subst-char-in-string 118,3707 +(defun replace-regexp-in-string 133,4296 +(defconst menuvisiblep 195,7009 +(defun set-window-text-height 212,7622 +(defmacro save-selected-frame 238,8572 +(defun warn 277,9869 +(defun redraw-modeline 284,10124 +(defun proof-buffer-syntactic-context-emulate 301,10720 +(defvar read-shell-command-map334,12027 +(defun read-shell-command 352,12729 +(defun remassq 364,13210 +(defun remassoc 376,13599 +(defun frames-of-buffer 389,14044 +(defmacro with-selected-window 428,15306 +(defun pg-pop-to-buffer 471,16684 +(defun process-live-p 522,18517 +(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context539,19020 + +lib/span.el,137 +(defsubst span-delete-spans 22,471 +(defsubst span-property-safe 26,635 +(defsubst span-set-start 30,774 +(defsubst span-set-end 34,906 + +lib/span-extent.el,973 +(defsubst span-make 12,367 +(defsubst span-detach 16,489 +(defsubst span-set-endpoints 20,576 +(defsubst span-set-property 24,709 (defsubst span-read-only 28,836 (defsubst span-read-write 32,940 (defun span-give-warning 36,1047 (defun span-write-warning 40,1155 (defsubst span-property 45,1355 -(defsubst delete-span 49,1470 -(defsubst mapcar-spans 55,1641 -(defsubst span-at 59,1847 -(defsubst span-at-before 63,1964 -(defsubst span-start 68,2161 -(defsubst span-end 72,2290 -(defsubst prev-span 76,2413 -(defsubst next-span 80,2559 -(defsubst span-live-p 84,2701 -(defun span-raise 92,2973 -(defalias 'span-object span-object96,3072 -(defalias 'span-string span-string97,3111 -(defsubst make-detached-span 100,3197 -(defsubst span-buffer 105,3259 -(defsubst span-detached-p 110,3351 -(defsubst set-span-face 115,3463 -(defsubst fold-spans 119,3558 -(defsubst set-span-properties 123,3755 -(defsubst set-span-keymap 127,3863 -(defsubst span-at-event 132,4007 - -lib/span-overlay.el,1201 +(defsubst span-delete 49,1470 +(defsubst span-mapcar-spans 55,1641 +(defsubst span-at 59,1852 +(defsubst span-at-before 63,1969 +(defsubst span-start 68,2166 +(defsubst span-end 72,2295 +(defsubst prev-span 76,2418 +(defsubst next-span 80,2564 +(defsubst span-live-p 84,2706 +(defun span-raise 92,2978 +(defalias 'span-object span-object96,3077 +(defalias 'span-string span-string97,3116 +(defsubst make-detached-span 100,3202 +(defsubst span-buffer 105,3264 +(defsubst span-detached-p 110,3356 +(defsubst set-span-face 115,3468 +(defsubst fold-spans 119,3563 +(defsubst set-span-properties 123,3760 +(defsubst set-span-keymap 127,3868 +(defsubst span-at-event 132,4012 + +lib/span-overlay.el,1206 (defalias 'span-start span-start12,370 (defalias 'span-end span-end13,408 -(defalias 'set-span-property set-span-property14,442 +(defalias 'span-set-property span-set-property14,442 (defalias 'span-property span-property15,485 -(defalias 'make-span make-span16,524 -(defalias 'detach-span detach-span17,560 -(defalias 'set-span-endpoints set-span-endpoints18,600 +(defalias 'span-make span-make16,524 +(defalias 'span-detach span-detach17,560 +(defalias 'span-set-endpoints span-set-endpoints18,600 (defalias 'span-buffer span-buffer19,645 (defun span-read-only-hook 21,686 (defun span-read-only 25,818 @@ -2345,37 +2372,37 @@ lib/span-overlay.el,1201 (defun spans-at-point-prop 62,2388 (defun spans-at-region-prop 68,2553 (defun span-at 76,2797 -(defsubst delete-span 82,3011 -(defsubst mapcar-spans 89,3233 -(defun span-at-before 93,3437 -(defun prev-span 110,4163 -(defun next-span 116,4314 -(defsubst span-live-p 145,5539 -(defun span-raise 151,5705 -(defalias 'span-object span-object157,5948 -(defun span-string 159,5989 -(defun set-span-properties 165,6171 -(defun span-find-span 177,6426 -(defsubst span-at-event 184,6733 -(defun make-detached-span 189,6857 -(defun fold-spans 194,6953 -(defsubst span-detached-p 209,7487 -(defsubst set-span-face 213,7602 -(defun set-span-keymap 217,7699 +(defsubst span-delete 82,3011 +(defsubst span-mapcar-spans 89,3233 +(defun span-at-before 93,3442 +(defun prev-span 110,4168 +(defun next-span 116,4319 +(defsubst span-live-p 145,5544 +(defun span-raise 151,5710 +(defalias 'span-object span-object157,5953 +(defun span-string 159,5994 +(defun set-span-properties 165,6176 +(defun span-find-span 177,6431 +(defsubst span-at-event 184,6738 +(defun make-detached-span 189,6862 +(defun fold-spans 194,6958 +(defsubst span-detached-p 209,7492 +(defsubst set-span-face 213,7607 +(defun set-span-keymap 217,7704 lib/texi-docstring-magic.el,584 (defun texi-docstring-magic-find-face 85,2997 (defun texi-docstring-magic-splice-sep 90,3162 (defconst texi-docstring-magic-munge-table100,3467 -(defun texi-docstring-magic-untabify 190,7187 -(defun texi-docstring-magic-munge-docstring 200,7502 -(defun texi-docstring-magic-texi 239,8789 -(defun texi-docstring-magic-format-default 252,9229 -(defun texi-docstring-magic-texi-for 268,9864 -(defconst texi-docstring-magic-comment326,11824 -(defun texi-docstring-magic 332,11978 -(defun texi-docstring-magic-face-at-point 366,13058 -(defun texi-docstring-magic-insert-magic 381,13581 +(defun texi-docstring-magic-untabify 190,7234 +(defun texi-docstring-magic-munge-docstring 200,7549 +(defun texi-docstring-magic-texi 239,8836 +(defun texi-docstring-magic-format-default 252,9276 +(defun texi-docstring-magic-texi-for 268,9911 +(defconst texi-docstring-magic-comment326,11871 +(defun texi-docstring-magic 332,12025 +(defun texi-docstring-magic-face-at-point 366,13105 +(defun texi-docstring-magic-insert-magic 381,13628 lib/unichars.el,35 (defvar unicode-character-list1,0 @@ -3460,91 +3487,91 @@ doc/ProofGeneral.texi,5379 @node Top166,5052 @node Preface203,6168 @node Latest news for version 3.7Latest news for version 3.7226,6764 -@node Future264,8432 -@node Credits295,9731 -@node Introducing Proof GeneralIntroducing Proof General394,13165 -@node Installing Proof GeneralInstalling Proof General450,15197 -@node Quick start guideQuick start guide464,15645 -@node Features of Proof GeneralFeatures of Proof General508,17753 -@node Supported proof assistantsSupported proof assistants597,21678 -@node Prerequisites for this manualPrerequisites for this manual646,23584 -@node Organization of this manualOrganization of this manual690,25210 -@node Basic Script ManagementBasic Script Management716,26038 -@node Walkthrough example in IsabelleWalkthrough example in Isabelle735,26638 -@node Proof scriptsProof scripts986,36291 -@node Script buffersScript buffers1029,38411 -@node Locked queue and editing regionsLocked queue and editing regions1051,38988 -@node Goal-save sequencesGoal-save sequences1107,41135 -@node Active scripting bufferActive scripting buffer1144,42621 -@node Summary of Proof General buffersSummary of Proof General buffers1213,46041 -@node Script editing commandsScript editing commands1275,48715 -@node Script processing commandsScript processing commands1353,51573 -@node Proof assistant commandsProof assistant commands1481,56874 -@node Toolbar commandsToolbar commands1631,61878 -@node Interrupting during trace outputInterrupting during trace output1655,62807 -@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1694,64731 -@node Goals buffer commandsGoals buffer commands1708,65231 -@node Advanced Script ManagementAdvanced Script Management1797,68764 -@node Visibility of completed proofsVisibility of completed proofs1828,69918 -@node Switching between proof scriptsSwitching between proof scripts1883,71841 -@node View of processed files View of processed files 1920,73813 -@node Retracting across filesRetracting across files1980,76864 -@node Asserting across filesAsserting across files1993,77495 -@node Automatic multiple file handlingAutomatic multiple file handling2006,78061 -@node Escaping script managementEscaping script management2031,79095 -@node Experimental featuresExperimental features2089,81298 -@node Support for other PackagesSupport for other Packages2123,82561 -@node Syntax highlightingSyntax highlighting2155,83436 -@node X-Symbol supportX-Symbol support2194,85057 -@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2253,87603 -@node Support for outline modeSupport for outline mode2312,89733 -@node Support for completionSupport for completion2338,90863 -@node Support for tagsSupport for tags2395,93031 -@node Customizing Proof GeneralCustomizing Proof General2447,95360 -@node Basic optionsBasic options2487,97030 -@node How to customizeHow to customize2511,97788 -@node Display customizationDisplay customization2562,99890 -@node User optionsUser options2687,105124 -@node Changing facesChanging faces2951,114523 -@node Tweaking configuration settingsTweaking configuration settings3026,117192 -@node Hints and TipsHints and Tips3083,119718 -@node Adding your own keybindingsAdding your own keybindings3102,120319 -@node Using file variablesUsing file variables3158,122852 -@node Using abbreviationsUsing abbreviations3217,125038 -@node LEGO Proof GeneralLEGO Proof General3256,126454 -@node LEGO specific commandsLEGO specific commands3297,127823 -@node LEGO tagsLEGO tags3317,128278 -@node LEGO customizationsLEGO customizations3327,128525 -@node Coq Proof GeneralCoq Proof General3359,129444 -@node Coq-specific commandsCoq-specific commands3375,129853 -@node Coq-specific variablesCoq-specific variables3397,130360 -@node Editing multiple proofsEditing multiple proofs3419,131018 -@node User-loaded tacticsUser-loaded tactics3443,132126 -@node Holes featureHoles feature3507,134600 -@node Isabelle Proof GeneralIsabelle Proof General3534,135887 -@node Isabelle commandsIsabelle commands3564,137017 -@node Logics and SettingsLogics and Settings3671,140065 -@node Isabelle customizationsIsabelle customizations3705,141605 -@node HOL Proof GeneralHOL Proof General3729,142087 -@node Shell Proof GeneralShell Proof General3771,143909 -@node Obtaining and InstallingObtaining and Installing3807,145368 -@node Obtaining Proof GeneralObtaining Proof General3823,145781 -@node Installing Proof General from tarballInstalling Proof General from tarball3854,147020 -@node Installing Proof General from RPM packageInstalling Proof General from RPM package3879,147852 -@node Setting the names of binariesSetting the names of binaries3894,148260 -@node Notes for syssiesNotes for syssies3922,149200 -@node Bugs and EnhancementsBugs and Enhancements3995,152138 -@node References4016,152953 -@node History of Proof GeneralHistory of Proof General4056,153977 -@node Old News for 3.0Old News for 3.04147,158079 -@node Old News for 3.1Old News for 3.14217,161773 -@node Old News for 3.2Old News for 3.24243,162945 -@node Old News for 3.3Old News for 3.34304,165948 -@node Old News for 3.4Old News for 3.44323,166845 -@node Function IndexFunction Index4346,167901 -@node Variable IndexVariable Index4350,167977 -@node Keystroke IndexKeystroke Index4354,168057 -@node Concept IndexConcept Index4358,168123 +@node Future265,8408 +@node Credits296,9707 +@node Introducing Proof GeneralIntroducing Proof General395,13141 +@node Installing Proof GeneralInstalling Proof General451,15183 +@node Quick start guideQuick start guide465,15631 +@node Features of Proof GeneralFeatures of Proof General509,17739 +@node Supported proof assistantsSupported proof assistants598,21664 +@node Prerequisites for this manualPrerequisites for this manual647,23570 +@node Organization of this manualOrganization of this manual691,25196 +@node Basic Script ManagementBasic Script Management717,26024 +@node Walkthrough example in IsabelleWalkthrough example in Isabelle736,26624 +@node Proof scriptsProof scripts987,36277 +@node Script buffersScript buffers1030,38397 +@node Locked queue and editing regionsLocked queue and editing regions1052,38974 +@node Goal-save sequencesGoal-save sequences1108,41121 +@node Active scripting bufferActive scripting buffer1145,42607 +@node Summary of Proof General buffersSummary of Proof General buffers1214,46027 +@node Script editing commandsScript editing commands1276,48701 +@node Script processing commandsScript processing commands1354,51552 +@node Proof assistant commandsProof assistant commands1482,56853 +@node Toolbar commandsToolbar commands1632,61857 +@node Interrupting during trace outputInterrupting during trace output1656,62786 +@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1695,64710 +@node Goals buffer commandsGoals buffer commands1709,65210 +@node Advanced Script ManagementAdvanced Script Management1798,68743 +@node Visibility of completed proofsVisibility of completed proofs1829,69897 +@node Switching between proof scriptsSwitching between proof scripts1884,71820 +@node View of processed files View of processed files 1921,73792 +@node Retracting across filesRetracting across files1981,76843 +@node Asserting across filesAsserting across files1994,77474 +@node Automatic multiple file handlingAutomatic multiple file handling2007,78040 +@node Escaping script managementEscaping script management2032,79074 +@node Experimental featuresExperimental features2090,81277 +@node Support for other PackagesSupport for other Packages2124,82539 +@node Syntax highlightingSyntax highlighting2156,83414 +@node X-Symbol supportX-Symbol support2195,85035 +@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2254,87581 +@node Support for outline modeSupport for outline mode2313,89711 +@node Support for completionSupport for completion2339,90841 +@node Support for tagsSupport for tags2397,93017 +@node Customizing Proof GeneralCustomizing Proof General2449,95346 +@node Basic optionsBasic options2489,97016 +@node How to customizeHow to customize2513,97774 +@node Display customizationDisplay customization2564,99876 +@node User optionsUser options2689,105114 +@node Changing facesChanging faces2953,114504 +@node Tweaking configuration settingsTweaking configuration settings3028,117173 +@node Hints and TipsHints and Tips3085,119699 +@node Adding your own keybindingsAdding your own keybindings3104,120300 +@node Using file variablesUsing file variables3160,122833 +@node Using abbreviationsUsing abbreviations3219,125019 +@node LEGO Proof GeneralLEGO Proof General3258,126435 +@node LEGO specific commandsLEGO specific commands3299,127804 +@node LEGO tagsLEGO tags3319,128259 +@node LEGO customizationsLEGO customizations3329,128506 +@node Coq Proof GeneralCoq Proof General3361,129425 +@node Coq-specific commandsCoq-specific commands3377,129834 +@node Coq-specific variablesCoq-specific variables3399,130341 +@node Editing multiple proofsEditing multiple proofs3421,130999 +@node User-loaded tacticsUser-loaded tactics3445,132107 +@node Holes featureHoles feature3509,134581 +@node Isabelle Proof GeneralIsabelle Proof General3536,135868 +@node Isabelle commandsIsabelle commands3566,136998 +@node Logics and SettingsLogics and Settings3673,140046 +@node Isabelle customizationsIsabelle customizations3707,141586 +@node HOL Proof GeneralHOL Proof General3731,142068 +@node Shell Proof GeneralShell Proof General3773,143890 +@node Obtaining and InstallingObtaining and Installing3809,145349 +@node Obtaining Proof GeneralObtaining Proof General3825,145762 +@node Installing Proof General from tarballInstalling Proof General from tarball3856,147001 +@node Installing Proof General from RPM packageInstalling Proof General from RPM package3881,147833 +@node Setting the names of binariesSetting the names of binaries3896,148241 +@node Notes for syssiesNotes for syssies3924,149181 +@node Bugs and EnhancementsBugs and Enhancements3999,152217 +@node References4020,153032 +@node History of Proof GeneralHistory of Proof General4060,154056 +@node Old News for 3.0Old News for 3.04151,158158 +@node Old News for 3.1Old News for 3.14221,161852 +@node Old News for 3.2Old News for 3.24247,163024 +@node Old News for 3.3Old News for 3.34308,166027 +@node Old News for 3.4Old News for 3.44327,166924 +@node Function IndexFunction Index4350,167980 +@node Variable IndexVariable Index4354,168056 +@node Keystroke IndexKeystroke Index4358,168136 +@node Concept IndexConcept Index4362,168202 doc/PG-adapting.texi,3776 @node Top157,4775 @@ -3553,58 +3580,58 @@ doc/PG-adapting.texi,3776 @node Credits272,9169 @node Beginning with a New ProverBeginning with a New Prover282,9461 @node Overview of adding a new proverOverview of adding a new prover323,11410 -@node Demonstration instance and easy configurationDemonstration instance and easy configuration397,14831 -@node Major modes used by Proof GeneralMajor modes used by Proof General466,18222 -@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands539,21305 -@node Settings for generic user-level commandsSettings for generic user-level commands554,21851 -@node Menu configurationMenu configuration599,23587 -@node Toolbar configurationToolbar configuration623,24505 -@node Proof Script SettingsProof Script Settings681,26750 -@node Recognizing commands and commentsRecognizing commands and comments703,27330 -@node Recognizing proofsRecognizing proofs824,32857 -@node Recognizing other elementsRecognizing other elements936,37676 -@node Configuring undo behaviourConfiguring undo behaviour1062,43154 -@node Nested proofsNested proofs1200,48501 -@node Safe (state-preserving) commandsSafe (state-preserving) commands1240,50128 -@node Activate scripting hookActivate scripting hook1263,51074 -@node Automatic multiple filesAutomatic multiple files1287,51938 -@node Completions1309,52785 -@node Proof Shell SettingsProof Shell Settings1349,54263 -@node Proof shell commandsProof shell commands1380,55545 -@node Script input to the shellScript input to the shell1547,62724 -@node Settings for matching various output from proof processSettings for matching various output from proof process1614,65767 -@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1745,71534 -@node Hooks and other settingsHooks and other settings1955,81081 -@node Goals Buffer SettingsGoals Buffer Settings2054,85078 -@node Splash Screen SettingsSplash Screen Settings2131,88192 -@node Global ConstantsGlobal Constants2157,88950 -@node Handling Multiple FilesHandling Multiple Files2183,89799 -@node Configuring Editing SyntaxConfiguring Editing Syntax2335,97583 -@node Configuring Font LockConfiguring Font Lock2392,99700 -@node Configuring X-SymbolConfiguring X-Symbol2479,103943 -@node Writing More Lisp CodeWriting More Lisp Code2539,106466 -@node Default values for generic settingsDefault values for generic settings2556,107111 -@node Adding prover-specific configurationsAdding prover-specific configurations2586,108194 -@node Useful variablesUseful variables2629,109476 -@node Useful functions and macrosUseful functions and macros2655,110270 -@node Internals of Proof GeneralInternals of Proof General2758,114233 -@node Spans2786,115141 -@node Proof General site configurationProof General site configuration2799,115515 -@node Configuration variable mechanismsConfiguration variable mechanisms2879,118603 -@node Global variablesGlobal variables2997,123839 -@node Proof script modeProof script mode3067,126389 -@node Proof shell modeProof shell mode3326,138044 -@node Debugging3732,154091 -@node Plans and IdeasPlans and Ideas3775,154968 -@node Proof by pointing and similar featuresProof by pointing and similar features3796,155690 -@node Granularity of atomic command sequencesGranularity of atomic command sequences3834,157348 -@node Browser mode for script files and theoriesBrowser mode for script files and theories3879,159573 -@node Demonstration InstantiationsDemonstration Instantiations3909,160604 -@node demoisa-easy.el3925,161035 -@node demoisa.el3988,163274 -@node Function IndexFunction Index4156,168803 -@node Variable IndexVariable Index4160,168879 -@node Concept IndexConcept Index4169,169058 +@node Demonstration instance and easy configurationDemonstration instance and easy configuration398,14707 +@node Major modes used by Proof GeneralMajor modes used by Proof General467,18098 +@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands500,19449 +@node Settings for generic user-level commandsSettings for generic user-level commands515,19995 +@node Menu configurationMenu configuration560,21729 +@node Toolbar configurationToolbar configuration584,22646 +@node Proof Script SettingsProof Script Settings642,24888 +@node Recognizing commands and commentsRecognizing commands and comments664,25468 +@node Recognizing proofsRecognizing proofs785,31003 +@node Recognizing other elementsRecognizing other elements897,35821 +@node Configuring undo behaviourConfiguring undo behaviour1023,41332 +@node Nested proofsNested proofs1160,46743 +@node Safe (state-preserving) commandsSafe (state-preserving) commands1200,48369 +@node Activate scripting hookActivate scripting hook1223,49315 +@node Automatic multiple filesAutomatic multiple files1247,50178 +@node Completions1269,51025 +@node Proof Shell SettingsProof Shell Settings1310,52514 +@node Proof shell commandsProof shell commands1341,53796 +@node Script input to the shellScript input to the shell1508,60959 +@node Settings for matching various output from proof processSettings for matching various output from proof process1575,63999 +@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1706,69760 +@node Hooks and other settingsHooks and other settings1916,79353 +@node Goals Buffer SettingsGoals Buffer Settings1997,82722 +@node Splash Screen SettingsSplash Screen Settings2074,85821 +@node Global ConstantsGlobal Constants2100,86579 +@node Handling Multiple FilesHandling Multiple Files2126,87420 +@node Configuring Editing SyntaxConfiguring Editing Syntax2278,95204 +@node Configuring Font LockConfiguring Font Lock2337,97325 +@node Configuring X-SymbolConfiguring X-Symbol2424,101610 +@node Writing More Lisp CodeWriting More Lisp Code2484,104130 +@node Default values for generic settingsDefault values for generic settings2501,104775 +@node Adding prover-specific configurationsAdding prover-specific configurations2531,105858 +@node Useful variablesUseful variables2574,107140 +@node Useful functions and macrosUseful functions and macros2589,107629 +@node Internals of Proof GeneralInternals of Proof General2692,111592 +@node Spans2720,112500 +@node Proof General site configurationProof General site configuration2733,112874 +@node Configuration variable mechanismsConfiguration variable mechanisms2813,115962 +@node Global variablesGlobal variables2931,121198 +@node Proof script modeProof script mode3001,123748 +@node Proof shell modeProof shell mode3260,135403 +@node Debugging3665,151380 +@node Plans and IdeasPlans and Ideas3708,152256 +@node Proof by pointing and similar featuresProof by pointing and similar features3729,152978 +@node Granularity of atomic command sequencesGranularity of atomic command sequences3767,154636 +@node Browser mode for script files and theoriesBrowser mode for script files and theories3812,156861 +@node Demonstration InstantiationsDemonstration Instantiations3842,157892 +@node demoisa-easy.el3858,158323 +@node demoisa.el3921,160562 +@node Function IndexFunction Index4089,166091 +@node Variable IndexVariable Index4093,166167 +@node Concept IndexConcept Index4102,166346 x-symbol/lisp/_pkg.el,0 @@ -3612,9 +3639,9 @@ x-symbol/lisp/custom-load.el,0 lib/holes-load.el,0 -generic/proof-system.el,0 +generic/test-req.el,0 -generic/_pkg.el,0 +generic/test-mac2.el,0 twelf/x-symbol-twelf.el,0 @@ -3622,7 +3649,7 @@ pgshell/pgshell.el,0 lego/x-symbol-lego.el,0 -isar/x-symbol-isar.el,0 +isar/test.el,0 isar/isar-templates.el,0 @@ -3630,6 +3657,8 @@ isar/isar-autotest.el,0 isar/interface-setup.el,0 +isar/comptest.el,0 + hol98/x-symbol-hol98.el,0 hol98/hol98.el,0 |