acl2/acl2.el,0 ccc/ccc.el,138 (defvar ccc-keywords nil)ccc-keywords17,587 (defvar ccc-tactics nil)ccc-tactics18,613 (defvar ccc-tacticals nil)ccc-tacticals19,638 coq/coq-abbrev.el,766 (defun holes-show-doc ()holes-show-doc12,313 (defun coq-local-vars-list-show-doc ()coq-local-vars-list-show-doc16,390 (defconst coq-tactics-menucoq-tactics-menu21,490 (defconst coq-tactics-abbrev-tablecoq-tactics-abbrev-table26,667 (defconst coq-tacticals-menucoq-tacticals-menu29,784 (defconst coq-tacticals-abbrev-tablecoq-tacticals-abbrev-table33,893 (defconst coq-commands-menucoq-commands-menu36,984 (defconst coq-commands-abbrev-tablecoq-commands-abbrev-table43,1207 (defconst coq-terms-menucoq-terms-menu46,1296 (defconst coq-terms-abbrev-tablecoq-terms-abbrev-table51,1434 (defun coq-install-abbrevs ()coq-install-abbrevs58,1628 (defpgdefault menu-entriesmenu-entries83,2604 (defpgdefault help-menu-entrieshelp-menu-entries148,4718 coq/coq-autotest.el,0 coq/coq-db.el,1218 (defconst coq-syntax-db nilcoq-syntax-db24,596 (defun coq-insert-from-db (db prompt)coq-insert-from-db70,2319 (defun coq-build-regexp-list-from-db (db &optional filter)coq-build-regexp-list-from-db88,3050 (defun coq-build-opt-regexp-from-db (db &optional filter)coq-build-opt-regexp-from-db107,3856 (defun max-length-db (db)max-length-db126,4677 (defun coq-build-menu-from-db-internal (db lgth menuwidth)coq-build-menu-from-db-internal138,4952 (defun coq-build-title-menu (db size)coq-build-title-menu175,6493 (defun coq-sort-menu-entries (menu)coq-sort-menu-entries184,6861 (defun coq-build-menu-from-db (db &optional size)coq-build-menu-from-db190,6988 (defcustom coq-holes-minor-mode tcoq-holes-minor-mode212,7827 (defun coq-build-abbrev-table-from-db (db)coq-build-abbrev-table-from-db218,7971 (defun filter-state-preserving (l)filter-state-preserving237,8609 (defun filter-state-changing (l)filter-state-changing242,8763 (defface coq-solve-tactics-facecoq-solve-tactics-face249,8984 (defface coq-cheat-facecoq-cheat-face258,9314 (defconst coq-solve-tactics-face 'coq-solve-tactics-facecoq-solve-tactics-face266,9562 (defconst coq-cheat-face 'coq-cheat-facecoq-cheat-face270,9726 coq/coq.el,13867 (defcustom coq-translate-to-v8 nilcoq-translate-to-v859,1804 (defun coq-build-prog-args ()coq-build-prog-args65,1984 (defcustom coq-compilercoq-compiler75,2278 (defcustom coq-dependency-analyzercoq-dependency-analyzer81,2415 (defcustom coq-compile-file-command (concat coq-compiler " %s")coq-compile-file-command87,2555 (defcustom coq-use-makefile nilcoq-use-makefile95,2892 (defcustom coq-default-undo-limit 200coq-default-undo-limit103,3115 (defconst coq-shell-init-cmdcoq-shell-init-cmd108,3243 (defcustom coq-prog-env nilcoq-prog-env116,3508 (defconst coq-shell-restart-cmd "Reset Initial.\n ")coq-shell-restart-cmd124,3758 (defvar coq-shell-prompt-patterncoq-shell-prompt-pattern126,3812 (defvar coq-shell-cd nilcoq-shell-cd134,4115 (defvar coq-shell-proof-completed-regexp "Subtree\\s-proved!\\|Proof\\s-completed"coq-shell-proof-completed-regexp138,4275 (defvar coq-goal-regexpcoq-goal-regexp141,4430 (defun get-coq-library-directory ()get-coq-library-directory146,4526 (defconst coq-library-directory (get-coq-library-directory)coq-library-directory152,4708 (defcustom coq-tags (concat coq-library-directory "/theories/TAGS")coq-tags155,4834 (defconst coq-interrupt-regexp "User Interrupt."coq-interrupt-regexp160,4982 (defcustom coq-www-home-page "http://coq.inria.fr/"coq-www-home-page163,5075 (defvar coq-outline-regexpcoq-outline-regexp174,5250 (defvar coq-outline-heading-end-regexp "\\.[ \t\n]")coq-outline-heading-end-regexp181,5462 (defvar coq-shell-outline-regexp coq-goal-regexp)coq-shell-outline-regexp183,5516 (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp)coq-shell-outline-heading-end-regexp184,5566 (defconst coq-state-preserving-tactics-regexpcoq-state-preserving-tactics-regexp187,5630 (defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp189,5732 (defconst coq-state-preserving-commands-regexpcoq-state-preserving-commands-regexp191,5841 (defconst coq-commands-regexpcoq-commands-regexp193,5954 (defvar coq-retractable-instruct-regexpcoq-retractable-instruct-regexp195,6033 (defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp197,6125 (defcustom coq-use-smie tcoq-use-smie229,6821 (defconst coq-smie-grammarcoq-smie-grammar237,7049 (defun coq-smie-rules (kind token)coq-smie-rules275,8870 (defun coq-set-undo-limit (undos)coq-set-undo-limit298,9601 (defun build-list-id-from-string (s)build-list-id-from-string302,9731 (defun coq-last-prompt-info (s)coq-last-prompt-info314,10229 (defun coq-last-prompt-info-safe ()coq-last-prompt-info-safe326,10761 (defvar coq-last-but-one-statenum 1coq-last-but-one-statenum332,11018 (defvar coq-last-but-one-proofnum 1coq-last-but-one-proofnum339,11316 (defvar coq-last-but-one-proofstack '()coq-last-but-one-proofstack342,11414 (defsubst coq-get-span-statenum (span)coq-get-span-statenum345,11524 (defsubst coq-get-span-proofnum (span)coq-get-span-proofnum349,11639 (defsubst coq-get-span-proofstack (span)coq-get-span-proofstack353,11754 (defsubst coq-set-span-statenum (span val)coq-set-span-statenum357,11898 (defsubst coq-get-span-goalcmd (span)coq-get-span-goalcmd361,12029 (defsubst coq-set-span-goalcmd (span val)coq-set-span-goalcmd365,12143 (defsubst coq-set-span-proofnum (span val)coq-set-span-proofnum369,12273 (defsubst coq-set-span-proofstack (span val)coq-set-span-proofstack373,12404 (defsubst proof-last-locked-span ()proof-last-locked-span377,12564 (defun proof-clone-buffer (s &optional erase)proof-clone-buffer381,12698 (defun proof-store-buffer-win (buffer &optional erase)proof-store-buffer-win395,13233 (defun proof-store-response-win (&optional erase)proof-store-response-win406,13726 (defun proof-store-goals-win (&optional erase)proof-store-goals-win410,13853 (defun coq-set-state-infos ()coq-set-state-infos422,14385 (defun count-not-intersection (l notin)count-not-intersection460,16472 (defun coq-find-and-forget (span)coq-find-and-forget490,17724 (defvar coq-current-goal 1coq-current-goal517,19032 (defun coq-goal-hyp ()coq-goal-hyp520,19097 (defun coq-state-preserving-p (cmd)coq-state-preserving-p533,19571 (defconst notation-print-kinds-tablenotation-print-kinds-table547,19885 (defun coq-PrintScope ()coq-PrintScope551,20052 (defun coq-guess-or-ask-for-string (s &optional dontguess)coq-guess-or-ask-for-string569,20601 (defun coq-ask-do (ask do &optional dontguess postformatcmd)coq-ask-do583,21141 (defsubst coq-put-into-brackets (s)coq-put-into-brackets592,21526 (defsubst coq-put-into-quotes (s) coq-put-into-quotes595,21587 (defun coq-SearchIsos ()coq-SearchIsos598,21647 (defun coq-SearchConstant ()coq-SearchConstant606,21888 (defun coq-Searchregexp ()coq-Searchregexp610,21981 (defun coq-SearchRewrite ()coq-SearchRewrite616,22124 (defun coq-SearchAbout ()coq-SearchAbout620,22221 (defun coq-Print () coq-Print626,22366 (defun coq-About () coq-About631,22491 (defun coq-LocateConstant ()coq-LocateConstant636,22611 (defun coq-LocateLibrary ()coq-LocateLibrary641,22714 (defun coq-LocateNotation ()coq-LocateNotation646,22831 (defun coq-Pwd ()coq-Pwd654,23063 (defun coq-Inspect ()coq-Inspect659,23187 (defun coq-PrintSection()coq-PrintSection663,23287 (defun coq-Print-implicit ()coq-Print-implicit667,23380 (defun coq-Check ()coq-Check672,23531 (defun coq-Show ()coq-Show677,23639 (defun coq-Compile ()coq-Compile691,24082 (defun coq-guess-command-line (filename)coq-guess-command-line703,24400 (defpacustom use-editing-holes tuse-editing-holes740,25953 (defun coq-mode-config ()coq-mode-config749,26256 (defun coq-shell-mode-config ()coq-shell-mode-config845,29749 (defun coq-goals-mode-config ()coq-goals-mode-config890,31577 (defun coq-response-config ()coq-response-config897,31821 (defpacustom print-fully-explicit nilprint-fully-explicit922,32646 (defpacustom print-implicit nilprint-implicit927,32794 (defpacustom print-coercions nilprint-coercions932,32960 (defpacustom print-match-wildcards tprint-match-wildcards937,33104 (defpacustom print-elim-types tprint-elim-types942,33284 (defpacustom printing-depth 50printing-depth947,33450 (defpacustom undo-depth coq-default-undo-limitundo-depth952,33611 (defpacustom time-commands niltime-commands957,33777 (defpacustom auto-compile-vos nilauto-compile-vos961,33887 (defun coq-maybe-compile-buffer ()coq-maybe-compile-buffer990,35001 (defun coq-ancestors-of (filename)coq-ancestors-of1026,36529 (defun coq-all-ancestors-of (filename)coq-all-ancestors-of1049,37493 (defun coq-process-require-command (span cmd)coq-process-require-command1060,37840 (defun coq-included-children (filename)coq-included-children1065,37967 (defun coq-process-file (rfilename)coq-process-file1086,38806 (defgroup coq-auto-compile ()coq-auto-compile1114,39791 (defcustom coq-compile-before-require nilcoq-compile-before-require1119,39942 (defcustom coq-compile-command ""coq-compile-command1128,40344 (defcustom coq-confirm-external-compilation-command tcoq-confirm-external-compilation-command1158,41652 (defconst coq-compile-substitution-listcoq-compile-substitution-list1164,41880 (defcustom coq-compile-auto-save 'ask-coqcoq-compile-auto-save1184,42801 (defcustom coq-lock-ancestors tcoq-lock-ancestors1209,43860 (defcustom coq-compile-ignore-library-directory tcoq-compile-ignore-library-directory1218,44175 (defcustom coq-compile-ignored-directories nilcoq-compile-ignored-directories1230,44659 (defcustom coq-load-path nilcoq-load-path1243,45293 (defcustom coq-load-path-include-current tcoq-load-path-include-current1258,45850 (defconst coq-require-command-regexpcoq-require-command-regexp1267,46169 (defconst coq-require-id-regexpcoq-require-id-regexp1274,46526 (defvar coq-compile-history nilcoq-compile-history1282,46960 (defun time-less-or-equal (time-1 time-2)time-less-or-equal1287,47064 (defun coq-max-dep-mod-time (dep-mod-times)coq-max-dep-mod-time1295,47402 (defun coq-prog-args ()coq-prog-args1318,48206 (defun coq-lock-ancestor (span ancestor-src)coq-lock-ancestor1327,48465 (defun coq-unlock-ancestor (ancestor-src)coq-unlock-ancestor1343,49240 (defun coq-unlock-all-ancestors-of-span (span)coq-unlock-all-ancestors-of-span1355,49733 (defun coq-compile-ignore-file (lib-obj-file)coq-compile-ignore-file1362,50029 (defun coq-library-src-of-obj-file (lib-obj-file)coq-library-src-of-obj-file1382,50810 (defun coq-include-options (file)coq-include-options1387,51042 (defun coq-get-library-dependencies (lib-src-file)coq-get-library-dependencies1406,51815 (defun coq-compile-library (src-file)coq-compile-library1435,53158 (defun coq-compile-library-if-necessary (max-dep-obj-time src obj)coq-compile-library-if-necessary1461,54263 (defun coq-make-lib-up-to-date (coq-obj-hash span lib-obj-file)coq-make-lib-up-to-date1506,56097 (defun coq-auto-compile-externally (span qualified-id absolute-module-obj-file)coq-auto-compile-externally1561,58526 (defun coq-map-module-id-to-obj-file (module-id)coq-map-module-id-to-obj-file1604,60688 (defun coq-check-module (coq-object-local-hash-symbol span module-id)coq-check-module1632,61873 (defvar coq-process-require-current-buffercoq-process-require-current-buffer1660,63310 (defun coq-compile-save-buffer-filter ()coq-compile-save-buffer-filter1666,63575 (defun coq-compile-save-some-buffers ()coq-compile-save-some-buffers1676,63989 (defun coq-preprocess-require-commands ()coq-preprocess-require-commands1698,64891 (defun coq-switch-buffer-kill-proof-shell ()coq-switch-buffer-kill-proof-shell1731,66453 (defun coq-preprocessing ()coq-preprocessing1751,67129 (defun coq-fake-constant-markup ()coq-fake-constant-markup1765,67584 (defun coq-create-span-menu (span idiom name)coq-create-span-menu1781,68189 (defconst module-kinds-tablemodule-kinds-table1799,68702 (defconst modtype-kinds-tablemodtype-kinds-table1803,68851 (defun coq-insert-section-or-module ()coq-insert-section-or-module1807,68980 (defconst reqkinds-kinds-tablereqkinds-kinds-table1828,69830 (defun coq-insert-requires ()coq-insert-requires1832,69974 (defun coq-end-Section ()coq-end-Section1845,70454 (defun coq-insert-intros ()coq-insert-intros1863,71032 (defun coq-insert-infoH-hook ()coq-insert-infoH-hook1875,71565 (defun coq-insert-as ()coq-insert-as1880,71773 (defun coq-insert-match ()coq-insert-match1897,72466 (defun coq-insert-solve-tactic ()coq-insert-solve-tactic1926,73636 (defun coq-insert-tactic ()coq-insert-tactic1932,73887 (defun coq-insert-tactical ()coq-insert-tactical1938,74089 (defun coq-insert-command ()coq-insert-command1944,74320 (defun coq-insert-term ()coq-insert-term1949,74485 (define-key coq-keymap [(control ?i)] 'coq-insert-intros)coq-keymap1954,74646 (define-key coq-keymap [(control ?m)] 'coq-insert-match)coq-keymap1955,74704 (define-key coq-keymap [(control ?()] 'coq-insert-section-or-module)coq-keymap1956,74761 (define-key coq-keymap [(control ?))] 'coq-end-Section)coq-keymap1957,74830 (define-key coq-keymap [(control ?s)] 'coq-Show)coq-keymap1958,74886 (define-key coq-keymap [(control ?t)] 'coq-insert-tactic)coq-keymap1959,74935 (define-key coq-keymap [(control ?T)] 'coq-insert-tactical)coq-keymap1960,74993 (define-key coq-keymap [(control ?r)] 'proof-store-response-win)coq-keymap1961,75053 (define-key coq-keymap [(control ?G)] 'proof-store-goals-win)coq-keymap1962,75118 (define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in ttycoq-keymap1965,75246 (define-key coq-keymap [(control ?\s)] 'coq-insert-term)coq-keymap1967,75320 (define-key coq-keymap [(control return)] 'coq-insert-command)coq-keymap1968,75377 (define-key coq-keymap [(control ?o)] 'coq-SearchIsos)coq-keymap1972,75502 (define-key coq-keymap [(control ?p)] 'coq-Print)coq-keymap1974,75558 (define-key coq-keymap [(control ?b)] 'coq-About)coq-keymap1975,75608 (define-key coq-keymap [(control ?a)] 'coq-SearchAbout)coq-keymap1976,75658 (define-key coq-keymap [(control ?c)] 'coq-Check)coq-keymap1977,75714 (define-key coq-keymap [(control ?H)] 'coq-PrintHint)coq-keymap1978,75764 (define-key coq-keymap [(control ?l)] 'coq-LocateConstant)coq-keymap1979,75818 (define-key coq-keymap [(control ?n)] 'coq-LocateNotation)coq-keymap1980,75877 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check)coq-goals-mode-map1983,75938 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?p)] 'coq-Print)coq-goals-mode-map1984,76020 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?o)] 'coq-SearchIsos)coq-goals-mode-map1985,76102 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?b)] 'coq-About)coq-goals-mode-map1986,76189 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-SearchAbout)coq-goals-mode-map1987,76271 (defvar last-coq-error-location nillast-coq-error-location1996,76573 (defun coq-get-last-error-location (&optional parseresp clean)coq-get-last-error-location2004,76957 (defun coq-highlight-error (&optional parseresp clean)coq-highlight-error2054,79520 (defun coq-highlight-error-hook ()coq-highlight-error-hook2082,80601 (defun first-word-of-buffer ()first-word-of-buffer2092,80818 (defun coq-show-first-goal ()coq-show-first-goal2100,81021 (defvar coq-modeline-string2 ")")coq-modeline-string22117,81716 (defvar coq-modeline-string1 ")")coq-modeline-string12118,81750 (defvar coq-modeline-string0 " Script(")coq-modeline-string02119,81784 (defun coq-build-subgoals-string (n)coq-build-subgoals-string2120,81825 (defun coq-update-minor-mode-alist ()coq-update-minor-mode-alist2125,81991 (defun is-not-split-vertic (selected-window)is-not-split-vertic2157,83385 (defun optim-resp-windows ()optim-resp-windows2166,83825 coq/coq-indent.el,4608 (defconst coq-any-command-regexpcoq-any-command-regexp20,368 (defconst coq-indent-inner-regexpcoq-indent-inner-regexp23,442 (defconst coq-comment-start-regexp "(\\*")coq-comment-start-regexp33,796 (defconst coq-comment-end-regexp "\\*)")coq-comment-end-regexp34,839 (defconst coq-comment-start-or-end-regexpcoq-comment-start-or-end-regexp35,880 (defconst coq-indent-open-regexpcoq-indent-open-regexp37,988 (defconst coq-indent-close-regexpcoq-indent-close-regexp42,1164 (defconst coq-indent-closepar-regexp "\\s)")coq-indent-closepar-regexp45,1275 (defconst coq-indent-closematch-regexp (proof-ids-to-regexp '("end")))coq-indent-closematch-regexp46,1320 (defconst coq-indent-openpar-regexp "\\s(")coq-indent-openpar-regexp47,1391 (defconst coq-indent-openmatch-regexp (proof-ids-to-regexp '("match" "Cases")))coq-indent-openmatch-regexp48,1435 (defconst coq-tacticals-tactics-regexcoq-tacticals-tactics-regex49,1515 (defconst coq-indent-any-regexpcoq-indent-any-regexp51,1634 (defconst coq-indent-kwcoq-indent-kw55,1850 (defconst coq-indent-pattern-regexp "\\(|\\(?:(\\|\\s-\\|\\w\\|\n\\)\\|with\\)")coq-indent-pattern-regexp65,2316 (defun coq-indent-goal-command-p (str)coq-indent-goal-command-p69,2419 (defconst coq-end-command-regexpcoq-end-command-regexp91,3470 (defun coq-search-comment-delimiter-forward ()coq-search-comment-delimiter-forward96,3622 (defun coq-search-comment-delimiter-backward ()coq-search-comment-delimiter-backward105,3952 (defun coq-skip-until-one-comment-backward ()coq-skip-until-one-comment-backward112,4226 (defun coq-skip-until-one-comment-forward ()coq-skip-until-one-comment-forward127,4933 (defun coq-looking-at-comment ()coq-looking-at-comment138,5451 (defun coq-find-comment-start ()coq-find-comment-start142,5592 (defun coq-find-comment-end ()coq-find-comment-end153,6025 (defun coq-looking-at-syntactic-context ()coq-looking-at-syntactic-context165,6518 (defconst coq-end-command-or-comment-regexpcoq-end-command-or-comment-regexp171,6740 (defconst coq-end-command-or-comment-start-regexpcoq-end-command-or-comment-start-regexp174,6849 (defun coq-find-not-in-comment-backward (reg &optional lim submatch)coq-find-not-in-comment-backward178,6967 (defun coq-find-not-in-comment-forward (reg &optional lim submatch)coq-find-not-in-comment-forward198,7868 (defun coq-find-command-end-backward ()coq-find-command-end-backward222,9007 (defun coq-find-command-end-forward ()coq-find-command-end-forward231,9398 (defun coq-find-command-end (direction)coq-find-command-end240,9775 (defun coq-find-current-start ()coq-find-current-start248,10107 (defun coq-find-real-start ()coq-find-real-start257,10398 (defun coq-command-at-point ()coq-command-at-point264,10617 (defun same-line (pt pt2)same-line272,10903 (defun coq-commands-at-line ()coq-commands-at-line275,10990 (defun coq-indent-only-spaces-on-line ()coq-indent-only-spaces-on-line294,11613 (defun coq-indent-find-reg (lim reg)coq-indent-find-reg300,11890 (defun coq-find-no-syntactic-on-line ()coq-find-no-syntactic-on-line314,12426 (defun coq-back-to-indentation-prevline ()coq-back-to-indentation-prevline327,12899 (defun coq-find-unclosed (&optional optlvl limit openreg closereg)coq-find-unclosed370,14785 (defun coq-find-at-same-level-zero (limit openreg)coq-find-at-same-level-zero400,16095 (defun coq-find-unopened (&optional optlvl limit)coq-find-unopened429,17361 (defun coq-find-last-unopened (&optional optlvl limit)coq-find-last-unopened472,18795 (defun coq-end-offset (&optional limit)coq-end-offset483,19192 (defun coq-add-iter (l f)coq-add-iter508,19962 (defun coq-goal-count (l) (coq-add-iter l 'coq-indent-goal-command-p))coq-goal-count511,20068 (defun coq-save-count (l) (coq-add-iter l '(lambda (x) (coq-save-command-p nil x))))coq-save-count513,20140 (defun coq-proof-count (l)coq-proof-count515,20226 (defun coq-goal-save-diff-maybe-proof (l)coq-goal-save-diff-maybe-proof519,20401 (defun coq-indent-command-offset (kind prevcol prevpoint)coq-indent-command-offset526,20622 (defun coq-indent-expr-offset (kind prevcol prevpoint record)coq-indent-expr-offset558,22225 (defun coq-indent-comment-offset ()coq-indent-comment-offset673,26909 (defun coq-indent-offset (&optional notcomments)coq-indent-offset705,28358 (defun coq-indent-calculate (&optional notcomments)coq-indent-calculate724,29233 (defun coq-indent-line ()coq-indent-line727,29321 (defun coq-indent-line-not-comments ()coq-indent-line-not-comments737,29687 (defun coq-indent-region (start end)coq-indent-region747,30076 coq/coq-local-vars.el,565 (defconst coq-local-vars-doc nilcoq-local-vars-doc20,429 (defun coq-insert-coq-prog-name (progname progargs)coq-insert-coq-prog-name78,2957 (defun coq-read-directory (prompt &optional default maynotmatch initialcontent)coq-read-directory89,3430 (defun coq-extract-directories-from-args (args)coq-extract-directories-from-args113,4533 (defun coq-ask-prog-args (&optional oldvalue)coq-ask-prog-args128,5085 (defun coq-ask-prog-name (&optional oldvalue)coq-ask-prog-name150,6153 (defun coq-ask-insert-coq-prog-name ()coq-ask-insert-coq-prog-name167,6864 coq/coq-mmm.el,0 coq/coq-syntax.el,4741 (defcustom coq-prog-name ;; da: moved from coq.el since needed herecoq-prog-name18,560 (defcustom coq-user-tactics-db nilcoq-user-tactics-db38,1342 (defcustom coq-user-commands-db nilcoq-user-commands-db55,1855 (defcustom coq-user-tacticals-db nilcoq-user-tacticals-db71,2374 (defcustom coq-user-solve-tactics-db nilcoq-user-solve-tactics-db87,2895 (defcustom coq-user-cheat-tactics-db nilcoq-user-cheat-tactics-db103,3414 (defcustom coq-user-reserved-db nilcoq-user-reserved-db122,3960 (defvar coq-tactics-dbcoq-tactics-db140,4491 (defvar coq-solve-tactics-dbcoq-solve-tactics-db298,12750 (defvar coq-solve-cheat-tactics-dbcoq-solve-cheat-tactics-db321,13595 (defvar coq-tacticals-dbcoq-tacticals-db333,13770 (defvar coq-decl-dbcoq-decl-db357,14656 (defvar coq-defn-dbcoq-defn-db382,16112 (defvar coq-goal-starters-dbcoq-goal-starters-db440,20467 (defvar coq-other-commands-dbcoq-other-commands-db469,22224 (defvar coq-commands-dbcoq-commands-db598,31690 (defvar coq-terms-dbcoq-terms-db605,31910 (defun coq-count-match (regexp strg)coq-count-match667,34525 (defun coq-module-opening-p (str)coq-module-opening-p683,35254 (defun coq-section-command-p (str)coq-section-command-p694,35665 (defun coq-goal-command-str-p (str)coq-goal-command-str-p698,35762 (defun coq-goal-command-p (span)coq-goal-command-p725,36864 (defvar coq-keywords-save-strictcoq-keywords-save-strict734,37147 (defvar coq-keywords-savecoq-keywords-save743,37260 (defun coq-save-command-p (span str)coq-save-command-p747,37338 (defvar coq-keywords-kill-goalcoq-keywords-kill-goal758,37666 (defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands762,37756 (defvar coq-keywords-goalcoq-keywords-goal765,37881 (defvar coq-keywords-declcoq-keywords-decl768,37964 (defvar coq-keywords-defncoq-keywords-defn771,38038 (defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands775,38113 (defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands784,38373 (defvar coq-keywords-commandscoq-keywords-commands789,38589 (defvar coq-solve-tacticscoq-solve-tactics794,38737 (defvar coq-solve-tactics-regexpcoq-solve-tactics-regexp798,38858 (defvar coq-solve-cheat-tacticscoq-solve-cheat-tactics802,38992 (defvar coq-solve-cheat-tactics-regexpcoq-solve-cheat-tactics-regexp806,39137 (defvar coq-tacticalscoq-tacticals810,39295 (defvar coq-reservedcoq-reserved816,39434 (defvar coq-reserved-regexp (proof-ids-to-regexp coq-reserved))coq-reserved-regexp826,39761 (defvar coq-state-changing-tacticscoq-state-changing-tactics828,39826 (defvar coq-state-preserving-tacticscoq-state-preserving-tactics831,39935 (defvar coq-tacticscoq-tactics835,40049 (defvar coq-tactics-regexp (coq-build-opt-regexp-from-db coq-tactics-db))coq-tactics-regexp838,40138 (defvar coq-retractable-instructcoq-retractable-instruct841,40293 (defvar coq-non-retractable-instructcoq-non-retractable-instruct844,40403 (defvar coq-keywordscoq-keywords848,40531 (defun proof-regexp-alt-list-symb (args)proof-regexp-alt-list-symb854,40755 (defvar coq-keywords-regexp (proof-regexp-alt-list coq-keywords))coq-keywords-regexp857,40860 (defvar coq-symbolscoq-symbols860,40928 (defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"coq-error-regexp879,41141 (defvar coq-id proof-id)coq-id882,41369 (defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)")coq-id-shy883,41394 (defvar coq-ids (concat proof-id "\\(" "\\s-+" proof-id "\\)*"))coq-ids886,41496 (defun coq-first-abstr-regexp (paren end)coq-first-abstr-regexp888,41562 (defcustom coq-variable-highlight-enable tcoq-variable-highlight-enable891,41657 (defvar coq-font-lock-termscoq-font-lock-terms897,41784 (defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict919,42867 (defconst coq-save-command-regexpcoq-save-command-regexp925,43037 (defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp930,43192 (defconst coq-goal-command-regexpcoq-goal-command-regexp934,43352 (defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp937,43454 (defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp941,43588 (defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp948,43838 (defconst coq-with-with-hole-regexpcoq-with-with-hole-regexp958,44128 (defvar coq-font-lock-keywords-1coq-font-lock-keywords-1973,44658 (defvar coq-font-lock-keywords coq-font-lock-keywords-1)coq-font-lock-keywords1001,45993 (defun coq-init-syntax-table ()coq-init-syntax-table1003,46051 (defconst coq-generic-expressioncoq-generic-expression1028,46778 coq/coq-unicode-tokens.el,781 (defconst coq-token-format "%s") ; plain tokenscoq-token-format39,1427 (defconst coq-token-match nil)coq-token-match40,1475 (defconst coq-hexcode-match nil)coq-hexcode-match41,1506 (defun coq-unicode-tokens-set (sym val)coq-unicode-tokens-set43,1540 (defcustom coq-token-symbol-mapcoq-token-symbol-map49,1768 (defcustom coq-shortcut-alistcoq-shortcut-alist165,4719 (defconst coq-control-char-format-regexpcoq-control-char-format-regexp254,6737 (defconst coq-control-char-format " %s ")coq-control-char-format258,6862 (defconst coq-control-characterscoq-control-characters260,6905 (defconst coq-control-region-format-regexp "\\(\s*%s\{\\)\\([^}]*\\)\\(\}\s*\\)")coq-control-region-format-regexp264,6997 (defconst coq-control-regionscoq-control-regions266,7080 hol98/hol98.el,194 (defvar hol98-keywords nil)hol98-keywords17,419 (defvar hol98-rules nil)hol98-rules18,447 (defvar hol98-tactics nil)hol98-tactics19,472 (defvar hol98-tacticals nil)hol98-tacticals20,499 isar/interface-setup.el,0 isar/isabelle-system.el,2188 (defgroup isabelle nilisabelle28,797 (defcustom isabelle-web-pageisabelle-web-page32,925 (defcustom isa-isabelle-commandisa-isabelle-command41,1142 (defvar isabelle-not-found nilisabelle-not-found59,1824 (defun isa-set-isabelle-command (&optional force)isa-set-isabelle-command62,1939 (defun isa-shell-command-to-string (command)isa-shell-command-to-string85,2957 (defun isa-getenv (envvar &optional default)isa-getenv91,3181 (defcustom isabelle-program-name-override nilisabelle-program-name-override111,3880 (defun isa-tool-list-logics ()isa-tool-list-logics122,4226 (defcustom isabelle-logics-available nilisabelle-logics-available129,4472 (defcustom isabelle-chosen-logic nilisabelle-chosen-logic139,4809 (defvar isabelle-chosen-logic-prev nilisabelle-chosen-logic-prev155,5393 (defun isabelle-hack-local-variables-function ()isabelle-hack-local-variables-function158,5513 (defun isabelle-set-prog-name (&optional filename)isabelle-set-prog-name170,5952 (defun isabelle-choose-logic (logic)isabelle-choose-logic194,7072 (defun isa-view-doc (docname)isa-view-doc213,7834 (defun isa-tool-list-docs ()isa-tool-list-docs220,8060 (defconst isabelle-verbatim-regexp "\\`\^VERBATIM: \\(\\(.\\|\n\\)*\\)\\'"isabelle-verbatim-regexp238,8790 (defun isabelle-verbatim (str)isabelle-verbatim241,8932 (defcustom isabelle-refresh-logics tisabelle-refresh-logics248,9093 (defvar isabelle-docs-menuisabelle-docs-menu256,9421 (defvar isabelle-logics-menu-entries nilisabelle-logics-menu-entries263,9706 (defun isabelle-logics-menu-calculate ()isabelle-logics-menu-calculate266,9779 (defvar isabelle-time-to-refresh-logics tisabelle-time-to-refresh-logics287,10421 (defun isabelle-logics-menu-refresh ()isabelle-logics-menu-refresh291,10516 (defun isabelle-menu-bar-update-logics ()isabelle-menu-bar-update-logics306,11149 (defun isabelle-load-isar-keywords (&optional kw)isabelle-load-isar-keywords322,11778 (defun isabelle-create-span-menu (span idiom name)isabelle-create-span-menu343,12506 (defun isabelle-xml-sml-escapes (xmlstring)isabelle-xml-sml-escapes359,12937 (defun isabelle-process-pgip (xmlstring)isabelle-process-pgip362,13038 isar/isar-autotest.el,50 (defvar isar-long-tests nilisar-long-tests8,186 isar/isar.el,2692 (defcustom isar-keywords-name nilisar-keywords-name39,915 (defpgdefault completion-table isar-keywords-major)completion-table55,1426 (defcustom isar-web-pageisar-web-page57,1479 (defun isar-strip-terminators ()isar-strip-terminators71,1829 (defun isar-markup-ml (string)isar-markup-ml83,2185 (defun isar-mode-config-set-variables ()isar-mode-config-set-variables88,2320 (defun isar-shell-mode-config-set-variables ()isar-shell-mode-config-set-variables153,5119 (defun isar-set-proof-find-theorems-command ()isar-set-proof-find-theorems-command235,8305 (defpacustom use-find-theorems-form niluse-find-theorems-form241,8489 (defun isar-set-undo-commands (&optional initp)isar-set-undo-commands246,8655 (defpacustom use-linear-undo tuse-linear-undo261,9288 (defun isar-configure-from-settings ()isar-configure-from-settings266,9446 (defun isar-remove-file (name files cmp-base)isar-remove-file274,9596 (defun isar-shell-compute-new-files-list ()isar-shell-compute-new-files-list286,9900 (define-derived-mode isar-shell-mode proof-shell-modeisar-shell-mode305,10470 (define-derived-mode isar-response-mode proof-response-modeisar-response-mode310,10597 (define-derived-mode isar-goals-mode proof-goals-modeisar-goals-mode315,10730 (define-derived-mode isar-mode proof-modeisar-mode320,10856 (defpgdefault menu-entriesmenu-entries372,12571 (defun isar-set-command ()isar-set-command403,13765 (defpgdefault help-menu-entries isabelle-docs-menu)help-menu-entries408,13895 (defun isar-count-undos (span)isar-count-undos411,13971 (defun isar-find-and-forget (span)isar-find-and-forget437,14937 (defun isar-goal-command-p (span)isar-goal-command-p473,16280 (defun isar-global-save-command-p (span str)isar-global-save-command-p478,16457 (defvar isar-current-goal 1isar-current-goal499,17241 (defun isar-state-preserving-p (cmd)isar-state-preserving-p502,17307 (defvar isar-shell-current-line-width nilisar-shell-current-line-width527,18156 (defun isar-shell-adjust-line-width ()isar-shell-adjust-line-width532,18348 (defsubst isar-string-wrapping (string)isar-string-wrapping555,19113 (defsubst isar-positions-of (filename start end)isar-positions-of564,19307 (defcustom isar-wrap-commands-singly tisar-wrap-commands-singly570,19512 (defun isar-command-wrapping (filename start end string)isar-command-wrapping576,19708 (defun isar-preprocessing ()isar-preprocessing584,20022 (defun isar-mode-config ()isar-mode-config602,20573 (defun isar-shell-mode-config ()isar-shell-mode-config616,21226 (defun isar-response-mode-config ()isar-response-mode-config626,21575 (defun isar-goals-mode-config ()isar-goals-mode-config636,21910 isar/isar-find-theorems.el,1360 (defvar isar-find-theorems-data (listisar-find-theorems-data19,565 (defun isar-find-theorems-minibuffer ()isar-find-theorems-minibuffer35,1039 (defun isar-find-theorems-form ()isar-find-theorems-form49,1658 (defvar isar-find-theorems-widget-number nilisar-find-theorems-widget-number92,3532 (defvar isar-find-theorems-widget-pattern nilisar-find-theorems-widget-pattern95,3630 (defvar isar-find-theorems-widget-intro nilisar-find-theorems-widget-intro98,3722 (defvar isar-find-theorems-widget-elim nilisar-find-theorems-widget-elim101,3808 (defvar isar-find-theorems-widget-dest nilisar-find-theorems-widget-dest104,3892 (defvar isar-find-theorems-widget-name nilisar-find-theorems-widget-name107,3976 (defvar isar-find-theorems-widget-simp nilisar-find-theorems-widget-simp110,4063 (defun isar-find-theorems-create-searchformisar-find-theorems-create-searchform115,4209 (defun isar-find-theorems-create-help ()isar-find-theorems-create-help255,8752 (defun isar-find-theorems-submit-searchformisar-find-theorems-submit-searchform298,10924 (defun isar-find-theorems-parse-criteria (option-string criteria-string)isar-find-theorems-parse-criteria376,13294 (defun isar-find-theorems-parse-number (num)isar-find-theorems-parse-number469,16275 (defun isar-find-theorems-filter-empty (strings)isar-find-theorems-filter-empty479,16552 isar/isar-keywords.el,1662 (defconst isar-keywords-majorisar-keywords-major7,222 (defconst isar-keywords-minorisar-keywords-minor280,4856 (defconst isar-keywords-controlisar-keywords-control339,5659 (defconst isar-keywords-diagisar-keywords-diag360,6153 (defconst isar-keywords-theory-beginisar-keywords-theory-begin434,7438 (defconst isar-keywords-theory-switchisar-keywords-theory-switch437,7491 (defconst isar-keywords-theory-endisar-keywords-theory-end440,7537 (defconst isar-keywords-theory-headingisar-keywords-theory-heading443,7585 (defconst isar-keywords-theory-declisar-keywords-theory-decl449,7692 (defconst isar-keywords-theory-scriptisar-keywords-theory-script552,9481 (defconst isar-keywords-theory-goalisar-keywords-theory-goal555,9544 (defconst isar-keywords-qedisar-keywords-qed583,10059 (defconst isar-keywords-qed-blockisar-keywords-qed-block590,10145 (defconst isar-keywords-qed-globalisar-keywords-qed-global593,10192 (defconst isar-keywords-proof-headingisar-keywords-proof-heading596,10241 (defconst isar-keywords-proof-goalisar-keywords-proof-goal601,10324 (defconst isar-keywords-proof-blockisar-keywords-proof-block606,10401 (defconst isar-keywords-proof-openisar-keywords-proof-open610,10463 (defconst isar-keywords-proof-closeisar-keywords-proof-close613,10509 (defconst isar-keywords-proof-chainisar-keywords-proof-chain616,10556 (defconst isar-keywords-proof-declisar-keywords-proof-decl623,10659 (defconst isar-keywords-proof-asmisar-keywords-proof-asm635,10821 (defconst isar-keywords-proof-asm-goalisar-keywords-proof-asm-goal642,10916 (defconst isar-keywords-proof-scriptisar-keywords-proof-script648,11005 isar/isar-mmm.el,127 (defconst isar-start-latex-regexpisar-start-latex-regexp24,744 (defconst isar-start-sml-regexpisar-start-sml-regexp36,1172 isar/isar-profiling.el,0 isar/isar-syntax.el,6862 (defconst isar-script-syntax-table-entriesisar-script-syntax-table-entries18,489 (defconst isar-script-syntax-table-alistisar-script-syntax-table-alist42,891 (defun isar-init-syntax-table ()isar-init-syntax-table51,1174 (defun isar-init-output-syntax-table ()isar-init-output-syntax-table59,1421 (defconst isar-keyword-begin "begin")isar-keyword-begin74,1863 (defconst isar-keyword-end "end")isar-keyword-end75,1901 (defconst isar-keywords-theory-encloseisar-keywords-theory-enclose77,1936 (defconst isar-keywords-theoryisar-keywords-theory82,2074 (defconst isar-keywords-saveisar-keywords-save87,2205 (defconst isar-keywords-proof-encloseisar-keywords-proof-enclose92,2320 (defconst isar-keywords-proofisar-keywords-proof98,2481 (defconst isar-keywords-proof-contextisar-keywords-proof-context105,2658 (defconst isar-keywords-local-goalisar-keywords-local-goal109,2765 (defconst isar-keywords-properisar-keywords-proper113,2870 (defconst isar-keywords-improperisar-keywords-improper118,2989 (defconst isar-keyword-level-alistisar-keyword-level-alist123,3121 (defconst isar-keywords-outline isar-keywords-outline138,3592 (defconst isar-keywords-indent-openisar-keywords-indent-open141,3668 (defconst isar-keywords-indent-closeisar-keywords-indent-close148,3854 (defconst isar-keywords-indent-encloseisar-keywords-indent-enclose153,3987 (defconst isar-ext-first "\\(?:\\\\<\\^?[A-Za-z]+>\\|[A-Za-z]\\)")isar-ext-first163,4216 (defconst isar-ext-rest "\\(?:\\\\<\\^?[A-Za-z]+>\\|[A-Za-z0-9'_]\\)")isar-ext-rest164,4283 (defconst isar-long-id-stuff (concat "\\(?:" isar-ext-rest "\\|\\.\\)+"))isar-long-id-stuff166,4355 (defconst isar-id (concat "\\(" isar-ext-first isar-ext-rest "*\\)"))isar-id167,4429 (defconst isar-idx (concat isar-id "\\(?:\\.[0-9]+\\)?"))isar-idx168,4499 (defconst isar-string "\"\\(\\(?:[^\"]\\|\\\\\"\\)*\\)\"")isar-string170,4558 (defun isar-ids-to-regexp (ids)isar-ids-to-regexp172,4618 (defconst isar-any-command-regexpisar-any-command-regexp204,6410 (defconst isar-name-regexpisar-name-regexp211,6783 (defconst isar-improper-regexpisar-improper-regexp217,7078 (defconst isar-save-command-regexpisar-save-command-regexp221,7226 (defconst isar-global-save-command-regexpisar-global-save-command-regexp224,7327 (defconst isar-goal-command-regexpisar-goal-command-regexp227,7441 (defconst isar-local-goal-command-regexpisar-local-goal-command-regexp230,7549 (defconst isar-comment-start "(*")isar-comment-start233,7662 (defconst isar-comment-end "*)")isar-comment-end234,7697 (defconst isar-comment-start-regexp (regexp-quote isar-comment-start))isar-comment-start-regexp235,7730 (defconst isar-comment-end-regexp (regexp-quote isar-comment-end))isar-comment-end-regexp236,7801 (defconst isar-string-start-regexp "\"\\|`\\|{\\*")isar-string-start-regexp238,7869 (defconst isar-string-end-regexp "\"\\|`\\|\\*}")isar-string-end-regexp239,7921 (defun isar-syntactic-context ()isar-syntactic-context241,7972 (defconst isar-antiq-regexpisar-antiq-regexp256,8367 (defconst isar-nesting-regexpisar-nesting-regexp262,8518 (defun isar-nesting ()isar-nesting265,8616 (defun isar-match-nesting (limit)isar-match-nesting277,9009 (defface isabelle-string-face isabelle-string-face289,9343 (defface isabelle-quote-face isabelle-quote-face297,9543 (defface isabelle-class-name-faceisabelle-class-name-face305,9739 (defface isabelle-tfree-name-faceisabelle-tfree-name-face313,9926 (defface isabelle-tvar-name-faceisabelle-tvar-name-face321,10119 (defface isabelle-free-name-faceisabelle-free-name-face329,10311 (defface isabelle-bound-name-faceisabelle-bound-name-face337,10499 (defface isabelle-var-name-faceisabelle-var-name-face345,10690 (defconst isabelle-string-face 'isabelle-string-face)isabelle-string-face353,10881 (defconst isabelle-quote-face 'isabelle-quote-face)isabelle-quote-face354,10935 (defconst isabelle-class-name-face 'isabelle-class-name-face)isabelle-class-name-face355,10988 (defconst isabelle-tfree-name-face 'isabelle-tfree-name-face)isabelle-tfree-name-face356,11050 (defconst isabelle-tvar-name-face 'isabelle-tvar-name-face)isabelle-tvar-name-face357,11112 (defconst isabelle-free-name-face 'isabelle-free-name-face)isabelle-free-name-face358,11173 (defconst isabelle-bound-name-face 'isabelle-bound-name-face)isabelle-bound-name-face359,11234 (defconst isabelle-var-name-face 'isabelle-var-name-face)isabelle-var-name-face360,11296 (defun isar-font-lock-fontify-syntactically-region isar-font-lock-fontify-syntactically-region366,11445 (defvar isar-font-lock-keywords-1isar-font-lock-keywords-1401,12721 (defun isar-output-flkprops (start regexp end props)isar-output-flkprops419,13729 (defun isar-output-flk (start regexp end face)isar-output-flk425,13981 (defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1428,14090 (defun isar-strip-output-markup (string)isar-strip-output-markup464,15513 (defconst isar-shell-font-lock-keywordsisar-shell-font-lock-keywords468,15649 (defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords471,15733 (defconst isar-linear-undo "linear_undo")isar-linear-undo505,16412 (defconst isar-undo "ProofGeneral.undo;")isar-undo507,16455 (defconst isar-prisar-pr509,16498 (defun isar-remove (name)isar-remove516,16656 (defun isar-undos (linearp i)isar-undos519,16731 (defun isar-cannot-undo (cmd)isar-cannot-undo529,16965 (defconst isar-undo-commandsisar-undo-commands532,17035 (defconst isar-theory-start-regexpisar-theory-start-regexp540,17172 (defconst isar-end-regexpisar-end-regexp546,17330 (defconst isar-undo-fail-regexpisar-undo-fail-regexp550,17431 (defconst isar-undo-skip-regexpisar-undo-skip-regexp554,17535 (defconst isar-undo-ignore-regexpisar-undo-ignore-regexp557,17656 (defconst isar-undo-remove-regexpisar-undo-remove-regexp560,17721 (defconst isar-keywords-imenuisar-keywords-imenu568,17878 (defconst isar-entity-regexp isar-entity-regexp575,18069 (defconst isar-named-entity-regexpisar-named-entity-regexp578,18165 (defconst isar-named-entity-name-match-numberisar-named-entity-name-match-number583,18295 (defconst isar-generic-expressionisar-generic-expression586,18396 (defconst isar-indent-any-regexpisar-indent-any-regexp597,18630 (defconst isar-indent-inner-regexpisar-indent-inner-regexp599,18723 (defconst isar-indent-enclose-regexpisar-indent-enclose-regexp601,18789 (defconst isar-indent-open-regexpisar-indent-open-regexp603,18905 (defconst isar-indent-close-regexpisar-indent-close-regexp605,19015 (defconst isar-outline-regexpisar-outline-regexp611,19152 (defconst isar-outline-heading-end-regexp "\n")isar-outline-heading-end-regexp615,19305 (defconst isar-outline-heading-alist isar-keyword-level-alist)isar-outline-heading-alist617,19354 isar/isar-unicode-tokens.el,2310 (defgroup isabelle-tokens nilisabelle-tokens25,672 (defun isar-set-and-restart-tokens (sym val)isar-set-and-restart-tokens30,812 (defconst isar-control-region-format-regexpisar-control-region-format-regexp43,1165 (defconst isar-control-char-format-regexpisar-control-char-format-regexp46,1259 (defconst isar-control-char-format "\\<^%s>")isar-control-char-format52,1406 (defconst isar-control-region-format-start "\\<^%s>")isar-control-region-format-start53,1455 (defconst isar-control-region-format-end "\\<^%s>")isar-control-region-format-end54,1509 (defcustom isar-control-charactersisar-control-characters57,1565 (defcustom isar-control-regionsisar-control-regions71,1978 (defconst isar-token-format "\\<%s>")isar-token-format97,2790 (defconst isar-token-variant-format-regexpisar-token-variant-format-regexp101,2941 (defcustom isar-greek-letters-tokensisar-greek-letters-tokens104,3055 (defcustom isar-misc-letters-tokensisar-misc-letters-tokens144,3913 (defcustom isar-symbols-tokensisar-symbols-tokens156,4231 (defcustom isar-extended-symbols-tokensisar-extended-symbols-tokens362,9042 (defun isar-try-char (charset code1 code2)isar-try-char431,10697 (defcustom isar-symbols-tokens-fallbacksisar-symbols-tokens-fallbacks435,10841 (defcustom isar-bold-nums-tokensisar-bold-nums-tokens462,11771 (defun isar-map-letters (f1 f2 &rest symbs)isar-map-letters478,12160 (defconst isar-script-letters-tokens ; \ \ ...isar-script-letters-tokens484,12308 (defconst isar-roman-letters-tokens ; \ \ ...isar-roman-letters-tokens489,12462 (defconst isar-fraktur-uppercase-letters-tokens ; \ \ ..isar-fraktur-uppercase-letters-tokens494,12636 (defconst isar-fraktur-lowercase-letters-tokens ; \ \ ..isar-fraktur-lowercase-letters-tokens499,12805 (defcustom isar-token-symbol-map nilisar-token-symbol-map504,12996 (defcustom isar-user-tokens nilisar-user-tokens521,13537 (defun isar-init-token-symbol-map ()isar-init-token-symbol-map535,13977 (defcustom isar-symbol-shortcutsisar-symbol-shortcuts560,14626 (defcustom isar-shortcut-alist nilisar-shortcut-alist632,16825 (defun isar-init-shortcut-alists ()isar-init-shortcut-alists640,17084 (defconst isar-tokens-customizable-variablesisar-tokens-customizable-variables661,17747 lego/lego.el,2849 (defcustom lego-tags "/usr/lib/lego/lib_Type/"lego-tags21,534 (defcustom lego-test-all-name "test_all"lego-test-all-name26,670 (defpgdefault help-menu-entrieshelp-menu-entries32,828 (defpgdefault menu-entriesmenu-entries36,988 (defvar lego-shell-handle-outputlego-shell-handle-output47,1289 (defconst lego-process-configlego-process-config55,1587 (defconst lego-pretty-set-width "Configure PrettyWidth %s; "lego-pretty-set-width66,2018 (defconst lego-interrupt-regexp "Interrupt.."lego-interrupt-regexp70,2160 (defcustom lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/"lego-www-home-page75,2277 (defcustom lego-www-latest-releaselego-www-latest-release80,2401 (defcustom lego-www-refcardlego-www-refcard86,2576 (defcustom lego-library-www-pagelego-library-www-page92,2725 (defvar lego-prog-name "lego"lego-prog-name101,2941 (defvar lego-shell-cd "Cd \"%s\";"lego-shell-cd104,3010 (defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*"lego-shell-proof-completed-regexp107,3109 (defvar lego-save-command-regexplego-save-command-regexp110,3249 (defvar lego-goal-command-regexplego-goal-command-regexp112,3339 (defvar lego-kill-goal-command "KillRef;")lego-kill-goal-command115,3430 (defvar lego-forget-id-command "Forget %s;")lego-forget-id-command116,3473 (defvar lego-undoable-commands-regexplego-undoable-commands-regexp118,3519 (defvar lego-goal-regexp "\\?\\([0-9]+\\)")lego-goal-regexp127,3893 (defvar lego-outline-regexplego-outline-regexp129,3938 (defvar lego-outline-heading-end-regexp ";\\|\\*)")lego-outline-heading-end-regexp135,4113 (defvar lego-shell-outline-regexp lego-goal-regexp)lego-shell-outline-regexp137,4166 (defvar lego-shell-outline-heading-end-regexp lego-goal-regexp)lego-shell-outline-heading-end-regexp138,4218 (define-derived-mode lego-shell-mode proof-shell-modelego-shell-mode144,4497 (define-derived-mode lego-mode proof-modelego-mode151,4658 (define-derived-mode lego-goals-mode proof-goals-modelego-goals-mode162,4968 (defun lego-count-undos (span)lego-count-undos173,5394 (defun lego-goal-command-p (span)lego-goal-command-p192,6131 (defun lego-find-and-forget (span)lego-find-and-forget197,6302 (defun lego-goal-hyp ()lego-goal-hyp239,8138 (defun lego-state-preserving-p (cmd)lego-state-preserving-p248,8335 (defvar lego-shell-current-line-width nillego-shell-current-line-width264,9038 (defun lego-shell-adjust-line-width ()lego-shell-adjust-line-width272,9345 (defun lego-mode-config ()lego-mode-config289,10046 (defun lego-equal-module-filename (module filename)lego-equal-module-filename357,12097 (defun lego-shell-compute-new-files-list ()lego-shell-compute-new-files-list363,12372 (defun lego-shell-mode-config ()lego-shell-mode-config373,12755 (defun lego-goals-mode-config ()lego-goals-mode-config420,14422 lego/lego-syntax.el,1148 (defconst lego-keywords-goal '("$?Goal"))lego-keywords-goal15,358 (defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen"))lego-keywords-save17,401 (defconst lego-commandslego-commands19,472 (defconst lego-keywordslego-keywords31,1030 (defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For"))lego-tacticals36,1207 (defconst lego-error-regexp "^\\(cannot assume\\|Error\\|Lego parser\\)"lego-error-regexp39,1315 (defvar lego-id proof-id)lego-id42,1473 (defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*")lego-ids44,1500 (defconst lego-arg-list-regexp "\\s *\\(\\[[^]]+\\]\\s *\\)*"lego-arg-list-regexp48,1696 (defun lego-decl-defn-regexp (char)lego-decl-defn-regexp51,1812 (defconst lego-definiendum-alternative-regexplego-definiendum-alternative-regexp59,2184 (defvar lego-font-lock-termslego-font-lock-terms63,2368 (defconst lego-goal-with-hole-regexplego-goal-with-hole-regexp89,3221 (defconst lego-save-with-hole-regexplego-save-with-hole-regexp94,3443 (defvar lego-font-lock-keywords-1lego-font-lock-keywords-199,3660 (defun lego-init-syntax-table ()lego-init-syntax-table110,4122 pgshell/pgshell.el,0 phox/phox.el,849 (defcustom phox-prog-name "phox -pg"phox-prog-name32,916 (defcustom phox-web-pagephox-web-page37,1018 (defcustom phox-doc-dirphox-doc-dir43,1168 (defcustom phox-lib-dirphox-lib-dir49,1315 (defcustom phox-tags-programphox-tags-program55,1458 (defcustom phox-tags-docphox-tags-doc61,1637 (defcustom phox-etagsphox-etags67,1774 (defpgdefault menu-entriesmenu-entries88,2224 (defun phox-config ()phox-config102,2417 (defun phox-shell-config ()phox-shell-config146,4343 (define-derived-mode phox-mode proof-modephox-mode170,5205 (define-derived-mode phox-shell-mode proof-shell-modephox-shell-mode186,5668 (define-derived-mode phox-response-mode proof-response-modephox-response-mode191,5796 (define-derived-mode phox-goals-mode proof-goals-modephox-goals-mode201,6157 (defpgdefault completion-tablecompletion-table224,6943 phox/phox-extraction.el,672 (defvar phox-prog-orig "phox -pg" "original name of phox binary.")phox-prog-orig19,619 (defun phox-prog-flags-modify(option)phox-prog-flags-modify21,687 (defun phox-prog-flags-extract()phox-prog-flags-extract50,1488 (defun phox-prog-flags-erase()phox-prog-flags-erase61,1778 (defun phox-toggle-extraction()phox-toggle-extraction69,1974 (defun phox-compile-theorem(name)phox-compile-theorem81,2376 (defun phox-compile-theorem-on-cursor()phox-compile-theorem-on-cursor87,2601 (defun phox-output ()phox-output103,3079 (defun phox-output-theorem (name)phox-output-theorem113,3291 (defun phox-output-theorem-on-cursor()phox-output-theorem-on-cursor120,3590 phox/phox-font.el,458 (defvar phox-sym-lock-enabled nil) ; da: for clean compilephox-sym-lock-enabled1,0 (defvar phox-sym-lock-color nil) ; da: for clean compilephox-sym-lock-color2,60 (defvar phox-sym-lock-keywords nil) ; da: for clean compilephox-sym-lock-keywords3,118 (defconst phox-font-lock-keywordsphox-font-lock-keywords11,511 (defconst phox-sym-lock-keywords-tablephox-sym-lock-keywords-table70,2628 (defun phox-sym-lock-start ()phox-sym-lock-start93,3202 phox/phox-fun.el,3113 (defconst phox-forget-id-command "del %s.\n")phox-forget-id-command11,186 (defconst phox-forget-proof-command "del_proof %s.\n")phox-forget-proof-command12,232 (defconst phox-forget-new-elim-command "edel elim %s.\n")phox-forget-new-elim-command13,287 (defconst phox-forget-new-intro-command "edel intro %s.\n")phox-forget-new-intro-command14,345 (defconst phox-forget-new-equation-command "edel equation %s.\n")phox-forget-new-equation-command15,405 (defconst phox-forget-close-def-command "edel closed %s.\n")phox-forget-close-def-command16,471 (defconst phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*")phox-comments-regexp18,597 (defconst phox-strict-comments-regexp "\\([ \n\t\r]+\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*\\|\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)+\\)")phox-strict-comments-regexp20,776 (defconst phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)")phox-ident-regexp21,941 (defconst phox-inductive-option "\\(\\[[^]]*]\\)?")phox-inductive-option22,1027 (defconst phox-spaces-regexp "[ \n\t\r]*")phox-spaces-regexp23,1079 (defconst phox-sy-definition-regexp (concatphox-sy-definition-regexp24,1122 (defconst phox-sy-inductive-regexp (concatphox-sy-inductive-regexp28,1309 (defconst phox-inductive-regexp (concatphox-inductive-regexp34,1522 (defconst phox-data-regexp (concatphox-data-regexp40,1673 (defconst phox-definition-regexp (concatphox-definition-regexp46,1827 (defconst phox-prove-claim-regexp (concatphox-prove-claim-regexp50,1971 (defconst phox-new-elim-regexp (concatphox-new-elim-regexp54,2077 (defconst phox-new-intro-regexp (concatphox-new-intro-regexp57,2196 (defconst phox-new-rewrite-regexp (concatphox-new-rewrite-regexp60,2317 (defconst phox-new-equation-regexp (concatphox-new-equation-regexp63,2442 (defconst phox-close-def-regexp (concatphox-close-def-regexp66,2569 (defun phox-init-syntax-table (&optional TABLE)phox-init-syntax-table71,2706 (defvar phox-top-keywordsphox-top-keywords87,3178 (defvar phox-proof-keywordsphox-proof-keywords135,3633 (defun phox-find-and-forget (span)phox-find-and-forget176,3983 (defalias 'phox-assert-next-command-interactive 'proof-assert-next-command-interactive)phox-assert-next-command-interactive255,6399 (defun phox-depend-theorem(theorem)phox-depend-theorem274,7365 (defun phox-eshow-extlist(extlist)phox-eshow-extlist283,7654 (defun phox-flag-name(name)phox-flag-name297,8251 (defun phox-path()phox-path308,8553 (defun phox-print-expression(expr)phox-print-expression319,8789 (defun phox-print-sort-expression(expr)phox-print-sort-expression332,9245 (defun phox-priority-symbols-list(symblist)phox-priority-symbols-list343,9557 (defun phox-search-string(string type)phox-search-string355,9929 (defun phox-constraints()phox-constraints370,10454 (defun phox-goals()phox-goals381,10710 (defvar phox-state-menuphox-state-menu393,10919 (defun phox-delete-symbol(symbol)phox-delete-symbol418,11909 (defun phox-delete-symbol-on-cursor()phox-delete-symbol-on-cursor424,12117 phox/phox-lang.el,517 (defvar phox-langphox-lang9,306 (defun phox-lang-absurd ()phox-lang-absurd17,535 (defun phox-lang-suppress (s)phox-lang-suppress22,629 (defun phox-lang-opendef ()phox-lang-opendef27,826 (defun phox-lang-instance (s)phox-lang-instance32,944 (defun phox-lang-open-instance (s)phox-lang-open-instance37,1073 (defun phox-lang-lock (s)phox-lang-lock42,1222 (defun phox-lang-unlock (s)phox-lang-unlock47,1352 (defun phox-lang-prove (s)phox-lang-prove52,1488 (defun phox-lang-let (s)phox-lang-let57,1622 phox/phox-outline.el,506 (defconst phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)")phox-outline-title-regexp20,745 (defconst phox-outline-section-regexp "\\((\\*\\*+\\)")phox-outline-section-regexp21,810 (defconst phox-outline-save-regexp "\\((\\*#\\)")phox-outline-save-regexp22,866 (defconst phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)")phox-outline-heading-end-regexp39,1409 (defun phox-outline-level()phox-outline-level45,1584 (defun phox-setup-outline ()phox-setup-outline59,2058 phox/phox-pbrpm.el,847 (defun phox-pbrpm-left-paren-p (char)phox-pbrpm-left-paren-p39,1671 (defun phox-pbrpm-right-paren-p (char)phox-pbrpm-right-paren-p46,1874 (defun phox-pbrpm-menu-from-string (order str)phox-pbrpm-menu-from-string54,2078 (defun phox-pbrpm-rename-in-cmd (cmd spans)phox-pbrpm-rename-in-cmd63,2410 (defun phox-pbrpm-get-region-name (region-info)phox-pbrpm-get-region-name96,3658 (defun phox-pbrpm-escape-string (str)phox-pbrpm-escape-string99,3785 (defun phox-pbrpm-generate-menu (click-infos region-infos)phox-pbrpm-generate-menu103,3920 (defalias 'proof-pbrpm-generate-menu 'phox-pbrpm-generate-menu)proof-pbrpm-generate-menu310,11400 (defalias 'proof-pbrpm-left-paren-p 'phox-pbrpm-left-paren-p)proof-pbrpm-left-paren-p311,11464 (defalias 'proof-pbrpm-right-paren-p 'phox-pbrpm-right-paren-p)proof-pbrpm-right-paren-p312,11526 phox/phox-sym-lock.el,2530 (defcustom phox-sym-lock-enabled tphox-sym-lock-enabled19,871 (defvar phox-sym-lock-sym-count 0phox-sym-lock-sym-count59,2452 (defvar phox-sym-lock-ext-start nil "Temporary for atomicization.")phox-sym-lock-ext-start62,2522 (defvar phox-sym-lock-ext-end nil "Temporary for atomicization.")phox-sym-lock-ext-end64,2644 (defvar phox-sym-lock-font-size nilphox-sym-lock-font-size67,2763 (defvar phox-sym-lock-keywords nilphox-sym-lock-keywords72,2953 (defvar phox-sym-lock-enabled nilphox-sym-lock-enabled77,3129 (defvar phox-sym-lock-color (face-foreground 'default)phox-sym-lock-color82,3291 (defvar phox-sym-lock-mouse-face 'defaultphox-sym-lock-mouse-face87,3509 (defvar phox-sym-lock-mouse-face-enabled tphox-sym-lock-mouse-face-enabled92,3699 (defconst phox-sym-lock-with-mule (featurep 'mule)phox-sym-lock-with-mule97,3889 (defun phox-sym-lock-gen-symbol (&optional prefix)phox-sym-lock-gen-symbol100,3973 (defun phox-sym-lock-make-symbols-atomic (&optional begin end)phox-sym-lock-make-symbols-atomic108,4275 (defun phox-sym-lock-compute-font-size ()phox-sym-lock-compute-font-size135,5216 (defvar phox-sym-lock-font-namephox-sym-lock-font-name173,6635 (defun phox-sym-lock-set-foreground ()phox-sym-lock-set-foreground216,8233 (defun phox-sym-lock-translate-char (char)phox-sym-lock-translate-char230,8842 (defun phox-sym-lock-translate-char-or-string (obj)phox-sym-lock-translate-char-or-string239,9159 (defun phox-sym-lock-remap-face (pat pos obj atomic)phox-sym-lock-remap-face246,9387 (defvar phox-sym-lock-clear-facephox-sym-lock-clear-face266,10375 (defun phox-sym-lock (fl)phox-sym-lock278,10794 (defun phox-sym-lock-rec (fl)phox-sym-lock-rec287,11198 (defun phox-sym-lock-atom-face (pat num pos obj &optional override)phox-sym-lock-atom-face293,11343 (defun phox-sym-lock-pre-idle-hook-first ()phox-sym-lock-pre-idle-hook-first298,11639 (defun phox-sym-lock-pre-idle-hook-last ()phox-sym-lock-pre-idle-hook-last308,12044 (defun phox-sym-lock-enable ()phox-sym-lock-enable317,12419 (defun phox-sym-lock-disable ()phox-sym-lock-disable330,12830 (defun phox-sym-lock-mouse-face-enable ()phox-sym-lock-mouse-face-enable343,13246 (defun phox-sym-lock-mouse-face-disable ()phox-sym-lock-mouse-face-disable350,13461 (defun phox-sym-lock-font-lock-hook ()phox-sym-lock-font-lock-hook357,13680 (defun font-lock-set-defaults (&optional explicit-defaults)font-lock-set-defaults372,14371 (defun phox-sym-lock-patch-keywords ()phox-sym-lock-patch-keywords384,14798 phox/phox-tags.el,495 (defun phox-tags-add-table(table)phox-tags-add-table26,869 (defun phox-tags-reset-table()phox-tags-reset-table35,1264 (defun phox-tags-add-doc-table()phox-tags-add-doc-table40,1374 (defun phox-tags-add-lib-table()phox-tags-add-lib-table46,1523 (defun phox-tags-add-local-table()phox-tags-add-local-table52,1658 (defun phox-tags-create-local-table()phox-tags-create-local-table58,1841 (defun phox-complete-tag()phox-complete-tag69,2091 (defvar phox-tags-menuphox-tags-menu76,2200 generic/pg-assoc.el,135 (defun proof-associated-buffers ()proof-associated-buffers33,973 (defun proof-associated-windows ()proof-associated-windows43,1183 generic/pg-autotest.el,1629 (defvar pg-autotest-success tpg-autotest-success29,690 (defvar pg-autotest-log tpg-autotest-log32,777 (defun pg-autotest-find-file (file)pg-autotest-find-file37,871 (defun pg-autotest-find-file-restart (file)pg-autotest-find-file-restart44,1137 (defmacro pg-autotest-apply (fn &rest args)pg-autotest-apply58,1611 (defmacro pg-autotest (fn &rest args)pg-autotest72,2026 (defun pg-autotest-log (file)pg-autotest-log89,2463 (defun pg-autotest-message (msg &rest args)pg-autotest-message98,2726 (defun pg-autotest-remark (msg)pg-autotest-remark107,3015 (defun pg-autotest-timestart (&optional clockname)pg-autotest-timestart110,3096 (defun pg-autotest-timetaken (&optional clockname)pg-autotest-timetaken115,3279 (defun pg-autotest-start (&optional debug)pg-autotest-start129,3667 (defun pg-autotest-exit ()pg-autotest-exit140,4121 (defun pg-autotest-test-process-wholefile (file)pg-autotest-test-process-wholefile160,4904 (defun pg-autotest-test-script-wholefile (file)pg-autotest-test-script-wholefile168,5191 (defun pg-autotest-test-script-randomjumps (file jumps)pg-autotest-test-script-randomjumps193,6123 (defun pg-autotest-test-retract-file (file)pg-autotest-test-retract-file242,7680 (defun pg-autotest-test-assert-processed (file)pg-autotest-test-assert-processed248,7821 (defun pg-autotest-test-assert-full ()pg-autotest-test-assert-full254,8047 (defun pg-autotest-test-assert-unprocessed (file)pg-autotest-test-assert-unprocessed261,8288 (defun pg-autotest-test-eval (body)pg-autotest-test-eval268,8553 (defun pg-autotest-test-quit-prover ()pg-autotest-test-quit-prover272,8652 generic/pg-custom.el,1058 (defpgcustom script-indent tscript-indent37,1199 (defconst proof-toolbar-entries-defaultproof-toolbar-entries-default42,1336 (defpgcustom toolbar-entries proof-toolbar-entries-defaulttoolbar-entries70,3069 (defpgcustom prog-args nilprog-args89,3802 (defpgcustom prog-env nilprog-env101,4378 (defpgcustom quit-timeout quit-timeout110,4805 (defpgcustom favourites nilfavourites122,5232 (defpgcustom menu-entries nilmenu-entries127,5421 (defpgcustom help-menu-entries nilhelp-menu-entries134,5657 (defpgcustom keymap (make-keymap (concat proof-assistant " keymap"))keymap141,5920 (defpgcustom completion-table nilcompletion-table146,6091 (defpgcustom tags-program niltags-program157,6465 (defpgcustom use-holes (eq proof-assistant-symbol 'coq)use-holes166,6849 (defpgcustom one-command-per-lineone-command-per-line173,7107 (defpgcustom maths-menu-enable nilmaths-menu-enable184,7343 (defpgcustom unicode-tokens-enable (eq proof-assistant-symbol 'isar)unicode-tokens-enable190,7523 (defpgcustom mmm-enable nilmmm-enable196,7730 generic/pg-goals.el,540 (define-derived-mode proof-goals-mode proof-universal-keys-only-modeproof-goals-mode29,734 (define-key proof-goals-mode-map [q] 'bury-buffer)proof-goals-mode-map56,1592 (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)proof-goals-mode-map58,1708 (define-key proof-goals-mode-map [C-M-mouse-3]proof-goals-mode-map59,1776 (defun proof-goals-config-done ()proof-goals-config-done68,1923 (defun pg-goals-display (string)pg-goals-display76,2189 (defun pg-goals-button-action (event)pg-goals-button-action117,3493 generic/pg-movie.el,642 (defconst pg-movie-xml-header "")pg-movie-xml-header33,944 (defconst pg-movie-stylesheetpg-movie-stylesheet35,1002 (defun pg-movie-stylesheet-location ()pg-movie-stylesheet-location38,1101 (defvar pg-movie-frame 0 "Frame counter for movie.")pg-movie-frame42,1209 (defun pg-movie-of-span (span)pg-movie-of-span44,1263 (defun pg-movie-of-region (start end)pg-movie-of-region80,2383 (defun pg-movie-export (&optional force)pg-movie-export87,2571 (defun pg-movie-export-from (script &optional force)pg-movie-export-from109,3175 (defun pg-movie-export-directory (dir extn)pg-movie-export-directory120,3496 generic/pg-pamacs.el,887 (defmacro deflocal (var value &optional docstring)deflocal35,1132 (deflocal proof-buffer-type nilproof-buffer-type42,1370 (defmacro proof-ass-sym (sym)proof-ass-sym50,1506 (defmacro proof-ass-symv (sym)proof-ass-symv56,1765 (defmacro proof-ass (sym)proof-ass62,2023 (defun proof-defpgcustom-fn (sym args)proof-defpgcustom-fn68,2275 (defun undefpgcustom (sym)undefpgcustom89,3145 (defmacro defpgcustom (sym &rest args)defpgcustom95,3369 (defun proof-defpgdefault-fn (sym value)proof-defpgdefault-fn106,3780 (defmacro defpgdefault (sym value)defpgdefault120,4238 (defmacro defpgfun (name arglist &rest args)defpgfun131,4600 (defun proof-defpacustom-fn (name val args)proof-defpacustom-fn145,4999 (defmacro defpacustom (name val &rest args)defpacustom212,7307 (defmacro proof-eval-when-ready-for-assistant (&rest body)proof-eval-when-ready-for-assistant233,8262 generic/pg-pbrpm.el,3173 (defvar pg-pbrpm-use-buffer-menu tpg-pbrpm-use-buffer-menu45,1207 (defvar pg-pbrpm-start-goal-regexp nilpg-pbrpm-start-goal-regexp48,1329 (defvar pg-pbrpm-start-goal-regexp-par-num nilpg-pbrpm-start-goal-regexp-par-num52,1486 (defvar pg-pbrpm-end-goal-regexp nilpg-pbrpm-end-goal-regexp55,1609 (defvar pg-pbrpm-start-hyp-regexp nilpg-pbrpm-start-hyp-regexp59,1761 (defvar pg-pbrpm-start-hyp-regexp-par-num nilpg-pbrpm-start-hyp-regexp-par-num63,1922 (defvar pg-pbrpm-start-concl-regexp nilpg-pbrpm-start-concl-regexp67,2129 (defvar pg-pbrpm-auto-select-regexp nilpg-pbrpm-auto-select-regexp71,2293 (defvar pg-pbrpm-buffer-menu nil)pg-pbrpm-buffer-menu78,2454 (defvar pg-pbrpm-spans nil)pg-pbrpm-spans79,2488 (defvar pg-pbrpm-goal-description nil)pg-pbrpm-goal-description80,2516 (defvar pg-pbrpm-windows-dialog-bug nil)pg-pbrpm-windows-dialog-bug81,2555 (defvar pbrpm-menu-desc nil)pbrpm-menu-desc82,2596 (defun pg-pbrpm-erase-buffer-menu ()pg-pbrpm-erase-buffer-menu84,2626 (defun pg-pbrpm-menu-change-hook (start end len)pg-pbrpm-menu-change-hook90,2798 (defun pg-pbrpm-create-reset-buffer-menu ()pg-pbrpm-create-reset-buffer-menu108,3373 (defun pg-pbrpm-analyse-goal-buffer ()pg-pbrpm-analyse-goal-buffer127,4215 (defun pg-pbrpm-button-action (event)pg-pbrpm-button-action187,6620 (defun pg-pbrpm-exists (f l0)pg-pbrpm-exists194,6846 (defun pg-pbrpm-eliminate-id (acc l)pg-pbrpm-eliminate-id198,6958 (defun pg-pbrpm-build-menu (event start end)pg-pbrpm-build-menu206,7204 (defun pg-pbrpm-setup-span (start end)pg-pbrpm-setup-span269,9524 (defun pg-pbrpm-run-command (args)pg-pbrpm-run-command329,11823 (defun pg-pbrpm-get-pos-info (pos)pg-pbrpm-get-pos-info362,13348 (defun pg-pbrpm-get-region-info (start end)pg-pbrpm-get-region-info404,14647 (defun pg-pbrpm-auto-select-around-point ()pg-pbrpm-auto-select-around-point415,15059 (defun pg-pbrpm-translate-position (buffer pos)pg-pbrpm-translate-position430,15583 (defun pg-pbrpm-process-click (event start end)pg-pbrpm-process-click438,15837 (defvar pg-pbrpm-remember-region-selected-region nil)pg-pbrpm-remember-region-selected-region458,16862 (defvar pg-pbrpm-regions-list nil)pg-pbrpm-regions-list459,16916 (defun pg-pbrpm-erase-regions-list ()pg-pbrpm-erase-regions-list461,16952 (defun pg-pbrpm-filter-regions-list ()pg-pbrpm-filter-regions-list470,17260 (defface pg-pbrpm-multiple-selection-facepg-pbrpm-multiple-selection-face477,17523 (defface pg-pbrpm-menu-input-facepg-pbrpm-menu-input-face485,17725 (defun pg-pbrpm-do-remember-region (start end)pg-pbrpm-do-remember-region493,17915 (defun pg-pbrpm-remember-region-drag-up-hook (event click-count)pg-pbrpm-remember-region-drag-up-hook514,18763 (defun pg-pbrpm-remember-region-click-hook (event click-count)pg-pbrpm-remember-region-click-hook518,18934 (defun pg-pbrpm-remember-region (event &optional delete)pg-pbrpm-remember-region523,19119 (defun pg-pbrpm-process-region (span)pg-pbrpm-process-region537,19833 (defun pg-pbrpm-process-regions-list ()pg-pbrpm-process-regions-list555,20562 (defun pg-pbrpm-region-expression (buffer start end)pg-pbrpm-region-expression559,20745 generic/pg-pgip.el,5070 (defalias 'pg-pgip-debug 'proof-debug)pg-pgip-debug38,1032 (defalias 'pg-pgip-error 'error)pg-pgip-error39,1073 (defalias 'pg-pgip-warning 'pg-internal-warning)pg-pgip-warning40,1108 (defconst pg-pgip-version-supported "2.0"pg-pgip-version-supported42,1158 (defun pg-pgip-process-packet (pgips)pg-pgip-process-packet46,1264 (defvar pg-pgip-last-seen-id nil)pg-pgip-last-seen-id56,1832 (defvar pg-pgip-last-seen-seq nil)pg-pgip-last-seen-seq57,1866 (defun pg-pgip-process-pgip (pgip)pg-pgip-process-pgip59,1902 (defun pg-pgip-process-msg (pgipmsg)pg-pgip-process-msg78,2842 (defvar pg-pgip-post-process-functionspg-pgip-post-process-functions93,3433 (defun pg-pgip-post-process (cmdname)pg-pgip-post-process103,3908 (defun pg-pgip-process-askpgip (node)pg-pgip-process-askpgip120,4523 (defun pg-pgip-process-usespgip (node)pg-pgip-process-usespgip126,4727 (defun pg-pgip-process-usespgml (node)pg-pgip-process-usespgml130,4891 (defun pg-pgip-process-pgmlconfig (node)pg-pgip-process-pgmlconfig134,5055 (defun pg-pgip-process-proverinfo (node)pg-pgip-process-proverinfo150,5672 (defun pg-pgip-process-hasprefs (node)pg-pgip-process-hasprefs167,6337 (defun pg-pgip-haspref (name type prefcat descr default)pg-pgip-haspref181,6969 (defun pg-pgip-process-prefval (node)pg-pgip-process-prefval198,7671 (defun pg-pgip-process-guiconfig (node)pg-pgip-process-guiconfig225,8379 (defvar proof-assistant-idtables nilproof-assistant-idtables232,8496 (defun pg-pgip-process-ids (node)pg-pgip-process-ids235,8613 (defun pg-complete-idtable-symbol ()pg-complete-idtable-symbol261,9685 (defalias 'pg-pgip-process-setids 'pg-pgip-process-ids)pg-pgip-process-setids266,9777 (defalias 'pg-pgip-process-addids 'pg-pgip-process-ids)pg-pgip-process-addids267,9833 (defalias 'pg-pgip-process-delids 'pg-pgip-process-ids)pg-pgip-process-delids268,9889 (defun pg-pgip-process-idvalue (node)pg-pgip-process-idvalue271,9947 (defun pg-pgip-process-menuadd (node)pg-pgip-process-menuadd283,10293 (defun pg-pgip-process-menudel (node)pg-pgip-process-menudel286,10336 (defun pg-pgip-process-ready (node)pg-pgip-process-ready295,10568 (defun pg-pgip-process-cleardisplay (node)pg-pgip-process-cleardisplay298,10609 (defun pg-pgip-process-proofstate (node)pg-pgip-process-proofstate312,11066 (defun pg-pgip-process-normalresponse (node)pg-pgip-process-normalresponse316,11143 (defun pg-pgip-process-errorresponse (node)pg-pgip-process-errorresponse320,11273 (defun pg-pgip-process-scriptinsert (node)pg-pgip-process-scriptinsert324,11402 (defun pg-pgip-process-metainforesponse (node)pg-pgip-process-metainforesponse329,11536 (defun pg-pgip-file-of-url (urlstr)pg-pgip-file-of-url338,11776 (defun pg-pgip-process-informfileloaded (node)pg-pgip-process-informfileloaded343,11911 (defun pg-pgip-process-informfileretracted (node)pg-pgip-process-informfileretracted349,12143 (defun pg-pgip-process-brokerstatus (node)pg-pgip-process-brokerstatus362,12590 (defun pg-pgip-process-proveravailmsg (node)pg-pgip-process-proveravailmsg365,12638 (defun pg-pgip-process-newprovermsg (node)pg-pgip-process-newprovermsg368,12688 (defun pg-pgip-process-proverstatusmsg (node)pg-pgip-process-proverstatusmsg371,12736 (defvar pg-pgip-srcids nilpg-pgip-srcids380,12982 (defun pg-pgip-process-newfile (node)pg-pgip-process-newfile384,13089 (defun pg-pgip-process-filestatus (node)pg-pgip-process-filestatus400,13671 (defun pg-pgip-process-newobj (node)pg-pgip-process-newobj420,14325 (defun pg-pgip-process-delobj (node)pg-pgip-process-delobj423,14367 (defun pg-pgip-process-objectstatus (node)pg-pgip-process-objectstatus426,14409 (defun pg-pgip-process-parsescript (node)pg-pgip-process-parsescript440,14761 (defun pg-pgip-get-pgiptype (node)pg-pgip-get-pgiptype463,15635 (defun pg-pgip-default-for (type)pg-pgip-default-for484,16498 (defun pg-pgip-subst-for (type)pg-pgip-subst-for497,16893 (defun pg-pgip-interpret-value (value type)pg-pgip-interpret-value510,17263 (defun pg-pgip-interpret-choice (choices value)pg-pgip-interpret-choice529,17988 (defun pg-pgip-string-of-command (pgip &optional refseq refid otherclass)pg-pgip-string-of-command560,19005 (defconst pg-pgip-idpg-pgip-id577,19766 (defvar pg-pgip-refseq nilpg-pgip-refseq583,20046 (defvar pg-pgip-refid nilpg-pgip-refid585,20143 (defvar pg-pgip-seq 0 "Sequence number of messages sent out.")pg-pgip-seq588,20235 (defun pg-pgip-assemble-packet (body &optional refseq refid otherclass)pg-pgip-assemble-packet590,20299 (defun pg-pgip-issue (pgip &optional block refseq refid otherclass)pg-pgip-issue608,21110 (defun pg-pgip-maybe-askpgip ()pg-pgip-maybe-askpgip625,21722 (defun pg-pgip-askprefs ()pg-pgip-askprefs631,21913 (defun pg-pgip-askids (&optional objtype thyname)pg-pgip-askids635,22027 (defun pg-pgip-reset ()pg-pgip-reset648,22315 (defconst pg-pgip-start-element-regexp "")pg-pgip-end-element-regexp680,23065 generic/pg-response.el,2348 (deflocal pg-response-eagerly-raise tpg-response-eagerly-raise32,788 (define-derived-mode proof-response-mode proof-universal-keys-only-modeproof-response-mode42,1013 (define-key proof-response-mode-map [mouse-1] 'pg-goals-button-action)proof-response-mode-map69,1950 (define-key proof-response-mode-map [q] 'bury-buffer)proof-response-mode-map70,2021 (define-key proof-response-mode-map [c] 'pg-response-clear-displays)proof-response-mode-map71,2075 (defun proof-response-config-done ()proof-response-config-done75,2161 (defvar pg-response-special-display-regexp nilpg-response-special-display-regexp86,2507 (defconst proof-multiframe-parametersproof-multiframe-parameters90,2674 (defun proof-multiple-frames-enable ()proof-multiple-frames-enable99,2964 (defun proof-three-window-enable ()proof-three-window-enable109,3292 (defun proof-select-three-b (b1 b2 b3 &optional nohorizontalsplit)proof-select-three-b112,3355 (defun proof-display-three-b (&optional nohorizontalsplit)proof-display-three-b127,3846 (defvar pg-frame-configuration nilpg-frame-configuration138,4236 (defun pg-cache-frame-configuration ()pg-cache-frame-configuration142,4383 (defun proof-layout-windows (&optional nohorizontalsplit)proof-layout-windows146,4554 (defun proof-delete-other-frames ()proof-delete-other-frames186,6341 (defvar pg-response-erase-flag nilpg-response-erase-flag217,7429 (defun pg-response-maybe-erasepg-response-maybe-erase221,7558 (defun pg-response-display (str)pg-response-display251,8662 (defun pg-response-display-with-face (str &optional face)pg-response-display-with-face276,9445 (defun pg-response-clear-displays ()pg-response-clear-displays304,10291 (defun pg-response-message (&rest args)pg-response-message317,10810 (defun pg-response-warning (&rest args)pg-response-warning323,11045 (defun proof-next-error (&optional argp)proof-next-error338,11451 (defun pg-response-has-error-location ()pg-response-has-error-location416,14260 (defvar proof-trace-last-fontify-pos nil)proof-trace-last-fontify-pos438,15073 (defun proof-trace-fontify-pos ()proof-trace-fontify-pos440,15116 (defun proof-trace-buffer-display (str)proof-trace-buffer-display448,15429 (defun proof-trace-buffer-finish ()proof-trace-buffer-finish459,15773 (defun pg-thms-buffer-clear ()pg-thms-buffer-clear477,16116 generic/pg-user.el,6413 (defun proof-script-new-command-advance ()proof-script-new-command-advance42,1231 (defun proof-maybe-follow-locked-end (&optional pos)proof-maybe-follow-locked-end66,2156 (defun proof-goto-command-start ()proof-goto-command-start92,2992 (defun proof-goto-command-end ()proof-goto-command-end115,3939 (defun proof-forward-command (&optional num)proof-forward-command130,4361 (defun proof-backward-command (&optional num)proof-backward-command151,5082 (defun proof-goto-point ()proof-goto-point162,5296 (defun proof-assert-next-command-interactive ()proof-assert-next-command-interactive176,5730 (defun proof-assert-until-point-interactive ()proof-assert-until-point-interactive188,6216 (defun proof-process-buffer ()proof-process-buffer194,6446 (defun proof-undo-last-successful-command ()proof-undo-last-successful-command212,6958 (defun proof-undo-and-delete-last-successful-command ()proof-undo-and-delete-last-successful-command217,7120 (defun proof-undo-last-successful-command-1 (&optional undo-action)proof-undo-last-successful-command-1229,7641 (defun proof-retract-buffer ()proof-retract-buffer246,8305 (defun proof-retract-current-goal ()proof-retract-current-goal255,8589 (defun proof-mouse-goto-point (event)proof-mouse-goto-point274,9109 (defvar proof-minibuffer-history nilproof-minibuffer-history289,9385 (defun proof-minibuffer-cmd (cmd)proof-minibuffer-cmd292,9480 (defun proof-frob-locked-end ()proof-frob-locked-end331,10887 (defmacro proof-if-setting-configured (var &rest body)proof-if-setting-configured367,11988 (defmacro proof-define-assistant-command (fn doc cmdvar &optional body)proof-define-assistant-command375,12257 (defmacro proof-define-assistant-command-witharg (fn doc cmdvar prompt &rest body)proof-define-assistant-command-witharg388,12712 (defun proof-issue-new-command (cmd)proof-issue-new-command408,13534 (defun proof-cd-sync ()proof-cd-sync448,14757 (defun proof-electric-terminator-enable ()proof-electric-terminator-enable499,16356 (defun proof-electric-terminator ()proof-electric-terminator507,16660 (defun proof-add-completions ()proof-add-completions531,17440 (defun proof-script-complete (&optional arg)proof-script-complete554,18263 (defun pg-copy-span-contents (span)pg-copy-span-contents568,18572 (defun pg-numth-span-higher-or-lower (span num &optional noerr)pg-numth-span-higher-or-lower582,18996 (defun pg-control-span-of (span)pg-control-span-of608,19742 (defun pg-move-span-contents (span num)pg-move-span-contents614,19946 (defun pg-fixup-children-spans (new-parent start end)pg-fixup-children-spans665,22064 (defun pg-move-region-down (&optional num)pg-move-region-down675,22321 (defun pg-move-region-up (&optional num)pg-move-region-up684,22614 (defun pg-pos-for-event (event)pg-pos-for-event698,22888 (defun pg-span-for-event (event)pg-span-for-event704,23109 (defun pg-span-context-menu (event)pg-span-context-menu708,23253 (defun pg-toggle-visibility ()pg-toggle-visibility724,23770 (defun pg-create-in-span-context-menu (span idiom name)pg-create-in-span-context-menu733,24077 (defun pg-span-undo (span)pg-span-undo758,25105 (defun pg-goals-buffers-hint ()pg-goals-buffers-hint771,25343 (defun pg-slow-fontify-tracing-hint ()pg-slow-fontify-tracing-hint775,25525 (defun pg-response-buffers-hint (&optional nextbuf)pg-response-buffers-hint779,25696 (defun pg-jump-to-end-hint ()pg-jump-to-end-hint791,26111 (defun pg-processing-complete-hint ()pg-processing-complete-hint795,26240 (defun pg-next-error-hint ()pg-next-error-hint812,26960 (defun pg-hint (hintmsg)pg-hint817,27112 (defun pg-identifier-under-mouse-query (event)pg-identifier-under-mouse-query828,27461 (defun pg-identifier-near-point-query ()pg-identifier-near-point-query839,27785 (defvar proof-query-identifier-history nilproof-query-identifier-history868,28708 (defun proof-query-identifier (string)proof-query-identifier871,28795 (defun pg-identifier-query (identifier &optional ctxt callback)pg-identifier-query882,29151 (defun proof-imenu-enable ()proof-imenu-enable915,30299 (defvar pg-input-ring nilpg-input-ring951,31602 (defvar pg-input-ring-index nilpg-input-ring-index954,31659 (defvar pg-stored-incomplete-input nilpg-stored-incomplete-input957,31731 (defun pg-previous-input (arg)pg-previous-input960,31834 (defun pg-next-input (arg)pg-next-input974,32297 (defun pg-delete-input ()pg-delete-input979,32419 (defun pg-get-old-input ()pg-get-old-input992,32757 (defun pg-restore-input ()pg-restore-input1006,33148 (defun pg-search-start (arg)pg-search-start1017,33438 (defun pg-regexp-arg (prompt)pg-regexp-arg1029,33930 (defun pg-search-arg (arg)pg-search-arg1041,34378 (defun pg-previous-matching-input-string-position (regexp arg &optional start)pg-previous-matching-input-string-position1055,34795 (defun pg-previous-matching-input (regexp n)pg-previous-matching-input1082,35960 (defun pg-next-matching-input (regexp n)pg-next-matching-input1101,36810 (defvar pg-matching-input-from-input-string ""pg-matching-input-from-input-string1109,37193 (defun pg-previous-matching-input-from-input (n)pg-previous-matching-input-from-input1113,37307 (defun pg-next-matching-input-from-input (n)pg-next-matching-input-from-input1131,38072 (defun pg-add-to-input-history (cmd)pg-add-to-input-history1142,38451 (defun pg-remove-from-input-history (cmd)pg-remove-from-input-history1154,38904 (defun pg-clear-input-ring ()pg-clear-input-ring1165,39284 (define-key proof-mode-map [remap undo] 'pg-protected-undo)proof-mode-map1182,39754 (define-key proof-mode-map [remap advertised-undo] 'pg-protected-undo)proof-mode-map1183,39814 (defun pg-protected-undo (&optional arg)pg-protected-undo1185,39886 (defun pg-protected-undo-1 (arg)pg-protected-undo-11215,41180 (defun next-undo-elt (arg)next-undo-elt1246,42617 (defvar proof-autosend-timer nil "Timer used by autosend.")proof-autosend-timer1273,43573 (deflocal proof-autosend-modified-tick nilproof-autosend-modified-tick1275,43634 (defun proof-autosend-enable (&optional nomsg)proof-autosend-enable1279,43756 (defun proof-autosend-delay ()proof-autosend-delay1293,44299 (defun proof-autosend-loop ()proof-autosend-loop1297,44432 (defun proof-autosend-loop-all ()proof-autosend-loop-all1311,44992 (defun proof-autosend-loop-next ()proof-autosend-loop-next1335,45772 generic/pg-vars.el,2462 (defvar proof-assistant-cusgrp nilproof-assistant-cusgrp22,388 (defvar proof-assistant-internals-cusgrp nilproof-assistant-internals-cusgrp28,648 (defvar proof-assistant ""proof-assistant34,918 (defvar proof-assistant-symbol nilproof-assistant-symbol39,1141 (defvar proof-mode-for-shell nilproof-mode-for-shell52,1683 (defvar proof-mode-for-response nilproof-mode-for-response57,1873 (defvar proof-mode-for-goals nilproof-mode-for-goals62,2099 (defvar proof-mode-for-script nilproof-mode-for-script67,2288 (defvar proof-ready-for-assistant-hook nilproof-ready-for-assistant-hook72,2465 (defvar proof-shell-busy nilproof-shell-busy83,2753 (defvar proof-shell-last-queuemode nilproof-shell-last-queuemode101,3424 (defvar proof-included-files-list nilproof-included-files-list105,3579 (defvar proof-script-buffer nilproof-script-buffer127,4598 (defvar proof-previous-script-buffer nilproof-previous-script-buffer130,4690 (defvar proof-shell-buffer nilproof-shell-buffer134,4863 (defvar proof-goals-buffer nilproof-goals-buffer137,4949 (defvar proof-response-buffer nilproof-response-buffer140,5004 (defvar proof-trace-buffer nilproof-trace-buffer143,5065 (defvar proof-thms-buffer nilproof-thms-buffer147,5219 (defvar proof-shell-error-or-interrupt-seen nilproof-shell-error-or-interrupt-seen151,5374 (defvar pg-response-next-error nilpg-response-next-error156,5598 (defvar proof-shell-proof-completed nilproof-shell-proof-completed159,5705 (defvar proof-shell-silent nilproof-shell-silent173,6090 (defvar proof-shell-last-prompt ""proof-shell-last-prompt176,6178 (defvar proof-shell-last-output ""proof-shell-last-output180,6348 (defvar proof-shell-last-output-kind nilproof-shell-last-output-kind184,6488 (defvar proof-assistant-settings nilproof-assistant-settings204,7252 (defvar pg-tracing-slow-mode nilpg-tracing-slow-mode212,7731 (defvar proof-nesting-depth 0proof-nesting-depth215,7820 (defvar proof-last-theorem-dependencies nilproof-last-theorem-dependencies222,8055 (defvar proof-autosend-running nilproof-autosend-running226,8217 (defvar proof-next-command-on-new-line nilproof-next-command-on-new-line231,8416 (defcustom proof-general-name "Proof-General"proof-general-name242,8650 (defcustom proof-general-home-pageproof-general-home-page247,8807 (defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name253,8967 (defcustom proof-universal-keysproof-universal-keys259,9151 generic/pg-xml.el,2460 (defalias 'pg-xml-error 'error)pg-xml-error18,381 (defun pg-xml-parse-string (arg)pg-xml-parse-string41,1023 (defun pg-xml-parse-buffer (&optional buffer nomsg start end)pg-xml-parse-buffer51,1335 (defun pg-xml-get-attr (attribute node &optional optional defaultval)pg-xml-get-attr70,1950 (defun pg-xml-child-elts (node)pg-xml-child-elts78,2252 (defun pg-xml-child-elt (node)pg-xml-child-elt83,2457 (defun pg-xml-get-child (child node)pg-xml-get-child91,2739 (defun pg-xml-get-text-content (node)pg-xml-get-text-content101,3106 (defmacro pg-xml-attr (name val) `(cons (quote ,name) ,val))pg-xml-attr112,3456 (defmacro pg-xml-node (name atts children)pg-xml-node114,3518 (defconst pg-xml-headerpg-xml-header117,3610 (defun pg-xml-string-of (xmls)pg-xml-string-of121,3686 (defun pg-xml-output-internal (xml indent-string outputfn)pg-xml-output-internal132,4053 (defun pg-xml-cdata (str)pg-xml-cdata166,5192 (defsubst pg-pgip-get-area (node &optional optional defaultval)pg-pgip-get-area174,5385 (defun pg-pgip-get-icon (node &optional optional defaultval)pg-pgip-get-icon177,5502 (defsubst pg-pgip-get-name (node &optional optional defaultval)pg-pgip-get-name181,5650 (defsubst pg-pgip-get-version (node &optional optional defaultval)pg-pgip-get-version184,5767 (defsubst pg-pgip-get-descr (node &optional optional defaultval)pg-pgip-get-descr187,5890 (defsubst pg-pgip-get-thmname (node &optional optional defaultval)pg-pgip-get-thmname190,6009 (defsubst pg-pgip-get-thyname (node &optional optional defaultval)pg-pgip-get-thyname193,6132 (defsubst pg-pgip-get-url (node &optional optional defaultval)pg-pgip-get-url196,6255 (defsubst pg-pgip-get-srcid (node &optional optional defaultval)pg-pgip-get-srcid199,6370 (defsubst pg-pgip-get-proverid (node &optional optional defaultval)pg-pgip-get-proverid202,6489 (defsubst pg-pgip-get-symname (node &optional optional defaultval)pg-pgip-get-symname205,6614 (defsubst pg-pgip-get-prefcat (node &optional optional defaultval)pg-pgip-get-prefcat208,6734 (defsubst pg-pgip-get-default (node &optional optional defaultval)pg-pgip-get-default211,6862 (defsubst pg-pgip-get-objtype (node &optional optional defaultval)pg-pgip-get-objtype214,6985 (defsubst pg-pgip-get-value (node)pg-pgip-get-value217,7108 (defalias 'pg-pgip-get-displaytext 'pg-pgip-get-pgmltext)pg-pgip-get-displaytext220,7178 (defun pg-pgip-get-pgmltext (node)pg-pgip-get-pgmltext222,7237 generic/proof-autoloads.el,180 (defsubst proof-shell-live-buffer nil "\proof-shell-live-buffer687,22209 (defsubst proof-replace-regexp-in-string (regexp rep string) "\proof-replace-regexp-in-string840,27709 generic/proof-auxmodes.el,257 (defun proof-mmm-support-available ()proof-mmm-support-available20,495 (defun proof-maths-menu-support-available ()proof-maths-menu-support-available44,1114 (defun proof-unicode-tokens-support-available ()proof-unicode-tokens-support-available58,1531 generic/proof-config.el,12929 (defgroup prover-config nilprover-config80,2632 (defcustom proof-guess-command-line nilproof-guess-command-line98,3482 (defcustom proof-assistant-home-page ""proof-assistant-home-page113,3977 (defcustom proof-context-command nilproof-context-command119,4147 (defcustom proof-info-command nilproof-info-command124,4281 (defcustom proof-showproof-command nilproof-showproof-command131,4552 (defcustom proof-goal-command nilproof-goal-command136,4688 (defcustom proof-save-command nilproof-save-command144,4985 (defcustom proof-find-theorems-command nilproof-find-theorems-command152,5294 (defcustom proof-query-identifier-command nilproof-query-identifier-command159,5602 (defcustom proof-assistant-true-value "true"proof-assistant-true-value173,6291 (defcustom proof-assistant-false-value "false"proof-assistant-false-value179,6481 (defcustom proof-assistant-format-int-fn 'int-to-stringproof-assistant-format-int-fn185,6675 (defcustom proof-assistant-format-float-fn 'number-to-stringproof-assistant-format-float-fn192,6924 (defcustom proof-assistant-format-string-fn (lambda (value) value)proof-assistant-format-string-fn199,7179 (defcustom proof-assistant-setting-format nilproof-assistant-setting-format206,7446 (defgroup proof-script nilproof-script228,8141 (defcustom proof-terminal-string nilproof-terminal-string233,8271 (defcustom proof-electric-terminator-noterminator nilproof-electric-terminator-noterminator243,8659 (defcustom proof-script-sexp-commands nilproof-script-sexp-commands248,8831 (defcustom proof-script-command-end-regexp nilproof-script-command-end-regexp259,9290 (defcustom proof-script-command-start-regexp nilproof-script-command-start-regexp277,10111 (defcustom proof-script-integral-proofs nilproof-script-integral-proofs288,10574 (defcustom proof-script-fly-past-comments nilproof-script-fly-past-comments303,11230 (defcustom proof-script-parse-function nilproof-script-parse-function308,11401 (defcustom proof-script-comment-start ""proof-script-comment-start326,12046 (defcustom proof-script-comment-start-regexp nilproof-script-comment-start-regexp337,12483 (defcustom proof-script-comment-end ""proof-script-comment-end345,12802 (defcustom proof-script-comment-end-regexp nilproof-script-comment-end-regexp357,13224 (defcustom proof-string-start-regexp "\""proof-string-start-regexp365,13537 (defcustom proof-string-end-regexp "\""proof-string-end-regexp370,13702 (defcustom proof-case-fold-search nilproof-case-fold-search375,13863 (defcustom proof-save-command-regexp nilproof-save-command-regexp384,14275 (defcustom proof-save-with-hole-regexp nilproof-save-with-hole-regexp389,14385 (defcustom proof-save-with-hole-result 2proof-save-with-hole-result400,14760 (defcustom proof-goal-command-regexp nilproof-goal-command-regexp410,15200 (defcustom proof-goal-with-hole-regexp nilproof-goal-with-hole-regexp418,15487 (defcustom proof-goal-with-hole-result 2proof-goal-with-hole-result430,15930 (defcustom proof-non-undoables-regexp nilproof-non-undoables-regexp439,16304 (defcustom proof-nested-undo-regexp nilproof-nested-undo-regexp450,16759 (defcustom proof-ignore-for-undo-count nilproof-ignore-for-undo-count466,17471 (defcustom proof-script-imenu-generic-expression nilproof-script-imenu-generic-expression474,17774 (defcustom proof-goal-command-p 'proof-generic-goal-command-pproof-goal-command-p482,18113 (defcustom proof-really-save-command-p (lambda (span cmd) t)proof-really-save-command-p493,18604 (defcustom proof-completed-proof-behaviour nilproof-completed-proof-behaviour502,18911 (defcustom proof-count-undos-fn 'proof-generic-count-undosproof-count-undos-fn530,20260 (defcustom proof-find-and-forget-fn 'proof-generic-find-and-forgetproof-find-and-forget-fn542,20811 (defcustom proof-forget-id-command nilproof-forget-id-command559,21520 (defcustom pg-topterm-goalhyplit-fn nilpg-topterm-goalhyplit-fn569,21878 (defcustom proof-kill-goal-command nilproof-kill-goal-command581,22413 (defcustom proof-undo-n-times-cmd nilproof-undo-n-times-cmd595,22917 (defcustom proof-nested-goals-history-p nilproof-nested-goals-history-p609,23454 (defcustom proof-arbitrary-undo-positions nilproof-arbitrary-undo-positions618,23791 (defcustom proof-state-preserving-p 'proof-generic-state-preserving-pproof-state-preserving-p632,24372 (defcustom proof-activate-scripting-hook nilproof-activate-scripting-hook642,24844 (defcustom proof-deactivate-scripting-hook nilproof-deactivate-scripting-hook661,25625 (defcustom proof-no-fully-processed-buffer nilproof-no-fully-processed-buffer670,25955 (defcustom proof-script-evaluate-elisp-comment-regexp "ELISP: -- \\(.*\\) --"proof-script-evaluate-elisp-comment-regexp681,26453 (defcustom proof-indent 2proof-indent699,27039 (defcustom proof-indent-hang nilproof-indent-hang704,27146 (defcustom proof-indent-enclose-offset 1proof-indent-enclose-offset709,27272 (defcustom proof-indent-open-offset 1proof-indent-open-offset714,27414 (defcustom proof-indent-close-offset 1proof-indent-close-offset719,27551 (defcustom proof-indent-any-regexp "\\s(\\|\\s)"proof-indent-any-regexp724,27689 (defcustom proof-indent-inner-regexp nilproof-indent-inner-regexp729,27849 (defcustom proof-indent-enclose-regexp nilproof-indent-enclose-regexp734,28003 (defcustom proof-indent-open-regexp "\\s("proof-indent-open-regexp739,28157 (defcustom proof-indent-close-regexp "\\s)"proof-indent-close-regexp744,28309 (defcustom proof-script-font-lock-keywords nilproof-script-font-lock-keywords750,28463 (defcustom proof-script-syntax-table-entries nilproof-script-syntax-table-entries758,28815 (defcustom proof-script-span-context-menu-extensions nilproof-script-span-context-menu-extensions776,29211 (defgroup proof-shell nilproof-shell802,29971 (defcustom proof-prog-name nilproof-prog-name812,30141 (defcustom proof-shell-auto-terminate-commands tproof-shell-auto-terminate-commands824,30608 (defcustom proof-shell-pre-sync-init-cmd nilproof-shell-pre-sync-init-cmd833,31013 (defcustom proof-shell-init-cmd nilproof-shell-init-cmd847,31571 (defcustom proof-shell-init-hook nilproof-shell-init-hook859,32117 (defcustom proof-shell-restart-cmd ""proof-shell-restart-cmd864,32256 (defcustom proof-shell-quit-cmd nilproof-shell-quit-cmd869,32411 (defcustom proof-shell-cd-cmd nilproof-shell-cd-cmd874,32578 (defcustom proof-shell-start-silent-cmd nilproof-shell-start-silent-cmd891,33249 (defcustom proof-shell-stop-silent-cmd nilproof-shell-stop-silent-cmd900,33625 (defcustom proof-shell-silent-threshold 2proof-shell-silent-threshold909,33960 (defcustom proof-shell-inform-file-processed-cmd nilproof-shell-inform-file-processed-cmd917,34294 (defcustom proof-shell-inform-file-retracted-cmd nilproof-shell-inform-file-retracted-cmd938,35222 (defcustom proof-auto-multiple-files nilproof-auto-multiple-files966,36494 (defcustom proof-cannot-reopen-processed-files nilproof-cannot-reopen-processed-files981,37215 (defcustom proof-shell-require-command-regexp nilproof-shell-require-command-regexp995,37881 (defcustom proof-done-advancing-require-function nilproof-done-advancing-require-function1006,38343 (defcustom proof-shell-annotated-prompt-regexp nilproof-shell-annotated-prompt-regexp1018,38703 (defcustom proof-shell-error-regexp nilproof-shell-error-regexp1033,39268 (defcustom proof-shell-truncate-before-error tproof-shell-truncate-before-error1053,40070 (defcustom pg-next-error-regexp nilpg-next-error-regexp1067,40609 (defcustom pg-next-error-filename-regexp nilpg-next-error-filename-regexp1082,41218 (defcustom pg-next-error-extract-filename nilpg-next-error-extract-filename1106,42251 (defcustom proof-shell-interrupt-regexp nilproof-shell-interrupt-regexp1113,42494 (defcustom proof-shell-proof-completed-regexp nilproof-shell-proof-completed-regexp1127,43089 (defcustom proof-shell-clear-response-regexp nilproof-shell-clear-response-regexp1140,43597 (defcustom proof-shell-clear-goals-regexp nilproof-shell-clear-goals-regexp1152,44049 (defcustom proof-shell-start-goals-regexp nilproof-shell-start-goals-regexp1164,44495 (defcustom proof-shell-end-goals-regexp nilproof-shell-end-goals-regexp1172,44862 (defcustom proof-shell-eager-annotation-start nilproof-shell-eager-annotation-start1186,45435 (defcustom proof-shell-eager-annotation-start-length 10proof-shell-eager-annotation-start-length1209,46454 (defcustom proof-shell-eager-annotation-end "\n"proof-shell-eager-annotation-end1220,46880 (defcustom proof-shell-strip-output-markup 'identityproof-shell-strip-output-markup1236,47555 (defcustom proof-shell-assumption-regexp nilproof-shell-assumption-regexp1245,47940 (defcustom proof-shell-process-file nilproof-shell-process-file1255,48344 (defcustom proof-shell-retract-files-regexp nilproof-shell-retract-files-regexp1281,49420 (defcustom proof-shell-compute-new-files-list nilproof-shell-compute-new-files-list1294,49908 (defcustom pg-special-char-regexp "[\200-\377]"pg-special-char-regexp1309,50475 (defcustom proof-shell-set-elisp-variable-regexp nilproof-shell-set-elisp-variable-regexp1314,50619 (defcustom proof-shell-match-pgip-cmd nilproof-shell-match-pgip-cmd1352,52285 (defcustom proof-shell-issue-pgip-cmd nilproof-shell-issue-pgip-cmd1366,52767 (defcustom proof-use-pgip-askprefs nilproof-use-pgip-askprefs1371,52932 (defcustom proof-shell-query-dependencies-cmd nilproof-shell-query-dependencies-cmd1379,53279 (defcustom proof-shell-theorem-dependency-list-regexp nilproof-shell-theorem-dependency-list-regexp1386,53539 (defcustom proof-shell-theorem-dependency-list-split nilproof-shell-theorem-dependency-list-split1402,54199 (defcustom proof-shell-show-dependency-cmd nilproof-shell-show-dependency-cmd1411,54622 (defcustom proof-shell-trace-output-regexp nilproof-shell-trace-output-regexp1433,55528 (defcustom proof-shell-thms-output-regexp nilproof-shell-thms-output-regexp1451,56122 (defcustom proof-tokens-activate-command nilproof-tokens-activate-command1464,56505 (defcustom proof-tokens-deactivate-command nilproof-tokens-deactivate-command1471,56745 (defcustom proof-tokens-extra-modes nilproof-tokens-extra-modes1478,56990 (defcustom proof-shell-unicode tproof-shell-unicode1493,57495 (defcustom proof-shell-filename-escapes nilproof-shell-filename-escapes1502,57885 (defcustom proof-shell-process-connection-type tproof-shell-process-connection-type1519,58565 (defcustom proof-shell-strip-crs-from-input tproof-shell-strip-crs-from-input1525,58756 (defcustom proof-shell-strip-crs-from-output (eq system-type 'cygwin32)proof-shell-strip-crs-from-output1537,59239 (defcustom proof-shell-extend-queue-hook nilproof-shell-extend-queue-hook1545,59607 (defcustom proof-shell-insert-hook nilproof-shell-insert-hook1555,60037 (defcustom proof-script-preprocess nilproof-script-preprocess1596,61997 (defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook1602,62148 (defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook1608,62363 (defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook1626,63109 (defcustom proof-shell-handle-output-system-specific nilproof-shell-handle-output-system-specific1634,63380 (defcustom proof-state-change-hook nilproof-state-change-hook1657,64353 (defcustom proof-shell-syntax-table-entries nilproof-shell-syntax-table-entries1667,64746 (defgroup proof-goals nilproof-goals1685,65117 (defcustom pg-subterm-first-special-char nilpg-subterm-first-special-char1690,65238 (defcustom pg-subterm-anns-use-stack nilpg-subterm-anns-use-stack1698,65550 (defcustom pg-goals-change-goal nilpg-goals-change-goal1707,65849 (defcustom pbp-goal-command nilpbp-goal-command1712,65965 (defcustom pbp-hyp-command nilpbp-hyp-command1717,66121 (defcustom pg-subterm-help-cmd nilpg-subterm-help-cmd1722,66283 (defcustom pg-goals-error-regexp nilpg-goals-error-regexp1729,66519 (defcustom proof-shell-result-start nilproof-shell-result-start1734,66679 (defcustom proof-shell-result-end ""proof-shell-result-end1740,66913 (defcustom pg-subterm-start-char nilpg-subterm-start-char1746,67126 (defcustom pg-subterm-sep-char nilpg-subterm-sep-char1757,67600 (defcustom pg-subterm-end-char nilpg-subterm-end-char1763,67779 (defcustom pg-topterm-regexp nilpg-topterm-regexp1769,67936 (defcustom proof-goals-font-lock-keywords nilproof-goals-font-lock-keywords1784,68536 (defcustom proof-response-font-lock-keywords nilproof-response-font-lock-keywords1792,68895 (defcustom proof-shell-font-lock-keywords nilproof-shell-font-lock-keywords1800,69257 (defcustom pg-before-fontify-output-hook nilpg-before-fontify-output-hook1811,69771 (defcustom pg-after-fontify-output-hook nilpg-after-fontify-output-hook1819,70132 generic/proof-depends.el,1643 (defvar proof-thm-names-of-files nilproof-thm-names-of-files25,639 (defvar proof-def-names-of-files nilproof-def-names-of-files31,923 (defun proof-depends-module-name-for-buffer ()proof-depends-module-name-for-buffer42,1238 (defun proof-depends-module-of (name)proof-depends-module-of52,1679 (defun proof-depends-names-in-same-file (names)proof-depends-names-in-same-file60,1970 (defun proof-depends-process-dependencies (name gspan)proof-depends-process-dependencies79,2578 (defun proof-dependency-in-span-context-menu (span)proof-dependency-in-span-context-menu132,4313 (defun proof-dep-alldeps-menu (span)proof-dep-alldeps-menu155,5203 (defun proof-dep-make-alldeps-menu (deps)proof-dep-make-alldeps-menu161,5429 (defun proof-dep-split-deps (deps)proof-dep-split-deps179,5924 (defun proof-dep-make-submenu (name namefn appfn list)proof-dep-make-submenu198,6590 (defun proof-make-highlight-depts-menu (name fn span prop)proof-make-highlight-depts-menu209,7001 (defun proof-goto-dependency (name span)proof-goto-dependency220,7309 (defun proof-show-dependency (thm)proof-show-dependency227,7561 (defconst pg-dep-span-priority 500)pg-dep-span-priority234,7850 (defconst pg-ordinary-span-priority 100)pg-ordinary-span-priority235,7886 (defun proof-highlight-depcs (name nmspans)proof-highlight-depcs237,7928 (defun proof-highlight-depts (name nmspans)proof-highlight-depts248,8394 (defun proof-depends-save-old-face (span)proof-depends-save-old-face260,8904 (defun proof-depends-restore-old-face (span)proof-depends-restore-old-face265,9081 (defun proof-dep-unhighlight ()proof-dep-unhighlight271,9310 generic/proof-easy-config.el,350 (defconst proof-easy-config-derived-modes-tableproof-easy-config-derived-modes-table16,544 (defun proof-easy-config-define-derived-modes ()proof-easy-config-define-derived-modes23,950 (defun proof-easy-config-check-setup (sym name)proof-easy-config-check-setup52,2135 (defmacro proof-easy-config (sym name &rest body)proof-easy-config84,3465 generic/proof.el,0 generic/proof-faces.el,3822 (defgroup proof-faces nilproof-faces29,809 (defconst pg-defface-window-systemspg-defface-window-systems36,989 (defmacro proof-face-specs (bl bd ow)proof-face-specs49,1551 (defface proof-queue-faceproof-queue-face64,2003 (defface proof-locked-faceproof-locked-face72,2281 (defface proof-declaration-name-faceproof-declaration-name-face82,2602 (defface proof-tacticals-name-faceproof-tacticals-name-face91,2888 (defface proof-tactics-name-faceproof-tactics-name-face100,3150 (defface proof-error-faceproof-error-face109,3415 (defface proof-warning-faceproof-warning-face117,3636 (defface proof-eager-annotation-faceproof-eager-annotation-face126,3893 (defface proof-debug-message-faceproof-debug-message-face134,4111 (defface proof-boring-faceproof-boring-face142,4310 (defface proof-mouse-highlight-faceproof-mouse-highlight-face150,4502 (defface proof-command-mouse-highlight-faceproof-command-mouse-highlight-face158,4720 (defface proof-region-mouse-highlight-faceproof-region-mouse-highlight-face166,4959 (defface proof-highlight-dependent-faceproof-highlight-dependent-face174,5201 (defface proof-highlight-dependency-faceproof-highlight-dependency-face182,5408 (defface proof-active-area-faceproof-active-area-face190,5605 (defface proof-script-sticky-error-faceproof-script-sticky-error-face198,5917 (defface proof-script-highlight-error-faceproof-script-highlight-error-face206,6146 (defconst proof-face-compat-doc "Evaluates to a face name, for compatibility.")proof-face-compat-doc218,6491 (defconst proof-queue-face 'proof-queue-face proof-face-compat-doc)proof-queue-face219,6571 (defconst proof-locked-face 'proof-locked-face proof-face-compat-doc)proof-locked-face220,6639 (defconst proof-declaration-name-face 'proof-declaration-name-face proof-face-compat-doc)proof-declaration-name-face221,6709 (defconst proof-tacticals-name-face 'proof-tacticals-name-face proof-face-compat-doc)proof-tacticals-name-face222,6799 (defconst proof-tactics-name-face 'proof-tactics-name-face proof-face-compat-doc)proof-tactics-name-face223,6885 (defconst proof-error-face 'proof-error-face proof-face-compat-doc)proof-error-face224,6967 (defconst proof-script-sticky-error-face 'proof-script-sticky-error-face proof-face-compat-doc)proof-script-sticky-error-face225,7035 (defconst proof-script-highlight-error-face 'proof-script-highlight-error-face proof-face-compat-doc)proof-script-highlight-error-face226,7131 (defconst proof-warning-face 'proof-warning-face proof-face-compat-doc)proof-warning-face227,7233 (defconst proof-eager-annotation-face 'proof-eager-annotation-face proof-face-compat-doc)proof-eager-annotation-face228,7305 (defconst proof-debug-message-face 'proof-debug-message-face proof-face-compat-doc)proof-debug-message-face229,7395 (defconst proof-boring-face 'proof-boring-face proof-face-compat-doc)proof-boring-face230,7479 (defconst proof-mouse-highlight-face 'proof-mouse-highlight-face proof-face-compat-doc)proof-mouse-highlight-face231,7549 (defconst proof-command-mouse-highlight-face 'proof-command-mouse-highlight-face proof-face-compat-doc)proof-command-mouse-highlight-face232,7637 (defconst proof-region-mouse-highlight-face 'proof-region-mouse-highlight-face proof-face-compat-doc)proof-region-mouse-highlight-face233,7741 (defconst proof-highlight-dependent-face 'proof-highlight-dependent-face proof-face-compat-doc)proof-highlight-dependent-face234,7843 (defconst proof-highlight-dependency-face 'proof-highlight-dependency-face proof-face-compat-doc)proof-highlight-dependency-face235,7939 (defconst proof-active-area-face 'proof-active-area-face proof-face-compat-doc)proof-active-area-face236,8037 (defconst proof-script-error-face 'proof-script-errror-face-compat-doc)proof-script-error-face237,8117 generic/proof-indent.el,448 (defun proof-indent-indent ()proof-indent-indent19,449 (defun proof-indent-offset ()proof-indent-offset28,715 (defun proof-indent-inner-p ()proof-indent-inner-p45,1316 (defun proof-indent-goto-prev () ; Note: may change point, even in case of failure!proof-indent-goto-prev54,1616 (defun proof-indent-calculate (indent inner) ; Note: may change point!proof-indent-calculate61,1949 (defun proof-indent-line ()proof-indent-line82,2708 generic/proof-maths-menu.el,143 (defun proof-maths-menu-set-global (flag)proof-maths-menu-set-global32,906 (defun proof-maths-menu-enable ()proof-maths-menu-enable46,1357 generic/proof-menu.el,3776 (defvar proof-display-some-buffers-count 0)proof-display-some-buffers-count36,815 (defun proof-display-some-buffers ()proof-display-some-buffers38,860 (defun proof-menu-define-keys (map)proof-menu-define-keys95,2987 (defun proof-menu-define-main ()proof-menu-define-main153,5812 (defvar proof-menu-favourites nilproof-menu-favourites162,5997 (defvar proof-menu-settings nilproof-menu-settings165,6104 (defun proof-menu-define-specific ()proof-menu-define-specific169,6193 (defun proof-assistant-menu-update ()proof-assistant-menu-update212,7455 (defvar proof-help-menuproof-help-menu226,7888 (defvar proof-show-hide-menuproof-show-hide-menu234,8158 (defvar proof-buffer-menuproof-buffer-menu245,8582 (defun proof-keep-response-history ()proof-keep-response-history308,10898 (defconst proof-quick-opts-menuproof-quick-opts-menu316,11208 (defun proof-quick-opts-vars ()proof-quick-opts-vars534,20114 (defun proof-quick-opts-changed-from-defaults-p ()proof-quick-opts-changed-from-defaults-p566,21054 (defun proof-quick-opts-changed-from-saved-p ()proof-quick-opts-changed-from-saved-p570,21159 (defun proof-set-document-centred ()proof-set-document-centred578,21315 (defun proof-set-non-document-centred ()proof-set-non-document-centred591,21741 (defun proof-quick-opts-save ()proof-quick-opts-save610,22452 (defun proof-quick-opts-reset ()proof-quick-opts-reset615,22620 (defconst proof-config-menuproof-config-menu627,22888 (defconst proof-advanced-menuproof-advanced-menu634,23067 (defvar proof-menuproof-menu652,23751 (defun proof-main-menu ()proof-main-menu661,24033 (defun proof-aux-menu ()proof-aux-menu673,24372 (defun proof-menu-define-favourites-menu ()proof-menu-define-favourites-menu689,24718 (defun proof-def-favourite (command inscript menuname &optional key new)proof-def-favourite709,25367 (defvar proof-make-favourite-cmd-history nilproof-make-favourite-cmd-history736,26360 (defvar proof-make-favourite-menu-history nilproof-make-favourite-menu-history739,26445 (defun proof-save-favourites ()proof-save-favourites742,26531 (defun proof-del-favourite (menuname)proof-del-favourite747,26679 (defun proof-read-favourite ()proof-read-favourite764,27235 (defun proof-add-favourite (command inscript menuname &optional key)proof-add-favourite788,28009 (defun proof-menu-define-settings-menu ()proof-menu-define-settings-menu815,29054 (defun proof-menu-entry-name (symbol)proof-menu-entry-name844,30046 (defun proof-menu-entry-for-setting (symbol setting type descr)proof-menu-entry-for-setting854,30396 (defun proof-settings-vars ()proof-settings-vars877,31034 (defun proof-settings-changed-from-defaults-p ()proof-settings-changed-from-defaults-p882,31211 (defun proof-settings-changed-from-saved-p ()proof-settings-changed-from-saved-p886,31317 (defun proof-settings-save ()proof-settings-save890,31420 (defun proof-settings-reset ()proof-settings-reset895,31587 (defun proof-assistant-invisible-command-ifposs (cmd)proof-assistant-invisible-command-ifposs900,31750 (defun proof-maybe-askprefs ()proof-maybe-askprefs922,32720 (defun proof-assistant-settings-cmd (setting)proof-assistant-settings-cmd928,32913 (defun proof-assistant-settings-cmds ()proof-assistant-settings-cmds936,33197 (defvar proof-assistant-format-tableproof-assistant-format-table946,33539 (defun proof-assistant-format-bool (value)proof-assistant-format-bool955,33965 (defun proof-assistant-format-int (value)proof-assistant-format-int958,34078 (defun proof-assistant-format-float (value)proof-assistant-format-float961,34170 (defun proof-assistant-format-string (value)proof-assistant-format-string964,34266 (defun proof-assistant-format (string curvalue)proof-assistant-format967,34364 generic/proof-mmm.el,116 (defun proof-mmm-set-global (flag)proof-mmm-set-global43,1439 (defun proof-mmm-enable ()proof-mmm-enable58,1978 generic/proof-script.el,10148 (deflocal proof-active-buffer-fake-minor-mode nilproof-active-buffer-fake-minor-mode46,1413 (deflocal proof-script-buffer-file-name nilproof-script-buffer-file-name49,1539 (deflocal pg-script-portions nilpg-script-portions56,1949 (defun proof-next-element-count (idiom)proof-next-element-count66,2169 (defun proof-element-id (idiom number)proof-element-id72,2411 (defun proof-next-element-id (idiom)proof-next-element-id76,2580 (deflocal proof-locked-span nilproof-locked-span112,3884 (deflocal proof-queue-span nilproof-queue-span119,4150 (deflocal proof-overlay-arrow nilproof-overlay-arrow128,4636 (defun proof-span-give-warning (&rest args)proof-span-give-warning134,4763 (defun proof-span-read-only (span &optional always)proof-span-read-only140,4943 (defun proof-strict-read-only ()proof-strict-read-only149,5316 (defsubst proof-set-queue-endpoints (start end)proof-set-queue-endpoints159,5694 (defun proof-set-overlay-arrow (pos)proof-set-overlay-arrow163,5835 (defsubst proof-set-locked-endpoints (start end)proof-set-locked-endpoints174,6173 (defsubst proof-detach-queue ()proof-detach-queue179,6349 (defsubst proof-detach-locked ()proof-detach-locked184,6488 (defsubst proof-set-queue-start (start)proof-set-queue-start191,6713 (defsubst proof-set-locked-end (end)proof-set-locked-end195,6839 (defsubst proof-set-queue-end (end)proof-set-queue-end207,7309 (defun proof-init-segmentation ()proof-init-segmentation218,7606 (defun proof-colour-locked ()proof-colour-locked248,8857 (defun proof-colour-locked-span ()proof-colour-locked-span255,9130 (defun proof-sticky-errors ()proof-sticky-errors261,9403 (defun proof-restart-buffers (buffers)proof-restart-buffers274,9819 (defun proof-script-buffers-with-spans ()proof-script-buffers-with-spans296,10638 (defun proof-script-remove-all-spans-and-deactivate ()proof-script-remove-all-spans-and-deactivate306,10994 (defun proof-script-clear-queue-spans-on-error (badspan &optional interruptp)proof-script-clear-queue-spans-on-error310,11184 (defun proof-script-delete-spans (beg end)proof-script-delete-spans336,12201 (defun proof-script-delete-secondary-spans (beg end)proof-script-delete-secondary-spans341,12400 (defun proof-unprocessed-begin ()proof-unprocessed-begin354,12689 (defun proof-script-end ()proof-script-end362,12943 (defun proof-queue-or-locked-end ()proof-queue-or-locked-end371,13253 (defun proof-locked-region-full-p ()proof-locked-region-full-p390,13846 (defun proof-locked-region-empty-p ()proof-locked-region-empty-p399,14118 (defun proof-only-whitespace-to-locked-region-p ()proof-only-whitespace-to-locked-region-p403,14268 (defun proof-in-locked-region-p ()proof-in-locked-region-p413,14617 (defun proof-goto-end-of-locked (&optional switch)proof-goto-end-of-locked425,14874 (defun proof-goto-end-of-locked-if-pos-not-visible-in-window ()proof-goto-end-of-locked-if-pos-not-visible-in-window442,15633 (defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window ()proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window453,16114 (defun proof-end-of-locked-visible-p ()proof-end-of-locked-visible-p465,16654 (defconst pg-idioms '(proof)pg-idioms484,17247 (defconst pg-all-idioms (append pg-idiomspg-all-idioms487,17343 (defun pg-clear-script-portions ()pg-clear-script-portions491,17464 (defun pg-remove-element (idiom id)pg-remove-element497,17699 (defun pg-get-element (idiomsym id)pg-get-element505,18002 (defun pg-add-element (idiomsym id span &optional name)pg-add-element515,18317 (defun pg-invisible-prop (idiom)pg-invisible-prop563,20279 (defun pg-set-element-span-invisible (span invisiblep)pg-set-element-span-invisible568,20480 (defun pg-toggle-element-span-visibility (span)pg-toggle-element-span-visibility581,21046 (defun pg-open-invisible-span (span &optional invisible)pg-open-invisible-span586,21207 (defun pg-make-element-invisible (idiomsym id)pg-make-element-invisible591,21378 (defun pg-make-element-visible (idiomsym id)pg-make-element-visible596,21589 (defun pg-toggle-element-visibility (idiomsym id)pg-toggle-element-visibility601,21783 (defun pg-show-all-portions (idiom &optional hide)pg-show-all-portions607,22046 (defun pg-show-all-proofs ()pg-show-all-proofs629,22790 (defun pg-hide-all-proofs ()pg-hide-all-proofs634,22918 (defun pg-add-proof-element (name span controlspan)pg-add-proof-element639,23049 (defun pg-span-name (span)pg-span-name654,23836 (defvar pg-span-context-menu-keymappg-span-context-menu-keymap687,25043 (defun pg-last-output-displayform ()pg-last-output-displayform694,25281 (defun pg-set-span-helphighlights (span &optional mouseface face)pg-set-span-helphighlights717,26172 (defun proof-complete-buffer-atomic (buffer)proof-complete-buffer-atomic775,28149 (defun proof-register-possibly-new-processed-fileproof-register-possibly-new-processed-file804,29419 (defun proof-query-save-this-buffer-p ()proof-query-save-this-buffer-p850,31293 (defun proof-inform-prover-file-retracted (rfile)proof-inform-prover-file-retracted855,31518 (defun proof-auto-retract-dependencies (cfile &optional informprover)proof-auto-retract-dependencies875,32369 (defun proof-unregister-buffer-file-name (&optional informprover)proof-unregister-buffer-file-name929,34919 (defsubst proof-action-completed (action)proof-action-completed975,36744 (defun proof-protected-process-or-retract (action &optional buffer)proof-protected-process-or-retract979,36914 (defun proof-deactivate-scripting-auto ()proof-deactivate-scripting-auto1007,38145 (defun proof-deactivate-scripting-query-user-action ()proof-deactivate-scripting-query-user-action1016,38503 (defun proof-deactivate-scripting-choose-action ()proof-deactivate-scripting-choose-action1060,40012 (defun proof-deactivate-scripting (&optional forcedaction)proof-deactivate-scripting1072,40397 (defun proof-activate-scripting (&optional nosaves queuemode)proof-activate-scripting1169,44520 (defun proof-toggle-active-scripting (&optional arg)proof-toggle-active-scripting1269,49045 (defun proof-done-advancing (span)proof-done-advancing1308,50290 (defun proof-done-advancing-comment (span)proof-done-advancing-comment1387,53275 (defun proof-done-advancing-save (span)proof-done-advancing-save1421,54661 (defun proof-make-goalsaveproof-make-goalsave1509,58025 (defun proof-get-name-from-goal (gspan)proof-get-name-from-goal1527,58890 (defun proof-done-advancing-autosave (span)proof-done-advancing-autosave1547,59915 (defun proof-done-advancing-other (span)proof-done-advancing-other1611,62411 (defun proof-segment-up-to-parser (pos &optional next-command-end)proof-segment-up-to-parser1640,63375 (defun proof-script-generic-parse-find-comment-end ()proof-script-generic-parse-find-comment-end1709,65641 (defun proof-script-generic-parse-cmdend ()proof-script-generic-parse-cmdend1718,66055 (defun proof-script-generic-parse-cmdstart ()proof-script-generic-parse-cmdstart1769,67951 (defun proof-script-generic-parse-sexp ()proof-script-generic-parse-sexp1808,69551 (defun proof-semis-to-vanillas (semis &optional queueflags)proof-semis-to-vanillas1820,70017 (defun proof-next-command-new-line ()proof-next-command-new-line1873,71690 (defun proof-script-next-command-advance ()proof-script-next-command-advance1878,71896 (defun proof-assert-until-point (&optional displayflags)proof-assert-until-point1897,72396 (defun proof-assert-electric-terminator ()proof-assert-electric-terminator1912,73023 (defun proof-assert-semis (semis &optional displayflags)proof-assert-semis1955,74655 (defun proof-retract-before-change (beg end)proof-retract-before-change1969,75396 (defun proof-insert-pbp-command (cmd)proof-insert-pbp-command1989,75992 (defun proof-insert-sendback-command (cmd)proof-insert-sendback-command2004,76495 (defun proof-done-retracting (span)proof-done-retracting2030,77398 (defun proof-setup-retract-action (start end proof-commands remove-action &optional proof-setup-retract-action2065,78852 (defun proof-last-goal-or-goalsave ()proof-last-goal-or-goalsave2077,79457 (defun proof-retract-target (target undo-action displayflags)proof-retract-target2101,80369 (defun proof-retract-until-point-interactive (&optional delete-region)proof-retract-until-point-interactive2180,83622 (defun proof-retract-until-point (&optional undo-action displayflags)proof-retract-until-point2189,84029 (define-derived-mode proof-mode fundamental-modeproof-mode2244,86037 (defun proof-script-set-visited-file-name ()proof-script-set-visited-file-name2280,87419 (defun proof-script-set-buffer-hooks ()proof-script-set-buffer-hooks2302,88432 (defun proof-script-kill-buffer-fn ()proof-script-kill-buffer-fn2310,88850 (defun proof-config-done-related ()proof-config-done-related2342,90167 (defun proof-generic-goal-command-p (span)proof-generic-goal-command-p2407,92652 (defun proof-generic-state-preserving-p (cmd)proof-generic-state-preserving-p2412,92865 (defun proof-generic-count-undos (span)proof-generic-count-undos2421,93382 (defun proof-generic-find-and-forget (span)proof-generic-find-and-forget2452,94510 (defconst proof-script-important-settingsproof-script-important-settings2503,96282 (defun proof-config-done ()proof-config-done2518,96828 (defun proof-setup-parsing-mechanism ()proof-setup-parsing-mechanism2585,98993 (defun proof-setup-imenu ()proof-setup-imenu2609,100065 (deflocal proof-segment-up-to-cache nil)proof-segment-up-to-cache2636,100843 (deflocal proof-segment-up-to-cache-start 0)proof-segment-up-to-cache-start2637,100884 (deflocal proof-last-edited-low-watermark nil)proof-last-edited-low-watermark2638,100929 (defun proof-segment-up-to-using-cache (pos &rest args)proof-segment-up-to-using-cache2648,101416 (defun proof-segment-cache-contents-for (pos)proof-segment-cache-contents-for2676,102418 (defun proof-script-after-change-function (start end prelength)proof-script-after-change-function2688,102787 (defun proof-script-set-after-change-functions ()proof-script-set-after-change-functions2700,103294 generic/proof-shell.el,6424 (defvar proof-marker nilproof-marker34,746 (defvar proof-action-list nilproof-action-list37,842 (defsubst proof-shell-invoke-callback (listitem)proof-shell-invoke-callback75,2315 (defvar proof-shell-last-goals-output ""proof-shell-last-goals-output89,2807 (defvar proof-shell-last-response-output ""proof-shell-last-response-output92,2887 (defvar proof-shell-delayed-output-start nilproof-shell-delayed-output-start95,2974 (defvar proof-shell-delayed-output-end nilproof-shell-delayed-output-end99,3156 (defvar proof-shell-delayed-output-flags nilproof-shell-delayed-output-flags103,3336 (defvar proof-shell-interrupt-pending nilproof-shell-interrupt-pending106,3461 (defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator117,3756 (defun proof-shell-ready-prover (&optional queuemode)proof-shell-ready-prover169,5340 (defsubst proof-shell-live-buffer ()proof-shell-live-buffer183,5879 (defun proof-shell-available-p ()proof-shell-available-p190,6099 (defun proof-grab-lock (&optional queuemode)proof-grab-lock196,6321 (defun proof-release-lock ()proof-release-lock206,6750 (defcustom proof-shell-fiddle-frames tproof-shell-fiddle-frames216,6924 (defun proof-shell-set-text-representation ()proof-shell-set-text-representation221,7082 (defun proof-shell-start ()proof-shell-start229,7410 (defvar proof-shell-kill-function-hooks nilproof-shell-kill-function-hooks412,13646 (defun proof-shell-kill-function ()proof-shell-kill-function415,13744 (defun proof-shell-clear-state ()proof-shell-clear-state476,15862 (defun proof-shell-exit (&optional dont-ask)proof-shell-exit492,16337 (defun proof-shell-bail-out (process event)proof-shell-bail-out512,17109 (defun proof-shell-restart ()proof-shell-restart522,17631 (defvar proof-shell-urgent-message-marker nilproof-shell-urgent-message-marker563,19003 (defvar proof-shell-urgent-message-scanner nilproof-shell-urgent-message-scanner566,19124 (defun proof-shell-handle-error-output (start-regexp append-face)proof-shell-handle-error-output570,19309 (defun proof-shell-handle-error-or-interrupt (err-or-int flags)proof-shell-handle-error-or-interrupt596,20171 (defun proof-shell-error-or-interrupt-action (err-or-int)proof-shell-error-or-interrupt-action639,21920 (defun proof-goals-pos (span maparg)proof-goals-pos666,23017 (defun proof-pbp-focus-on-first-goal ()proof-pbp-focus-on-first-goal671,23228 (defsubst proof-shell-string-match-safe (regexp string)proof-shell-string-match-safe683,23644 (defun proof-shell-handle-immediate-output (cmd start end flags)proof-shell-handle-immediate-output687,23805 (defun proof-interrupt-process ()proof-interrupt-process754,26412 (defun proof-shell-insert (strings action &optional scriptspan)proof-shell-insert788,27645 (defun proof-shell-action-list-item (cmd callback &optional flags)proof-shell-action-list-item839,29471 (defun proof-shell-set-silent (span)proof-shell-set-silent844,29713 (defun proof-shell-start-silent-item ()proof-shell-start-silent-item850,29932 (defun proof-shell-clear-silent (span)proof-shell-clear-silent856,30121 (defun proof-shell-stop-silent-item ()proof-shell-stop-silent-item862,30343 (defsubst proof-shell-should-be-silent ()proof-shell-should-be-silent868,30532 (defsubst proof-shell-insert-action-item (item)proof-shell-insert-action-item879,31042 (defsubst proof-shell-slurp-comments ()proof-shell-slurp-comments883,31217 (defun proof-add-to-queue (queueitems &optional queuemode)proof-add-to-queue894,31622 (defun proof-start-queue (start end queueitems &optional queuemode)proof-start-queue952,33646 (defun proof-extend-queue (end queueitems)proof-extend-queue964,34041 (defun proof-shell-exec-loop ()proof-shell-exec-loop983,34660 (defun proof-shell-insert-loopback-cmd (cmd)proof-shell-insert-loopback-cmd1051,36963 (defun proof-shell-process-urgent-message (start end)proof-shell-process-urgent-message1076,38127 (defun proof-shell-process-urgent-message-default (start end)proof-shell-process-urgent-message-default1125,39847 (defun proof-shell-process-urgent-message-trace (start end)proof-shell-process-urgent-message-trace1141,40431 (defun proof-shell-process-urgent-message-retract (start end)proof-shell-process-urgent-message-retract1154,40990 (defun proof-shell-process-urgent-message-elisp ()proof-shell-process-urgent-message-elisp1175,41838 (defun proof-shell-process-urgent-message-thmdeps ()proof-shell-process-urgent-message-thmdeps1190,42333 (defun proof-shell-strip-eager-annotations (start end)proof-shell-strip-eager-annotations1204,42712 (defun proof-shell-filter (str)proof-shell-filter1220,43212 (defun proof-shell-filter-first-command ()proof-shell-filter-first-command1320,46584 (defun proof-shell-process-urgent-messages ()proof-shell-process-urgent-messages1335,47127 (defun proof-shell-filter-manage-output (start end)proof-shell-filter-manage-output1385,48693 (defsubst proof-shell-display-output-as-response (flags str)proof-shell-display-output-as-response1417,49940 (defun proof-shell-handle-delayed-output ()proof-shell-handle-delayed-output1423,50235 (defvar pg-last-tracing-output-time nilpg-last-tracing-output-time1518,53694 (defconst pg-slow-mode-duration 2pg-slow-mode-duration1521,53800 (defconst pg-fast-tracing-mode-threshold 50000pg-fast-tracing-mode-threshold1524,53882 (defvar pg-tracing-cleanup-timer nil)pg-tracing-cleanup-timer1527,54010 (defun pg-tracing-tight-loop ()pg-tracing-tight-loop1529,54049 (defun pg-finish-tracing-display ()pg-finish-tracing-display1572,55761 (defun proof-shell-wait (&optional interrupt-on-input timeoutsecs)proof-shell-wait1590,56125 (defun proof-done-invisible (span)proof-done-invisible1620,57336 (defun proof-shell-invisible-command (cmd &optional wait invisiblecallbackproof-shell-invisible-command1626,57506 (defun proof-shell-invisible-cmd-get-result (cmd)proof-shell-invisible-cmd-get-result1673,59098 (defun proof-shell-invisible-command-invisible-result (cmd)proof-shell-invisible-command-invisible-result1685,59534 (defun pg-insert-last-output-as-comment ()pg-insert-last-output-as-comment1705,60035 (define-derived-mode proof-shell-mode scomint-modeproof-shell-mode1724,60507 (defconst proof-shell-important-settingsproof-shell-important-settings1761,61534 (defun proof-shell-config-done ()proof-shell-config-done1767,61649 generic/proof-site.el,1113 (defconst proof-assistant-table-defaultproof-assistant-table-default26,771 (defconst proof-general-short-versionproof-general-short-version59,1766 (defconst proof-general-version-year "2010")proof-general-version-year65,1953 (defgroup proof-general nilproof-general72,2106 (defgroup proof-general-internals nilproof-general-internals77,2214 (defun proof-home-directory-fn ()proof-home-directory-fn90,2602 (defcustom proof-home-directoryproof-home-directory101,2974 (defcustom proof-images-directoryproof-images-directory110,3340 (defcustom proof-info-directoryproof-info-directory116,3542 (defcustom proof-assistant-tableproof-assistant-table145,4519 (defcustom proof-assistants nilproof-assistants182,5687 (defun proof-ready-for-assistant (assistantsym &optional assistant-name)proof-ready-for-assistant211,6841 (defvar proof-general-configured-provers proof-general-configured-provers263,9133 (defun proof-chose-prover (prompt)proof-chose-prover333,11656 (defun proofgeneral (prover)proofgeneral338,11788 (defun proof-visit-example-file (prover)proof-visit-example-file347,12106 generic/proof-splash.el,1738 (defcustom proof-splash-enable tproof-splash-enable34,1007 (defcustom proof-splash-time 8proof-splash-time39,1159 (defcustom proof-splash-contentsproof-splash-contents47,1443 (defconst proof-splash-startup-msgproof-splash-startup-msg91,3008 (defconst proof-splash-welcome "*Proof General Welcome*"proof-splash-welcome100,3386 (define-derived-mode proof-splash-mode fundamental-modeproof-splash-mode103,3490 (define-key proof-splash-mode-map "q" 'bury-buffer)proof-splash-mode-map109,3664 (define-key proof-splash-mode-map [mouse-3] 'bury-buffer)proof-splash-mode-map110,3716 (defsubst proof-emacs-imagep (img)proof-emacs-imagep115,3843 (defun proof-get-image (name &optional nojpeg default)proof-get-image120,3968 (defvar proof-splash-timeout-conf nilproof-splash-timeout-conf142,4768 (defun proof-splash-centre-spaces (glyph)proof-splash-centre-spaces145,4881 (defun proof-splash-remove-screen (&optional nothing)proof-splash-remove-screen172,6037 (defun proof-splash-remove-buffer ()proof-splash-remove-buffer189,6693 (defvar proof-splash-seen nilproof-splash-seen200,7081 (defun proof-splash-insert-contents ()proof-splash-insert-contents203,7183 (defun proof-splash-display-screen (&optional timeout)proof-splash-display-screen243,8313 (defalias 'pg-about 'proof-splash-display-screen)pg-about279,9835 (defun proof-splash-message ()proof-splash-message282,9901 (defun proof-splash-timeout-waiter ()proof-splash-timeout-waiter295,10345 (defvar proof-splash-old-frame-title-format nil)proof-splash-old-frame-title-format308,10903 (defun proof-splash-set-frame-titles ()proof-splash-set-frame-titles310,10953 (defun proof-splash-unset-frame-titles ()proof-splash-unset-frame-titles319,11268 generic/proof-syntax.el,2484 (defsubst proof-ids-to-regexp (l)proof-ids-to-regexp22,516 (defsubst proof-anchor-regexp (e)proof-anchor-regexp29,754 (defconst proof-no-regexp "\\<\\>"proof-no-regexp33,859 (defsubst proof-regexp-alt (&rest args)proof-regexp-alt36,950 (defsubst proof-regexp-alt-list (args)proof-regexp-alt-list45,1262 (defsubst proof-re-search-forward-region (startre endre)proof-re-search-forward-region49,1397 (defsubst proof-search-forward (string &optional bound noerror count)proof-search-forward62,1895 (defsubst proof-replace-regexp-in-string (regexp rep string)proof-replace-regexp-in-string69,2165 (defsubst proof-re-search-forward (regexp &optional bound noerror count)proof-re-search-forward74,2416 (defsubst proof-re-search-backward (regexp &optional bound noerror count)proof-re-search-backward79,2674 (defsubst proof-re-search-forward-safe (regexp &optional bound noerror count)proof-re-search-forward-safe84,2935 (defsubst proof-string-match (regexp string &optional start)proof-string-match90,3216 (defsubst proof-string-match-safe (regexp string &optional start)proof-string-match-safe95,3445 (defsubst proof-stringfn-match (regexp-or-fn string)proof-stringfn-match99,3649 (defsubst proof-looking-at (regexp)proof-looking-at106,3912 (defsubst proof-looking-at-safe (regexp)proof-looking-at-safe111,4099 (defun proof-buffer-syntactic-context (&optional buffer)proof-buffer-syntactic-context120,4312 (defsubst proof-looking-at-syntactic-context-default ()proof-looking-at-syntactic-context-default141,5174 (defun proof-looking-at-syntactic-context ()proof-looking-at-syntactic-context150,5529 (defun proof-inside-comment (pos)proof-inside-comment159,5991 (defun proof-inside-string (pos)proof-inside-string165,6164 (defsubst proof-replace-string (string to-string)proof-replace-string175,6363 (defsubst proof-replace-regexp (regexp to-string)proof-replace-regexp180,6567 (defsubst proof-replace-regexp-nocasefold (regexp to-string)proof-replace-regexp-nocasefold185,6776 (defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)"proof-id195,7064 (defsubst proof-ids (proof-id &optional sepregexp)proof-ids201,7284 (defun proof-zap-commas (limit)proof-zap-commas208,7536 (defadvice font-lock-fontify-keywords-regionfont-lock-fontify-keywords-region234,8422 (defun proof-format (alist string)proof-format250,9018 (defun proof-format-filename (string filename)proof-format-filename269,9657 (defun proof-insert (text)proof-insert316,11059 generic/proof-toolbar.el,3466 (defun proof-toolbar-function (token)proof-toolbar-function33,812 (defun proof-toolbar-icon (token)proof-toolbar-icon37,959 (defun proof-toolbar-enabler (token)proof-toolbar-enabler41,1106 (defun proof-toolbar-make-icon (tle)proof-toolbar-make-icon50,1308 (defun proof-toolbar-make-toolbar-items (map tles)proof-toolbar-make-toolbar-items59,1616 (defvar proof-toolbar-map nilproof-toolbar-map85,2492 (defun proof-toolbar-available-p ()proof-toolbar-available-p88,2591 (defun proof-toolbar-setup ()proof-toolbar-setup98,2897 (defun proof-toolbar-enable ()proof-toolbar-enable119,3754 (defalias 'proof-toolbar-undo 'proof-undo-last-successful-command)proof-toolbar-undo152,4812 (defun proof-toolbar-undo-enable-p ()proof-toolbar-undo-enable-p154,4880 (defalias 'proof-toolbar-delete 'proof-undo-and-delete-last-successful-command)proof-toolbar-delete161,5038 (defun proof-toolbar-delete-enable-p ()proof-toolbar-delete-enable-p163,5119 (defalias 'proof-toolbar-home 'proof-goto-end-of-locked)proof-toolbar-home171,5301 (defalias 'proof-toolbar-next 'proof-assert-next-command-interactive)proof-toolbar-next175,5368 (defun proof-toolbar-next-enable-p ()proof-toolbar-next-enable-p177,5439 (defalias 'proof-toolbar-goto 'proof-goto-point)proof-toolbar-goto183,5555 (defun proof-toolbar-goto-enable-p ()proof-toolbar-goto-enable-p185,5605 (defalias 'proof-toolbar-retract 'proof-retract-buffer)proof-toolbar-retract190,5690 (defun proof-toolbar-retract-enable-p ()proof-toolbar-retract-enable-p192,5747 (defalias 'proof-toolbar-use 'proof-process-buffer)proof-toolbar-use198,5866 (defalias 'proof-toolbar-use-enable-p 'proof-toolbar-next-enable-p)proof-toolbar-use-enable-p199,5918 (defalias 'proof-toolbar-restart 'proof-shell-restart)proof-toolbar-restart203,5999 (defalias 'proof-toolbar-goal 'proof-issue-goal)proof-toolbar-goal207,6064 (defalias 'proof-toolbar-qed 'proof-issue-save)proof-toolbar-qed211,6122 (defun proof-toolbar-qed-enable-p ()proof-toolbar-qed-enable-p213,6171 (defalias 'proof-toolbar-state 'proof-prf)proof-toolbar-state221,6333 (defalias 'proof-toolbar-state-enable-p 'proof-shell-available-p)proof-toolbar-state-enable-p222,6376 (defalias 'proof-toolbar-context 'proof-ctxt)proof-toolbar-context226,6455 (defalias 'proof-toolbar-context-enable-p 'proof-shell-available-p)proof-toolbar-context-enable-p227,6501 (defalias 'proof-toolbar-command 'proof-minibuffer-cmd)proof-toolbar-command231,6582 (defalias 'proof-toolbar-command-enable-p 'proof-shell-available-p)proof-toolbar-command-enable-p232,6638 (defun proof-toolbar-help ()proof-toolbar-help236,6743 (defalias 'proof-toolbar-find 'proof-find-theorems)proof-toolbar-find242,6823 (defalias 'proof-toolbar-find-enable-p 'proof-shell-available-p)proof-toolbar-find-enable-p243,6875 (defalias 'proof-toolbar-info 'proof-query-identifier)proof-toolbar-info247,6950 (defalias 'proof-toolbar-info-enable-p 'proof-shell-available-p)proof-toolbar-info-enable-p248,7005 (defalias 'proof-toolbar-visibility 'pg-toggle-visibility)proof-toolbar-visibility252,7103 (defun proof-toolbar-visibility-enable-p ()proof-toolbar-visibility-enable-p254,7163 (defalias 'proof-toolbar-interrupt 'proof-interrupt-process)proof-toolbar-interrupt259,7277 (defun proof-toolbar-interrupt-enable-p () proof-shell-busy)proof-toolbar-interrupt-enable-p260,7338 (defun proof-toolbar-scripting-menu ()proof-toolbar-scripting-menu268,7491 generic/proof-unicode-tokens.el,856 (defvar proof-unicode-tokens-initialised nilproof-unicode-tokens-initialised31,827 (defun proof-unicode-tokens-init ()proof-unicode-tokens-init34,934 (defun proof-unicode-tokens-configure ()proof-unicode-tokens-configure48,1436 (defun proof-unicode-tokens-mode-if-enabled ()proof-unicode-tokens-mode-if-enabled60,1882 (defun proof-unicode-tokens-set-global (flag)proof-unicode-tokens-set-global66,2081 (defun proof-unicode-tokens-enable ()proof-unicode-tokens-enable82,2651 (defun proof-unicode-tokens-reconfigure ()proof-unicode-tokens-reconfigure102,3504 (defun proof-unicode-tokens-configure-prover ()proof-unicode-tokens-configure-prover128,4392 (defun proof-unicode-tokens-activate-prover ()proof-unicode-tokens-activate-prover133,4573 (defun proof-unicode-tokens-deactivate-prover ()proof-unicode-tokens-deactivate-prover140,4819 generic/proof-useropts.el,2510 (defgroup proof-user-options nilproof-user-options21,564 (defun proof-set-value (sym value)proof-set-value29,743 (defcustom proof-electric-terminator-enable nilproof-electric-terminator-enable62,1866 (defcustom proof-toolbar-enable tproof-toolbar-enable74,2398 (defcustom proof-imenu-enable nilproof-imenu-enable80,2571 (defcustom pg-show-hints tpg-show-hints86,2742 (defcustom proof-shell-quiet-errors tproof-shell-quiet-errors91,2875 (defcustom proof-trace-output-slow-catchup tproof-trace-output-slow-catchup98,3146 (defcustom proof-strict-state-preserving tproof-strict-state-preserving108,3643 (defcustom proof-strict-read-only 'retractproof-strict-read-only121,4252 (defcustom proof-three-window-enable nilproof-three-window-enable134,4831 (defcustom proof-multiple-frames-enable nilproof-multiple-frames-enable153,5581 (defcustom proof-delete-empty-windows nilproof-delete-empty-windows162,5914 (defcustom proof-shrink-windows-tofit nilproof-shrink-windows-tofit173,6445 (defcustom proof-auto-raise-buffers tproof-auto-raise-buffers180,6717 (defcustom proof-colour-locked tproof-colour-locked187,6952 (defcustom proof-sticky-errors nilproof-sticky-errors195,7202 (defcustom proof-query-file-save-when-activating-scriptingproof-query-file-save-when-activating-scripting202,7419 (defcustom proof-prog-name-askproof-prog-name-ask218,8139 (defcustom proof-prog-name-guessproof-prog-name-guess224,8299 (defcustom proof-tidy-responseproof-tidy-response232,8564 (defcustom proof-keep-response-historyproof-keep-response-history246,9027 (defcustom pg-input-ring-size 32pg-input-ring-size256,9415 (defcustom proof-general-debug nilproof-general-debug261,9567 (defcustom proof-use-parser-cache tproof-use-parser-cache270,9938 (defcustom proof-follow-mode 'lockedproof-follow-mode277,10192 (defcustom proof-auto-action-when-deactivating-scripting nilproof-auto-action-when-deactivating-scripting301,11369 (defcustom proof-rsh-command nilproof-rsh-command329,12551 (defcustom proof-disappearing-proofs nilproof-disappearing-proofs345,13101 (defcustom proof-full-annotation tproof-full-annotation350,13262 (defcustom proof-minibuffer-messages nilproof-minibuffer-messages359,13632 (defcustom proof-autosend-enable nilproof-autosend-enable367,13941 (defcustom proof-autosend-delay 0.8proof-autosend-delay373,14121 (defcustom proof-autosend-all nilproof-autosend-all379,14279 (defcustom proof-fast-process-buffer proof-fast-process-buffer384,14448 generic/proof-utils.el,3227 (defmacro proof-with-current-buffer-if-exists (buf &rest body)proof-with-current-buffer-if-exists61,1729 (defmacro proof-with-script-buffer (&rest body)proof-with-script-buffer70,2106 (defmacro proof-map-buffers (buflist &rest body)proof-map-buffers81,2487 (defmacro proof-sym (string)proof-sym86,2672 (defsubst proof-try-require (symbol)proof-try-require91,2833 (defun proof-save-some-buffers (buffers)proof-save-some-buffers104,3164 (defun proof-save-this-buffer ()proof-save-this-buffer124,3760 (defun proof-file-truename (filename)proof-file-truename137,4124 (defun proof-files-to-buffers (filenames)proof-files-to-buffers141,4306 (defun proof-buffers-in-mode (mode &optional buflist)proof-buffers-in-mode149,4545 (defun pg-save-from-death ()pg-save-from-death163,4995 (defun proof-define-keys (map kbl)proof-define-keys182,5611 (defun pg-remove-specials (&optional start end)pg-remove-specials193,5896 (defun pg-remove-specials-in-string (string)pg-remove-specials-in-string203,6232 (defun proof-safe-split-window-vertically ()proof-safe-split-window-vertically213,6457 (defun proof-warn-if-unset (tag sym)proof-warn-if-unset218,6637 (defun proof-get-window-for-buffer (buffer)proof-get-window-for-buffer223,6855 (defun proof-display-and-keep-buffer (buffer &optional pos force)proof-display-and-keep-buffer272,9165 (defun proof-clean-buffer (buffer)proof-clean-buffer314,10888 (defun pg-internal-warning (message &rest args)pg-internal-warning330,11544 (defun proof-debug (msg &rest args)proof-debug338,11826 (defun proof-switch-to-buffer (buf &optional noselect)proof-switch-to-buffer353,12370 (defun proof-resize-window-tofit (&optional window)proof-resize-window-tofit375,13494 (defun proof-submit-bug-report ()proof-submit-bug-report470,17342 (defun proof-deftoggle-fn (var &optional othername)proof-deftoggle-fn505,18699 (defmacro proof-deftoggle (var &optional othername)proof-deftoggle520,19365 (defun proof-defintset-fn (var &optional othername)proof-defintset-fn531,19878 (defmacro proof-defintset (var &optional othername)proof-defintset550,20702 (defun proof-deffloatset-fn (var &optional othername)proof-deffloatset-fn557,21081 (defmacro proof-deffloatset (var &optional othername)proof-deffloatset573,21795 (defun proof-defstringset-fn (var &optional othername)proof-defstringset-fn580,22180 (defmacro proof-defstringset (var &optional othername)proof-defstringset593,22806 (defun proof-escape-keymap-doc (string)proof-escape-keymap-doc606,23262 (defmacro proof-defshortcut (fn string &optional key)proof-defshortcut610,23416 (defmacro proof-definvisible (fn string &optional key)proof-definvisible625,24014 (defun pg-custom-save-vars (&rest variables)pg-custom-save-vars652,24943 (defun pg-custom-reset-vars (&rest variables)pg-custom-reset-vars668,25587 (defun proof-locate-executable (progname &optional returnnopath extrapath)proof-locate-executable681,25924 (defun pg-current-word-pos (&optional strict really-word)pg-current-word-pos696,26474 (defsubst proof-shell-strip-output-markup (string &optional push)proof-shell-strip-output-markup741,28129 (defun proof-minibuffer-message (str)proof-minibuffer-message747,28393 lib/bufhist.el,2047 (defun bufhist-ring-update (ring index newitem)bufhist-ring-update38,1391 (defgroup bufhist nilbufhist47,1713 (defcustom bufhist-ring-size 30bufhist-ring-size51,1794 (defvar bufhist-ring nilbufhist-ring56,1905 (defvar bufhist-ring-pos nilbufhist-ring-pos59,1979 (defvar bufhist-lastswitch-modified-tick nilbufhist-lastswitch-modified-tick62,2058 (defvar bufhist-read-only-history tbufhist-read-only-history65,2164 (defvar bufhist-saved-mode-line-format nilbufhist-saved-mode-line-format68,2235 (defvar bufhist-normal-read-only nilbufhist-normal-read-only71,2338 (defvar bufhist-top-point 0bufhist-top-point74,2432 (defun bufhist-mode-line-format-entry ()bufhist-mode-line-format-entry77,2522 (defconst bufhist-minor-mode-mapbufhist-minor-mode-map106,3596 (define-minor-mode bufhist-modebufhist-mode119,4073 (defun bufhist-get-buffer-contents ()bufhist-get-buffer-contents141,4954 (defun bufhist-restore-buffer-contents (buf)bufhist-restore-buffer-contents150,5296 (defun bufhist-checkpoint ()bufhist-checkpoint159,5610 (defun bufhist-erase-buffer ()bufhist-erase-buffer167,5979 (defun bufhist-checkpoint-and-erase ()bufhist-checkpoint-and-erase178,6350 (defun bufhist-switch-to-index (n &optional nosave browsing)bufhist-switch-to-index184,6536 (defun bufhist-first ()bufhist-first223,8135 (defun bufhist-last ()bufhist-last228,8294 (defun bufhist-prev (&optional n)bufhist-prev233,8438 (defun bufhist-next (&optional n)bufhist-next241,8661 (defun bufhist-delete ()bufhist-delete246,8801 (defun bufhist-clear ()bufhist-clear258,9342 (defun bufhist-init (&optional readwrite ringsize)bufhist-init273,9737 (defun bufhist-exit ()bufhist-exit301,10746 (defun bufhist-set-readwrite (readwrite)bufhist-set-readwrite311,11010 (defun bufhist-before-change-function (&rest args)bufhist-before-change-function326,11630 (define-button-type 'bufhist-nextbufhist-next340,12053 (define-button-type 'bufhist-prevbufhist-prev344,12150 (defun bufhist-insert-buttons ()bufhist-insert-buttons351,12362 lib/holes.el,4313 (defvar holes-default-hole holes-default-hole44,1121 (defvar holes-active-hole holes-default-holeholes-active-hole50,1299 (defgroup holes nilholes60,1496 (defcustom holes-empty-hole-string "#"holes-empty-hole-string65,1595 (defcustom holes-empty-hole-regexp "#\\|@{\\([^{}]*\\)}"holes-empty-hole-regexp70,1738 (defface active-hole-faceactive-hole-face92,2440 (defface inactive-hole-faceinactive-hole-face102,2856 (defvar hole-maphole-map116,3297 (defvar holes-mode-mapholes-mode-map126,3688 (defun holes-region-beginning-or-nil ()holes-region-beginning-or-nil172,5425 (defun holes-region-end-or-nil ()holes-region-end-or-nil176,5561 (defun holes-copy-active-region ()holes-copy-active-region180,5679 (defun holes-is-hole-p (span)holes-is-hole-p186,5889 (defun holes-hole-start-position (hole)holes-hole-start-position190,5981 (defun holes-hole-end-position (hole)holes-hole-end-position196,6164 (defun holes-hole-buffer (hole)holes-hole-buffer201,6335 (defun holes-hole-at (&optional pos)holes-hole-at207,6509 (defun holes-active-hole-exist-p ()holes-active-hole-exist-p212,6679 (defun holes-active-hole-start-position ()holes-active-hole-start-position219,6932 (defun holes-active-hole-end-position ()holes-active-hole-end-position227,7300 (defun holes-active-hole-buffer ()holes-active-hole-buffer236,7663 (defun holes-goto-active-hole ()holes-goto-active-hole244,7964 (defun holes-highlight-hole-as-active (hole)holes-highlight-hole-as-active253,8223 (defun holes-highlight-hole (hole)holes-highlight-hole261,8531 (defun holes-disable-active-hole ()holes-disable-active-hole269,8818 (defun holes-set-active-hole (hole)holes-set-active-hole282,9350 (defun holes-is-in-hole-p (&optional pos)holes-is-in-hole-p292,9695 (defun holes-make-hole (start end)holes-make-hole296,9833 (defun holes-make-hole-at (&optional start end)holes-make-hole-at314,10489 (defun holes-clear-hole (hole)holes-clear-hole328,10942 (defun holes-clear-hole-at (&optional pos)holes-clear-hole-at337,11200 (defun holes-map-holes (function &optional object from to)holes-map-holes345,11456 (defun holes-clear-all-buffer-holes (&optional start end)holes-clear-all-buffer-holes349,11610 (defun holes-next (pos buffer)holes-next359,11911 (defun holes-next-after-active-hole ()holes-next-after-active-hole366,12163 (defun holes-set-active-hole-next (&optional buffer pos)holes-set-active-hole-next373,12379 (defun holes-replace-segment (start end str &optional buffer)holes-replace-segment392,12916 (defun holes-replace (str &optional thehole)holes-replace401,13269 (defun holes-replace-active-hole (&optional str)holes-replace-active-hole429,14447 (defun holes-replace-update-active-hole (&optional str)holes-replace-update-active-hole436,14738 (defun holes-delete-update-active-hole ()holes-delete-update-active-hole454,15385 (defun holes-set-make-active-hole (&optional start end)holes-set-make-active-hole462,15612 (defalias 'holes-track-mouse-selection 'mouse-drag-track)holes-track-mouse-selection477,16167 (defsubst holes-track-mouse-clicks ()holes-track-mouse-clicks478,16225 (defun holes-mouse-replace-active-hole (event)holes-mouse-replace-active-hole482,16335 (defun holes-destroy-hole (&optional span)holes-destroy-hole496,16806 (defsubst holes-hole-at-event (event)holes-hole-at-event510,17188 (defun holes-mouse-destroy-hole (event)holes-mouse-destroy-hole514,17288 (defun holes-mouse-forget-hole (event)holes-mouse-forget-hole521,17509 (defun holes-mouse-set-make-active-hole (event)holes-mouse-set-make-active-hole531,17801 (defun holes-mouse-set-active-hole (event)holes-mouse-set-active-hole547,18300 (defun holes-set-point-next-hole-destroy ()holes-set-point-next-hole-destroy556,18551 (defun holes-replace-string-by-holes-backward (limit)holes-replace-string-by-holes-backward582,19532 (defun holes-skeleton-end-hook ()holes-skeleton-end-hook600,20232 (defconst holes-jump-docholes-jump-doc609,20670 (defun holes-replace-string-by-holes-backward-jump (pos &optional noindent)holes-replace-string-by-holes-backward-jump616,20876 (define-minor-mode holes-mode holes-mode633,21558 (defun holes-abbrev-complete ()holes-abbrev-complete728,25040 (defun holes-insert-and-expand (s)holes-insert-and-expand738,25383 lib/local-vars-list.el,665 (defconst local-vars-list-doc nillocal-vars-list-doc28,825 (defun local-vars-list-insert-empty-zone ()local-vars-list-insert-empty-zone44,1387 (defun local-vars-list-find ()local-vars-list-find82,2090 (defun local-vars-list-goto-var (symb lpat rpat)local-vars-list-goto-var101,2861 (defun local-vars-list-get-current (lpat rpat)local-vars-list-get-current127,3908 (defun local-vars-list-set-current (val lpat rpat)local-vars-list-set-current148,4758 (defun local-vars-list-get (symb)local-vars-list-get171,5473 (defun local-vars-list-get-safe (symb)local-vars-list-get-safe188,6003 (defun local-vars-list-set (symb val)local-vars-list-set193,6197 lib/maths-menu.el,425 (defvar maths-menu-filter-predicate '(lambda (char) t)maths-menu-filter-predicate56,2317 (defvar maths-menu-tokenise-insert '(lambda (char) (insert char))maths-menu-tokenise-insert59,2426 (defun maths-menu-build-menu (spec)maths-menu-build-menu62,2563 (defvar maths-menu-menumaths-menu-menu84,3324 (defvar maths-menu-mode-mapmaths-menu-mode-map344,12882 (define-minor-mode maths-menu-modemaths-menu-mode352,13101 lib/pg-dev.el,319 (defconst pg-dev-lisp-font-lock-keywordspg-dev-lisp-font-lock-keywords52,1587 (defun pg-loadpath ()pg-loadpath78,2286 (defun unload-pg ()unload-pg88,2457 (defun profile-pg ()profile-pg119,3351 (defun elp-pack-number (number width)elp-pack-number148,4378 (defun pg-bug-references ()pg-bug-references157,4578 lib/pg-fontsets.el,352 (defcustom pg-fontsets-default-fontset nilpg-fontsets-default-fontset24,722 (defvar pg-fontsets-names nilpg-fontsets-names29,868 (defun pg-fontsets-make-fontsetsizes (basefont)pg-fontsets-make-fontsetsizes32,949 (defconst pg-fontsets-base-fontspg-fontsets-base-fonts51,1710 (defun pg-fontsets-make-fontsets ()pg-fontsets-make-fontsets57,1840 lib/proof-compat.el,326 (defvar proof-running-on-win32 (memq system-type '(win32 windows-nt cygwin))proof-running-on-win3232,980 (defun pg-custom-undeclare-variable (symbol)pg-custom-undeclare-variable53,1782 (defmacro save-selected-frame (&rest body)save-selected-frame85,2553 (defmacro declare-function (&rest args)declare-function151,4561 lib/scomint.el,1525 (defvar scomint-buffer-maximum-size 800000scomint-buffer-maximum-size19,493 (defvar scomint-output-filter-functions nilscomint-output-filter-functions24,684 (defvar scomint-mode-mapscomint-mode-map27,794 (defvar scomint-last-input-start nil)scomint-last-input-start33,973 (defvar scomint-last-input-end nil)scomint-last-input-end34,1011 (defvar scomint-last-output-start nil)scomint-last-output-start35,1047 (defvar scomint-exec-hook nilscomint-exec-hook37,1087 (define-derived-mode scomint-mode fundamental-mode "SComint"scomint-mode46,1430 (defsubst scomint-check-proc (buffer)scomint-check-proc65,2345 (defun scomint-make-in-buffer (name buffer program &optional startfile &rest switches)scomint-make-in-buffer73,2685 (defun scomint-make (name program &optional startfile &rest switches)scomint-make97,3952 (defun scomint-exec (buffer name command startfile switches)scomint-exec110,4663 (defun scomint-exec-1 (name buffer command switches)scomint-exec-1147,6256 (defalias 'scomint-send-string 'process-send-string)scomint-send-string197,8386 (defun scomint-send-eof ()scomint-send-eof199,8440 (defun scomint-send-input (&optional no-newline artificial)scomint-send-input208,8673 (defun scomint-truncate-buffer (&optional string)scomint-truncate-buffer234,9569 (defun scomint-strip-ctrl-m (&optional string)scomint-strip-ctrl-m247,9963 (defun scomint-output-filter (process string)scomint-output-filter261,10526 (defun scomint-interrupt-process ()scomint-interrupt-process284,11281 lib/span.el,2711 (defalias 'span-start 'overlay-start)span-start22,611 (defalias 'span-end 'overlay-end)span-end23,649 (defalias 'span-set-property 'overlay-put)span-set-property24,683 (defalias 'span-property 'overlay-get)span-property25,726 (defalias 'span-make 'make-overlay)span-make26,765 (defalias 'span-detach 'delete-overlay)span-detach27,801 (defalias 'span-set-endpoints 'move-overlay)span-set-endpoints28,841 (defalias 'span-buffer 'overlay-buffer)span-buffer29,886 (defun span-read-only-hook (overlay after start end &optional len)span-read-only-hook31,927 (defsubst span-read-only (span)span-read-only36,1117 (defsubst span-read-write (span)span-read-write43,1427 (defsubst span-write-warning (span fun)span-write-warning48,1597 (defsubst span-lt (s u)span-lt59,2121 (defsubst spans-at-point-prop (pt prop)spans-at-point-prop64,2265 (defsubst spans-at-region-prop (start end prop)spans-at-region-prop73,2456 (defsubst span-at (pt prop)span-at83,2722 (defsubst span-delete (span)span-delete87,2848 (defsubst span-add-delete-action (span action)span-add-delete-action93,3044 (defsubst span-mapcar-spans (fn start end prop)span-mapcar-spans99,3323 (defsubst span-mapc-spans (fn start end prop)span-mapc-spans103,3498 (defsubst span-mapcar-spans-inorder (fn start end prop)span-mapcar-spans-inorder107,3669 (defun span-at-before (pt prop)span-at-before113,3874 (defsubst prev-span (span prop)prev-span130,4598 (defsubst next-span (span prop)next-span136,4751 (defsubst span-live-p (span)span-live-p142,4965 (defsubst span-raise (span)span-raise148,5131 (defsubst span-string (span)span-string152,5264 (defsubst set-span-properties (span plist)set-span-properties157,5424 (defsubst span-find-span (overlay-list &optional prop)span-find-span163,5618 (defsubst span-at-event (event &optional prop)span-at-event171,5930 (defun fold-spans (f &optional buffer from to maparg ignored-flags prop val)fold-spans177,6127 (defsubst span-detached-p (span)span-detached-p191,6660 (defsubst set-span-face (span face)set-span-face195,6776 (defsubst set-span-keymap (span map)set-span-keymap199,6874 (defsubst span-delete-spans (start end prop)span-delete-spans207,7043 (defsubst span-property-safe (span name)span-property-safe211,7205 (defsubst span-set-start (span value)span-set-start215,7342 (defsubst span-set-end (span value)span-set-end219,7474 (defun span-make-self-removing-span (beg end &rest props)span-make-self-removing-span227,7634 (defun span-delete-self-modification-hook (span &rest args)span-delete-self-modification-hook237,8002 (defun span-make-modifying-removing-span (beg end &rest props)span-make-modifying-removing-span242,8176 lib/texi-docstring-magic.el,1112 (defun texi-docstring-magic-find-face (face)texi-docstring-magic-find-face88,3027 (defun texi-docstring-magic-splice-sep (strings sep)texi-docstring-magic-splice-sep93,3192 (defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table103,3497 (defun texi-docstring-magic-untabify (string)texi-docstring-magic-untabify193,7260 (defun texi-docstring-magic-munge-docstring (docstring args)texi-docstring-magic-munge-docstring200,7458 (defun texi-docstring-magic-texi (env grp name docstring args &optional endtext)texi-docstring-magic-texi239,8739 (defun texi-docstring-magic-format-default (default)texi-docstring-magic-format-default252,9179 (defun texi-docstring-magic-texi-for (symbol &optional noerror)texi-docstring-magic-texi-for268,9812 (defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11771 (defun texi-docstring-magic (&optional noerror)texi-docstring-magic332,11925 (defun texi-docstring-magic-face-at-point ()texi-docstring-magic-face-at-point366,13004 (defun texi-docstring-magic-insert-magic (symbol)texi-docstring-magic-insert-magic381,13527 lib/unicode-chars.el,127 (defvar unicode-chars-alistunicode-chars-alist12,348 (defun unicode-chars-list-chars ()unicode-chars-list-chars5051,245975 lib/unicode-tokens.el,9990 (defgroup unicode-tokens-options nilunicode-tokens-options55,1711 (defcustom unicode-tokens-add-help-echo tunicode-tokens-add-help-echo60,1836 (defun unicode-tokens-toggle-add-help-echo ()unicode-tokens-toggle-add-help-echo65,2003 (defvar unicode-tokens-token-symbol-map nilunicode-tokens-token-symbol-map79,2409 (defvar unicode-tokens-token-format "%s"unicode-tokens-token-format98,3068 (defvar unicode-tokens-token-variant-format-regexp nilunicode-tokens-token-variant-format-regexp104,3317 (defvar unicode-tokens-shortcut-alist nilunicode-tokens-shortcut-alist118,3850 (defvar unicode-tokens-shortcut-replacement-alist nilunicode-tokens-shortcut-replacement-alist124,4127 (defvar unicode-tokens-control-region-format-regexp nilunicode-tokens-control-region-format-regexp132,4333 (defvar unicode-tokens-control-char-format-regexp nilunicode-tokens-control-char-format-regexp139,4701 (defvar unicode-tokens-control-regions nilunicode-tokens-control-regions146,5062 (defvar unicode-tokens-control-characters nilunicode-tokens-control-characters149,5138 (defvar unicode-tokens-control-char-format nilunicode-tokens-control-char-format152,5220 (defvar unicode-tokens-control-region-format-start nilunicode-tokens-control-region-format-start155,5333 (defvar unicode-tokens-control-region-format-end nilunicode-tokens-control-region-format-end158,5450 (defvar unicode-tokens-tokens-customizable-variables nilunicode-tokens-tokens-customizable-variables161,5563 (defconst unicode-tokens-configuration-variablesunicode-tokens-configuration-variables168,5731 (defun unicode-tokens-config (sym)unicode-tokens-config183,6130 (defun unicode-tokens-config-var (sym)unicode-tokens-config-var187,6275 (defun unicode-tokens-copy-configuration-variables ()unicode-tokens-copy-configuration-variables199,6715 (defvar unicode-tokens-token-list nilunicode-tokens-token-list227,7931 (defvar unicode-tokens-hash-table nilunicode-tokens-hash-table230,8051 (defvar unicode-tokens-token-match-regexp nilunicode-tokens-token-match-regexp233,8167 (defvar unicode-tokens-uchar-hash-table nilunicode-tokens-uchar-hash-table239,8450 (defvar unicode-tokens-uchar-regexp nilunicode-tokens-uchar-regexp243,8637 (defgroup unicode-tokens-faces nilunicode-tokens-faces251,8822 (defconst unicode-tokens-font-family-alternativesunicode-tokens-font-family-alternatives261,9119 (defface unicode-tokens-symbol-font-faceunicode-tokens-symbol-font-face276,9616 (defface unicode-tokens-script-font-faceunicode-tokens-script-font-face286,9974 (defface unicode-tokens-fraktur-font-faceunicode-tokens-fraktur-font-face291,10118 (defface unicode-tokens-serif-font-faceunicode-tokens-serif-font-face296,10243 (defface unicode-tokens-sans-font-faceunicode-tokens-sans-font-face301,10380 (defface unicode-tokens-highlight-faceunicode-tokens-highlight-face306,10502 (defconst unicode-tokens-fontsunicode-tokens-fonts315,10864 (defconst unicode-tokens-fontsymb-propertiesunicode-tokens-fontsymb-properties324,11081 (define-widget 'unicode-tokens-token-symbol-map 'lazyunicode-tokens-token-symbol-map352,12697 (define-widget 'unicode-tokens-shortcut-alist 'lazyunicode-tokens-shortcut-alist370,13249 (defconst unicode-tokens-font-lock-extra-managed-propsunicode-tokens-font-lock-extra-managed-props383,13580 (defun unicode-tokens-font-lock-keywords ()unicode-tokens-font-lock-keywords387,13734 (defun unicode-tokens-calculate-token-match (toks)unicode-tokens-calculate-token-match420,15105 (defun unicode-tokens-usable-composition (comp)unicode-tokens-usable-composition450,16141 (defun unicode-tokens-help-echo ()unicode-tokens-help-echo463,16520 (defvar unicode-tokens-show-symbols nilunicode-tokens-show-symbols468,16722 (defun unicode-tokens-interpret-composition (comp)unicode-tokens-interpret-composition471,16836 (defun unicode-tokens-font-lock-compose-symbol (match)unicode-tokens-font-lock-compose-symbol489,17348 (defun unicode-tokens-prepend-text-properties-in-match (props matchno)unicode-tokens-prepend-text-properties-in-match527,18880 (defun unicode-tokens-prepend-text-property (start end prop value &optional object)unicode-tokens-prepend-text-property541,19458 (defun unicode-tokens-show-symbols (&optional arg)unicode-tokens-show-symbols566,20603 (defun unicode-tokens-symbs-to-props (symbs &optional facenil)unicode-tokens-symbs-to-props574,20913 (defvar unicode-tokens-show-controls nilunicode-tokens-show-controls594,21612 (defun unicode-tokens-show-controls (&optional arg)unicode-tokens-show-controls597,21703 (defun unicode-tokens-control-char (name s &rest props)unicode-tokens-control-char609,22216 (defun unicode-tokens-control-region (name start end &rest props)unicode-tokens-control-region618,22655 (defun unicode-tokens-control-font-lock-keywords ()unicode-tokens-control-font-lock-keywords629,23202 (defvar unicode-tokens-use-shortcuts tunicode-tokens-use-shortcuts640,23526 (defun unicode-tokens-use-shortcuts (&optional arg)unicode-tokens-use-shortcuts643,23629 (defun unicode-tokens-map-ordering (s1 s2)unicode-tokens-map-ordering659,24225 (defun unicode-tokens-quail-define-rules ()unicode-tokens-quail-define-rules668,24578 (defun unicode-tokens-insert-token (tok)unicode-tokens-insert-token691,25255 (defun unicode-tokens-annotate-region (name)unicode-tokens-annotate-region700,25559 (defun unicode-tokens-insert-control (name)unicode-tokens-insert-control724,26397 (defun unicode-tokens-insert-uchar-as-token (char)unicode-tokens-insert-uchar-as-token734,26846 (defun unicode-tokens-delete-token-near-point ()unicode-tokens-delete-token-near-point740,27067 (defun unicode-tokens-delete-backward-char (&optional arg)unicode-tokens-delete-backward-char752,27508 (defun unicode-tokens-delete-char (&optional arg)unicode-tokens-delete-char763,27889 (defun unicode-tokens-delete-backward-1 ()unicode-tokens-delete-backward-1774,28243 (defun unicode-tokens-delete-1 ()unicode-tokens-delete-1791,28839 (defun unicode-tokens-prev-token ()unicode-tokens-prev-token807,29383 (defun unicode-tokens-rotate-token-forward (&optional n)unicode-tokens-rotate-token-forward815,29680 (defun unicode-tokens-rotate-token-backward (&optional n)unicode-tokens-rotate-token-backward842,30570 (defun unicode-tokens-replace-shortcut-match (&rest ignore)unicode-tokens-replace-shortcut-match847,30772 (defun unicode-tokens-replace-shortcuts ()unicode-tokens-replace-shortcuts856,31142 (defun unicode-tokens-replace-unicode-match (&rest ignore)unicode-tokens-replace-unicode-match870,31740 (defun unicode-tokens-replace-unicode ()unicode-tokens-replace-unicode877,32041 (defun unicode-tokens-copy-token (tokname)unicode-tokens-copy-token894,32640 (define-button-type 'unicode-tokens-listunicode-tokens-list901,32861 (defun unicode-tokens-list-tokens ()unicode-tokens-list-tokens907,33065 (defun unicode-tokens-list-shortcuts ()unicode-tokens-list-shortcuts946,34249 (defalias 'unicode-tokens-list-unicode-chars 'unicode-chars-list-chars)unicode-tokens-list-unicode-chars964,34887 (defun unicode-tokens-encode-in-temp-buffer (str fn)unicode-tokens-encode-in-temp-buffer966,34960 (defun unicode-tokens-encode (beg end)unicode-tokens-encode984,35616 (defun unicode-tokens-encode-str (str)unicode-tokens-encode-str990,35852 (defun unicode-tokens-copy (beg end)unicode-tokens-copy994,36014 (defun unicode-tokens-paste ()unicode-tokens-paste1003,36420 (defvar unicode-tokens-highlight-unicode nilunicode-tokens-highlight-unicode1022,37141 (defconst unicode-tokens-unicode-highlight-patternsunicode-tokens-unicode-highlight-patterns1025,37233 (defun unicode-tokens-highlight-unicode ()unicode-tokens-highlight-unicode1029,37402 (defun unicode-tokens-highlight-unicode-setkeywords ()unicode-tokens-highlight-unicode-setkeywords1041,37865 (defun unicode-tokens-initialise ()unicode-tokens-initialise1053,38234 (defvar unicode-tokens-mode-map (make-sparse-keymap)unicode-tokens-mode-map1073,38905 (defvar unicode-tokens-display-tableunicode-tokens-display-table1076,39002 (define-minor-mode unicode-tokens-modeunicode-tokens-mode1083,39253 (defun unicode-tokens-set-font-var (fontvar)unicode-tokens-set-font-var1219,43828 (defun unicode-tokens-set-font-var-aux (fontvar font)unicode-tokens-set-font-var-aux1235,44317 (defun unicode-tokens-mouse-set-font ()unicode-tokens-mouse-set-font1266,45478 (defsubst unicode-tokens-face-font-sym (fontsym)unicode-tokens-face-font-sym1279,45992 (defun unicode-tokens-set-font-restart (fontsym)unicode-tokens-set-font-restart1283,46172 (defun unicode-tokens-save-fonts ()unicode-tokens-save-fonts1294,46482 (defun unicode-tokens-custom-save-faces (&rest faces)unicode-tokens-custom-save-faces1302,46738 (define-key unicode-tokens-mode-mapunicode-tokens-mode-map1319,47194 (define-key unicode-tokens-mode-mapunicode-tokens-mode-map1322,47301 (defvar unicode-tokens-quail-translation-keymapunicode-tokens-quail-translation-keymap1326,47391 (define-key unicode-tokens-quail-translation-keymapunicode-tokens-quail-translation-keymap1333,47581 (defun unicode-tokens-quail-delete-last-char ()unicode-tokens-quail-delete-last-char1337,47715 (define-key unicode-tokens-mode-map [(control ?,)]unicode-tokens-mode-map1352,48142 (define-key unicode-tokens-mode-map [(control ?.)]unicode-tokens-mode-map1354,48234 (define-key unicode-tokens-mode-mapunicode-tokens-mode-map1356,48325 (define-key unicode-tokens-mode-mapunicode-tokens-mode-map1358,48431 (define-key unicode-tokens-mode-mapunicode-tokens-mode-map1361,48546 (define-key unicode-tokens-mode-mapunicode-tokens-mode-map1363,48655 (define-key unicode-tokens-mode-mapunicode-tokens-mode-map1365,48763 (define-key unicode-tokens-mode-mapunicode-tokens-mode-map1367,48869 (defun unicode-tokens-customize-submenu ()unicode-tokens-customize-submenu1375,48993 (defun unicode-tokens-define-menu ()unicode-tokens-define-menu1382,49216 contrib/mmm/mmm-auto.el,563 (defvar mmm-autoloaded-classesmmm-autoloaded-classes67,2676 (defun mmm-autoload-class (class file &optional private)mmm-autoload-class89,3439 (defvar mmm-changed-buffers-list ()mmm-changed-buffers-list129,4992 (defun mmm-major-mode-change ()mmm-major-mode-change132,5099 (defun mmm-check-changed-buffers ()mmm-check-changed-buffers145,5620 (defun mmm-mode-on-maybe ()mmm-mode-on-maybe154,5970 (defalias 'mmm-add-find-file-hooks 'mmm-add-find-file-hook)mmm-add-find-file-hooks166,6374 (defun mmm-add-find-file-hook ()mmm-add-find-file-hook167,6434 contrib/mmm/mmm-class.el,773 (defun mmm-get-class-spec (class)mmm-get-class-spec42,1296 (defun mmm-get-class-parameter (class param)mmm-get-class-parameter59,1939 (defun mmm-set-class-parameter (class param value)mmm-set-class-parameter63,2105 (defun* mmm-apply-classmmm-apply-class75,2455 (defun* mmm-apply-classesmmm-apply-classes90,3072 (defun* mmm-apply-all (&key (start (point-min)) (stop (point-max)))mmm-apply-all110,3803 (defun* mmm-ifymmm-ify124,4250 (defun* mmm-match-regionmmm-match-region206,7095 (defun mmm-match->point (beginp offset match)mmm-match->point269,9480 (defun mmm-match-and-verify (pos start stop &optional verify)mmm-match-and-verify284,10050 (defun mmm-get-form (form)mmm-get-form310,11101 (defun mmm-default-get-form ()mmm-default-get-form321,11576 contrib/mmm/mmm-cmds.el,1292 (defun mmm-ify-by-class (class)mmm-ify-by-class41,1210 (defun mmm-ify-region (submode front back)mmm-ify-region63,1822 (defun mmm-ify-by-regexpmmm-ify-by-regexp75,2243 (defun mmm-parse-buffer ()mmm-parse-buffer97,2886 (defun mmm-parse-region (start stop)mmm-parse-region106,3222 (defun mmm-parse-block (&optional lines)mmm-parse-block115,3601 (defun mmm-get-block (lines)mmm-get-block132,4352 (defun mmm-reparse-current-region ()mmm-reparse-current-region146,4634 (defun mmm-clear-current-region ()mmm-clear-current-region167,5210 (defun mmm-clear-regions (start stop)mmm-clear-regions172,5374 (defun mmm-clear-all-regions ()mmm-clear-all-regions177,5520 (defun* mmm-end-current-region (&optional arg)mmm-end-current-region185,5680 (defun mmm-narrow-to-submode-region (&optional pos)mmm-narrow-to-submode-region220,6928 (defun mmm-insert-region (arg)mmm-insert-region239,7542 (defun mmm-insert-by-key (key &optional arg)mmm-insert-by-key258,8348 (defun mmm-get-insertion-spec (key &optional classlist)mmm-get-insertion-spec342,11613 (defun mmm-insertion-help ()mmm-insertion-help369,12573 (defun mmm-display-insertion-key (spec)mmm-display-insertion-key379,12936 (defun mmm-get-all-insertion-keys (&optional classlist)mmm-get-all-insertion-keys401,13723 contrib/mmm/mmm-compat.el,739 (defvar mmm-xemacs (featurep 'xemacs)mmm-xemacs40,1313 (defvar mmm-keywords-usedmmm-keywords-used49,1616 (defmacro mmm-regexp-opt (strings paren)mmm-regexp-opt91,2632 (defvar mmm-evaporate-propertymmm-evaporate-property110,3281 (defmacro mmm-set-keymap-default (keymap binding)mmm-set-keymap-default128,4047 (defmacro mmm-event-key (event)mmm-event-key137,4489 (defvar skeleton-positions ())skeleton-positions146,4708 (defun mmm-fixup-skeleton ()mmm-fixup-skeleton147,4739 (defmacro mmm-make-temp-buffer (buffer name)mmm-make-temp-buffer159,5162 (defvar mmm-font-lock-available-p (or window-system mmm-xemacs)mmm-font-lock-available-p172,5558 (defmacro mmm-set-font-lock-defaults ()mmm-set-font-lock-defaults179,5772 contrib/mmm/mmm-cweb.el,367 (defvar mmm-cweb-section-tagsmmm-cweb-section-tags38,1117 (defvar mmm-cweb-section-regexpmmm-cweb-section-regexp41,1164 (defvar mmm-cweb-c-part-tagsmmm-cweb-c-part-tags44,1254 (defvar mmm-cweb-c-part-regexpmmm-cweb-c-part-regexp47,1313 (defun mmm-cweb-in-limbo (pos)mmm-cweb-in-limbo50,1397 (defun mmm-cweb-verify-brief-c ()mmm-cweb-verify-brief-c57,1622 contrib/mmm/mmm-mason.el,665 (defvar mmm-mason-perl-tagsmmm-mason-perl-tags41,1236 (defvar mmm-mason-pseudo-perl-tagsmmm-mason-pseudo-perl-tags45,1377 (defvar mmm-mason-non-perl-tagsmmm-mason-non-perl-tags48,1453 (defvar mmm-mason-perl-tags-regexpmmm-mason-perl-tags-regexp51,1554 (defvar mmm-mason-pseudo-perl-tags-regexpmmm-mason-pseudo-perl-tags-regexp56,1749 (defvar mmm-mason-tag-names-regexpmmm-mason-tag-names-regexp61,1966 (defun mmm-mason-verify-inline ()mmm-mason-verify-inline66,2186 (defun mmm-mason-start-line ()mmm-mason-start-line156,4838 (defun mmm-mason-end-line ()mmm-mason-end-line161,4903 (defun mmm-mason-set-mode-line ()mmm-mason-set-mode-line168,4997 contrib/mmm/mmm-mode.el,1961 (defun mmm-mode (&optional arg)mmm-mode101,3867 (defun mmm-mode-on ()mmm-mode-on140,5372 (defun mmm-mode-off ()mmm-mode-off181,7048 (defvar mmm-mode-map (make-sparse-keymap)mmm-mode-map206,7760 (defvar mmm-mode-prefix-map (make-sparse-keymap)mmm-mode-prefix-map209,7835 (defvar mmm-mode-menu-map (make-sparse-keymap "MMM")mmm-mode-menu-map212,7945 (defun mmm-define-key (key binding &optional keymap)mmm-define-key215,8036 (define-key mmm-mode-prefix-map [?h] 'mmm-insertion-help)mmm-mode-prefix-map239,8791 (define-key mmm-mode-prefix-map (vector help-char) prefix-help-command)mmm-mode-prefix-map246,9049 (define-key mmm-mode-map mmm-mode-prefix-key mmm-mode-prefix-map)mmm-mode-map249,9160 (define-key mmm-mode-menu-map [off]mmm-mode-menu-map252,9262 (define-key mmm-mode-menu-map [sep0] '(menu-item "----"))mmm-mode-menu-map254,9334 (define-key mmm-mode-menu-map [clhist]mmm-mode-menu-map256,9393 (define-key mmm-mode-menu-map [end]mmm-mode-menu-map258,9474 (define-key mmm-mode-menu-map [clear]mmm-mode-menu-map260,9555 (define-key mmm-mode-menu-map [reparse]mmm-mode-menu-map262,9642 (define-key mmm-mode-menu-map [sep10] '(menu-item "----"))mmm-mode-menu-map265,9736 (define-key mmm-mode-menu-map [ins-help]mmm-mode-menu-map267,9796 (define-key mmm-mode-menu-map [sep20] '(menu-item "----"))mmm-mode-menu-map270,9887 (define-key mmm-mode-menu-map [region]mmm-mode-menu-map272,9947 (define-key mmm-mode-menu-map [regexp]mmm-mode-menu-map274,10054 (define-key mmm-mode-menu-map [class]mmm-mode-menu-map276,10139 (define-key mmm-mode-menu-map [sep30] '(menu-item "----"))mmm-mode-menu-map279,10225 (define-key mmm-mode-menu-map [parse-region]mmm-mode-menu-map281,10285 (define-key mmm-mode-menu-map [parse-buffer]mmm-mode-menu-map283,10398 (define-key mmm-mode-menu-map [parse-block]mmm-mode-menu-map285,10483 (define-key mmm-mode-map [menu-bar mmm] (cons "MMM" mmm-mode-menu-map))mmm-mode-map288,10566 contrib/mmm/mmm-region.el,3064 (defsubst mmm-overlay-at (&optional pos type)mmm-overlay-at54,1749 (defun mmm-overlays-at (&optional pos type)mmm-overlays-at59,1934 (defun mmm-included-p (ovl pos &optional type)mmm-included-p72,2387 (defun mmm-overlays-containing (start stop)mmm-overlays-containing112,3876 (defun mmm-overlays-contained-in (start stop)mmm-overlays-contained-in125,4314 (defun mmm-overlays-overlapping (start stop)mmm-overlays-overlapping138,4754 (defun mmm-sort-overlays (overlays)mmm-sort-overlays149,5117 (defvar mmm-current-overlay nilmmm-current-overlay158,5359 (defvar mmm-previous-overlay nilmmm-previous-overlay163,5574 (defvar mmm-current-submode nilmmm-current-submode168,5762 (defvar mmm-previous-submode nilmmm-previous-submode173,5962 (defun mmm-update-current-submode (&optional pos)mmm-update-current-submode178,6135 (defun mmm-set-current-submode (mode &optional pos)mmm-set-current-submode199,6930 (defun mmm-submode-at (&optional pos type)mmm-submode-at210,7373 (defun mmm-match-front (ovl)mmm-match-front219,7648 (defun mmm-match-back (ovl)mmm-match-back238,8409 (defun mmm-front-start (ovl)mmm-front-start257,9154 (defun mmm-back-end (ovl)mmm-back-end265,9458 (defun mmm-valid-submode-region (submode beg end)mmm-valid-submode-region278,9805 (defun* mmm-make-regionmmm-make-region305,10961 (defun mmm-make-overlay (submode beg end name face beg-sticky end-sticky evapmmm-make-overlay431,16311 (defun mmm-get-face (face submode &optional delim)mmm-get-face459,17444 (defun mmm-clear-overlays (&optional start stop strict)mmm-clear-overlays470,17736 (defun mmm-update-mode-info (mode &optional force)mmm-update-mode-info486,18201 (defun mmm-update-submode-region ()mmm-update-submode-region571,21841 (defun mmm-add-hooks ()mmm-add-hooks588,22571 (defun mmm-remove-hooks ()mmm-remove-hooks591,22668 (defun mmm-get-local-variables-list (type mode)mmm-get-local-variables-list597,22795 (defun mmm-get-locals (type)mmm-get-locals617,23491 (defun mmm-get-saved-local (mode var)mmm-get-saved-local630,23988 (defun mmm-set-local-variables (mode)mmm-set-local-variables634,24153 (defun mmm-get-saved-local-variables (mode)mmm-get-saved-local-variables645,24531 (defun mmm-save-changed-local-variables (ovl mode)mmm-save-changed-local-variables653,24806 (defun mmm-clear-local-variables ()mmm-clear-local-variables672,25510 (defun mmm-enable-font-lock (mode)mmm-enable-font-lock683,25775 (defun mmm-update-font-lock-buffer ()mmm-update-font-lock-buffer691,26035 (defun mmm-refontify-maybe (&optional start stop)mmm-refontify-maybe704,26446 (defun mmm-submode-changes-in (start stop)mmm-submode-changes-in719,26926 (defun mmm-regions-in (start stop &optional flag delim)mmm-regions-in730,27283 (defun mmm-regions-alist (start stop)mmm-regions-alist744,27761 (defun mmm-fontify-region (start stop &optional loudly)mmm-fontify-region761,28288 (defun mmm-fontify-region-list (mode regions)mmm-fontify-region-list781,29284 (defun mmm-beginning-of-syntax ()mmm-beginning-of-syntax803,30032 contrib/mmm/mmm-rpm.el,242 (defconst mmm-rpm-sh-start-tagsmmm-rpm-sh-start-tags48,1618 (defvar mmm-rpm-sh-end-tagsmmm-rpm-sh-end-tags53,1842 (defvar mmm-rpm-sh-start-regexpmmm-rpm-sh-start-regexp57,2016 (defvar mmm-rpm-sh-end-regexpmmm-rpm-sh-end-regexp61,2194 contrib/mmm/mmm-sample.el,289 (defvar mmm-here-doc-mode-alist '()mmm-here-doc-mode-alist84,2601 (defun mmm-here-doc-get-mode (string)mmm-here-doc-get-mode93,3086 (defun mmm-file-variables-verify ()mmm-file-variables-verify208,6343 (defun mmm-file-variables-find-back (bound)mmm-file-variables-find-back232,7148 contrib/mmm/mmm-univ.el,60 (defun mmm-univ-get-mode (string)mmm-univ-get-mode38,1205 contrib/mmm/mmm-utils.el,555 (defmacro mmm-valid-buffer (&rest body)mmm-valid-buffer42,1332 (defmacro mmm-save-all (&rest body)mmm-save-all61,1941 (defun mmm-format-string (string arg-pairs)mmm-format-string74,2223 (defun mmm-format-matches (string &optional on-string)mmm-format-matches85,2661 (defmacro mmm-save-keyword (param)mmm-save-keyword108,3419 (defmacro mmm-save-keywords (&rest params)mmm-save-keywords116,3746 (defun mmm-looking-back-at (regexp &optional bound)mmm-looking-back-at129,4244 (defun mmm-make-marker (pos beg-p sticky-p)mmm-make-marker146,4784 contrib/mmm/mmm-vars.el,4660 (defgroup mmm nilmmm104,3283 (defvar mmm-c-derived-modesmmm-c-derived-modes111,3393 (defvar mmm-save-local-variablesmmm-save-local-variables115,3512 (defvar mmm-buffer-saved-locals ()mmm-buffer-saved-locals341,10293 (defvar mmm-region-saved-locals-defaults ()mmm-region-saved-locals-defaults346,10493 (defvar mmm-region-saved-locals-for-dominant ()mmm-region-saved-locals-for-dominant352,10753 (defgroup mmm-faces nilmmm-faces362,11130 (defcustom mmm-submode-decoration-level 1mmm-submode-decoration-level368,11301 (defface mmm-init-submode-face '((t (:background "Pink")))mmm-init-submode-face386,12145 (defface mmm-cleanup-submode-face '((t (:background "Wheat")))mmm-cleanup-submode-face390,12285 (defface mmm-declaration-submode-face '((t (:background "Aquamarine")))mmm-declaration-submode-face394,12422 (defface mmm-comment-submode-face '((t (:background "SkyBlue")))mmm-comment-submode-face398,12568 (defface mmm-output-submode-face '((t (:background "Plum")))mmm-output-submode-face402,12721 (defface mmm-special-submode-face '((t (:background "MediumSpringGreen")))mmm-special-submode-face406,12870 (defface mmm-code-submode-face '((t (:background "LightGray")))mmm-code-submode-face410,13034 (defface mmm-default-submode-face '((t (:background "gray85")))mmm-default-submode-face414,13173 (defface mmm-delimiter-face nilmmm-delimiter-face419,13381 (defcustom mmm-mode-string " MMM"mmm-mode-string426,13507 (defcustom mmm-submode-mode-line-format "~M[~m]"mmm-submode-mode-line-format431,13638 (defvar mmm-primary-mode-display-name nilmmm-primary-mode-display-name448,14293 (defvar mmm-buffer-mode-display-name nilmmm-buffer-mode-display-name453,14507 (defun mmm-set-mode-line ()mmm-set-mode-line459,14806 (defvar mmm-classes nilmmm-classes483,15614 (defvar mmm-global-classes '(universal)mmm-global-classes489,15859 (defcustom mmm-mode-ext-classes-alist nilmmm-mode-ext-classes-alist496,16041 (defun mmm-add-mode-ext-class (mode ext class)mmm-add-mode-ext-class515,16831 (defcustom mmm-major-mode-preferencesmmm-major-mode-preferences524,17156 (defun mmm-add-to-major-mode-preferences (language mode &optional default)mmm-add-to-major-mode-preferences542,17884 (defun mmm-ensure-modename (symbol)mmm-ensure-modename558,18642 (defun mmm-modename->function (mode)mmm-modename->function567,18945 (defcustom mmm-delimiter-mode 'fundamental-modemmm-delimiter-mode581,19394 (defcustom mmm-mode-prefix-key [(control ?c) ?%]mmm-mode-prefix-key591,19663 (defcustom mmm-command-modifiers '(control)mmm-command-modifiers596,19790 (defcustom mmm-insert-modifiers '()mmm-insert-modifiers610,20423 (defcustom mmm-use-old-command-keys nilmmm-use-old-command-keys625,21101 (defun mmm-use-old-command-keys ()mmm-use-old-command-keys635,21565 (defcustom mmm-mode-hook ()mmm-mode-hook643,21757 (defun mmm-run-constructed-hook (body &optional suffix)mmm-run-constructed-hook663,22564 (defun mmm-run-major-hook ()mmm-run-major-hook671,22908 (defun mmm-run-submode-hook (submode)mmm-run-submode-hook674,22985 (defvar mmm-class-hooks-run ()mmm-class-hooks-run677,23072 (defun mmm-run-class-hook (class)mmm-run-class-hook682,23244 (defvar mmm-primary-mode-entry-hook nilmmm-primary-mode-entry-hook687,23416 (defcustom mmm-major-mode-hook ()mmm-major-mode-hook702,24063 (defun mmm-run-major-mode-hook ()mmm-run-major-mode-hook716,24694 (defcustom mmm-global-mode nilmmm-global-mode729,25235 (defcustom mmm-never-modesmmm-never-modes745,25902 (defvar mmm-set-file-name-for-modes '(mew-draft-mode)mmm-set-file-name-for-modes763,26202 (defvar mmm-mode nilmmm-mode774,26561 (defvar mmm-primary-mode nilmmm-primary-mode782,26769 (defvar mmm-classes-alist nilmmm-classes-alist793,27135 (defun mmm-add-classes (classes)mmm-add-classes948,35342 (defun mmm-add-group (group classes)mmm-add-group953,35507 (defun mmm-add-to-group (group classes)mmm-add-to-group963,35880 (defconst mmm-version "0.4.8"mmm-version977,36307 (defun mmm-version ()mmm-version980,36372 (defvar mmm-temp-buffer-name " *mmm-temp*"mmm-temp-buffer-name987,36515 (defvar mmm-interactive-history nilmmm-interactive-history993,36645 (defun mmm-add-to-history (class)mmm-add-to-history999,36914 (defun mmm-clear-history ()mmm-clear-history1002,36997 (defvar mmm-mode-ext-classes ()mmm-mode-ext-classes1010,37182 (defun mmm-get-mode-ext-classes ()mmm-get-mode-ext-classes1015,37393 (defun mmm-clear-mode-ext-classes ()mmm-clear-mode-ext-classes1024,37720 (defun mmm-mode-ext-applies (element)mmm-mode-ext-applies1028,37845 (defun mmm-get-all-classes (global)mmm-get-all-classes1042,38224