diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-03-17 17:05:48 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-03-17 17:05:48 +0000 |
| commit | 116cb433b17154d3d6297a89e56b6d467655b9dc (patch) | |
| tree | f430c32a024417fe2d39b82180569bb1913bb091 /TAGS | |
| parent | 67251e5d346f954679b86a7f2ffa19be826fb909 (diff) | |
New files.
Diffstat (limited to 'TAGS')
| -rw-r--r-- | TAGS | 2321 |
1 files changed, 2321 insertions, 0 deletions
@@ -0,0 +1,2321 @@ + +generic/pg-assoc.el,342 +(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 + +generic/pg-goals.el,1074 +(define-derived-mode proof-goals-mode proof-goals-mode24,570 +(define-key proof-goals-mode-map proof-goals-mode-map44,1260 +(define-key proof-goals-mode-map proof-goals-mode-map47,1343 +(define-key proof-goals-mode-map proof-goals-mode-map48,1413 +(define-key proof-goals-mode-map proof-goals-mode-map53,1829 +(define-key proof-goals-mode-map proof-goals-mode-map55,1902 +(define-key proof-goals-mode-map proof-goals-mode-map56,1970 +(define-key proof-goals-mode-map proof-goals-mode-map59,2230 +(defun proof-goals-config-done proof-goals-config-done74,2494 +(defun pg-goals-display pg-goals-display84,2782 +(defun pg-goals-analyse-structure pg-goals-analyse-structure133,4725 +(defun pg-goals-make-top-span pg-goals-make-top-span257,9571 +(defun pg-goals-yank-subterm pg-goals-yank-subterm287,10578 +(defun pg-goals-button-action pg-goals-button-action314,11478 +(defun proof-expand-path proof-expand-path335,12451 +(defun pg-goals-construct-command pg-goals-construct-command344,12695 +(defun pg-goals-get-subterm-help pg-goals-get-subterm-help368,13547 + +generic/pg-metadata.el,266 +(defcustom pg-metadata-default-directory pg-metadata-default-directory23,620 +(defface proof-preparsed-span proof-preparsed-span28,794 +(defun pg-metadata-filename-for pg-metadata-filename-for39,1057 +(defun pg-write-metadata-file pg-write-metadata-file54,1500 + +generic/pg-pgip.el,1094 +(defalias 'pg-pgip-error pg-pgip-error17,536 +(defun pg-pgip-process-packet pg-pgip-process-packet20,585 +(defun pg-pgip-process-cmds pg-pgip-process-cmds28,973 +(defun pg-pgip-post-process pg-pgip-post-process76,2234 +(defun pg-pgip-haspref pg-pgip-haspref112,3182 +(defun pg-pgip-default-for pg-pgip-default-for175,5465 +(defun pg-pgip-subst-for pg-pgip-subst-for186,5777 +(defun pg-pgip-get-type pg-pgip-get-type193,5938 +(defun pg-pgip-pgiptype pg-pgip-pgiptype200,6160 +(defun pg-pgip-interpret-bool pg-pgip-interpret-bool224,7024 +(defun pg-pgip-interpret-int pg-pgip-interpret-int233,7300 +(defun pg-pgip-interpret-string pg-pgip-interpret-string238,7463 +(defun pg-pgip-interpret-choice pg-pgip-interpret-choice241,7513 +(defun pg-pgip-interpret-value pg-pgip-interpret-value261,8208 +(defun pg-pgip-get-attr pg-pgip-get-attr284,8833 +(defun pg-pgip-get-version pg-pgip-get-version291,9046 +(defun pg-prover-interpret-pgip-command pg-prover-interpret-pgip-command299,9284 +(defun pg-issue-pgip pg-issue-pgip316,9706 +(defun pg-pgip-askprefs pg-pgip-askprefs322,9886 + +generic/pg-response.el,898 +(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-regexp60,1857 +(defun proof-multiple-frames-enable proof-multiple-frames-enable64,2022 +(defvar pg-response-erase-flag pg-response-erase-flag109,3850 +(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response112,3965 +(defun pg-response-display pg-response-display142,5115 +(defun pg-response-display-with-face pg-response-display-with-face152,5523 +(defun pg-response-clear-displays pg-response-clear-displays187,6880 +(defvar pg-response-next-error pg-response-next-error204,7410 +(defun proof-next-error proof-next-error208,7532 +(defun proof-trace-buffer-display proof-trace-buffer-display304,10994 +(defun pg-thms-buffer-clear pg-thms-buffer-clear334,11730 + +generic/pg-thymodes.el,219 +(defmacro pg-defthymode pg-defthymode19,466 +(defmacro pg-do-unless-null pg-do-unless-null67,2277 +(defun pg-symval pg-symval72,2364 +(defun pg-modesym pg-modesym78,2520 +(defun pg-modesymval pg-modesymval82,2634 + +generic/pg-user.el,3080 +(defmacro proof-maybe-save-point proof-maybe-save-point18,407 +(defun proof-maybe-follow-locked-end proof-maybe-follow-locked-end26,609 +(defun proof-assert-next-command-interactive proof-assert-next-command-interactive40,974 +(defun proof-process-buffer proof-process-buffer50,1345 +(defun proof-undo-last-successful-command proof-undo-last-successful-command64,1662 +(defun proof-undo-and-delete-last-successful-command proof-undo-and-delete-last-successful-command69,1824 +(defun proof-undo-last-successful-command-1 proof-undo-last-successful-command-191,2796 +(defun proof-retract-buffer proof-retract-buffer107,3361 +(defun proof-retract-current-goal proof-retract-current-goal116,3641 +(defun proof-interrupt-process proof-interrupt-process134,4132 +(defun proof-goto-command-start proof-goto-command-start161,5117 +(defun proof-goto-command-end proof-goto-command-end184,6059 +(defun proof-mouse-goto-point proof-mouse-goto-point209,6839 +(defun proof-mouse-track-insert proof-mouse-track-insert224,7413 +(defvar proof-minibuffer-history proof-minibuffer-history259,8523 +(defun proof-minibuffer-cmd proof-minibuffer-cmd262,8617 +(defun proof-frob-locked-end proof-frob-locked-end310,10423 +(defmacro proof-if-setting-configured proof-if-setting-configured403,13337 +(defmacro proof-define-assistant-command proof-define-assistant-command410,13592 +(defmacro proof-define-assistant-command-witharg proof-define-assistant-command-witharg422,14043 +(defun proof-issue-new-command proof-issue-new-command442,14849 +(defun proof-cd-sync proof-cd-sync481,16280 +(deflocal proof-electric-terminator proof-electric-terminator532,17749 +(defun proof-electric-terminator-enable proof-electric-terminator-enable542,18096 +(defun proof-electric-term-incomment-fn proof-electric-term-incomment-fn553,18583 +(defun proof-process-electric-terminator proof-process-electric-terminator573,19339 +(defun proof-electric-terminator proof-electric-terminator600,20490 +(defun proof-add-completions proof-add-completions622,21128 +(defun proof-script-complete proof-script-complete642,21885 +(defun pg-insert-last-output-as-comment pg-insert-last-output-as-comment670,22476 +(defun pg-copy-span-contents pg-copy-span-contents701,23704 +(defun pg-numth-span-higher-or-lower pg-numth-span-higher-or-lower718,24257 +(defun pg-control-span-of pg-control-span-of744,25008 +(defun pg-move-span-contents pg-move-span-contents750,25212 +(defun pg-fixup-children-span pg-fixup-children-span804,27436 +(defun pg-move-region-down pg-move-region-down811,27644 +(defun pg-move-region-up pg-move-region-up820,27938 +(defun proof-forward-command proof-forward-command826,28145 +(defun proof-backward-command proof-backward-command847,28867 +(defvar pg-span-context-menu-keymappg-span-context-menu-keymap863,29111 +(defun pg-span-for-event pg-span-for-event879,29538 +(defun pg-span-context-menu pg-span-context-menu890,29922 +(defun pg-toggle-visibility pg-toggle-visibility905,30382 +(defun pg-create-in-span-context-menu pg-create-in-span-context-menu915,30704 + +generic/pg-xhtml.el,573 +(defvar pg-xhtml-dir pg-xhtml-dir17,415 +(defun pg-xhtml-dir pg-xhtml-dir20,481 +(defvar pg-xhtml-file-count pg-xhtml-file-count32,848 +(defun pg-xhtml-next-file pg-xhtml-next-file35,920 +(defvar pg-xhtml-header pg-xhtml-header47,1151 +(defmacro pg-xhtml-write-tempfile pg-xhtml-write-tempfile53,1392 +(defun pg-xhtml-cleanup-tempdir pg-xhtml-cleanup-tempdir71,1982 +(defvar pg-mozilla-prog-name pg-mozilla-prog-name75,2113 +(defun pg-xhtml-display-file-mozilla pg-xhtml-display-file-mozilla79,2221 +(defalias 'pg-xhtml-display-file pg-xhtml-display-file84,2394 + +generic/pg-xml.el,1487 +(defconst pg-xml-name pg-xml-name32,840 +(defconst pg-xml-space pg-xml-space33,893 +(defconst pg-xml-ref pg-xml-ref34,928 +(defconst pg-xml-start-open-elt-regexp pg-xml-start-open-elt-regexp36,1004 +(defconst pg-xml-end-open-elt-regexp pg-xml-end-open-elt-regexp38,1098 +(defconst pg-xml-close-elt-regexp pg-xml-close-elt-regexp40,1177 +(defconst pg-xml-attribute-regexp pg-xml-attribute-regexp42,1268 +(defconst pg-xml-attribute-val-regexp pg-xml-attribute-val-regexp44,1356 +(defconst pg-xml-comment-start-regexp pg-xml-comment-start-regexp47,1507 +(defconst pg-xml-comment-end-regexp pg-xml-comment-end-regexp48,1553 +(defconst pg-xml-anymarkup-regexp pg-xml-anymarkup-regexp49,1596 +(defconst pg-xml-special-eltspg-xml-special-elts50,1635 +(defvar xmlparse xmlparse54,1734 +(defun pg-xml-add-text pg-xml-add-text57,1789 +(defun pg-xml-parse-buffer pg-xml-parse-buffer64,2001 +(defun pg-xml-parse-string pg-xml-parse-string171,5971 +(defconst pg-xml-header pg-xml-header188,6460 +(defvar pg-xml-doc pg-xml-doc191,6536 +(defvar pg-xml-openelts pg-xml-openelts194,6626 +(defvar pg-xml-indentp pg-xml-indentp197,6682 +(defun pg-xml-encode-entities pg-xml-encode-entities200,6755 +(defun pg-xml-begin-write pg-xml-begin-write210,7244 +(defun pg-xml-indent pg-xml-indent215,7436 +(defun pg-xml-openelt pg-xml-openelt221,7575 +(defun pg-xml-closeelt pg-xml-closeelt240,8121 +(defun pg-xml-writetext pg-xml-writetext252,8391 +(defun pg-xml-doc pg-xml-doc255,8492 + +generic/_pkg.el,0 + +generic/proof-autoloads.el,0 + +generic/proof-compat.el,707 +(defun pg-custom-undeclare-variable pg-custom-undeclare-variable28,994 +(defun subst-char-in-string subst-char-in-string99,3134 +(defun replace-regexp-in-string replace-regexp-in-string112,3625 +(defconst menuvisiblep menuvisiblep174,6338 +(defun warn warn218,7684 +(defun redraw-modeline redraw-modeline225,7939 +(defun replace-in-string replace-in-string240,8506 +(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate289,10024 +(defvar read-shell-command-mapread-shell-command-map322,11331 +(defun read-shell-command read-shell-command340,12033 +(defun remassq remassq352,12514 +(defun remassoc remassoc364,12903 +(defun process-live-p process-live-p398,13973 + +generic/proof-config.el,15774 +(defgroup proof-user-options proof-user-options84,3160 +(defcustom proof-electric-terminator-enable proof-electric-terminator-enable89,3274 +(defcustom proof-toolbar-enable proof-toolbar-enable101,3808 +(defpgcustom x-symbol-enable x-symbol-enable108,4046 +(defpgcustom mmm-enable mmm-enable117,4396 +(defcustom proof-output-fontify-enable proof-output-fontify-enable126,4750 +(defcustom proof-trace-output-fontify-enable proof-trace-output-fontify-enable135,5072 +(defcustom proof-strict-state-preserving proof-strict-state-preserving145,5576 +(defcustom proof-strict-read-only proof-strict-read-only158,6185 +(defcustom proof-three-window-mode proof-three-window-mode168,6535 +(defcustom proof-multiple-frames-enable proof-multiple-frames-enable189,7347 +(defcustom proof-delete-empty-windows proof-delete-empty-windows198,7683 +(defcustom proof-shrink-windows-tofit proof-shrink-windows-tofit209,8214 +(defcustom proof-toolbar-use-button-enablers proof-toolbar-use-button-enablers216,8486 +(defcustom proof-query-file-save-when-activating-scripting proof-query-file-save-when-activating-scripting250,9784 +(defpgcustom script-indent script-indent266,10507 +(defcustom proof-one-command-per-line proof-one-command-per-line272,10695 +(defcustom proof-prog-name-ask proof-prog-name-ask280,10915 +(defcustom proof-prog-name-guess proof-prog-name-guess286,11076 +(defcustom proof-tidy-responseproof-tidy-response294,11336 +(defcustom proof-show-debug-messages proof-show-debug-messages308,11803 +(defcustom proof-experimental-features proof-experimental-features317,12181 +(defcustom proof-follow-mode proof-follow-mode336,12928 +(defcustom proof-auto-action-when-deactivating-scripting proof-auto-action-when-deactivating-scripting354,13694 +(defcustom proof-script-command-separator proof-script-command-separator377,14645 +(defcustom proof-rsh-command proof-rsh-command385,14938 +(defcustom proof-disappearing-proofs proof-disappearing-proofs401,15475 +(defgroup proof-faces proof-faces428,16119 +(defmacro proof-face-specs proof-face-specs433,16225 +(defface proof-queue-face proof-queue-face448,16671 +(defface proof-locked-faceproof-locked-face456,16944 +(defface proof-declaration-name-faceproof-declaration-name-face464,17202 +(defconst proof-declaration-name-face proof-declaration-name-face476,17595 +(defface proof-tacticals-name-faceproof-tacticals-name-face481,17831 +(defconst proof-tacticals-name-face proof-tacticals-name-face490,18093 +(defface proof-tactics-name-faceproof-tactics-name-face495,18323 +(defconst proof-tactics-name-face proof-tactics-name-face504,18588 +(defface proof-error-face proof-error-face509,18812 +(defface proof-warning-faceproof-warning-face517,19016 +(defface proof-eager-annotation-faceproof-eager-annotation-face526,19273 +(defface proof-debug-message-faceproof-debug-message-face534,19491 +(defface proof-boring-faceproof-boring-face542,19690 +(defface proof-mouse-highlight-faceproof-mouse-highlight-face550,19882 +(defface proof-highlight-dependent-faceproof-highlight-dependent-face558,20078 +(defface proof-highlight-dependency-faceproof-highlight-dependency-face566,20287 +(defgroup prover-config prover-config584,20546 +(defcustom proof-mode-for-shell proof-mode-for-shell618,21665 +(defcustom proof-mode-for-response proof-mode-for-response625,21912 +(defcustom proof-mode-for-goals proof-mode-for-goals632,22195 +(defcustom proof-mode-for-script proof-mode-for-script639,22450 +(defcustom proof-guess-command-line proof-guess-command-line650,22884 +(defcustom proof-assistant-home-page proof-assistant-home-page665,23381 +(defcustom proof-context-command proof-context-command671,23551 +(defcustom proof-info-command proof-info-command676,23685 +(defcustom proof-showproof-command proof-showproof-command683,23957 +(defcustom proof-goal-command proof-goal-command688,24093 +(defcustom proof-save-command proof-save-command696,24391 +(defcustom proof-find-theorems-command proof-find-theorems-command704,24701 +(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default711,25010 +(defpgcustom toolbar-entries toolbar-entries742,26742 +(defcustom proof-assistant-true-value proof-assistant-true-value760,27463 +(defcustom proof-assistant-false-value proof-assistant-false-value766,27653 +(defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn772,27847 +(defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn779,28096 +(defcustom proof-assistant-setting-format proof-assistant-setting-format786,28363 +(defgroup proof-script proof-script808,29058 +(defcustom proof-terminal-char proof-terminal-char813,29188 +(defcustom proof-script-sexp-commands proof-script-sexp-commands823,29592 +(defcustom proof-script-command-end-regexp proof-script-command-end-regexp834,30062 +(defcustom proof-script-command-start-regexp proof-script-command-start-regexp852,30881 +(defcustom proof-script-use-old-parser proof-script-use-old-parser863,31343 +(defcustom proof-script-integral-proofs proof-script-integral-proofs875,31837 +(defcustom proof-script-fly-past-comments proof-script-fly-past-comments890,32493 +(defcustom proof-script-parse-function proof-script-parse-function897,32799 +(defcustom proof-script-comment-start proof-script-comment-start915,33445 +(defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp926,33880 +(defcustom proof-script-comment-end proof-script-comment-end934,34197 +(defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp943,34528 +(defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn951,34839 +(defcustom proof-string-start-regexp proof-string-start-regexp957,35091 +(defcustom proof-string-end-regexp proof-string-end-regexp962,35256 +(defcustom proof-case-fold-search proof-case-fold-search967,35417 +(defcustom proof-save-command-regexp proof-save-command-regexp976,35833 +(defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp981,35944 +(defcustom proof-save-with-hole-result proof-save-with-hole-result993,36396 +(defcustom proof-goal-command-regexp proof-goal-command-regexp1004,36860 +(defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1013,37252 +(defcustom proof-goal-with-hole-result proof-goal-with-hole-result1025,37699 +(defcustom proof-non-undoables-regexp proof-non-undoables-regexp1035,38098 +(defcustom proof-nested-undo-regexp proof-nested-undo-regexp1046,38554 +(defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1062,39266 +(defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1070,39569 +(defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1114,41303 +(defcustom proof-goal-command-p proof-goal-command-p1140,42531 +(defcustom proof-really-save-command-p proof-really-save-command-p1165,43824 +(defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1177,44285 +(defcustom proof-count-undos-fn proof-count-undos-fn1205,45645 +(defconst proof-no-command proof-no-command1240,47246 +(defcustom proof-find-and-forget-fn proof-find-and-forget-fn1245,47450 +(defcustom proof-forget-id-command proof-forget-id-command1262,48161 +(defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1272,48519 +(defcustom proof-kill-goal-command proof-kill-goal-command1284,49000 +(defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1298,49510 +(defcustom proof-nested-goals-history-p proof-nested-goals-history-p1312,50059 +(defcustom proof-state-preserving-p proof-state-preserving-p1321,50397 +(defcustom proof-activate-scripting-hook proof-activate-scripting-hook1331,50867 +(defcustom proof-indent proof-indent1354,51680 +(defcustom proof-indent-hang proof-indent-hang1359,51787 +(defcustom proof-indent-enclose-offset proof-indent-enclose-offset1364,51913 +(defcustom proof-indent-open-offset proof-indent-open-offset1369,52055 +(defcustom proof-indent-close-offset proof-indent-close-offset1374,52192 +(defcustom proof-indent-any-regexp proof-indent-any-regexp1379,52330 +(defcustom proof-indent-inner-regexp proof-indent-inner-regexp1384,52490 +(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1389,52644 +(defcustom proof-indent-open-regexp proof-indent-open-regexp1394,52798 +(defcustom proof-indent-close-regexp proof-indent-close-regexp1399,52950 +(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1405,53104 +(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1417,53477 +(defgroup proof-shell proof-shell1443,54266 +(defcustom proof-prog-name proof-prog-name1453,54437 +(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1462,54792 +(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1471,55189 +(defcustom proof-shell-init-cmd proof-shell-init-cmd1485,55748 +(defcustom proof-shell-restart-cmd proof-shell-restart-cmd1496,56218 +(defcustom proof-shell-quit-cmd proof-shell-quit-cmd1501,56373 +(defcustom proof-shell-quit-timeout proof-shell-quit-timeout1506,56540 +(defcustom proof-shell-cd-cmd proof-shell-cd-cmd1516,56988 +(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1533,57655 +(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1542,58031 +(defcustom proof-shell-silent-threshold proof-shell-silent-threshold1551,58368 +(defcustom proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1559,58702 +(defcustom proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1580,59625 +(defcustom proof-auto-multiple-files proof-auto-multiple-files1603,60666 +(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1629,61491 +(defcustom proof-shell-wakeup-char proof-shell-wakeup-char1638,61829 +(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1644,62060 +(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1660,62700 +(defcustom proof-shell-error-regexp proof-shell-error-regexp1665,62835 +(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1685,63629 +(defcustom pg-next-error-regexp pg-next-error-regexp1699,64172 +(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1714,64782 +(defcustom pg-next-error-extract-filename pg-next-error-extract-filename1738,65820 +(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1745,66063 +(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1759,66655 +(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1772,67163 +(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1779,67462 +(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1786,67755 +(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1794,68122 +(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1800,68364 +(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1818,69102 +(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1829,69529 +(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1845,70205 +(defcustom proof-shell-process-file proof-shell-process-file1855,70617 +(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1877,71569 +(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1886,71905 +(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1898,72450 +(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp1906,72774 +(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd1939,74246 +(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd1948,74576 +(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd1957,74932 +(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp1964,75192 +(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split1980,75852 +(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd1989,76277 +(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp1996,76546 +(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2012,77090 +(defcustom proof-shell-filename-escapes proof-shell-filename-escapes2024,77475 +(defcustom proof-shell-process-connection-type proof-shell-process-connection-type2041,78155 +(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2061,79033 +(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2073,79522 +(defcustom proof-shell-insert-hook proof-shell-insert-hook2081,79890 +(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2119,81731 +(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2135,82203 +(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2141,82418 +(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2149,82784 +(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2159,83154 +(defcustom proof-state-change-hook proof-state-change-hook2178,84019 +(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2189,84401 +(defgroup proof-goals proof-goals2203,84758 +(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2208,84879 +(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2216,85191 +(defcustom pg-goals-change-goal pg-goals-change-goal2225,85495 +(defcustom pbp-goal-command pbp-goal-command2230,85610 +(defcustom pbp-hyp-command pbp-hyp-command2235,85766 +(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2240,85928 +(defcustom pg-goals-error-regexp pg-goals-error-regexp2247,86164 +(defcustom proof-shell-result-start proof-shell-result-start2252,86324 +(defcustom proof-shell-result-end proof-shell-result-end2258,86558 +(defcustom pg-subterm-start-char pg-subterm-start-char2264,86771 +(defcustom pg-subterm-sep-char pg-subterm-sep-char2278,87353 +(defcustom pg-subterm-end-char pg-subterm-end-char2284,87532 +(defcustom pg-topterm-char pg-topterm-char2290,87689 +(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2307,88295 +(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2321,88974 +(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2333,89552 +(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2341,89912 +(defgroup proof-x-symbol proof-x-symbol2353,90166 +(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2358,90294 +(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2371,90923 +(defcustom proof-xsym-activate-command proof-xsym-activate-command2379,91300 +(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2386,91536 +(defpgcustom x-symbol-language x-symbol-language2393,91778 +(defpgcustom favourites favourites2408,92225 +(defpgcustom menu-entries menu-entries2413,92415 +(defpgcustom help-menu-entries help-menu-entries2420,92652 +(defpgcustom keymap keymap2427,92915 +(defpgcustom completion-table completion-table2432,93086 +(defpgcustom tags-program tags-program2442,93449 +(defcustom proof-general-name proof-general-name2454,93622 +(defcustom proof-general-home-pageproof-general-home-page2459,93779 +(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2465,93933 +(defcustom proof-universal-keysproof-universal-keys2473,94209 + +generic/proof-depends.el,1325 +(defvar proof-thm-names-of-files proof-thm-names-of-files19,532 +(defvar proof-def-names-of-files proof-def-names-of-files25,816 +(defun proof-depends-module-name-for-buffer proof-depends-module-name-for-buffer34,1120 +(defun proof-depends-module-of proof-depends-module-of44,1562 +(defun proof-depends-names-in-same-file proof-depends-names-in-same-file52,1856 +(defun proof-depends-process-dependencies proof-depends-process-dependencies71,2476 +(defun proof-dependency-in-span-context-menu proof-dependency-in-span-context-menu124,4218 +(defun proof-dep-alldeps-menu proof-dep-alldeps-menu147,5121 +(defun proof-dep-make-alldeps-menu proof-dep-make-alldeps-menu153,5348 +(defun proof-dep-split-deps proof-dep-split-deps171,5844 +(defun proof-dep-make-submenu proof-dep-make-submenu192,6543 +(defun proof-make-highlight-depts-menu proof-make-highlight-depts-menu202,6896 +(defun proof-goto-dependency proof-goto-dependency212,7200 +(defun proof-show-dependency proof-show-dependency218,7423 +(defconst pg-dep-span-priority pg-dep-span-priority225,7713 +(defconst pg-ordinary-span-priority pg-ordinary-span-priority226,7749 +(defun proof-highlight-depcs proof-highlight-depcs228,7791 +(defun proof-highlight-depts proof-highlight-depts238,8221 +(defun proof-dep-unhighlight proof-dep-unhighlight249,8695 + +generic/proof-easy-config.el,315 +(defvar proof-easy-config-derived-modes-tableproof-easy-config-derived-modes-table15,484 +(defun proof-easy-config-define-derived-modes proof-easy-config-define-derived-modes22,888 +(defun proof-easy-config-check-setup proof-easy-config-check-setup57,2391 +(defmacro proof-easy-config proof-easy-config74,3051 + +generic/proof.el,809 +(deflocal proof-buffer-type proof-buffer-type35,900 +(defvar proof-shell-busy proof-shell-busy38,1014 +(defvar proof-included-files-list proof-included-files-list43,1171 +(defvar proof-script-buffer proof-script-buffer66,2186 +(defvar proof-previous-script-buffer proof-previous-script-buffer70,2326 +(defvar proof-shell-buffer proof-shell-buffer75,2580 +(defvar proof-goals-buffer proof-goals-buffer78,2666 +(defvar proof-response-buffer proof-response-buffer81,2721 +(defvar proof-trace-buffer proof-trace-buffer84,2782 +(defvar proof-thms-buffer proof-thms-buffer88,2936 +(defvar proof-shell-error-or-interrupt-seen proof-shell-error-or-interrupt-seen92,3091 +(defvar proof-shell-proof-completed proof-shell-proof-completed97,3316 +(defvar proof-terminal-string proof-terminal-string109,3861 + +generic/proof-indent.el,344 +(defun proof-indent-indent proof-indent-indent13,337 +(defun proof-indent-offset proof-indent-offset22,603 +(defun proof-indent-inner-p proof-indent-inner-p39,1203 +(defun proof-indent-goto-prev proof-indent-goto-prev48,1510 +(defun proof-indent-calculate proof-indent-calculate55,1843 +(defun proof-indent-line proof-indent-line74,2559 + +generic/proof-menu.el,4154 +(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-keys69,2324 +(define-key map map72,2472 +(define-key map map73,2524 +(define-key map map74,2575 +(define-key map map75,2628 +(define-key map map76,2682 +(define-key map map77,2744 +(define-key map map78,2804 +(define-key map map79,2866 +(define-key map map81,2987 +(define-key map map82,3051 +(define-key map map83,3106 +(define-key map map84,3177 +(define-key map map85,3259 +(define-key map map86,3313 +(define-key map map87,3378 +(define-key map map88,3452 +(define-key map map89,3507 +(define-key map map91,3645 +(define-key map map92,3711 +(define-key map map94,3861 +(define-key map map95,3931 +(define-key map map96,3997 +(define-key map map98,4112 +(define-key map map99,4175 +(define-key map map101,4260 +(define-key map map108,4586 +(define-key map map109,4645 +(defun proof-menu-define-main proof-menu-define-main129,5235 +(defun proof-menu-define-specific proof-menu-define-specific139,5436 +(defun proof-assistant-menu-update proof-assistant-menu-update174,6443 +(defvar proof-help-menuproof-help-menu188,6874 +(defvar proof-show-hide-menuproof-show-hide-menu196,7152 +(defvar proof-buffer-menuproof-buffer-menu205,7465 +(defvar proof-quick-opts-menuproof-quick-opts-menu257,9363 +(defun proof-quick-opts-vars proof-quick-opts-vars343,12701 +(defun proof-quick-opts-changed-from-defaults-p proof-quick-opts-changed-from-defaults-p363,13275 +(defun proof-quick-opts-changed-from-saved-p proof-quick-opts-changed-from-saved-p367,13380 +(defun proof-quick-opts-save proof-quick-opts-save378,13732 +(defun proof-quick-opts-reset proof-quick-opts-reset383,13900 +(defconst proof-config-menuproof-config-menu395,14168 +(defconst proof-advanced-menuproof-advanced-menu402,14347 +(defvar proof-menu proof-menu419,14909 +(defvar proof-main-menuproof-main-menu428,15193 +(defvar proof-aux-menuproof-aux-menu438,15419 +(defvar proof-menu-favourites proof-menu-favourites454,15741 +(defun proof-menu-define-favourites-menu proof-menu-define-favourites-menu457,15848 +(defmacro proof-defshortcut proof-defshortcut478,16519 +(defmacro proof-definvisible proof-definvisible492,17056 +(defun proof-def-favourite proof-def-favourite505,17603 +(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history528,18578 +(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history531,18663 +(defun proof-save-favourites proof-save-favourites534,18749 +(defun proof-del-favourite proof-del-favourite539,18897 +(defun proof-read-favourite proof-read-favourite556,19458 +(defun proof-add-favourite proof-add-favourite581,20261 +(defvar proof-assistant-settings proof-assistant-settings608,21312 +(defvar proof-menu-settings proof-menu-settings615,21675 +(defun proof-menu-define-settings-menu proof-menu-define-settings-menu618,21749 +(defun proof-menu-entry-name proof-menu-entry-name636,22393 +(defun proof-menu-entry-for-setting proof-menu-entry-for-setting641,22552 +(defun proof-settings-vars proof-settings-vars659,23042 +(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p664,23219 +(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p668,23325 +(defun proof-settings-save proof-settings-save672,23428 +(defun proof-settings-reset proof-settings-reset677,23595 +(defun proof-defpacustom-fn proof-defpacustom-fn685,23841 +(defmacro defpacustom defpacustom745,26033 +(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs756,26673 +(defun proof-assistant-settings-cmd proof-assistant-settings-cmd776,27523 +(defun proof-assistant-format proof-assistant-format802,28660 +(defvar proof-assistant-format-table proof-assistant-format-table819,29402 +(defun proof-assistant-format-bool proof-assistant-format-bool827,29771 +(defun proof-assistant-format-int proof-assistant-format-int830,29884 +(defun proof-assistant-format-string proof-assistant-format-string833,29976 + +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,7883 +(defvar proof-last-theorem-dependencies proof-last-theorem-dependencies37,1030 +(defvar proof-nesting-depth proof-nesting-depth41,1192 +(defvar proof-element-counters proof-element-counters48,1425 +(deflocal proof-active-buffer-fake-minor-mode proof-active-buffer-fake-minor-mode54,1565 +(deflocal proof-script-buffer-file-name proof-script-buffer-file-name57,1691 +(defun proof-next-element-count proof-next-element-count71,2215 +(defun proof-element-id proof-element-id80,2544 +(defun proof-next-element-id proof-next-element-id84,2713 +(deflocal proof-script-last-entity proof-script-last-entity98,3030 +(defun proof-script-find-next-entity proof-script-find-next-entity105,3311 +(deflocal proof-locked-span proof-locked-span181,6057 +(deflocal proof-queue-span proof-queue-span188,6323 +(defun proof-span-read-only proof-span-read-only200,6837 +(defun proof-strict-read-only proof-strict-read-only207,7094 +(defsubst proof-set-queue-endpoints proof-set-queue-endpoints219,7721 +(defsubst proof-set-locked-endpoints proof-set-locked-endpoints223,7862 +(defsubst proof-detach-queue proof-detach-queue227,8006 +(defsubst proof-detach-locked proof-detach-locked231,8138 +(defsubst proof-set-queue-start proof-set-queue-start235,8274 +(defsubst proof-set-locked-end proof-set-locked-end239,8400 +(defsubst proof-set-queue-end proof-set-queue-end254,8950 +(defun proof-init-segmentation proof-init-segmentation264,9206 +(defun proof-restart-buffers proof-restart-buffers296,10578 +(defun proof-script-buffers-with-spans proof-script-buffers-with-spans318,11499 +(defun proof-script-remove-all-spans-and-deactivate proof-script-remove-all-spans-and-deactivate328,11856 +(defun proof-script-clear-queue-spans proof-script-clear-queue-spans332,12044 +(defun proof-unprocessed-begin proof-unprocessed-begin350,12585 +(defun proof-script-end proof-script-end358,12841 +(defun proof-queue-or-locked-end proof-queue-or-locked-end367,13142 +(defun proof-locked-end proof-locked-end381,13806 +(defun proof-locked-region-full-p proof-locked-region-full-p397,14178 +(defun proof-locked-region-empty-p proof-locked-region-empty-p405,14435 +(defun proof-only-whitespace-to-locked-region-p proof-only-whitespace-to-locked-region-p409,14585 +(defun proof-in-locked-region-p proof-in-locked-region-p422,15221 +(defun proof-goto-end-of-locked proof-goto-end-of-locked434,15484 +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window445,15980 +(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible461,16753 +(defvar pg-idioms pg-idioms480,17403 +(defvar pg-visibility-specs pg-visibility-specs483,17499 +(deflocal pg-script-portions pg-script-portions488,17707 +(defun pg-clear-script-portions pg-clear-script-portions491,17829 +(defun pg-add-script-element pg-add-script-element509,18495 +(defun pg-remove-script-element pg-remove-script-element512,18571 +(defsubst pg-visname pg-visname520,18849 +(defun pg-add-element pg-add-element524,18994 +(defun pg-open-invisible-span pg-open-invisible-span558,20627 +(defun pg-remove-element pg-remove-element569,20991 +(defun pg-make-element-invisible pg-make-element-invisible576,21261 +(defun pg-make-element-visible pg-make-element-visible582,21518 +(defun pg-toggle-element-visibility pg-toggle-element-visibility587,21697 +(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs595,22028 +(defun pg-show-all-portions pg-show-all-portions602,22299 +(defun pg-show-all-proofs pg-show-all-proofs620,22973 +(defun pg-hide-all-proofs pg-hide-all-proofs625,23101 +(defun pg-add-proof-element pg-add-proof-element630,23232 +(defun pg-span-name pg-span-name644,23853 +(defun pg-set-span-helphighlights pg-set-span-helphighlights663,24500 +(defun proof-complete-buffer-atomic proof-complete-buffer-atomic679,25038 +(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file744,27769 +(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted795,29902 +(defun proof-auto-retract-dependencies proof-auto-retract-dependencies802,30135 +(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name856,32666 +(defun proof-protected-process-or-retract proof-protected-process-or-retract898,34280 +(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto926,35471 +(defun proof-deactivate-scripting proof-deactivate-scripting935,35830 +(defun proof-activate-scripting proof-activate-scripting1069,41130 +(defun proof-toggle-active-scripting proof-toggle-active-scripting1198,46894 +(defun proof-done-advancing proof-done-advancing1239,48258 +(defun proof-done-advancing-comment proof-done-advancing-comment1308,51020 +(defun proof-done-advancing-save proof-done-advancing-save1324,51658 +(defun proof-make-goalsave proof-make-goalsave1417,55280 +(defun proof-get-name-from-goal proof-get-name-from-goal1432,56025 +(defun proof-done-advancing-autosave proof-done-advancing-autosave1451,57050 +(defun proof-done-advancing-other proof-done-advancing-other1514,59493 +(defun proof-segment-up-to-parser proof-segment-up-to-parser1542,60473 +(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1605,62557 +(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1614,62973 +(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1639,63865 +(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1702,66574 +(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1726,67506 +(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1778,69698 +(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1839,72068 +(defun proof-semis-to-vanillas proof-semis-to-vanillas1910,74720 +(defun proof-script-new-command-advance proof-script-new-command-advance1949,76048 +(defun proof-script-next-command-advance proof-script-next-command-advance1991,77785 +(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2003,78228 +(defun proof-assert-until-point proof-assert-until-point2029,79350 +(defun proof-assert-next-commandproof-assert-next-command2082,81786 +(defun proof-goto-point proof-goto-point2130,84052 +(defun proof-insert-pbp-command proof-insert-pbp-command2147,84578 +(defun proof-done-retracting proof-done-retracting2179,85652 +(defun proof-setup-retract-action proof-setup-retract-action2206,86764 +(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2216,87247 +(defun proof-retract-target proof-retract-target2239,88066 +(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2323,91687 +(defun proof-retract-until-point proof-retract-until-point2331,92072 +(define-derived-mode proof-mode proof-mode2366,93227 +(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2399,94521 +(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2423,95525 +(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2433,96019 +(defun proof-config-done-related proof-config-done-related2477,97840 +(defun proof-generic-goal-command-p proof-generic-goal-command-p2539,100118 +(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2543,100291 +(defun proof-generic-count-undos proof-generic-count-undos2552,100806 +(defun proof-generic-find-and-forget proof-generic-find-and-forget2581,101837 +(defconst proof-script-important-settingsproof-script-important-settings2626,103499 +(defun proof-config-done proof-config-done2639,103982 +(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2735,107546 +(defun proof-setup-imenu proof-setup-imenu2779,109399 +(defun proof-setup-func-menu proof-setup-func-menu2793,109861 + +generic/proof-shell.el,4413 +(defvar proof-marker proof-marker52,1495 +(defvar proof-action-list proof-action-list55,1592 +(defvar proof-shell-silent proof-shell-silent63,1768 +(defvar proof-shell-last-prompt proof-shell-last-prompt77,2251 +(defvar proof-shell-last-output proof-shell-last-output82,2475 +(defvar proof-shell-last-output-kind proof-shell-last-output-kind86,2636 +(defvar proof-shell-delayed-output proof-shell-delayed-output107,3458 +(defvar proof-shell-delayed-output-kind proof-shell-delayed-output-kind110,3579 +(defun proof-shell-ready-prover proof-shell-ready-prover146,4614 +(defun proof-shell-live-buffer proof-shell-live-buffer160,5154 +(defun proof-shell-available-p proof-shell-available-p167,5389 +(defun proof-grab-lock proof-grab-lock173,5612 +(defun proof-release-lock proof-release-lock183,6065 +(defun proof-shell-start proof-shell-start196,6418 +(defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator349,12168 +(defvar proof-shell-kill-function-hooks proof-shell-kill-function-hooks382,13077 +(defun proof-shell-kill-function proof-shell-kill-function385,13175 +(defun proof-shell-clear-state proof-shell-clear-state468,16664 +(defun proof-shell-exit proof-shell-exit483,17107 +(defun proof-shell-bail-out proof-shell-bail-out495,17552 +(defun proof-shell-restart proof-shell-restart504,18029 +(defvar proof-shell-no-response-display proof-shell-no-response-display546,19413 +(defvar proof-shell-urgent-message-marker proof-shell-urgent-message-marker549,19517 +(defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner552,19638 +(defun proof-shell-handle-output proof-shell-handle-output556,19765 +(defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output630,23102 +(defvar proof-shell-ignore-errors proof-shell-ignore-errors665,24496 +(defun proof-shell-handle-error proof-shell-handle-error671,24698 +(defun proof-shell-handle-interrupt proof-shell-handle-interrupt687,25438 +(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action701,26054 +(defun proof-goals-pos proof-goals-pos719,26880 +(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal724,27085 +(defsubst proof-shell-string-match-safe proof-shell-string-match-safe736,27620 +(defun proof-shell-process-output proof-shell-process-output741,27788 +(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge852,32428 +(defun proof-shell-insert proof-shell-insert861,32737 +(defun proof-shell-command-queue-item proof-shell-command-queue-item929,35271 +(defun proof-shell-set-silent proof-shell-set-silent934,35428 +(defun proof-shell-start-silent-item proof-shell-start-silent-item940,35647 +(defun proof-shell-clear-silent proof-shell-clear-silent946,35839 +(defun proof-shell-stop-silent-item proof-shell-stop-silent-item952,36061 +(defun proof-shell-should-be-silent proof-shell-should-be-silent959,36333 +(defun proof-append-alist proof-append-alist972,36889 +(defun proof-start-queue proof-start-queue1028,39016 +(defun proof-extend-queue proof-extend-queue1039,39365 +(defun proof-shell-exec-loop proof-shell-exec-loop1050,39746 +(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1109,42092 +(defun proof-shell-message proof-shell-message1147,43796 +(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1153,44012 +(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1349,52248 +(defun proof-shell-filter proof-shell-filter1418,55304 +(defun proof-shell-filter-process-output proof-shell-filter-process-output1571,61641 +(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1614,63236 +(defun proof-shell-show-annotations proof-shell-show-annotations1630,63771 +(defun proof-shell-wait proof-shell-wait1651,64268 +(defun proof-done-invisible proof-done-invisible1661,64679 +(defun proof-shell-invisible-command proof-shell-invisible-command1704,66402 +(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1729,67473 +(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1746,68154 +(define-derived-mode proof-shell-mode proof-shell-mode1766,68658 +(defconst proof-shell-important-settingsproof-shell-important-settings1836,71261 +(defun proof-shell-config-done proof-shell-config-done1841,71361 + +generic/proof-site.el,1154 +(defgroup proof-general proof-general20,586 +(defgroup proof-general-internals proof-general-internals33,1002 +(defun proof-home-directory-fn proof-home-directory-fn42,1195 +(defcustom proof-home-directoryproof-home-directory53,1565 +(defcustom proof-images-directoryproof-images-directory62,1931 +(defcustom proof-info-directoryproof-info-directory68,2132 +(defcustom proof-assistant-tableproof-assistant-table97,3381 +(defun proof-string-to-list proof-string-to-list155,5278 +(defcustom proof-assistants proof-assistants171,5769 +(defun proof-ready-for-assistant proof-ready-for-assistant219,7594 +(defconst proof-general-version proof-general-version334,11887 +(defcustom proof-assistant-cusgrp proof-assistant-cusgrp349,12450 +(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp357,12753 +(defcustom proof-assistant proof-assistant365,13065 +(defcustom proof-assistant-symbol proof-assistant-symbol373,13334 +(defvar proof-running-on-XEmacs proof-running-on-XEmacs390,13882 +(defvar proof-running-on-Emacs21 proof-running-on-Emacs21392,14004 +(defvar proof-running-on-win32 proof-running-on-win32396,14251 + +generic/proof-splash.el,898 +(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,1968 +(defconst proof-splash-welcome proof-splash-welcome68,2351 +(defun proof-get-image proof-get-image87,2915 +(defvar proof-splash-timeout-conf proof-splash-timeout-conf138,4699 +(defun proof-splash-centre-spaces proof-splash-centre-spaces141,4812 +(defun proof-splash-remove-screen proof-splash-remove-screen169,5981 +(defun proof-splash-remove-buffer proof-splash-remove-buffer190,6698 +(defvar proof-splash-seen proof-splash-seen206,7362 +(defun proof-splash-display-screen proof-splash-display-screen210,7479 +(defun proof-splash-message proof-splash-message284,10605 +(defun proof-splash-timeout-waiter proof-splash-timeout-waiter294,10968 + +generic/proof-syntax.el,1296 +(defun proof-ids-to-regexp proof-ids-to-regexp16,445 +(defun proof-anchor-regexp proof-anchor-regexp20,609 +(defconst proof-no-regexpproof-no-regexp24,711 +(defun proof-regexp-alt proof-regexp-alt29,806 +(defun proof-regexp-region proof-regexp-region38,1092 +(defun proof-re-search-forward-region proof-re-search-forward-region47,1515 +(defun proof-re-search-forward proof-re-search-forward60,2010 +(defun proof-re-search-backward proof-re-search-backward66,2271 +(defun proof-string-match proof-string-match72,2535 +(defun proof-string-match-safe proof-string-match-safe78,2767 +(defun proof-stringfn-match proof-stringfn-match82,2972 +(defun proof-looking-at proof-looking-at89,3232 +(defun proof-looking-at-safe proof-looking-at-safe95,3422 +(defun proof-looking-at-syntactic-context proof-looking-at-syntactic-context99,3562 +(defun proof-replace-string proof-replace-string111,3894 +(defun proof-replace-regexp proof-replace-regexp116,4079 +(defvar proof-id proof-id124,4292 +(defun proof-ids proof-ids130,4512 +(defun proof-zap-commas proof-zap-commas143,5073 +(defun proof-format proof-format161,5636 +(defun proof-format-filename proof-format-filename180,6275 +(defun proof-insert proof-insert229,7753 +(defun proof-splice-separator proof-splice-separator265,8762 + +generic/proof-system.el,0 + +generic/proof-toolbar.el,3887 +(defun proof-toolbar-function proof-toolbar-function57,1912 +(defun proof-toolbar-icon proof-toolbar-icon60,2009 +(defun proof-toolbar-enabler proof-toolbar-enabler63,2110 +(defun proof-toolbar-function-with-enabler proof-toolbar-function-with-enabler66,2218 +(defun proof-toolbar-make-icon proof-toolbar-make-icon73,2391 +(defun proof-toolbar-make-toolbar-item proof-toolbar-make-toolbar-item91,2991 +(defvar proof-toolbar proof-toolbar130,4372 +(deflocal proof-toolbar-itimer proof-toolbar-itimer134,4501 +(defun proof-toolbar-setup proof-toolbar-setup138,4611 +(defun proof-toolbar-build proof-toolbar-build183,6227 +(defalias 'proof-toolbar-enable proof-toolbar-enable254,8658 +(defun proof-toolbar-setup-refresh proof-toolbar-setup-refresh263,8897 +(defun proof-toolbar-disable-refresh proof-toolbar-disable-refresh284,9667 +(deflocal proof-toolbar-refresh-flag proof-toolbar-refresh-flag291,9989 +(defun proof-toolbar-refresh proof-toolbar-refresh297,10260 +(defvar proof-toolbar-enablersproof-toolbar-enablers301,10405 +(defvar proof-toolbar-enablers-last-stateproof-toolbar-enablers-last-state307,10581 +(defun proof-toolbar-really-refresh proof-toolbar-really-refresh311,10672 +(defun proof-toolbar-undo-enable-p proof-toolbar-undo-enable-p364,12502 +(defalias 'proof-toolbar-undo proof-toolbar-undo369,12650 +(defun proof-toolbar-delete-enable-p proof-toolbar-delete-enable-p375,12769 +(defalias 'proof-toolbar-delete proof-toolbar-delete381,12943 +(defun proof-toolbar-lockedend-enable-p proof-toolbar-lockedend-enable-p388,13079 +(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend391,13129 +(defun proof-toolbar-next-enable-p proof-toolbar-next-enable-p400,13217 +(defalias 'proof-toolbar-next proof-toolbar-next404,13324 +(defun proof-toolbar-goto-enable-p proof-toolbar-goto-enable-p411,13418 +(defalias 'proof-toolbar-goto proof-toolbar-goto414,13491 +(defun proof-toolbar-retract-enable-p proof-toolbar-retract-enable-p421,13567 +(defalias 'proof-toolbar-retract proof-toolbar-retract425,13678 +(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p432,13757 +(defalias 'proof-toolbar-use proof-toolbar-use433,13825 +(defun proof-toolbar-restart-enable-p proof-toolbar-restart-enable-p439,13903 +(defalias 'proof-toolbar-restart proof-toolbar-restart444,14064 +(defun proof-toolbar-goal-enable-p proof-toolbar-goal-enable-p450,14142 +(defalias 'proof-toolbar-goal proof-toolbar-goal457,14375 +(defun proof-toolbar-qed-enable-p proof-toolbar-qed-enable-p464,14447 +(defalias 'proof-toolbar-qed proof-toolbar-qed470,14599 +(defun proof-toolbar-state-enable-p proof-toolbar-state-enable-p476,14671 +(defalias 'proof-toolbar-state proof-toolbar-state479,14742 +(defun proof-toolbar-context-enable-p proof-toolbar-context-enable-p485,14811 +(defalias 'proof-toolbar-context proof-toolbar-context488,14884 +(defun proof-toolbar-info-enable-p proof-toolbar-info-enable-p496,15044 +(defalias 'proof-toolbar-info proof-toolbar-info499,15088 +(defun proof-toolbar-command-enable-p proof-toolbar-command-enable-p505,15157 +(defalias 'proof-toolbar-command proof-toolbar-command508,15228 +(defun proof-toolbar-help-enable-p proof-toolbar-help-enable-p514,15308 +(defun proof-toolbar-help proof-toolbar-help517,15353 +(defun proof-toolbar-find-enable-p proof-toolbar-find-enable-p525,15447 +(defalias 'proof-toolbar-find proof-toolbar-find528,15516 +(defun proof-toolbar-visibility-enable-p proof-toolbar-visibility-enable-p534,15614 +(defalias 'proof-toolbar-visibility proof-toolbar-visibility537,15714 +(defun proof-toolbar-interrupt-enable-p proof-toolbar-interrupt-enable-p543,15802 +(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt546,15866 +(defun proof-toolbar-make-menu-item proof-toolbar-make-menu-item555,16055 +(defconst proof-toolbar-scripting-menuproof-toolbar-scripting-menu577,16743 + +generic/proof-utils.el,2953 +(defmacro deflocal deflocal18,464 +(defmacro proof-with-current-buffer-if-exists proof-with-current-buffer-if-exists25,702 +(defmacro proof-with-script-buffer proof-with-script-buffer34,1079 +(defmacro proof-map-buffers proof-map-buffers45,1466 +(defmacro proof-sym proof-sym50,1651 +(defun proof-try-require proof-try-require55,1812 +(defun proof-set-value proof-set-value67,2153 +(defun proof-ass-symv proof-ass-symv127,4330 +(defmacro proof-ass-sym proof-ass-sym132,4517 +(defun proof-defpgcustom-fn proof-defpgcustom-fn136,4656 +(defun undefpgcustom undefpgcustom161,5740 +(defmacro defpgcustom defpgcustom167,5964 +(defmacro proof-ass proof-ass176,6381 +(defun proof-defpgdefault-fn proof-defpgdefault-fn181,6557 +(defmacro defpgdefault defpgdefault195,7016 +(defmacro defpgfun defpgfun206,7378 +(defun proof-file-truename proof-file-truename221,7672 +(defun proof-file-to-buffer proof-file-to-buffer225,7855 +(defun proof-files-to-buffers proof-files-to-buffers236,8184 +(defun proof-buffers-in-mode proof-buffers-in-mode243,8467 +(defun pg-save-from-death pg-save-from-death257,8918 +(defun proof-define-keys proof-define-keys276,9528 +(deflocal proof-font-lock-keywords proof-font-lock-keywords305,10529 +(deflocal proof-font-lock-keywords-case-fold-search proof-font-lock-keywords-case-fold-search311,10792 +(defun proof-font-lock-configure-defaults proof-font-lock-configure-defaults314,10915 +(defun proof-font-lock-clear-font-lock-vars proof-font-lock-clear-font-lock-vars362,13228 +(defun proof-font-lock-set-font-lock-vars proof-font-lock-set-font-lock-vars373,13601 +(defun proof-fontify-region proof-fontify-region380,13814 +(defconst pg-special-char-regexp pg-special-char-regexp434,15780 +(defun pg-remove-specials pg-remove-specials438,15892 +(defun proof-fontify-buffer proof-fontify-buffer452,16317 +(defun proof-warn-if-unset proof-warn-if-unset465,16558 +(defun proof-display-and-keep-buffer proof-display-and-keep-buffer470,16776 +(defun proof-clean-buffer proof-clean-buffer533,19342 +(defun proof-message proof-message545,19820 +(defun proof-warning proof-warning550,20033 +(defun proof-debug proof-debug557,20367 +(defun proof-switch-to-buffer proof-switch-to-buffer569,20830 +(defun proof-resize-window-tofit proof-resize-window-tofit587,21669 +(defun proof-submit-bug-report proof-submit-bug-report656,24209 +(defun proof-deftoggle-fn proof-deftoggle-fn679,24981 +(defmacro proof-deftoggle proof-deftoggle694,25636 +(defun proof-defintset-fn proof-defintset-fn701,26010 +(defmacro proof-defintset proof-defintset715,26665 +(defun proof-defstringset-fn proof-defstringset-fn722,27042 +(defmacro proof-defstringset proof-defstringset735,27669 +(defun pg-custom-save-vars pg-custom-save-vars749,28134 +(defun pg-custom-reset-vars pg-custom-reset-vars767,28860 +(defun proof-locate-executable proof-locate-executable780,29197 +(defconst proof-extra-flsproof-extra-fls810,30484 + +generic/proof-x-symbol.el,960 +(defvar proof-x-symbol-initialized proof-x-symbol-initialized52,2019 +(defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file55,2114 +(defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available61,2296 +(defun proof-x-symbol-initialize proof-x-symbol-initialize81,3041 +(defun proof-x-symbol-enable proof-x-symbol-enable176,6904 +(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers202,8109 +(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers217,8863 +(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region239,9567 +(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input241,9633 +(defun proof-x-symbol-set-language proof-x-symbol-set-language258,10224 +(defun proof-x-symbol-shell-config proof-x-symbol-shell-config263,10395 +(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer305,12320 + +generic/span.el,192 +(defsubst delete-spans delete-spans22,471 +(defsubst span-property-safe span-property-safe26,625 +(defsubst set-span-start set-span-start30,764 +(defsubst set-span-end set-span-end34,896 + +generic/span-extent.el,942 +(defsubst make-span make-span16,549 +(defsubst detach-span detach-span20,671 +(defsubst set-span-endpoints set-span-endpoints24,758 +(defsubst set-span-property set-span-property28,891 +(defsubst span-read-only span-read-only32,1018 +(defsubst span-read-write span-read-write36,1122 +(defun span-give-warning span-give-warning40,1229 +(defun span-write-warning span-write-warning44,1327 +(defsubst span-property span-property49,1527 +(defsubst delete-span delete-span53,1642 +(defsubst mapcar-spans mapcar-spans59,1813 +(defsubst span-at span-at63,2019 +(defsubst span-at-before span-at-before67,2136 +(defsubst span-start span-start72,2333 +(defsubst span-end span-end76,2462 +(defsubst prev-span prev-span80,2585 +(defsubst next-span next-span84,2731 +(defsubst span-live-p span-live-p88,2873 +(defun span-raise span-raise96,3145 +(defalias 'span-object span-object100,3244 +(defalias 'span-string span-string101,3283 + +generic/span-overlay.el,1699 +(defvar before-list before-list20,763 +(defun foldr foldr27,898 +(defun foldl foldl39,1231 +(defsubst span-start span-start51,1548 +(defsubst span-end span-end55,1640 +(defun set-span-property set-span-property59,1726 +(defsubst span-property span-property63,1842 +(defun span-read-only-hook span-read-only-hook67,1953 +(defun span-read-only span-read-only71,2085 +(defun span-read-write span-read-write86,2863 +(defun span-give-warning span-give-warning92,3082 +(defun span-write-warning span-write-warning96,3190 +(defun int-nil-lt int-nil-lt101,3413 +(defun span-lt span-lt110,3616 +(defun span-traverse span-traverse115,3775 +(defun add-span add-span131,4222 +(defun make-span make-span145,4624 +(defun remove-span remove-span149,4755 +(defun spans-at-point spans-at-point162,5208 +(defun append-unique append-unique176,5688 +(defun spans-at-region spans-at-region179,5775 +(defun spans-at-point-prop spans-at-point-prop186,5997 +(defun spans-at-region-prop spans-at-region-prop194,6247 +(defun span-at span-at206,6594 +(defsubst detach-span detach-span212,6808 +(defsubst delete-span delete-span218,6935 +(defsubst set-span-endpoints set-span-endpoints226,7178 +(defsubst mapcar-spans mapcar-spans233,7394 +(defun map-spans-aux map-spans-aux237,7589 +(defsubst map-spans map-spans241,7704 +(defun find-span-aux find-span-aux244,7762 +(defun find-span find-span249,7888 +(defun span-at-before span-at-before252,7953 +(defun prev-span prev-span265,8395 +(defun next-span next-span274,8677 +(defsubst span-live-p span-live-p299,9668 +(defun span-raise span-raise305,9834 +(defalias 'span-object span-object311,10065 +(defun span-string span-string313,10106 + +generic/texi-docstring-magic.el,958 +(defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2988 +(defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep90,3153 +(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table100,3458 +(defun texi-docstring-magic-untabify texi-docstring-magic-untabify190,7177 +(defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7492 +(defun texi-docstring-magic-texi texi-docstring-magic-texi239,8779 +(defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9219 +(defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9854 +(defconst texi-docstring-magic-commenttexi-docstring-magic-comment323,11705 +(defun texi-docstring-magic texi-docstring-magic329,11859 +(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point353,12571 +(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic368,13094 + +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 + +coq/coq.el,4334 +(defcustom coq-prog-name coq-prog-name12,314 +(defcustom coq-default-undo-limit coq-default-undo-limit19,473 +(defconst coq-shell-init-cmd coq-shell-init-cmd24,601 +(defconst coq-shell-restart-cmd coq-shell-restart-cmd36,1002 +(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern40,1084 +(defvar coq-shell-cd coq-shell-cd44,1259 +(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp47,1359 +(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp50,1485 +(defvar coq-goal-regexpcoq-goal-regexp53,1616 +(defun coq-library-directory coq-library-directory62,1805 +(defcustom coq-tags coq-tags69,1985 +(defconst coq-interrupt-regexp coq-interrupt-regexp74,2134 +(defcustom coq-www-home-page coq-www-home-page79,2254 +(defpgdefault menu-entriesmenu-entries86,2389 +(defvar coq-outline-regexpcoq-outline-regexp103,2783 +(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp108,3192 +(defvar coq-shell-outline-regexp coq-shell-outline-regexp110,3251 +(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp111,3301 +(defconst coq-kill-goal-command coq-kill-goal-command113,3364 +(defconst coq-forget-id-command coq-forget-id-command114,3407 +(defconst coq-back-n-command coq-back-n-command115,3453 +(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp119,3515 +(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp121,3612 +(defconst coq-tactics-regexpcoq-tactics-regexp123,3713 +(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp125,3779 +(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp127,3886 +(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp129,3998 +(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp131,4089 +(defvar coq-keywords-sectioncoq-keywords-section134,4188 +(defvar coq-section-regexp coq-section-regexp139,4333 +(defun coq-set-undo-limit coq-set-undo-limit172,5400 +(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp183,5743 +(defun coq-count-match coq-count-match216,7187 +(defun coq-goal-command-p coq-goal-command-p228,7607 +(defun coq-proof-mode-p coq-proof-mode-p255,8943 +(defun coq-is-comment-p coq-is-comment-p270,9449 +(defun coq-is-goalsave-p coq-is-goalsave-p271,9522 +(defun coq-is-module-equal-p coq-is-module-equal-p272,9597 +(defun coq-is-def-p coq-is-def-p275,9793 +(defun coq-is-decl-defn-p coq-is-decl-defn-p277,9901 +(defun coq-state-preserving-command-p coq-state-preserving-command-p282,10068 +(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p285,10202 +(defun coq-state-changing-command-p coq-state-changing-command-p288,10334 +(defun coq-section-or-module-start-p coq-section-or-module-start-p294,10642 +(defun coq-find-and-forget coq-find-and-forget302,10895 +(defvar coq-current-goal coq-current-goal394,15449 +(defun coq-goal-hyp coq-goal-hyp397,15514 +(defun coq-state-preserving-p coq-state-preserving-p410,15944 +(defun coq-SearchIsos coq-SearchIsos417,16261 +(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string431,16695 +(defun coq-Print coq-Print441,16989 +(defun coq-Check coq-Check450,17247 +(defun coq-Show coq-Show459,17489 +(defun coq-PrintHint coq-PrintHint468,17763 +(defun coq-end-Section coq-end-Section474,17906 +(defun coq-Compile coq-Compile492,18490 +(define-key coq-keymap coq-keymap503,18863 +(define-key coq-keymap coq-keymap504,18919 +(define-key coq-keymap coq-keymap505,18971 +(define-key coq-keymap coq-keymap506,19026 +(define-key coq-keymap coq-keymap507,19076 +(define-key coq-keymap coq-keymap508,19126 +(defun coq-guess-command-line coq-guess-command-line565,21036 +(defun coq-pre-shell-start coq-pre-shell-start587,21842 +(defun coq-mode-config coq-mode-config598,22284 +(defun coq-shell-mode-config coq-shell-mode-config764,28257 +(defun coq-goals-mode-config coq-goals-mode-config803,29892 +(defun coq-response-config coq-response-config810,30123 +(defpacustom print-only-first-subgoal print-only-first-subgoal831,30713 +(defpacustom auto-compile-vos auto-compile-vos836,30864 +(defun coq-fake-constant-markup coq-fake-constant-markup857,31607 +(defun coq-create-span-menu coq-create-span-menu879,32414 + +coq/coq-syntax.el,2622 +(defvar coq-version-is-V74 coq-version-is-V7416,414 +(defvar coq-version-is-V7 coq-version-is-V717,446 +(defvar coq-version-is-V6 coq-version-is-V625,766 +(defvar coq-version-is-V7 coq-version-is-V732,1129 +(defvar coq-version-is-V74 coq-version-is-V7440,1534 +(defvar coq-keywords-declcoq-keywords-decl93,3303 +(defvar coq-keywords-defncoq-keywords-defn108,3659 +(defvar coq-keywords-savecoq-keywords-save150,4616 +(defvar coq-keywords-kill-goal coq-keywords-kill-goal156,4690 +(defcustom coq-user-state-changing-commands coq-user-state-changing-commands162,4740 +(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands174,5137 +(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands188,5623 +(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands236,6753 +(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands302,8581 +(defvar coq-keywords-commandscoq-keywords-commands312,8778 +(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics318,8928 +(defvar coq-state-changing-tacticscoq-state-changing-tactics329,9354 +(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics422,10916 +(defvar coq-state-preserving-tacticscoq-state-preserving-tactics433,11330 +(defvar coq-tacticscoq-tactics437,11428 +(defvar coq-retractable-instructcoq-retractable-instruct440,11517 +(defvar coq-non-retractable-instructcoq-non-retractable-instruct443,11627 +(defvar coq-keywordscoq-keywords447,11749 +(defvar coq-tacticalscoq-tacticals452,11914 +(defvar coq-reservedcoq-reserved461,12090 +(defvar coq-symbolscoq-symbols479,12298 +(defvar coq-error-regexp coq-error-regexp497,12502 +(defvar coq-id coq-id500,12705 +(defvar coq-ids coq-ids502,12731 +(defun coq-first-abstr-regexp coq-first-abstr-regexp504,12768 +(defun coq-next-abstr-regexp coq-next-abstr-regexp507,12856 +(defvar coq-font-lock-termscoq-font-lock-terms510,12934 +(defconst coq-save-command-regexpcoq-save-command-regexp525,13587 +(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp527,13686 +(defconst coq-goal-command-regexpcoq-goal-command-regexp530,13817 +(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp532,13916 +(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp538,14205 +(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp541,14338 +(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1544,14478 +(defvar coq-font-lock-keywords coq-font-lock-keywords565,15521 +(defun coq-init-syntax-table coq-init-syntax-table567,15579 + +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 + +demoisa/demoisa-easy.el,0 + +demoisa/demoisa.el,568 +(defcustom isabelledemo-prog-name isabelledemo-prog-name54,1801 +(defcustom isabelledemo-web-pageisabelledemo-web-page59,1923 +(defun demoisa-config demoisa-config70,2153 +(defun demoisa-shell-config demoisa-shell-config90,2902 +(define-derived-mode demoisa-mode demoisa-mode119,3979 +(define-derived-mode demoisa-shell-mode demoisa-shell-mode124,4102 +(define-derived-mode demoisa-response-mode demoisa-response-mode129,4245 +(define-derived-mode demoisa-goals-mode demoisa-goals-mode133,4372 +(defun demoisa-pre-shell-start demoisa-pre-shell-start152,5154 + +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 + +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-found63,2027 +(defun isa-set-isatool-command isa-set-isatool-command66,2140 +(defun isa-shell-command-to-string isa-shell-command-to-string86,2924 +(defun isa-getenv isa-getenv94,3376 +(defcustom isabelle-program-name isabelle-program-name113,4033 +(defvar isabelle-prog-name isabelle-prog-name139,4981 +(defun isabelle-command-line isabelle-command-line142,5108 +(defun isabelle-choose-logic isabelle-choose-logic165,6016 +(defun isa-tool-list-logics isa-tool-list-logics185,6902 +(defun isa-view-doc isa-view-doc191,7125 +(defvar isabelle-version-string isabelle-version-string198,7349 +(defun isa-version isa-version200,7390 +(defconst isa-supports-pgip isa-supports-pgip213,7873 +(defun isa-tool-list-docs isa-tool-list-docs221,8103 +(defun isa-quit isa-quit240,8832 +(defconst isabelle-verbatim-regexp isabelle-verbatim-regexp247,9027 +(defun isabelle-verbatim isabelle-verbatim250,9168 +(defcustom isabelle-refresh-logics isabelle-refresh-logics266,9759 +(defcustom isabelle-logics-available isabelle-logics-available274,10086 +(defcustom isabelle-chosen-logic isabelle-chosen-logic282,10386 +(defconst isabelle-docs-menu isabelle-docs-menu295,10854 +(defun isabelle-logics-menu-calculate isabelle-logics-menu-calculate303,11143 +(defun isabelle-logics-menu-refresh isabelle-logics-menu-refresh319,11623 +(defconst isabelle-logics-menu isabelle-logics-menu337,12218 +(defun isabelle-load-isar-keywords isabelle-load-isar-keywords346,12678 +(defpacustom show-types show-types373,13633 +(defpacustom show-sorts show-sorts378,13749 +(defpacustom show-consts show-consts383,13865 +(defpacustom long-names long-names388,13999 +(defpacustom eta-contract eta-contract393,14131 +(defpacustom trace-simplifier trace-simplifier398,14272 +(defpacustom trace-rules trace-rules403,14404 +(defpacustom quick-and-dirty quick-and-dirty408,14536 +(defpacustom full-proofs full-proofs413,14672 +(defpacustom global-timing global-timing419,14981 +(defpacustom theorem-dependencies theorem-dependencies425,15139 +(defpacustom goals-limit goals-limit431,15404 +(defpacustom prems-limit prems-limit436,15543 +(defpacustom print-depth print-depth441,15703 +(defpgdefault menu-entriesmenu-entries453,15992 +(defpgdefault help-menu-entries help-menu-entries460,16154 +(defpgdefault x-symbol-language x-symbol-language468,16348 +(defun isabelle-convert-idmarkup-to-subterm isabelle-convert-idmarkup-to-subterm491,16963 +(defun isabelle-create-span-menu isabelle-create-span-menu516,18002 +(defun isabelle-xml-sml-escapes isabelle-xml-sml-escapes533,18496 +(defun isabelle-process-pgip isabelle-process-pgip536,18597 +(defun isabelle-parse-syntax-dump isabelle-parse-syntax-dump553,19183 + +isa/isa.el,2283 +(defcustom isa-outline-regexpisa-outline-regexp43,1346 +(defcustom isa-outline-heading-end-regexp isa-outline-heading-end-regexp50,1583 +(defvar isa-shell-outline-regexp isa-shell-outline-regexp55,1735 +(defvar isa-shell-outline-heading-end-regexp isa-shell-outline-heading-end-regexp56,1797 +(defun isa-mode-config-set-variables isa-mode-config-set-variables59,1849 +(defun isa-shell-mode-config-set-variables isa-shell-mode-config-set-variables141,5258 +(defun isa-update-thy-only isa-update-thy-only278,10968 +(defun isa-shell-update-thy isa-shell-update-thy290,11476 +(defun isa-remove-file isa-remove-file315,12679 +(defun isa-shell-compute-new-files-list isa-shell-compute-new-files-list325,12997 +(define-derived-mode isa-shell-mode isa-shell-mode341,13509 +(define-derived-mode isa-response-mode isa-response-mode346,13634 +(define-derived-mode isa-goals-mode isa-goals-mode351,13803 +(define-derived-mode isa-proofscript-mode isa-proofscript-mode356,13960 +(defun isa-mode isa-mode365,14141 +(define-key map map409,15681 +(define-key map map410,15731 +(defun isa-process-thy-file isa-process-thy-file414,15888 +(defcustom isa-retract-thy-file-command isa-retract-thy-file-command420,16097 +(defun isa-retract-thy-file isa-retract-thy-file426,16334 +(defgroup thy thy442,16963 +(defun isa-splice-separator isa-splice-separator454,17293 +(defun isa-file-name-cons-extension isa-file-name-cons-extension463,17545 +(defun isa-format isa-format470,17811 +(define-key isa-proofscript-mode-map isa-proofscript-mode-map482,18186 +(defcustom isa-not-undoable-commands-regexpisa-not-undoable-commands-regexp492,18319 +(defun isa-count-undos isa-count-undos499,18572 +(defun isa-goal-command-p isa-goal-command-p529,19737 +(defun isa-find-and-forget isa-find-and-forget542,20382 +(defun isa-state-preserving-p isa-state-preserving-p545,20437 +(defun isa-pre-shell-start isa-pre-shell-start554,20805 +(defun isa-mode-config isa-mode-config561,21082 +(defun isa-shell-mode-config isa-shell-mode-config588,22155 +(defun isa-response-mode-config isa-response-mode-config595,22404 +(defun isa-goals-mode-config isa-goals-mode-config600,22565 +(defun isa-preprocessing isa-preprocessing608,22889 +(defpgdefault completion-tablecompletion-table622,23393 + +isa/isa-syntax.el,3046 +(defun isa-init-syntax-table isa-init-syntax-table14,304 +(defun isa-init-output-syntax-table isa-init-output-syntax-table34,952 +(defgroup isa-syntax isa-syntax71,2164 +(defcustom isa-keywords-defnisa-keywords-defn75,2266 +(defcustom isa-keywords-goalisa-keywords-goal82,2461 +(defcustom isa-keywords-saveisa-keywords-save88,2668 +(defcustom isa-keywords-commandsisa-keywords-commands97,2960 +(defcustom isa-keywords-smlisa-keywords-sml109,3349 +(defcustom isa-keyword-symbolsisa-keyword-symbols119,3818 +(defcustom isa-sml-names-keywordsisa-sml-names-keywords125,4013 +(defcustom isa-sml-typenames-keywordsisa-sml-typenames-keywords131,4186 +(defconst isa-keywordsisa-keywords140,4482 +(defconst isa-keywords-proof-commandsisa-keywords-proof-commands146,4663 +(defconst isa-tacticalsisa-tacticals151,4857 +(defconst isa-id isa-id159,5124 +(defconst isa-idx isa-idx160,5173 +(defconst isa-ids isa-ids162,5228 +(defconst isa-string isa-string165,5339 +(defcustom isa-save-command-regexpisa-save-command-regexp167,5398 +(defconst isa-save-with-hole-regexpisa-save-with-hole-regexp181,5802 +(defcustom isa-goal-command-regexpisa-goal-command-regexp185,5937 +(defconst isa-string-regexpisa-string-regexp197,6321 +(defconst isa-goal-with-hole-regexpisa-goal-with-hole-regexp201,6452 +(defconst isa-proof-command-regexpisa-proof-command-regexp209,6694 +(defface isabelle-class-name-faceisabelle-class-name-face216,6905 +(defface isabelle-tfree-name-faceisabelle-tfree-name-face226,7190 +(defface isabelle-tvar-name-faceisabelle-tvar-name-face236,7477 +(defface isabelle-free-name-faceisabelle-free-name-face246,7767 +(defface isabelle-bound-name-faceisabelle-bound-name-face256,8053 +(defface isabelle-var-name-faceisabelle-var-name-face266,8342 +(defface isabelle-sml-symbol-faceisabelle-sml-symbol-face277,8679 +(defconst isabelle-class-name-face isabelle-class-name-face287,9055 +(defconst isabelle-tfree-name-face isabelle-tfree-name-face288,9117 +(defconst isabelle-tvar-name-face isabelle-tvar-name-face289,9179 +(defconst isabelle-free-name-face isabelle-free-name-face290,9239 +(defconst isabelle-bound-name-face isabelle-bound-name-face291,9299 +(defconst isabelle-var-name-face isabelle-var-name-face292,9361 +(defconst isabelle-sml-symbol-face isabelle-sml-symbol-face293,9419 +(defconst isa-sml-function-var-names-regexp isa-sml-function-var-names-regexp296,9547 +(defconst isa-sml-type-names-regexp isa-sml-type-names-regexp301,9807 +(defvar isa-font-lock-keywords-1isa-font-lock-keywords-1305,9975 +(defvar isa-output-font-lock-keywords-1isa-output-font-lock-keywords-1315,10532 +(defvar isa-goals-font-lock-keywords isa-goals-font-lock-keywords327,11103 +(defconst isa-indent-any-regexpisa-indent-any-regexp341,11378 +(defconst isa-indent-inner-regexpisa-indent-inner-regexp343,11481 +(defconst isa-indent-enclose-regexpisa-indent-enclose-regexp345,11551 +(defconst isa-indent-open-regexpisa-indent-open-regexp347,11630 +(defconst isa-indent-close-regexpisa-indent-close-regexp349,11732 + +isa/isa-x-symbol.el,0 + +isa/thy-mode.el,2895 +(defcustom thy-heading-indent thy-heading-indent27,813 +(defcustom thy-indent-level thy-indent-level32,917 +(defcustom thy-indent-strings thy-indent-strings37,1044 +(defcustom thy-use-sml-mode thy-use-sml-mode44,1269 +(defcustom thy-sectionsthy-sections55,1677 +(defcustom thy-id-headerthy-id-header108,3354 +(defcustom thy-templatethy-template120,3654 +(defvar thy-mode-map thy-mode-map145,4082 +(defvar thy-mode-syntax-table thy-mode-syntax-table147,4109 +(defun thy-add-menus thy-add-menus182,5669 +(defun thy-mode thy-mode220,7065 +(defun thy-mode-quiet thy-mode-quiet275,8824 +(defun thy-proofgeneral-send-string thy-proofgeneral-send-string355,11584 +(defun isa-sml-hook isa-sml-hook434,14191 +(defun isa-sml-mode isa-sml-mode448,14786 +(defcustom isa-ml-file-extension isa-ml-file-extension453,14918 +(defun thy-find-other-file thy-find-other-file458,15040 +(defvar thy-minor-sml-mode-map thy-minor-sml-mode-map481,15922 +(defun thy-install-sml-mode thy-install-sml-mode483,15959 +(defun thy-minor-sml-mode thy-minor-sml-mode492,16345 +(defun thy-do-sml-indent thy-do-sml-indent510,16995 +(defun thy-insert-name thy-insert-name520,17392 +(defun thy-insert-class thy-insert-class526,17590 +(defun thy-insert-default-sort thy-insert-default-sort536,17862 +(defun thy-insert-type thy-insert-type544,18034 +(defun thy-insert-arity thy-insert-arity567,18604 +(defun thy-insert-const thy-insert-const580,18979 +(defun thy-insert-rule thy-insert-rule592,19368 +(defun thy-insert-template thy-insert-template601,19550 +(defun isa-read-idlist isa-read-idlist633,20429 +(defun isa-read-id isa-read-id642,20716 +(defun isa-read-string isa-read-string650,20945 +(defun isa-read-num isa-read-num658,21182 +(defun thy-read-thy-name thy-read-thy-name669,21474 +(defun thy-read-logic-image thy-read-logic-image678,21776 +(defun thy-insert-header thy-insert-header688,22040 +(defun thy-insert-id-header thy-insert-id-header706,22605 +(defun thy-check-mode thy-check-mode718,22964 +(defconst thy-headings-regexpthy-headings-regexp723,23069 +(defvar thy-mode-font-lock-keywordsthy-mode-font-lock-keywords733,23328 +(defun thy-goto-next-section thy-goto-next-section755,24088 +(defun thy-goto-prev-section thy-goto-prev-section783,25065 +(defun thy-goto-top-of-section thy-goto-top-of-section790,25378 +(defun thy-current-section thy-current-section797,25575 +(defun thy-kill-line thy-kill-line815,26038 +(defun thy-indent-line thy-indent-line877,28122 +(defun thy-calculate-indentation thy-calculate-indentation904,29156 +(defun thy-long-comment-string-indentation thy-long-comment-string-indentation924,29815 +(defun thy-string-indentation thy-string-indentation959,30799 +(defun thy-indentation-for thy-indentation-for978,31449 +(defun thy-string-start thy-string-start984,31608 +(defun thy-comment-or-string-start thy-comment-or-string-start998,32145 + +isa/x-symbol-isabelle.el,3147 +(defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts20,624 +(defvar x-symbol-isabelle-name x-symbol-isabelle-name30,1125 +(defvar x-symbol-isabelle-modeline-name x-symbol-isabelle-modeline-name31,1175 +(defcustom x-symbol-isabelle-header-groups-alist x-symbol-isabelle-header-groups-alist33,1223 +(defcustom x-symbol-isabelle-electric-ignore x-symbol-isabelle-electric-ignore40,1451 +(defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts48,1707 +(defvar x-symbol-isabelle-extra-menu-items x-symbol-isabelle-extra-menu-items51,1816 +(defvar x-symbol-isabelle-token-grammarx-symbol-isabelle-token-grammar55,1914 +(defun x-symbol-isabelle-token-list x-symbol-isabelle-token-list62,2120 +(defvar x-symbol-isabelle-user-table x-symbol-isabelle-user-table65,2209 +(defvar x-symbol-isabelle-generated-data x-symbol-isabelle-generated-data68,2330 +(defvar x-symbol-isabelle-master-directory x-symbol-isabelle-master-directory76,2573 +(defvar x-symbol-isabelle-image-searchpath x-symbol-isabelle-image-searchpath77,2626 +(defvar x-symbol-isabelle-image-cached-dirs x-symbol-isabelle-image-cached-dirs78,2678 +(defvar x-symbol-isabelle-image-file-truename-alist x-symbol-isabelle-image-file-truename-alist79,2748 +(defvar x-symbol-isabelle-image-keywords x-symbol-isabelle-image-keywords80,2805 +(defvar x-symbol-isabelle-subscript-matcherx-symbol-isabelle-subscript-matcher90,3142 +(defun x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher93,3227 +(defun x-symbol-isabelle-make-ctrl-regexp x-symbol-isabelle-make-ctrl-regexp100,3466 +(defconst x-symbol-isabelle-font-lock-bold-regexpx-symbol-isabelle-font-lock-bold-regexp106,3678 +(defconst x-symbol-isabelle-font-lock-scripts-regexpx-symbol-isabelle-font-lock-scripts-regexp110,3821 +(defun x-symbol-isabelle-match-bold x-symbol-isabelle-match-bold114,3986 +(defun x-symbol-isabelle-match-scripts x-symbol-isabelle-match-scripts124,4374 +(defvar x-symbol-isabelle-font-lock-keywordsx-symbol-isabelle-font-lock-keywords134,4786 +(defvar x-symbol-isabelle-font-lock-allowed-faces x-symbol-isabelle-font-lock-allowed-faces146,5297 +(defcustom x-symbol-isabelle-class-alistx-symbol-isabelle-class-alist153,5529 +(defcustom x-symbol-isabelle-class-face-alist x-symbol-isabelle-class-face-alist164,5954 +(defvar x-symbol-isabelle-case-insensitive x-symbol-isabelle-case-insensitive179,6482 +(defvar x-symbol-isabelle-token-shape x-symbol-isabelle-token-shape180,6530 +(defvar x-symbol-isabelle-input-token-ignore x-symbol-isabelle-input-token-ignore181,6573 +(defvar x-symbol-isabelle-token-list x-symbol-isabelle-token-list182,6623 +(defvar x-symbol-isabelle-symbol-table x-symbol-isabelle-symbol-table184,6672 +(defvar x-symbol-isabelle-xsymbol-table x-symbol-isabelle-xsymbol-table283,9383 +(defun x-symbol-isabelle-prepare-table x-symbol-isabelle-prepare-table428,13785 +(defvar x-symbol-isabelle-tablex-symbol-isabelle-table440,14196 +(defcustom x-symbol-isabelle-auto-stylex-symbol-isabelle-auto-style454,14549 +(defcustom x-symbol-isabelle-auto-coding-alist x-symbol-isabelle-auto-coding-alist468,15059 + +isa/x-symbol-isa.el,0 + +isar/isar.el,1882 +(defcustom isar-keywords-name isar-keywords-name25,547 +(defpgdefault completion-table completion-table42,1071 +(defcustom isar-web-pageisar-web-page44,1124 +(defun isar-detect-header isar-detect-header62,1488 +(defun isar-strip-terminators isar-strip-terminators97,2751 +(defun isar-markup-ml isar-markup-ml110,3122 +(defun isar-mode-config-set-variables isar-mode-config-set-variables115,3257 +(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables176,5942 +(defun isar-remove-file isar-remove-file285,10574 +(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list295,10937 +(defun isar-activate-scripting isar-activate-scripting306,11403 +(define-derived-mode isar-shell-mode isar-shell-mode315,11573 +(define-derived-mode isar-response-mode isar-response-mode320,11696 +(define-derived-mode isar-goals-mode isar-goals-mode325,11878 +(define-derived-mode isar-mode isar-mode330,12053 +(defpgdefault menu-entriesmenu-entries363,13409 +(defun isar-count-undos isar-count-undos387,14431 +(defun isar-find-and-forget isar-find-and-forget413,15532 +(defun isar-goal-command-p isar-goal-command-p456,17150 +(defun isar-global-save-command-p isar-global-save-command-p460,17282 +(defvar isar-current-goal isar-current-goal481,18119 +(defun isar-state-preserving-p isar-state-preserving-p484,18185 +(defvar isar-shell-current-line-width isar-shell-current-line-width504,18948 +(defun isar-shell-adjust-line-width isar-shell-adjust-line-width510,19170 +(defun isar-pre-shell-start isar-pre-shell-start530,20056 +(defun isar-preprocessing isar-preprocessing542,20392 +(defun isar-mode-config isar-mode-config565,21603 +(defun isar-shell-mode-config isar-shell-mode-config576,22106 +(defun isar-response-mode-config isar-response-mode-config587,22476 +(defun isar-goals-mode-config isar-goals-mode-config596,22733 + +isar/isar-keywords.el,1650 +(defconst isar-keywords-majorisar-keywords-major14,378 +(defconst isar-keywords-minorisar-keywords-minor169,2840 +(defconst isar-keywords-controlisar-keywords-control207,3351 +(defconst isar-keywords-diagisar-keywords-diag225,3768 +(defconst isar-keywords-theory-beginisar-keywords-theory-begin268,4490 +(defconst isar-keywords-theory-switchisar-keywords-theory-switch271,4543 +(defconst isar-keywords-theory-endisar-keywords-theory-end274,4598 +(defconst isar-keywords-theory-headingisar-keywords-theory-heading277,4646 +(defconst isar-keywords-theory-declisar-keywords-theory-decl283,4753 +(defconst isar-keywords-theory-scriptisar-keywords-theory-script326,5463 +(defconst isar-keywords-theory-goalisar-keywords-theory-goal330,5540 +(defconst isar-keywords-qedisar-keywords-qed337,5650 +(defconst isar-keywords-qed-blockisar-keywords-qed-block344,5736 +(defconst isar-keywords-qed-globalisar-keywords-qed-global347,5783 +(defconst isar-keywords-proof-headingisar-keywords-proof-heading350,5832 +(defconst isar-keywords-proof-goalisar-keywords-proof-goal355,5915 +(defconst isar-keywords-proof-blockisar-keywords-proof-block361,5998 +(defconst isar-keywords-proof-openisar-keywords-proof-open365,6060 +(defconst isar-keywords-proof-closeisar-keywords-proof-close368,6106 +(defconst isar-keywords-proof-chainisar-keywords-proof-chain371,6153 +(defconst isar-keywords-proof-declisar-keywords-proof-decl378,6256 +(defconst isar-keywords-proof-asmisar-keywords-proof-asm386,6365 +(defconst isar-keywords-proof-asm-goalisar-keywords-proof-asm-goal393,6460 +(defconst isar-keywords-proof-scriptisar-keywords-proof-script396,6515 + +isar/isar-mmm.el,129 +(defconst isar-start-latex-regexp isar-start-latex-regexp23,689 +(defconst isar-start-sml-regexp isar-start-sml-regexp35,1122 + +isar/isar-syntax.el,4568 +(defun isar-init-syntax-table isar-init-syntax-table17,390 +(defun isar-init-output-syntax-table isar-init-output-syntax-table56,1757 +(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose71,2172 +(defconst isar-keywords-theoryisar-keywords-theory76,2324 +(defconst isar-keywords-saveisar-keywords-save81,2469 +(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose86,2598 +(defconst isar-keywords-proofisar-keywords-proof92,2780 +(defconst isar-keywords-proof-contextisar-keywords-proof-context99,2978 +(defconst isar-keywords-local-goalisar-keywords-local-goal103,3092 +(defconst isar-keywords-improperisar-keywords-improper107,3204 +(defconst isar-keywords-outlineisar-keywords-outline112,3343 +(defconst isar-keywords-fumeisar-keywords-fume115,3408 +(defconst isar-keywords-indent-openisar-keywords-indent-open122,3626 +(defconst isar-keywords-indent-closeisar-keywords-indent-close128,3810 +(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose132,3915 +(defun isar-ids-to-regexp isar-ids-to-regexp148,4459 +(defconst isar-long-id-stuff isar-long-id-stuff170,5281 +(defconst isar-id isar-id172,5336 +(defconst isar-idx isar-idx173,5386 +(defconst isar-string isar-string175,5443 +(defconst isar-any-command-regexpisar-any-command-regexp177,5501 +(defconst isar-name-regexpisar-name-regexp181,5635 +(defconst isar-tac-regexpisar-tac-regexp185,5787 +(defconst isar-save-command-regexpisar-save-command-regexp189,5895 +(defconst isar-global-save-command-regexpisar-global-save-command-regexp192,5996 +(defconst isar-goal-command-regexpisar-goal-command-regexp195,6110 +(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp198,6218 +(defconst isar-comment-start isar-comment-start201,6331 +(defconst isar-comment-end isar-comment-end202,6366 +(defconst isar-comment-start-regexp isar-comment-start-regexp203,6399 +(defconst isar-comment-end-regexp isar-comment-end-regexp204,6470 +(defconst isar-string-start-regexp isar-string-start-regexp206,6538 +(defconst isar-string-end-regexp isar-string-end-regexp207,6586 +(defconst isar-antiq-regexpisar-antiq-regexp212,6653 +(defun isar-match-antiq isar-match-antiq216,6796 +(defface isabelle-class-name-faceisabelle-class-name-face232,7210 +(defface isabelle-tfree-name-faceisabelle-tfree-name-face242,7485 +(defface isabelle-tvar-name-faceisabelle-tvar-name-face252,7766 +(defface isabelle-free-name-faceisabelle-free-name-face262,8046 +(defface isabelle-bound-name-faceisabelle-bound-name-face272,8322 +(defface isabelle-var-name-faceisabelle-var-name-face282,8601 +(defconst isabelle-class-name-face isabelle-class-name-face292,8880 +(defconst isabelle-tfree-name-face isabelle-tfree-name-face293,8942 +(defconst isabelle-tvar-name-face isabelle-tvar-name-face294,9004 +(defconst isabelle-free-name-face isabelle-free-name-face295,9065 +(defconst isabelle-bound-name-face isabelle-bound-name-face296,9126 +(defconst isabelle-var-name-face isabelle-var-name-face297,9188 +(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1299,9249 +(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1313,10178 +(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords325,10834 +(defconst isar-undo isar-undo356,11468 +(defconst isar-kill isar-kill357,11497 +(defun isar-remove isar-remove359,11527 +(defun isar-undos isar-undos362,11606 +(defun isar-cannot-undo isar-cannot-undo366,11712 +(defconst isar-undo-fail-regexpisar-undo-fail-regexp370,11783 +(defconst isar-undo-skip-regexpisar-undo-skip-regexp374,11921 +(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp377,12042 +(defconst isar-undo-remove-regexpisar-undo-remove-regexp380,12107 +(defconst isar-undo-kill-regexpisar-undo-kill-regexp385,12247 +(defconst isar-any-entity-regexpisar-any-entity-regexp391,12379 +(defconst isar-named-entity-regexpisar-named-entity-regexp395,12522 +(defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp399,12657 +(defconst isar-next-entity-regexpsisar-next-entity-regexps402,12759 +(defconst isar-indent-any-regexpisar-indent-any-regexp410,12942 +(defconst isar-indent-inner-regexpisar-indent-inner-regexp412,13035 +(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp414,13101 +(defconst isar-indent-open-regexpisar-indent-open-regexp416,13217 +(defconst isar-indent-close-regexpisar-indent-close-regexp418,13327 +(defconst isar-outline-regexpisar-outline-regexp424,13464 +(defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp428,13615 + +isar/mmm-isar-latex.el,292 +(defconst mmm-isar-latex-sh-start-tagsmmm-isar-latex-sh-start-tags5,32 +(defvar mmm-isar-latex-sh-end-tagsmmm-isar-latex-sh-end-tags10,263 +(defvar mmm-isar-latex-sh-start-regexpmmm-isar-latex-sh-start-regexp14,451 +(defvar mmm-isar-latex-sh-end-regexpmmm-isar-latex-sh-end-regexp18,643 + +isar/test.el,56 +(defun isar-goal-command-p isar-goal-command-p38,1315 + +isar/x-symbol-isar.el,0 + +lclam/lclam.el,805 +(defcustom lclam-prog-name lclam-prog-name13,330 +(defcustom lclam-web-pagelclam-web-page19,478 +(defun lclam-config lclam-config30,708 +(defun lclam-shell-config lclam-shell-config50,1419 +(define-derived-mode lclam-proofscript-mode lclam-proofscript-mode70,2078 +(define-derived-mode lclam-shell-mode lclam-shell-mode75,2201 +(define-derived-mode lclam-response-mode lclam-response-mode80,2335 +(define-derived-mode lclam-goals-mode lclam-goals-mode84,2458 +(defun lclam-mode lclam-mode92,2686 +(defun lclam-pre-shell-start lclam-pre-shell-start105,2969 +(define-derived-mode thy-mode thy-mode139,3912 +(defvar thy-mode-map thy-mode-map144,4027 +(defun thy-add-menus thy-add-menus146,4054 +(defun process-thy-file process-thy-file184,5865 +(defun update-thy-only update-thy-only190,6066 + +lego/lego.el,2717 +(defcustom lego-tags lego-tags19,493 +(defcustom lego-test-all-name lego-test-all-name24,629 +(defpgdefault help-menu-entrieshelp-menu-entries30,787 +(defpgdefault menu-entriesmenu-entries34,947 +(defvar lego-shell-process-outputlego-shell-process-output45,1249 +(defconst lego-process-configlego-process-config53,1572 +(defconst lego-pretty-set-width lego-pretty-set-width64,2003 +(defconst lego-interrupt-regexp lego-interrupt-regexp68,2146 +(defcustom lego-www-home-page lego-www-home-page73,2263 +(defcustom lego-www-latest-releaselego-www-latest-release78,2387 +(defcustom lego-www-refcardlego-www-refcard84,2565 +(defcustom lego-library-www-pagelego-library-www-page90,2714 +(defvar lego-prog-name lego-prog-name99,2930 +(defvar lego-shell-prompt-pattern lego-shell-prompt-pattern102,2999 +(defvar lego-shell-cd lego-shell-cd105,3120 +(defvar lego-shell-abort-goal-regexp lego-shell-abort-goal-regexp108,3220 +(defvar lego-shell-proof-completed-regexp lego-shell-proof-completed-regexp113,3412 +(defvar lego-save-command-regexplego-save-command-regexp116,3552 +(defvar lego-goal-command-regexplego-goal-command-regexp118,3642 +(defvar lego-kill-goal-command lego-kill-goal-command121,3733 +(defvar lego-forget-id-command lego-forget-id-command122,3776 +(defvar lego-undoable-commands-regexplego-undoable-commands-regexp124,3822 +(defvar lego-goal-regexp lego-goal-regexp133,4196 +(defvar lego-outline-regexplego-outline-regexp135,4241 +(defvar lego-outline-heading-end-regexp lego-outline-heading-end-regexp141,4417 +(defvar lego-shell-outline-regexp lego-shell-outline-regexp143,4470 +(defvar lego-shell-outline-heading-end-regexp lego-shell-outline-heading-end-regexp144,4522 +(define-derived-mode lego-shell-mode lego-shell-mode150,4801 +(define-derived-mode lego-mode lego-mode156,4974 +(define-derived-mode lego-goals-mode lego-goals-mode167,5271 +(defun lego-count-undos lego-count-undos178,5697 +(defun lego-goal-command-p lego-goal-command-p198,6516 +(defun lego-find-and-forget lego-find-and-forget202,6648 +(defun lego-goal-hyp lego-goal-hyp242,8430 +(defun lego-state-preserving-p lego-state-preserving-p251,8628 +(defvar lego-shell-current-line-width lego-shell-current-line-width267,9331 +(defun lego-shell-adjust-line-width lego-shell-adjust-line-width275,9638 +(defun lego-pre-shell-start lego-pre-shell-start294,10375 +(defun lego-mode-config lego-mode-config301,10572 +(defun lego-equal-module-filename lego-equal-module-filename370,12667 +(defun lego-shell-compute-new-files-list lego-shell-compute-new-files-list376,12942 +(defun lego-shell-mode-config lego-shell-mode-config390,13468 +(defun lego-goals-mode-config lego-goals-mode-config436,15311 + +lego/lego-syntax.el,919 +(defconst lego-keywords-goal lego-keywords-goal15,358 +(defconst lego-keywords-save lego-keywords-save17,401 +(defconst lego-commandslego-commands19,472 +(defconst lego-keywordslego-keywords31,1032 +(defconst lego-tacticals lego-tacticals36,1209 +(defconst lego-error-regexp lego-error-regexp39,1317 +(defvar lego-id lego-id42,1476 +(defvar lego-ids lego-ids44,1503 +(defconst lego-arg-list-regexp lego-arg-list-regexp48,1699 +(defun lego-decl-defn-regexp lego-decl-defn-regexp51,1815 +(defconst lego-definiendum-alternative-regexplego-definiendum-alternative-regexp59,2187 +(defvar lego-font-lock-termslego-font-lock-terms63,2371 +(defconst lego-goal-with-hole-regexplego-goal-with-hole-regexp89,3227 +(defconst lego-save-with-hole-regexplego-save-with-hole-regexp94,3450 +(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 + +pgkit/pgip.el,48 +(defun pgip-add-markup pgip-add-markup59,1946 + +phox/phox.el,886 +(defcustom phox-prog-name phox-prog-name30,907 +(defcustom phox-sym-lock phox-sym-lock35,1009 +(defcustom phox-web-pagephox-web-page40,1107 +(defcustom phox-doc-dir phox-doc-dir46,1257 +(defcustom phox-lib-dir phox-lib-dir52,1405 +(defcustom phox-tags-program phox-tags-program58,1549 +(defcustom phox-tags-doc phox-tags-doc64,1729 +(defcustom phox-etags phox-etags70,1867 +(defpgdefault menu-entriesmenu-entries90,2297 +(defun phox-config phox-config107,2626 +(defun phox-shell-config phox-shell-config148,4520 +(define-derived-mode phox-mode phox-mode188,6100 +(define-derived-mode phox-shell-mode phox-shell-mode203,6544 +(define-derived-mode phox-response-mode phox-response-mode208,6672 +(define-derived-mode phox-goals-mode phox-goals-mode220,7091 +(defun phox-pre-shell-start phox-pre-shell-start246,8150 +(defpgdefault completion-tablecompletion-table260,8664 + +phox/phox-extraction.el,603 +(defvar phox-prog-orig phox-prog-orig11,480 +(defun phox-prog-flags-modify(phox-prog-flags-modify13,548 +(defun phox-prog-flags-extract(phox-prog-flags-extract42,1352 +(defun phox-prog-flags-erase(phox-prog-flags-erase53,1643 +(defun phox-toggle-extraction(phox-toggle-extraction61,1839 +(defun phox-compile-theorem(phox-compile-theorem73,2241 +(defun phox-compile-theorem-on-cursor(phox-compile-theorem-on-cursor79,2467 +(defun phox-output phox-output95,2946 +(defun phox-output-theorem phox-output-theorem105,3160 +(defun phox-output-theorem-on-cursor(phox-output-theorem-on-cursor112,3460 + +phox/phox-font.el,196 +(defconst phox-font-lock-keywordsphox-font-lock-keywords6,282 +(defconst phox-sym-lock-keywords-tablephox-sym-lock-keywords-table62,2258 +(defun phox-sym-lock-start phox-sym-lock-start85,2839 + +phox/phox-fun.el,1048 +(defun phox-init-syntax-table phox-init-syntax-table67,2357 +(defvar phox-top-keywordsphox-top-keywords83,2830 +(defvar phox-proof-keywordsphox-proof-keywords130,3278 +(defun phox-find-and-forget phox-find-and-forget171,3628 +(defun phox-assert-next-command-interactive phox-assert-next-command-interactive248,5940 +(defun phox-depend-theorem(phox-depend-theorem267,6770 +(defun phox-eshow-extlist(phox-eshow-extlist276,7060 +(defun phox-flag-name(phox-flag-name290,7659 +(defun phox-path(phox-path301,7962 +(defun phox-print-expression(phox-print-expression312,8199 +(defun phox-print-sort-expression(phox-print-sort-expression325,8657 +(defun phox-priority-symbols-list(phox-priority-symbols-list336,8970 +(defun phox-search-string(phox-search-string348,9343 +(defun phox-constraints(phox-constraints363,9871 +(defun phox-goals(phox-goals374,10128 +(defvar phox-state-menuphox-state-menu386,10338 +(defun phox-delete-symbol(phox-delete-symbol411,11328 +(defun phox-delete-symbol-on-cursor(phox-delete-symbol-on-cursor417,11537 + +phox/phox-outline.el,108 +(defun phox-outline-level(phox-outline-level32,1113 +(defun phox-setup-outline phox-setup-outline46,1587 + +phox/phox-sym-lock.el,2167 +(defvar phox-sym-lock-sym-count phox-sym-lock-sym-count34,1669 +(defvar phox-sym-lock-ext-start phox-sym-lock-ext-start37,1739 +(defvar phox-sym-lock-ext-end phox-sym-lock-ext-end39,1861 +(defvar phox-sym-lock-font-size phox-sym-lock-font-size42,1980 +(defvar phox-sym-lock-keywords phox-sym-lock-keywords47,2170 +(defvar phox-sym-lock-enabled phox-sym-lock-enabled52,2346 +(defvar phox-sym-lock-color phox-sym-lock-color57,2508 +(defvar phox-sym-lock-mouse-face phox-sym-lock-mouse-face62,2726 +(defvar phox-sym-lock-mouse-face-enabled phox-sym-lock-mouse-face-enabled67,2916 +(defconst phox-sym-lock-with-mule phox-sym-lock-with-mule72,3106 +(defun phox-sym-lock-gen-symbol phox-sym-lock-gen-symbol75,3190 +(defun phox-sym-lock-make-symbols-atomic phox-sym-lock-make-symbols-atomic83,3493 +(defun phox-sym-lock-compute-font-size phox-sym-lock-compute-font-size110,4435 +(defvar phox-sym-lock-font-namephox-sym-lock-font-name147,5781 +(defun phox-sym-lock-set-foreground phox-sym-lock-set-foreground185,7066 +(defun phox-sym-lock-translate-char phox-sym-lock-translate-char199,7675 +(defun phox-sym-lock-translate-char-or-string phox-sym-lock-translate-char-or-string207,7943 +(defun phox-sym-lock-remap-face phox-sym-lock-remap-face214,8170 +(defvar phox-sym-lock-clear-facephox-sym-lock-clear-face234,9160 +(defun phox-sym-lock phox-sym-lock246,9582 +(defun phox-sym-lock-rec phox-sym-lock-rec255,9986 +(defun phox-sym-lock-atom-face phox-sym-lock-atom-face261,10139 +(defun phox-sym-lock-pre-idle-hook-first phox-sym-lock-pre-idle-hook-first266,10435 +(defun phox-sym-lock-pre-idle-hook-last phox-sym-lock-pre-idle-hook-last274,10793 +(defun phox-sym-lock-enable phox-sym-lock-enable283,11168 +(defun phox-sym-lock-disable phox-sym-lock-disable296,11581 +(defun phox-sym-lock-mouse-face-enable phox-sym-lock-mouse-face-enable309,11999 +(defun phox-sym-lock-mouse-face-disable phox-sym-lock-mouse-face-disable316,12214 +(defun phox-sym-lock-font-lock-hook phox-sym-lock-font-lock-hook323,12433 +(defun font-lock-set-defaults font-lock-set-defaults338,13126 +(defun phox-sym-lock-patch-keywords phox-sym-lock-patch-keywords349,13504 + +phox/phox-tags.el,483 +(defun phox-tags-add-table(phox-tags-add-table21,766 +(defun phox-tags-reset-table(phox-tags-reset-table38,1359 +(defun phox-tags-add-doc-table(phox-tags-add-doc-table48,1629 +(defun phox-tags-add-lib-table(phox-tags-add-lib-table54,1778 +(defun phox-tags-add-local-table(phox-tags-add-local-table60,1914 +(defun phox-tags-create-local-table(phox-tags-create-local-table66,2097 +(defun phox-complete-tag(phox-complete-tag77,2349 +(defvar phox-tags-menuphox-tags-menu96,2904 + +phox/x-symbol-phox.el,2672 +(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-faces127,4556 +(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive133,4781 +(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape134,4825 +(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore135,4864 +(defvar x-symbol-phox-token-list x-symbol-phox-token-list142,5103 +(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table144,5148 +(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table165,5603 +(defvar x-symbol-phox-tablex-symbol-phox-table172,5774 +(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist183,6146 +(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist185,6236 +(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree188,6327 +(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist190,6420 +(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist192,6517 +(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec196,6674 +(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec198,6774 + +plastic/plastic.el,4425 +(defcustom plastic-tags plastic-tags28,805 +(defcustom plastic-test-all-name plastic-test-all-name33,937 +(defvar plastic-lit-string plastic-lit-string39,1110 +(defcustom plastic-help-menu-listplastic-help-menu-list43,1223 +(defvar plastic-shell-process-outputplastic-shell-process-output57,1717 +(defconst plastic-process-config plastic-process-config65,2043 +(defconst plastic-pretty-set-width plastic-pretty-set-width72,2293 +(defconst plastic-interrupt-regexp plastic-interrupt-regexp76,2442 +(defcustom plastic-www-home-page plastic-www-home-page82,2563 +(defcustom plastic-www-latest-releaseplastic-www-latest-release87,2700 +(defcustom plastic-www-refcardplastic-www-refcard93,2873 +(defcustom plastic-library-www-pageplastic-library-www-page99,3004 +(defcustom plastic-base plastic-base109,3219 +(defvar plastic-prog-name plastic-prog-name117,3391 +(defun plastic-set-default-env-vars plastic-set-default-env-vars121,3499 +(defvar plastic-shell-prompt-pattern plastic-shell-prompt-pattern129,3737 +(defvar plastic-shell-cd plastic-shell-cd132,3862 +(defvar plastic-shell-abort-goal-regexp plastic-shell-abort-goal-regexp136,4004 +(defvar plastic-shell-proof-completed-regexp plastic-shell-proof-completed-regexp140,4172 +(defvar plastic-save-command-regexpplastic-save-command-regexp143,4315 +(defvar plastic-goal-command-regexpplastic-goal-command-regexp145,4411 +(defvar plastic-kill-goal-command plastic-kill-goal-command148,4508 +(defvar plastic-forget-id-command plastic-forget-id-command150,4609 +(defvar plastic-undoable-commands-regexpplastic-undoable-commands-regexp153,4690 +(defvar plastic-goal-regexp plastic-goal-regexp165,5137 +(defvar plastic-outline-regexpplastic-outline-regexp167,5185 +(defvar plastic-outline-heading-end-regexp plastic-outline-heading-end-regexp173,5364 +(defvar plastic-shell-outline-regexp plastic-shell-outline-regexp175,5420 +(defvar plastic-shell-outline-heading-end-regexp plastic-shell-outline-heading-end-regexp176,5478 +(defvar plastic-error-occurred plastic-error-occurred178,5549 +(define-derived-mode plastic-shell-mode plastic-shell-mode187,5881 +(define-derived-mode plastic-mode plastic-mode193,6063 +(define-derived-mode plastic-goals-mode plastic-goals-mode207,6516 +(defun plastic-count-undos plastic-count-undos216,6861 +(defun plastic-goal-command-p plastic-goal-command-p236,7737 +(defun plastic-find-and-forget plastic-find-and-forget240,7890 +(defun plastic-goal-hyp plastic-goal-hyp274,9170 +(defun plastic-state-preserving-p plastic-state-preserving-p285,9420 +(defvar plastic-shell-current-line-width plastic-shell-current-line-width307,10348 +(defun plastic-shell-adjust-line-width plastic-shell-adjust-line-width315,10664 +(defun plastic-pre-shell-start plastic-pre-shell-start336,11543 +(defun plastic-mode-config plastic-mode-config351,12109 +(defun plastic-show-shell-buffer plastic-show-shell-buffer448,15751 +(defun plastic-equal-module-filename plastic-equal-module-filename454,15854 +(defun plastic-shell-compute-new-files-list plastic-shell-compute-new-files-list460,16132 +(defun plastic-shell-mode-config plastic-shell-mode-config476,16669 +(defun plastic-goals-mode-config plastic-goals-mode-config527,18859 +(defun plastic-small-bar plastic-small-bar539,19141 +(defun plastic-large-bar plastic-large-bar541,19230 +(defun plastic-preprocessing plastic-preprocessing543,19368 +(defun plastic-all-ctxt plastic-all-ctxt594,21196 +(defun plastic-send-one-undo plastic-send-one-undo601,21374 +(defun plastic-minibuf-cmd plastic-minibuf-cmd611,21702 +(defun plastic-minibuf plastic-minibuf623,22181 +(defun plastic-synchro plastic-synchro630,22387 +(defun plastic-send-minibuf plastic-send-minibuf635,22528 +(defun plastic-had-error plastic-had-error643,22857 +(defun plastic-reset-error plastic-reset-error647,23032 +(defun plastic-call-if-no-error plastic-call-if-no-error650,23171 +(defun plastic-show-shell plastic-show-shell655,23375 +(define-key plastic-keymap plastic-keymap663,23582 +(define-key plastic-keymap plastic-keymap664,23632 +(define-key plastic-keymap plastic-keymap665,23682 +(define-key plastic-keymap plastic-keymap666,23731 +(define-key plastic-keymap plastic-keymap667,23779 +(define-key plastic-keymap plastic-keymap668,23827 +(defalias 'proof-toolbar-command proof-toolbar-command678,24066 +(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd679,24117 + +plastic/plastic-syntax.el,1015 +(defconst plastic-keywords-goal plastic-keywords-goal18,537 +(defconst plastic-keywords-save plastic-keywords-save20,583 +(defconst plastic-commandsplastic-commands22,657 +(defconst plastic-keywordsplastic-keywords35,1267 +(defconst plastic-tacticals plastic-tacticals40,1450 +(defconst plastic-error-regexp plastic-error-regexp43,1561 +(defvar plastic-id plastic-id46,1695 +(defvar plastic-ids plastic-ids48,1725 +(defconst plastic-arg-list-regexp plastic-arg-list-regexp52,1933 +(defun plastic-decl-defn-regexp plastic-decl-defn-regexp55,2052 +(defconst plastic-definiendum-alternative-regexpplastic-definiendum-alternative-regexp63,2433 +(defvar plastic-font-lock-termsplastic-font-lock-terms67,2626 +(defconst plastic-goal-with-hole-regexpplastic-goal-with-hole-regexp89,3339 +(defconst plastic-save-with-hole-regexpplastic-save-with-hole-regexp94,3566 +(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 +(defcustom twelf-root-dirtwelf-root-dir25,583 +(defcustom twelf-info-dirtwelf-info-dir31,741 +(defun twelf-add-read-declaration twelf-add-read-declaration97,3163 +(defun twelf-set-syntax twelf-set-syntax110,3498 +(defun twelf-set-word twelf-set-word112,3595 +(defun twelf-set-symbol twelf-set-symbol113,3657 +(defun twelf-map-string twelf-map-string115,3721 +(defun twelf-mode-extra-config twelf-mode-extra-config162,5783 +(defconst twelf-syntax-menutwelf-syntax-menu168,5989 +(defpacustom chatter chatter182,6356 +(defpacustom double-check double-check187,6449 +(defpacustom print-implicit print-implicit191,6586 +(defpgdefault menu-entriesmenu-entries203,6730 + +twelf/twelf-font.el,1425 +(defun twelf-font-create-face twelf-font-create-face31,828 +(defvar twelf-font-dark-background twelf-font-dark-background38,1086 +(defvar twelf-font-patternstwelf-font-patterns64,2444 +(defun twelf-font-fontify-decl twelf-font-fontify-decl105,4294 +(defun twelf-font-fontify-buffer twelf-font-fontify-buffer115,4591 +(defun twelf-font-unfontify twelf-font-unfontify122,4850 +(defvar font-lock-message-threshold font-lock-message-threshold127,5024 +(defun twelf-font-fontify-region twelf-font-fontify-region129,5102 +(defun twelf-font-highlight twelf-font-highlight195,7602 +(defun twelf-font-find-delimited-comment twelf-font-find-delimited-comment204,8059 +(defun twelf-font-find-decl twelf-font-find-decl223,8739 +(defun twelf-font-find-binder twelf-font-find-binder239,9229 +(defun twelf-font-find-parm twelf-font-find-parm301,11086 +(defun twelf-font-find-evar twelf-font-find-evar308,11409 +(defun twelf-current-decl twelf-current-decl330,12151 +(defun twelf-next-decl twelf-next-decl357,13307 +(defconst *whitespace* *whitespace*382,14329 +(defconst *twelf-comment-start* *twelf-comment-start*385,14427 +(defconst *twelf-id-chars* *twelf-id-chars*388,14556 +(defun skip-twelf-comments-and-whitespace skip-twelf-comments-and-whitespace391,14674 +(defun twelf-end-of-par twelf-end-of-par403,15148 +(defun skip-ahead skip-ahead426,15922 +(defun current-line-absolute current-line-absolute438,16344 + +twelf/twelf-old.el,10513 +(defvar twelf-indent twelf-indent212,8763 +(defvar twelf-infix-regexp twelf-infix-regexp215,8823 +(defvar twelf-server-program twelf-server-program219,9018 +(defvar twelf-info-file twelf-info-file222,9099 +(defvar twelf-server-display-commands twelf-server-display-commands225,9172 +(defvar twelf-highlight-range-function twelf-highlight-range-function230,9420 +(defvar twelf-focus-function twelf-focus-function235,9703 +(defvar twelf-server-echo-commands twelf-server-echo-commands241,9983 +(defvar twelf-save-silently twelf-save-silently244,10104 +(defvar twelf-server-timeout twelf-server-timeout248,10276 +(defvar twelf-sml-program twelf-sml-program252,10423 +(defvar twelf-sml-args twelf-sml-args255,10495 +(defvar twelf-sml-display-queries twelf-sml-display-queries258,10561 +(defvar twelf-mode-hook twelf-mode-hook261,10669 +(defvar twelf-server-mode-hook twelf-server-mode-hook264,10763 +(defvar twelf-config-mode-hook twelf-config-mode-hook267,10871 +(defvar twelf-sml-mode-hook twelf-sml-mode-hook270,10985 +(defvar twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode273,11066 +(defvar twelf-config-mode twelf-config-mode276,11158 +(defvar *twelf-server-buffer-name* *twelf-server-buffer-name*283,11422 +(defvar *twelf-server-buffer* *twelf-server-buffer*286,11526 +(defvar *twelf-server-process-name* *twelf-server-process-name*289,11614 +(defvar *twelf-config-buffer* *twelf-config-buffer*292,11705 +(defvar *twelf-config-time* *twelf-config-time*295,11799 +(defvar *twelf-config-list* *twelf-config-list*298,11912 +(defvar *twelf-server-last-process-mark* *twelf-server-last-process-mark*301,12024 +(defvar *twelf-last-region-sent* *twelf-last-region-sent*304,12142 +(defvar *twelf-last-input-buffer* *twelf-last-input-buffer*311,12466 +(defvar *twelf-error-pos* *twelf-error-pos*315,12589 +(defconst *twelf-read-functions**twelf-read-functions*318,12665 +(defconst *twelf-parm-table**twelf-parm-table*325,12903 +(defvar twelf-chatter twelf-chatter338,13279 +(defvar twelf-double-check twelf-double-check346,13496 +(defvar twelf-print-implicit twelf-print-implicit349,13583 +(defconst *twelf-track-parms**twelf-track-parms*352,13675 +(defun install-basic-twelf-keybindings install-basic-twelf-keybindings363,14099 +(defun install-twelf-keybindings install-twelf-keybindings388,15068 +(defvar twelf-mode-map twelf-mode-map404,15833 +(defvar twelf-mode-syntax-table twelf-mode-syntax-table416,16269 +(defun set-twelf-syntax set-twelf-syntax419,16348 +(defun set-word set-word421,16445 +(defun set-symbol set-symbol422,16500 +(defun map-string map-string424,16558 +(defconst *whitespace* *whitespace*456,18035 +(defconst *twelf-comment-start* *twelf-comment-start*459,18133 +(defconst *twelf-id-chars* *twelf-id-chars*462,18262 +(defun skip-twelf-comments-and-whitespace skip-twelf-comments-and-whitespace465,18380 +(defun twelf-end-of-par twelf-end-of-par477,18854 +(defun twelf-current-decl twelf-current-decl500,19628 +(defun twelf-mark-decl twelf-mark-decl527,20784 +(defun twelf-indent-decl twelf-indent-decl536,21050 +(defun twelf-indent-region twelf-indent-region545,21336 +(defun twelf-indent-lines twelf-indent-lines556,21660 +(defun twelf-comment-indent twelf-comment-indent564,21833 +(defun looked-at looked-at575,22189 +(defun twelf-indent-line twelf-indent-line580,22361 +(defun twelf-indent-line-to twelf-indent-line-to613,24104 +(defun twelf-calculate-indent twelf-calculate-indent626,24559 +(defun twelf-dsb twelf-dsb641,25183 +(defun twelf-mode-variables twelf-mode-variables667,26595 +(defun twelf-mode twelf-mode689,27408 +(defun twelf-info twelf-info904,35790 +(defconst twelf-error-regexptwelf-error-regexp918,36330 +(defconst twelf-error-fields-regexptwelf-error-fields-regexp922,36441 +(defconst twelf-error-decl-regexptwelf-error-decl-regexp928,36654 +(defun looked-at-nth looked-at-nth932,36803 +(defun looked-at-nth-int looked-at-nth-int938,36985 +(defun twelf-error-parser twelf-error-parser943,37100 +(defun twelf-error-decl twelf-error-decl957,37703 +(defun twelf-mark-relative twelf-mark-relative963,37882 +(defun twelf-mark-absolute twelf-mark-absolute979,38552 +(defun twelf-find-decl twelf-find-decl1004,39438 +(defun twelf-next-error twelf-next-error1019,39994 +(defun twelf-goto-error twelf-goto-error1087,42804 +(defun twelf-convert-standard-filename twelf-convert-standard-filename1101,43342 +(defun string-member string-member1113,43837 +(defun twelf-config-proceed-p twelf-config-proceed-p1125,44329 +(defun twelf-save-if-config twelf-save-if-config1132,44591 +(defun twelf-config-save-some-buffers twelf-config-save-some-buffers1145,45063 +(defun twelf-save-check-config twelf-save-check-config1149,45228 +(defun twelf-check-config twelf-check-config1164,45784 +(defun twelf-save-check-file twelf-save-check-file1176,46224 +(defun twelf-buffer-substring twelf-buffer-substring1192,46947 +(defun twelf-buffer-substring-dot twelf-buffer-substring-dot1198,47209 +(defun twelf-check-declaration twelf-check-declaration1204,47475 +(defun twelf-highlight-range-zmacs twelf-highlight-range-zmacs1227,48535 +(defun twelf-focus twelf-focus1233,48785 +(defun twelf-focus-noop twelf-focus-noop1239,49051 +(defun twelf-type-const twelf-type-const1322,52673 +(defvar twelf-server-mode-map twelf-server-mode-map1439,57815 +(defconst twelf-server-cd-regexp twelf-server-cd-regexp1451,58367 +(defun looked-at-string looked-at-string1454,58507 +(defun twelf-server-directory-tracker twelf-server-directory-tracker1458,58648 +(defun twelf-input-filter twelf-input-filter1480,59822 +(defun twelf-server-mode twelf-server-mode1486,60077 +(defun twelf-parse-config twelf-parse-config1519,61294 +(defun twelf-server-read-config twelf-server-read-config1537,62186 +(defun twelf-server-sync-config twelf-server-sync-config1546,62523 +(defun twelf-get-server-buffer twelf-get-server-buffer1576,64029 +(defun twelf-init-variables twelf-init-variables1593,64703 +(defun twelf-server twelf-server1600,64916 +(defun twelf-server-process twelf-server-process1642,66830 +(defun twelf-server-display twelf-server-display1651,67236 +(defun display-server-buffer display-server-buffer1658,67510 +(defun twelf-server-send-command twelf-server-send-command1673,68242 +(defun twelf-accept-process-output twelf-accept-process-output1694,69202 +(defun twelf-server-wait twelf-server-wait1703,69641 +(defun twelf-server-quit twelf-server-quit1745,71779 +(defun twelf-server-interrupt twelf-server-interrupt1750,71900 +(defun twelf-reset twelf-reset1755,72036 +(defun twelf-config-directory twelf-config-directory1760,72180 +(defun twelf-server-configure twelf-server-configure1771,72594 +(defun natp natp1844,75886 +(defun twelf-read-nat twelf-read-nat1848,75987 +(defun twelf-read-bool twelf-read-bool1857,76254 +(defun twelf-read-limit twelf-read-limit1863,76402 +(defun twelf-read-strategy twelf-read-strategy1873,76702 +(defun twelf-read-value twelf-read-value1879,76854 +(defun twelf-set twelf-set1883,77017 +(defun twelf-set-parm twelf-set-parm1896,77494 +(defun track-parm track-parm1905,77791 +(defun twelf-toggle-double-check twelf-toggle-double-check1910,77965 +(defun twelf-toggle-print-implicit twelf-toggle-print-implicit1916,78168 +(defun twelf-get twelf-get1922,78381 +(defun twelf-timers-reset twelf-timers-reset1936,79007 +(defun twelf-timers-show twelf-timers-show1941,79127 +(defun twelf-timers-check twelf-timers-check1947,79278 +(defun twelf-server-restart twelf-server-restart1953,79443 +(defun twelf-config-mode twelf-config-mode1969,80120 +(defun twelf-config-mode-check twelf-config-mode-check1985,80719 +(defun twelf-tag twelf-tag1994,81169 +(defun twelf-tag-files twelf-tag-files2022,82433 +(default: *tags-errors*)*tags-errors*2026,82736 +(defun twelf-tag-file twelf-tag-file2047,83487 +(defun twelf-next-decl twelf-next-decl2082,84709 +(defun skip-ahead skip-ahead2107,85731 +(defun current-line-absolute current-line-absolute2119,86153 +(defun new-temp-buffer new-temp-buffer2124,86363 +(defun rev-relativize rev-relativize2135,86747 +(defvar twelf-sml-mode-map twelf-sml-mode-map2149,87207 +(defconst twelf-sml-prompt-regexp twelf-sml-prompt-regexp2159,87585 +(defun expand-dir expand-dir2161,87640 +(defun twelf-sml-cd twelf-sml-cd2168,87901 +(defconst twelf-sml-cd-regexp twelf-sml-cd-regexp2180,88390 +(defun twelf-sml-directory-tracker twelf-sml-directory-tracker2183,88524 +(defun twelf-sml-mode twelf-sml-mode2199,89369 +(defun twelf-sml twelf-sml2250,91303 +(defun switch-to-twelf-sml switch-to-twelf-sml2270,92263 +(defun display-twelf-sml-buffer display-twelf-sml-buffer2281,92612 +(defun twelf-sml-send-string twelf-sml-send-string2297,93328 +(defun twelf-sml-send-region twelf-sml-send-region2302,93532 +(defun twelf-sml-send-query twelf-sml-send-query2326,94738 +(defun twelf-sml-send-newline twelf-sml-send-newline2336,95135 +(defun twelf-sml-send-semicolon twelf-sml-send-semicolon2344,95463 +(defun twelf-sml-status twelf-sml-status2352,95797 +(defvar twelf-sml-init twelf-sml-init2374,96744 +(defun twelf-sml-set-mode twelf-sml-set-mode2377,96921 +(defun twelf-sml-quit twelf-sml-quit2403,98098 +(defun twelf-sml-process-buffer twelf-sml-process-buffer2408,98210 +(defun twelf-sml-process twelf-sml-process2412,98326 +(defvar twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode2424,98842 +(defun install-twelf-to-twelf-sml-keybindings install-twelf-to-twelf-sml-keybindings2427,98927 +(defvar twelf-to-twelf-sml-mode-map twelf-to-twelf-sml-mode-map2437,99312 +(defun twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode2448,99825 +(defconst twelf-at-point-menutwelf-at-point-menu2498,101692 +(defconst twelf-server-state-menutwelf-server-state-menu2508,102064 +(defconst twelf-error-menutwelf-error-menu2518,102381 +(defconst twelf-tags-menutwelf-tags-menu2524,102525 +(defun twelf-toggle-server-display-commands twelf-toggle-server-display-commands2534,102810 +(defconst twelf-options-menutwelf-options-menu2537,102934 +(defconst twelf-timers-menutwelf-timers-menu2572,104672 +(defconst twelf-syntax-menutwelf-syntax-menu2585,105166 +(defun twelf-add-menu twelf-add-menu2612,106032 +(defun twelf-remove-menu twelf-remove-menu2616,106134 +(defun twelf-reset-menu twelf-reset-menu2620,106232 +(defun twelf-server-add-menu twelf-server-add-menu2647,107131 +(defun twelf-server-remove-menu twelf-server-remove-menu2651,107254 +(defun twelf-server-reset-menu twelf-server-reset-menu2655,107366 + +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,29 + function to to372,14916 + +doc/ProofGeneral.texi,5555 +@node TopTop160,4927 +@node PrefacePreface196,6032 +@node Latest news for 3.4Latest news for 3.4237,7225 +@node FutureFuture265,8459 +@node CreditsCredits301,9718 +@node Introducing Proof GeneralIntroducing Proof General396,13067 +@node Quick start guideQuick start guide451,15057 +@node Features of Proof GeneralFeatures of Proof General503,17475 +@node Supported proof assistantsSupported proof assistants592,21400 +@node Prerequisites for this manualPrerequisites for this manual637,23133 +@node Organization of this manualOrganization of this manual681,24759 +@node Basic Script ManagementBasic Script Management707,25586 +@node Walkthrough example in LEGOWalkthrough example in LEGO726,26182 +@node Proof scriptsProof scripts878,31233 +@node Script buffersScript buffers921,33353 +@node Locked queue and editing regionsLocked queue and editing regions943,33930 +@node Goal-save sequencesGoal-save sequences999,36077 +@node Active scripting bufferActive scripting buffer1036,37551 +@node Summary of Proof General buffersSummary of Proof General buffers1105,40971 +@node Script editing commandsScript editing commands1167,43645 +@node Script processing commandsScript processing commands1245,46409 +@node Proof assistant commandsProof assistant commands1373,51710 +@node Toolbar commandsToolbar commands1533,57273 +@node Interrupting during trace outputInterrupting during trace output1557,58202 +@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1596,60125 +@node Goals buffer commandsGoals buffer commands1610,60625 +@node Advanced Script ManagementAdvanced Script Management1700,64158 +@node Visibility of completed proofsVisibility of completed proofs1731,65312 +@node Switching between proof scriptsSwitching between proof scripts1786,67235 +@node View of processed files View of processed files 1823,69207 +@node Retracting across filesRetracting across files1883,72258 +@node Asserting across filesAsserting across files1896,72889 +@node Automatic multiple file handlingAutomatic multiple file handling1909,73455 +@node Escaping script managementEscaping script management1934,74489 +@node Experimental featuresExperimental features1992,76692 +@node Support for other PackagesSupport for other Packages2029,78062 +@node Syntax highlightingSyntax highlighting2061,78927 +@node X-Symbol supportX-Symbol support2100,80533 +@node Support for function menusSupport for function menus2159,83079 +@node Support for outline modeSupport for outline mode2188,84375 +@node Support for completionSupport for completion2207,85138 +@node Support for tagsSupport for tags2264,87299 +@node Customizing Proof GeneralCustomizing Proof General2316,89627 +@node Basic optionsBasic options2356,91297 +@node How to customizeHow to customize2380,92055 +@node Display customizationDisplay customization2431,94145 +@node User optionsUser options2516,97673 +@node Changing facesChanging faces2771,106746 +@node Tweaking configuration settingsTweaking configuration settings2846,109415 +@node Hints and TipsHints and Tips2903,111940 +@node Adding your own keybindingsAdding your own keybindings2922,112541 +@node Using file variablesUsing file variables2978,115074 +@node Using abbreviationsUsing abbreviations3031,116903 +@node LEGO Proof GeneralLEGO Proof General3094,118722 +@node LEGO specific commandsLEGO specific commands3135,120091 +@node LEGO tagsLEGO tags3155,120546 +@node LEGO customizationsLEGO customizations3165,120793 +@node Coq Proof GeneralCoq Proof General3197,121711 +@node Coq-specific commandsCoq-specific commands3212,122102 +@node Coq-specific variablesCoq-specific variables3234,122609 +@node Editing multiple proofsEditing multiple proofs3272,123769 +@node User-loaded tacticsUser-loaded tactics3296,124877 +@node Isabelle Proof GeneralIsabelle Proof General3364,127459 +@node Classic IsabelleClassic Isabelle3431,130629 +@node ML filesML files3447,131067 +@node Theory filesTheory files3518,133492 +@node General commands for IsabelleGeneral commands for Isabelle3572,135957 +@node Specific commands for IsabelleSpecific commands for Isabelle3584,136439 +@node Isabelle customizationsIsabelle customizations3613,137379 +@node Isabelle/IsarIsabelle/Isar3678,139477 +@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3699,140245 +@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3706,140499 +@node HOL Proof GeneralHOL Proof General3786,142743 +@node Obtaining and InstallingObtaining and Installing3828,144524 +@node Obtaining Proof GeneralObtaining Proof General3844,144932 +@node Installing Proof General from tarballInstalling Proof General from tarball3875,146149 +@node Installing Proof General from RPM packageInstalling Proof General from RPM package3900,146981 +@node Setting the names of binariesSetting the names of binaries3915,147389 +@node Notes for syssiesNotes for syssies3943,148317 +@node Known bugs and workaroundsKnown bugs and workarounds4016,151266 +@node ReferencesReferences4029,151673 +@node History of Proof GeneralHistory of Proof General4069,152697 +@node Old News for 3.0Old News for 3.04159,156774 +@node Old News for 3.1Old News for 3.14229,160468 +@node Old News for 3.2Old News for 3.24255,161640 +@node Old News for 3.3Old News for 3.34316,164643 +@node Function IndexFunction Index4343,165642 +@node Variable IndexVariable Index4347,165718 +@node Keystroke IndexKeystroke Index4351,165798 +@node Concept IndexConcept Index4355,165864 + +doc/PG-adapting.texi,3785 +@node TopTop157,4710 +@node IntroductionIntroduction194,5824 +@node FutureFuture235,7472 +@node CreditsCredits271,9063 +@node Beginning with a new proverBeginning with a new prover281,9355 +@node Overview of adding a new proverOverview of adding a new prover322,11304 +@node Demonstration instance and easy configurationDemonstration instance and easy configuration396,14632 +@node Major modes used by Proof GeneralMajor modes used by Proof General465,18023 +@node Menus and toolbar and user-level commandsMenus and toolbar and user-level commands538,21106 +@node Settings for generic user-level commandsSettings for generic user-level commands553,21652 +@node Menu configurationMenu configuration598,23388 +@node Toolbar configurationToolbar configuration622,24306 +@node Proof script settingsProof script settings680,26551 +@node Recognizing commands and commentsRecognizing commands and comments702,27131 +@node Recognizing proofsRecognizing proofs820,32562 +@node Recognizing other elementsRecognizing other elements923,36956 +@node Configuring undo behaviourConfiguring undo behaviour989,39895 +@node Nested proofsNested proofs1128,45238 +@node Safe (state-preserving) commandsSafe (state-preserving) commands1168,46865 +@node Activate scripting hookActivate scripting hook1191,47804 +@node Automatic multiple filesAutomatic multiple files1215,48668 +@node CompletionsCompletions1237,49515 +@node Proof shell settingsProof shell settings1277,50989 +@node Proof shell commandsProof shell commands1308,52271 +@node Script input to the shellScript input to the shell1466,58926 +@node Settings for matching various output from proof processSettings for matching various output from proof process1531,61816 +@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1661,67484 +@node Hooks and other settingsHooks and other settings1841,75568 +@node Goals buffer settingsGoals buffer settings1930,79134 +@node Splash screen settingsSplash screen settings2007,82237 +@node Global constantsGlobal constants2033,82995 +@node Handling multiple filesHandling multiple files2059,83839 +@node Configuring Font LockConfiguring Font Lock2197,90906 +@node Configuring X-SymbolConfiguring X-Symbol2240,92799 +@node Writing more lisp codeWriting more lisp code2300,95322 +@node Default values for generic settingsDefault values for generic settings2317,95967 +@node Adding prover-specific configurationsAdding prover-specific configurations2347,97050 +@node Useful variablesUseful variables2390,98320 +@node Useful functions and macrosUseful functions and macros2411,98825 +@node Internals of Proof GeneralInternals of Proof General2514,102640 +@node SpansSpans2542,103548 +@node Proof General site configurationProof General site configuration2555,103922 +@node Configuration variable mechanismsConfiguration variable mechanisms2635,107038 +@node Global variablesGlobal variables2753,112274 +@node Proof script modeProof script mode2823,114824 +@node Proof shell modeProof shell mode3083,126458 +@node DebuggingDebugging3497,142513 +@node Plans and ideasPlans and ideas3540,143408 +@node Proof by pointing and similar featuresProof by pointing and similar features3561,144130 +@node Granularity of atomic command sequencesGranularity of atomic command sequences3599,145788 +@node Browser mode for script files and theoriesBrowser mode for script files and theories3644,148013 +@node Demonstration InstantiationsDemonstration Instantiations3674,149044 +@node demoisa-easy.eldemoisa-easy.el3690,149475 +@node demoisa.eldemoisa.el3753,151713 +@node Function IndexFunction Index3921,157229 +@node Variable IndexVariable Index3925,157305 +@node Concept IndexConcept Index3934,157484 |