diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-18 10:57:26 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-18 10:57:26 +0000 |
| commit | 9d0f7a3b737b5d9feb2ff49e0ccb34c706cd96bd (patch) | |
| tree | eff814f367cbb37d7f273c2837a061bec55d92fc /TAGS | |
| parent | 8434363ba8e148c4b239576d734f3e52486cd074 (diff) | |
Updated.
Diffstat (limited to 'TAGS')
| -rw-r--r-- | TAGS | 3238 |
1 files changed, 1589 insertions, 1649 deletions
@@ -1,228 +1,213 @@ acl2/acl2.el,0 -acl2/x-symbol-acl2.el,1868 -(defvar x-symbol-acl2-symbol-table x-symbol-acl2-symbol-table8,157 -(defvar x-symbol-acl2-master-directory x-symbol-acl2-master-directory50,1696 -(defvar x-symbol-acl2-image-searchpath x-symbol-acl2-image-searchpath51,1744 -(defvar x-symbol-acl2-image-cached-dirs x-symbol-acl2-image-cached-dirs52,1792 -(defvar x-symbol-acl2-image-keywords x-symbol-acl2-image-keywords53,1858 -(defvar x-symbol-acl2-font-lock-keywords x-symbol-acl2-font-lock-keywords54,1900 -(defvar x-symbol-acl2-header-groups-alist x-symbol-acl2-header-groups-alist55,1946 -(defvar x-symbol-acl2-class-alist x-symbol-acl2-class-alist56,1993 -(defvar x-symbol-acl2-class-face-alist x-symbol-acl2-class-face-alist59,2133 -(defvar x-symbol-acl2-electric-ignore x-symbol-acl2-electric-ignore60,2177 -(defvar x-symbol-acl2-required-fonts x-symbol-acl2-required-fonts61,2220 -(defvar x-symbol-acl2-case-insensitive x-symbol-acl2-case-insensitive62,2262 -(defvar x-symbol-acl2-token-shape x-symbol-acl2-token-shape65,2414 -(defvar x-symbol-acl2-table x-symbol-acl2-table66,2481 -(defun x-symbol-acl2-default-token-list x-symbol-acl2-default-token-list67,2537 -(defvar x-symbol-acl2-token-list x-symbol-acl2-token-list68,2594 -(defvar x-symbol-acl2-input-token-ignore x-symbol-acl2-input-token-ignore69,2662 -(defvar x-symbol-acl2-exec-specs x-symbol-acl2-exec-specs72,2728 -(defvar x-symbol-acl2-menu-alist x-symbol-acl2-menu-alist73,2766 -(defvar x-symbol-acl2-grid-alist x-symbol-acl2-grid-alist74,2804 -(defvar x-symbol-acl2-decode-atree x-symbol-acl2-decode-atree75,2842 -(defvar x-symbol-acl2-decode-alist x-symbol-acl2-decode-alist76,2882 -(defvar x-symbol-acl2-encode-alist x-symbol-acl2-encode-alist77,2922 -(defvar x-symbol-acl2-nomule-decode-exec x-symbol-acl2-nomule-decode-exec78,2962 -(defvar x-symbol-acl2-nomule-encode-exec x-symbol-acl2-nomule-encode-exec79,3008 +acl2/x-symbol-acl2.el,0 coq/coq-abbrev.el,49 -(defpgdefault menu-entriesmenu-entries144,7699 +(defpgdefault menu-entriesmenu-entries147,7898 coq/coq-abbrev-V7.el,49 (defpgdefault menu-entriesmenu-entries119,5878 coq/coq.el,4517 -(defcustom coq-prog-name coq-prog-name13,356 -(defcustom coq-default-undo-limit coq-default-undo-limit20,515 -(defconst coq-shell-init-cmd coq-shell-init-cmd25,643 -(defconst coq-shell-restart-cmd coq-shell-restart-cmd38,1066 -(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern42,1148 -(defvar coq-shell-cd coq-shell-cd46,1323 -(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp49,1423 -(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp52,1549 -(defvar coq-goal-regexpcoq-goal-regexp55,1680 -(defun coq-library-directory coq-library-directory64,1869 -(defcustom coq-tags coq-tags71,2049 -(defconst coq-interrupt-regexp coq-interrupt-regexp76,2198 -(defcustom coq-www-home-page coq-www-home-page81,2318 -(defun coq-insert-section coq-insert-section97,2568 -(defconst module-kinds-table module-kinds-table106,2825 -(defconst modtype-kinds-tablemodtype-kinds-table110,2961 -(defun coq-insert-module coq-insert-module114,3090 -(defvar coq-outline-regexpcoq-outline-regexp135,3847 -(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp140,4256 -(defvar coq-shell-outline-regexp coq-shell-outline-regexp142,4315 -(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp143,4365 -(defconst coq-kill-goal-command coq-kill-goal-command145,4428 -(defconst coq-forget-id-command coq-forget-id-command146,4471 -(defconst coq-back-n-command coq-back-n-command147,4517 -(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp151,4579 -(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp153,4676 -(defconst coq-tactics-regexpcoq-tactics-regexp155,4777 -(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp157,4843 -(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp159,4950 -(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp161,5062 -(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp163,5153 -(defvar coq-keywords-sectioncoq-keywords-section166,5252 -(defvar coq-section-regexp coq-section-regexp171,5397 -(defun coq-set-undo-limit coq-set-undo-limit204,6464 -(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp215,6807 -(defun coq-proof-mode-p coq-proof-mode-p223,7195 -(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp238,7701 -(defun coq-is-goalsave-p coq-is-goalsave-p240,7805 -(defun coq-is-module-equal-p coq-is-module-equal-p241,7880 -(defun coq-is-def-p coq-is-def-p244,8076 -(defun coq-is-decl-defn-p coq-is-decl-defn-p246,8184 -(defun coq-state-preserving-command-p coq-state-preserving-command-p251,8351 -(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p254,8485 -(defun coq-state-changing-command-p coq-state-changing-command-p257,8617 -(defun coq-section-or-module-start-p coq-section-or-module-start-p263,8925 -(defun coq-find-and-forget coq-find-and-forget271,9178 -(defvar coq-current-goal coq-current-goal363,13745 -(defun coq-goal-hyp coq-goal-hyp366,13810 -(defun coq-state-preserving-p coq-state-preserving-p379,14240 -(defun coq-SearchIsos coq-SearchIsos386,14557 -(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string400,14991 -(defun coq-Print coq-Print410,15285 -(defun coq-Check coq-Check419,15543 -(defun coq-Show coq-Show428,15785 -(defun coq-PrintHint coq-PrintHint437,16059 -(defun coq-end-Section coq-end-Section443,16202 -(defun coq-Compile coq-Compile461,16786 -(define-key coq-keymap coq-keymap472,17160 -(define-key coq-keymap coq-keymap473,17219 -(define-key coq-keymap coq-keymap474,17277 -(define-key coq-keymap coq-keymap475,17333 -(define-key coq-keymap coq-keymap476,17388 -(define-key coq-keymap coq-keymap477,17438 -(define-key coq-keymap coq-keymap478,17488 -(define-key global-map global-map485,17834 -(defun coq-guess-command-line coq-guess-command-line543,19752 -(defun coq-pre-shell-start coq-pre-shell-start565,20558 -(defun coq-mode-config coq-mode-config576,21000 -(defun coq-shell-mode-config coq-shell-mode-config747,27209 -(defun coq-goals-mode-config coq-goals-mode-config786,28844 -(defun coq-response-config coq-response-config793,29075 -(defpacustom print-only-first-subgoal print-only-first-subgoal814,29665 -(defpacustom auto-compile-vos auto-compile-vos819,29816 -(defun coq-fake-constant-markup coq-fake-constant-markup840,30671 -(defun coq-create-span-menu coq-create-span-menu862,31478 - -coq/coq-indent.el,1790 +(defcustom coq-prog-name coq-prog-name13,353 +(defcustom coq-default-undo-limit coq-default-undo-limit20,512 +(defconst coq-shell-init-cmd coq-shell-init-cmd25,640 +(defconst coq-shell-restart-cmd coq-shell-restart-cmd38,1063 +(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern42,1145 +(defvar coq-shell-cd coq-shell-cd46,1320 +(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp49,1420 +(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp52,1546 +(defvar coq-goal-regexpcoq-goal-regexp55,1677 +(defun coq-library-directory coq-library-directory64,1866 +(defcustom coq-tags coq-tags71,2046 +(defconst coq-interrupt-regexp coq-interrupt-regexp76,2195 +(defcustom coq-www-home-page coq-www-home-page81,2315 +(defun coq-insert-section coq-insert-section97,2565 +(defconst module-kinds-table module-kinds-table106,2822 +(defconst modtype-kinds-tablemodtype-kinds-table110,2958 +(defun coq-insert-module coq-insert-module114,3087 +(defvar coq-outline-regexpcoq-outline-regexp135,3844 +(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp140,4253 +(defvar coq-shell-outline-regexp coq-shell-outline-regexp142,4312 +(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp143,4362 +(defconst coq-kill-goal-command coq-kill-goal-command145,4425 +(defconst coq-forget-id-command coq-forget-id-command146,4468 +(defconst coq-back-n-command coq-back-n-command147,4514 +(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp151,4576 +(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp153,4673 +(defconst coq-tactics-regexpcoq-tactics-regexp155,4774 +(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp157,4840 +(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp159,4947 +(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp161,5059 +(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp163,5150 +(defvar coq-keywords-sectioncoq-keywords-section166,5249 +(defvar coq-section-regexp coq-section-regexp171,5394 +(defun coq-set-undo-limit coq-set-undo-limit204,6461 +(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp215,6804 +(defun coq-proof-mode-p coq-proof-mode-p223,7192 +(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp238,7698 +(defun coq-is-goalsave-p coq-is-goalsave-p240,7802 +(defun coq-is-module-equal-p coq-is-module-equal-p241,7877 +(defun coq-is-def-p coq-is-def-p244,8073 +(defun coq-is-decl-defn-p coq-is-decl-defn-p246,8181 +(defun coq-state-preserving-command-p coq-state-preserving-command-p251,8348 +(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p254,8482 +(defun coq-state-changing-command-p coq-state-changing-command-p257,8614 +(defun coq-section-or-module-start-p coq-section-or-module-start-p263,8922 +(defun coq-find-and-forget coq-find-and-forget271,9175 +(defvar coq-current-goal coq-current-goal363,13742 +(defun coq-goal-hyp coq-goal-hyp366,13807 +(defun coq-state-preserving-p coq-state-preserving-p379,14237 +(defun coq-SearchIsos coq-SearchIsos386,14554 +(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string400,14988 +(defun coq-Print coq-Print410,15282 +(defun coq-Check coq-Check419,15540 +(defun coq-Show coq-Show428,15782 +(defun coq-PrintHint coq-PrintHint437,16056 +(defun coq-end-Section coq-end-Section443,16199 +(defun coq-Compile coq-Compile461,16783 +(define-key coq-keymap coq-keymap472,17157 +(define-key coq-keymap coq-keymap473,17216 +(define-key coq-keymap coq-keymap474,17274 +(define-key coq-keymap coq-keymap475,17330 +(define-key coq-keymap coq-keymap476,17385 +(define-key coq-keymap coq-keymap477,17435 +(define-key coq-keymap coq-keymap478,17485 +(define-key global-map global-map487,17993 +(defun coq-guess-command-line coq-guess-command-line545,19911 +(defun coq-pre-shell-start coq-pre-shell-start567,20717 +(defun coq-mode-config coq-mode-config578,21159 +(defun coq-shell-mode-config coq-shell-mode-config753,27574 +(defun coq-goals-mode-config coq-goals-mode-config792,29209 +(defun coq-response-config coq-response-config799,29440 +(defpacustom print-only-first-subgoal print-only-first-subgoal820,30030 +(defpacustom auto-compile-vos auto-compile-vos825,30181 +(defun coq-fake-constant-markup coq-fake-constant-markup846,31036 +(defun coq-create-span-menu coq-create-span-menu868,31843 + +coq/coq-indent.el,1791 (defconst coq-any-command-regexpcoq-any-command-regexp11,262 (defconst coq-indent-inner-regexpcoq-indent-inner-regexp15,354 -(defconst coq-indent-open-regexpcoq-indent-open-regexp40,907 -(defconst coq-indent-close-regexpcoq-indent-close-regexp45,1077 -(defconst coq-indent-closepar-regexp coq-indent-closepar-regexp50,1235 -(defconst coq-indent-closematch-regexp coq-indent-closematch-regexp52,1281 -(defconst coq-indent-openpar-regexp coq-indent-openpar-regexp54,1353 -(defconst coq-indent-openmatch-regexp coq-indent-openmatch-regexp56,1398 -(defconst coq-indent-any-regexpcoq-indent-any-regexp58,1479 -(defconst coq-indent-kw coq-indent-kw67,1709 -(defconst coq-indent-pattern-regexp coq-indent-pattern-regexp78,2126 -(defun coq-find-command-start coq-find-command-start83,2213 -(defun coq-find-real-start coq-find-real-start92,2486 -(defun coq-find-end coq-find-end104,2880 -(defun coq-current-command-string coq-current-command-string114,3151 -(defun is-at-a-space-or-tab is-at-a-space-or-tab122,3350 -(defun only-spaces-on-line only-spaces-on-line128,3554 -(defun find-reg find-reg135,3802 -(defun coq-back-to-indentation-prevline coq-back-to-indentation-prevline149,4177 -(defun coq-find-unclosed coq-find-unclosed178,5413 -(defun coq-find-at-same-level-zero coq-find-at-same-level-zero205,6594 -(defun coq-find-unopened coq-find-unopened233,7678 -(defun coq-find-last-unopened coq-find-last-unopened279,9031 -(defun coq-end-offset coq-end-offset292,9435 -(defun coq-indent-command-offset coq-indent-command-offset320,10254 -(defun coq-indent-expr-offset coq-indent-expr-offset365,12014 -(defun coq-indent-offset coq-indent-offset477,16217 -(defun coq-indent-calculate coq-indent-calculate497,16880 -(defun proof-indent-line proof-indent-line511,17327 - -coq/coq-syntax.el,2989 -(defvar coq-version-is-V74 coq-version-is-V7416,416 -(defvar coq-version-is-V7 coq-version-is-V717,448 -(defvar coq-version-is-V6 coq-version-is-V625,768 -(defvar coq-version-is-V7 coq-version-is-V732,1131 -(defvar coq-version-is-V74 coq-version-is-V7440,1536 -(defvar coq-version-is-V8 coq-version-is-V848,1910 -(defvar coq-keywords-declcoq-keywords-decl122,4416 -(defvar coq-keywords-defncoq-keywords-defn137,4772 -(defun coq-count-match coq-count-match211,7128 -(defun coq-goal-command-p coq-goal-command-p223,7548 -(defvar coq-keywords-save-strictcoq-keywords-save-strict243,8132 -(defvar coq-keywords-savecoq-keywords-save251,8229 -(defun coq-save-command-p coq-save-command-p255,8305 -(defvar coq-keywords-kill-goal coq-keywords-kill-goal263,8584 -(defcustom coq-user-state-changing-commands coq-user-state-changing-commands269,8634 -(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands281,9031 -(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands294,9471 -(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands341,10582 -(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands415,12600 -(defvar coq-keywords-commandscoq-keywords-commands425,12797 -(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics431,12947 -(defvar coq-state-changing-tacticscoq-state-changing-tactics442,13373 -(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics643,16698 -(defvar coq-state-preserving-tacticscoq-state-preserving-tactics654,17112 -(defvar coq-tacticscoq-tactics658,17210 -(defvar coq-retractable-instructcoq-retractable-instruct661,17299 -(defvar coq-non-retractable-instructcoq-non-retractable-instruct664,17409 -(defvar coq-keywordscoq-keywords668,17531 -(defvar coq-tacticalscoq-tacticals673,17696 -(defvar coq-reservedcoq-reserved682,17872 -(defvar coq-symbolscoq-symbols706,18139 -(defvar coq-error-regexp coq-error-regexp724,18343 -(defvar coq-id coq-id727,18559 -(defvar coq-ids coq-ids729,18585 -(defun coq-first-abstr-regexp coq-first-abstr-regexp731,18622 -(defun coq-next-abstr-regexp coq-next-abstr-regexp734,18710 -(defvar coq-font-lock-termscoq-font-lock-terms737,18788 -(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict752,19441 -(defconst coq-save-command-regexpcoq-save-command-regexp754,19554 -(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp756,19653 -(defconst coq-goal-command-regexpcoq-goal-command-regexp759,19791 -(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp761,19890 -(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp767,20179 -(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp770,20312 -(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1773,20449 -(defvar coq-font-lock-keywords coq-font-lock-keywords794,21492 -(defun coq-init-syntax-table coq-init-syntax-table796,21550 - -coq/x-symbol-coq.el,2282 -(defvar x-symbol-coq-symbol-table x-symbol-coq-symbol-table8,155 -(defvar x-symbol-coq-master-directory x-symbol-coq-master-directory51,1712 -(defvar x-symbol-coq-image-searchpath x-symbol-coq-image-searchpath52,1759 -(defvar x-symbol-coq-image-cached-dirs x-symbol-coq-image-cached-dirs53,1806 -(defvar x-symbol-coq-image-file-truename-alist x-symbol-coq-image-file-truename-alist54,1871 -(defvar x-symbol-coq-image-keywords x-symbol-coq-image-keywords55,1923 -(defvar x-symbol-coq-font-lock-keywords x-symbol-coq-font-lock-keywords56,1964 -(defvar x-symbol-coq-header-groups-alist x-symbol-coq-header-groups-alist57,2009 -(defvar x-symbol-coq-class-alist x-symbol-coq-class-alist58,2055 -(defvar x-symbol-coq-class-face-alist x-symbol-coq-class-face-alist61,2192 -(defvar x-symbol-coq-electric-ignore x-symbol-coq-electric-ignore62,2235 -(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts63,2277 -(defvar x-symbol-coq-case-insensitive x-symbol-coq-case-insensitive64,2318 -(defvar x-symbol-coq-extra-menu-items x-symbol-coq-extra-menu-items65,2361 -(defvar x-symbol-coq-token-grammar x-symbol-coq-token-grammar66,2404 -(defvar x-symbol-coq-input-token-grammar x-symbol-coq-input-token-grammar67,2444 -(defvar x-symbol-coq-generated-data x-symbol-coq-generated-data68,2490 -(defvar x-symbol-coq-token-shape x-symbol-coq-token-shape76,2756 -(defvar x-symbol-coq-table x-symbol-coq-table78,2795 -(defvar x-symbol-coq-user-table x-symbol-coq-user-table79,2849 -(defun x-symbol-coq-default-token-list x-symbol-coq-default-token-list80,2886 -(defvar x-symbol-coq-token-list x-symbol-coq-token-list81,2942 -(defvar x-symbol-coq-input-token-ignore x-symbol-coq-input-token-ignore82,3008 -(defvar x-symbol-coq-exec-specs x-symbol-coq-exec-specs85,3073 -(defvar x-symbol-coq-menu-alist x-symbol-coq-menu-alist86,3110 -(defvar x-symbol-coq-grid-alist x-symbol-coq-grid-alist87,3147 -(defvar x-symbol-coq-decode-atree x-symbol-coq-decode-atree88,3184 -(defvar x-symbol-coq-decode-alist x-symbol-coq-decode-alist89,3223 -(defvar x-symbol-coq-encode-alist x-symbol-coq-encode-alist90,3262 -(defvar x-symbol-coq-nomule-decode-exec x-symbol-coq-nomule-decode-exec91,3301 -(defvar x-symbol-coq-nomule-encode-exec x-symbol-coq-nomule-encode-exec92,3346 +(defconst coq-indent-open-regexpcoq-indent-open-regexp43,1113 +(defconst coq-indent-close-regexpcoq-indent-close-regexp48,1283 +(defconst coq-indent-closepar-regexp coq-indent-closepar-regexp53,1441 +(defconst coq-indent-closematch-regexp coq-indent-closematch-regexp55,1487 +(defconst coq-indent-openpar-regexp coq-indent-openpar-regexp57,1559 +(defconst coq-indent-openmatch-regexp coq-indent-openmatch-regexp59,1604 +(defconst coq-indent-any-regexpcoq-indent-any-regexp61,1685 +(defconst coq-indent-kw coq-indent-kw70,1914 +(defconst coq-indent-pattern-regexp coq-indent-pattern-regexp81,2331 +(defun coq-find-command-start coq-find-command-start86,2418 +(defun coq-find-real-start coq-find-real-start95,2691 +(defun coq-find-end coq-find-end107,3085 +(defun coq-current-command-string coq-current-command-string117,3356 +(defun is-at-a-space-or-tab is-at-a-space-or-tab125,3555 +(defun only-spaces-on-line only-spaces-on-line131,3759 +(defun find-reg find-reg138,4007 +(defun coq-back-to-indentation-prevline coq-back-to-indentation-prevline152,4382 +(defun coq-find-unclosed coq-find-unclosed181,5618 +(defun coq-find-at-same-level-zero coq-find-at-same-level-zero208,6799 +(defun coq-find-unopened coq-find-unopened236,7883 +(defun coq-find-last-unopened coq-find-last-unopened282,9236 +(defun coq-end-offset coq-end-offset295,9640 +(defun coq-indent-command-offset coq-indent-command-offset323,10459 +(defun coq-indent-expr-offset coq-indent-expr-offset368,12219 +(defun coq-indent-offset coq-indent-offset480,16422 +(defun coq-indent-calculate coq-indent-calculate500,17085 +(defun proof-indent-line proof-indent-line514,17532 + +coq/coq-syntax.el,3214 +(defvar coq-version-is-V74 coq-version-is-V7416,413 +(defvar coq-version-is-V7 coq-version-is-V717,445 +(defvar coq-version-is-V6 coq-version-is-V625,765 +(defvar coq-version-is-V7 coq-version-is-V732,1128 +(defvar coq-version-is-V74 coq-version-is-V7440,1533 +(defvar coq-version-is-V8 coq-version-is-V848,1907 +(defvar coq-keywords-declcoq-keywords-decl122,4413 +(defvar coq-keywords-defncoq-keywords-defn137,4769 +(defun coq-count-match coq-count-match211,7125 +(defun coq-goal-command-p coq-goal-command-p223,7545 +(defvar coq-keywords-save-strictcoq-keywords-save-strict243,8129 +(defvar coq-keywords-savecoq-keywords-save251,8226 +(defun coq-save-command-p coq-save-command-p255,8302 +(defvar coq-keywords-kill-goal coq-keywords-kill-goal263,8581 +(defcustom coq-user-state-changing-commands coq-user-state-changing-commands269,8631 +(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands281,9028 +(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands294,9468 +(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands341,10579 +(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands415,12597 +(defvar coq-keywords-commandscoq-keywords-commands425,12794 +(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics431,12944 +(defvar coq-state-changing-tacticscoq-state-changing-tactics442,13370 +(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics643,16695 +(defvar coq-state-preserving-tacticscoq-state-preserving-tactics654,17109 +(defvar coq-tacticscoq-tactics658,17207 +(defvar coq-retractable-instructcoq-retractable-instruct661,17296 +(defvar coq-non-retractable-instructcoq-non-retractable-instruct664,17406 +(defvar coq-keywordscoq-keywords668,17528 +(defvar coq-tacticalscoq-tacticals673,17693 +(defvar coq-reserved-commoncoq-reserved-common695,18076 +(defvar coq-reserved-V8coq-reserved-V8711,18269 +(defvar coq-reserved-V7coq-reserved-V7722,18373 +(defvar coq-reserved coq-reserved727,18448 +(defvar coq-symbolscoq-symbols735,18604 +(defvar coq-error-regexp coq-error-regexp753,18808 +(defvar coq-id coq-id756,19024 +(defvar coq-ids coq-ids758,19050 +(defun coq-first-abstr-regexp coq-first-abstr-regexp760,19087 +(defun coq-next-abstr-regexp coq-next-abstr-regexp763,19175 +(defvar coq-font-lock-termscoq-font-lock-terms766,19253 +(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict781,19906 +(defconst coq-save-command-regexpcoq-save-command-regexp783,20019 +(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp785,20118 +(defconst coq-goal-command-regexpcoq-goal-command-regexp788,20256 +(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp790,20355 +(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp796,20644 +(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp799,20777 +(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1802,20917 +(defvar coq-font-lock-keywords coq-font-lock-keywords823,21960 +(defun coq-init-syntax-table coq-init-syntax-table825,22018 +(defconst coq-generic-expressioncoq-generic-expression854,22916 + +coq/x-symbol-coq.el,2822 +(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts16,382 +(defvar x-symbol-coq-name x-symbol-coq-name24,783 +(defvar x-symbol-coq-modeline-name x-symbol-coq-modeline-name25,823 +(defcustom x-symbol-coq-header-groups-alist x-symbol-coq-header-groups-alist27,866 +(defcustom x-symbol-coq-electric-ignore x-symbol-coq-electric-ignore34,1084 +(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts41,1329 +(defvar x-symbol-coq-extra-menu-items x-symbol-coq-extra-menu-items44,1428 +(defvar x-symbol-coq-token-grammarx-symbol-coq-token-grammar48,1516 +(defun x-symbol-coq-default-token-list x-symbol-coq-default-token-list63,2165 +(defvar x-symbol-coq-user-table x-symbol-coq-user-table75,2453 +(defvar x-symbol-coq-generated-data x-symbol-coq-generated-data78,2559 +(defvar x-symbol-coq-master-directory x-symbol-coq-master-directory86,2797 +(defvar x-symbol-coq-image-searchpath x-symbol-coq-image-searchpath87,2845 +(defvar x-symbol-coq-image-cached-dirs x-symbol-coq-image-cached-dirs88,2892 +(defvar x-symbol-coq-image-file-truename-alist x-symbol-coq-image-file-truename-alist89,2957 +(defvar x-symbol-coq-image-keywords x-symbol-coq-image-keywords90,3009 +(defcustom x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher98,3257 +(defcustom x-symbol-coq-font-lock-regexp x-symbol-coq-font-lock-regexp104,3489 +(defcustom x-symbol-coq-font-lock-limit-regexp x-symbol-coq-font-lock-limit-regexp109,3661 +(defcustom x-symbol-coq-font-lock-contents-regexp x-symbol-coq-font-lock-contents-regexp115,3849 +(defcustom x-symbol-coq-single-char-regexp x-symbol-coq-single-char-regexp122,4103 +(defun x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher127,4251 +(defun coq-match-subscript coq-match-subscript161,5887 +(defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces168,6106 +(defcustom x-symbol-coq-class-alistx-symbol-coq-class-alist173,6331 +(defcustom x-symbol-coq-class-face-alist x-symbol-coq-class-face-alist184,6709 +(defvar x-symbol-coq-font-lock-keywords x-symbol-coq-font-lock-keywords194,7019 +(defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces196,7065 +(defvar x-symbol-coq-case-insensitive x-symbol-coq-case-insensitive202,7289 +(defvar x-symbol-coq-token-shape x-symbol-coq-token-shape203,7332 +(defvar x-symbol-coq-input-token-ignore x-symbol-coq-input-token-ignore204,7370 +(defvar x-symbol-coq-token-list x-symbol-coq-token-list205,7415 +(defvar x-symbol-coq-symbol-table x-symbol-coq-symbol-table207,7459 +(defvar x-symbol-coq-xsymbol-table x-symbol-coq-xsymbol-table311,9878 +(defun x-symbol-coq-prepare-table x-symbol-coq-prepare-table458,13746 +(defvar x-symbol-coq-tablex-symbol-coq-table467,14013 +(defcustom x-symbol-coq-auto-stylex-symbol-coq-auto-style474,14174 demoisa/demoisa-easy.el,0 @@ -237,74 +222,75 @@ demoisa/demoisa.el,568 (define-derived-mode demoisa-goals-mode demoisa-goals-mode133,4387 (defun demoisa-pre-shell-start demoisa-pre-shell-start152,5169 -generic/holes.el,3537 +generic/holes.el,3536 (defun holes-short-doc holes-short-doc24,736 -(defcustom empty-hole-string empty-hole-string151,5475 -(defcustom empty-hole-regexp empty-hole-regexp154,5580 -(defcustom hole-search-limit hole-search-limit157,6180 -(defface active-hole-faceactive-hole-face170,6546 -(defface inactive-hole-faceinactive-hole-face180,7003 -(defun region-beginning-or-nil region-beginning-or-nil199,7539 -(defun region-end-or-nil region-end-or-nil203,7628 -(defun copy-active-region copy-active-region207,7707 -(defun is-hole-p is-hole-p213,7885 -(defun hole-start-position hole-start-position218,7945 -(defun hole-end-position hole-end-position223,8082 -(defun hole-buffer hole-buffer228,8212 -(defun hole-at hole-at233,8334 -(defun active-hole-exist-p active-hole-exist-p242,8522 -(defun active-hole-start-position active-hole-start-position252,8773 -(defun active-hole-end-position active-hole-end-position263,9123 -(defun active-hole-buffer active-hole-buffer275,9469 -(defun goto-active-hole goto-active-hole286,9749 -(defun highlight-hole-as-active highlight-hole-as-active298,10022 -(defun highlight-hole highlight-hole308,10329 -(defun disable-active-hole disable-active-hole319,10624 -(defun set-active-hole set-active-hole337,11133 -(defun is-in-hole-p is-in-hole-p349,11434 -(defun make-hole make-hole359,11579 -(defun make-hole-at make-hole-at384,12394 -(defun clear-hole clear-hole403,12836 -(defun clear-hole-at clear-hole-at413,13053 -(defun map-holes map-holes422,13282 -(defun mapcar-holes mapcar-holes428,13396 -(defun clear-all-buffer-holes clear-all-buffer-holes432,13495 -(defun next-hole next-hole444,13729 -(defun next-after-active-hole next-after-active-hole453,13993 -(defun set-active-hole-next set-active-hole-next460,14173 -(defun set-active-hole-next-after-active set-active-hole-next-after-active477,14530 -(defun replace-segment replace-segment488,14688 -(defun replace-hole replace-hole504,15004 -(defun replace-active-hole replace-active-hole538,16160 -(defun replace-update-active-hole replace-update-active-hole547,16443 -(defun delete-update-active-hole delete-update-active-hole570,17069 -(defun set-make-active-hole set-make-active-hole579,17266 -(defun mouse-replace-active-hole mouse-replace-active-hole626,18613 -(defun destroy-hole destroy-hole644,19089 -(defun hole-at-event hole-at-event659,19400 -(defun mouse-destroy-hole mouse-destroy-hole661,19459 -(defun mouse-forget-hole mouse-forget-hole669,19633 -(defun mouse-set-make-active-hole mouse-set-make-active-hole683,19874 -(defun mouse-set-active-hole mouse-set-active-hole703,20325 -(defun set-point-next-hole-destroy set-point-next-hole-destroy713,20519 -(defun count-char-in-string count-char-in-string777,22766 -(defun count-re-in-string count-re-in-string787,22971 -(defun count-chars-in-last-expand count-chars-in-last-expand797,23182 -(defun count-newlines-in-last-expand count-newlines-in-last-expand801,23271 -(defun indent-last-expand indent-last-expand805,23382 -(defun count-holes-in-last-expand count-holes-in-last-expand820,23708 -(defun replace-string-by-holes replace-string-by-holes824,23827 -(defun replace-string-by-holes-backward replace-string-by-holes-backward843,24253 -(defun replace-string-by-holes-move-point replace-string-by-holes-move-point874,25071 -(defun replace-string-by-holes-backward-move-point replace-string-by-holes-backward-move-point881,25225 -(defun holes-abbrev-complete holes-abbrev-complete891,25401 -(defun insert-and-expand insert-and-expand913,26203 - -generic/pg-assoc.el,342 +(defcustom empty-hole-string empty-hole-string149,5370 +(defcustom empty-hole-regexp empty-hole-regexp152,5475 +(defcustom hole-search-limit hole-search-limit155,6075 +(defface active-hole-faceactive-hole-face168,6441 +(defface inactive-hole-faceinactive-hole-face178,6898 +(defun region-beginning-or-nil region-beginning-or-nil197,7434 +(defun region-end-or-nil region-end-or-nil201,7523 +(defun copy-active-region copy-active-region205,7602 +(defun is-hole-p is-hole-p211,7780 +(defun hole-start-position hole-start-position216,7840 +(defun hole-end-position hole-end-position221,7977 +(defun hole-buffer hole-buffer226,8107 +(defun hole-at hole-at231,8229 +(defun active-hole-exist-p active-hole-exist-p240,8417 +(defun active-hole-start-position active-hole-start-position250,8668 +(defun active-hole-end-position active-hole-end-position261,9018 +(defun active-hole-buffer active-hole-buffer273,9364 +(defun goto-active-hole goto-active-hole284,9644 +(defun highlight-hole-as-active highlight-hole-as-active296,9917 +(defun highlight-hole highlight-hole306,10224 +(defun disable-active-hole disable-active-hole317,10519 +(defun set-active-hole set-active-hole335,11028 +(defun is-in-hole-p is-in-hole-p347,11329 +(defun make-hole make-hole357,11474 +(defun make-hole-at make-hole-at382,12289 +(defun clear-hole clear-hole401,12731 +(defun clear-hole-at clear-hole-at411,12948 +(defun map-holes map-holes420,13177 +(defun mapcar-holes mapcar-holes426,13291 +(defun clear-all-buffer-holes clear-all-buffer-holes430,13390 +(defun next-hole next-hole442,13624 +(defun next-after-active-hole next-after-active-hole451,13888 +(defun set-active-hole-next set-active-hole-next458,14068 +(defun set-active-hole-next-after-active set-active-hole-next-after-active475,14425 +(defun replace-segment replace-segment486,14583 +(defun replace-hole replace-hole502,14899 +(defun replace-active-hole replace-active-hole536,16055 +(defun replace-update-active-hole replace-update-active-hole545,16338 +(defun delete-update-active-hole delete-update-active-hole568,16964 +(defun set-make-active-hole set-make-active-hole577,17161 +(defun mouse-replace-active-hole mouse-replace-active-hole624,18508 +(defun destroy-hole destroy-hole642,18984 +(defun hole-at-event hole-at-event657,19295 +(defun mouse-destroy-hole mouse-destroy-hole659,19354 +(defun mouse-forget-hole mouse-forget-hole667,19528 +(defun mouse-set-make-active-hole mouse-set-make-active-hole681,19769 +(defun mouse-set-active-hole mouse-set-active-hole701,20220 +(defun set-point-next-hole-destroy set-point-next-hole-destroy711,20414 +(defun count-char-in-string count-char-in-string775,22661 +(defun count-re-in-string count-re-in-string785,22866 +(defun count-chars-in-last-expand count-chars-in-last-expand795,23077 +(defun count-newlines-in-last-expand count-newlines-in-last-expand799,23166 +(defun indent-last-expand indent-last-expand803,23277 +(defun count-holes-in-last-expand count-holes-in-last-expand818,23603 +(defun replace-string-by-holes replace-string-by-holes822,23722 +(defun replace-string-by-holes-backward replace-string-by-holes-backward841,24148 +(defun replace-string-by-holes-move-point replace-string-by-holes-move-point872,24966 +(defun replace-string-by-holes-backward-move-point replace-string-by-holes-backward-move-point879,25120 +(defun holes-abbrev-complete holes-abbrev-complete889,25296 +(defun insert-and-expand insert-and-expand911,26098 + +generic/pg-assoc.el,408 (define-derived-mode proof-universal-keys-only-mode proof-universal-keys-only-mode20,563 -(defun pg-assoc-strip-subterm-markup pg-assoc-strip-subterm-markup32,978 -(defun pg-assoc-strip-subterm-markup-buf pg-assoc-strip-subterm-markup-buf58,1911 -(defun pg-assoc-strip-subterm-markup-buf-old pg-assoc-strip-subterm-markup-buf-old80,2660 +(defun proof-associated-buffers proof-associated-buffers32,987 +(defun pg-assoc-strip-subterm-markup pg-assoc-strip-subterm-markup46,1287 +(defun pg-assoc-strip-subterm-markup-buf pg-assoc-strip-subterm-markup-buf72,2220 +(defun pg-assoc-strip-subterm-markup-buf-old pg-assoc-strip-subterm-markup-buf-old94,2969 generic/pg-goals.el,1074 (define-derived-mode proof-goals-mode proof-goals-mode28,650 @@ -325,64 +311,58 @@ generic/pg-goals.el,1074 (defun pg-goals-construct-command pg-goals-construct-command348,12775 (defun pg-goals-get-subterm-help pg-goals-get-subterm-help372,13627 -generic/pg-init.el,0 - -generic/pg-metadata.el,266 +generic/pg-metadata.el,204 (defcustom pg-metadata-default-directory pg-metadata-default-directory23,628 (defface proof-preparsed-span proof-preparsed-span28,802 (defun pg-metadata-filename-for pg-metadata-filename-for39,1065 -(defun pg-write-metadata-file pg-write-metadata-file54,1508 - -generic/pg-nxml.el,66 -(defun pg-nxml-support-available pg-nxml-support-available9,236 -generic/pg-pgip.el,1153 +generic/pg-pgip.el,1154 (defalias 'pg-pgip-error pg-pgip-error17,544 (defun pg-pgip-process-packet pg-pgip-process-packet20,593 (defun pg-pgip-process-cmds pg-pgip-process-cmds28,981 -(defun pg-pgip-post-process pg-pgip-post-process80,2331 -(defun pg-pgip-haspref pg-pgip-haspref116,3279 -(defun pg-pgip-default-for pg-pgip-default-for179,5562 -(defun pg-pgip-subst-for pg-pgip-subst-for190,5874 -(defun pg-pgip-get-type pg-pgip-get-type197,6035 -(defun pg-pgip-pgiptype pg-pgip-pgiptype204,6257 -(defun pg-pgip-interpret-bool pg-pgip-interpret-bool228,7121 -(defun pg-pgip-interpret-int pg-pgip-interpret-int237,7397 -(defun pg-pgip-interpret-string pg-pgip-interpret-string242,7560 -(defun pg-pgip-interpret-choice pg-pgip-interpret-choice245,7610 -(defun pg-pgip-interpret-value pg-pgip-interpret-value265,8305 -(defun pg-pgip-get-attr pg-pgip-get-attr288,8930 -(defun pg-pgip-get-version pg-pgip-get-version295,9143 -(defun pg-prover-interpret-pgip-command pg-prover-interpret-pgip-command303,9375 -(defun pg-issue-pgip pg-issue-pgip320,9797 -(defun pg-pgip-askprefs pg-pgip-askprefs328,10069 -(defun pg-pgip-parsescript pg-pgip-parsescript337,10281 - -generic/pg-response.el,1667 -(define-derived-mode proof-response-mode proof-response-mode24,598 -(defun proof-response-config-done proof-response-config-done47,1491 -(defvar proof-shell-special-display-regexp proof-shell-special-display-regexp60,1857 -(defconst proof-multiframe-specifiers proof-multiframe-specifiers68,2254 -(defun proof-map-multiple-frame-specifiers proof-map-multiple-frame-specifiers81,2787 -(defconst proof-multiframe-parametersproof-multiframe-parameters88,3053 -(defun proof-multiple-frames-enable proof-multiple-frames-enable95,3253 -(defun proof-three-window-mode proof-three-window-mode120,4139 -(defun proof-select-three-b proof-select-three-b124,4201 -(defun proof-display-three-b proof-display-three-b137,4583 -(defvar pg-frame-configuration pg-frame-configuration149,5025 -(defun pg-cache-frame-configuration pg-cache-frame-configuration153,5172 -(defun proof-layout-windows proof-layout-windows157,5343 -(defun proof-delete-other-frames proof-delete-other-frames179,6173 -(defvar pg-response-erase-flag pg-response-erase-flag201,6831 -(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response204,6946 -(defun pg-response-display pg-response-display234,8096 -(defun pg-response-display-with-face pg-response-display-with-face251,8918 -(defun pg-response-clear-displays pg-response-clear-displays286,10275 -(defvar pg-response-next-error pg-response-next-error303,10805 -(defun proof-next-error proof-next-error307,10927 -(defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos402,14340 -(defun proof-trace-buffer-display proof-trace-buffer-display405,14432 -(defun pg-thms-buffer-clear pg-thms-buffer-clear445,15652 +(defun pg-pgip-post-process pg-pgip-post-process88,2599 +(defun pg-pgip-haspref pg-pgip-haspref125,3616 +(defun pg-pgip-default-for pg-pgip-default-for188,5899 +(defun pg-pgip-subst-for pg-pgip-subst-for199,6211 +(defun pg-pgip-get-type pg-pgip-get-type206,6372 +(defun pg-pgip-pgiptype pg-pgip-pgiptype213,6594 +(defun pg-pgip-interpret-bool pg-pgip-interpret-bool237,7458 +(defun pg-pgip-interpret-int pg-pgip-interpret-int246,7734 +(defun pg-pgip-interpret-string pg-pgip-interpret-string251,7897 +(defun pg-pgip-interpret-choice pg-pgip-interpret-choice254,7947 +(defun pg-pgip-interpret-value pg-pgip-interpret-value274,8642 +(defun pg-pgip-get-attr pg-pgip-get-attr297,9267 +(defun pg-pgip-get-version pg-pgip-get-version304,9480 +(defun pg-prover-interpret-pgip-command pg-prover-interpret-pgip-command312,9712 +(defun pg-issue-pgip pg-issue-pgip329,10134 +(defun pg-pgip-askprefs pg-pgip-askprefs337,10406 +(defun pg-pgip-parsescript pg-pgip-parsescript346,10618 + +generic/pg-response.el,1673 +(define-derived-mode proof-response-mode proof-response-mode24,597 +(defun proof-response-config-done proof-response-config-done47,1490 +(defvar proof-shell-special-display-regexp proof-shell-special-display-regexp68,2265 +(defconst proof-multiframe-specifiers proof-multiframe-specifiers76,2670 +(defun proof-map-multiple-frame-specifiers proof-map-multiple-frame-specifiers85,3034 +(defconst proof-multiframe-parametersproof-multiframe-parameters95,3496 +(defun proof-multiple-frames-enable proof-multiple-frames-enable103,3730 +(defun proof-three-window-enable proof-three-window-enable125,4450 +(defun proof-select-three-b proof-select-three-b129,4514 +(defun proof-display-three-b proof-display-three-b142,4896 +(defvar pg-frame-configuration pg-frame-configuration154,5338 +(defun pg-cache-frame-configuration pg-cache-frame-configuration158,5485 +(defun proof-layout-windows proof-layout-windows162,5656 +(defun proof-delete-other-frames proof-delete-other-frames193,6906 +(defvar pg-response-erase-flag pg-response-erase-flag224,8001 +(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response227,8116 +(defun pg-response-display pg-response-display257,9266 +(defun pg-response-display-with-face pg-response-display-with-face274,10088 +(defun pg-response-clear-displays pg-response-clear-displays309,11445 +(defvar pg-response-next-error pg-response-next-error326,11975 +(defun proof-next-error proof-next-error330,12097 +(defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos425,15510 +(defun proof-trace-buffer-display proof-trace-buffer-display428,15602 +(defun pg-thms-buffer-clear pg-thms-buffer-clear468,16822 generic/pg-thymodes.el,219 (defmacro pg-defthymode pg-defthymode19,466 @@ -391,57 +371,58 @@ generic/pg-thymodes.el,219 (defun pg-modesym pg-modesym78,2520 (defun pg-modesymval pg-modesymval82,2634 -generic/pg-user.el,3464 -(defmacro proof-maybe-save-point proof-maybe-save-point21,413 -(defun proof-maybe-follow-locked-end proof-maybe-follow-locked-end29,615 -(defun proof-assert-next-command-interactive proof-assert-next-command-interactive43,980 -(defun proof-process-buffer proof-process-buffer53,1351 -(defun proof-undo-last-successful-command proof-undo-last-successful-command67,1668 -(defun proof-undo-and-delete-last-successful-command proof-undo-and-delete-last-successful-command72,1830 -(defun proof-undo-last-successful-command-1 proof-undo-last-successful-command-194,2802 -(defun proof-retract-buffer proof-retract-buffer110,3367 -(defun proof-retract-current-goal proof-retract-current-goal119,3647 -(defun proof-interrupt-process proof-interrupt-process137,4138 -(defun proof-goto-command-start proof-goto-command-start164,5123 -(defun proof-goto-command-end proof-goto-command-end187,6065 -(defun proof-mouse-goto-point proof-mouse-goto-point212,6845 -(defun proof-mouse-track-insert proof-mouse-track-insert227,7419 -(defvar proof-minibuffer-history proof-minibuffer-history262,8529 -(defun proof-minibuffer-cmd proof-minibuffer-cmd265,8623 -(defun proof-frob-locked-end proof-frob-locked-end313,10429 -(defmacro proof-if-setting-configured proof-if-setting-configured406,13343 -(defmacro proof-define-assistant-command proof-define-assistant-command413,13598 -(defmacro proof-define-assistant-command-witharg proof-define-assistant-command-witharg425,14049 -(defun proof-issue-new-command proof-issue-new-command445,14855 -(defun proof-cd-sync proof-cd-sync490,16354 -(deflocal proof-electric-terminator proof-electric-terminator541,17823 -(defun proof-electric-terminator-enable proof-electric-terminator-enable551,18170 -(defun proof-electric-term-incomment-fn proof-electric-term-incomment-fn562,18657 -(defun proof-process-electric-terminator proof-process-electric-terminator582,19413 -(defun proof-electric-terminator proof-electric-terminator609,20564 -(defun proof-add-completions proof-add-completions631,21202 -(defun proof-script-complete proof-script-complete651,21959 -(defun pg-insert-last-output-as-comment pg-insert-last-output-as-comment679,22550 -(defun pg-copy-span-contents pg-copy-span-contents710,23778 -(defun pg-numth-span-higher-or-lower pg-numth-span-higher-or-lower727,24338 -(defun pg-control-span-of pg-control-span-of753,25089 -(defun pg-move-span-contents pg-move-span-contents759,25293 -(defun pg-fixup-children-span pg-fixup-children-span813,27517 -(defun pg-move-region-down pg-move-region-down820,27725 -(defun pg-move-region-up pg-move-region-up829,28019 -(defun proof-forward-command proof-forward-command859,28859 -(defun proof-backward-command proof-backward-command880,29581 -(defvar pg-span-context-menu-keymappg-span-context-menu-keymap896,29825 -(defun pg-span-for-event pg-span-for-event912,30252 -(defun pg-span-context-menu pg-span-context-menu923,30636 -(defun pg-toggle-visibility pg-toggle-visibility938,31096 -(defun pg-create-in-span-context-menu pg-create-in-span-context-menu948,31418 -(defun pg-goals-buffers-hint pg-goals-buffers-hint1020,33971 -(defun pg-response-buffers-hint pg-response-buffers-hint1023,34138 -(defun pg-jump-to-end-hint pg-jump-to-end-hint1029,34360 -(defun pg-processing-complete-hint pg-processing-complete-hint1032,34476 -(defun pg-hint pg-hint1048,35162 -(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1067,35838 +generic/pg-user.el,3521 +(defmacro proof-maybe-save-point proof-maybe-save-point21,410 +(defun proof-maybe-follow-locked-end proof-maybe-follow-locked-end29,612 +(defun proof-assert-next-command-interactive proof-assert-next-command-interactive43,977 +(defun proof-process-buffer proof-process-buffer53,1348 +(defun proof-undo-last-successful-command proof-undo-last-successful-command67,1665 +(defun proof-undo-and-delete-last-successful-command proof-undo-and-delete-last-successful-command72,1827 +(defun proof-undo-last-successful-command-1 proof-undo-last-successful-command-194,2799 +(defun proof-retract-buffer proof-retract-buffer110,3364 +(defun proof-retract-current-goal proof-retract-current-goal119,3644 +(defun proof-interrupt-process proof-interrupt-process137,4135 +(defun proof-goto-command-start proof-goto-command-start164,5120 +(defun proof-goto-command-end proof-goto-command-end187,6062 +(defun proof-mouse-goto-point proof-mouse-goto-point212,6842 +(defun proof-mouse-track-insert proof-mouse-track-insert227,7416 +(defvar proof-minibuffer-history proof-minibuffer-history262,8526 +(defun proof-minibuffer-cmd proof-minibuffer-cmd265,8620 +(defun proof-frob-locked-end proof-frob-locked-end313,10426 +(defmacro proof-if-setting-configured proof-if-setting-configured406,13340 +(defmacro proof-define-assistant-command proof-define-assistant-command413,13595 +(defmacro proof-define-assistant-command-witharg proof-define-assistant-command-witharg425,14046 +(defun proof-issue-new-command proof-issue-new-command445,14852 +(defun proof-cd-sync proof-cd-sync490,16351 +(deflocal proof-electric-terminator proof-electric-terminator541,17820 +(defun proof-electric-terminator-enable proof-electric-terminator-enable551,18167 +(defun proof-electric-term-incomment-fn proof-electric-term-incomment-fn562,18654 +(defun proof-process-electric-terminator proof-process-electric-terminator582,19410 +(defun proof-electric-terminator proof-electric-terminator609,20561 +(defun proof-add-completions proof-add-completions631,21199 +(defun proof-script-complete proof-script-complete651,21956 +(defun pg-insert-last-output-as-comment pg-insert-last-output-as-comment679,22547 +(defun pg-copy-span-contents pg-copy-span-contents710,23775 +(defun pg-numth-span-higher-or-lower pg-numth-span-higher-or-lower727,24335 +(defun pg-control-span-of pg-control-span-of753,25086 +(defun pg-move-span-contents pg-move-span-contents759,25290 +(defun pg-fixup-children-span pg-fixup-children-span813,27514 +(defun pg-move-region-down pg-move-region-down820,27722 +(defun pg-move-region-up pg-move-region-up829,28016 +(defun proof-forward-command proof-forward-command859,28856 +(defun proof-backward-command proof-backward-command880,29578 +(defvar pg-span-context-menu-keymappg-span-context-menu-keymap896,29822 +(defun pg-span-for-event pg-span-for-event912,30249 +(defun pg-span-context-menu pg-span-context-menu923,30633 +(defun pg-toggle-visibility pg-toggle-visibility938,31093 +(defun pg-create-in-span-context-menu pg-create-in-span-context-menu948,31415 +(defun pg-goals-buffers-hint pg-goals-buffers-hint1020,33968 +(defun pg-response-buffers-hint pg-response-buffers-hint1023,34135 +(defun pg-jump-to-end-hint pg-jump-to-end-hint1032,34489 +(defun pg-processing-complete-hint pg-processing-complete-hint1035,34605 +(defun pg-hint pg-hint1051,35291 +(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1070,35967 +(defun proof-imenu-enable proof-imenu-enable1115,37594 generic/pg-xhtml.el,573 (defvar pg-xhtml-dir pg-xhtml-dir17,423 @@ -488,240 +469,246 @@ generic/_pkg.el,0 generic/proof-autoloads.el,0 -generic/proof-compat.el,938 +generic/proof-compat.el,999 (defun pg-custom-undeclare-variable pg-custom-undeclare-variable28,1002 (defun subst-char-in-string subst-char-in-string99,3142 (defun replace-regexp-in-string replace-regexp-in-string112,3633 (defconst menuvisiblep menuvisiblep174,6346 (defun set-window-text-height set-window-text-height191,6965 -(defun warn warn246,8849 -(defun redraw-modeline redraw-modeline253,9104 -(defun replace-in-string replace-in-string268,9671 -(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate317,11189 -(defvar read-shell-command-mapread-shell-command-map350,12496 -(defun read-shell-command read-shell-command368,13198 -(defun remassq remassq380,13679 -(defun remassoc remassoc392,14068 -(defun frames-of-buffer frames-of-buffer405,14513 -(defmacro with-selected-window with-selected-window444,15776 -(defun pg-pop-to-buffer pg-pop-to-buffer480,16901 -(defun process-live-p process-live-p531,18753 - -generic/proof-config.el,15985 -(defgroup proof-user-options proof-user-options84,3174 -(defcustom proof-electric-terminator-enable proof-electric-terminator-enable89,3288 -(defcustom proof-toolbar-enable proof-toolbar-enable101,3822 -(defpgcustom x-symbol-enable x-symbol-enable108,4060 -(defpgcustom mmm-enable mmm-enable117,4410 -(defcustom pg-show-hints pg-show-hints126,4764 -(defcustom proof-output-fontify-enable proof-output-fontify-enable131,4899 -(defcustom proof-trace-output-slow-catchup proof-trace-output-slow-catchup141,5281 -(defcustom proof-strict-state-preserving proof-strict-state-preserving151,5779 -(defcustom proof-strict-read-only proof-strict-read-only164,6388 -(defcustom proof-three-window-mode proof-three-window-mode174,6738 -(defcustom proof-multiple-frames-enable proof-multiple-frames-enable192,7467 -(defcustom proof-delete-empty-windows proof-delete-empty-windows201,7803 -(defcustom proof-shrink-windows-tofit proof-shrink-windows-tofit212,8334 -(defcustom proof-toolbar-use-button-enablers proof-toolbar-use-button-enablers219,8606 -(defcustom proof-query-file-save-when-activating-scripting proof-query-file-save-when-activating-scripting242,9478 -(defpgcustom script-indent script-indent258,10201 -(defcustom proof-one-command-per-line proof-one-command-per-line264,10389 -(defcustom proof-prog-name-ask proof-prog-name-ask272,10609 -(defcustom proof-prog-name-guess proof-prog-name-guess278,10770 -(defcustom proof-tidy-responseproof-tidy-response286,11030 -(defcustom proof-show-debug-messages proof-show-debug-messages300,11497 -(defcustom proof-experimental-features proof-experimental-features309,11875 -(defcustom proof-follow-mode proof-follow-mode327,12637 -(defcustom proof-auto-action-when-deactivating-scripting proof-auto-action-when-deactivating-scripting353,13832 -(defcustom proof-script-command-separator proof-script-command-separator376,14783 -(defcustom proof-rsh-command proof-rsh-command384,15076 -(defcustom proof-disappearing-proofs proof-disappearing-proofs400,15613 -(defgroup proof-faces proof-faces427,16263 -(defmacro proof-face-specs proof-face-specs432,16369 -(defface proof-queue-face proof-queue-face447,16815 -(defface proof-locked-faceproof-locked-face455,17088 -(defface proof-declaration-name-faceproof-declaration-name-face463,17346 -(defconst proof-declaration-name-face proof-declaration-name-face475,17739 -(defface proof-tacticals-name-faceproof-tacticals-name-face480,17975 -(defconst proof-tacticals-name-face proof-tacticals-name-face489,18237 -(defface proof-tactics-name-faceproof-tactics-name-face494,18467 -(defconst proof-tactics-name-face proof-tactics-name-face503,18732 -(defface proof-error-face proof-error-face508,18956 -(defface proof-warning-faceproof-warning-face516,19160 -(defface proof-eager-annotation-faceproof-eager-annotation-face525,19417 -(defface proof-debug-message-faceproof-debug-message-face533,19635 -(defface proof-boring-faceproof-boring-face541,19834 -(defface proof-mouse-highlight-faceproof-mouse-highlight-face549,20026 -(defface proof-highlight-dependent-faceproof-highlight-dependent-face557,20222 -(defface proof-highlight-dependency-faceproof-highlight-dependency-face565,20431 -(defgroup prover-config prover-config583,20690 -(defcustom proof-mode-for-shell proof-mode-for-shell617,21809 -(defcustom proof-mode-for-response proof-mode-for-response624,22056 -(defcustom proof-mode-for-goals proof-mode-for-goals631,22339 -(defcustom proof-mode-for-script proof-mode-for-script638,22594 -(defcustom proof-guess-command-line proof-guess-command-line649,23028 -(defcustom proof-assistant-home-page proof-assistant-home-page664,23525 -(defcustom proof-context-command proof-context-command670,23695 -(defcustom proof-info-command proof-info-command675,23829 -(defcustom proof-showproof-command proof-showproof-command682,24101 -(defcustom proof-goal-command proof-goal-command687,24237 -(defcustom proof-save-command proof-save-command695,24535 -(defcustom proof-find-theorems-command proof-find-theorems-command703,24845 -(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default710,25154 -(defpgcustom toolbar-entries toolbar-entries741,26886 -(defcustom proof-assistant-true-value proof-assistant-true-value759,27607 -(defcustom proof-assistant-false-value proof-assistant-false-value765,27797 -(defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn771,27991 -(defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn778,28240 -(defcustom proof-assistant-setting-format proof-assistant-setting-format785,28507 -(defgroup proof-script proof-script807,29202 -(defcustom proof-terminal-char proof-terminal-char812,29332 -(defcustom proof-script-sexp-commands proof-script-sexp-commands822,29736 -(defcustom proof-script-command-end-regexp proof-script-command-end-regexp833,30206 -(defcustom proof-script-command-start-regexp proof-script-command-start-regexp851,31025 -(defcustom proof-script-use-old-parser proof-script-use-old-parser862,31487 -(defcustom proof-script-integral-proofs proof-script-integral-proofs874,31976 -(defcustom proof-script-fly-past-comments proof-script-fly-past-comments889,32632 -(defcustom proof-script-parse-function proof-script-parse-function896,32938 -(defcustom proof-script-comment-start proof-script-comment-start914,33584 -(defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp925,34019 -(defcustom proof-script-comment-end proof-script-comment-end933,34336 -(defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp942,34667 -(defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn950,34978 -(defcustom proof-string-start-regexp proof-string-start-regexp956,35230 -(defcustom proof-string-end-regexp proof-string-end-regexp961,35395 -(defcustom proof-case-fold-search proof-case-fold-search966,35556 -(defcustom proof-save-command-regexp proof-save-command-regexp975,35972 -(defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp980,36083 -(defcustom proof-save-with-hole-result proof-save-with-hole-result992,36535 -(defcustom proof-goal-command-regexp proof-goal-command-regexp1003,36999 -(defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1012,37391 -(defcustom proof-goal-with-hole-result proof-goal-with-hole-result1024,37838 -(defcustom proof-non-undoables-regexp proof-non-undoables-regexp1034,38237 -(defcustom proof-nested-undo-regexp proof-nested-undo-regexp1045,38693 -(defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1061,39405 -(defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1069,39708 -(defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1113,41442 -(defcustom proof-goal-command-p proof-goal-command-p1139,42670 -(defcustom proof-really-save-command-p proof-really-save-command-p1166,44106 -(defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1178,44567 -(defcustom proof-count-undos-fn proof-count-undos-fn1206,45927 -(defconst proof-no-command proof-no-command1241,47528 -(defcustom proof-find-and-forget-fn proof-find-and-forget-fn1246,47732 -(defcustom proof-forget-id-command proof-forget-id-command1263,48443 -(defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1273,48801 -(defcustom proof-kill-goal-command proof-kill-goal-command1285,49282 -(defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1299,49792 -(defcustom proof-nested-goals-history-p proof-nested-goals-history-p1313,50341 -(defcustom proof-state-preserving-p proof-state-preserving-p1322,50679 -(defcustom proof-activate-scripting-hook proof-activate-scripting-hook1332,51149 -(defcustom proof-indent proof-indent1355,51962 -(defcustom proof-indent-pad-eol proof-indent-pad-eol1361,52136 -(defcustom proof-indent-hang proof-indent-hang1368,52376 -(defcustom proof-indent-enclose-offset proof-indent-enclose-offset1373,52502 -(defcustom proof-indent-open-offset proof-indent-open-offset1378,52644 -(defcustom proof-indent-close-offset proof-indent-close-offset1383,52781 -(defcustom proof-indent-any-regexp proof-indent-any-regexp1388,52919 -(defcustom proof-indent-inner-regexp proof-indent-inner-regexp1393,53079 -(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1398,53233 -(defcustom proof-indent-open-regexp proof-indent-open-regexp1403,53387 -(defcustom proof-indent-close-regexp proof-indent-close-regexp1408,53539 -(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1414,53693 -(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1426,54066 -(defgroup proof-shell proof-shell1452,54855 -(defcustom proof-prog-name proof-prog-name1462,55026 -(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1471,55381 -(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1480,55778 -(defcustom proof-shell-init-cmd proof-shell-init-cmd1494,56337 -(defcustom proof-shell-restart-cmd proof-shell-restart-cmd1505,56807 -(defcustom proof-shell-quit-cmd proof-shell-quit-cmd1510,56962 -(defcustom proof-shell-quit-timeout proof-shell-quit-timeout1515,57129 -(defcustom proof-shell-cd-cmd proof-shell-cd-cmd1525,57577 -(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1542,58244 -(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1551,58620 -(defcustom proof-shell-silent-threshold proof-shell-silent-threshold1560,58957 -(defcustom proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1568,59291 -(defcustom proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1589,60214 -(defcustom proof-auto-multiple-files proof-auto-multiple-files1612,61255 -(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1638,62080 -(defcustom proof-shell-wakeup-char proof-shell-wakeup-char1648,62502 -(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1654,62733 -(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1670,63373 -(defcustom proof-shell-error-regexp proof-shell-error-regexp1675,63508 -(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1695,64302 -(defcustom pg-next-error-regexp pg-next-error-regexp1709,64845 -(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1724,65455 -(defcustom pg-next-error-extract-filename pg-next-error-extract-filename1748,66493 -(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1755,66736 -(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1769,67328 -(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1782,67836 -(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1789,68135 -(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1796,68428 -(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1804,68795 -(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1810,69037 -(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1828,69775 -(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1839,70202 -(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1855,70878 -(defcustom proof-shell-process-file proof-shell-process-file1865,71290 -(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1887,72242 -(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1896,72578 -(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1908,73123 -(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp1916,73447 -(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd1949,74919 -(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd1958,75249 -(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd1967,75605 -(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp1974,75865 -(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split1990,76525 -(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd1999,76950 -(defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2006,77219 -(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2029,78300 -(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2045,78844 -(defcustom proof-shell-filename-escapes proof-shell-filename-escapes2057,79229 -(defcustom proof-shell-process-connection-type proof-shell-process-connection-type2074,79909 -(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2094,80787 -(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2106,81276 -(defcustom proof-shell-insert-hook proof-shell-insert-hook2114,81644 -(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2154,83608 -(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2170,84080 -(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2176,84295 -(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2191,84909 -(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2201,85279 -(defcustom proof-state-change-hook proof-state-change-hook2220,86144 -(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2231,86526 -(defgroup proof-goals proof-goals2245,86883 -(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2250,87004 -(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2258,87316 -(defcustom pg-goals-change-goal pg-goals-change-goal2267,87620 -(defcustom pbp-goal-command pbp-goal-command2272,87735 -(defcustom pbp-hyp-command pbp-hyp-command2277,87891 -(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2282,88053 -(defcustom pg-goals-error-regexp pg-goals-error-regexp2289,88289 -(defcustom proof-shell-result-start proof-shell-result-start2294,88449 -(defcustom proof-shell-result-end proof-shell-result-end2300,88683 -(defcustom pg-subterm-start-char pg-subterm-start-char2306,88896 -(defcustom pg-subterm-sep-char pg-subterm-sep-char2320,89478 -(defcustom pg-subterm-end-char pg-subterm-end-char2326,89657 -(defcustom pg-topterm-char pg-topterm-char2332,89814 -(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2349,90420 -(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2363,91099 -(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2375,91677 -(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2383,92037 -(defgroup proof-x-symbol proof-x-symbol2395,92291 -(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2400,92419 -(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2413,93048 -(defcustom proof-xsym-activate-command proof-xsym-activate-command2421,93425 -(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2428,93661 -(defpgcustom x-symbol-language x-symbol-language2435,93903 -(defpgcustom favourites favourites2450,94350 -(defpgcustom menu-entries menu-entries2455,94540 -(defpgcustom help-menu-entries help-menu-entries2462,94777 -(defpgcustom keymap keymap2469,95040 -(defpgcustom completion-table completion-table2474,95211 -(defpgcustom tags-program tags-program2484,95576 -(defcustom proof-general-name proof-general-name2496,95749 -(defcustom proof-general-home-pageproof-general-home-page2501,95906 -(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2507,96065 -(defcustom proof-universal-keysproof-universal-keys2515,96341 +(defmacro save-selected-frame save-selected-frame217,7915 +(defun warn warn256,9217 +(defun redraw-modeline redraw-modeline263,9472 +(defun replace-in-string replace-in-string278,10039 +(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate327,11557 +(defvar read-shell-command-mapread-shell-command-map360,12864 +(defun read-shell-command read-shell-command378,13566 +(defun remassq remassq390,14047 +(defun remassoc remassoc402,14436 +(defun frames-of-buffer frames-of-buffer415,14881 +(defmacro with-selected-window with-selected-window454,16144 +(defun pg-pop-to-buffer pg-pop-to-buffer490,17269 +(defun process-live-p process-live-p541,19121 + +generic/proof-config.el,16423 +(defgroup proof-user-options proof-user-options84,3173 +(defcustom proof-electric-terminator-enable proof-electric-terminator-enable89,3287 +(defcustom proof-toolbar-enable proof-toolbar-enable101,3821 +(defcustom proof-imenu-enable proof-imenu-enable107,3994 +(defpgcustom x-symbol-enable x-symbol-enable113,4165 +(defpgcustom mmm-enable mmm-enable122,4515 +(defcustom pg-show-hints pg-show-hints131,4869 +(defcustom proof-output-fontify-enable proof-output-fontify-enable136,5004 +(defcustom proof-trace-output-slow-catchup proof-trace-output-slow-catchup146,5386 +(defcustom proof-strict-state-preserving proof-strict-state-preserving156,5884 +(defcustom proof-strict-read-only proof-strict-read-only169,6493 +(defcustom proof-three-window-enable proof-three-window-enable179,6843 +(defcustom proof-multiple-frames-enable proof-multiple-frames-enable198,7598 +(defcustom proof-delete-empty-windows proof-delete-empty-windows207,7934 +(defcustom proof-shrink-windows-tofit proof-shrink-windows-tofit218,8465 +(defcustom proof-toolbar-use-button-enablers proof-toolbar-use-button-enablers225,8737 +(defcustom proof-query-file-save-when-activating-scripting proof-query-file-save-when-activating-scripting248,9609 +(defpgcustom script-indent script-indent264,10332 +(defcustom proof-one-command-per-line proof-one-command-per-line270,10520 +(defcustom proof-prog-name-ask proof-prog-name-ask278,10740 +(defcustom proof-prog-name-guess proof-prog-name-guess284,10901 +(defcustom proof-tidy-responseproof-tidy-response292,11161 +(defcustom proof-show-debug-messages proof-show-debug-messages306,11628 +(defcustom proof-experimental-features proof-experimental-features315,12006 +(defcustom proof-follow-mode proof-follow-mode333,12768 +(defcustom proof-auto-action-when-deactivating-scripting proof-auto-action-when-deactivating-scripting359,13963 +(defcustom proof-script-command-separator proof-script-command-separator382,14914 +(defcustom proof-rsh-command proof-rsh-command390,15207 +(defcustom proof-disappearing-proofs proof-disappearing-proofs406,15744 +(defgroup proof-faces proof-faces433,16394 +(defmacro proof-face-specs proof-face-specs438,16500 +(defface proof-queue-face proof-queue-face453,16946 +(defface proof-locked-faceproof-locked-face461,17219 +(defface proof-declaration-name-faceproof-declaration-name-face469,17477 +(defconst proof-declaration-name-face proof-declaration-name-face481,17870 +(defface proof-tacticals-name-faceproof-tacticals-name-face486,18106 +(defconst proof-tacticals-name-face proof-tacticals-name-face495,18368 +(defface proof-tactics-name-faceproof-tactics-name-face500,18598 +(defconst proof-tactics-name-face proof-tactics-name-face509,18863 +(defface proof-error-face proof-error-face514,19087 +(defface proof-warning-faceproof-warning-face522,19294 +(defface proof-eager-annotation-faceproof-eager-annotation-face531,19551 +(defface proof-debug-message-faceproof-debug-message-face539,19769 +(defface proof-boring-faceproof-boring-face547,19968 +(defface proof-mouse-highlight-faceproof-mouse-highlight-face555,20160 +(defface proof-highlight-dependent-faceproof-highlight-dependent-face563,20356 +(defface proof-highlight-dependency-faceproof-highlight-dependency-face571,20565 +(defgroup prover-config prover-config589,20824 +(defcustom proof-mode-for-shell proof-mode-for-shell623,21943 +(defcustom proof-mode-for-response proof-mode-for-response630,22190 +(defcustom proof-mode-for-goals proof-mode-for-goals637,22473 +(defcustom proof-mode-for-script proof-mode-for-script644,22728 +(defcustom proof-guess-command-line proof-guess-command-line655,23162 +(defcustom proof-assistant-home-page proof-assistant-home-page670,23659 +(defcustom proof-context-command proof-context-command676,23829 +(defcustom proof-info-command proof-info-command681,23963 +(defcustom proof-showproof-command proof-showproof-command688,24235 +(defcustom proof-goal-command proof-goal-command693,24371 +(defcustom proof-save-command proof-save-command701,24669 +(defcustom proof-find-theorems-command proof-find-theorems-command709,24979 +(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default716,25288 +(defpgcustom toolbar-entries toolbar-entries747,27020 +(defcustom proof-assistant-true-value proof-assistant-true-value765,27741 +(defcustom proof-assistant-false-value proof-assistant-false-value771,27931 +(defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn777,28125 +(defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn784,28374 +(defcustom proof-assistant-setting-format proof-assistant-setting-format791,28641 +(defgroup proof-script proof-script813,29336 +(defcustom proof-terminal-char proof-terminal-char818,29466 +(defcustom proof-script-sexp-commands proof-script-sexp-commands828,29870 +(defcustom proof-script-command-end-regexp proof-script-command-end-regexp839,30340 +(defcustom proof-script-command-start-regexp proof-script-command-start-regexp857,31159 +(defcustom proof-script-use-old-parser proof-script-use-old-parser868,31621 +(defcustom proof-script-integral-proofs proof-script-integral-proofs880,32110 +(defcustom proof-script-fly-past-comments proof-script-fly-past-comments895,32766 +(defcustom proof-script-parse-function proof-script-parse-function902,33083 +(defcustom proof-script-comment-start proof-script-comment-start920,33729 +(defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp931,34164 +(defcustom proof-script-comment-end proof-script-comment-end939,34481 +(defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp951,34899 +(defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn959,35210 +(defcustom proof-string-start-regexp proof-string-start-regexp965,35462 +(defcustom proof-string-end-regexp proof-string-end-regexp970,35627 +(defcustom proof-case-fold-search proof-case-fold-search975,35788 +(defcustom proof-save-command-regexp proof-save-command-regexp984,36204 +(defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp989,36315 +(defcustom proof-save-with-hole-result proof-save-with-hole-result1001,36767 +(defcustom proof-goal-command-regexp proof-goal-command-regexp1012,37231 +(defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1021,37623 +(defcustom proof-goal-with-hole-result proof-goal-with-hole-result1033,38067 +(defcustom proof-non-undoables-regexp proof-non-undoables-regexp1043,38466 +(defcustom proof-nested-undo-regexp proof-nested-undo-regexp1054,38922 +(defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1070,39634 +(defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1078,39937 +(defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1122,41671 +(defcustom proof-script-imenu-generic-expression proof-script-imenu-generic-expression1142,42501 +(defcustom proof-goal-command-p proof-goal-command-p1157,43162 +(defcustom proof-really-save-command-p proof-really-save-command-p1184,44598 +(defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1196,45059 +(defcustom proof-count-undos-fn proof-count-undos-fn1224,46419 +(defconst proof-no-command proof-no-command1259,48020 +(defcustom proof-find-and-forget-fn proof-find-and-forget-fn1264,48224 +(defcustom proof-forget-id-command proof-forget-id-command1281,48935 +(defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1291,49293 +(defcustom proof-kill-goal-command proof-kill-goal-command1303,49774 +(defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1317,50284 +(defcustom proof-nested-goals-history-p proof-nested-goals-history-p1331,50833 +(defcustom proof-state-preserving-p proof-state-preserving-p1340,51171 +(defcustom proof-activate-scripting-hook proof-activate-scripting-hook1350,51641 +(defcustom proof-indent proof-indent1373,52454 +(defcustom proof-indent-pad-eol proof-indent-pad-eol1379,52628 +(defcustom proof-indent-hang proof-indent-hang1386,52868 +(defcustom proof-indent-enclose-offset proof-indent-enclose-offset1391,52994 +(defcustom proof-indent-open-offset proof-indent-open-offset1396,53136 +(defcustom proof-indent-close-offset proof-indent-close-offset1401,53273 +(defcustom proof-indent-any-regexp proof-indent-any-regexp1406,53411 +(defcustom proof-indent-inner-regexp proof-indent-inner-regexp1411,53571 +(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1416,53725 +(defcustom proof-indent-open-regexp proof-indent-open-regexp1421,53879 +(defcustom proof-indent-close-regexp proof-indent-close-regexp1426,54031 +(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1432,54185 +(defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries1440,54508 +(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1458,54905 +(defgroup proof-shell proof-shell1484,55694 +(defcustom proof-prog-name proof-prog-name1494,55865 +(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1503,56220 +(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1512,56617 +(defcustom proof-shell-init-cmd proof-shell-init-cmd1526,57176 +(defcustom proof-shell-restart-cmd proof-shell-restart-cmd1537,57646 +(defcustom proof-shell-quit-cmd proof-shell-quit-cmd1542,57801 +(defcustom proof-shell-quit-timeout proof-shell-quit-timeout1547,57968 +(defcustom proof-shell-cd-cmd proof-shell-cd-cmd1557,58416 +(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1574,59083 +(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1583,59459 +(defcustom proof-shell-silent-threshold proof-shell-silent-threshold1592,59796 +(defcustom proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1600,60130 +(defcustom proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1621,61053 +(defcustom proof-auto-multiple-files proof-auto-multiple-files1644,62094 +(defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files1659,62815 +(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1684,63612 +(defcustom proof-shell-wakeup-char proof-shell-wakeup-char1694,64034 +(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1700,64265 +(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1716,64905 +(defcustom proof-shell-error-regexp proof-shell-error-regexp1721,65040 +(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1741,65834 +(defcustom pg-next-error-regexp pg-next-error-regexp1755,66377 +(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1770,66987 +(defcustom pg-next-error-extract-filename pg-next-error-extract-filename1794,68025 +(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1801,68268 +(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1815,68860 +(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1828,69368 +(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1835,69667 +(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1842,69960 +(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1850,70327 +(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1856,70569 +(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1874,71307 +(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1885,71734 +(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1901,72410 +(defcustom proof-shell-process-file proof-shell-process-file1911,72822 +(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1933,73774 +(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1942,74110 +(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1954,74655 +(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp1962,74979 +(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd1995,76451 +(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd2004,76781 +(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd2013,77137 +(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp2020,77397 +(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split2036,78057 +(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd2045,78482 +(defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2052,78751 +(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2075,79832 +(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2091,80376 +(defcustom proof-shell-filename-escapes proof-shell-filename-escapes2103,80761 +(defcustom proof-shell-process-connection-type proof-shell-process-connection-type2120,81441 +(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2140,82319 +(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2152,82808 +(defcustom proof-shell-insert-hook proof-shell-insert-hook2160,83176 +(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2200,85140 +(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2216,85612 +(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2222,85827 +(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2237,86441 +(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2247,86811 +(defcustom proof-state-change-hook proof-state-change-hook2266,87676 +(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2277,88058 +(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2285,88386 +(defgroup proof-goals proof-goals2303,88758 +(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2308,88879 +(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2316,89191 +(defcustom pg-goals-change-goal pg-goals-change-goal2325,89495 +(defcustom pbp-goal-command pbp-goal-command2330,89610 +(defcustom pbp-hyp-command pbp-hyp-command2335,89766 +(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2340,89928 +(defcustom pg-goals-error-regexp pg-goals-error-regexp2347,90164 +(defcustom proof-shell-result-start proof-shell-result-start2352,90324 +(defcustom proof-shell-result-end proof-shell-result-end2358,90558 +(defcustom pg-subterm-start-char pg-subterm-start-char2364,90771 +(defcustom pg-subterm-sep-char pg-subterm-sep-char2378,91353 +(defcustom pg-subterm-end-char pg-subterm-end-char2384,91532 +(defcustom pg-topterm-char pg-topterm-char2390,91689 +(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2407,92295 +(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2421,92974 +(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2433,93552 +(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2441,93912 +(defgroup proof-x-symbol proof-x-symbol2453,94166 +(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2458,94294 +(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2471,94923 +(defcustom proof-xsym-activate-command proof-xsym-activate-command2479,95300 +(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2486,95536 +(defpgcustom x-symbol-language x-symbol-language2493,95778 +(defpgcustom favourites favourites2508,96225 +(defpgcustom menu-entries menu-entries2513,96415 +(defpgcustom help-menu-entries help-menu-entries2520,96652 +(defpgcustom keymap keymap2527,96915 +(defpgcustom completion-table completion-table2532,97086 +(defpgcustom tags-program tags-program2542,97451 +(defcustom proof-general-name proof-general-name2554,97624 +(defcustom proof-general-home-pageproof-general-home-page2559,97781 +(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2565,97940 +(defcustom proof-universal-keysproof-universal-keys2573,98216 generic/proof-depends.el,1325 (defvar proof-thm-names-of-files proof-thm-names-of-files19,540 @@ -747,8 +734,8 @@ generic/proof-depends.el,1325 generic/proof-easy-config.el,317 (defconst proof-easy-config-derived-modes-tableproof-easy-config-derived-modes-table15,492 (defun proof-easy-config-define-derived-modes proof-easy-config-define-derived-modes22,898 -(defun proof-easy-config-check-setup proof-easy-config-check-setup57,2460 -(defmacro proof-easy-config proof-easy-config89,3785 +(defun proof-easy-config-check-setup proof-easy-config-check-setup59,2510 +(defmacro proof-easy-config proof-easy-config91,3835 generic/proof.el,809 (deflocal proof-buffer-type proof-buffer-type35,900 @@ -766,320 +753,326 @@ generic/proof.el,809 (defvar proof-terminal-string proof-terminal-string109,3861 generic/proof-indent.el,475 -(defun proof-indent-indent proof-indent-indent13,357 -(defun proof-indent-offset proof-indent-offset22,623 -(defun proof-indent-inner-p proof-indent-inner-p39,1223 -(defun proof-indent-goto-prev proof-indent-goto-prev48,1530 -(defun proof-indent-calculate proof-indent-calculate55,1863 -(defun proof-indent-line proof-indent-line74,2579 -(defun proof-indent-pad-eol proof-indent-pad-eol98,3380 -(defun proof-indent-pad-eol-region proof-indent-pad-eol-region116,3974 - -generic/proof-menu.el,4163 -(defvar proof-display-some-buffers-count proof-display-some-buffers-count19,468 -(defun proof-display-some-buffers proof-display-some-buffers21,513 -(defun proof-menu-define-keys proof-menu-define-keys81,2842 -(define-key map map84,2990 -(define-key map map85,3042 -(define-key map map86,3093 -(define-key map map87,3146 -(define-key map map88,3200 -(define-key map map89,3262 -(define-key map map90,3322 -(define-key map map91,3384 -(define-key map map93,3505 -(define-key map map94,3569 -(define-key map map95,3624 -(define-key map map96,3695 -(define-key map map97,3777 -(define-key map map98,3831 -(define-key map map99,3896 -(define-key map map100,3970 -(define-key map map101,4025 -(define-key map map103,4163 -(define-key map map104,4229 -(define-key map map106,4379 -(define-key map map107,4449 -(define-key map map108,4515 -(define-key map map110,4630 -(define-key map map111,4693 -(define-key map map113,4778 -(define-key map map120,5104 -(define-key map map121,5163 -(defun proof-menu-define-main proof-menu-define-main141,5753 -(defun proof-menu-define-specific proof-menu-define-specific151,5954 -(defun proof-assistant-menu-update proof-assistant-menu-update186,6971 -(defvar proof-help-menuproof-help-menu200,7402 -(defvar proof-show-hide-menuproof-show-hide-menu208,7680 -(defvar proof-buffer-menuproof-buffer-menu217,7993 -(defvar proof-quick-opts-menuproof-quick-opts-menu271,9982 -(defun proof-quick-opts-vars proof-quick-opts-vars374,14225 -(defun proof-quick-opts-changed-from-defaults-p proof-quick-opts-changed-from-defaults-p396,14882 -(defun proof-quick-opts-changed-from-saved-p proof-quick-opts-changed-from-saved-p400,14987 -(defun proof-quick-opts-save proof-quick-opts-save411,15339 -(defun proof-quick-opts-reset proof-quick-opts-reset416,15507 -(defconst proof-config-menuproof-config-menu428,15775 -(defconst proof-advanced-menuproof-advanced-menu435,15954 -(defvar proof-menu proof-menu453,16600 -(defvar proof-main-menuproof-main-menu462,16884 -(defvar proof-aux-menuproof-aux-menu472,17110 -(defvar proof-menu-favourites proof-menu-favourites488,17432 -(defun proof-menu-define-favourites-menu proof-menu-define-favourites-menu491,17539 -(defmacro proof-defshortcut proof-defshortcut512,18210 -(defmacro proof-definvisible proof-definvisible526,18747 -(defun proof-def-favourite proof-def-favourite539,19294 -(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history562,20269 -(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history565,20354 -(defun proof-save-favourites proof-save-favourites568,20440 -(defun proof-del-favourite proof-del-favourite573,20588 -(defun proof-read-favourite proof-read-favourite590,21149 -(defun proof-add-favourite proof-add-favourite615,21952 -(defvar proof-assistant-settings proof-assistant-settings642,23003 -(defvar proof-menu-settings proof-menu-settings649,23366 -(defun proof-menu-define-settings-menu proof-menu-define-settings-menu652,23440 -(defun proof-menu-entry-name proof-menu-entry-name670,24084 -(defun proof-menu-entry-for-setting proof-menu-entry-for-setting675,24243 -(defun proof-settings-vars proof-settings-vars693,24733 -(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p698,24910 -(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p702,25016 -(defun proof-settings-save proof-settings-save706,25119 -(defun proof-settings-reset proof-settings-reset711,25286 -(defun proof-defpacustom-fn proof-defpacustom-fn719,25532 -(defmacro defpacustom defpacustom779,27724 -(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs790,28364 -(defun proof-assistant-settings-cmd proof-assistant-settings-cmd810,29214 -(defun proof-assistant-format proof-assistant-format828,29903 -(defvar proof-assistant-format-table proof-assistant-format-table845,30645 -(defun proof-assistant-format-bool proof-assistant-format-bool853,31014 -(defun proof-assistant-format-int proof-assistant-format-int856,31127 -(defun proof-assistant-format-string proof-assistant-format-string859,31219 +(defun proof-indent-indent proof-indent-indent13,353 +(defun proof-indent-offset proof-indent-offset22,619 +(defun proof-indent-inner-p proof-indent-inner-p39,1219 +(defun proof-indent-goto-prev proof-indent-goto-prev48,1526 +(defun proof-indent-calculate proof-indent-calculate55,1859 +(defun proof-indent-line proof-indent-line74,2575 +(defun proof-indent-pad-eol proof-indent-pad-eol98,3376 +(defun proof-indent-pad-eol-region proof-indent-pad-eol-region116,3970 + +generic/proof-menu.el,4254 +(defvar proof-display-some-buffers-count proof-display-some-buffers-count19,467 +(defun proof-display-some-buffers proof-display-some-buffers21,512 +(defun proof-menu-define-keys proof-menu-define-keys80,2714 +(define-key map map83,2862 +(define-key map map84,2914 +(define-key map map85,2965 +(define-key map map86,3018 +(define-key map map87,3072 +(define-key map map88,3134 +(define-key map map89,3194 +(define-key map map90,3256 +(define-key map map92,3377 +(define-key map map93,3441 +(define-key map map94,3496 +(define-key map map95,3567 +(define-key map map96,3632 +(define-key map map97,3714 +(define-key map map98,3768 +(define-key map map99,3833 +(define-key map map100,3907 +(define-key map map101,3962 +(define-key map map103,4100 +(define-key map map104,4166 +(define-key map map106,4316 +(define-key map map107,4386 +(define-key map map108,4452 +(define-key map map110,4567 +(define-key map map111,4630 +(define-key map map113,4715 +(define-key map map120,5041 +(define-key map map121,5100 +(defun proof-menu-define-main proof-menu-define-main141,5690 +(defun proof-menu-define-specific proof-menu-define-specific151,5891 +(defun proof-assistant-menu-update proof-assistant-menu-update186,6908 +(defvar proof-help-menuproof-help-menu200,7339 +(defvar proof-show-hide-menuproof-show-hide-menu208,7617 +(defvar proof-buffer-menuproof-buffer-menu217,7930 +(defconst proof-quick-opts-menuproof-quick-opts-menu272,9922 +(defun proof-quick-opts-vars proof-quick-opts-vars380,14353 +(defun proof-quick-opts-changed-from-defaults-p proof-quick-opts-changed-from-defaults-p403,15035 +(defun proof-quick-opts-changed-from-saved-p proof-quick-opts-changed-from-saved-p407,15140 +(defun proof-quick-opts-save proof-quick-opts-save418,15492 +(defun proof-quick-opts-reset proof-quick-opts-reset423,15660 +(defconst proof-config-menuproof-config-menu435,15928 +(defconst proof-advanced-menuproof-advanced-menu442,16107 +(defvar proof-menu proof-menu461,16888 +(defvar proof-main-menuproof-main-menu470,17172 +(defvar proof-aux-menuproof-aux-menu480,17398 +(defvar proof-menu-favourites proof-menu-favourites496,17720 +(defun proof-menu-define-favourites-menu proof-menu-define-favourites-menu499,17827 +(defmacro proof-defshortcut proof-defshortcut520,18498 +(defmacro proof-definvisible proof-definvisible536,19153 +(defun proof-def-favourite proof-def-favourite551,19772 +(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history574,20747 +(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history577,20832 +(defun proof-save-favourites proof-save-favourites580,20918 +(defun proof-del-favourite proof-del-favourite585,21066 +(defun proof-read-favourite proof-read-favourite602,21627 +(defun proof-add-favourite proof-add-favourite627,22430 +(defvar proof-assistant-settings proof-assistant-settings654,23481 +(defvar proof-menu-settings proof-menu-settings661,23844 +(defun proof-menu-define-settings-menu proof-menu-define-settings-menu664,23918 +(defun proof-menu-entry-name proof-menu-entry-name682,24562 +(defun proof-menu-entry-for-setting proof-menu-entry-for-setting687,24721 +(defun proof-settings-vars proof-settings-vars705,25211 +(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p710,25388 +(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p714,25494 +(defun proof-settings-save proof-settings-save718,25597 +(defun proof-settings-reset proof-settings-reset723,25764 +(defun proof-defpacustom-fn proof-defpacustom-fn731,26010 +(defmacro defpacustom defpacustom791,28202 +(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs802,28842 +(defun proof-maybe-askprefs proof-maybe-askprefs821,29691 +(defun proof-assistant-settings-cmd proof-assistant-settings-cmd828,29895 +(defun proof-assistant-format proof-assistant-format845,30555 +(defvar proof-assistant-format-table proof-assistant-format-table862,31297 +(defun proof-assistant-format-bool proof-assistant-format-bool870,31666 +(defun proof-assistant-format-int proof-assistant-format-int873,31779 +(defun proof-assistant-format-string proof-assistant-format-string876,31871 generic/proof-mmm.el,179 (defun proof-mmm-support-available proof-mmm-support-available25,909 (defun proof-mmm-set-global proof-mmm-set-global49,1757 (defun proof-mmm-enable proof-mmm-enable64,2298 -generic/proof-script.el,8028 -(defvar proof-last-theorem-dependencies proof-last-theorem-dependencies41,1047 -(defvar proof-nesting-depth proof-nesting-depth45,1209 -(defvar proof-element-counters proof-element-counters52,1440 -(deflocal proof-active-buffer-fake-minor-mode proof-active-buffer-fake-minor-mode58,1580 -(deflocal proof-script-buffer-file-name proof-script-buffer-file-name61,1706 -(defun proof-next-element-count proof-next-element-count75,2230 -(defun proof-element-id proof-element-id84,2557 -(defun proof-next-element-id proof-next-element-id88,2726 -(deflocal proof-script-last-entity proof-script-last-entity102,3042 -(defun proof-script-find-next-entity proof-script-find-next-entity109,3322 -(deflocal proof-locked-span proof-locked-span185,6064 -(deflocal proof-queue-span proof-queue-span192,6330 -(defun proof-span-read-only proof-span-read-only204,6844 -(defun proof-strict-read-only proof-strict-read-only211,7101 -(defsubst proof-set-queue-endpoints proof-set-queue-endpoints230,7988 -(defsubst proof-set-locked-endpoints proof-set-locked-endpoints234,8129 -(defsubst proof-detach-queue proof-detach-queue238,8273 -(defsubst proof-detach-locked proof-detach-locked242,8405 -(defsubst proof-set-queue-start proof-set-queue-start246,8541 -(defsubst proof-set-locked-end proof-set-locked-end250,8667 -(defsubst proof-set-queue-end proof-set-queue-end265,9214 -(defun proof-init-segmentation proof-init-segmentation275,9470 -(defun proof-restart-buffers proof-restart-buffers307,10841 -(defun proof-script-buffers-with-spans proof-script-buffers-with-spans329,11763 -(defun proof-script-remove-all-spans-and-deactivate proof-script-remove-all-spans-and-deactivate339,12119 -(defun proof-script-clear-queue-spans proof-script-clear-queue-spans343,12307 -(defun proof-unprocessed-begin proof-unprocessed-begin361,12848 -(defun proof-script-end proof-script-end369,13102 -(defun proof-queue-or-locked-end proof-queue-or-locked-end378,13403 -(defun proof-locked-end proof-locked-end392,14066 -(defun proof-locked-region-full-p proof-locked-region-full-p408,14436 -(defun proof-locked-region-empty-p proof-locked-region-empty-p416,14693 -(defun proof-only-whitespace-to-locked-region-p proof-only-whitespace-to-locked-region-p420,14843 -(defun proof-in-locked-region-p proof-in-locked-region-p433,15479 -(defun proof-goto-end-of-locked proof-goto-end-of-locked445,15742 -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window456,16238 -(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window470,16863 -(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible491,17813 -(defvar pg-idioms pg-idioms510,18463 -(defvar pg-visibility-specs pg-visibility-specs513,18559 -(deflocal pg-script-portions pg-script-portions518,18766 -(defun pg-clear-script-portions pg-clear-script-portions521,18888 -(defun pg-add-script-element pg-add-script-element539,19552 -(defun pg-remove-script-element pg-remove-script-element542,19628 -(defsubst pg-visname pg-visname550,19906 -(defun pg-add-element pg-add-element554,20051 -(defun pg-open-invisible-span pg-open-invisible-span588,21680 -(defun pg-remove-element pg-remove-element599,22043 -(defun pg-make-element-invisible pg-make-element-invisible606,22313 -(defun pg-make-element-visible pg-make-element-visible612,22570 -(defun pg-toggle-element-visibility pg-toggle-element-visibility617,22749 -(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs625,23079 -(defun pg-show-all-portions pg-show-all-portions632,23350 -(defun pg-show-all-proofs pg-show-all-proofs650,24021 -(defun pg-hide-all-proofs pg-hide-all-proofs655,24149 -(defun pg-add-proof-element pg-add-proof-element660,24280 -(defun pg-span-name pg-span-name674,24900 -(defun pg-set-span-helphighlights pg-set-span-helphighlights695,25606 -(defun proof-complete-buffer-atomic proof-complete-buffer-atomic720,26430 -(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file761,28345 -(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted812,30473 -(defun proof-auto-retract-dependencies proof-auto-retract-dependencies819,30705 -(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name873,33245 -(defun proof-protected-process-or-retract proof-protected-process-or-retract915,34858 -(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto942,36028 -(defun proof-deactivate-scripting proof-deactivate-scripting951,36386 -(defun proof-activate-scripting proof-activate-scripting1085,41678 -(defun proof-toggle-active-scripting proof-toggle-active-scripting1214,47431 -(defun proof-done-advancing proof-done-advancing1255,48792 -(defun proof-done-advancing-comment proof-done-advancing-comment1325,51563 -(defun proof-done-advancing-save proof-done-advancing-save1341,52201 -(defun proof-make-goalsave proof-make-goalsave1434,55814 -(defun proof-get-name-from-goal proof-get-name-from-goal1449,56557 -(defun proof-done-advancing-autosave proof-done-advancing-autosave1468,57583 -(defun proof-done-advancing-other proof-done-advancing-other1532,60100 -(defun proof-segment-up-to-parser proof-segment-up-to-parser1560,61080 -(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1623,63156 -(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1632,63572 -(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1657,64467 -(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1720,67175 -(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1744,68111 -(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1796,70310 -(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1857,72670 -(defun proof-semis-to-vanillas proof-semis-to-vanillas1928,75315 -(defun proof-script-new-command-advance proof-script-new-command-advance1967,76641 -(defun proof-script-next-command-advance proof-script-next-command-advance2009,78382 -(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2021,78823 -(defun proof-assert-until-point proof-assert-until-point2047,79945 -(defun proof-assert-next-commandproof-assert-next-command2100,82377 -(defun proof-goto-point proof-goto-point2148,84640 -(defun proof-insert-pbp-command proof-insert-pbp-command2165,85166 -(defun proof-done-retracting proof-done-retracting2197,86239 -(defun proof-setup-retract-action proof-setup-retract-action2224,87350 -(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2234,87833 -(defun proof-retract-target proof-retract-target2258,88702 -(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2343,92343 -(defun proof-retract-until-point proof-retract-until-point2351,92728 -(define-derived-mode proof-mode proof-mode2386,93903 -(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2419,95196 -(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2443,96198 -(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2453,96694 -(defun proof-config-done-related proof-config-done-related2497,98516 -(defun proof-generic-goal-command-p proof-generic-goal-command-p2559,100792 -(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2563,100967 -(defun proof-generic-count-undos proof-generic-count-undos2572,101484 -(defun proof-generic-find-and-forget proof-generic-find-and-forget2601,102514 -(defconst proof-script-important-settingsproof-script-important-settings2652,104339 -(defun proof-config-done proof-config-done2665,104876 -(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2759,108364 -(defun proof-setup-imenu proof-setup-imenu2803,110217 -(defun proof-setup-func-menu proof-setup-func-menu2817,110679 - -generic/proof-shell.el,5150 -(defvar proof-shell-last-output proof-shell-last-output19,459 -(defvar proof-marker proof-marker63,1715 -(defvar proof-action-list proof-action-list66,1812 -(defvar proof-shell-silent proof-shell-silent74,1988 -(defvar proof-shell-last-prompt proof-shell-last-prompt88,2471 -(defvar proof-shell-last-output-kind proof-shell-last-output-kind93,2701 -(defvar proof-shell-delayed-output proof-shell-delayed-output114,3523 -(defvar proof-shell-delayed-output-kind proof-shell-delayed-output-kind117,3644 -(defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator126,3847 -(defun proof-shell-ready-prover proof-shell-ready-prover179,5323 -(defun proof-shell-live-buffer proof-shell-live-buffer193,5863 -(defun proof-shell-available-p proof-shell-available-p200,6098 -(defun proof-grab-lock proof-grab-lock206,6321 -(defun proof-release-lock proof-release-lock223,7038 -(defun proof-shell-start proof-shell-start243,7594 -(defvar proof-shell-kill-function-hooks proof-shell-kill-function-hooks403,13646 -(defun proof-shell-kill-function proof-shell-kill-function406,13744 -(defun proof-shell-clear-state proof-shell-clear-state490,17261 -(defun proof-shell-exit proof-shell-exit505,17704 -(defun proof-shell-bail-out proof-shell-bail-out517,18149 -(defun proof-shell-restart proof-shell-restart526,18626 -(defvar proof-shell-no-response-display proof-shell-no-response-display568,20010 -(defvar proof-shell-urgent-message-marker proof-shell-urgent-message-marker571,20114 -(defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner574,20235 -(defun proof-shell-handle-output proof-shell-handle-output578,20362 -(defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output652,23699 -(defvar proof-shell-ignore-errors proof-shell-ignore-errors687,25121 -(defun proof-shell-handle-error proof-shell-handle-error693,25323 -(defun proof-shell-handle-interrupt proof-shell-handle-interrupt711,26167 -(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action725,26783 -(defun proof-goals-pos proof-goals-pos743,27609 -(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal748,27814 -(defsubst proof-shell-string-match-safe proof-shell-string-match-safe760,28349 -(defun proof-shell-process-output proof-shell-process-output765,28517 -(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge876,33157 -(defun proof-shell-insert proof-shell-insert885,33466 -(defun proof-shell-command-queue-item proof-shell-command-queue-item953,36000 -(defun proof-shell-set-silent proof-shell-set-silent958,36157 -(defun proof-shell-start-silent-item proof-shell-start-silent-item964,36376 -(defun proof-shell-clear-silent proof-shell-clear-silent970,36568 -(defun proof-shell-stop-silent-item proof-shell-stop-silent-item976,36790 -(defun proof-shell-should-be-silent proof-shell-should-be-silent983,37062 -(defun proof-append-alist proof-append-alist996,37618 -(defun proof-start-queue proof-start-queue1052,39745 -(defun proof-extend-queue proof-extend-queue1063,40094 -(defun proof-shell-exec-loop proof-shell-exec-loop1074,40475 -(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1136,42942 -(defun proof-shell-message proof-shell-message1174,44665 -(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1180,44881 -(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1391,53791 -(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1393,53861 -(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1405,54231 -(defun proof-shell-filter proof-shell-filter1474,57287 -(defun proof-shell-filter-process-output proof-shell-filter-process-output1627,63624 -(defvar pg-last-tracing-output-time pg-last-tracing-output-time1680,65678 -(defvar pg-tracing-slow-mode pg-tracing-slow-mode1683,65784 -(defconst pg-slow-mode-duration pg-slow-mode-duration1686,65873 -(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1689,65955 -(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1692,66083 -(defun pg-tracing-tight-loop pg-tracing-tight-loop1694,66122 -(defun pg-finish-tracing-display pg-finish-tracing-display1737,67864 -(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1748,68134 -(defun proof-shell-show-annotations proof-shell-show-annotations1764,68669 -(defun proof-shell-wait proof-shell-wait1785,69166 -(defun proof-done-invisible proof-done-invisible1805,70076 -(defun proof-shell-invisible-command proof-shell-invisible-command1848,71799 -(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1875,72988 -(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1892,73669 -(define-derived-mode proof-shell-mode proof-shell-mode1912,74173 -(defconst proof-shell-important-settingsproof-shell-important-settings1982,76776 -(defun proof-shell-config-done proof-shell-config-done1987,76876 +generic/proof-script.el,8106 +(defvar proof-last-theorem-dependencies proof-last-theorem-dependencies41,1046 +(defvar proof-nesting-depth proof-nesting-depth45,1208 +(defvar proof-element-counters proof-element-counters52,1439 +(deflocal proof-active-buffer-fake-minor-mode proof-active-buffer-fake-minor-mode58,1579 +(deflocal proof-script-buffer-file-name proof-script-buffer-file-name61,1705 +(defun proof-next-element-count proof-next-element-count75,2229 +(defun proof-element-id proof-element-id84,2556 +(defun proof-next-element-id proof-next-element-id88,2725 +(deflocal proof-script-last-entity proof-script-last-entity102,3041 +(defun proof-script-find-next-entity proof-script-find-next-entity109,3321 +(deflocal proof-locked-span proof-locked-span185,6063 +(deflocal proof-queue-span proof-queue-span192,6329 +(defun proof-span-read-only proof-span-read-only204,6843 +(defun proof-strict-read-only proof-strict-read-only211,7100 +(defsubst proof-set-queue-endpoints proof-set-queue-endpoints230,7987 +(defsubst proof-set-locked-endpoints proof-set-locked-endpoints234,8128 +(defsubst proof-detach-queue proof-detach-queue238,8272 +(defsubst proof-detach-locked proof-detach-locked242,8404 +(defsubst proof-set-queue-start proof-set-queue-start246,8540 +(defsubst proof-set-locked-end proof-set-locked-end250,8666 +(defsubst proof-set-queue-end proof-set-queue-end265,9213 +(defun proof-init-segmentation proof-init-segmentation275,9469 +(defun proof-restart-buffers proof-restart-buffers307,10840 +(defun proof-script-buffers-with-spans proof-script-buffers-with-spans329,11762 +(defun proof-script-remove-all-spans-and-deactivate proof-script-remove-all-spans-and-deactivate339,12118 +(defun proof-script-clear-queue-spans proof-script-clear-queue-spans343,12306 +(defun proof-unprocessed-begin proof-unprocessed-begin361,12847 +(defun proof-script-end proof-script-end369,13101 +(defun proof-queue-or-locked-end proof-queue-or-locked-end378,13402 +(defun proof-locked-end proof-locked-end392,14065 +(defun proof-locked-region-full-p proof-locked-region-full-p408,14435 +(defun proof-locked-region-empty-p proof-locked-region-empty-p416,14692 +(defun proof-only-whitespace-to-locked-region-p proof-only-whitespace-to-locked-region-p420,14842 +(defun proof-in-locked-region-p proof-in-locked-region-p433,15478 +(defun proof-goto-end-of-locked proof-goto-end-of-locked445,15741 +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window456,16237 +(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window467,16718 +(defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p481,17371 +(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible490,17822 +(defvar pg-idioms pg-idioms509,18472 +(defvar pg-visibility-specs pg-visibility-specs512,18568 +(deflocal pg-script-portions pg-script-portions517,18775 +(defun pg-clear-script-portions pg-clear-script-portions520,18897 +(defun pg-add-script-element pg-add-script-element538,19561 +(defun pg-remove-script-element pg-remove-script-element541,19637 +(defsubst pg-visname pg-visname549,19915 +(defun pg-add-element pg-add-element553,20060 +(defun pg-open-invisible-span pg-open-invisible-span587,21689 +(defun pg-remove-element pg-remove-element598,22052 +(defun pg-make-element-invisible pg-make-element-invisible605,22322 +(defun pg-make-element-visible pg-make-element-visible611,22579 +(defun pg-toggle-element-visibility pg-toggle-element-visibility616,22758 +(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs624,23088 +(defun pg-show-all-portions pg-show-all-portions631,23359 +(defun pg-show-all-proofs pg-show-all-proofs649,24030 +(defun pg-hide-all-proofs pg-hide-all-proofs654,24158 +(defun pg-add-proof-element pg-add-proof-element659,24289 +(defun pg-span-name pg-span-name673,24909 +(defun pg-set-span-helphighlights pg-set-span-helphighlights694,25616 +(defun proof-complete-buffer-atomic proof-complete-buffer-atomic719,26440 +(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file760,28355 +(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted811,30483 +(defun proof-auto-retract-dependencies proof-auto-retract-dependencies818,30715 +(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name872,33255 +(defun proof-protected-process-or-retract proof-protected-process-or-retract918,35078 +(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto945,36248 +(defun proof-deactivate-scripting proof-deactivate-scripting954,36606 +(defun proof-activate-scripting proof-activate-scripting1088,41898 +(defun proof-toggle-active-scripting proof-toggle-active-scripting1216,47652 +(defun proof-done-advancing proof-done-advancing1257,49013 +(defun proof-done-advancing-comment proof-done-advancing-comment1327,51784 +(defun proof-done-advancing-save proof-done-advancing-save1346,52526 +(defun proof-make-goalsave proof-make-goalsave1439,56139 +(defun proof-get-name-from-goal proof-get-name-from-goal1454,56882 +(defun proof-done-advancing-autosave proof-done-advancing-autosave1473,57908 +(defun proof-done-advancing-other proof-done-advancing-other1537,60425 +(defun proof-segment-up-to-parser proof-segment-up-to-parser1565,61405 +(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1628,63481 +(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1637,63897 +(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1662,64792 +(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1725,67500 +(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1749,68436 +(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1801,70635 +(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1862,72995 +(defun proof-semis-to-vanillas proof-semis-to-vanillas1933,75640 +(defun proof-script-new-command-advance proof-script-new-command-advance1972,76966 +(defun proof-script-next-command-advance proof-script-next-command-advance2014,78707 +(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2026,79148 +(defun proof-assert-until-point proof-assert-until-point2052,80270 +(defun proof-assert-next-commandproof-assert-next-command2105,82702 +(defun proof-goto-point proof-goto-point2153,84965 +(defun proof-insert-pbp-command proof-insert-pbp-command2170,85491 +(defun proof-done-retracting proof-done-retracting2202,86564 +(defun proof-setup-retract-action proof-setup-retract-action2229,87675 +(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2239,88158 +(defun proof-retract-target proof-retract-target2263,89027 +(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2348,92668 +(defun proof-retract-until-point proof-retract-until-point2356,93053 +(define-derived-mode proof-mode proof-mode2401,94914 +(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2434,96231 +(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2458,97233 +(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2468,97729 +(defun proof-config-done-related proof-config-done-related2512,99551 +(defun proof-generic-goal-command-p proof-generic-goal-command-p2582,102117 +(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2586,102292 +(defun proof-generic-count-undos proof-generic-count-undos2595,102809 +(defun proof-generic-find-and-forget proof-generic-find-and-forget2624,103839 +(defconst proof-script-important-settingsproof-script-important-settings2675,105664 +(defun proof-config-done proof-config-done2688,106201 +(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2785,109749 +(defun proof-setup-imenu proof-setup-imenu2829,111602 +(defun proof-setup-func-menu proof-setup-func-menu2846,112207 + +generic/proof-shell.el,5288 +(defvar proof-shell-last-output proof-shell-last-output19,458 +(defvar proof-marker proof-marker63,1714 +(defvar proof-action-list proof-action-list66,1811 +(defvar proof-shell-silent proof-shell-silent74,1987 +(defvar proof-shell-last-prompt proof-shell-last-prompt88,2470 +(defvar proof-shell-last-output-kind proof-shell-last-output-kind93,2700 +(defvar proof-shell-delayed-output proof-shell-delayed-output114,3522 +(defvar proof-shell-delayed-output-kind proof-shell-delayed-output-kind117,3643 +(defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator126,3846 +(defun proof-shell-ready-prover proof-shell-ready-prover179,5322 +(defun proof-shell-live-buffer proof-shell-live-buffer193,5862 +(defun proof-shell-available-p proof-shell-available-p200,6097 +(defun proof-grab-lock proof-grab-lock206,6320 +(defun proof-release-lock proof-release-lock223,7037 +(defcustom proof-shell-fiddle-frames proof-shell-fiddle-frames243,7593 +(deflocal proof-eagerly-raise proof-eagerly-raise250,7834 +(defun proof-shell-start proof-shell-start253,7940 +(defvar proof-shell-kill-function-hooks proof-shell-kill-function-hooks437,15128 +(defun proof-shell-kill-function proof-shell-kill-function440,15226 +(defun proof-shell-clear-state proof-shell-clear-state531,19076 +(defun proof-shell-exit proof-shell-exit546,19519 +(defun proof-shell-bail-out proof-shell-bail-out558,19964 +(defun proof-shell-restart proof-shell-restart567,20441 +(defvar proof-shell-no-response-display proof-shell-no-response-display609,21825 +(defvar proof-shell-urgent-message-marker proof-shell-urgent-message-marker612,21929 +(defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner615,22050 +(defun proof-shell-handle-output proof-shell-handle-output619,22177 +(defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output693,25514 +(defvar proof-shell-ignore-errors proof-shell-ignore-errors728,26936 +(defun proof-shell-handle-error proof-shell-handle-error734,27138 +(defun proof-shell-handle-interrupt proof-shell-handle-interrupt752,27982 +(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action766,28598 +(defun proof-goals-pos proof-goals-pos784,29424 +(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal789,29629 +(defsubst proof-shell-string-match-safe proof-shell-string-match-safe801,30164 +(defun proof-shell-process-output proof-shell-process-output806,30332 +(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge917,34972 +(defun proof-shell-insert proof-shell-insert926,35281 +(defun proof-shell-command-queue-item proof-shell-command-queue-item994,37815 +(defun proof-shell-set-silent proof-shell-set-silent999,37972 +(defun proof-shell-start-silent-item proof-shell-start-silent-item1005,38191 +(defun proof-shell-clear-silent proof-shell-clear-silent1011,38383 +(defun proof-shell-stop-silent-item proof-shell-stop-silent-item1017,38605 +(defun proof-shell-should-be-silent proof-shell-should-be-silent1024,38877 +(defun proof-append-alist proof-append-alist1037,39433 +(defun proof-start-queue proof-start-queue1093,41560 +(defun proof-extend-queue proof-extend-queue1104,41909 +(defun proof-shell-exec-loop proof-shell-exec-loop1115,42290 +(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1177,44757 +(defun proof-shell-message proof-shell-message1215,46480 +(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1221,46696 +(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1432,55614 +(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1434,55684 +(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1446,56054 +(defun proof-shell-filter proof-shell-filter1515,59110 +(defun proof-shell-filter-process-output proof-shell-filter-process-output1668,65447 +(defvar pg-last-tracing-output-time pg-last-tracing-output-time1721,67501 +(defvar pg-tracing-slow-mode pg-tracing-slow-mode1724,67607 +(defconst pg-slow-mode-duration pg-slow-mode-duration1727,67696 +(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1730,67778 +(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1733,67906 +(defun pg-tracing-tight-loop pg-tracing-tight-loop1735,67945 +(defun pg-finish-tracing-display pg-finish-tracing-display1778,69687 +(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1789,69957 +(defun proof-shell-show-annotations proof-shell-show-annotations1805,70492 +(defun proof-shell-wait proof-shell-wait1826,70989 +(defun proof-done-invisible proof-done-invisible1846,71899 +(defun proof-shell-invisible-command proof-shell-invisible-command1889,73622 +(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1916,74811 +(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1933,75492 +(define-derived-mode proof-shell-mode proof-shell-mode1953,75996 +(defconst proof-shell-important-settingsproof-shell-important-settings2023,78599 +(defun proof-shell-config-done proof-shell-config-done2028,78699 generic/proof-site.el,1154 -(defgroup proof-general proof-general20,592 -(defgroup proof-general-internals proof-general-internals33,1008 -(defun proof-home-directory-fn proof-home-directory-fn42,1201 -(defcustom proof-home-directoryproof-home-directory53,1571 -(defcustom proof-images-directoryproof-images-directory62,1937 -(defcustom proof-info-directoryproof-info-directory68,2138 -(defcustom proof-assistant-tableproof-assistant-table97,3387 -(defun proof-string-to-list proof-string-to-list156,5331 -(defcustom proof-assistants proof-assistants172,5822 -(defun proof-ready-for-assistant proof-ready-for-assistant220,7647 -(defconst proof-general-version proof-general-version335,11940 -(defcustom proof-assistant-cusgrp proof-assistant-cusgrp350,12503 -(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp358,12806 -(defcustom proof-assistant proof-assistant366,13118 -(defcustom proof-assistant-symbol proof-assistant-symbol374,13387 -(defvar proof-running-on-XEmacs proof-running-on-XEmacs391,13935 -(defvar proof-running-on-Emacs21 proof-running-on-Emacs21393,14057 -(defvar proof-running-on-win32 proof-running-on-win32397,14304 - -generic/proof-splash.el,898 -(defcustom proof-splash-enable proof-splash-enable14,380 -(defcustom proof-splash-time proof-splash-time19,532 -(defcustom proof-splash-contentsproof-splash-contents27,817 -(defconst proof-splash-startup-msg proof-splash-startup-msg59,1971 -(defconst proof-splash-welcome proof-splash-welcome68,2354 -(defun proof-get-image proof-get-image87,2918 -(defvar proof-splash-timeout-conf proof-splash-timeout-conf139,4742 -(defun proof-splash-centre-spaces proof-splash-centre-spaces142,4855 -(defun proof-splash-remove-screen proof-splash-remove-screen170,6024 -(defun proof-splash-remove-buffer proof-splash-remove-buffer191,6741 -(defvar proof-splash-seen proof-splash-seen207,7405 -(defun proof-splash-display-screen proof-splash-display-screen211,7522 -(defun proof-splash-message proof-splash-message285,10648 -(defun proof-splash-timeout-waiter proof-splash-timeout-waiter295,11011 +(defgroup proof-general proof-general20,593 +(defgroup proof-general-internals proof-general-internals33,1009 +(defun proof-home-directory-fn proof-home-directory-fn42,1202 +(defcustom proof-home-directoryproof-home-directory53,1572 +(defcustom proof-images-directoryproof-images-directory62,1938 +(defcustom proof-info-directoryproof-info-directory68,2139 +(defcustom proof-assistant-tableproof-assistant-table97,3388 +(defun proof-string-to-list proof-string-to-list156,5373 +(defcustom proof-assistants proof-assistants172,5864 +(defun proof-ready-for-assistant proof-ready-for-assistant220,7689 +(defconst proof-general-version proof-general-version335,11982 +(defcustom proof-assistant-cusgrp proof-assistant-cusgrp350,12555 +(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp358,12858 +(defcustom proof-assistant proof-assistant366,13170 +(defcustom proof-assistant-symbol proof-assistant-symbol374,13439 +(defvar proof-running-on-XEmacs proof-running-on-XEmacs391,13987 +(defvar proof-running-on-Emacs21 proof-running-on-Emacs21393,14109 +(defvar proof-running-on-win32 proof-running-on-win32397,14356 + +generic/proof-splash.el,976 +(defcustom proof-splash-enable proof-splash-enable14,379 +(defcustom proof-splash-time proof-splash-time19,531 +(defcustom proof-splash-contentsproof-splash-contents27,816 +(defconst proof-splash-startup-msg proof-splash-startup-msg59,1970 +(defconst proof-splash-welcome proof-splash-welcome68,2349 +(defun proof-get-image proof-get-image87,2913 +(defvar proof-splash-timeout-conf proof-splash-timeout-conf139,4737 +(defun proof-splash-centre-spaces proof-splash-centre-spaces142,4850 +(defun proof-splash-remove-screen proof-splash-remove-screen170,6019 +(defun proof-splash-remove-buffer proof-splash-remove-buffer191,6736 +(defvar proof-splash-seen proof-splash-seen207,7400 +(defun proof-splash-display-screen proof-splash-display-screen211,7517 +(defun proof-splash-message proof-splash-message286,10676 +(defun proof-splash-timeout-waiter proof-splash-timeout-waiter296,11039 +(defun proof-splash-set-frame-titles proof-splash-set-frame-titles313,11778 generic/proof-syntax.el,1296 (defun proof-ids-to-regexp proof-ids-to-regexp16,445 @@ -1166,71 +1159,72 @@ generic/proof-toolbar.el,3888 (defun proof-toolbar-make-menu-item proof-toolbar-make-menu-item558,16193 (defconst proof-toolbar-scripting-menuproof-toolbar-scripting-menu580,16881 -generic/proof-utils.el,2953 -(defmacro deflocal deflocal18,472 -(defmacro proof-with-current-buffer-if-exists proof-with-current-buffer-if-exists25,710 -(defmacro proof-with-script-buffer proof-with-script-buffer34,1087 -(defmacro proof-map-buffers proof-map-buffers45,1474 -(defmacro proof-sym proof-sym50,1659 -(defun proof-try-require proof-try-require55,1820 -(defun proof-set-value proof-set-value67,2161 -(defun proof-ass-symv proof-ass-symv127,4338 -(defmacro proof-ass-sym proof-ass-sym132,4525 -(defun proof-defpgcustom-fn proof-defpgcustom-fn136,4664 -(defun undefpgcustom undefpgcustom161,5748 -(defmacro defpgcustom defpgcustom167,5972 -(defmacro proof-ass proof-ass176,6389 -(defun proof-defpgdefault-fn proof-defpgdefault-fn181,6565 -(defmacro defpgdefault defpgdefault195,7024 -(defmacro defpgfun defpgfun206,7386 -(defun proof-file-truename proof-file-truename221,7680 -(defun proof-file-to-buffer proof-file-to-buffer225,7863 -(defun proof-files-to-buffers proof-files-to-buffers236,8192 -(defun proof-buffers-in-mode proof-buffers-in-mode243,8475 -(defun pg-save-from-death pg-save-from-death257,8926 -(defun proof-define-keys proof-define-keys276,9536 -(deflocal proof-font-lock-keywords proof-font-lock-keywords305,10537 -(deflocal proof-font-lock-keywords-case-fold-search proof-font-lock-keywords-case-fold-search311,10800 -(defun proof-font-lock-configure-defaults proof-font-lock-configure-defaults314,10923 -(defun proof-font-lock-clear-font-lock-vars proof-font-lock-clear-font-lock-vars362,13236 -(defun proof-font-lock-set-font-lock-vars proof-font-lock-set-font-lock-vars373,13609 -(defun proof-fontify-region proof-fontify-region380,13822 -(defconst pg-special-char-regexp pg-special-char-regexp434,15788 -(defun pg-remove-specials pg-remove-specials438,15900 -(defun proof-fontify-buffer proof-fontify-buffer452,16325 -(defun proof-warn-if-unset proof-warn-if-unset465,16566 -(defun proof-display-and-keep-buffer proof-display-and-keep-buffer470,16784 -(defun proof-clean-buffer proof-clean-buffer533,19410 -(defun proof-message proof-message545,19888 -(defun proof-warning proof-warning550,20101 -(defun proof-debug proof-debug557,20435 -(defun proof-switch-to-buffer proof-switch-to-buffer570,20926 -(defun proof-resize-window-tofit proof-resize-window-tofit603,22618 -(defun proof-submit-bug-report proof-submit-bug-report703,26646 -(defun proof-deftoggle-fn proof-deftoggle-fn726,27425 -(defmacro proof-deftoggle proof-deftoggle741,28080 -(defun proof-defintset-fn proof-defintset-fn748,28454 -(defmacro proof-defintset proof-defintset762,29109 -(defun proof-defstringset-fn proof-defstringset-fn769,29486 -(defmacro proof-defstringset proof-defstringset782,30113 -(defun pg-custom-save-vars pg-custom-save-vars796,30578 -(defun pg-custom-reset-vars pg-custom-reset-vars814,31304 -(defun proof-locate-executable proof-locate-executable827,31641 -(defconst proof-extra-flsproof-extra-fls857,32928 +generic/proof-utils.el,3027 +(defmacro deflocal deflocal18,471 +(defmacro proof-with-current-buffer-if-exists proof-with-current-buffer-if-exists25,709 +(defmacro proof-with-script-buffer proof-with-script-buffer34,1086 +(defmacro proof-map-buffers proof-map-buffers45,1473 +(defmacro proof-sym proof-sym50,1658 +(defun proof-try-require proof-try-require55,1819 +(defun proof-set-value proof-set-value67,2160 +(defun proof-ass-symv proof-ass-symv127,4337 +(defmacro proof-ass-sym proof-ass-sym132,4524 +(defun proof-defpgcustom-fn proof-defpgcustom-fn136,4663 +(defun undefpgcustom undefpgcustom161,5747 +(defmacro defpgcustom defpgcustom167,5971 +(defmacro proof-ass proof-ass176,6388 +(defun proof-defpgdefault-fn proof-defpgdefault-fn181,6564 +(defmacro defpgdefault defpgdefault195,7023 +(defmacro defpgfun defpgfun206,7385 +(defun proof-file-truename proof-file-truename221,7679 +(defun proof-file-to-buffer proof-file-to-buffer225,7862 +(defun proof-files-to-buffers proof-files-to-buffers236,8191 +(defun proof-buffers-in-mode proof-buffers-in-mode243,8474 +(defun pg-save-from-death pg-save-from-death257,8925 +(defun proof-define-keys proof-define-keys276,9535 +(deflocal proof-font-lock-keywords proof-font-lock-keywords305,10536 +(deflocal proof-font-lock-keywords-case-fold-search proof-font-lock-keywords-case-fold-search311,10801 +(defun proof-font-lock-configure-defaults proof-font-lock-configure-defaults314,10924 +(defun proof-font-lock-clear-font-lock-vars proof-font-lock-clear-font-lock-vars362,13237 +(defun proof-font-lock-set-font-lock-vars proof-font-lock-set-font-lock-vars373,13610 +(defun proof-fontify-region proof-fontify-region380,13823 +(defconst pg-special-char-regexp pg-special-char-regexp434,15789 +(defun pg-remove-specials pg-remove-specials438,15901 +(defun proof-fontify-buffer proof-fontify-buffer452,16326 +(defun proof-warn-if-unset proof-warn-if-unset465,16567 +(defun proof-get-window-for-buffer proof-get-window-for-buffer470,16785 +(defun proof-display-and-keep-buffer proof-display-and-keep-buffer507,18437 +(defun proof-clean-buffer proof-clean-buffer538,19713 +(defun proof-message proof-message550,20191 +(defun proof-warning proof-warning555,20404 +(defun proof-debug proof-debug562,20738 +(defun proof-switch-to-buffer proof-switch-to-buffer575,21229 +(defun proof-resize-window-tofit proof-resize-window-tofit608,22921 +(defun proof-submit-bug-report proof-submit-bug-report708,26949 +(defun proof-deftoggle-fn proof-deftoggle-fn731,27728 +(defmacro proof-deftoggle proof-deftoggle746,28383 +(defun proof-defintset-fn proof-defintset-fn753,28757 +(defmacro proof-defintset proof-defintset767,29412 +(defun proof-defstringset-fn proof-defstringset-fn774,29789 +(defmacro proof-defstringset proof-defstringset787,30416 +(defun pg-custom-save-vars pg-custom-save-vars801,30881 +(defun pg-custom-reset-vars pg-custom-reset-vars819,31607 +(defun proof-locate-executable proof-locate-executable832,31944 +(defconst proof-extra-flsproof-extra-fls864,33357 generic/proof-x-symbol.el,960 -(defvar proof-x-symbol-initialized proof-x-symbol-initialized53,2150 -(defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file56,2245 -(defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available62,2427 -(defun proof-x-symbol-initialize proof-x-symbol-initialize82,3172 -(defun proof-x-symbol-enable proof-x-symbol-enable177,7035 -(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers199,8004 -(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers214,8758 -(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region236,9462 -(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input238,9528 -(defun proof-x-symbol-set-language proof-x-symbol-set-language255,10119 -(defun proof-x-symbol-shell-config proof-x-symbol-shell-config260,10290 -(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer308,12457 +(defvar proof-x-symbol-initialized proof-x-symbol-initialized53,2149 +(defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file56,2244 +(defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available62,2426 +(defun proof-x-symbol-initialize proof-x-symbol-initialize82,3171 +(defun proof-x-symbol-enable proof-x-symbol-enable177,7034 +(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers199,8003 +(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers214,8757 +(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region236,9461 +(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input238,9527 +(defun proof-x-symbol-set-language proof-x-symbol-set-language255,10118 +(defun proof-x-symbol-shell-config proof-x-symbol-shell-config260,10289 +(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer308,12456 generic/span.el,192 (defsubst delete-spans delete-spans22,471 @@ -1239,86 +1233,86 @@ generic/span.el,192 (defsubst set-span-end set-span-end34,896 generic/span-extent.el,1346 -(defsubst make-span make-span16,559 -(defsubst detach-span detach-span20,681 -(defsubst set-span-endpoints set-span-endpoints24,768 -(defsubst set-span-property set-span-property28,901 -(defsubst span-read-only span-read-only32,1028 -(defsubst span-read-write span-read-write36,1132 -(defun span-give-warning span-give-warning40,1239 -(defun span-write-warning span-write-warning44,1337 -(defsubst span-property span-property49,1537 -(defsubst delete-span delete-span53,1652 -(defsubst mapcar-spans mapcar-spans59,1823 -(defsubst span-at span-at63,2029 -(defsubst span-at-before span-at-before67,2146 -(defsubst span-start span-start72,2343 -(defsubst span-end span-end76,2472 -(defsubst prev-span prev-span80,2595 -(defsubst next-span next-span84,2741 -(defsubst span-live-p span-live-p88,2883 -(defun span-raise span-raise96,3155 -(defalias 'span-object span-object100,3254 -(defalias 'span-string span-string101,3293 -(defsubst make-detached-span make-detached-span104,3379 -(defsubst span-buffer span-buffer110,3476 -(defsubst span-detached-p span-detached-p115,3568 -(defsubst set-span-face set-span-face120,3680 -(defsubst fold-spans fold-spans125,3776 -(defsubst set-span-properties set-span-properties130,3974 -(defsubst set-span-keymap set-span-keymap135,4083 -(defsubst span-at-event span-at-event140,4198 +(defsubst make-span make-span16,557 +(defsubst detach-span detach-span20,679 +(defsubst set-span-endpoints set-span-endpoints24,766 +(defsubst set-span-property set-span-property28,899 +(defsubst span-read-only span-read-only32,1026 +(defsubst span-read-write span-read-write36,1130 +(defun span-give-warning span-give-warning40,1237 +(defun span-write-warning span-write-warning44,1335 +(defsubst span-property span-property49,1535 +(defsubst delete-span delete-span53,1650 +(defsubst mapcar-spans mapcar-spans59,1821 +(defsubst span-at span-at63,2027 +(defsubst span-at-before span-at-before67,2144 +(defsubst span-start span-start72,2341 +(defsubst span-end span-end76,2470 +(defsubst prev-span prev-span80,2593 +(defsubst next-span next-span84,2739 +(defsubst span-live-p span-live-p88,2881 +(defun span-raise span-raise96,3153 +(defalias 'span-object span-object100,3252 +(defalias 'span-string span-string101,3291 +(defsubst make-detached-span make-detached-span104,3377 +(defsubst span-buffer span-buffer110,3474 +(defsubst span-detached-p span-detached-p115,3566 +(defsubst set-span-face set-span-face120,3678 +(defsubst fold-spans fold-spans125,3774 +(defsubst set-span-properties set-span-properties130,3972 +(defsubst set-span-keymap set-span-keymap135,4081 +(defsubst span-at-event span-at-event140,4196 generic/span-overlay.el,2198 -(defvar before-list before-list20,774 -(defun foldr foldr27,909 -(defun foldl foldl39,1242 -(defsubst span-start span-start51,1559 -(defsubst span-end span-end55,1651 -(defun set-span-property set-span-property59,1737 -(defsubst span-property span-property63,1853 -(defun span-read-only-hook span-read-only-hook67,1964 -(defun span-read-only span-read-only71,2096 -(defun span-read-write span-read-write86,2874 -(defun span-give-warning span-give-warning92,3093 -(defun span-write-warning span-write-warning96,3201 -(defun int-nil-lt int-nil-lt101,3424 -(defun span-lt span-lt110,3627 -(defun span-traverse span-traverse115,3786 -(defun add-span add-span131,4233 -(defun make-span make-span145,4635 -(defun remove-span remove-span149,4766 -(defun spans-at-point spans-at-point162,5219 -(defun append-unique append-unique176,5699 -(defun spans-at-region spans-at-region179,5786 -(defun spans-at-point-prop spans-at-point-prop186,6008 -(defun spans-at-region-prop spans-at-region-prop194,6258 -(defun span-at span-at206,6605 -(defsubst detach-span detach-span212,6819 -(defsubst delete-span delete-span218,6946 -(defsubst set-span-endpoints set-span-endpoints226,7189 -(defsubst mapcar-spans mapcar-spans233,7405 -(defun map-spans-aux map-spans-aux237,7609 -(defsubst map-spans map-spans241,7724 -(defun find-span-aux find-span-aux244,7782 -(defun find-span find-span249,7908 -(defun span-at-before span-at-before252,7973 -(defun prev-span prev-span265,8415 -(defun next-span next-span274,8697 -(defsubst span-live-p span-live-p299,9681 -(defun span-raise span-raise305,9847 -(defalias 'span-object span-object311,10078 -(defun span-string span-string313,10119 -(defun set-span-properties set-span-properties319,10301 -(defun span-find-span span-find-span331,10556 -(defsubst span-at-event span-at-event342,10915 -(defun make-detached-span make-detached-span347,11039 -(defun fold-spans-aux fold-spans-aux353,11173 -(defun fold-spans fold-spans361,11429 -(defsubst span-buffer span-buffer368,11637 -(defsubst span-detached-p span-detached-p373,11729 -(defsubst set-span-face set-span-face381,11925 -(defsubst set-span-keymap set-span-keymap386,12025 +(defvar before-list before-list20,771 +(defun foldr foldr27,906 +(defun foldl foldl39,1239 +(defsubst span-start span-start51,1556 +(defsubst span-end span-end55,1648 +(defun set-span-property set-span-property59,1734 +(defsubst span-property span-property63,1850 +(defun span-read-only-hook span-read-only-hook67,1961 +(defun span-read-only span-read-only71,2093 +(defun span-read-write span-read-write86,2871 +(defun span-give-warning span-give-warning92,3090 +(defun span-write-warning span-write-warning96,3198 +(defun int-nil-lt int-nil-lt101,3421 +(defun span-lt span-lt110,3624 +(defun span-traverse span-traverse115,3783 +(defun add-span add-span131,4230 +(defun make-span make-span145,4632 +(defun remove-span remove-span149,4763 +(defun spans-at-point spans-at-point162,5216 +(defun append-unique append-unique176,5696 +(defun spans-at-region spans-at-region179,5783 +(defun spans-at-point-prop spans-at-point-prop186,6005 +(defun spans-at-region-prop spans-at-region-prop194,6255 +(defun span-at span-at206,6602 +(defsubst detach-span detach-span212,6816 +(defsubst delete-span delete-span218,6943 +(defsubst set-span-endpoints set-span-endpoints226,7186 +(defsubst mapcar-spans mapcar-spans233,7402 +(defun map-spans-aux map-spans-aux237,7606 +(defsubst map-spans map-spans241,7721 +(defun find-span-aux find-span-aux244,7779 +(defun find-span find-span249,7905 +(defun span-at-before span-at-before252,7970 +(defun prev-span prev-span265,8412 +(defun next-span next-span274,8694 +(defsubst span-live-p span-live-p299,9678 +(defun span-raise span-raise305,9844 +(defalias 'span-object span-object311,10075 +(defun span-string span-string313,10116 +(defun set-span-properties set-span-properties319,10298 +(defun span-find-span span-find-span331,10553 +(defsubst span-at-event span-at-event342,10912 +(defun make-detached-span make-detached-span347,11036 +(defun fold-spans-aux fold-spans-aux353,11170 +(defun fold-spans fold-spans361,11426 +(defsubst span-buffer span-buffer368,11634 +(defsubst span-detached-p span-detached-p373,11726 +(defsubst set-span-face set-span-face381,11922 +(defsubst set-span-keymap set-span-keymap386,12022 generic/texi-docstring-magic.el,958 (defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2996 @@ -1336,87 +1330,66 @@ generic/texi-docstring-magic.el,958 hol98/hol98.el,0 -hol98/x-symbol-hol98.el,1918 -(defvar x-symbol-hol98-symbol-table x-symbol-hol98-symbol-table8,159 -(defvar x-symbol-hol98-master-directory x-symbol-hol98-master-directory50,1699 -(defvar x-symbol-hol98-image-searchpath x-symbol-hol98-image-searchpath51,1748 -(defvar x-symbol-hol98-image-cached-dirs x-symbol-hol98-image-cached-dirs52,1797 -(defvar x-symbol-hol98-image-keywords x-symbol-hol98-image-keywords53,1864 -(defvar x-symbol-hol98-font-lock-keywords x-symbol-hol98-font-lock-keywords54,1907 -(defvar x-symbol-hol98-header-groups-alist x-symbol-hol98-header-groups-alist55,1954 -(defvar x-symbol-hol98-class-alist x-symbol-hol98-class-alist56,2002 -(defvar x-symbol-hol98-class-face-alist x-symbol-hol98-class-face-alist59,2145 -(defvar x-symbol-hol98-electric-ignore x-symbol-hol98-electric-ignore60,2190 -(defvar x-symbol-hol98-required-fonts x-symbol-hol98-required-fonts61,2234 -(defvar x-symbol-hol98-case-insensitive x-symbol-hol98-case-insensitive62,2277 -(defvar x-symbol-hol98-token-shape x-symbol-hol98-token-shape65,2430 -(defvar x-symbol-hol98-table x-symbol-hol98-table66,2498 -(defun x-symbol-hol98-default-token-list x-symbol-hol98-default-token-list67,2556 -(defvar x-symbol-hol98-token-list x-symbol-hol98-token-list68,2614 -(defvar x-symbol-hol98-input-token-ignore x-symbol-hol98-input-token-ignore69,2684 -(defvar x-symbol-hol98-exec-specs x-symbol-hol98-exec-specs72,2751 -(defvar x-symbol-hol98-menu-alist x-symbol-hol98-menu-alist73,2790 -(defvar x-symbol-hol98-grid-alist x-symbol-hol98-grid-alist74,2829 -(defvar x-symbol-hol98-decode-atree x-symbol-hol98-decode-atree75,2868 -(defvar x-symbol-hol98-decode-alist x-symbol-hol98-decode-alist76,2909 -(defvar x-symbol-hol98-encode-alist x-symbol-hol98-encode-alist77,2950 -(defvar x-symbol-hol98-nomule-decode-exec x-symbol-hol98-nomule-decode-exec78,2991 -(defvar x-symbol-hol98-nomule-encode-exec x-symbol-hol98-nomule-encode-exec79,3038 +hol98/x-symbol-hol98.el,0 isa/interface-setup.el,0 -isa/isabelle-system.el,2954 -(defconst isa-running-isar isa-running-isar17,538 -(defgroup isabelle isabelle23,720 -(defcustom isabelle-web-pageisabelle-web-page27,849 -(defcustom isa-isatool-commandisa-isatool-command38,1144 -(defvar isatool-not-found isatool-not-found64,2063 -(defun isa-set-isatool-command isa-set-isatool-command67,2176 -(defun isa-shell-command-to-string isa-shell-command-to-string87,2960 -(defun isa-getenv isa-getenv95,3412 -(defcustom isabelle-program-name isabelle-program-name114,4069 -(defvar isabelle-prog-name isabelle-prog-name140,5017 -(defun isabelle-command-line isabelle-command-line143,5144 -(defun isabelle-choose-logic isabelle-choose-logic166,6052 -(defun isa-tool-list-logics isa-tool-list-logics188,7024 -(defun isa-view-doc isa-view-doc194,7247 -(defvar isabelle-version-string isabelle-version-string201,7471 -(defun isa-version isa-version203,7512 -(defconst isa-supports-pgip isa-supports-pgip216,7995 -(defun isa-tool-list-docs isa-tool-list-docs224,8225 -(defun isa-quit isa-quit243,8954 -(defconst isabelle-verbatim-regexp isabelle-verbatim-regexp250,9149 -(defun isabelle-verbatim isabelle-verbatim253,9290 -(defcustom isabelle-refresh-logics isabelle-refresh-logics269,9881 -(defcustom isabelle-logics-available isabelle-logics-available277,10208 -(defcustom isabelle-chosen-logic isabelle-chosen-logic285,10508 -(defconst isabelle-docs-menu isabelle-docs-menu298,10976 -(defun isabelle-logics-menu-calculate isabelle-logics-menu-calculate306,11265 -(defun isabelle-logics-menu-refresh isabelle-logics-menu-refresh322,11745 -(defconst isabelle-logics-menu isabelle-logics-menu340,12340 -(defun isabelle-load-isar-keywords isabelle-load-isar-keywords349,12800 -(defpacustom show-types show-types376,13755 -(defpacustom show-sorts show-sorts381,13871 -(defpacustom show-consts show-consts386,13987 -(defpacustom long-names long-names391,14121 -(defpacustom eta-contract eta-contract396,14253 -(defpacustom trace-simplifier trace-simplifier401,14394 -(defpacustom trace-rules trace-rules406,14526 -(defpacustom quick-and-dirty quick-and-dirty411,14658 -(defpacustom full-proofs full-proofs416,14794 -(defpacustom global-timing global-timing422,15103 -(defpacustom theorem-dependencies theorem-dependencies428,15261 -(defpacustom goals-limit goals-limit434,15526 -(defpacustom prems-limit prems-limit439,15665 -(defpacustom print-depth print-depth444,15825 -(defpgdefault menu-entriesmenu-entries456,16114 -(defpgdefault help-menu-entries help-menu-entries463,16276 -(defpgdefault x-symbol-language x-symbol-language471,16470 -(defun isabelle-convert-idmarkup-to-subterm isabelle-convert-idmarkup-to-subterm494,17085 -(defun isabelle-create-span-menu isabelle-create-span-menu519,18124 -(defun isabelle-xml-sml-escapes isabelle-xml-sml-escapes536,18618 -(defun isabelle-process-pgip isabelle-process-pgip539,18719 -(defun isabelle-parse-syntax-dump isabelle-parse-syntax-dump556,19305 +isa/isabelle-system.el,3268 +(defconst isa-running-isar isa-running-isar17,537 +(defgroup isabelle isabelle23,719 +(defcustom isabelle-web-pageisabelle-web-page27,848 +(defcustom isa-isatool-commandisa-isatool-command38,1143 +(defvar isatool-not-found isatool-not-found64,2062 +(defun isa-set-isatool-command isa-set-isatool-command67,2175 +(defun isa-shell-command-to-string isa-shell-command-to-string87,2959 +(defun isa-getenv isa-getenv95,3411 +(defcustom isabelle-program-name isabelle-program-name114,4068 +(defvar isabelle-prog-name isabelle-prog-name140,5016 +(defun isabelle-command-line isabelle-command-line143,5143 +(defun isabelle-choose-logic isabelle-choose-logic166,6051 +(defun isa-tool-list-logics isa-tool-list-logics188,7023 +(defun isa-view-doc isa-view-doc195,7261 +(defvar isabelle-version-string isabelle-version-string202,7485 +(defun isa-version isa-version204,7526 +(defconst isa-supports-pgip isa-supports-pgip217,8009 +(defun isa-tool-list-docs isa-tool-list-docs225,8239 +(defun isa-quit isa-quit243,8961 +(defconst isabelle-verbatim-regexp isabelle-verbatim-regexp250,9156 +(defun isabelle-verbatim isabelle-verbatim253,9297 +(defcustom isabelle-refresh-logics isabelle-refresh-logics269,9888 +(defcustom isabelle-logics-available isabelle-logics-available277,10215 +(defcustom isabelle-chosen-logic isabelle-chosen-logic285,10515 +(defconst isabelle-docs-menu isabelle-docs-menu298,10983 +(defun isabelle-logics-menu-calculate isabelle-logics-menu-calculate308,11376 +(defvar isabelle-time-to-refresh-logics isabelle-time-to-refresh-logics324,11885 +(defun isabelle-logics-menu-refresh isabelle-logics-menu-refresh327,11978 +(defun isabelle-logics-menu-filter isabelle-logics-menu-filter344,12677 +(defun isabelle-menu-bar-update-logics isabelle-menu-bar-update-logics350,12887 +(defvar isabelle-logics-menu-entries isabelle-logics-menu-entries361,13243 +(defvar isabelle-logics-menu isabelle-logics-menu363,13315 +(defun isabelle-load-isar-keywords isabelle-load-isar-keywords376,13933 +(defpacustom show-types show-types403,14888 +(defpacustom show-sorts show-sorts408,15004 +(defpacustom show-consts show-consts413,15120 +(defpacustom long-names long-names418,15254 +(defpacustom eta-contract eta-contract423,15386 +(defpacustom trace-simplifier trace-simplifier428,15527 +(defpacustom trace-rules trace-rules433,15659 +(defpacustom quick-and-dirty quick-and-dirty438,15791 +(defpacustom full-proofs full-proofs443,15927 +(defpacustom global-timing global-timing449,16236 +(defpacustom theorem-dependencies theorem-dependencies455,16394 +(defpacustom goals-limit goals-limit461,16659 +(defpacustom prems-limit prems-limit466,16798 +(defpacustom print-depth print-depth471,16958 +(defpgdefault menu-entriesmenu-entries483,17247 +(defpgdefault help-menu-entries help-menu-entries490,17409 +(defpgdefault x-symbol-language x-symbol-language498,17603 +(defun isabelle-convert-idmarkup-to-subterm isabelle-convert-idmarkup-to-subterm521,18218 +(defun isabelle-create-span-menu isabelle-create-span-menu546,19257 +(defun isabelle-xml-sml-escapes isabelle-xml-sml-escapes563,19751 +(defun isabelle-process-pgip isabelle-process-pgip566,19852 +(defun isabelle-parse-syntax-dump isabelle-parse-syntax-dump583,20438 isa/isa.el,2283 (defcustom isa-outline-regexpisa-outline-regexp43,1354 @@ -1425,37 +1398,37 @@ isa/isa.el,2283 (defvar isa-shell-outline-heading-end-regexp isa-shell-outline-heading-end-regexp56,1805 (defun isa-mode-config-set-variables isa-mode-config-set-variables59,1857 (defun isa-shell-mode-config-set-variables isa-shell-mode-config-set-variables141,5266 -(defun isa-update-thy-only isa-update-thy-only278,10976 -(defun isa-shell-update-thy isa-shell-update-thy290,11484 -(defun isa-remove-file isa-remove-file315,12687 -(defun isa-shell-compute-new-files-list isa-shell-compute-new-files-list325,13005 -(define-derived-mode isa-shell-mode isa-shell-mode341,13517 -(define-derived-mode isa-response-mode isa-response-mode346,13642 -(define-derived-mode isa-goals-mode isa-goals-mode351,13811 -(define-derived-mode isa-proofscript-mode isa-proofscript-mode356,13968 -(defun isa-mode isa-mode365,14149 -(define-key map map409,15689 -(define-key map map410,15739 -(defun isa-process-thy-file isa-process-thy-file414,15896 -(defcustom isa-retract-thy-file-command isa-retract-thy-file-command420,16105 -(defun isa-retract-thy-file isa-retract-thy-file426,16342 -(defgroup thy thy442,16971 -(defun isa-splice-separator isa-splice-separator454,17301 -(defun isa-file-name-cons-extension isa-file-name-cons-extension463,17553 -(defun isa-format isa-format470,17819 -(define-key isa-proofscript-mode-map isa-proofscript-mode-map482,18194 -(defcustom isa-not-undoable-commands-regexpisa-not-undoable-commands-regexp492,18327 -(defun isa-count-undos isa-count-undos499,18580 -(defun isa-goal-command-p isa-goal-command-p529,19745 -(defun isa-find-and-forget isa-find-and-forget542,20390 -(defun isa-state-preserving-p isa-state-preserving-p545,20445 -(defun isa-pre-shell-start isa-pre-shell-start554,20813 -(defun isa-mode-config isa-mode-config561,21090 -(defun isa-shell-mode-config isa-shell-mode-config588,22163 -(defun isa-response-mode-config isa-response-mode-config595,22412 -(defun isa-goals-mode-config isa-goals-mode-config600,22573 -(defun isa-preprocessing isa-preprocessing608,22897 -(defpgdefault completion-tablecompletion-table622,23401 +(defun isa-update-thy-only isa-update-thy-only283,11186 +(defun isa-shell-update-thy isa-shell-update-thy295,11694 +(defun isa-remove-file isa-remove-file320,12897 +(defun isa-shell-compute-new-files-list isa-shell-compute-new-files-list330,13215 +(define-derived-mode isa-shell-mode isa-shell-mode346,13727 +(define-derived-mode isa-response-mode isa-response-mode351,13852 +(define-derived-mode isa-goals-mode isa-goals-mode356,14021 +(define-derived-mode isa-proofscript-mode isa-proofscript-mode361,14178 +(defun isa-mode isa-mode370,14359 +(define-key map map414,15899 +(define-key map map415,15949 +(defun isa-process-thy-file isa-process-thy-file419,16106 +(defcustom isa-retract-thy-file-command isa-retract-thy-file-command425,16315 +(defun isa-retract-thy-file isa-retract-thy-file431,16552 +(defgroup thy thy447,17181 +(defun isa-splice-separator isa-splice-separator459,17511 +(defun isa-file-name-cons-extension isa-file-name-cons-extension468,17763 +(defun isa-format isa-format475,18029 +(define-key isa-proofscript-mode-map isa-proofscript-mode-map487,18404 +(defcustom isa-not-undoable-commands-regexpisa-not-undoable-commands-regexp497,18537 +(defun isa-count-undos isa-count-undos504,18790 +(defun isa-goal-command-p isa-goal-command-p534,19955 +(defun isa-find-and-forget isa-find-and-forget547,20600 +(defun isa-state-preserving-p isa-state-preserving-p550,20655 +(defun isa-pre-shell-start isa-pre-shell-start559,21023 +(defun isa-mode-config isa-mode-config566,21300 +(defun isa-shell-mode-config isa-shell-mode-config593,22373 +(defun isa-response-mode-config isa-response-mode-config600,22622 +(defun isa-goals-mode-config isa-goals-mode-config605,22783 +(defun isa-preprocessing isa-preprocessing613,23107 +(defpgdefault completion-tablecompletion-table627,23611 isa/isa-syntax.el,3046 (defun isa-init-syntax-table isa-init-syntax-table14,312 @@ -1508,131 +1481,131 @@ isa/isa-syntax.el,3046 (defconst isa-indent-close-regexpisa-indent-close-regexp349,11740 isa/thy-mode.el,2895 -(defcustom thy-heading-indent thy-heading-indent27,821 -(defcustom thy-indent-level thy-indent-level32,925 -(defcustom thy-indent-strings thy-indent-strings37,1052 -(defcustom thy-use-sml-mode thy-use-sml-mode44,1277 -(defcustom thy-sectionsthy-sections55,1685 -(defcustom thy-id-headerthy-id-header108,3362 -(defcustom thy-templatethy-template120,3662 -(defvar thy-mode-map thy-mode-map145,4090 -(defvar thy-mode-syntax-table thy-mode-syntax-table147,4117 -(defun thy-add-menus thy-add-menus182,5677 -(defun thy-mode thy-mode220,7073 -(defun thy-mode-quiet thy-mode-quiet275,8832 -(defun thy-proofgeneral-send-string thy-proofgeneral-send-string355,11592 -(defun isa-sml-hook isa-sml-hook434,14199 -(defun isa-sml-mode isa-sml-mode448,14794 -(defcustom isa-ml-file-extension isa-ml-file-extension453,14926 -(defun thy-find-other-file thy-find-other-file458,15048 -(defvar thy-minor-sml-mode-map thy-minor-sml-mode-map481,15930 -(defun thy-install-sml-mode thy-install-sml-mode483,15967 -(defun thy-minor-sml-mode thy-minor-sml-mode492,16353 -(defun thy-do-sml-indent thy-do-sml-indent510,17003 -(defun thy-insert-name thy-insert-name520,17400 -(defun thy-insert-class thy-insert-class526,17598 -(defun thy-insert-default-sort thy-insert-default-sort536,17870 -(defun thy-insert-type thy-insert-type544,18042 -(defun thy-insert-arity thy-insert-arity567,18612 -(defun thy-insert-const thy-insert-const580,18987 -(defun thy-insert-rule thy-insert-rule592,19376 -(defun thy-insert-template thy-insert-template601,19558 -(defun isa-read-idlist isa-read-idlist633,20437 -(defun isa-read-id isa-read-id642,20724 -(defun isa-read-string isa-read-string650,20953 -(defun isa-read-num isa-read-num658,21190 -(defun thy-read-thy-name thy-read-thy-name669,21482 -(defun thy-read-logic-image thy-read-logic-image678,21784 -(defun thy-insert-header thy-insert-header688,22048 -(defun thy-insert-id-header thy-insert-id-header706,22613 -(defun thy-check-mode thy-check-mode718,22972 -(defconst thy-headings-regexpthy-headings-regexp723,23077 -(defvar thy-mode-font-lock-keywordsthy-mode-font-lock-keywords733,23336 -(defun thy-goto-next-section thy-goto-next-section755,24096 -(defun thy-goto-prev-section thy-goto-prev-section783,25073 -(defun thy-goto-top-of-section thy-goto-top-of-section790,25386 -(defun thy-current-section thy-current-section797,25583 -(defun thy-kill-line thy-kill-line815,26046 -(defun thy-indent-line thy-indent-line877,28130 -(defun thy-calculate-indentation thy-calculate-indentation904,29164 -(defun thy-long-comment-string-indentation thy-long-comment-string-indentation924,29823 -(defun thy-string-indentation thy-string-indentation959,30807 -(defun thy-indentation-for thy-indentation-for978,31457 -(defun thy-string-start thy-string-start984,31616 -(defun thy-comment-or-string-start thy-comment-or-string-start998,32153 - -isa/x-symbol-isabelle.el,3170 -(defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts20,628 -(defvar x-symbol-isabelle-name x-symbol-isabelle-name30,1129 -(defvar x-symbol-isabelle-modeline-name x-symbol-isabelle-modeline-name31,1179 -(defcustom x-symbol-isabelle-header-groups-alist x-symbol-isabelle-header-groups-alist33,1227 -(defcustom x-symbol-isabelle-electric-ignore x-symbol-isabelle-electric-ignore40,1455 -(defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts48,1711 -(defvar x-symbol-isabelle-extra-menu-items x-symbol-isabelle-extra-menu-items51,1820 -(defvar x-symbol-isabelle-token-grammarx-symbol-isabelle-token-grammar55,1918 -(defun x-symbol-isabelle-token-list x-symbol-isabelle-token-list62,2124 -(defvar x-symbol-isabelle-user-table x-symbol-isabelle-user-table65,2213 -(defvar x-symbol-isabelle-generated-data x-symbol-isabelle-generated-data68,2334 -(defvar x-symbol-isabelle-master-directory x-symbol-isabelle-master-directory76,2577 -(defvar x-symbol-isabelle-image-searchpath x-symbol-isabelle-image-searchpath77,2630 -(defvar x-symbol-isabelle-image-cached-dirs x-symbol-isabelle-image-cached-dirs78,2682 -(defvar x-symbol-isabelle-image-file-truename-alist x-symbol-isabelle-image-file-truename-alist79,2752 -(defvar x-symbol-isabelle-image-keywords x-symbol-isabelle-image-keywords80,2809 -(defcustom x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher90,3153 -(defcustom x-symbol-isabelle-font-lock-regexp x-symbol-isabelle-font-lock-regexp96,3400 -(defcustom x-symbol-isabelle-font-lock-limit-regexp x-symbol-isabelle-font-lock-limit-regexp101,3584 -(defcustom x-symbol-isabelle-font-lock-contents-regexp x-symbol-isabelle-font-lock-contents-regexp107,3802 -(defcustom x-symbol-isabelle-single-char-regexp x-symbol-isabelle-single-char-regexp114,4065 -(defun x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher120,4254 -(defun isabelle-match-subscript isabelle-match-subscript154,5929 -(defvar x-symbol-isabelle-font-lock-keywordsx-symbol-isabelle-font-lock-keywords163,6324 -(defvar x-symbol-isabelle-font-lock-allowed-faces x-symbol-isabelle-font-lock-allowed-faces170,6592 -(defcustom x-symbol-isabelle-class-alistx-symbol-isabelle-class-alist177,6824 -(defcustom x-symbol-isabelle-class-face-alist x-symbol-isabelle-class-face-alist188,7249 -(defvar x-symbol-isabelle-case-insensitive x-symbol-isabelle-case-insensitive203,7777 -(defvar x-symbol-isabelle-token-shape x-symbol-isabelle-token-shape204,7825 -(defvar x-symbol-isabelle-input-token-ignore x-symbol-isabelle-input-token-ignore205,7868 -(defvar x-symbol-isabelle-token-list x-symbol-isabelle-token-list206,7918 -(defvar x-symbol-isabelle-symbol-table x-symbol-isabelle-symbol-table208,7967 -(defvar x-symbol-isabelle-xsymbol-table x-symbol-isabelle-xsymbol-table307,10678 -(defun x-symbol-isabelle-prepare-table x-symbol-isabelle-prepare-table452,15080 -(defvar x-symbol-isabelle-tablex-symbol-isabelle-table464,15491 -(defcustom x-symbol-isabelle-auto-stylex-symbol-isabelle-auto-style478,15844 -(defcustom x-symbol-isabelle-auto-coding-alist x-symbol-isabelle-auto-coding-alist492,16354 +(defcustom thy-heading-indent thy-heading-indent27,816 +(defcustom thy-indent-level thy-indent-level32,920 +(defcustom thy-indent-strings thy-indent-strings37,1047 +(defcustom thy-use-sml-mode thy-use-sml-mode44,1272 +(defcustom thy-sectionsthy-sections55,1680 +(defcustom thy-id-headerthy-id-header108,3357 +(defcustom thy-templatethy-template120,3657 +(defvar thy-mode-map thy-mode-map145,4085 +(defvar thy-mode-syntax-table thy-mode-syntax-table147,4112 +(defun thy-add-menus thy-add-menus182,5672 +(defun thy-mode thy-mode220,7068 +(defun thy-mode-quiet thy-mode-quiet275,8827 +(defun thy-proofgeneral-send-string thy-proofgeneral-send-string355,11587 +(defun isa-sml-hook isa-sml-hook434,14194 +(defun isa-sml-mode isa-sml-mode448,14789 +(defcustom isa-ml-file-extension isa-ml-file-extension453,14921 +(defun thy-find-other-file thy-find-other-file458,15043 +(defvar thy-minor-sml-mode-map thy-minor-sml-mode-map481,15925 +(defun thy-install-sml-mode thy-install-sml-mode483,15962 +(defun thy-minor-sml-mode thy-minor-sml-mode492,16348 +(defun thy-do-sml-indent thy-do-sml-indent510,16998 +(defun thy-insert-name thy-insert-name520,17395 +(defun thy-insert-class thy-insert-class526,17593 +(defun thy-insert-default-sort thy-insert-default-sort536,17865 +(defun thy-insert-type thy-insert-type544,18037 +(defun thy-insert-arity thy-insert-arity567,18607 +(defun thy-insert-const thy-insert-const580,18982 +(defun thy-insert-rule thy-insert-rule592,19371 +(defun thy-insert-template thy-insert-template601,19553 +(defun isa-read-idlist isa-read-idlist633,20432 +(defun isa-read-id isa-read-id642,20719 +(defun isa-read-string isa-read-string650,20948 +(defun isa-read-num isa-read-num658,21185 +(defun thy-read-thy-name thy-read-thy-name669,21477 +(defun thy-read-logic-image thy-read-logic-image678,21779 +(defun thy-insert-header thy-insert-header688,22043 +(defun thy-insert-id-header thy-insert-id-header706,22608 +(defun thy-check-mode thy-check-mode718,22967 +(defconst thy-headings-regexpthy-headings-regexp723,23072 +(defvar thy-mode-font-lock-keywordsthy-mode-font-lock-keywords733,23331 +(defun thy-goto-next-section thy-goto-next-section755,24091 +(defun thy-goto-prev-section thy-goto-prev-section783,25068 +(defun thy-goto-top-of-section thy-goto-top-of-section790,25381 +(defun thy-current-section thy-current-section797,25578 +(defun thy-kill-line thy-kill-line815,26041 +(defun thy-indent-line thy-indent-line877,28125 +(defun thy-calculate-indentation thy-calculate-indentation904,29159 +(defun thy-long-comment-string-indentation thy-long-comment-string-indentation924,29818 +(defun thy-string-indentation thy-string-indentation959,30802 +(defun thy-indentation-for thy-indentation-for978,31452 +(defun thy-string-start thy-string-start984,31611 +(defun thy-comment-or-string-start thy-comment-or-string-start998,32148 + +isa/x-symbol-isabelle.el,3169 +(defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts20,624 +(defvar x-symbol-isabelle-name x-symbol-isabelle-name28,1028 +(defvar x-symbol-isabelle-modeline-name x-symbol-isabelle-modeline-name29,1078 +(defcustom x-symbol-isabelle-header-groups-alist x-symbol-isabelle-header-groups-alist31,1126 +(defcustom x-symbol-isabelle-electric-ignore x-symbol-isabelle-electric-ignore38,1354 +(defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts46,1610 +(defvar x-symbol-isabelle-extra-menu-items x-symbol-isabelle-extra-menu-items49,1719 +(defvar x-symbol-isabelle-token-grammarx-symbol-isabelle-token-grammar53,1817 +(defun x-symbol-isabelle-token-list x-symbol-isabelle-token-list60,2023 +(defvar x-symbol-isabelle-user-table x-symbol-isabelle-user-table63,2112 +(defvar x-symbol-isabelle-generated-data x-symbol-isabelle-generated-data66,2233 +(defvar x-symbol-isabelle-master-directory x-symbol-isabelle-master-directory74,2476 +(defvar x-symbol-isabelle-image-searchpath x-symbol-isabelle-image-searchpath75,2529 +(defvar x-symbol-isabelle-image-cached-dirs x-symbol-isabelle-image-cached-dirs76,2581 +(defvar x-symbol-isabelle-image-file-truename-alist x-symbol-isabelle-image-file-truename-alist77,2651 +(defvar x-symbol-isabelle-image-keywords x-symbol-isabelle-image-keywords78,2708 +(defcustom x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher88,3052 +(defcustom x-symbol-isabelle-font-lock-regexp x-symbol-isabelle-font-lock-regexp94,3299 +(defcustom x-symbol-isabelle-font-lock-limit-regexp x-symbol-isabelle-font-lock-limit-regexp99,3483 +(defcustom x-symbol-isabelle-font-lock-contents-regexp x-symbol-isabelle-font-lock-contents-regexp105,3701 +(defcustom x-symbol-isabelle-single-char-regexp x-symbol-isabelle-single-char-regexp115,4078 +(defun x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher121,4288 +(defun isabelle-match-subscript isabelle-match-subscript155,5963 +(defvar x-symbol-isabelle-font-lock-keywordsx-symbol-isabelle-font-lock-keywords164,6358 +(defvar x-symbol-isabelle-font-lock-allowed-faces x-symbol-isabelle-font-lock-allowed-faces171,6626 +(defcustom x-symbol-isabelle-class-alistx-symbol-isabelle-class-alist178,6858 +(defcustom x-symbol-isabelle-class-face-alist x-symbol-isabelle-class-face-alist189,7283 +(defvar x-symbol-isabelle-case-insensitive x-symbol-isabelle-case-insensitive204,7811 +(defvar x-symbol-isabelle-token-shape x-symbol-isabelle-token-shape205,7859 +(defvar x-symbol-isabelle-input-token-ignore x-symbol-isabelle-input-token-ignore206,7902 +(defvar x-symbol-isabelle-token-list x-symbol-isabelle-token-list207,7952 +(defvar x-symbol-isabelle-symbol-table x-symbol-isabelle-symbol-table209,8001 +(defvar x-symbol-isabelle-xsymbol-table x-symbol-isabelle-xsymbol-table308,10712 +(defun x-symbol-isabelle-prepare-table x-symbol-isabelle-prepare-table453,15114 +(defvar x-symbol-isabelle-tablex-symbol-isabelle-table465,15525 +(defcustom x-symbol-isabelle-auto-stylex-symbol-isabelle-auto-style479,15878 +(defcustom x-symbol-isabelle-auto-coding-alist x-symbol-isabelle-auto-coding-alist493,16388 isa/x-symbol-isa.el,0 -isar/isar.el,1882 -(defcustom isar-keywords-name isar-keywords-name25,555 -(defpgdefault completion-table completion-table42,1079 -(defcustom isar-web-pageisar-web-page44,1132 -(defun isar-detect-header isar-detect-header62,1496 -(defun isar-strip-terminators isar-strip-terminators97,2759 -(defun isar-markup-ml isar-markup-ml110,3130 -(defun isar-mode-config-set-variables isar-mode-config-set-variables115,3265 -(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables176,5950 -(defun isar-remove-file isar-remove-file289,10711 -(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list299,11074 -(defun isar-activate-scripting isar-activate-scripting310,11540 -(define-derived-mode isar-shell-mode isar-shell-mode319,11710 -(define-derived-mode isar-response-mode isar-response-mode324,11833 -(define-derived-mode isar-goals-mode isar-goals-mode329,12015 -(define-derived-mode isar-mode isar-mode334,12190 -(defpgdefault menu-entriesmenu-entries367,13546 -(defun isar-count-undos isar-count-undos391,14568 -(defun isar-find-and-forget isar-find-and-forget417,15669 -(defun isar-goal-command-p isar-goal-command-p461,17336 -(defun isar-global-save-command-p isar-global-save-command-p465,17468 -(defvar isar-current-goal isar-current-goal486,18305 -(defun isar-state-preserving-p isar-state-preserving-p489,18371 -(defvar isar-shell-current-line-width isar-shell-current-line-width508,19078 -(defun isar-shell-adjust-line-width isar-shell-adjust-line-width514,19296 -(defun isar-pre-shell-start isar-pre-shell-start534,20179 -(defun isar-preprocessing isar-preprocessing546,20515 -(defun isar-mode-config isar-mode-config569,21726 -(defun isar-shell-mode-config isar-shell-mode-config580,22229 -(defun isar-response-mode-config isar-response-mode-config591,22599 -(defun isar-goals-mode-config isar-goals-mode-config600,22856 +isar/isar.el,1883 +(defcustom isar-keywords-name isar-keywords-name28,631 +(defpgdefault completion-table completion-table45,1155 +(defcustom isar-web-pageisar-web-page47,1208 +(defun isar-detect-header isar-detect-header65,1572 +(defun isar-strip-terminators isar-strip-terminators100,2835 +(defun isar-markup-ml isar-markup-ml113,3206 +(defun isar-mode-config-set-variables isar-mode-config-set-variables118,3341 +(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables182,6172 +(defun isar-remove-file isar-remove-file296,10961 +(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11324 +(defun isar-activate-scripting isar-activate-scripting317,11790 +(define-derived-mode isar-shell-mode isar-shell-mode326,11960 +(define-derived-mode isar-response-mode isar-response-mode331,12083 +(define-derived-mode isar-goals-mode isar-goals-mode336,12265 +(define-derived-mode isar-mode isar-mode341,12440 +(defpgdefault menu-entriesmenu-entries374,13796 +(defun isar-count-undos isar-count-undos398,14818 +(defun isar-find-and-forget isar-find-and-forget424,15919 +(defun isar-goal-command-p isar-goal-command-p471,17764 +(defun isar-global-save-command-p isar-global-save-command-p475,17896 +(defvar isar-current-goal isar-current-goal496,18733 +(defun isar-state-preserving-p isar-state-preserving-p499,18799 +(defvar isar-shell-current-line-width isar-shell-current-line-width521,19757 +(defun isar-shell-adjust-line-width isar-shell-adjust-line-width527,19975 +(defun isar-pre-shell-start isar-pre-shell-start547,20858 +(defun isar-preprocessing isar-preprocessing559,21194 +(defun isar-mode-config isar-mode-config582,22405 +(defun isar-shell-mode-config isar-shell-mode-config593,22908 +(defun isar-response-mode-config isar-response-mode-config604,23278 +(defun isar-goals-mode-config isar-goals-mode-config613,23535 isar/isar-keywords.el,1650 (defconst isar-keywords-majorisar-keywords-major14,378 @@ -1664,99 +1637,102 @@ isar/isar-mmm.el,129 (defconst isar-start-latex-regexp isar-start-latex-regexp23,697 (defconst isar-start-sml-regexp isar-start-sml-regexp35,1130 -isar/isar-syntax.el,4680 -(defun isar-init-syntax-table isar-init-syntax-table17,389 -(defun isar-init-output-syntax-table isar-init-output-syntax-table56,1756 -(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose71,2171 -(defconst isar-keywords-theoryisar-keywords-theory76,2323 -(defconst isar-keywords-saveisar-keywords-save81,2468 -(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose86,2597 -(defconst isar-keywords-proofisar-keywords-proof92,2779 -(defconst isar-keywords-proof-contextisar-keywords-proof-context99,2977 -(defconst isar-keywords-local-goalisar-keywords-local-goal103,3091 -(defconst isar-keywords-improperisar-keywords-improper107,3203 -(defconst isar-keywords-outlineisar-keywords-outline112,3342 -(defconst isar-keywords-fumeisar-keywords-fume115,3407 -(defconst isar-keywords-indent-openisar-keywords-indent-open122,3625 -(defconst isar-keywords-indent-closeisar-keywords-indent-close128,3809 -(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose132,3914 -(defun isar-regexp-simple-alt isar-regexp-simple-alt140,4093 -(defun isar-ids-to-regexp isar-ids-to-regexp160,4854 -(defconst isar-ext-first isar-ext-first194,6122 -(defconst isar-ext-rest isar-ext-rest195,6189 -(defconst isar-long-id-stuff isar-long-id-stuff197,6261 -(defconst isar-id isar-id198,6334 -(defconst isar-idx isar-idx199,6406 -(defconst isar-string isar-string201,6465 -(defconst isar-any-command-regexpisar-any-command-regexp203,6527 -(defconst isar-name-regexpisar-name-regexp207,6661 -(defconst isar-tac-regexpisar-tac-regexp211,6813 -(defconst isar-save-command-regexpisar-save-command-regexp215,6921 -(defconst isar-global-save-command-regexpisar-global-save-command-regexp218,7022 -(defconst isar-goal-command-regexpisar-goal-command-regexp221,7136 -(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp224,7244 -(defconst isar-comment-start isar-comment-start227,7357 -(defconst isar-comment-end isar-comment-end228,7392 -(defconst isar-comment-start-regexp isar-comment-start-regexp229,7425 -(defconst isar-comment-end-regexp isar-comment-end-regexp230,7496 -(defconst isar-string-start-regexp isar-string-start-regexp232,7564 -(defconst isar-string-end-regexp isar-string-end-regexp233,7612 -(defconst isar-antiq-regexpisar-antiq-regexp242,7862 -(defface isabelle-class-name-faceisabelle-class-name-face249,8042 -(defface isabelle-tfree-name-faceisabelle-tfree-name-face259,8317 -(defface isabelle-tvar-name-faceisabelle-tvar-name-face269,8598 -(defface isabelle-free-name-faceisabelle-free-name-face279,8878 -(defface isabelle-bound-name-faceisabelle-bound-name-face289,9154 -(defface isabelle-var-name-faceisabelle-var-name-face299,9433 -(defconst isabelle-class-name-face isabelle-class-name-face309,9712 -(defconst isabelle-tfree-name-face isabelle-tfree-name-face310,9774 -(defconst isabelle-tvar-name-face isabelle-tvar-name-face311,9836 -(defconst isabelle-free-name-face isabelle-free-name-face312,9897 -(defconst isabelle-bound-name-face isabelle-bound-name-face313,9958 -(defconst isabelle-var-name-face isabelle-var-name-face314,10020 -(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1316,10081 -(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1330,11010 -(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords342,11666 -(defconst isar-undo isar-undo373,12300 -(defconst isar-kill isar-kill374,12362 -(defun isar-remove isar-remove376,12392 -(defun isar-undos isar-undos379,12471 -(defun isar-cannot-undo isar-cannot-undo383,12577 -(defconst isar-undo-fail-regexpisar-undo-fail-regexp387,12648 -(defconst isar-undo-skip-regexpisar-undo-skip-regexp391,12786 -(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp394,12907 -(defconst isar-undo-remove-regexpisar-undo-remove-regexp397,12972 -(defconst isar-undo-kill-regexpisar-undo-kill-regexp402,13112 -(defconst isar-any-entity-regexpisar-any-entity-regexp408,13244 -(defconst isar-named-entity-regexpisar-named-entity-regexp412,13391 -(defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp416,13528 -(defconst isar-next-entity-regexpsisar-next-entity-regexps419,13632 -(defconst isar-indent-any-regexpisar-indent-any-regexp427,13815 -(defconst isar-indent-inner-regexpisar-indent-inner-regexp429,13908 -(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp431,13974 -(defconst isar-indent-open-regexpisar-indent-open-regexp433,14090 -(defconst isar-indent-close-regexpisar-indent-close-regexp435,14200 -(defconst isar-outline-regexpisar-outline-regexp441,14337 -(defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp445,14490 +isar/isar-syntax.el,4918 +(defconst isar-script-syntax-table-entries isar-script-syntax-table-entries18,414 +(defconst isar-script-syntax-table-alistisar-script-syntax-table-alist57,1326 +(defun isar-init-syntax-table isar-init-syntax-table66,1609 +(defun isar-init-output-syntax-table isar-init-output-syntax-table74,1857 +(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose89,2272 +(defconst isar-keywords-theoryisar-keywords-theory94,2424 +(defconst isar-keywords-saveisar-keywords-save99,2569 +(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose104,2698 +(defconst isar-keywords-proofisar-keywords-proof110,2880 +(defconst isar-keywords-proof-contextisar-keywords-proof-context117,3078 +(defconst isar-keywords-local-goalisar-keywords-local-goal121,3192 +(defconst isar-keywords-improperisar-keywords-improper125,3304 +(defconst isar-keywords-outlineisar-keywords-outline130,3443 +(defconst isar-keywords-fumeisar-keywords-fume133,3508 +(defconst isar-keywords-indent-openisar-keywords-indent-open140,3726 +(defconst isar-keywords-indent-closeisar-keywords-indent-close146,3910 +(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose150,4015 +(defun isar-regexp-simple-alt isar-regexp-simple-alt158,4194 +(defun isar-ids-to-regexp isar-ids-to-regexp178,4955 +(defconst isar-ext-first isar-ext-first212,6223 +(defconst isar-ext-rest isar-ext-rest213,6290 +(defconst isar-long-id-stuff isar-long-id-stuff215,6362 +(defconst isar-id isar-id216,6436 +(defconst isar-idx isar-idx217,6506 +(defconst isar-string isar-string219,6565 +(defconst isar-any-command-regexpisar-any-command-regexp221,6627 +(defconst isar-name-regexpisar-name-regexp225,6761 +(defconst isar-tac-regexpisar-tac-regexp229,6930 +(defconst isar-save-command-regexpisar-save-command-regexp233,7038 +(defconst isar-global-save-command-regexpisar-global-save-command-regexp236,7139 +(defconst isar-goal-command-regexpisar-goal-command-regexp239,7253 +(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp242,7361 +(defconst isar-comment-start isar-comment-start245,7474 +(defconst isar-comment-end isar-comment-end246,7509 +(defconst isar-comment-start-regexp isar-comment-start-regexp247,7542 +(defconst isar-comment-end-regexp isar-comment-end-regexp248,7613 +(defconst isar-string-start-regexp isar-string-start-regexp250,7681 +(defconst isar-string-end-regexp isar-string-end-regexp251,7729 +(defconst isar-antiq-regexpisar-antiq-regexp260,7979 +(defface isabelle-class-name-faceisabelle-class-name-face267,8159 +(defface isabelle-tfree-name-faceisabelle-tfree-name-face277,8434 +(defface isabelle-tvar-name-faceisabelle-tvar-name-face287,8715 +(defface isabelle-free-name-faceisabelle-free-name-face297,8995 +(defface isabelle-bound-name-faceisabelle-bound-name-face307,9271 +(defface isabelle-var-name-faceisabelle-var-name-face317,9550 +(defconst isabelle-class-name-face isabelle-class-name-face327,9829 +(defconst isabelle-tfree-name-face isabelle-tfree-name-face328,9891 +(defconst isabelle-tvar-name-face isabelle-tvar-name-face329,9953 +(defconst isabelle-free-name-face isabelle-free-name-face330,10014 +(defconst isabelle-bound-name-face isabelle-bound-name-face331,10075 +(defconst isabelle-var-name-face isabelle-var-name-face332,10137 +(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1334,10198 +(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1348,11127 +(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords360,11783 +(defconst isar-undo isar-undo391,12417 +(defconst isar-kill isar-kill392,12479 +(defun isar-remove isar-remove394,12509 +(defun isar-undos isar-undos397,12588 +(defun isar-cannot-undo isar-cannot-undo401,12694 +(defconst isar-undo-fail-regexpisar-undo-fail-regexp405,12765 +(defconst isar-undo-skip-regexpisar-undo-skip-regexp409,12903 +(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp412,13024 +(defconst isar-undo-remove-regexpisar-undo-remove-regexp415,13089 +(defconst isar-undo-kill-regexpisar-undo-kill-regexp420,13229 +(defconst isar-any-entity-regexpisar-any-entity-regexp426,13371 +(defconst isar-named-entity-regexpisar-named-entity-regexp431,13558 +(defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp436,13735 +(defconst isar-next-entity-regexpsisar-next-entity-regexps439,13837 +(defconst isar-generic-expressionisar-generic-expression447,14144 +(defconst isar-indent-any-regexpisar-indent-any-regexp458,14378 +(defconst isar-indent-inner-regexpisar-indent-inner-regexp460,14471 +(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp462,14537 +(defconst isar-indent-open-regexpisar-indent-open-regexp464,14653 +(defconst isar-indent-close-regexpisar-indent-close-regexp466,14763 +(defconst isar-outline-regexpisar-outline-regexp472,14900 +(defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp476,15053 isar/x-symbol-isar.el,0 lclam/lclam.el,805 -(defcustom lclam-prog-name lclam-prog-name15,341 -(defcustom lclam-web-pagelclam-web-page21,489 -(defun lclam-config lclam-config32,719 -(defun lclam-shell-config lclam-shell-config52,1433 -(define-derived-mode lclam-proofscript-mode lclam-proofscript-mode72,2092 -(define-derived-mode lclam-shell-mode lclam-shell-mode77,2215 -(define-derived-mode lclam-response-mode lclam-response-mode82,2349 -(define-derived-mode lclam-goals-mode lclam-goals-mode86,2472 -(defun lclam-mode lclam-mode94,2700 -(defun lclam-pre-shell-start lclam-pre-shell-start107,2983 -(define-derived-mode thy-mode thy-mode141,3926 -(defvar thy-mode-map thy-mode-map144,4024 -(defun thy-add-menus thy-add-menus146,4051 -(defun process-thy-file process-thy-file186,5965 -(defun update-thy-only update-thy-only192,6166 +(defcustom lclam-prog-name lclam-prog-name15,385 +(defcustom lclam-web-pagelclam-web-page21,533 +(defun lclam-config lclam-config32,763 +(defun lclam-shell-config lclam-shell-config52,1477 +(define-derived-mode lclam-proofscript-mode lclam-proofscript-mode72,2136 +(define-derived-mode lclam-shell-mode lclam-shell-mode77,2259 +(define-derived-mode lclam-response-mode lclam-response-mode82,2393 +(define-derived-mode lclam-goals-mode lclam-goals-mode86,2516 +(defun lclam-mode lclam-mode94,2744 +(defun lclam-pre-shell-start lclam-pre-shell-start107,3027 +(define-derived-mode thy-mode thy-mode141,3970 +(defvar thy-mode-map thy-mode-map144,4068 +(defun thy-add-menus thy-add-menus146,4095 +(defun process-thy-file process-thy-file186,6009 +(defun update-thy-only update-thy-only192,6210 lego/lego.el,2717 (defcustom lego-tags lego-tags19,493 @@ -1821,32 +1797,7 @@ lego/lego-syntax.el,919 (defvar lego-font-lock-keywords-1lego-font-lock-keywords-199,3667 (defun lego-init-syntax-table lego-init-syntax-table110,4134 -lego/x-symbol-lego.el,1868 -(defvar x-symbol-lego-symbol-table x-symbol-lego-symbol-table9,206 -(defvar x-symbol-lego-master-directory x-symbol-lego-master-directory48,1583 -(defvar x-symbol-lego-image-searchpath x-symbol-lego-image-searchpath49,1631 -(defvar x-symbol-lego-image-cached-dirs x-symbol-lego-image-cached-dirs50,1679 -(defvar x-symbol-lego-image-keywords x-symbol-lego-image-keywords51,1745 -(defvar x-symbol-lego-font-lock-keywords x-symbol-lego-font-lock-keywords52,1787 -(defvar x-symbol-lego-header-groups-alist x-symbol-lego-header-groups-alist53,1833 -(defvar x-symbol-lego-class-alist x-symbol-lego-class-alist54,1880 -(defvar x-symbol-lego-class-face-alist x-symbol-lego-class-face-alist57,2020 -(defvar x-symbol-lego-electric-ignore x-symbol-lego-electric-ignore58,2064 -(defvar x-symbol-lego-required-fonts x-symbol-lego-required-fonts59,2107 -(defvar x-symbol-lego-case-insensitive x-symbol-lego-case-insensitive60,2149 -(defvar x-symbol-lego-token-shape x-symbol-lego-token-shape63,2301 -(defvar x-symbol-lego-table x-symbol-lego-table64,2368 -(defun x-symbol-lego-default-token-list x-symbol-lego-default-token-list65,2424 -(defvar x-symbol-lego-token-list x-symbol-lego-token-list66,2481 -(defvar x-symbol-lego-input-token-ignore x-symbol-lego-input-token-ignore67,2549 -(defvar x-symbol-lego-exec-specs x-symbol-lego-exec-specs70,2615 -(defvar x-symbol-lego-menu-alist x-symbol-lego-menu-alist71,2653 -(defvar x-symbol-lego-grid-alist x-symbol-lego-grid-alist72,2691 -(defvar x-symbol-lego-decode-atree x-symbol-lego-decode-atree73,2729 -(defvar x-symbol-lego-decode-alist x-symbol-lego-decode-alist74,2769 -(defvar x-symbol-lego-encode-alist x-symbol-lego-encode-alist75,2809 -(defvar x-symbol-lego-nomule-decode-exec x-symbol-lego-nomule-decode-exec76,2849 -(defvar x-symbol-lego-nomule-encode-exec x-symbol-lego-nomule-encode-exec77,2895 +lego/x-symbol-lego.el,0 mmm/mmm-auto.el,499 (defvar mmm-autoloaded-classesmmm-autoloaded-classes67,2675 @@ -2082,13 +2033,13 @@ phox/phox.el,886 (defcustom phox-etags phox-etags70,1867 (defpgdefault menu-entriesmenu-entries90,2297 (defun phox-config phox-config107,2626 -(defun phox-shell-config phox-shell-config147,4476 -(define-derived-mode phox-mode phox-mode187,6056 -(define-derived-mode phox-shell-mode phox-shell-mode202,6500 -(define-derived-mode phox-response-mode phox-response-mode207,6628 -(define-derived-mode phox-goals-mode phox-goals-mode219,7047 -(defun phox-pre-shell-start phox-pre-shell-start245,8106 -(defpgdefault completion-tablecompletion-table259,8620 +(defun phox-shell-config phox-shell-config149,4550 +(define-derived-mode phox-mode phox-mode189,6130 +(define-derived-mode phox-shell-mode phox-shell-mode204,6574 +(define-derived-mode phox-response-mode phox-response-mode209,6702 +(define-derived-mode phox-goals-mode phox-goals-mode221,7121 +(defun phox-pre-shell-start phox-pre-shell-start247,8180 +(defpgdefault completion-tablecompletion-table261,8694 phox/phox-extraction.el,603 (defvar phox-prog-orig phox-prog-orig11,480 @@ -2175,41 +2126,41 @@ phox/phox-tags.el,483 (defvar phox-tags-menuphox-tags-menu96,2904 phox/x-symbol-phox.el,2672 -(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts21,706 -(defvar x-symbol-phox-name x-symbol-phox-name31,1205 -(defvar x-symbol-phox-modeline-name x-symbol-phox-modeline-name32,1247 -(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist34,1292 -(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore41,1512 -(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts48,1760 -(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items51,1861 -(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar55,1951 -(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar66,2457 -(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list72,2712 -(defvar x-symbol-phox-user-table x-symbol-phox-user-table84,3001 -(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data87,3110 -(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory95,3349 -(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath96,3398 -(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs97,3446 -(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist98,3512 -(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords99,3565 -(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist105,3785 -(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist116,4167 -(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords126,4480 -(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces128,4527 -(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive134,4752 -(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape135,4796 -(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore136,4835 -(defvar x-symbol-phox-token-list x-symbol-phox-token-list143,5074 -(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table145,5119 -(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table166,5574 -(defvar x-symbol-phox-tablex-symbol-phox-table173,5745 -(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist184,6117 -(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist186,6207 -(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree189,6298 -(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist191,6391 -(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist193,6488 -(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec197,6645 -(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec199,6745 +(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts21,705 +(defvar x-symbol-phox-name x-symbol-phox-name31,1204 +(defvar x-symbol-phox-modeline-name x-symbol-phox-modeline-name32,1246 +(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist34,1291 +(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore41,1511 +(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts48,1759 +(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items51,1860 +(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar55,1950 +(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar66,2456 +(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list72,2711 +(defvar x-symbol-phox-user-table x-symbol-phox-user-table84,3000 +(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data87,3109 +(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory95,3348 +(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath96,3397 +(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs97,3445 +(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist98,3511 +(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords99,3564 +(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist105,3784 +(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist116,4166 +(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords126,4479 +(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces128,4526 +(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive134,4751 +(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape135,4795 +(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore136,4834 +(defvar x-symbol-phox-token-list x-symbol-phox-token-list143,5073 +(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table145,5118 +(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table166,5573 +(defvar x-symbol-phox-tablex-symbol-phox-table173,5744 +(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist184,6116 +(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist186,6206 +(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree189,6297 +(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist191,6390 +(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist193,6487 +(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec197,6644 +(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec199,6744 plastic/plastic.el,4425 (defcustom plastic-tags plastic-tags28,805 @@ -2299,20 +2250,20 @@ plastic/plastic-syntax.el,1015 (defvar plastic-font-lock-keywords-1plastic-font-lock-keywords-199,3792 (defun plastic-init-syntax-table plastic-init-syntax-table108,4184 -twelf/twelf.el,676 +twelf/twelf.el,677 (defcustom twelf-root-dirtwelf-root-dir25,591 (defcustom twelf-info-dirtwelf-info-dir31,749 -(defun twelf-add-read-declaration twelf-add-read-declaration97,3171 -(defun twelf-set-syntax twelf-set-syntax110,3506 -(defun twelf-set-word twelf-set-word112,3603 -(defun twelf-set-symbol twelf-set-symbol113,3665 -(defun twelf-map-string twelf-map-string115,3729 -(defun twelf-mode-extra-config twelf-mode-extra-config162,5791 -(defconst twelf-syntax-menutwelf-syntax-menu168,5997 -(defpacustom chatter chatter182,6364 -(defpacustom double-check double-check187,6457 -(defpacustom print-implicit print-implicit191,6594 -(defpgdefault menu-entriesmenu-entries203,6738 +(defun twelf-add-read-declaration twelf-add-read-declaration100,3259 +(defun twelf-set-syntax twelf-set-syntax113,3594 +(defun twelf-set-word twelf-set-word115,3691 +(defun twelf-set-symbol twelf-set-symbol116,3753 +(defun twelf-map-string twelf-map-string118,3817 +(defun twelf-mode-extra-config twelf-mode-extra-config165,5879 +(defconst twelf-syntax-menutwelf-syntax-menu171,6085 +(defpacustom chatter chatter185,6452 +(defpacustom double-check double-check190,6545 +(defpacustom print-implicit print-implicit194,6682 +(defpgdefault menu-entriesmenu-entries206,6826 twelf/twelf-font.el,1425 (defun twelf-font-create-face twelf-font-create-face31,836 @@ -2519,200 +2470,189 @@ twelf/twelf-old.el,10513 (defun twelf-server-remove-menu twelf-server-remove-menu2651,107262 (defun twelf-server-reset-menu twelf-server-reset-menu2655,107374 -twelf/x-symbol-twelf.el,1918 -(defvar x-symbol-twelf-symbol-table x-symbol-twelf-symbol-table8,159 -(defvar x-symbol-twelf-master-directory x-symbol-twelf-master-directory52,1785 -(defvar x-symbol-twelf-image-searchpath x-symbol-twelf-image-searchpath53,1834 -(defvar x-symbol-twelf-image-cached-dirs x-symbol-twelf-image-cached-dirs54,1883 -(defvar x-symbol-twelf-image-keywords x-symbol-twelf-image-keywords55,1950 -(defvar x-symbol-twelf-font-lock-keywords x-symbol-twelf-font-lock-keywords56,1993 -(defvar x-symbol-twelf-header-groups-alist x-symbol-twelf-header-groups-alist57,2040 -(defvar x-symbol-twelf-class-alist x-symbol-twelf-class-alist58,2088 -(defvar x-symbol-twelf-class-face-alist x-symbol-twelf-class-face-alist61,2231 -(defvar x-symbol-twelf-electric-ignore x-symbol-twelf-electric-ignore62,2276 -(defvar x-symbol-twelf-required-fonts x-symbol-twelf-required-fonts63,2320 -(defvar x-symbol-twelf-case-insensitive x-symbol-twelf-case-insensitive64,2363 -(defvar x-symbol-twelf-token-shape x-symbol-twelf-token-shape67,2516 -(defvar x-symbol-twelf-table x-symbol-twelf-table68,2584 -(defun x-symbol-twelf-default-token-list x-symbol-twelf-default-token-list69,2642 -(defvar x-symbol-twelf-token-list x-symbol-twelf-token-list70,2700 -(defvar x-symbol-twelf-input-token-ignore x-symbol-twelf-input-token-ignore71,2770 -(defvar x-symbol-twelf-exec-specs x-symbol-twelf-exec-specs74,2837 -(defvar x-symbol-twelf-menu-alist x-symbol-twelf-menu-alist75,2876 -(defvar x-symbol-twelf-grid-alist x-symbol-twelf-grid-alist76,2915 -(defvar x-symbol-twelf-decode-atree x-symbol-twelf-decode-atree77,2954 -(defvar x-symbol-twelf-decode-alist x-symbol-twelf-decode-alist78,2995 -(defvar x-symbol-twelf-encode-alist x-symbol-twelf-encode-alist79,3036 -(defvar x-symbol-twelf-nomule-decode-exec x-symbol-twelf-nomule-decode-exec80,3077 -(defvar x-symbol-twelf-nomule-encode-exec x-symbol-twelf-nomule-encode-exec81,3124 - -todo,742 - function to to410,16315 +twelf/x-symbol-twelf.el,0 + +todo,1296 + function to to364,15045 $Id: todo,2,21 -This is an outline file. Use C-c C-n,4,68 - -- with multiple frame mode,12,328 - E.g. twelf,131,4631 - E.g. twelf, ACL2,131,4631 - Also,132,4667 -*** C Improved configurability of command settings,184,6779 - We should let command settings,185,6836 - We should let command settings, etc,185,6836 - Save foo;435,17404 -*** D Fix INFO-DIR-ENTRY in 536,21351 -*** C Fixing up errors caused by pbp-generated commands; currently,598,23697 - should mean generates an error. With LEGO pbp,601,23903 - tactic which always succeeds,602,23967 - decodes annotations eagerly. Lazily would be faster,610,24323 - the tech report claims --- djs: probably not much faster,611,24392 - -doc/ProofGeneral.texi,5607 -@node TopTop160,4965 -@node PrefacePreface196,6070 -@node Latest news for 3.5Latest news for 3.5219,6658 -@node FutureFuture250,7831 -@node CreditsCredits286,9095 -@node Introducing Proof GeneralIntroducing Proof General381,12444 -@node Quick start guideQuick start guide436,14436 -@node Features of Proof GeneralFeatures of Proof General488,16854 -@node Supported proof assistantsSupported proof assistants577,20779 -@node Prerequisites for this manualPrerequisites for this manual622,22512 -@node Organization of this manualOrganization of this manual666,24138 -@node Basic Script ManagementBasic Script Management692,24965 -@node Walkthrough example in LEGOWalkthrough example in LEGO711,25561 -@node Proof scriptsProof scripts863,30612 -@node Script buffersScript buffers906,32732 -@node Locked queue and editing regionsLocked queue and editing regions928,33309 -@node Goal-save sequencesGoal-save sequences984,35456 -@node Active scripting bufferActive scripting buffer1021,36930 -@node Summary of Proof General buffersSummary of Proof General buffers1090,40350 -@node Script editing commandsScript editing commands1152,43024 -@node Script processing commandsScript processing commands1230,45788 -@node Proof assistant commandsProof assistant commands1358,51089 -@node Toolbar commandsToolbar commands1518,56652 -@node Interrupting during trace outputInterrupting during trace output1542,57581 -@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1581,59504 -@node Goals buffer commandsGoals buffer commands1595,60004 -@node Advanced Script ManagementAdvanced Script Management1685,63537 -@node Visibility of completed proofsVisibility of completed proofs1716,64691 -@node Switching between proof scriptsSwitching between proof scripts1771,66614 -@node View of processed files View of processed files 1808,68586 -@node Retracting across filesRetracting across files1868,71637 -@node Asserting across filesAsserting across files1881,72268 -@node Automatic multiple file handlingAutomatic multiple file handling1894,72834 -@node Escaping script managementEscaping script management1919,73868 -@node Experimental featuresExperimental features1977,76071 -@node Support for other PackagesSupport for other Packages2014,77441 -@node Syntax highlightingSyntax highlighting2046,78306 -@node X-Symbol supportX-Symbol support2085,79912 -@node Support for function menusSupport for function menus2144,82458 -@node Support for outline modeSupport for outline mode2173,83754 -@node Support for completionSupport for completion2192,84517 -@node Support for tagsSupport for tags2250,86681 -@node Customizing Proof GeneralCustomizing Proof General2302,89009 -@node Basic optionsBasic options2342,90679 -@node How to customizeHow to customize2366,91437 -@node Display customizationDisplay customization2417,93527 -@node User optionsUser options2523,97560 -@node Changing facesChanging faces2778,106633 -@node Tweaking configuration settingsTweaking configuration settings2853,109302 -@node Hints and TipsHints and Tips2910,111827 -@node Adding your own keybindingsAdding your own keybindings2929,112428 -@node Using file variablesUsing file variables2985,114961 -@node Using abbreviationsUsing abbreviations3038,116790 -@node LEGO Proof GeneralLEGO Proof General3101,118609 -@node LEGO specific commandsLEGO specific commands3142,119978 -@node LEGO tagsLEGO tags3162,120433 -@node LEGO customizationsLEGO customizations3172,120680 -@node Coq Proof GeneralCoq Proof General3204,121598 -@node Coq-specific commandsCoq-specific commands3219,121989 -@node Coq-specific variablesCoq-specific variables3241,122496 -@node Editing multiple proofsEditing multiple proofs3279,123656 -@node User-loaded tacticsUser-loaded tactics3303,124764 -@node Isabelle Proof GeneralIsabelle Proof General3371,127346 -@node Classic IsabelleClassic Isabelle3438,130521 -@node ML filesML files3454,130959 -@node Theory filesTheory files3525,133384 -@node General commands for IsabelleGeneral commands for Isabelle3579,135855 -@node Specific commands for IsabelleSpecific commands for Isabelle3591,136337 -@node Isabelle customizationsIsabelle customizations3620,137277 -@node Isabelle/IsarIsabelle/Isar3685,139375 -@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3706,140143 -@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3713,140397 -@node HOL Proof GeneralHOL Proof General3793,142641 -@node Obtaining and InstallingObtaining and Installing3835,144422 -@node Obtaining Proof GeneralObtaining Proof General3851,144835 -@node Installing Proof General from tarballInstalling Proof General from tarball3882,146074 -@node Installing Proof General from RPM packageInstalling Proof General from RPM package3907,146906 -@node Setting the names of binariesSetting the names of binaries3922,147314 -@node Notes for syssiesNotes for syssies3950,148242 -@node Known bugs and workaroundsKnown bugs and workarounds4023,151191 -@node ReferencesReferences4036,151624 -@node History of Proof GeneralHistory of Proof General4076,152648 -@node Old News for 3.0Old News for 3.04167,156750 -@node Old News for 3.1Old News for 3.14237,160444 -@node Old News for 3.2Old News for 3.24263,161616 -@node Old News for 3.3Old News for 3.34324,164619 -@node Old News for 3.4Old News for 3.44343,165516 -@node Function IndexFunction Index4366,166572 -@node Variable IndexVariable Index4370,166648 -@node Keystroke IndexKeystroke Index4374,166728 -@node Concept IndexConcept Index4378,166794 - -doc/PG-adapting.texi,3785 +This is an outline file. Use C-c C-n,4,67 +X 32,944 +*** C Improved configurability of command settings,163,6426 + We should let command settings,164,6483 + We should let command settings, etc,164,6483 + - XEmacs pg forces on font-lock,314,12632 + Save foo;390,16168 +*** A Doc new bits: font lock keywords,460,18869 +*** A Doc new bits: font lock keywords, filename %e,460,18869 + Added proof-{script,461,18926 + Added proof-{script,shell,461,18926 + Added proof-{script,shell,goals,461,18926 + Presently used only in proof-easy-config,462,18986 + - Mention configuring function menus,473,19322 + - document mouse functions,475,19408 + - document mouse functions, proof-cd,475,19408 + - document mouse functions, proof-cd, process quit timeout,475,19408 + X-Symbol,476,19471 + X-Symbol, prog-name-guess,476,19471 +*** D Fix INFO-DIR-ENTRY in 490,19979 +*** C Fixing up errors caused by pbp-generated commands; currently,556,22430 + should mean generates an error. With LEGO pbp,559,22636 + tactic which always succeeds,560,22700 + decodes annotations eagerly. Lazily would be faster,568,23056 + the tech report claims --- djs: probably not much faster,569,23125 +*** 6. Update Emacs and prover versions in texi,658,26128 + +doc/ProofGeneral.texi,5815 +@node TopTop166,5018 +@node PrefacePreface203,6141 +@node Latest news for 3.5Latest news for 3.5226,6729 +@node FutureFuture264,8387 +@node CreditsCredits299,9937 +@node Introducing Proof GeneralIntroducing Proof General397,13352 +@node Quick start guideQuick start guide452,15344 +@node Features of Proof GeneralFeatures of Proof General506,17913 +@node Supported proof assistantsSupported proof assistants595,21838 +@node Prerequisites for this manualPrerequisites for this manual647,23834 +@node Organization of this manualOrganization of this manual691,25460 +@node Basic Script ManagementBasic Script Management717,26287 +@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar736,26892 +@node Proof scriptsProof scripts963,35427 +@node Script buffersScript buffers1006,37547 +@node Locked queue and editing regionsLocked queue and editing regions1028,38124 +@node Goal-save sequencesGoal-save sequences1084,40271 +@node Active scripting bufferActive scripting buffer1121,41757 +@node Summary of Proof General buffersSummary of Proof General buffers1190,45177 +@node Script editing commandsScript editing commands1252,47851 +@node Script processing commandsScript processing commands1330,50615 +@node Proof assistant commandsProof assistant commands1458,55916 +@node Toolbar commandsToolbar commands1620,61579 +@node Interrupting during trace outputInterrupting during trace output1644,62508 +@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1683,64431 +@node Goals buffer commandsGoals buffer commands1697,64931 +@node Advanced Script ManagementAdvanced Script Management1787,68464 +@node Visibility of completed proofsVisibility of completed proofs1818,69618 +@node Switching between proof scriptsSwitching between proof scripts1873,71541 +@node View of processed files View of processed files 1910,73513 +@node Retracting across filesRetracting across files1970,76564 +@node Asserting across filesAsserting across files1983,77195 +@node Automatic multiple file handlingAutomatic multiple file handling1996,77761 +@node Escaping script managementEscaping script management2021,78795 +@node Experimental featuresExperimental features2079,80998 +@node Support for other PackagesSupport for other Packages2113,82260 +@node Syntax highlightingSyntax highlighting2145,83135 +@node X-Symbol supportX-Symbol support2184,84744 +@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2243,87290 +@node Support for outline modeSupport for outline mode2302,89420 +@node Support for completionSupport for completion2328,90550 +@node Support for tagsSupport for tags2385,92713 +@node Customizing Proof GeneralCustomizing Proof General2437,95041 +@node Basic optionsBasic options2477,96711 +@node How to customizeHow to customize2501,97469 +@node Display customizationDisplay customization2552,99559 +@node User optionsUser options2666,104169 +@node Changing facesChanging faces2920,113175 +@node Tweaking configuration settingsTweaking configuration settings2995,115844 +@node Hints and TipsHints and Tips3052,118369 +@node Adding your own keybindingsAdding your own keybindings3071,118970 +@node Using file variablesUsing file variables3127,121503 +@node Using abbreviationsUsing abbreviations3180,123326 +@node LEGO Proof GeneralLEGO Proof General3219,124741 +@node LEGO specific commandsLEGO specific commands3260,126110 +@node LEGO tagsLEGO tags3280,126565 +@node LEGO customizationsLEGO customizations3290,126812 +@node Coq Proof GeneralCoq Proof General3322,127730 +@node Coq-specific commandsCoq-specific commands3338,128139 +@node Coq-specific variablesCoq-specific variables3360,128646 +@node Editing multiple proofsEditing multiple proofs3398,129861 +@node User-loaded tacticsUser-loaded tactics3422,130969 +@node Holes featureHoles feature3487,133496 +@node Isabelle Proof GeneralIsabelle Proof General3514,134782 +@node Classic IsabelleClassic Isabelle3583,138105 +@node ML filesML files3599,138543 +@node Theory filesTheory files3670,140968 +@node General commands for IsabelleGeneral commands for Isabelle3724,143439 +@node Specific commands for IsabelleSpecific commands for Isabelle3736,143921 +@node Isabelle customizationsIsabelle customizations3765,144861 +@node Isabelle/IsarIsabelle/Isar3830,146959 +@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3851,147722 +@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3858,147976 +@node Logics and SettingsLogics and Settings3945,150504 +@node HOL Proof GeneralHOL Proof General3986,152192 +@node Shell Proof GeneralShell Proof General4027,153976 +@node Obtaining and InstallingObtaining and Installing4063,155434 +@node Obtaining Proof GeneralObtaining Proof General4079,155847 +@node Installing Proof General from tarballInstalling Proof General from tarball4110,157086 +@node Installing Proof General from RPM packageInstalling Proof General from RPM package4135,157918 +@node Setting the names of binariesSetting the names of binaries4150,158326 +@node Notes for syssiesNotes for syssies4178,159254 +@node Known bugs and workaroundsKnown bugs and workarounds4251,162203 +@node ReferencesReferences4264,162636 +@node History of Proof GeneralHistory of Proof General4304,163660 +@node Old News for 3.0Old News for 3.04395,167762 +@node Old News for 3.1Old News for 3.14465,171456 +@node Old News for 3.2Old News for 3.24491,172628 +@node Old News for 3.3Old News for 3.34552,175631 +@node Old News for 3.4Old News for 3.44571,176528 +@node Function IndexFunction Index4594,177584 +@node Variable IndexVariable Index4598,177660 +@node Keystroke IndexKeystroke Index4602,177740 +@node Concept IndexConcept Index4606,177806 + +doc/PG-adapting.texi,3791 @node TopTop157,4774 @node IntroductionIntroduction194,5888 @node FutureFuture235,7541 @node CreditsCredits271,9137 @node Beginning with a new proverBeginning with a new prover281,9429 @node Overview of adding a new proverOverview of adding a new prover322,11378 -@node Demonstration instance and easy configurationDemonstration instance and easy configuration396,14706 -@node Major modes used by Proof GeneralMajor modes used by Proof General465,18097 -@node Menus and toolbar and user-level commandsMenus and toolbar and user-level commands538,21180 -@node Settings for generic user-level commandsSettings for generic user-level commands553,21726 -@node Menu configurationMenu configuration598,23462 -@node Toolbar configurationToolbar configuration622,24380 -@node Proof script settingsProof script settings680,26625 -@node Recognizing commands and commentsRecognizing commands and comments702,27205 -@node Recognizing proofsRecognizing proofs820,32636 -@node Recognizing other elementsRecognizing other elements923,37030 -@node Configuring undo behaviourConfiguring undo behaviour989,39969 -@node Nested proofsNested proofs1128,45311 -@node Safe (state-preserving) commandsSafe (state-preserving) commands1168,46938 -@node Activate scripting hookActivate scripting hook1191,47884 -@node Automatic multiple filesAutomatic multiple files1215,48748 -@node CompletionsCompletions1237,49595 -@node Proof shell settingsProof shell settings1277,51071 -@node Proof shell commandsProof shell commands1308,52353 -@node Script input to the shellScript input to the shell1466,59008 -@node Settings for matching various output from proof processSettings for matching various output from proof process1533,62051 -@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1663,67719 -@node Hooks and other settingsHooks and other settings1843,75803 -@node Goals buffer settingsGoals buffer settings1939,79636 -@node Splash screen settingsSplash screen settings2016,82744 -@node Global constantsGlobal constants2042,83502 -@node Handling multiple filesHandling multiple files2068,84351 -@node Configuring Font LockConfiguring Font Lock2206,91418 -@node Configuring X-SymbolConfiguring X-Symbol2249,93311 -@node Writing more lisp codeWriting more lisp code2309,95834 -@node Default values for generic settingsDefault values for generic settings2326,96479 -@node Adding prover-specific configurationsAdding prover-specific configurations2356,97562 -@node Useful variablesUseful variables2399,98832 -@node Useful functions and macrosUseful functions and macros2420,99337 -@node Internals of Proof GeneralInternals of Proof General2524,103232 -@node SpansSpans2552,104140 -@node Proof General site configurationProof General site configuration2565,104514 -@node Configuration variable mechanismsConfiguration variable mechanisms2645,107630 -@node Global variablesGlobal variables2763,112866 -@node Proof script modeProof script mode2833,115416 -@node Proof shell modeProof shell mode3093,127070 -@node DebuggingDebugging3507,143125 -@node Plans and ideasPlans and ideas3550,144020 -@node Proof by pointing and similar featuresProof by pointing and similar features3571,144742 -@node Granularity of atomic command sequencesGranularity of atomic command sequences3609,146400 -@node Browser mode for script files and theoriesBrowser mode for script files and theories3654,148625 -@node Demonstration InstantiationsDemonstration Instantiations3684,149656 -@node demoisa-easy.eldemoisa-easy.el3700,150087 -@node demoisa.eldemoisa.el3763,152326 -@node Function IndexFunction Index3931,157843 -@node Variable IndexVariable Index3935,157919 -@node Concept IndexConcept Index3944,158098 +@node Demonstration instance and easy configurationDemonstration instance and easy configuration396,14799 +@node Major modes used by Proof GeneralMajor modes used by Proof General465,18190 +@node Menus and toolbar and user-level commandsMenus and toolbar and user-level commands538,21273 +@node Settings for generic user-level commandsSettings for generic user-level commands553,21819 +@node Menu configurationMenu configuration598,23555 +@node Toolbar configurationToolbar configuration622,24473 +@node Proof script settingsProof script settings680,26718 +@node Recognizing commands and commentsRecognizing commands and comments702,27298 +@node Recognizing proofsRecognizing proofs823,32825 +@node Recognizing other elementsRecognizing other elements936,37640 +@node Configuring undo behaviourConfiguring undo behaviour1062,43118 +@node Nested proofsNested proofs1201,48460 +@node Safe (state-preserving) commandsSafe (state-preserving) commands1241,50087 +@node Activate scripting hookActivate scripting hook1264,51033 +@node Automatic multiple filesAutomatic multiple files1288,51897 +@node CompletionsCompletions1310,52744 +@node Proof shell settingsProof shell settings1350,54220 +@node Proof shell commandsProof shell commands1381,55502 +@node Script input to the shellScript input to the shell1539,62157 +@node Settings for matching various output from proof processSettings for matching various output from proof process1606,65200 +@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1737,70964 +@node Hooks and other settingsHooks and other settings1931,79717 +@node Goals buffer settingsGoals buffer settings2027,83550 +@node Splash screen settingsSplash screen settings2104,86658 +@node Global constantsGlobal constants2130,87416 +@node Handling multiple filesHandling multiple files2156,88265 +@node Configuring Font LockConfiguring Font Lock2308,96049 +@node Configuring X-SymbolConfiguring X-Symbol2351,97942 +@node Writing more lisp codeWriting more lisp code2411,100465 +@node Default values for generic settingsDefault values for generic settings2428,101110 +@node Adding prover-specific configurationsAdding prover-specific configurations2458,102193 +@node Useful variablesUseful variables2501,103463 +@node Useful functions and macrosUseful functions and macros2522,103968 +@node Internals of Proof GeneralInternals of Proof General2625,107795 +@node SpansSpans2653,108703 +@node Proof General site configurationProof General site configuration2666,109077 +@node Configuration variable mechanismsConfiguration variable mechanisms2746,112221 +@node Global variablesGlobal variables2864,117457 +@node Proof script modeProof script mode2934,120007 +@node Proof shell modeProof shell mode3193,131662 +@node DebuggingDebugging3607,147717 +@node Plans and ideasPlans and ideas3650,148612 +@node Proof by pointing and similar featuresProof by pointing and similar features3671,149334 +@node Granularity of atomic command sequencesGranularity of atomic command sequences3709,150992 +@node Browser mode for script files and theoriesBrowser mode for script files and theories3754,153217 +@node Demonstration InstantiationsDemonstration Instantiations3784,154248 +@node demoisa-easy.eldemoisa-easy.el3800,154679 +@node demoisa.eldemoisa.el3863,156917 +@node Function IndexFunction Index4031,162433 +@node Variable IndexVariable Index4035,162509 +@node Concept IndexConcept Index4044,162688 |