diff options
| -rw-r--r-- | TAGS | 2239 | ||||
| -rw-r--r-- | images/README | 13 |
2 files changed, 1501 insertions, 751 deletions
@@ -13,175 +13,176 @@ coq/coq-abbrev.el,468 (defpgdefault menu-entries 71,2121 (defpgdefault help-menu-entries152,5542 -coq/coq-db.el,434 +coq/coq-db.el,474 (defconst coq-syntax-db 18,455 -(defvar coq-user-tactics-db48,1608 -(defun coq-insert-from-db 58,1957 -(defun coq-build-regexp-list-from-db 76,2738 -(defun max-length-db 98,3790 -(defun coq-build-menu-from-db-internal 110,4065 -(defun coq-build-title-menu 145,5689 -(defun coq-build-menu-from-db 155,6058 -(defun coq-build-abbrev-table-from-db 175,6805 -(defun filter-state-preserving 191,7359 -(defun filter-state-changing 196,7513 +(defvar coq-user-tactics-db54,1828 +(defun coq-insert-from-db 64,2177 +(defun coq-build-regexp-list-from-db 82,2958 +(defun max-length-db 104,4011 +(defun coq-build-menu-from-db-internal 116,4286 +(defun coq-build-title-menu 151,5910 +(defun coq-sort-menu-entries 160,6278 +(defun coq-build-menu-from-db 163,6398 +(defun coq-build-abbrev-table-from-db 183,7169 +(defun filter-state-preserving 199,7723 +(defun filter-state-changing 204,7877 coq/coq.el,6119 -(defcustom coq-prog-name 28,654 -(defcustom coq-prog-args 41,1184 -(defcustom coq-compile-file-command 44,1294 -(defcustom coq-default-undo-limit 54,1663 -(defconst coq-shell-init-cmd 59,1791 -(defcustom coq-utf-safe 68,2007 -(defconst coq-shell-restart-cmd 84,2639 -(defvar coq-shell-prompt-pattern 91,2899 -(defvar coq-shell-cd 98,3221 -(defvar coq-shell-abort-goal-regexp 102,3376 -(defvar coq-shell-proof-completed-regexp 105,3502 -(defvar coq-goal-regexp108,3633 -(defun coq-library-directory 117,3822 -(defcustom coq-tags 124,4002 -(defconst coq-interrupt-regexp 129,4152 -(defcustom coq-www-home-page 134,4273 -(defvar coq-outline-regexp144,4444 -(defvar coq-outline-heading-end-regexp 151,4658 -(defvar coq-shell-outline-regexp 153,4712 -(defvar coq-shell-outline-heading-end-regexp 154,4762 -(defconst coq-kill-goal-command 159,4872 -(defconst coq-forget-id-command 160,4915 -(defconst coq-back-n-command 161,4962 -(defconst coq-state-preserving-tactics-regexp 165,5106 -(defconst coq-state-changing-commands-regexp167,5207 -(defconst coq-state-preserving-commands-regexp 169,5314 -(defconst coq-commands-regexp 171,5426 -(defvar coq-retractable-instruct-regexp 173,5504 -(defvar coq-non-retractable-instruct-regexp 175,5595 -(defvar coq-keywords-section179,5735 -(defvar coq-section-regexp 182,5829 -(defun coq-set-undo-limit 216,6929 -(defconst coq-keywords-decl-defn-regexp227,7368 -(defun coq-proof-mode-p 231,7518 -(defun coq-is-comment-or-proverprocp 242,7928 -(defun coq-is-goalsave-p 244,8032 -(defun coq-is-module-equal-p 245,8107 -(defun coq-is-def-p 248,8303 -(defun coq-is-decl-defn-p 250,8411 -(defun coq-state-preserving-command-p 255,8578 -(defun coq-command-p 258,8712 -(defun coq-state-preserving-tactic-p 261,8812 -(defun coq-state-changing-tactic-p 266,8960 -(defun coq-state-changing-command-p 273,9194 -(defun coq-section-or-module-start-p 280,9540 -(defun build-list-id-from-string 289,9781 -(defun coq-last-prompt-info 302,10311 -(defun coq-last-prompt-info-safe 314,10852 -(defvar coq-last-but-one-statenum 324,11367 -(defvar coq-last-but-one-proofnum 326,11434 -(defvar coq-last-but-one-proofstack 328,11497 -(defun coq-get-span-statenum 330,11539 -(defun coq-get-span-proofnum 335,11654 -(defun coq-get-span-proofstack 340,11769 -(defun coq-set-span-statenum 345,11913 -(defun coq-get-span-goalcmd 350,12044 -(defun coq-set-span-goalcmd 355,12158 -(defun coq-set-span-proofnum 360,12288 -(defun coq-set-span-proofstack 365,12419 -(defun proof-last-locked-span 370,12579 -(defun coq-set-state-infos 385,13183 -(defun count-not-intersection 425,15262 -(defun coq-find-and-forget-v81 456,16516 -(defun coq-find-and-forget-v80 484,17648 -(defun coq-find-and-forget 579,22347 -(defvar coq-current-goal 592,22887 -(defun coq-goal-hyp 595,22952 -(defun coq-state-preserving-p 608,23382 -(defconst notation-print-kinds-table 623,23888 -(defun coq-PrintScope 627,24056 -(defun coq-guess-or-ask-for-string 646,24612 -(defun coq-ask-do 657,24997 -(defun coq-SearchIsos 666,25385 -(defun coq-SearchConstant 672,25618 -(defun coq-SearchRewrite 676,25711 -(defun coq-SearchAbout 680,25809 -(defun coq-Print 684,25901 -(defun coq-About 688,26023 -(defun coq-LocateConstant 692,26140 -(defun coq-LocateLibrary 698,26275 -(defun coq-addquotes 704,26425 -(defun coq-LocateNotation 706,26473 -(defun coq-Pwd 713,26672 -(defun coq-Inspect 719,26804 -(defun coq-PrintSection(723,26904 -(defun coq-Print-implicit 727,26998 -(defun coq-Check 732,27150 -(defun coq-Show 737,27260 -(defun coq-PrintHint 752,27706 -(defun coq-Compile 760,27852 -(defun coq-guess-command-line 773,28171 -(defun coq-pre-shell-start 795,29019 -(defun coq-mode-config 807,29543 -(defun coq-hybrid-ouput-goals-response-p 923,33750 -(defun coq-hybrid-ouput-goals-response 929,34008 -(defun coq-shell-mode-config 951,34920 -(defun coq-goals-mode-config 992,36757 -(defun coq-response-config 999,36989 -(defun coq-maybe-compile-buffer 1019,37695 -(defun coq-ancestors-of 1056,39229 -(defun coq-all-ancestors-of 1079,40196 -(defconst coq-require-command-regexp 1091,40589 -(defun coq-process-require-command 1096,40798 -(defun coq-included-children 1101,40925 -(defun coq-process-file 1122,41764 -(defpacustom print-fully-explicit 1147,42679 -(defpacustom print-implicit 1152,42828 -(defpacustom print-coercions 1157,42995 -(defpacustom print-match-wildcards 1162,43140 -(defpacustom print-elim-types 1167,43321 -(defpacustom printing-depth 1172,43488 -(defpacustom time-commands 1177,43650 -(defpacustom auto-compile-vos 1181,43761 -(defpacustom translate-to-v8 1203,44716 -(defun coq-preprocessing 1212,44932 -(defun coq-fake-constant-markup 1227,45351 -(defun coq-create-span-menu 1249,46158 -(defconst module-kinds-table 1276,46960 -(defconst modtype-kinds-table1280,47110 -(defun coq-insert-section-or-module 1284,47239 -(defconst reqkinds-kinds-table1307,48099 -(defun coq-insert-requires 1312,48244 -(defun coq-end-Section 1328,48750 -(defun coq-insert-intros 1346,49334 -(defun coq-insert-match 1358,49858 -(defun coq-insert-tactic 1390,51036 -(defun coq-insert-tactical 1396,51275 -(defun coq-insert-command 1402,51524 -(defun coq-insert-term 1408,51768 -(define-key coq-keymap 1415,51966 -(define-key coq-keymap 1416,52024 -(define-key coq-keymap 1417,52081 -(define-key coq-keymap 1418,52150 -(define-key coq-keymap 1419,52206 -(define-key coq-keymap 1420,52255 -(define-key coq-keymap 1421,52313 -(define-key coq-keymap 1423,52374 -(define-key coq-keymap 1424,52433 -(define-key coq-keymap 1426,52497 -(define-key coq-keymap 1427,52557 -(define-key coq-keymap 1429,52613 -(define-key coq-keymap 1430,52663 -(define-key coq-keymap 1431,52713 -(define-key coq-keymap 1432,52763 -(define-key coq-keymap 1433,52817 -(define-key coq-keymap 1434,52876 -(defvar last-coq-error-location 1444,53059 -(defun coq-get-last-error-location 1453,53458 -(defun coq-highlight-error 1486,54855 -(defun coq-decide-highlight-error 1555,57540 -(defun coq-highlight-error-hook 1560,57702 -(defun first-word-of-buffer 1571,58095 -(defun coq-show-first-goal 1580,58326 -(defun is-not-split-vertic 1605,59215 -(defun optim-resp-windows 1614,59654 +(defcustom coq-prog-name 28,652 +(defcustom coq-prog-args 41,1182 +(defcustom coq-compile-file-command 44,1292 +(defcustom coq-default-undo-limit 54,1661 +(defconst coq-shell-init-cmd 59,1789 +(defcustom coq-utf-safe 68,2005 +(defconst coq-shell-restart-cmd 84,2637 +(defvar coq-shell-prompt-pattern 91,2897 +(defvar coq-shell-cd 98,3219 +(defvar coq-shell-abort-goal-regexp 102,3374 +(defvar coq-shell-proof-completed-regexp 105,3500 +(defvar coq-goal-regexp108,3631 +(defun coq-library-directory 117,3820 +(defcustom coq-tags 124,4000 +(defconst coq-interrupt-regexp 129,4150 +(defcustom coq-www-home-page 134,4271 +(defvar coq-outline-regexp144,4442 +(defvar coq-outline-heading-end-regexp 151,4656 +(defvar coq-shell-outline-regexp 153,4710 +(defvar coq-shell-outline-heading-end-regexp 154,4760 +(defconst coq-kill-goal-command 159,4870 +(defconst coq-forget-id-command 160,4913 +(defconst coq-back-n-command 161,4960 +(defconst coq-state-preserving-tactics-regexp 165,5104 +(defconst coq-state-changing-commands-regexp167,5205 +(defconst coq-state-preserving-commands-regexp 169,5312 +(defconst coq-commands-regexp 171,5424 +(defvar coq-retractable-instruct-regexp 173,5502 +(defvar coq-non-retractable-instruct-regexp 175,5593 +(defvar coq-keywords-section179,5733 +(defvar coq-section-regexp 182,5827 +(defun coq-set-undo-limit 216,6927 +(defconst coq-keywords-decl-defn-regexp227,7366 +(defun coq-proof-mode-p 231,7516 +(defun coq-is-comment-or-proverprocp 242,7926 +(defun coq-is-goalsave-p 244,8030 +(defun coq-is-module-equal-p 245,8105 +(defun coq-is-def-p 248,8301 +(defun coq-is-decl-defn-p 250,8409 +(defun coq-state-preserving-command-p 255,8576 +(defun coq-command-p 258,8710 +(defun coq-state-preserving-tactic-p 261,8810 +(defun coq-state-changing-tactic-p 266,8958 +(defun coq-state-changing-command-p 273,9192 +(defun coq-section-or-module-start-p 280,9538 +(defun build-list-id-from-string 289,9779 +(defun coq-last-prompt-info 302,10309 +(defun coq-last-prompt-info-safe 314,10850 +(defvar coq-last-but-one-statenum 324,11365 +(defvar coq-last-but-one-proofnum 326,11432 +(defvar coq-last-but-one-proofstack 328,11495 +(defun coq-get-span-statenum 330,11537 +(defun coq-get-span-proofnum 335,11652 +(defun coq-get-span-proofstack 340,11767 +(defun coq-set-span-statenum 345,11911 +(defun coq-get-span-goalcmd 350,12042 +(defun coq-set-span-goalcmd 355,12156 +(defun coq-set-span-proofnum 360,12286 +(defun coq-set-span-proofstack 365,12417 +(defun proof-last-locked-span 370,12577 +(defun coq-set-state-infos 385,13181 +(defun count-not-intersection 425,15260 +(defun coq-find-and-forget-v81 456,16514 +(defun coq-find-and-forget-v80 484,17646 +(defun coq-find-and-forget 579,22345 +(defvar coq-current-goal 592,22885 +(defun coq-goal-hyp 595,22950 +(defun coq-state-preserving-p 608,23380 +(defconst notation-print-kinds-table 623,23886 +(defun coq-PrintScope 627,24054 +(defun coq-guess-or-ask-for-string 646,24610 +(defun coq-ask-do 657,24995 +(defun coq-SearchIsos 666,25383 +(defun coq-SearchConstant 672,25616 +(defun coq-SearchRewrite 676,25709 +(defun coq-SearchAbout 680,25807 +(defun coq-Print 684,25899 +(defun coq-About 688,26021 +(defun coq-LocateConstant 692,26138 +(defun coq-LocateLibrary 698,26273 +(defun coq-addquotes 704,26423 +(defun coq-LocateNotation 706,26471 +(defun coq-Pwd 713,26670 +(defun coq-Inspect 719,26802 +(defun coq-PrintSection(723,26902 +(defun coq-Print-implicit 727,26996 +(defun coq-Check 732,27148 +(defun coq-Show 737,27258 +(defun coq-PrintHint 752,27704 +(defun coq-Compile 760,27850 +(defun coq-guess-command-line 773,28169 +(defun coq-pre-shell-start 795,29017 +(defun coq-mode-config 807,29541 +(defun coq-hybrid-ouput-goals-response-p 923,33751 +(defun coq-hybrid-ouput-goals-response 929,34009 +(defun coq-shell-mode-config 951,34921 +(defun coq-goals-mode-config 992,36758 +(defun coq-response-config 999,36990 +(defun coq-maybe-compile-buffer 1019,37696 +(defun coq-ancestors-of 1056,39230 +(defun coq-all-ancestors-of 1079,40197 +(defconst coq-require-command-regexp 1091,40590 +(defun coq-process-require-command 1096,40799 +(defun coq-included-children 1101,40926 +(defun coq-process-file 1122,41765 +(defpacustom print-fully-explicit 1147,42680 +(defpacustom print-implicit 1152,42829 +(defpacustom print-coercions 1157,42996 +(defpacustom print-match-wildcards 1162,43141 +(defpacustom print-elim-types 1167,43322 +(defpacustom printing-depth 1172,43489 +(defpacustom time-commands 1177,43651 +(defpacustom auto-compile-vos 1181,43762 +(defpacustom translate-to-v8 1203,44717 +(defun coq-preprocessing 1212,44933 +(defun coq-fake-constant-markup 1227,45352 +(defun coq-create-span-menu 1249,46159 +(defconst module-kinds-table 1276,46961 +(defconst modtype-kinds-table1280,47111 +(defun coq-insert-section-or-module 1284,47240 +(defconst reqkinds-kinds-table1307,48100 +(defun coq-insert-requires 1312,48245 +(defun coq-end-Section 1328,48751 +(defun coq-insert-intros 1346,49335 +(defun coq-insert-match 1358,49859 +(defun coq-insert-tactic 1390,51037 +(defun coq-insert-tactical 1396,51276 +(defun coq-insert-command 1402,51525 +(defun coq-insert-term 1408,51769 +(define-key coq-keymap 1415,51967 +(define-key coq-keymap 1416,52025 +(define-key coq-keymap 1417,52082 +(define-key coq-keymap 1418,52151 +(define-key coq-keymap 1419,52207 +(define-key coq-keymap 1420,52256 +(define-key coq-keymap 1421,52314 +(define-key coq-keymap 1423,52375 +(define-key coq-keymap 1424,52434 +(define-key coq-keymap 1426,52498 +(define-key coq-keymap 1427,52558 +(define-key coq-keymap 1429,52614 +(define-key coq-keymap 1430,52664 +(define-key coq-keymap 1431,52714 +(define-key coq-keymap 1432,52764 +(define-key coq-keymap 1433,52818 +(define-key coq-keymap 1434,52877 +(defvar last-coq-error-location 1444,53060 +(defun coq-get-last-error-location 1453,53459 +(defun coq-highlight-error 1486,54856 +(defun coq-decide-highlight-error 1555,57541 +(defun coq-highlight-error-hook 1560,57703 +(defun first-word-of-buffer 1571,58096 +(defun coq-show-first-goal 1580,58327 +(defun is-not-split-vertic 1605,59216 +(defun optim-resp-windows 1614,59655 coq/coq-indent.el,2241 (defconst coq-any-command-regexp11,262 @@ -246,66 +247,66 @@ 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,2331 -(defvar coq-version-is-V8 21,716 -(defvar coq-version-is-V8-0 23,795 -(defvar coq-version-is-V8-1 30,1167 -(defcustom coq-user-tactics-db 80,3378 -(defcustom coq-user-commands-db 97,3886 -(defvar coq-tactics-db114,4401 -(defvar coq-tacticals-db269,12393 -(defvar coq-decl-db291,13144 -(defvar coq-defn-db313,14362 -(defvar coq-goal-starters-db358,17620 -(defvar coq-commands-db379,18708 -(defvar coq-terms-db499,26844 -(defun coq-count-match 563,29478 -(defun coq-goal-command-str-v80-p 582,30332 -(defun coq-module-opening-p 605,31198 -(defun coq-section-command-p 616,31610 -(defun coq-goal-command-str-v81-p 620,31707 -(defun coq-goal-command-p-v81 635,32375 -(defun coq-goal-command-str-p 645,32711 -(defun coq-goal-command-p 655,33072 -(defvar coq-keywords-save-strict663,33380 -(defvar coq-keywords-save671,33479 -(defun coq-save-command-p 675,33555 -(defvar coq-keywords-kill-goal 684,33849 -(defvar coq-keywords-state-changing-misc-commands688,33940 -(defvar coq-keywords-goal691,34065 -(defvar coq-keywords-decl694,34148 -(defvar coq-keywords-defn697,34222 -(defvar coq-keywords-state-changing-commands701,34297 -(defvar coq-keywords-state-preserving-commands710,34495 -(defvar coq-keywords-commands715,34711 -(defvar coq-tacticals720,34859 -(defvar coq-reserved725,34995 -(defvar coq-state-changing-tactics734,35281 -(defvar coq-state-preserving-tactics737,35390 -(defvar coq-tactics741,35504 -(defvar coq-retractable-instruct744,35593 -(defvar coq-non-retractable-instruct747,35703 -(defvar coq-keywords751,35825 -(defvar coq-symbols758,35992 -(defvar coq-error-regexp 777,36205 -(defvar coq-id 780,36433 -(defvar coq-id-shy 781,36458 -(defvar coq-ids 783,36512 -(defun coq-first-abstr-regexp 785,36553 -(defun coq-first-abstr-regexp 788,36677 -(defvar coq-font-lock-terms796,36869 -(defconst coq-save-command-regexp-strict815,37667 -(defconst coq-save-command-regexp819,37834 -(defconst coq-save-with-hole-regexp823,37987 -(defconst coq-goal-command-regexp827,38145 -(defconst coq-goal-with-hole-regexp830,38245 -(defconst coq-decl-with-hole-regexp836,38532 -(defconst coq-defn-with-hole-regexp840,38664 -(defconst coq-with-with-hole-regexp874,39503 -(defvar coq-font-lock-keywords-1880,39755 -(defvar coq-font-lock-keywords 902,40869 -(defun coq-init-syntax-table 904,40927 -(defconst coq-generic-expression933,41825 +coq/coq-syntax.el,2333 +(defvar coq-version-is-V8 21,729 +(defvar coq-version-is-V8-0 23,808 +(defvar coq-version-is-V8-1 30,1180 +(defcustom coq-user-tactics-db 80,3391 +(defcustom coq-user-commands-db 97,3897 +(defcustom coq-user-tacticals-db 113,4409 +(defvar coq-tactics-db131,4925 +(defvar coq-tacticals-db286,12908 +(defvar coq-decl-db310,13723 +(defvar coq-defn-db332,14941 +(defvar coq-goal-starters-db384,18849 +(defvar coq-commands-db409,20266 +(defvar coq-terms-db533,29360 +(defun coq-count-match 597,31994 +(defun coq-goal-command-str-v80-p 616,32848 +(defun coq-module-opening-p 639,33714 +(defun coq-section-command-p 650,34126 +(defun coq-goal-command-str-v81-p 654,34223 +(defun coq-goal-command-p-v81 669,34891 +(defun coq-goal-command-str-p 679,35227 +(defun coq-goal-command-p 689,35588 +(defvar coq-keywords-save-strict697,35896 +(defvar coq-keywords-save706,36007 +(defun coq-save-command-p 710,36083 +(defvar coq-keywords-kill-goal 719,36377 +(defvar coq-keywords-state-changing-misc-commands723,36468 +(defvar coq-keywords-goal726,36593 +(defvar coq-keywords-decl729,36676 +(defvar coq-keywords-defn732,36750 +(defvar coq-keywords-state-changing-commands736,36825 +(defvar coq-keywords-state-preserving-commands745,37023 +(defvar coq-keywords-commands750,37239 +(defvar coq-tacticals755,37387 +(defvar coq-reserved760,37523 +(defvar coq-state-changing-tactics769,37816 +(defvar coq-state-preserving-tactics772,37925 +(defvar coq-tactics776,38039 +(defvar coq-retractable-instruct779,38128 +(defvar coq-non-retractable-instruct782,38238 +(defvar coq-keywords786,38360 +(defvar coq-symbols793,38527 +(defvar coq-error-regexp 812,38740 +(defvar coq-id 815,38968 +(defvar coq-id-shy 816,38993 +(defvar coq-ids 818,39047 +(defun coq-first-abstr-regexp 820,39088 +(defvar coq-font-lock-terms823,39184 +(defconst coq-save-command-regexp-strict837,39796 +(defconst coq-save-command-regexp841,39963 +(defconst coq-save-with-hole-regexp845,40116 +(defconst coq-goal-command-regexp849,40274 +(defconst coq-goal-with-hole-regexp852,40374 +(defconst coq-decl-with-hole-regexp856,40506 +(defconst coq-defn-with-hole-regexp860,40638 +(defconst coq-with-with-hole-regexp871,40922 +(defvar coq-font-lock-keywords-1877,41212 +(defvar coq-font-lock-keywords 900,42408 +(defun coq-init-syntax-table 902,42466 +(defconst coq-generic-expression931,43364 coq/x-symbol-coq.el,1746 (defvar x-symbol-coq-required-fonts 16,384 @@ -357,7 +358,7 @@ demoisa/demoisa.el,390 (define-derived-mode demoisa-goals-mode 133,4387 (defun demoisa-pre-shell-start 152,5169 -isar/isabelle-system.el,1582 +isar/isabelle-system.el,1471 (defgroup isabelle 19,602 (defcustom isabelle-web-page23,730 (defcustom isa-isatool-command34,1025 @@ -371,66 +372,61 @@ isar/isabelle-system.el,1582 (defun isabelle-choose-logic 162,5857 (defun isa-tool-list-logics 184,6829 (defun isa-view-doc 191,7067 -(defvar isabelle-version-string 198,7291 -(defun isa-version 200,7332 -(defconst isa-supports-pgip 213,7815 -(defun isa-tool-list-docs 221,8045 -(defun isa-quit 239,8767 -(defconst isabelle-verbatim-regexp 246,8962 -(defun isabelle-verbatim 249,9103 -(defcustom isabelle-refresh-logics 256,9259 -(defcustom isabelle-logics-available 264,9586 -(defcustom isabelle-chosen-logic 272,9886 -(defconst isabelle-docs-menu 285,10354 -(defun isabelle-logics-menu-calculate 295,10747 -(defvar isabelle-time-to-refresh-logics 311,11256 -(defun isabelle-logics-menu-refresh 314,11349 -(defun isabelle-logics-menu-filter 331,12048 -(defun isabelle-menu-bar-update-logics 337,12258 -(defvar isabelle-logics-menu-entries 348,12614 -(defvar isabelle-logics-menu 350,12686 -(defun isabelle-load-isar-keywords 363,13304 -(defpgdefault menu-entries384,14045 -(defpgdefault help-menu-entries 387,14097 -(defpgdefault x-symbol-language 395,14291 -(defun isabelle-convert-idmarkup-to-subterm 418,14906 -(defun isabelle-create-span-menu 442,15918 -(defun isabelle-xml-sml-escapes 458,16363 -(defun isabelle-process-pgip 461,16464 - -isar/isar.el,1314 -(defcustom isar-keywords-name 28,583 -(defpgdefault completion-table 45,1107 -(defcustom isar-web-page47,1160 -(defun isar-strip-terminators 61,1497 -(defun isar-markup-ml 74,1874 -(defun isar-mode-config-set-variables 79,2009 -(defun isar-shell-mode-config-set-variables 144,5024 -(defun isar-remove-file 249,9478 -(defun isar-shell-compute-new-files-list 259,9841 -(defun isar-activate-scripting 270,10307 -(define-derived-mode isar-shell-mode 279,10477 -(define-derived-mode isar-response-mode 284,10600 -(define-derived-mode isar-goals-mode 289,10782 -(define-derived-mode isar-mode 294,10957 -(defpgdefault menu-entries348,12934 -(defun isar-count-undos 378,14173 -(defun isar-detect-begin 405,15291 -(defun isar-command-nested 417,15656 -(defun isar-find-and-forget 434,16125 -(defun isar-goal-command-p 479,17865 -(defun isar-global-save-command-p 484,18037 -(defvar isar-current-goal 505,18882 -(defun isar-state-preserving-p 508,18948 -(defvar isar-shell-current-line-width 533,20107 -(defun isar-shell-adjust-line-width 539,20325 -(defun isar-pre-shell-start 559,21210 -(defun isar-preprocessing 571,21553 -(defun isar-mode-config 594,22819 -(defun isar-shell-mode-config 606,23389 -(defun isar-response-mode-config 617,23759 -(defun isar-goals-mode-config 626,24016 -(defun isar-goalhyp-test 637,24396 +(defun isa-tool-list-docs 199,7292 +(defun isa-quit 217,8014 +(defconst isabelle-verbatim-regexp 224,8209 +(defun isabelle-verbatim 227,8350 +(defcustom isabelle-refresh-logics 234,8506 +(defcustom isabelle-logics-available 242,8833 +(defcustom isabelle-chosen-logic 250,9133 +(defconst isabelle-docs-menu 263,9601 +(defun isabelle-logics-menu-calculate 273,9994 +(defvar isabelle-time-to-refresh-logics 289,10503 +(defun isabelle-logics-menu-refresh 292,10596 +(defun isabelle-logics-menu-filter 309,11295 +(defun isabelle-menu-bar-update-logics 315,11505 +(defvar isabelle-logics-menu-entries 326,11861 +(defvar isabelle-logics-menu 328,11933 +(defun isabelle-load-isar-keywords 341,12551 +(defpgdefault menu-entries362,13292 +(defpgdefault help-menu-entries 365,13344 +(defpgdefault x-symbol-language 373,13538 +(defun isabelle-convert-idmarkup-to-subterm 396,14153 +(defun isabelle-create-span-menu 420,15165 +(defun isabelle-xml-sml-escapes 436,15610 +(defun isabelle-process-pgip 439,15711 + +isar/isar.el,1243 +(defcustom isar-keywords-name 28,586 +(defpgdefault completion-table 45,1110 +(defcustom isar-web-page47,1163 +(defun isar-strip-terminators 61,1500 +(defun isar-markup-ml 74,1877 +(defun isar-mode-config-set-variables 79,2012 +(defun isar-shell-mode-config-set-variables 144,5027 +(defun isar-remove-file 241,9187 +(defun isar-shell-compute-new-files-list 251,9550 +(defun isar-activate-scripting 262,10016 +(define-derived-mode isar-shell-mode 271,10186 +(define-derived-mode isar-response-mode 276,10309 +(define-derived-mode isar-goals-mode 281,10491 +(define-derived-mode isar-mode 286,10666 +(defpgdefault menu-entries340,12643 +(defun isar-count-undos 370,13882 +(defun isar-find-and-forget 397,15007 +(defun isar-goal-command-p 438,16590 +(defun isar-global-save-command-p 443,16762 +(defvar isar-current-goal 464,17607 +(defun isar-state-preserving-p 467,17673 +(defvar isar-shell-current-line-width 492,18832 +(defun isar-shell-adjust-line-width 498,19050 +(defun isar-pre-shell-start 518,19935 +(defun isar-preprocessing 530,20278 +(defun isar-mode-config 553,21544 +(defun isar-shell-mode-config 565,22114 +(defun isar-response-mode-config 576,22484 +(defun isar-goals-mode-config 585,22741 +(defun isar-goalhyplit-test 596,23087 isar/isar-find-theorems.el,778 (defun isar-find-theorems-minibuffer 18,715 @@ -541,29 +537,29 @@ isar/isar-syntax.el,3471 (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-keywords420,14311 -(defconst isar-undo 454,14990 -(defun isar-remove 456,15052 -(defun isar-undos 459,15127 -(defun isar-cannot-undo 463,15233 -(defconst isar-theory-start-regexp466,15303 -(defconst isar-end-regexp472,15468 -(defconst isar-undo-fail-regexp476,15569 -(defconst isar-undo-skip-regexp480,15707 -(defconst isar-undo-ignore-regexp483,15828 -(defconst isar-undo-remove-regexp486,15893 -(defconst isar-any-entity-regexp494,16068 -(defconst isar-named-entity-regexp499,16255 -(defconst isar-unnamed-entity-regexp504,16432 -(defconst isar-next-entity-regexps507,16534 -(defconst isar-generic-expression515,16845 -(defconst isar-indent-any-regexp526,17162 -(defconst isar-indent-inner-regexp528,17255 -(defconst isar-indent-enclose-regexp530,17321 -(defconst isar-indent-open-regexp532,17437 -(defconst isar-indent-close-regexp534,17547 -(defconst isar-outline-regexp540,17684 -(defconst isar-outline-heading-end-regexp 544,17837 +(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,630 @@ -661,10 +657,10 @@ lego/lego.el,1766 (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,12761 -(defun lego-shell-compute-new-files-list 379,13036 -(defun lego-shell-mode-config 393,13562 -(defun lego-goals-mode-config 442,15498 +(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 lego/lego-syntax.el,600 (defconst lego-keywords-goal 15,358 @@ -890,32 +886,32 @@ plastic/plastic.el,2907 (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,15861 -(defun plastic-equal-module-filename 456,15964 -(defun plastic-shell-compute-new-files-list 462,16242 -(defun plastic-shell-mode-config 478,16779 -(defun plastic-goals-mode-config 529,18972 -(defun plastic-small-bar 541,19254 -(defun plastic-large-bar 543,19343 -(defun plastic-preprocessing 545,19481 -(defun plastic-all-ctxt 596,21309 -(defun plastic-send-one-undo 603,21487 -(defun plastic-minibuf-cmd 613,21815 -(defun plastic-minibuf 625,22294 -(defun plastic-synchro 632,22500 -(defun plastic-send-minibuf 637,22641 -(defun plastic-had-error 645,22970 -(defun plastic-reset-error 649,23145 -(defun plastic-call-if-no-error 652,23284 -(defun plastic-show-shell 657,23488 -(define-key plastic-keymap 666,23750 -(define-key plastic-keymap 667,23811 -(define-key plastic-keymap 668,23872 -(define-key plastic-keymap 669,23932 -(define-key plastic-keymap 670,23991 -(define-key plastic-keymap 671,24050 -(defalias 'proof-toolbar-command proof-toolbar-command681,24300 -(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd682,24351 +(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 plastic/plastic-syntax.el,648 (defconst plastic-keywords-goal 18,537 @@ -1155,13 +1151,14 @@ twelf/twelf-old.el,6958 (defun twelf-server-remove-menu 2651,107262 (defun twelf-server-reset-menu 2655,107374 -generic/pg-assoc.el,292 -(define-derived-mode proof-universal-keys-only-mode 20,565 -(defun proof-associated-buffers 32,989 -(defun proof-associated-windows 41,1186 -(defun pg-assoc-strip-subterm-markup 54,1602 -(defun pg-assoc-strip-subterm-markup-buf 80,2535 -(defun pg-assoc-strip-subterm-markup-buf-old 102,3271 +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 54,1600 +(defvar pg-assoc-ann-regexp 80,2533 +(defun pg-assoc-strip-subterm-markup-buf 83,2628 +(defun pg-assoc-strip-subterm-markup-buf-old 106,3347 generic/pg-autotest.el,442 (defvar pg-autotest-success 20,514 @@ -1187,13 +1184,13 @@ generic/pg-goals.el,704 (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 147,5298 -(defun pg-goals-make-top-span 274,10333 -(defun pg-goals-yank-subterm 309,11643 -(defun pg-goals-button-action 336,12543 -(defun proof-expand-path 357,13516 -(defun pg-goals-construct-command 366,13760 -(defun pg-goals-get-subterm-help 390,14612 +(defun pg-goals-analyse-structure 149,5301 +(defun pg-goals-make-top-span 276,10348 +(defun pg-goals-yank-subterm 316,11852 +(defun pg-goals-button-action 343,12752 +(defun proof-expand-path 364,13725 +(defun pg-goals-construct-command 373,13969 +(defun pg-goals-get-subterm-help 402,14994 generic/pg-metadata.el,128 (defcustom pg-metadata-default-directory 23,628 @@ -1360,15 +1357,15 @@ generic/pg-response.el,1188 (defun proof-shell-maybe-erase-response245,9051 (defun pg-response-display 276,10253 (defun pg-response-display-with-face 293,11075 -(defun pg-response-clear-displays 335,12689 -(defvar pg-response-next-error 353,13268 -(defun proof-next-error 357,13390 -(defun pg-response-has-error-location 437,16324 -(defvar proof-trace-last-fontify-pos 460,17157 -(defun proof-trace-fontify-pos 462,17200 -(defun proof-trace-buffer-display 470,17514 -(defun proof-trace-buffer-finish 494,18487 -(defun pg-thms-buffer-clear 515,19066 +(defun pg-response-clear-displays 331,12432 +(defvar pg-response-next-error 349,13011 +(defun proof-next-error 353,13133 +(defun pg-response-has-error-location 433,16067 +(defvar proof-trace-last-fontify-pos 456,16900 +(defun proof-trace-fontify-pos 458,16943 +(defun proof-trace-buffer-display 466,17257 +(defun proof-trace-buffer-finish 490,18230 +(defun pg-thms-buffer-clear 511,18809 generic/pg-thymodes.el,152 (defmacro pg-defthymode 19,466 @@ -1462,7 +1459,7 @@ generic/pg-xml.el,447 generic/proof-autoloads.el,80 (defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region250,10161 -generic/proof-config.el,11060 +generic/proof-config.el,11148 (defgroup proof-user-options 85,3232 (defcustom proof-electric-terminator-enable 90,3346 (defcustom proof-toolbar-enable 102,3880 @@ -1505,191 +1502,193 @@ generic/proof-config.el,11060 (defconst proof-tactics-name-face 525,19626 (defface proof-error-face 530,19850 (defface proof-warning-face538,20057 -(defface proof-eager-annotation-face547,20314 -(defface proof-debug-message-face555,20532 -(defface proof-boring-face563,20731 -(defface proof-mouse-highlight-face571,20923 -(defface proof-highlight-dependent-face579,21119 -(defface proof-highlight-dependency-face587,21328 -(defgroup prover-config 605,21587 -(defcustom proof-mode-for-shell 639,22706 -(defcustom proof-mode-for-response 646,22953 -(defcustom proof-mode-for-goals 653,23236 -(defcustom proof-mode-for-script 660,23491 -(defcustom proof-guess-command-line 671,23925 -(defcustom proof-assistant-home-page 686,24422 -(defcustom proof-context-command 692,24592 -(defcustom proof-info-command 697,24726 -(defcustom proof-showproof-command 704,24998 -(defcustom proof-goal-command 709,25134 -(defcustom proof-save-command 717,25432 -(defcustom proof-find-theorems-command 725,25742 -(defconst proof-toolbar-entries-default732,26051 -(defpgcustom toolbar-entries 764,27873 -(defcustom proof-assistant-true-value 782,28594 -(defcustom proof-assistant-false-value 788,28784 -(defcustom proof-assistant-format-int-fn 794,28978 -(defcustom proof-assistant-format-string-fn 801,29227 -(defcustom proof-assistant-setting-format 808,29494 -(defgroup proof-script 830,30189 -(defcustom proof-terminal-char 835,30319 -(defcustom proof-script-sexp-commands 845,30723 -(defcustom proof-script-command-end-regexp 856,31193 -(defcustom proof-script-command-start-regexp 874,32012 -(defcustom proof-script-use-old-parser 885,32474 -(defcustom proof-script-integral-proofs 897,32963 -(defcustom proof-script-fly-past-comments 912,33619 -(defcustom proof-script-parse-function 919,33936 -(defcustom proof-script-comment-start 937,34582 -(defcustom proof-script-comment-start-regexp 948,35017 -(defcustom proof-script-comment-end 956,35334 -(defcustom proof-script-comment-end-regexp 968,35752 -(defcustom pg-insert-output-as-comment-fn 976,36063 -(defcustom proof-string-start-regexp 982,36315 -(defcustom proof-string-end-regexp 987,36480 -(defcustom proof-case-fold-search 992,36641 -(defcustom proof-save-command-regexp 1001,37057 -(defcustom proof-save-with-hole-regexp 1006,37168 -(defcustom proof-save-with-hole-result 1018,37620 -(defcustom proof-goal-command-regexp 1029,38084 -(defcustom proof-goal-with-hole-regexp 1038,38476 -(defcustom proof-goal-with-hole-result 1050,38920 -(defcustom proof-non-undoables-regexp 1060,39319 -(defcustom proof-nested-undo-regexp 1071,39775 -(defcustom proof-ignore-for-undo-count 1087,40487 -(defcustom proof-script-next-entity-regexps 1095,40790 -(defcustom proof-script-find-next-entity-fn1139,42524 -(defcustom proof-script-imenu-generic-expression 1159,43354 -(defcustom proof-goal-command-p 1177,44209 -(defcustom proof-really-save-command-p 1204,45650 -(defcustom proof-completed-proof-behaviour 1216,46111 -(defcustom proof-count-undos-fn 1244,47471 -(defconst proof-no-command 1279,49072 -(defcustom proof-find-and-forget-fn 1284,49276 -(defcustom proof-forget-id-command 1301,49987 -(defcustom pg-topterm-goalhyp-fn 1311,50345 -(defcustom proof-kill-goal-command 1323,50898 -(defcustom proof-undo-n-times-cmd 1337,51408 -(defcustom proof-nested-goals-history-p 1351,51957 -(defcustom proof-state-preserving-p 1360,52295 -(defcustom proof-activate-scripting-hook 1370,52765 -(defcustom proof-deactivate-scripting-hook 1389,53543 -(defcustom proof-indent 1402,53908 -(defcustom proof-indent-hang 1407,54015 -(defcustom proof-indent-enclose-offset 1412,54141 -(defcustom proof-indent-open-offset 1417,54283 -(defcustom proof-indent-close-offset 1422,54420 -(defcustom proof-indent-any-regexp 1427,54558 -(defcustom proof-indent-inner-regexp 1432,54718 -(defcustom proof-indent-enclose-regexp 1437,54872 -(defcustom proof-indent-open-regexp 1442,55026 -(defcustom proof-indent-close-regexp 1447,55178 -(defcustom proof-script-font-lock-keywords 1453,55332 -(defcustom proof-script-syntax-table-entries 1461,55655 -(defcustom proof-script-span-context-menu-extensions 1479,56052 -(defgroup proof-shell 1505,56841 -(defcustom proof-prog-name 1515,57012 -(defpgcustom prog-args 1528,57647 -(defpgcustom prog-env 1541,58222 -(defcustom proof-shell-auto-terminate-commands 1550,58648 -(defcustom proof-shell-pre-sync-init-cmd 1559,59045 -(defcustom proof-shell-init-cmd 1573,59604 -(defcustom proof-shell-restart-cmd 1584,60074 -(defcustom proof-shell-quit-cmd 1589,60229 -(defcustom proof-shell-quit-timeout 1594,60396 -(defcustom proof-shell-cd-cmd 1604,60844 -(defcustom proof-shell-start-silent-cmd 1621,61511 -(defcustom proof-shell-stop-silent-cmd 1630,61887 -(defcustom proof-shell-silent-threshold 1639,62224 -(defcustom proof-shell-inform-file-processed-cmd 1647,62558 -(defcustom proof-shell-inform-file-retracted-cmd 1668,63481 -(defcustom proof-auto-multiple-files 1696,64752 -(defcustom proof-cannot-reopen-processed-files 1711,65473 -(defcustom proof-shell-require-command-regexp 1725,66140 -(defcustom proof-done-advancing-require-function 1736,66602 -(defcustom proof-shell-quiet-errors 1742,66842 -(defcustom proof-shell-prompt-pattern 1755,67176 -(defcustom proof-shell-wakeup-char 1765,67598 -(defcustom proof-shell-annotated-prompt-regexp 1771,67829 -(defcustom proof-shell-abort-goal-regexp 1787,68469 -(defcustom proof-shell-error-regexp 1792,68604 -(defcustom proof-shell-truncate-before-error 1812,69398 -(defcustom pg-next-error-regexp 1826,69941 -(defcustom pg-next-error-filename-regexp 1841,70551 -(defcustom pg-next-error-extract-filename 1865,71589 -(defcustom proof-shell-interrupt-regexp 1872,71832 -(defcustom proof-shell-proof-completed-regexp 1886,72424 -(defcustom proof-shell-clear-response-regexp 1899,72932 -(defcustom proof-shell-clear-goals-regexp 1906,73231 -(defcustom proof-shell-start-goals-regexp 1913,73524 -(defcustom proof-shell-end-goals-regexp 1921,73891 -(defcustom proof-shell-eager-annotation-start 1927,74133 -(defcustom proof-shell-eager-annotation-start-length 1945,74871 -(defcustom proof-shell-eager-annotation-end 1956,75298 -(defcustom proof-shell-assumption-regexp 1972,75974 -(defcustom proof-shell-process-file 1982,76386 -(defcustom proof-shell-retract-files-regexp 2004,77338 -(defcustom proof-shell-compute-new-files-list 2013,77674 -(defcustom pg-use-specials-for-fontify 2025,78219 -(defcustom pg-special-char-regexp 2033,78567 -(defcustom proof-shell-set-elisp-variable-regexp 2038,78711 -(defcustom proof-shell-match-pgip-cmd 2071,80183 -(defcustom proof-shell-issue-pgip-cmd 2080,80513 -(defcustom proof-shell-query-dependencies-cmd 2089,80869 -(defcustom proof-shell-theorem-dependency-list-regexp 2096,81129 -(defcustom proof-shell-theorem-dependency-list-split 2112,81789 -(defcustom proof-shell-show-dependency-cmd 2121,82214 -(defcustom proof-shell-identifier-under-mouse-cmd 2128,82483 -(defcustom proof-shell-trace-output-regexp 2151,83564 -(defcustom proof-shell-thms-output-regexp 2167,84108 -(defcustom proof-shell-unicode 2180,84494 -(defcustom proof-shell-filename-escapes 2188,84822 -(defcustom proof-shell-process-connection-type 2205,85502 -(defcustom proof-shell-strip-crs-from-input 2228,86549 -(defcustom proof-shell-strip-crs-from-output 2240,87038 -(defcustom proof-shell-insert-hook 2248,87406 -(defcustom proof-pre-shell-start-hook 2288,89370 -(defcustom proof-shell-handle-delayed-output-hook2304,89842 -(defcustom proof-shell-handle-error-or-interrupt-hook2310,90057 -(defcustom proof-shell-pre-interrupt-hook2328,90806 -(defcustom proof-shell-process-output-system-specific 2336,91078 -(defcustom proof-state-change-hook 2355,91943 -(defcustom proof-shell-font-lock-keywords 2366,92325 -(defcustom proof-shell-syntax-table-entries 2374,92653 -(defgroup proof-goals 2392,93025 -(defcustom pg-subterm-first-special-char 2397,93146 -(defcustom pg-subterm-anns-use-stack 2405,93458 -(defcustom pg-goals-change-goal 2414,93762 -(defcustom pbp-goal-command 2419,93877 -(defcustom pbp-hyp-command 2424,94033 -(defcustom pg-subterm-help-cmd 2429,94195 -(defcustom pg-goals-error-regexp 2436,94431 -(defcustom proof-shell-result-start 2441,94591 -(defcustom proof-shell-result-end 2447,94825 -(defcustom pg-subterm-start-char 2453,95038 -(defcustom pg-subterm-sep-char 2467,95620 -(defcustom pg-subterm-end-char 2473,95799 -(defcustom pg-topterm-regexp 2479,95956 -(defcustom proof-goals-font-lock-keywords 2496,96556 -(defcustom proof-resp-font-lock-keywords 2510,97235 -(defcustom pg-before-fontify-output-hook 2522,97813 -(defcustom pg-after-fontify-output-hook 2530,98173 -(defgroup proof-x-symbol 2542,98427 -(defcustom proof-xsym-extra-modes 2547,98555 -(defcustom proof-xsym-font-lock-keywords 2560,99184 -(defcustom proof-xsym-activate-command 2568,99561 -(defcustom proof-xsym-deactivate-command 2575,99797 -(defpgcustom x-symbol-language 2582,100039 -(defpgcustom favourites 2597,100486 -(defpgcustom menu-entries 2602,100676 -(defpgcustom help-menu-entries 2609,100913 -(defpgcustom keymap 2616,101176 -(defpgcustom completion-table 2621,101347 -(defpgcustom tags-program 2631,101712 -(defcustom proof-general-name 2643,101885 -(defcustom proof-general-home-page2648,102042 -(defcustom proof-unnamed-theorem-name2654,102201 -(defcustom proof-universal-keys2662,102477 +(defconst proof-warning-face 547,20314 +(defface proof-eager-annotation-face549,20365 +(defface proof-debug-message-face557,20583 +(defface proof-boring-face565,20782 +(defface proof-mouse-highlight-face573,20974 +(defface proof-highlight-dependent-face581,21170 +(defface proof-highlight-dependency-face589,21379 +(defface proof-active-area-face 597,21576 +(defgroup prover-config 614,21852 +(defcustom proof-mode-for-shell 648,22971 +(defcustom proof-mode-for-response 655,23218 +(defcustom proof-mode-for-goals 662,23501 +(defcustom proof-mode-for-script 669,23756 +(defcustom proof-guess-command-line 680,24190 +(defcustom proof-assistant-home-page 695,24687 +(defcustom proof-context-command 701,24857 +(defcustom proof-info-command 706,24991 +(defcustom proof-showproof-command 713,25263 +(defcustom proof-goal-command 718,25399 +(defcustom proof-save-command 726,25697 +(defcustom proof-find-theorems-command 734,26007 +(defconst proof-toolbar-entries-default741,26316 +(defpgcustom toolbar-entries 773,28138 +(defcustom proof-assistant-true-value 791,28859 +(defcustom proof-assistant-false-value 797,29049 +(defcustom proof-assistant-format-int-fn 803,29243 +(defcustom proof-assistant-format-string-fn 810,29492 +(defcustom proof-assistant-setting-format 817,29759 +(defgroup proof-script 839,30454 +(defcustom proof-terminal-char 844,30584 +(defcustom proof-script-sexp-commands 854,30988 +(defcustom proof-script-command-end-regexp 865,31458 +(defcustom proof-script-command-start-regexp 883,32277 +(defcustom proof-script-use-old-parser 894,32739 +(defcustom proof-script-integral-proofs 906,33228 +(defcustom proof-script-fly-past-comments 921,33884 +(defcustom proof-script-parse-function 928,34201 +(defcustom proof-script-comment-start 946,34847 +(defcustom proof-script-comment-start-regexp 957,35282 +(defcustom proof-script-comment-end 965,35599 +(defcustom proof-script-comment-end-regexp 977,36017 +(defcustom pg-insert-output-as-comment-fn 985,36328 +(defcustom proof-string-start-regexp 991,36580 +(defcustom proof-string-end-regexp 996,36745 +(defcustom proof-case-fold-search 1001,36906 +(defcustom proof-save-command-regexp 1010,37322 +(defcustom proof-save-with-hole-regexp 1015,37433 +(defcustom proof-save-with-hole-result 1027,37885 +(defcustom proof-goal-command-regexp 1038,38349 +(defcustom proof-goal-with-hole-regexp 1047,38741 +(defcustom proof-goal-with-hole-result 1059,39185 +(defcustom proof-non-undoables-regexp 1069,39584 +(defcustom proof-nested-undo-regexp 1080,40040 +(defcustom proof-ignore-for-undo-count 1096,40752 +(defcustom proof-script-next-entity-regexps 1104,41055 +(defcustom proof-script-find-next-entity-fn1148,42789 +(defcustom proof-script-imenu-generic-expression 1168,43619 +(defcustom proof-goal-command-p 1186,44474 +(defcustom proof-really-save-command-p 1213,45915 +(defcustom proof-completed-proof-behaviour 1225,46376 +(defcustom proof-count-undos-fn 1253,47736 +(defconst proof-no-command 1288,49337 +(defcustom proof-find-and-forget-fn 1293,49541 +(defcustom proof-forget-id-command 1310,50252 +(defcustom pg-topterm-goalhyplit-fn 1320,50610 +(defcustom proof-kill-goal-command 1332,51166 +(defcustom proof-undo-n-times-cmd 1346,51676 +(defcustom proof-nested-goals-history-p 1360,52225 +(defcustom proof-state-preserving-p 1369,52563 +(defcustom proof-activate-scripting-hook 1379,53033 +(defcustom proof-deactivate-scripting-hook 1398,53811 +(defcustom proof-indent 1411,54176 +(defcustom proof-indent-hang 1416,54283 +(defcustom proof-indent-enclose-offset 1421,54409 +(defcustom proof-indent-open-offset 1426,54551 +(defcustom proof-indent-close-offset 1431,54688 +(defcustom proof-indent-any-regexp 1436,54826 +(defcustom proof-indent-inner-regexp 1441,54986 +(defcustom proof-indent-enclose-regexp 1446,55140 +(defcustom proof-indent-open-regexp 1451,55294 +(defcustom proof-indent-close-regexp 1456,55446 +(defcustom proof-script-font-lock-keywords 1462,55600 +(defcustom proof-script-syntax-table-entries 1470,55923 +(defcustom proof-script-span-context-menu-extensions 1488,56320 +(defgroup proof-shell 1514,57109 +(defcustom proof-prog-name 1524,57280 +(defpgcustom prog-args 1537,57915 +(defpgcustom prog-env 1550,58490 +(defcustom proof-shell-auto-terminate-commands 1559,58916 +(defcustom proof-shell-pre-sync-init-cmd 1568,59313 +(defcustom proof-shell-init-cmd 1582,59872 +(defcustom proof-shell-restart-cmd 1593,60342 +(defcustom proof-shell-quit-cmd 1598,60497 +(defcustom proof-shell-quit-timeout 1603,60664 +(defcustom proof-shell-cd-cmd 1613,61112 +(defcustom proof-shell-start-silent-cmd 1630,61779 +(defcustom proof-shell-stop-silent-cmd 1639,62155 +(defcustom proof-shell-silent-threshold 1648,62492 +(defcustom proof-shell-inform-file-processed-cmd 1656,62826 +(defcustom proof-shell-inform-file-retracted-cmd 1677,63749 +(defcustom proof-auto-multiple-files 1705,65020 +(defcustom proof-cannot-reopen-processed-files 1720,65741 +(defcustom proof-shell-require-command-regexp 1734,66408 +(defcustom proof-done-advancing-require-function 1745,66870 +(defcustom proof-shell-quiet-errors 1751,67110 +(defcustom proof-shell-prompt-pattern 1764,67444 +(defcustom proof-shell-wakeup-char 1774,67866 +(defcustom proof-shell-annotated-prompt-regexp 1780,68097 +(defcustom proof-shell-abort-goal-regexp 1796,68737 +(defcustom proof-shell-error-regexp 1801,68872 +(defcustom proof-shell-truncate-before-error 1821,69666 +(defcustom pg-next-error-regexp 1835,70209 +(defcustom pg-next-error-filename-regexp 1850,70819 +(defcustom pg-next-error-extract-filename 1874,71857 +(defcustom proof-shell-interrupt-regexp 1881,72100 +(defcustom proof-shell-proof-completed-regexp 1895,72692 +(defcustom proof-shell-clear-response-regexp 1908,73200 +(defcustom proof-shell-clear-goals-regexp 1915,73499 +(defcustom proof-shell-start-goals-regexp 1922,73792 +(defcustom proof-shell-end-goals-regexp 1930,74159 +(defcustom proof-shell-eager-annotation-start 1936,74401 +(defcustom proof-shell-eager-annotation-start-length 1954,75139 +(defcustom proof-shell-eager-annotation-end 1965,75566 +(defcustom proof-shell-assumption-regexp 1981,76242 +(defcustom proof-shell-process-file 1991,76657 +(defcustom proof-shell-retract-files-regexp 2013,77609 +(defcustom proof-shell-compute-new-files-list 2022,77945 +(defcustom pg-use-specials-for-fontify 2034,78490 +(defcustom pg-special-char-regexp 2042,78838 +(defcustom proof-shell-set-elisp-variable-regexp 2047,78982 +(defcustom proof-shell-match-pgip-cmd 2080,80454 +(defcustom proof-shell-issue-pgip-cmd 2089,80784 +(defcustom proof-shell-query-dependencies-cmd 2098,81140 +(defcustom proof-shell-theorem-dependency-list-regexp 2105,81400 +(defcustom proof-shell-theorem-dependency-list-split 2121,82060 +(defcustom proof-shell-show-dependency-cmd 2130,82485 +(defcustom proof-shell-identifier-under-mouse-cmd 2137,82754 +(defcustom proof-shell-trace-output-regexp 2160,83835 +(defcustom proof-shell-thms-output-regexp 2176,84379 +(defcustom proof-shell-unicode 2189,84765 +(defcustom proof-shell-filename-escapes 2197,85093 +(defcustom proof-shell-process-connection-type 2214,85773 +(defcustom proof-shell-strip-crs-from-input 2237,86820 +(defcustom proof-shell-strip-crs-from-output 2249,87309 +(defcustom proof-shell-insert-hook 2257,87677 +(defcustom proof-pre-shell-start-hook 2297,89641 +(defcustom proof-shell-handle-delayed-output-hook2313,90113 +(defcustom proof-shell-handle-error-or-interrupt-hook2319,90328 +(defcustom proof-shell-pre-interrupt-hook2337,91077 +(defcustom proof-shell-process-output-system-specific 2345,91349 +(defcustom proof-state-change-hook 2364,92214 +(defcustom proof-shell-font-lock-keywords 2375,92596 +(defcustom proof-shell-syntax-table-entries 2383,92924 +(defgroup proof-goals 2401,93296 +(defcustom pg-subterm-first-special-char 2406,93417 +(defcustom pg-subterm-anns-use-stack 2414,93729 +(defcustom pg-goals-change-goal 2423,94033 +(defcustom pbp-goal-command 2428,94148 +(defcustom pbp-hyp-command 2433,94304 +(defcustom pg-subterm-help-cmd 2438,94466 +(defcustom pg-goals-error-regexp 2445,94702 +(defcustom proof-shell-result-start 2450,94862 +(defcustom proof-shell-result-end 2456,95096 +(defcustom pg-subterm-start-char 2462,95309 +(defcustom pg-subterm-sep-char 2476,95891 +(defcustom pg-subterm-end-char 2482,96070 +(defcustom pg-topterm-regexp 2488,96227 +(defcustom proof-goals-font-lock-keywords 2505,96830 +(defcustom proof-resp-font-lock-keywords 2519,97509 +(defcustom pg-before-fontify-output-hook 2531,98087 +(defcustom pg-after-fontify-output-hook 2539,98447 +(defgroup proof-x-symbol 2551,98701 +(defcustom proof-xsym-extra-modes 2556,98829 +(defcustom proof-xsym-font-lock-keywords 2569,99458 +(defcustom proof-xsym-activate-command 2577,99835 +(defcustom proof-xsym-deactivate-command 2584,100071 +(defpgcustom x-symbol-language 2591,100313 +(defpgcustom favourites 2606,100760 +(defpgcustom menu-entries 2611,100950 +(defpgcustom help-menu-entries 2618,101187 +(defpgcustom keymap 2625,101450 +(defpgcustom completion-table 2630,101621 +(defpgcustom tags-program 2640,101986 +(defcustom proof-general-name 2652,102159 +(defcustom proof-general-home-page2657,102316 +(defcustom proof-unnamed-theorem-name2663,102475 +(defcustom proof-universal-keys2671,102751 generic/proof-depends.el,824 (defvar proof-thm-names-of-files 19,540 @@ -1837,104 +1836,104 @@ generic/proof-script.el,5105 (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 230,7988 -(defsubst proof-set-locked-endpoints 234,8129 -(defsubst proof-detach-queue 238,8273 -(defsubst proof-detach-locked 242,8405 -(defsubst proof-set-queue-start 246,8541 -(defsubst proof-set-locked-end 250,8667 -(defsubst proof-set-queue-end 265,9214 -(defun proof-init-segmentation 275,9470 -(defun proof-restart-buffers 307,10841 -(defun proof-script-buffers-with-spans 329,11763 -(defun proof-script-remove-all-spans-and-deactivate 339,12119 -(defun proof-script-clear-queue-spans 343,12307 -(defun proof-unprocessed-begin 361,12848 -(defun proof-script-end 369,13102 -(defun proof-queue-or-locked-end 378,13403 -(defun proof-locked-end 392,14066 -(defun proof-locked-region-full-p 408,14436 -(defun proof-locked-region-empty-p 416,14693 -(defun proof-only-whitespace-to-locked-region-p 420,14843 -(defun proof-in-locked-region-p 433,15479 -(defun proof-goto-end-of-locked 445,15742 -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 462,16501 -(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 473,16982 -(defun proof-end-of-locked-visible-p 487,17635 -(defun proof-goto-end-of-queue-or-locked-if-not-visible 496,18086 -(defvar pg-idioms 515,18736 -(defvar pg-visibility-specs 518,18832 -(deflocal pg-script-portions 523,19039 -(defun pg-clear-script-portions 526,19161 -(defun pg-add-script-element 544,19825 -(defun pg-remove-script-element 547,19901 -(defsubst pg-visname 555,20179 -(defun pg-add-element 559,20324 -(defun pg-open-invisible-span 593,21953 -(defun pg-remove-element 604,22316 -(defun pg-make-element-invisible 611,22586 -(defun pg-make-element-visible 617,22843 -(defun pg-toggle-element-visibility 622,23022 -(defun pg-redisplay-for-gnuemacs 630,23352 -(defun pg-show-all-portions 637,23623 -(defun pg-show-all-proofs 655,24294 -(defun pg-hide-all-proofs 660,24422 -(defun pg-add-proof-element 665,24553 -(defun pg-span-name 679,25173 -(defun pg-set-span-helphighlights 700,25880 -(defun proof-complete-buffer-atomic 725,26704 -(defun proof-register-possibly-new-processed-file 766,28619 -(defun proof-inform-prover-file-retracted 817,30747 -(defun proof-auto-retract-dependencies 836,31533 -(defun proof-unregister-buffer-file-name 890,34073 -(defun proof-protected-process-or-retract 936,35896 -(defun proof-deactivate-scripting-auto 963,37066 -(defun proof-deactivate-scripting 972,37424 -(defun proof-activate-scripting 1109,42829 -(defun proof-toggle-active-scripting 1237,48583 -(defun proof-done-advancing 1278,49944 -(defun proof-done-advancing-comment 1363,53350 -(defun proof-done-advancing-save 1382,54092 -(defun proof-make-goalsave 1475,57707 -(defun proof-get-name-from-goal 1490,58450 -(defun proof-done-advancing-autosave 1509,59476 -(defun proof-done-advancing-other 1574,62022 -(defun proof-segment-up-to-parser 1602,62981 -(defun proof-script-generic-parse-find-comment-end 1665,65057 -(defun proof-script-generic-parse-cmdend 1674,65473 -(defun proof-script-generic-parse-cmdstart 1699,66368 -(defun proof-script-generic-parse-sexp 1762,69076 -(defun proof-cmdstart-add-segment-for-cmd 1786,70012 -(defun proof-segment-up-to-cmdstart 1838,72211 -(defun proof-segment-up-to-cmdend 1899,74571 -(defun proof-semis-to-vanillas 1970,77218 -(defun proof-script-new-command-advance 2009,78544 -(defun proof-script-next-command-advance 2051,80285 -(defun proof-assert-until-point-interactive 2063,80726 -(defun proof-assert-until-point 2089,81848 -(defun proof-assert-next-command2142,84280 -(defun proof-goto-point 2190,86543 -(defun proof-insert-pbp-command 2207,87069 -(defun proof-done-retracting 2240,88182 -(defun proof-setup-retract-action 2267,89293 -(defun proof-last-goal-or-goalsave 2277,89776 -(defun proof-retract-target 2300,90616 -(defun proof-retract-until-point-interactive 2385,94257 -(defun proof-retract-until-point 2393,94642 -(define-derived-mode proof-mode 2438,96503 -(defun proof-script-set-visited-file-name 2472,97873 -(defun proof-script-set-buffer-hooks 2496,98875 -(defun proof-script-kill-buffer-fn 2506,99371 -(defun proof-config-done-related 2550,101193 -(defun proof-generic-goal-command-p 2622,103761 -(defun proof-generic-state-preserving-p 2627,103973 -(defun proof-generic-count-undos 2636,104490 -(defun proof-generic-find-and-forget 2665,105520 -(defconst proof-script-important-settings2716,107345 -(defun proof-config-done 2729,107882 -(defun proof-setup-parsing-mechanism 2826,111430 -(defun proof-setup-imenu 2870,113283 -(defun proof-setup-func-menu 2887,113888 +(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 540,19640 +(defun pg-remove-script-element 543,19716 +(defsubst pg-visname 551,19994 +(defun pg-add-element 555,20139 +(defun pg-open-invisible-span 589,21768 +(defun pg-remove-element 600,22131 +(defun pg-make-element-invisible 607,22401 +(defun pg-make-element-visible 613,22658 +(defun pg-toggle-element-visibility 618,22837 +(defun pg-redisplay-for-gnuemacs 626,23167 +(defun pg-show-all-portions 633,23438 +(defun pg-show-all-proofs 651,24109 +(defun pg-hide-all-proofs 656,24237 +(defun pg-add-proof-element 661,24368 +(defun pg-span-name 675,24988 +(defun pg-set-span-helphighlights 696,25695 +(defun proof-complete-buffer-atomic 721,26519 +(defun proof-register-possibly-new-processed-file 762,28434 +(defun proof-inform-prover-file-retracted 813,30562 +(defun proof-auto-retract-dependencies 832,31348 +(defun proof-unregister-buffer-file-name 886,33888 +(defun proof-protected-process-or-retract 932,35711 +(defun proof-deactivate-scripting-auto 959,36881 +(defun proof-deactivate-scripting 968,37239 +(defun proof-activate-scripting 1105,42644 +(defun proof-toggle-active-scripting 1233,48398 +(defun proof-done-advancing 1274,49759 +(defun proof-done-advancing-comment 1360,53126 +(defun proof-done-advancing-save 1379,53868 +(defun proof-make-goalsave 1472,57483 +(defun proof-get-name-from-goal 1487,58226 +(defun proof-done-advancing-autosave 1506,59252 +(defun proof-done-advancing-other 1571,61798 +(defun proof-segment-up-to-parser 1599,62757 +(defun proof-script-generic-parse-find-comment-end 1662,64833 +(defun proof-script-generic-parse-cmdend 1671,65249 +(defun proof-script-generic-parse-cmdstart 1696,66144 +(defun proof-script-generic-parse-sexp 1759,68852 +(defun proof-cmdstart-add-segment-for-cmd 1783,69788 +(defun proof-segment-up-to-cmdstart 1835,71987 +(defun proof-segment-up-to-cmdend 1896,74347 +(defun proof-semis-to-vanillas 1967,76994 +(defun proof-script-new-command-advance 2006,78320 +(defun proof-script-next-command-advance 2048,80061 +(defun proof-assert-until-point-interactive 2060,80502 +(defun proof-assert-until-point 2086,81624 +(defun proof-assert-next-command2139,84056 +(defun proof-goto-point 2187,86319 +(defun proof-insert-pbp-command 2204,86845 +(defun proof-done-retracting 2237,87958 +(defun proof-setup-retract-action 2264,89069 +(defun proof-last-goal-or-goalsave 2274,89552 +(defun proof-retract-target 2297,90392 +(defun proof-retract-until-point-interactive 2382,94033 +(defun proof-retract-until-point 2390,94418 +(define-derived-mode proof-mode 2435,96279 +(defun proof-script-set-visited-file-name 2469,97649 +(defun proof-script-set-buffer-hooks 2493,98651 +(defun proof-script-kill-buffer-fn 2503,99147 +(defun proof-config-done-related 2547,100969 +(defun proof-generic-goal-command-p 2619,103537 +(defun proof-generic-state-preserving-p 2624,103749 +(defun proof-generic-count-undos 2633,104266 +(defun proof-generic-find-and-forget 2662,105296 +(defconst proof-script-important-settings2713,107121 +(defun proof-config-done 2726,107658 +(defun proof-setup-parsing-mechanism 2823,111206 +(defun proof-setup-imenu 2867,113059 +(defun proof-setup-func-menu 2884,113664 generic/proof-shell.el,3337 (defvar proof-shell-last-output 19,457 @@ -1982,34 +1981,34 @@ generic/proof-shell.el,3337 (defun proof-shell-stop-silent-item 1066,40650 (defun proof-shell-should-be-silent 1073,40922 (defun proof-append-alist 1086,41478 -(defun proof-start-queue 1142,43605 -(defun proof-extend-queue 1153,43954 -(defun proof-shell-exec-loop 1164,44335 -(defun proof-shell-insert-loopback-cmd 1229,46923 -(defun proof-shell-message 1266,48631 -(defun proof-shell-process-urgent-message 1272,48847 -(defvar proof-shell-minibuffer-urgent-interactive-input-history 1481,57735 -(defun proof-shell-minibuffer-urgent-interactive-input 1483,57805 -(defun proof-shell-process-urgent-messages 1495,58175 -(defun proof-shell-filter 1567,61345 -(defun proof-shell-filter-process-output 1720,67682 -(defvar pg-last-tracing-output-time 1773,69736 -(defvar pg-tracing-slow-mode 1776,69842 -(defconst pg-slow-mode-duration 1779,69931 -(defconst pg-fast-tracing-mode-threshold 1782,70013 -(defvar pg-tracing-cleanup-timer 1785,70141 -(defun pg-tracing-tight-loop 1787,70180 -(defun pg-finish-tracing-display 1830,71898 -(defun proof-shell-dont-show-annotations 1843,72204 -(defun proof-shell-show-annotations 1859,72739 -(defun proof-shell-wait 1880,73236 -(defun proof-done-invisible 1900,74146 -(defun proof-shell-invisible-command 1943,75869 -(defun proof-shell-invisible-cmd-get-result 1976,77119 -(defun proof-shell-invisible-command-invisible-result 1993,77800 -(define-derived-mode proof-shell-mode 2013,78304 -(defconst proof-shell-important-settings2084,80975 -(defun proof-shell-config-done 2089,81075 +(defun proof-start-queue 1145,43715 +(defun proof-extend-queue 1156,44064 +(defun proof-shell-exec-loop 1167,44445 +(defun proof-shell-insert-loopback-cmd 1232,47033 +(defun proof-shell-message 1260,48359 +(defun proof-shell-process-urgent-message 1266,48575 +(defvar proof-shell-minibuffer-urgent-interactive-input-history 1475,57463 +(defun proof-shell-minibuffer-urgent-interactive-input 1477,57533 +(defun proof-shell-process-urgent-messages 1489,57903 +(defun proof-shell-filter 1561,61073 +(defun proof-shell-filter-process-output 1714,67410 +(defvar pg-last-tracing-output-time 1767,69464 +(defvar pg-tracing-slow-mode 1770,69570 +(defconst pg-slow-mode-duration 1773,69659 +(defconst pg-fast-tracing-mode-threshold 1776,69741 +(defvar pg-tracing-cleanup-timer 1779,69869 +(defun pg-tracing-tight-loop 1781,69908 +(defun pg-finish-tracing-display 1824,71626 +(defun proof-shell-dont-show-annotations 1837,71932 +(defun proof-shell-show-annotations 1853,72467 +(defun proof-shell-wait 1874,72964 +(defun proof-done-invisible 1894,73874 +(defun proof-shell-invisible-command 1937,75597 +(defun proof-shell-invisible-cmd-get-result 1970,76847 +(defun proof-shell-invisible-command-invisible-result 1987,77528 +(define-derived-mode proof-shell-mode 2007,78032 +(defconst proof-shell-important-settings2078,80703 +(defun proof-shell-config-done 2083,80803 generic/proof-site.el,720 (defgroup proof-general 20,594 @@ -2034,20 +2033,20 @@ 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,1979 -(defconst proof-splash-welcome 67,2358 -(defun proof-get-image 86,2922 -(defvar proof-splash-timeout-conf 141,4773 -(defun proof-splash-centre-spaces 144,4886 -(defun proof-splash-remove-screen 172,6055 -(defun proof-splash-remove-buffer 193,6804 -(defvar proof-splash-seen 209,7468 -(defun proof-splash-display-screen 213,7585 -(defun proof-splash-message 288,10744 -(defun proof-splash-timeout-waiter 298,11107 -(defvar proof-splash-old-frame-title-format 315,11846 -(defun proof-splash-set-frame-titles 317,11896 -(defun proof-splash-unset-frame-titles 326,12212 +(defconst proof-splash-startup-msg 58,1986 +(defconst proof-splash-welcome 67,2365 +(defun proof-get-image 86,2929 +(defvar proof-splash-timeout-conf 141,4780 +(defun proof-splash-centre-spaces 144,4893 +(defun proof-splash-remove-screen 172,6062 +(defun proof-splash-remove-buffer 193,6811 +(defvar proof-splash-seen 209,7475 +(defun proof-splash-display-screen 213,7592 +(defun proof-splash-message 288,10751 +(defun proof-splash-timeout-waiter 298,11114 +(defvar proof-splash-old-frame-title-format 315,11853 +(defun proof-splash-set-frame-titles 317,11903 +(defun proof-splash-unset-frame-titles 326,12219 generic/proof-syntax.el,972 (defun proof-ids-to-regexp 16,445 @@ -2183,13 +2182,13 @@ generic/proof-utils.el,2099 (defun proof-deftoggle-fn 809,30923 (defmacro proof-deftoggle 824,31578 (defun proof-defintset-fn 831,31952 -(defmacro proof-defintset 845,32607 -(defun proof-defstringset-fn 852,32984 -(defmacro proof-defstringset 865,33611 -(defun pg-custom-save-vars 879,34076 -(defun pg-custom-reset-vars 897,34802 -(defun proof-locate-executable 910,35139 -(defconst proof-extra-fls939,36320 +(defmacro proof-defintset 847,32660 +(defun proof-defstringset-fn 854,33037 +(defmacro proof-defstringset 867,33664 +(defun pg-custom-save-vars 881,34129 +(defun pg-custom-reset-vars 899,34855 +(defun proof-locate-executable 912,35192 +(defconst proof-extra-fls941,36373 generic/proof-x-symbol.el,613 (defvar proof-x-symbol-initialized 54,2151 @@ -2297,17 +2296,16 @@ lib/holes.el,2447 (defvar holes-mode 862,26942 (defun holes-mode 868,27138 -lib/local-vars-list.el,410 +lib/local-vars-list.el,372 (defconst local-vars-list-doc 25,759 -(defun local-vars-list-help 38,1213 -(defun local-vars-list-insert-empty-zone 43,1399 -(defun local-vars-list-find 81,2107 -(defun local-vars-list-goto-var 100,2882 -(defun local-vars-list-get-current 126,3932 -(defun local-vars-list-set-current 147,4782 -(defun local-vars-list-get 170,5499 -(defun local-vars-list-get-safe 187,6031 -(defun local-vars-list-set 192,6225 +(defun local-vars-list-insert-empty-zone 41,1323 +(defun local-vars-list-find 79,2031 +(defun local-vars-list-goto-var 98,2806 +(defun local-vars-list-get-current 124,3856 +(defun local-vars-list-set-current 145,4706 +(defun local-vars-list-get 168,5423 +(defun local-vars-list-get-safe 185,5955 +(defun local-vars-list-set 190,6149 lib/proof-compat.el,1002 (defvar proof-running-on-XEmacs 24,760 @@ -2761,6 +2759,747 @@ mmm/mmm-vars.el,2667 (defun mmm-mode-ext-applies 1023,38161 (defun mmm-get-all-classes 1037,38645 +x-symbol/lisp/auto-autoloads.el,63 +(defalias 'x-symbol-map-autoload x-symbol-map-autoload23,974 + +x-symbol/lisp/x-symbol-bib.el,549 +(defcustom x-symbol-bib-auto-style 42,1544 +(defcustom x-symbol-bib-modeline-name 49,1800 +(defcustom x-symbol-bib-header-groups-alist 55,1979 +(defcustom x-symbol-bib-electric-ignore 62,2268 +(defcustom x-symbol-bib-class-alist 69,2558 +(defcustom x-symbol-bib-class-face-alist 76,2824 +(defvar x-symbol-bib-token-grammar89,3308 +(defvar x-symbol-bib-required-fonts 99,3784 +(defvar x-symbol-bib-user-table 103,3960 +(defvar x-symbol-bib-table106,4064 +(defvar x-symbol-bib-generated-data 113,4390 +(defun x-symbol-bib-default-token-list 117,4529 + +x-symbol/lisp/x-symbol.el,9173 +(defvar x-symbol-trace-invisible 51,1979 +(defconst x-symbol-language-access-alist66,2494 +(defstruct (x-symbol-generated178,8375 +(defstruct (x-symbol-grammar189,8587 +(defvar x-symbol-map 212,9415 +(defvar x-symbol-unalias-alist 216,9542 +(defvar x-symbol-latin-decode-alists 220,9659 +(defvar x-symbol-context-atree 224,9844 +(defvar x-symbol-electric-atree 228,9959 +(defvar x-symbol-grid-alist 231,10053 +(defvar x-symbol-menu-alist 234,10136 +(defvar x-symbol-all-charsyms 237,10243 +(defvar x-symbol-fancy-value-cache 242,10451 +(defvar x-symbol-fchar-tables 246,10614 +(defvar x-symbol-bchar-tables 249,10743 +(defvar x-symbol-cstring-table 251,10779 +(defvar x-symbol-fontified-cstring-table 253,10816 +(defvar x-symbol-charsym-decode-obarray 255,10863 +(defun x-symbol-set-variable 262,11092 +(defun x-symbol-ensure-hashtable 276,11727 +(defun x-symbol-puthash 283,12029 +(defun x-symbol-call-function-or-regexp 291,12358 +(defun x-symbol-match-in-alist 300,12758 +(defun x-symbol-fancy-string 329,13982 +(defun x-symbol-fancy-value 351,14899 +(defun x-symbol-fancy-associations 370,15666 +(defun x-symbol-language-value 399,16818 +(defun x-symbol-charsym-face 413,17476 +(defun x-symbol-image-available-p 426,18103 +(defun x-symbol-default-context-info-ignore 431,18315 +(defun x-symbol-default-info-keys-keymaps 445,19082 +(defun x-symbol-alias-charsym 457,19557 +(defun x-symbol-default-valid-charsym 466,19926 +(defun x-symbol-next-valid-charsym 488,20963 +(defun x-symbol-valid-context-charsym 515,21970 +(defun x-symbol-next-valid-charsym-before 526,22569 +(defun x-symbol-prefix-arg-texts 550,23626 +(defun x-symbol-region-text 559,23921 +(defun x-symbol-language-text 568,24217 +(defun x-symbol-coding-text 576,24617 +(defun x-symbol-language-modeline-text 594,25312 +(defun x-symbol-coding-modeline-text 600,25548 +(defun x-symbol-translate-to-ascii 646,27453 +(defun x-symbol-package-web 680,28718 +(defun x-symbol-package-info 687,28939 +(defun x-symbol-package-bug 693,29100 +(defun x-symbol-package-reply-to-report 744,31073 +(defvar x-symbol-encode-rchars 764,31801 +(defun x-symbol-even-escapes-before-p 772,32083 +(defun x-symbol-decode-region 780,32262 +(defun x-symbol-decode-all 793,32735 +(defun x-symbol-decode-single-token 856,35803 +(defun x-symbol-decode-lisp 865,36110 +(defun x-symbol-encode-string 897,37577 +(defun x-symbol-encode-all 908,37896 +(defun x-symbol-encode-lisp 970,40852 +(defun x-symbol-decode-recode 1006,42257 +(defun x-symbol-decode 1036,43633 +(defun x-symbol-encode-recode 1049,44224 +(defun x-symbol-encode 1077,45500 +(defun x-symbol-unalias 1093,46259 +(defun x-symbol-copy-region-encoded 1158,49178 +(defun x-symbol-yank-decoded 1186,50428 +(defun x-symbol-update-modeline 1213,51528 +(defun x-symbol-auto-coding-alist 1237,52383 +(defun x-symbol-auto-8bit-search 1273,53544 +(defvar x-symbol-font-family-postfixes1298,54334 +(defvar x-symbol-font-lock-property-alist1301,54450 +(defvar x-symbol-font-lock-keywords1305,54631 +(defvar x-symbol-subscript-matcher 1332,55626 +(defvar x-symbol-subscript-type 1336,55729 +(defun x-symbol-subscripts-available-p 1339,55780 +(defun x-symbol-font-lock-start 1345,56021 +(defun x-symbol-match-subscript 1354,56407 +(defun x-symbol-init-font-lock 1360,56620 +(defun x-symbol-set-image 1392,58208 +(defun x-symbol-mode-internal 1410,58954 +(defun nuke-x-symbol 1484,62057 +(defun x-symbol-options-filter 1497,62510 +(defun x-symbol-extra-filter 1533,63666 +(defun x-symbol-menu-filter 1541,63914 +(defvar x-symbol-list-mode-map1568,64751 +(defvar x-symbol-list-buffer 1594,65901 +(defvar x-symbol-list-win-config 1596,65977 +(defvar x-symbol-invisible-spec 1598,66088 +(defvar x-symbol-itimer 1602,66238 +(defvar x-symbol-invisible-display-table1605,66321 +(defvar x-symbol-invisible-font 1614,66557 +(defvar x-symbol-charsym-info-cache 1638,67675 +(defvar x-symbol-language-info-caches 1640,67766 +(defvar x-symbol-coding-info-cache 1642,67860 +(defvar x-symbol-keys-info-cache 1644,67949 +(defun x-symbol-list-bury 1652,68254 +(defun x-symbol-list-restore 1658,68450 +(defun x-symbol-list-store 1688,69668 +(defun x-symbol-list-mode 1697,70085 +(defun x-symbol-list-scroll 1718,70887 +(defun x-symbol-init-language-interactive 1741,71529 +(defun x-symbol-list-menu 1758,72243 +(defun x-symbol-list-selected 1813,74151 +(defun x-symbol-list-menu-selected 1839,75360 +(defun x-symbol-list-mouse-selected 1850,75813 +(defun x-symbol-charsym-info 1867,76535 +(defun x-symbol-language-info 1881,77136 +(defun x-symbol-coding-info 1913,78336 +(defun x-symbol-keys-info 1933,79108 +(defun x-symbol-info 1957,80031 +(defun x-symbol-list-info 1970,80569 +(defun x-symbol-highlight-echo 1984,81112 +(defun x-symbol-point-info 1995,81661 +(defun x-symbol-hide-revealed-at-point 2041,83583 +(defun x-symbol-reveal-invisible 2078,85250 +(defun x-symbol-show-info-and-invisible 2126,87442 +(defun x-symbol-start-itimer-once 2162,88984 +(defun x-symbol-setup-minibuffer 2178,89610 +(defvar x-symbol-language-history 2196,90181 +(defvar x-symbol-token-history 2199,90305 +(defvar x-symbol-last-abbrev 2202,90381 +(defvar x-symbol-electric-pos 2204,90477 +(defvar x-symbol-command-keys 2207,90559 +(defvar x-symbol-help-keys 2211,90690 +(defvar x-symbol-help-language 2213,90785 +(defvar x-symbol-help-completions 2215,90884 +(defvar x-symbol-help-completions1 2217,90976 +(defun x-symbol-map-default-binding 2225,91252 +(defun x-symbol-read-charsym-token 2256,92330 +(defun x-symbol-insert-command 2282,93253 +(defun x-symbol-read-language 2333,95260 +(defun x-symbol-read-token 2348,95938 +(defun x-symbol-read-token-direct 2387,97447 +(defun x-symbol-grid 2399,97847 +(defun x-symbol-replace-from 2487,101463 +(defvar x-symbol-token-search-prelude-size 2523,102964 +(defun x-symbol-replace-token 2525,103012 +(defun x-symbol-match-token-before 2550,104103 +(defun x-symbol-token-input 2594,105906 +(defun x-symbol-modify-key 2615,106736 +(defun x-symbol-rotate-key 2648,108065 +(defun x-symbol-electric-input 2702,110275 +(defun x-symbol-help-mapper 2744,111976 +(defun x-symbol-help-output 2767,112815 +(defun x-symbol-help 2810,114411 +(defvar x-symbol-face-docstrings2863,116480 +(defvar x-symbol-all-key-prefixes 2869,116668 +(defvar x-symbol-all-key-chain-alist 2871,116779 +(defvar x-symbol-all-horizontal-chain-alist 2873,116878 +(defvar x-symbol-all-chain-subchains-alist 2875,116991 +(defvar x-symbol-all-exclusive-context-alist 2877,117105 +(defalias 'x-symbol-table-grouping x-symbol-table-grouping2885,117401 +(defalias 'x-symbol-table-aspects x-symbol-table-aspects2886,117442 +(defalias 'x-symbol-table-score x-symbol-table-score2887,117483 +(defalias 'x-symbol-table-input x-symbol-table-input2888,117523 +(defsubst x-symbol-table-prefixes 2889,117564 +(defsubst x-symbol-table-junk 2890,117615 +(defsubst x-symbol-charsym-defined-p 2892,117666 +(defun x-symbol-try-font-name-0 2900,117967 +(defun x-symbol-try-font-name 2918,118523 +(defun x-symbol-set-cstrings 2935,119039 +(defun x-symbol-init-charsym-command 2980,121017 +(defun x-symbol-init-charsym-input 2988,121383 +(defun x-symbol-init-charsym-aspects 3057,124101 +(defun x-symbol-init-cset 3087,125381 +(defun x-symbol-make-atree 3237,132204 +(defun x-symbol-atree-push 3241,132284 +(defun x-symbol-component-root-p 3261,132973 +(defun x-symbol-component-elements 3265,133112 +(defun x-symbol-component-merge 3272,133360 +(defun x-symbol-component-space 3286,133908 +(defun x-symbol-modify-less-than 3300,134492 +(defun x-symbol-inherit-aspects 3305,134715 +(defun x-symbol-compute-aspects 3314,135154 +(defun x-symbol-init-aspects 3330,135872 +(defun x-symbol-sort-modify-chain 3375,137921 +(defun x-symbol-init-horizontal/key-alist 3390,138493 +(defun x-symbol-init-exclusive-alist 3406,139239 +(defun x-symbol-init-horizontal-chain 3444,140843 +(defun x-symbol-init-exclusive-chain 3452,141175 +(defun x-symbol-init-rotate-chain 3459,141502 +(defun x-symbol-init-context-atree 3480,142376 +(defun x-symbol-init-key-bindings 3525,144659 +(defun x-symbol-rotate-modify-less-than 3548,145582 +(defun x-symbol-subgroup-less-than 3556,145977 +(defun x-symbol-header-charsyms 3561,146234 +(defun x-symbol-init-grid/menu 3587,147284 +(defun x-symbol-init-input 3658,149884 +(defun x-symbol-init-latin-decoding 3788,156360 +(defun x-symbol-get-prime-for 3829,158231 +(defun x-symbol-alist-to-obarray 3838,158555 +(defun x-symbol-alist-to-hash-table 3844,158763 +(defun x-symbol-init-language 3854,159096 +(defvar x-symbol-latin1-cset3978,164561 +(defvar x-symbol-latin2-cset3984,164734 +(defvar x-symbol-latin3-cset3990,164907 +(defvar x-symbol-latin5-cset3996,165080 +(defvar x-symbol-latin9-cset4002,165252 +(defvar x-symbol-xsymb0-cset4008,165458 +(defvar x-symbol-xsymb1-cset4014,165713 +(defvar x-symbol-latin1-table4020,165955 +(defvar x-symbol-latin2-table4121,170425 +(defvar x-symbol-latin3-table4220,173626 +(defvar x-symbol-latin5-table4319,176507 +(defvar x-symbol-latin9-table4418,178817 +(defvar x-symbol-xsymb0-table4517,181207 +(defvar x-symbol-xsymb1-table4667,188603 +(defvar x-symbol-no-of-charsyms 4875,199238 +(defun x-symbol-mac-setup1 4883,199604 +(defun x-symbol-mac-setup2 4909,200513 + +x-symbol/lisp/x-symbol-emacs.el,1125 +(defun emacs-version>=34,1341 +(defvar x-symbol-emacs-has-font-lock-with-props68,3002 +(defvar x-symbol-emacs-has-correct-find-safe-coding81,3494 +(defvar x-symbol-emacs-after-create-image-function96,4008 +(defvar image-types 122,4865 +(defvar init-file-loaded 158,6252 +(defvar message-stack 161,6325 +(defun region-active-p 244,9635 +(defvar x-symbol-data-directory 281,11000 +(defun x-symbol-directory-files 351,13277 +(defun x-symbol-event-in-current-buffer 365,13665 +(defun x-symbol-create-image 368,13714 +(defun x-symbol-make-glyph 371,13799 +(defun x-symbol-set-glyph-image 374,13870 +(defvar x-symbol-heading-strut-glyph 389,14367 +(defvar x-symbol-invisible-face 392,14454 +(defvar x-symbol-face 393,14512 +(defvar x-symbol-sub-face 394,14550 +(defvar x-symbol-sup-face 395,14596 +(defvar x-symbol-emacs-w32-font-directories397,14643 +(defvar x-symbol-invisible-display-table 410,15121 +(defalias 'x-symbol-window-width x-symbol-window-width412,15168 +(defun x-symbol-set-face-font 414,15217 +(defun x-symbol-event-matches-key-specifier-p 425,15690 +(defun start-itimer 435,15962 +(defun itimer-live-p 437,16059 + +x-symbol/lisp/x-symbol-hooks.el,3109 +(defvar x-symbol-warn-of-old-emacs 66,2522 +(defvar x-symbol-data-directory81,3030 +(defvar x-symbol-font-directory87,3246 +(defun x-symbol-define-user-options 98,3661 +(defun x-symbol-auto-mode-suffixes 126,5060 +(defcustom x-symbol-initialize 143,5652 +(defvar x-symbol-orig-comint-input-sender 177,7219 +(defun x-symbol-coding-system-from-locale 185,7531 +(defun x-symbol-buffer-coding 223,9137 +(defvar x-symbol-default-coding279,11196 +(defcustom x-symbol-compose-key 325,13040 +(defcustom x-symbol-auto-key-autoload 332,13308 +(defvar x-symbol-auto-conversion-method 340,13623 +(defvar x-symbol-language-alist 361,14586 +(defcustom x-symbol-charsym-name 370,14923 +(defcustom x-symbol-tex-name 378,15273 +(defcustom x-symbol-tex-modes384,15440 +(defcustom x-symbol-sgml-name 392,15708 +(defcustom x-symbol-sgml-modes398,15880 +(defcustom x-symbol-bib-name 407,16207 +(defcustom x-symbol-bib-modes 413,16377 +(defcustom x-symbol-texi-name 420,16603 +(defcustom x-symbol-texi-modes 426,16779 +(defvar x-symbol-mode 438,17188 +(defvar x-symbol-language 445,17415 +(defvar x-symbol-coding 460,18103 +(defvar x-symbol-8bits 487,19379 +(defvar x-symbol-unique 502,19965 +(defvar x-symbol-subscripts 517,20547 +(defvar x-symbol-image 530,21112 +(defcustom x-symbol-auto-mode-suffixes 547,21754 +(defcustom x-symbol-auto-8bit-search-limit 556,22179 +(defcustom x-symbol-auto-style-alist 563,22461 +(defvar x-symbol-mode-disable-alist 609,24419 +(defun x-symbol-image-set-colormap 617,24694 +(defcustom x-symbol-image-colormap-allocation 635,25402 +(defcustom x-symbol-image-convert-colormap646,25858 +(defalias 'x-symbol-cset-registry x-symbol-cset-registry665,26545 +(defalias 'x-symbol-cset-coding x-symbol-cset-coding666,26587 +(defalias 'x-symbol-cset-leading x-symbol-cset-leading667,26627 +(defalias 'x-symbol-cset-score x-symbol-cset-score668,26668 +(defalias 'x-symbol-cset-left x-symbol-cset-left669,26708 +(defalias 'x-symbol-cset-right x-symbol-cset-right670,26745 +(defvar x-symbol-input-initialized 672,26784 +(defun x-symbol-key-autoload 681,27080 +(defalias 'x-symbol-map-autoload x-symbol-map-autoload703,28055 +(defun x-symbol-buffer-file-name 710,28304 +(defun x-symbol-auto-set-variable 723,28776 +(defun x-symbol-mode 729,28994 +(defun turn-on-x-symbol-conditionally 860,34373 +(defun x-symbol-fontify 868,34663 +(defun x-symbol-comint-output-filter 896,35787 +(defun x-symbol-comint-send 905,36149 +(defun x-symbol-format-decode 921,36806 +(defun x-symbol-format-encode 943,37724 +(defun x-symbol-after-insert-file 958,38250 +(defun x-symbol-write-region-annotate-function 995,40092 +(defun x-symbol-write-file-hook 1015,41096 +(defvar x-symbol-modeline-string 1076,43560 +(defvar x-symbol-mode-map1081,43775 +(defconst x-symbol-early-language-access-alist1090,44065 +(defun x-symbol-init-language-accesses 1095,44274 +(defun x-symbol-register-language 1126,45445 +(defun x-symbol-initialize 1146,46317 +(defun x-symbol-after-init 1248,51435 +(defun x-symbol-inherit-from-buffer 1306,54270 +(defun x-symbol-auctex-math-insert 1339,55750 +(defun x-symbol-turn-on-bib-cite 1348,56068 + +x-symbol/lisp/x-symbol-image.el,1980 +(defvar x-symbol-image-process-buffer 48,1782 +(defvar x-symbol-image-process-name 51,1893 +(defvar x-symbol-image-highlight-map54,1992 +(defun x-symbol-image-try-special 73,2736 +(defvar x-symbol-image-broken-image82,3092 +(defvar x-symbol-image-create-image87,3298 +(defvar x-symbol-image-design-glyph92,3528 +(defvar x-symbol-image-locked-glyph98,3773 +(defvar x-symbol-image-remote-glyph104,4005 +(defvar x-symbol-image-junk-glyph110,4240 +(defvar x-symbol-image-buffer-extents 116,4471 +(defvar x-symbol-image-memory-cache 121,4705 +(defvar x-symbol-image-all-recursive-dirs 131,5181 +(defvar x-symbol-image-all-dirs 133,5289 +(defun x-symbol-image-parse-buffer 142,5583 +(defun x-symbol-image-after-change-function 184,7740 +(defun x-symbol-image-delete-extents 201,8322 +(defun x-symbol-image-parse-region 230,9501 +(defun x-symbol-image-default-file-name 313,12935 +(defun x-symbol-image-init-memory-cache 329,13656 +(defun x-symbol-image-init-memory-cache-1 359,14931 +(defun x-symbol-image-searchpath 371,15428 +(defun x-symbol-image-searchpath-1 399,16532 +(defun x-symbol-image-mouse-editor 425,17580 +(defun x-symbol-image-editor 433,17814 +(defun x-symbol-image-highlight-menu 462,18897 +(defun x-symbol-image-help-echo 471,19252 +(defun x-symbol-image-file-name 486,19870 +(defun x-symbol-image-event-file 502,20552 +(defun x-symbol-image-active-file 513,20947 +(defvar x-symbol-image-process-stack 569,22856 +(defvar x-symbol-image-process-elem 573,23024 +(defun x-symbol-image-create-glyph 587,23677 +(defun x-symbol-image-cache-name 645,25868 +(defun x-symbol-image-process-stack 670,26998 +(defun x-symbol-image-convert-file 683,27562 +(defun x-symbol-image-start-convert-mono 691,27895 +(defun x-symbol-image-start-convert-color 702,28375 +(defun x-symbol-image-start-convert-truecolor 713,28866 +(defun x-symbol-image-start-convert-mswindows 723,29317 +(defun x-symbol-image-start-convert-colormap 738,29917 +(defun x-symbol-image-process-sentinel 755,30778 + +x-symbol/lisp/x-symbol-macs.el,569 +(defmacro x-symbol-ignore-property-changes 43,1617 +(defun x-symbol-set/push-assq/assoc 62,2278 +(defmacro x-symbol-set-assq 76,2819 +(defmacro x-symbol-set-assoc 82,3057 +(defmacro x-symbol-push-assq 88,3300 +(defmacro x-symbol-push-assoc 95,3618 +(defmacro x-symbol-dolist-delaying 107,4113 +(defmacro x-symbol-do-plist 148,5816 +(defmacro x-symbol-while-charsym 168,6560 +(defmacro x-symbol-encode-for-charsym 190,7309 +(defmacro x-symbol-decode-for-charsym 220,8473 +(defmacro x-symbol-decode-unique-test 245,9292 +(defmacro x-symbol-set-buffer-multibyte 251,9467 + +x-symbol/lisp/x-symbol-mule.el,1507 +(defvar x-symbol-mule-default-charset48,2000 +(defalias 'x-symbol-make-cset x-symbol-make-cset71,2912 +(defalias 'x-symbol-make-char x-symbol-make-char72,2968 +(defalias 'x-symbol-init-charsym-syntax x-symbol-init-charsym-syntax73,3024 +(defalias 'x-symbol-charsym-after x-symbol-charsym-after74,3100 +(defalias 'x-symbol-string-to-charsyms x-symbol-string-to-charsyms75,3164 +(defalias 'x-symbol-match-before x-symbol-match-before76,3238 +(defalias 'x-symbol-encode-lisp x-symbol-encode-lisp77,3300 +(defalias 'x-symbol-pre-command-hook x-symbol-pre-command-hook78,3360 +(defalias 'x-symbol-post-command-hook x-symbol-post-command-hook79,3430 +(defalias 'x-symbol-encode-charsym-after x-symbol-encode-charsym-after80,3502 +(defalias 'x-symbol-init-quail-bindings x-symbol-init-quail-bindings81,3580 +(defvar x-symbol-mule-char-table 83,3657 +(defvar x-symbol-mule-pre-command 85,3738 +(defun x-symbol-mule-make-charset 93,4009 +(defvar x-symbol-mule-default-font 107,4558 +(defun x-symbol-mule-default-font 109,4599 +(defun x-symbol-mule-make-cset 128,5509 +(defun x-symbol-mule-make-char 179,7564 +(defun x-symbol-mule-init-charsym-syntax 209,8700 +(defun x-symbol-mule-init-quail-bindings 225,9330 +(defun x-symbol-mule-encode-charsym-after 244,10054 +(defun x-symbol-mule-charsym-after 248,10159 +(defun x-symbol-mule-string-to-charsyms 257,10570 +(defun x-symbol-mule-match-before 270,11056 +(defun x-symbol-mule-pre-command-hook 294,12046 +(defun x-symbol-mule-post-command-hook 303,12449 + +x-symbol/lisp/x-symbol-nomule.el,1954 +(defalias 'x-symbol-make-cset x-symbol-make-cset46,1779 +(defalias 'x-symbol-make-char x-symbol-make-char47,1837 +(defalias 'x-symbol-init-charsym-syntax x-symbol-init-charsym-syntax48,1895 +(defalias 'x-symbol-charsym-after x-symbol-charsym-after49,1944 +(defalias 'x-symbol-string-to-charsyms x-symbol-string-to-charsyms50,2010 +(defalias 'x-symbol-match-before x-symbol-match-before51,2086 +(defalias 'x-symbol-encode-lisp x-symbol-encode-lisp52,2150 +(defalias 'x-symbol-pre-command-hook x-symbol-pre-command-hook53,2212 +(defalias 'x-symbol-post-command-hook x-symbol-post-command-hook54,2284 +(defalias 'x-symbol-encode-charsym-after x-symbol-encode-charsym-after55,2358 +(defalias 'x-symbol-init-quail-bindings x-symbol-init-quail-bindings56,2438 +(defvar x-symbol-nomule-mouse-yank-function 58,2488 +(defvar x-symbol-nomule-mouse-track-function61,2629 +(defvar x-symbol-nomule-cstring-regexp 66,2867 +(defvar x-symbol-nomule-char-table 71,3128 +(defvar x-symbol-nomule-pre-command 73,3211 +(defvar x-symbol-nomule-leading-faces-alist 76,3309 +(defvar x-symbol-nomule-font-lock-face 79,3482 +(defvar x-symbol-nomule-display-table82,3583 +(defvar x-symbol-nomule-character-quote-syntax 93,3945 +(defun x-symbol-nomule-init-faces 101,4248 +(defun x-symbol-nomule-make-cset 124,5108 +(defun x-symbol-nomule-make-char 150,6186 +(defun x-symbol-nomule-multibyte-char-p 180,7511 +(defun x-symbol-nomule-encode-charsym-after 185,7749 +(defun x-symbol-nomule-charsym-after 197,8147 +(defun x-symbol-nomule-string-to-charsyms 220,9090 +(defun x-symbol-nomule-match-before 236,9730 +(defun x-symbol-nomule-goto-leading-char 269,11142 +(defun x-symbol-nomule-mouse-yank-function 275,11371 +(defun x-symbol-nomule-mouse-track-function 282,11690 +(defun x-symbol-nomule-pre-command-hook 299,12476 +(defun x-symbol-nomule-post-command-hook 313,13109 +(defun x-symbol-nomule-match-cstring 351,14756 +(defun x-symbol-nomule-fontify-cstrings 369,15504 + +x-symbol/lisp/x-symbol-sgml.el,1521 +(defcustom x-symbol-sgml-auto-style41,1525 +(defcustom x-symbol-sgml-auto-coding-alist52,1947 +(defface x-symbol-sgml-symbol-face71,2757 +(defface x-symbol-sgml-noname-face79,3038 +(defcustom x-symbol-sgml-modeline-name 87,3301 +(defcustom x-symbol-sgml-header-groups-alist93,3484 +(defcustom x-symbol-sgml-class-alist113,4257 +(defcustom x-symbol-sgml-class-face-alist124,4674 +(defcustom x-symbol-sgml-electric-ignore 134,5097 +(defvar x-symbol-sgml-token-list 141,5365 +(defvar x-symbol-sgml-token-grammar156,6077 +(defvar x-symbol-sgml-user-table 163,6317 +(defvar x-symbol-sgml-generated-data 166,6426 +(defcustom x-symbol-sgml-master-directory 175,6746 +(defcustom x-symbol-sgml-image-searchpath 182,6973 +(defcustom x-symbol-sgml-image-cached-dirs 189,7223 +(defcustom x-symbol-sgml-image-file-truename-alist196,7489 +(defcustom x-symbol-sgml-image-keywords226,8698 +(defun x-symbol-sgml-image-file-truename 236,9078 +(defcustom x-symbol-sgml-subscript-matcher 250,9639 +(defcustom x-symbol-sgml-font-lock-regexp 256,9875 +(defcustom x-symbol-sgml-font-lock-limit-regexp 262,10079 +(defcustom x-symbol-sgml-font-lock-contents-regexp 269,10350 +(defcustom x-symbol-sgml-font-lock-alist276,10605 +(defun x-symbol-sgml-default-token-list 292,11264 +(defvar x-symbol-sgml-latin1-table310,12052 +(defvar x-symbol-sgml-latinN-table409,15286 +(defvar x-symbol-sgml-xsymb0-table495,17715 +(defvar x-symbol-sgml-xsymb1-table601,21570 +(defvar x-symbol-sgml-table640,23549 +(defun x-symbol-sgml-subscript-matcher 657,24155 + +x-symbol/lisp/x-symbol-tex.el,2359 +(defcustom x-symbol-tex-auto-style55,1896 +(defcustom x-symbol-tex-auto-coding-alist70,2510 +(defcustom x-symbol-tex-coding-master 87,3158 +(defcustom x-symbol-tex-modeline-name 99,3626 +(defcustom x-symbol-tex-header-groups-alist 105,3805 +(defcustom x-symbol-tex-electric-ignore 112,4065 +(defcustom x-symbol-tex-electric-ignore-regexp 119,4364 +(defcustom x-symbol-tex-token-suppress-space 126,4653 +(defvar x-symbol-tex-extra-menu-items135,5045 +(defvar x-symbol-tex-token-grammar145,5474 +(defvar x-symbol-tex-verb-delimiter-regexp 160,6263 +(defvar x-symbol-tex-env-verbatim-regexp 164,6456 +(defvar x-symbol-tex-env-tabbing-regexp 168,6637 +(defvar x-symbol-tex-user-table 172,6812 +(defvar x-symbol-tex-generated-data 175,6916 +(defcustom x-symbol-tex-master-directory 184,7234 +(defcustom x-symbol-tex-image-searchpath191,7518 +(defcustom x-symbol-tex-image-cached-dirs 209,8205 +(defcustom x-symbol-tex-image-keywords216,8458 +(defcustom x-symbol-tex-subscript-matcher 234,9311 +(defcustom x-symbol-tex-invisible-braces 240,9543 +(defcustom x-symbol-tex-font-lock-allowed-faces245,9639 +(defvar x-symbol-tex-font-lock-regexp256,10183 +(defvar x-symbol-tex-font-lock-limit-regexp 261,10425 +(defface x-symbol-tex-math-face270,10764 +(defface x-symbol-tex-text-face278,11034 +(defcustom x-symbol-tex-class-alist286,11306 +(defcustom x-symbol-tex-class-face-alist320,12867 +(defun x-symbol-tex-auto-coding-alist 336,13456 +(defun x-symbol-tex-default-master-directory 360,14702 +(defun x-symbol-tex-default-electric-ignore 368,15088 +(defun x-symbol-tex-default-token-list 390,16097 +(defun x-symbol-tex-after-init-language 400,16459 +(defvar x-symbol-tex-required-fonts 419,17293 +(defvar x-symbol-tex-latin1-table423,17445 +(defvar x-symbol-tex-latinN-table522,21630 +(defvar x-symbol-tex-xsymb0-table611,25318 +(defvar x-symbol-tex-xsymb1-table726,29931 +(defvar x-symbol-tex-table886,37347 +(defun x-symbol-tex-subscript-matcher 903,37904 +(defun x-symbol-tex-encode 951,39573 +(defun x-symbol-tex-decode 972,40387 +(defun x-symbol-tex-token-input 1047,43403 +(defun x-symbol-tex-translate-locations 1063,43971 +(defun x-symbol-tex-error-location 1119,45896 +(defun x-symbol-tex-preview-locations 1149,46926 +(defun x-symbol-tex-xdecode-old 1203,48666 +(defvar x-symbol-tex-xdecode-obarray 1245,50315 +(defun x-symbol-tex-xdecode-latex 1247,50358 + +x-symbol/lisp/x-symbol-texi.el,597 +(defcustom x-symbol-texi-auto-style 41,1573 +(defcustom x-symbol-texi-modeline-name 48,1832 +(defcustom x-symbol-texi-header-groups-alist54,2015 +(defcustom x-symbol-texi-electric-ignore 69,2682 +(defcustom x-symbol-texi-class-alist76,2950 +(defcustom x-symbol-texi-class-face-alist 89,3508 +(defvar x-symbol-texi-token-grammar98,3801 +(defvar x-symbol-texi-user-table 107,4094 +(defvar x-symbol-texi-generated-data 110,4206 +(defvar x-symbol-texi-latin1-table119,4523 +(defvar x-symbol-texi-latinN-table218,7766 +(defvar x-symbol-texi-xsymbX-table303,10629 +(defvar x-symbol-texi-table327,11362 + +x-symbol/lisp/x-symbol-unichars.el,99 +(defvar x-symbol-unicode-character-list5,115 +(defun x-symbol-list-unicode-characters 5044,235676 + +x-symbol/lisp/x-symbol-unicode.el,170 +(defconst x-symbol-xsym-unicode-map 12,383 +(defconst x-symbol-old-tables 260,9819 +(defconst x-symbol-unicode-table 276,10252 +(defconst x-symbol-unicode-cset292,10757 + +x-symbol/lisp/x-symbol-unicode-extras.el,38 +(defconst x-symol-unicode-extras 2,1 + +x-symbol/lisp/x-symbol-vars.el,8055 +(defconst x-symbol-version 40,1516 +(defgroup x-symbol 49,1858 +(defgroup x-symbol-mode 56,2069 +(defgroup x-symbol-input-init 61,2198 +(defgroup x-symbol-input-control 66,2334 +(defgroup x-symbol-info-general 71,2466 +(defgroup x-symbol-info-strings 76,2602 +(defgroup x-symbol-miscellaneous 81,2738 +(defgroup x-symbol-image-general 86,2864 +(defgroup x-symbol-image-language 91,3029 +(defgroup x-symbol-tex 101,3458 +(defgroup x-symbol-sgml 107,3589 +(defgroup x-symbol-bib 113,3725 +(defgroup x-symbol-texi 119,3859 +(define-widget 'x-symbol-key x-symbol-key132,4246 +(define-widget 'x-symbol-auto-style x-symbol-auto-style136,4336 +(define-widget 'x-symbol-command x-symbol-command156,5203 +(define-widget 'x-symbol-charsym x-symbol-charsym161,5311 +(define-widget 'x-symbol-group x-symbol-group165,5402 +(define-widget 'x-symbol-coding x-symbol-coding169,5494 +(define-widget 'x-symbol-function-or-regexp x-symbol-function-or-regexp178,5712 +(define-widget 'x-symbol-fancy-spec x-symbol-fancy-spec182,5881 +(define-widget 'x-symbol-fancy x-symbol-fancy191,6229 +(define-widget 'x-symbol-auto-coding x-symbol-auto-coding200,6582 +(define-widget 'x-symbol-headers x-symbol-headers211,6889 +(define-widget 'x-symbol-class-info x-symbol-class-info217,7045 +(define-widget 'x-symbol-class-faces x-symbol-class-faces224,7288 +(define-widget 'x-symbol-image-keywords x-symbol-image-keywords232,7568 +(defconst x-symbol-cache-variables 249,8155 +(defun x-symbol-set-cache-variable 258,8514 +(defconst x-symbol-LANG-name 270,8931 +(defconst x-symbol-LANG-modes 276,9186 +(defconst x-symbol-LANG-auto-style 282,9519 +(defcustom x-symbol-LANG-modeline-name 336,11613 +(defconst x-symbol-LANG-required-fonts 343,11898 +(defconst x-symbol-LANG-token-grammar348,12134 +(defconst x-symbol-LANG-generated-data 416,15400 +(defconst x-symbol-LANG-table 422,15652 +(defconst x-symbol-LANG-header-groups-alist 435,16207 +(defconst x-symbol-LANG-class-alist441,16510 +(defconst x-symbol-LANG-class-face-alist 455,17122 +(defconst x-symbol-LANG-electric-ignore 466,17574 +(defconst x-symbol-LANG-extra-menu-items 477,18088 +(defconst x-symbol-LANG-subscript-matcher 485,18533 +(defconst x-symbol-LANG-image-keywords 494,19001 +(defconst x-symbol-LANG-master-directory 509,19696 +(defconst x-symbol-LANG-image-searchpath 515,19987 +(defconst x-symbol-LANG-image-cached-dirs 523,20414 +(defvar x-symbol-package-url 534,20885 +(defconst x-symbol-maintainer-address 539,21129 +(defvar x-symbol-installer-address 542,21268 +(defcustom x-symbol-token-input 552,21708 +(defcustom x-symbol-electric-input 567,22362 +(defcustom x-symbol-local-menu 598,24006 +(defcustom x-symbol-local-grid 608,24350 +(defcustom x-symbol-temp-grid 620,24893 +(defcustom x-symbol-temp-help 630,25272 +(defvar x-symbol-use-refbuffer-once 640,25670 +(defcustom x-symbol-reveal-invisible 657,26459 +(defcustom x-symbol-character-info 676,27270 +(defcustom x-symbol-context-info 695,28145 +(defcustom x-symbol-charsym-modeline-name 710,28745 +(defcustom x-symbol-coding-name-alist716,28955 +(defcustom x-symbol-coding-modeline-alist742,29899 +(defcustom x-symbol-modeline-state-list757,30432 +(defcustom x-symbol-set-coding-system-if-undecided 794,31811 +(defcustom x-symbol-auto-coding-search-limit 807,32387 +(defcustom x-symbol-charsym-ascii-alist 819,32858 +(defcustom x-symbol-charsym-ascii-groups832,33446 +(defcustom x-symbol-valid-charsym-function 843,33930 +(defvar x-symbol-user-table 849,34181 +(defvar x-symbol-mule-change-default-face 861,34742 +(defcustom x-symbol-map-default-keys-alist872,35242 +(defcustom x-symbol-map-default-bindings902,36271 +(defvar x-symbol-after-init-input-hook 915,36725 +(defvar x-symbol-menu929,37366 +(defcustom x-symbol-menu-max-items 1005,40730 +(defcustom x-symbol-header-groups-alist1013,41090 +(defcustom x-symbol-completions-buffer 1042,42228 +(defcustom x-symbol-grid-buffer-format 1049,42470 +(defcustom x-symbol-grid-reuse 1058,42862 +(defcustom x-symbol-grid-header-echo1065,43142 +(defcustom x-symbol-grid-ignore-charsyms 1076,43585 +(defcustom x-symbol-grid-tab-width 1082,43812 +(defface x-symbol-heading-face1089,44115 +(defvar x-symbol-heading-strut-glyph1101,44565 +(defvar x-symbol-key-init-ignore 1115,45116 +(defvar x-symbol-quail-init-ignore 1119,45254 +(defvar x-symbol-context-init-ignore 1123,45394 +(defcustom x-symbol-context-ignore 1130,45685 +(defcustom x-symbol-electric-ignore 1138,46014 +(defcustom x-symbol-rotate-suffix-char 1149,46535 +(defcustom x-symbol-rotate-prefix-alist1158,46977 +(defvar x-symbol-list-mode-hook 1181,47657 +(defvar x-symbol-key-min-length 1186,47824 +(defvar x-symbol-quail-suffix-string 1191,48048 +(defvar x-symbol-define-input-method-quail 1194,48100 +(defcustom x-symbol-idle-delay 1201,48355 +(defface x-symbol-revealed-face1209,48703 +(defcustom x-symbol-context-info-ignore 1217,48995 +(defcustom x-symbol-context-info-threshold 1225,49388 +(defcustom x-symbol-context-info-ignore-regexp 1231,49594 +(defcustom x-symbol-context-info-ignore-groups1237,49821 +(defface x-symbol-info-face1251,50343 +(defface x-symbol-emph-info-face1262,50788 +(defcustom x-symbol-info-intro-after1270,51073 +(defcustom x-symbol-info-intro-before1279,51379 +(defcustom x-symbol-info-intro-highlight1288,51684 +(defcustom x-symbol-info-intro-list1297,52025 +(defcustom x-symbol-info-intro-yank1306,52413 +(defcustom x-symbol-info-alias-after1315,52795 +(defcustom x-symbol-info-alias-before1325,53227 +(defcustom x-symbol-info-context-pre1335,53644 +(defcustom x-symbol-info-context-post1344,54033 +(defcustom x-symbol-info-token-pre 1353,54349 +(defcustom x-symbol-info-token-charsym1360,54609 +(defcustom x-symbol-info-classes-pre 1369,54957 +(defcustom x-symbol-info-classes-sep 1376,55213 +(defcustom x-symbol-info-classes-post 1383,55468 +(defcustom x-symbol-info-classes-charsym 1390,55728 +(defcustom x-symbol-info-coding-pre 1397,56006 +(defcustom x-symbol-info-coding-sep 1404,56252 +(defcustom x-symbol-info-coding-post 1411,56499 +(defcustom x-symbol-info-coding-alist1418,56723 +(defcustom x-symbol-info-keys-keymaps 1434,57353 +(defcustom x-symbol-info-keys-pre1442,57729 +(defcustom x-symbol-info-keys-sep 1451,58097 +(defcustom x-symbol-info-keys-post 1458,58354 +(defconst x-symbol-fancy-cache-size 1465,58581 +(defvar x-symbol-cache-size 1468,58688 +(defvar x-symbol-modify-aspects-alist1477,59011 +(defvar x-symbol-rotate-aspects-alist1491,59696 +(defvar x-symbol-group-input-alist1507,60510 +(defvar x-symbol-group-syntax-alist1557,62097 +(defvar x-symbol-subgroup-string-alist1600,63344 +(defvar x-symbol-latin-force-use 1614,63859 +(defvar x-symbol-font-sizes1623,64369 +(defvar x-symbol-font-lock-with-extra-props1633,64777 +(defvar x-symbol-latin1-fonts1637,64928 +(defvar x-symbol-latin2-fonts1642,65128 +(defvar x-symbol-latin3-fonts1648,65391 +(defvar x-symbol-latin5-fonts1654,65654 +(defvar x-symbol-latin9-fonts1661,65961 +(defvar x-symbol-xsymb0-fonts1666,66159 +(defvar x-symbol-xsymb1-fonts1672,66450 +(defcustom x-symbol-image-max-width 1683,66913 +(defcustom x-symbol-image-max-height 1688,67035 +(defcustom x-symbol-image-update-cache 1693,67158 +(defcustom x-symbol-image-use-remote 1709,67929 +(defcustom x-symbol-image-current-marker 1734,69128 +(defcustom x-symbol-image-scale-method 1742,69475 +(defcustom x-symbol-image-explicitly-relative-regexp 1756,70205 +(defcustom x-symbol-image-searchpath-follow-symlink 1761,70387 +(defcustom x-symbol-image-cache-directories1776,71082 +(defvar x-symbol-image-temp-name1825,73064 +(defcustom x-symbol-image-convert-mono-regexp1834,73481 +(defcustom x-symbol-image-help-echo1848,74169 +(defcustom x-symbol-image-editor-alist1860,74673 +(defvar x-symbol-image-menu1893,76029 +(defvar x-symbol-image-data-directory 1914,77032 +(defvar x-symbol-image-special-glyphs1918,77199 +(defcustom x-symbol-image-convert-file-alist1951,78897 +(defcustom x-symbol-image-convert-program1961,79365 +(defcustom x-symbol-image-converter1967,79592 +(defun x-symbol-variable-interactive 2074,84086 +(defvar x-symbol-use-unicode 2093,84916 + +x-symbol/lisp/x-symbol-xmacs.el,522 +(defun x-symbol-paren-reset-mode 102,4657 +(defvar x-symbol-xmacs-default-face-fonts 136,6073 +(defalias 'x-symbol-directory-files x-symbol-directory-files138,6121 +(defun x-symbol-event-in-current-buffer 140,6176 +(defun x-symbol-create-image 144,6318 +(defalias 'x-symbol-make-glyph x-symbol-make-glyph149,6483 +(defalias 'x-symbol-set-glyph-image x-symbol-set-glyph-image151,6528 +(defun x-symbol-set-face-font 153,6583 +(defun x-symbol-event-matches-key-specifier-p 163,7016 +(defun x-symbol-window-width 173,7418 + TODO.developer,26 function to 401,16137 @@ -2871,47 +3610,51 @@ doc/PG-adapting.texi,3776 @node Recognizing proofsRecognizing proofs824,32857 @node Recognizing other elementsRecognizing other elements936,37676 @node Configuring undo behaviourConfiguring undo behaviour1062,43154 -@node Nested proofsNested proofs1200,48495 -@node Safe (state-preserving) commandsSafe (state-preserving) commands1240,50122 -@node Activate scripting hookActivate scripting hook1263,51068 -@node Automatic multiple filesAutomatic multiple files1287,51932 -@node Completions1309,52779 -@node Proof Shell SettingsProof Shell Settings1349,54257 -@node Proof shell commandsProof shell commands1380,55539 -@node Script input to the shellScript input to the shell1547,62718 -@node Settings for matching various output from proof processSettings for matching various output from proof process1614,65761 -@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1745,71525 -@node Hooks and other settingsHooks and other settings1955,81078 -@node Goals Buffer SettingsGoals Buffer Settings2054,85075 -@node Splash Screen SettingsSplash Screen Settings2131,88183 -@node Global ConstantsGlobal Constants2157,88941 -@node Handling Multiple FilesHandling Multiple Files2183,89790 -@node Configuring Editing SyntaxConfiguring Editing Syntax2335,97574 -@node Configuring Font LockConfiguring Font Lock2392,99691 -@node Configuring X-SymbolConfiguring X-Symbol2479,103934 -@node Writing More Lisp CodeWriting More Lisp Code2539,106457 -@node Default values for generic settingsDefault values for generic settings2556,107102 -@node Adding prover-specific configurationsAdding prover-specific configurations2586,108185 -@node Useful variablesUseful variables2629,109467 -@node Useful functions and macrosUseful functions and macros2655,110261 -@node Internals of Proof GeneralInternals of Proof General2758,114224 -@node Spans2786,115132 -@node Proof General site configurationProof General site configuration2799,115506 -@node Configuration variable mechanismsConfiguration variable mechanisms2879,118594 -@node Global variablesGlobal variables2997,123830 -@node Proof script modeProof script mode3067,126380 -@node Proof shell modeProof shell mode3326,138035 -@node Debugging3732,154082 -@node Plans and IdeasPlans and Ideas3775,154977 -@node Proof by pointing and similar featuresProof by pointing and similar features3796,155699 -@node Granularity of atomic command sequencesGranularity of atomic command sequences3834,157357 -@node Browser mode for script files and theoriesBrowser mode for script files and theories3879,159582 -@node Demonstration InstantiationsDemonstration Instantiations3909,160613 -@node demoisa-easy.el3925,161044 -@node demoisa.el3988,163283 -@node Function IndexFunction Index4156,168812 -@node Variable IndexVariable Index4160,168888 -@node Concept IndexConcept Index4169,169067 +@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,81087 +@node Goals Buffer SettingsGoals Buffer Settings2054,85084 +@node Splash Screen SettingsSplash Screen Settings2131,88198 +@node Global ConstantsGlobal Constants2157,88956 +@node Handling Multiple FilesHandling Multiple Files2183,89805 +@node Configuring Editing SyntaxConfiguring Editing Syntax2335,97589 +@node Configuring Font LockConfiguring Font Lock2392,99706 +@node Configuring X-SymbolConfiguring X-Symbol2479,103949 +@node Writing More Lisp CodeWriting More Lisp Code2539,106472 +@node Default values for generic settingsDefault values for generic settings2556,107117 +@node Adding prover-specific configurationsAdding prover-specific configurations2586,108200 +@node Useful variablesUseful variables2629,109482 +@node Useful functions and macrosUseful functions and macros2655,110276 +@node Internals of Proof GeneralInternals of Proof General2758,114239 +@node Spans2786,115147 +@node Proof General site configurationProof General site configuration2799,115521 +@node Configuration variable mechanismsConfiguration variable mechanisms2879,118609 +@node Global variablesGlobal variables2997,123845 +@node Proof script modeProof script mode3067,126395 +@node Proof shell modeProof shell mode3326,138050 +@node Debugging3732,154097 +@node Plans and IdeasPlans and Ideas3775,154992 +@node Proof by pointing and similar featuresProof by pointing and similar features3796,155714 +@node Granularity of atomic command sequencesGranularity of atomic command sequences3834,157372 +@node Browser mode for script files and theoriesBrowser mode for script files and theories3879,159597 +@node Demonstration InstantiationsDemonstration Instantiations3909,160628 +@node demoisa-easy.el3925,161059 +@node demoisa.el3988,163298 +@node Function IndexFunction Index4156,168827 +@node Variable IndexVariable Index4160,168903 +@node Concept IndexConcept Index4169,169082 + +x-symbol/lisp/_pkg.el,0 + +x-symbol/lisp/custom-load.el,0 lib/holes-load.el,0 @@ -2919,6 +3662,8 @@ generic/proof-system.el,0 generic/_pkg.el,0 +generic/pg-festival.el,0 + twelf/x-symbol-twelf.el,0 pgshell/pgshell.el,0 diff --git a/images/README b/images/README index e9bc5489..2c64018f 100644 --- a/images/README +++ b/images/README @@ -2,12 +2,17 @@ $Id$ Icons for Proof General. -David Aspinall <da@dcs.ed.ac.uk> +David Aspinall <da@inf.ed.ac.uk> + +The images in this directory were made with The Gimp and Inkscape. +They were created in my spare time as a donation to the Proof General +project. The images here are released under the Creative Commons +license, see http://creativecommons.org/licenses/by-nc-sa/3.0/ + +The search icon includes portions from Andrew Fitzsimon's Etiquette +search icon (under CC 2.0). -Contact: Proof General maintainer <proofgen@dcs.ed.ac.uk> -The images in this directory were made with The Gimp -(check www.gimp.org). |