path: root/TAGS


acl2/acl2.el,0

ccc/ccc.el,138
(defvar ccc-keywords nil)ccc-keywords
17,587
(defvar ccc-tactics nil)ccc-tactics
18,613
(defvar ccc-tacticals nil)ccc-tacticals
19,638

coq/coq-abbrev.el,766
(defun holes-show-doc ()holes-show-doc
12,313
(defun coq-local-vars-list-show-doc ()coq-local-vars-list-show-doc
16,390
(defconst coq-tactics-menucoq-tactics-menu
21,490
(defconst coq-tactics-abbrev-tablecoq-tactics-abbrev-table
26,667
(defconst coq-tacticals-menucoq-tacticals-menu
29,784
(defconst coq-tacticals-abbrev-tablecoq-tacticals-abbrev-table
33,893
(defconst coq-commands-menucoq-commands-menu
36,984
(defconst coq-commands-abbrev-tablecoq-commands-abbrev-table
43,1207
(defconst coq-terms-menucoq-terms-menu
46,1296
(defconst coq-terms-abbrev-tablecoq-terms-abbrev-table
51,1434
(defun coq-install-abbrevs ()coq-install-abbrevs
58,1628
(defpgdefault menu-entriesmenu-entries
83,2604
(defpgdefault help-menu-entrieshelp-menu-entries
148,4718

coq/coq-autotest.el,0

coq/coq-db.el,1218
(defconst coq-syntax-db nilcoq-syntax-db
24,596
(defun coq-insert-from-db (db prompt)coq-insert-from-db
70,2319
(defun coq-build-regexp-list-from-db (db &optional filter)coq-build-regexp-list-from-db
88,3050
(defun coq-build-opt-regexp-from-db (db &optional filter)coq-build-opt-regexp-from-db
107,3856
(defun max-length-db (db)max-length-db
126,4677
(defun coq-build-menu-from-db-internal (db lgth menuwidth)coq-build-menu-from-db-internal
138,4952
(defun coq-build-title-menu (db size)coq-build-title-menu
175,6493
(defun coq-sort-menu-entries (menu)coq-sort-menu-entries
184,6861
(defun coq-build-menu-from-db (db &optional size)coq-build-menu-from-db
190,6988
(defcustom coq-holes-minor-mode tcoq-holes-minor-mode
212,7827
(defun coq-build-abbrev-table-from-db (db)coq-build-abbrev-table-from-db
218,7971
(defun filter-state-preserving (l)filter-state-preserving
237,8609
(defun filter-state-changing (l)filter-state-changing
242,8763
(defface coq-solve-tactics-facecoq-solve-tactics-face
249,8984
(defface coq-cheat-facecoq-cheat-face
258,9314
(defconst coq-solve-tactics-face 'coq-solve-tactics-facecoq-solve-tactics-face
266,9562
(defconst coq-cheat-face 'coq-cheat-facecoq-cheat-face
270,9726

coq/coq.el,13867
(defcustom coq-translate-to-v8 nilcoq-translate-to-v8
59,1804
(defun coq-build-prog-args ()coq-build-prog-args
65,1984
(defcustom coq-compilercoq-compiler
75,2278
(defcustom coq-dependency-analyzercoq-dependency-analyzer
81,2415
(defcustom coq-compile-file-command (concat coq-compiler " %s")coq-compile-file-command
87,2555
(defcustom coq-use-makefile nilcoq-use-makefile
95,2892
(defcustom coq-default-undo-limit 200coq-default-undo-limit
103,3115
(defconst coq-shell-init-cmdcoq-shell-init-cmd
108,3243
(defcustom coq-prog-env nilcoq-prog-env
116,3508
(defconst coq-shell-restart-cmd "Reset Initial.\n ")coq-shell-restart-cmd
124,3758
(defvar coq-shell-prompt-patterncoq-shell-prompt-pattern
126,3812
(defvar coq-shell-cd nilcoq-shell-cd
134,4115
(defvar coq-shell-proof-completed-regexp "Subtree\\s-proved!\\|Proof\\s-completed"coq-shell-proof-completed-regexp
138,4275
(defvar coq-goal-regexpcoq-goal-regexp
141,4430
(defun get-coq-library-directory ()get-coq-library-directory
146,4526
(defconst coq-library-directory (get-coq-library-directory)coq-library-directory
152,4708
(defcustom coq-tags (concat coq-library-directory "/theories/TAGS")coq-tags
155,4834
(defconst coq-interrupt-regexp "User Interrupt."coq-interrupt-regexp
160,4982
(defcustom coq-www-home-page "http://coq.inria.fr/"coq-www-home-page
163,5075
(defvar coq-outline-regexpcoq-outline-regexp
174,5250
(defvar coq-outline-heading-end-regexp "\\.[ \t\n]")coq-outline-heading-end-regexp
181,5462
(defvar coq-shell-outline-regexp coq-goal-regexp)coq-shell-outline-regexp
183,5516
(defvar coq-shell-outline-heading-end-regexp coq-goal-regexp)coq-shell-outline-heading-end-regexp
184,5566
(defconst coq-state-preserving-tactics-regexpcoq-state-preserving-tactics-regexp
187,5630
(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp
189,5732
(defconst coq-state-preserving-commands-regexpcoq-state-preserving-commands-regexp
191,5841
(defconst coq-commands-regexpcoq-commands-regexp
193,5954
(defvar coq-retractable-instruct-regexpcoq-retractable-instruct-regexp
195,6033
(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp
197,6125
(defcustom coq-use-smie tcoq-use-smie
229,6821
(defconst coq-smie-grammarcoq-smie-grammar
237,7049
(defun coq-smie-rules (kind token)coq-smie-rules
275,8870
(defun coq-set-undo-limit (undos)coq-set-undo-limit
298,9601
(defun build-list-id-from-string (s)build-list-id-from-string
302,9731
(defun coq-last-prompt-info (s)coq-last-prompt-info
314,10229
(defun coq-last-prompt-info-safe ()coq-last-prompt-info-safe
326,10761
(defvar coq-last-but-one-statenum 1coq-last-but-one-statenum
332,11018
(defvar coq-last-but-one-proofnum 1coq-last-but-one-proofnum
339,11316
(defvar coq-last-but-one-proofstack '()coq-last-but-one-proofstack
342,11414
(defsubst coq-get-span-statenum (span)coq-get-span-statenum
345,11524
(defsubst coq-get-span-proofnum (span)coq-get-span-proofnum
349,11639
(defsubst coq-get-span-proofstack (span)coq-get-span-proofstack
353,11754
(defsubst coq-set-span-statenum (span val)coq-set-span-statenum
357,11898
(defsubst coq-get-span-goalcmd (span)coq-get-span-goalcmd
361,12029
(defsubst coq-set-span-goalcmd (span val)coq-set-span-goalcmd
365,12143
(defsubst coq-set-span-proofnum (span val)coq-set-span-proofnum
369,12273
(defsubst coq-set-span-proofstack (span val)coq-set-span-proofstack
373,12404
(defsubst proof-last-locked-span ()proof-last-locked-span
377,12564
(defun proof-clone-buffer (s &optional erase)proof-clone-buffer
381,12698
(defun proof-store-buffer-win (buffer &optional erase)proof-store-buffer-win
395,13233
(defun proof-store-response-win (&optional erase)proof-store-response-win
406,13726
(defun proof-store-goals-win (&optional erase)proof-store-goals-win
410,13853
(defun coq-set-state-infos ()coq-set-state-infos
422,14385
(defun count-not-intersection (l notin)count-not-intersection
460,16472
(defun coq-find-and-forget (span)coq-find-and-forget
490,17724
(defvar coq-current-goal 1coq-current-goal
517,19032
(defun coq-goal-hyp ()coq-goal-hyp
520,19097
(defun coq-state-preserving-p (cmd)coq-state-preserving-p
533,19571
(defconst notation-print-kinds-tablenotation-print-kinds-table
547,19885
(defun coq-PrintScope ()coq-PrintScope
551,20052
(defun coq-guess-or-ask-for-string (s &optional dontguess)coq-guess-or-ask-for-string
569,20601
(defun coq-ask-do (ask do &optional dontguess postformatcmd)coq-ask-do
583,21141
(defsubst coq-put-into-brackets (s)coq-put-into-brackets
592,21526
(defsubst coq-put-into-quotes (s) coq-put-into-quotes
595,21587
(defun coq-SearchIsos ()coq-SearchIsos
598,21647
(defun coq-SearchConstant ()coq-SearchConstant
606,21888
(defun coq-Searchregexp ()coq-Searchregexp
610,21981
(defun coq-SearchRewrite ()coq-SearchRewrite
616,22124
(defun coq-SearchAbout ()coq-SearchAbout
620,22221
(defun coq-Print () coq-Print
626,22366
(defun coq-About () coq-About
631,22491
(defun coq-LocateConstant ()coq-LocateConstant
636,22611
(defun coq-LocateLibrary ()coq-LocateLibrary
641,22714
(defun coq-LocateNotation ()coq-LocateNotation
646,22831
(defun coq-Pwd ()coq-Pwd
654,23063
(defun coq-Inspect ()coq-Inspect
659,23187
(defun coq-PrintSection()coq-PrintSection
663,23287
(defun coq-Print-implicit ()coq-Print-implicit
667,23380
(defun coq-Check ()coq-Check
672,23531
(defun coq-Show ()coq-Show
677,23639
(defun coq-Compile ()coq-Compile
691,24082
(defun coq-guess-command-line (filename)coq-guess-command-line
703,24400
(defpacustom use-editing-holes tuse-editing-holes
740,25953
(defun coq-mode-config ()coq-mode-config
749,26256
(defun coq-shell-mode-config ()coq-shell-mode-config
845,29749
(defun coq-goals-mode-config ()coq-goals-mode-config
890,31577
(defun coq-response-config ()coq-response-config
897,31821
(defpacustom print-fully-explicit nilprint-fully-explicit
922,32646
(defpacustom print-implicit nilprint-implicit
927,32794
(defpacustom print-coercions nilprint-coercions
932,32960
(defpacustom print-match-wildcards tprint-match-wildcards
937,33104
(defpacustom print-elim-types tprint-elim-types
942,33284
(defpacustom printing-depth 50printing-depth
947,33450
(defpacustom undo-depth coq-default-undo-limitundo-depth
952,33611
(defpacustom time-commands niltime-commands
957,33777
(defpacustom auto-compile-vos nilauto-compile-vos
961,33887
(defun coq-maybe-compile-buffer ()coq-maybe-compile-buffer
990,35001
(defun coq-ancestors-of (filename)coq-ancestors-of
1026,36529
(defun coq-all-ancestors-of (filename)coq-all-ancestors-of
1049,37493
(defun coq-process-require-command (span cmd)coq-process-require-command
1060,37840
(defun coq-included-children (filename)coq-included-children
1065,37967
(defun coq-process-file (rfilename)coq-process-file
1086,38806
(defgroup coq-auto-compile ()coq-auto-compile
1114,39791
(defcustom coq-compile-before-require nilcoq-compile-before-require
1119,39942
(defcustom coq-compile-command ""coq-compile-command
1128,40344
(defcustom coq-confirm-external-compilation-command tcoq-confirm-external-compilation-command
1158,41652
(defconst coq-compile-substitution-listcoq-compile-substitution-list
1164,41880
(defcustom coq-compile-auto-save 'ask-coqcoq-compile-auto-save
1184,42801
(defcustom coq-lock-ancestors tcoq-lock-ancestors
1209,43860
(defcustom coq-compile-ignore-library-directory tcoq-compile-ignore-library-directory
1218,44175
(defcustom coq-compile-ignored-directories nilcoq-compile-ignored-directories
1230,44659
(defcustom coq-load-path nilcoq-load-path
1243,45293
(defcustom coq-load-path-include-current tcoq-load-path-include-current
1258,45850
(defconst coq-require-command-regexpcoq-require-command-regexp
1267,46169
(defconst coq-require-id-regexpcoq-require-id-regexp
1274,46526
(defvar coq-compile-history nilcoq-compile-history
1282,46960
(defun time-less-or-equal (time-1 time-2)time-less-or-equal
1287,47064
(defun coq-max-dep-mod-time (dep-mod-times)coq-max-dep-mod-time
1295,47402
(defun coq-prog-args ()coq-prog-args
1318,48206
(defun coq-lock-ancestor (span ancestor-src)coq-lock-ancestor
1327,48465
(defun coq-unlock-ancestor (ancestor-src)coq-unlock-ancestor
1343,49240
(defun coq-unlock-all-ancestors-of-span (span)coq-unlock-all-ancestors-of-span
1355,49733
(defun coq-compile-ignore-file (lib-obj-file)coq-compile-ignore-file
1362,50029
(defun coq-library-src-of-obj-file (lib-obj-file)coq-library-src-of-obj-file
1382,50810
(defun coq-include-options (file)coq-include-options
1387,51042
(defun coq-get-library-dependencies (lib-src-file)coq-get-library-dependencies
1406,51815
(defun coq-compile-library (src-file)coq-compile-library
1435,53158
(defun coq-compile-library-if-necessary (max-dep-obj-time src obj)coq-compile-library-if-necessary
1461,54263
(defun coq-make-lib-up-to-date (coq-obj-hash span lib-obj-file)coq-make-lib-up-to-date
1506,56097
(defun coq-auto-compile-externally (span qualified-id absolute-module-obj-file)coq-auto-compile-externally
1561,58526
(defun coq-map-module-id-to-obj-file (module-id)coq-map-module-id-to-obj-file
1604,60688
(defun coq-check-module (coq-object-local-hash-symbol span module-id)coq-check-module
1632,61873
(defvar coq-process-require-current-buffercoq-process-require-current-buffer
1660,63310
(defun coq-compile-save-buffer-filter ()coq-compile-save-buffer-filter
1666,63575
(defun coq-compile-save-some-buffers ()coq-compile-save-some-buffers
1676,63989
(defun coq-preprocess-require-commands ()coq-preprocess-require-commands
1698,64891
(defun coq-switch-buffer-kill-proof-shell ()coq-switch-buffer-kill-proof-shell
1731,66453
(defun coq-preprocessing ()coq-preprocessing
1751,67129
(defun coq-fake-constant-markup ()coq-fake-constant-markup
1765,67584
(defun coq-create-span-menu (span idiom name)coq-create-span-menu
1781,68189
(defconst module-kinds-tablemodule-kinds-table
1799,68702
(defconst modtype-kinds-tablemodtype-kinds-table
1803,68851
(defun coq-insert-section-or-module ()coq-insert-section-or-module
1807,68980
(defconst reqkinds-kinds-tablereqkinds-kinds-table
1828,69830
(defun coq-insert-requires ()coq-insert-requires
1832,69974
(defun coq-end-Section ()coq-end-Section
1845,70454
(defun coq-insert-intros ()coq-insert-intros
1863,71032
(defun coq-insert-infoH-hook ()coq-insert-infoH-hook
1875,71565
(defun coq-insert-as ()coq-insert-as
1880,71773
(defun coq-insert-match ()coq-insert-match
1897,72466
(defun coq-insert-solve-tactic ()coq-insert-solve-tactic
1926,73636
(defun coq-insert-tactic ()coq-insert-tactic
1932,73887
(defun coq-insert-tactical ()coq-insert-tactical
1938,74089
(defun coq-insert-command ()coq-insert-command
1944,74320
(defun coq-insert-term ()coq-insert-term
1949,74485
(define-key coq-keymap [(control ?i)] 'coq-insert-intros)coq-keymap
1954,74646
(define-key coq-keymap [(control ?m)] 'coq-insert-match)coq-keymap
1955,74704
(define-key coq-keymap [(control ?()] 'coq-insert-section-or-module)coq-keymap
1956,74761
(define-key coq-keymap [(control ?))] 'coq-end-Section)coq-keymap
1957,74830
(define-key coq-keymap [(control ?s)] 'coq-Show)coq-keymap
1958,74886
(define-key coq-keymap [(control ?t)] 'coq-insert-tactic)coq-keymap
1959,74935
(define-key coq-keymap [(control ?T)] 'coq-insert-tactical)coq-keymap
1960,74993
(define-key coq-keymap [(control ?r)] 'proof-store-response-win)coq-keymap
1961,75053
(define-key coq-keymap [(control ?G)] 'proof-store-goals-win)coq-keymap
1962,75118
(define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in ttycoq-keymap
1965,75246
(define-key coq-keymap [(control ?\s)] 'coq-insert-term)coq-keymap
1967,75320
(define-key coq-keymap [(control return)] 'coq-insert-command)coq-keymap
1968,75377
(define-key coq-keymap [(control ?o)] 'coq-SearchIsos)coq-keymap
1972,75502
(define-key coq-keymap [(control ?p)] 'coq-Print)coq-keymap
1974,75558
(define-key coq-keymap [(control ?b)] 'coq-About)coq-keymap
1975,75608
(define-key coq-keymap [(control ?a)] 'coq-SearchAbout)coq-keymap
1976,75658
(define-key coq-keymap [(control ?c)] 'coq-Check)coq-keymap
1977,75714
(define-key coq-keymap [(control ?H)] 'coq-PrintHint)coq-keymap
1978,75764
(define-key coq-keymap [(control ?l)] 'coq-LocateConstant)coq-keymap
1979,75818
(define-key coq-keymap [(control ?n)] 'coq-LocateNotation)coq-keymap
1980,75877
(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check)coq-goals-mode-map
1983,75938
(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?p)] 'coq-Print)coq-goals-mode-map
1984,76020
(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?o)] 'coq-SearchIsos)coq-goals-mode-map
1985,76102
(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?b)] 'coq-About)coq-goals-mode-map
1986,76189
(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-SearchAbout)coq-goals-mode-map
1987,76271
(defvar last-coq-error-location nillast-coq-error-location
1996,76573
(defun coq-get-last-error-location (&optional parseresp clean)coq-get-last-error-location
2004,76957
(defun coq-highlight-error (&optional parseresp clean)coq-highlight-error
2054,79520
(defun coq-highlight-error-hook ()coq-highlight-error-hook
2082,80601
(defun first-word-of-buffer ()first-word-of-buffer
2092,80818
(defun coq-show-first-goal ()coq-show-first-goal
2100,81021
(defvar coq-modeline-string2 ")")coq-modeline-string2
2117,81716
(defvar coq-modeline-string1 ")")coq-modeline-string1
2118,81750
(defvar coq-modeline-string0 " Script(")coq-modeline-string0
2119,81784
(defun coq-build-subgoals-string (n)coq-build-subgoals-string
2120,81825
(defun coq-update-minor-mode-alist ()coq-update-minor-mode-alist
2125,81991
(defun is-not-split-vertic (selected-window)is-not-split-vertic
2157,83385
(defun optim-resp-windows ()optim-resp-windows
2166,83825

coq/coq-indent.el,4608
(defconst coq-any-command-regexpcoq-any-command-regexp
20,368
(defconst coq-indent-inner-regexpcoq-indent-inner-regexp
23,442
(defconst coq-comment-start-regexp "(\\*")coq-comment-start-regexp
33,796
(defconst coq-comment-end-regexp "\\*)")coq-comment-end-regexp
34,839
(defconst coq-comment-start-or-end-regexpcoq-comment-start-or-end-regexp
35,880
(defconst coq-indent-open-regexpcoq-indent-open-regexp
37,988
(defconst coq-indent-close-regexpcoq-indent-close-regexp
42,1164
(defconst coq-indent-closepar-regexp "\\s)")coq-indent-closepar-regexp
45,1275
(defconst coq-indent-closematch-regexp (proof-ids-to-regexp '("end")))coq-indent-closematch-regexp
46,1320
(defconst coq-indent-openpar-regexp "\\s(")coq-indent-openpar-regexp
47,1391
(defconst coq-indent-openmatch-regexp (proof-ids-to-regexp '("match" "Cases")))coq-indent-openmatch-regexp
48,1435
(defconst coq-tacticals-tactics-regexcoq-tacticals-tactics-regex
49,1515
(defconst coq-indent-any-regexpcoq-indent-any-regexp
51,1634
(defconst coq-indent-kwcoq-indent-kw
55,1850
(defconst coq-indent-pattern-regexp "\\(|\\(?:(\\|\\s-\\|\\w\\|\n\\)\\|with\\)")coq-indent-pattern-regexp
65,2316
(defun coq-indent-goal-command-p (str)coq-indent-goal-command-p
69,2419
(defconst coq-end-command-regexpcoq-end-command-regexp
91,3470
(defun coq-search-comment-delimiter-forward ()coq-search-comment-delimiter-forward
96,3622
(defun coq-search-comment-delimiter-backward ()coq-search-comment-delimiter-backward
105,3952
(defun coq-skip-until-one-comment-backward ()coq-skip-until-one-comment-backward
112,4226
(defun coq-skip-until-one-comment-forward ()coq-skip-until-one-comment-forward
127,4933
(defun coq-looking-at-comment ()coq-looking-at-comment
138,5451
(defun coq-find-comment-start ()coq-find-comment-start
142,5592
(defun coq-find-comment-end ()coq-find-comment-end
153,6025
(defun coq-looking-at-syntactic-context ()coq-looking-at-syntactic-context
165,6518
(defconst coq-end-command-or-comment-regexpcoq-end-command-or-comment-regexp
171,6740
(defconst coq-end-command-or-comment-start-regexpcoq-end-command-or-comment-start-regexp
174,6849
(defun coq-find-not-in-comment-backward (reg &optional lim submatch)coq-find-not-in-comment-backward
178,6967
(defun coq-find-not-in-comment-forward (reg &optional lim submatch)coq-find-not-in-comment-forward
198,7868
(defun coq-find-command-end-backward ()coq-find-command-end-backward
222,9007
(defun coq-find-command-end-forward ()coq-find-command-end-forward
231,9398
(defun coq-find-command-end (direction)coq-find-command-end
240,9775
(defun coq-find-current-start ()coq-find-current-start
248,10107
(defun coq-find-real-start ()coq-find-real-start
257,10398
(defun coq-command-at-point ()coq-command-at-point
264,10617
(defun same-line (pt pt2)same-line
272,10903
(defun coq-commands-at-line ()coq-commands-at-line
275,10990
(defun coq-indent-only-spaces-on-line ()coq-indent-only-spaces-on-line
294,11613
(defun coq-indent-find-reg (lim reg)coq-indent-find-reg
300,11890
(defun coq-find-no-syntactic-on-line ()coq-find-no-syntactic-on-line
314,12426
(defun coq-back-to-indentation-prevline ()coq-back-to-indentation-prevline
327,12899
(defun coq-find-unclosed (&optional optlvl limit openreg closereg)coq-find-unclosed
370,14785
(defun coq-find-at-same-level-zero (limit openreg)coq-find-at-same-level-zero
400,16095
(defun coq-find-unopened (&optional optlvl limit)coq-find-unopened
429,17361
(defun coq-find-last-unopened (&optional optlvl limit)coq-find-last-unopened
472,18795
(defun coq-end-offset (&optional limit)coq-end-offset
483,19192
(defun coq-add-iter (l f)coq-add-iter
508,19962
(defun coq-goal-count (l) (coq-add-iter l 'coq-indent-goal-command-p))coq-goal-count
511,20068
(defun coq-save-count (l) (coq-add-iter l '(lambda (x) (coq-save-command-p nil x))))coq-save-count
513,20140
(defun coq-proof-count (l)coq-proof-count
515,20226
(defun coq-goal-save-diff-maybe-proof (l)coq-goal-save-diff-maybe-proof
519,20401
(defun coq-indent-command-offset (kind prevcol prevpoint)coq-indent-command-offset
526,20622
(defun coq-indent-expr-offset (kind prevcol prevpoint record)coq-indent-expr-offset
558,22225
(defun coq-indent-comment-offset ()coq-indent-comment-offset
673,26909
(defun coq-indent-offset (&optional notcomments)coq-indent-offset
705,28358
(defun coq-indent-calculate (&optional notcomments)coq-indent-calculate
724,29233
(defun coq-indent-line ()coq-indent-line
727,29321
(defun coq-indent-line-not-comments ()coq-indent-line-not-comments
737,29687
(defun coq-indent-region (start end)coq-indent-region
747,30076

coq/coq-local-vars.el,565
(defconst coq-local-vars-doc nilcoq-local-vars-doc
20,429
(defun coq-insert-coq-prog-name (progname progargs)coq-insert-coq-prog-name
78,2957
(defun coq-read-directory (prompt &optional default maynotmatch initialcontent)coq-read-directory
89,3430
(defun coq-extract-directories-from-args (args)coq-extract-directories-from-args
113,4533
(defun coq-ask-prog-args (&optional oldvalue)coq-ask-prog-args
128,5085
(defun coq-ask-prog-name (&optional oldvalue)coq-ask-prog-name
150,6153
(defun coq-ask-insert-coq-prog-name ()coq-ask-insert-coq-prog-name
167,6864

coq/coq-mmm.el,0

coq/coq-syntax.el,4741
(defcustom coq-prog-name  ;; da: moved from coq.el since needed herecoq-prog-name
18,560
(defcustom coq-user-tactics-db nilcoq-user-tactics-db
38,1342
(defcustom coq-user-commands-db nilcoq-user-commands-db
55,1855
(defcustom coq-user-tacticals-db nilcoq-user-tacticals-db
71,2374
(defcustom coq-user-solve-tactics-db nilcoq-user-solve-tactics-db
87,2895
(defcustom coq-user-cheat-tactics-db nilcoq-user-cheat-tactics-db
103,3414
(defcustom coq-user-reserved-db nilcoq-user-reserved-db
122,3960
(defvar coq-tactics-dbcoq-tactics-db
140,4491
(defvar coq-solve-tactics-dbcoq-solve-tactics-db
298,12750
(defvar coq-solve-cheat-tactics-dbcoq-solve-cheat-tactics-db
321,13595
(defvar coq-tacticals-dbcoq-tacticals-db
333,13770
(defvar coq-decl-dbcoq-decl-db
357,14656
(defvar coq-defn-dbcoq-defn-db
382,16112
(defvar coq-goal-starters-dbcoq-goal-starters-db
440,20467
(defvar coq-other-commands-dbcoq-other-commands-db
469,22224
(defvar coq-commands-dbcoq-commands-db
598,31690
(defvar coq-terms-dbcoq-terms-db
605,31910
(defun coq-count-match (regexp strg)coq-count-match
667,34525
(defun coq-module-opening-p (str)coq-module-opening-p
683,35254
(defun coq-section-command-p (str)coq-section-command-p
694,35665
(defun coq-goal-command-str-p (str)coq-goal-command-str-p
698,35762
(defun coq-goal-command-p (span)coq-goal-command-p
725,36864
(defvar coq-keywords-save-strictcoq-keywords-save-strict
734,37147
(defvar coq-keywords-savecoq-keywords-save
743,37260
(defun coq-save-command-p (span str)coq-save-command-p
747,37338
(defvar coq-keywords-kill-goalcoq-keywords-kill-goal
758,37666
(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands
762,37756
(defvar coq-keywords-goalcoq-keywords-goal
765,37881
(defvar coq-keywords-declcoq-keywords-decl
768,37964
(defvar coq-keywords-defncoq-keywords-defn
771,38038
(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands
775,38113
(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands
784,38373
(defvar coq-keywords-commandscoq-keywords-commands
789,38589
(defvar coq-solve-tacticscoq-solve-tactics
794,38737
(defvar coq-solve-tactics-regexpcoq-solve-tactics-regexp
798,38858
(defvar coq-solve-cheat-tacticscoq-solve-cheat-tactics
802,38992
(defvar coq-solve-cheat-tactics-regexpcoq-solve-cheat-tactics-regexp
806,39137
(defvar coq-tacticalscoq-tacticals
810,39295
(defvar coq-reservedcoq-reserved
816,39434
(defvar coq-reserved-regexp (proof-ids-to-regexp coq-reserved))coq-reserved-regexp
826,39761
(defvar coq-state-changing-tacticscoq-state-changing-tactics
828,39826
(defvar coq-state-preserving-tacticscoq-state-preserving-tactics
831,39935
(defvar coq-tacticscoq-tactics
835,40049
(defvar coq-tactics-regexp (coq-build-opt-regexp-from-db coq-tactics-db))coq-tactics-regexp
838,40138
(defvar coq-retractable-instructcoq-retractable-instruct
841,40293
(defvar coq-non-retractable-instructcoq-non-retractable-instruct
844,40403
(defvar coq-keywordscoq-keywords
848,40531
(defun proof-regexp-alt-list-symb (args)proof-regexp-alt-list-symb
854,40755
(defvar coq-keywords-regexp (proof-regexp-alt-list coq-keywords))coq-keywords-regexp
857,40860
(defvar coq-symbolscoq-symbols
860,40928
(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"coq-error-regexp
879,41141
(defvar coq-id proof-id)coq-id
882,41369
(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)")coq-id-shy
883,41394
(defvar coq-ids (concat proof-id "\\(" "\\s-+" proof-id "\\)*"))coq-ids
886,41496
(defun coq-first-abstr-regexp (paren end)coq-first-abstr-regexp
888,41562
(defcustom coq-variable-highlight-enable tcoq-variable-highlight-enable
891,41657
(defvar coq-font-lock-termscoq-font-lock-terms
897,41784
(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict
919,42867
(defconst coq-save-command-regexpcoq-save-command-regexp
925,43037
(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp
930,43192
(defconst coq-goal-command-regexpcoq-goal-command-regexp
934,43352
(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp
937,43454
(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp
941,43588
(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp
948,43838
(defconst coq-with-with-hole-regexpcoq-with-with-hole-regexp
958,44128
(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1
973,44658
(defvar coq-font-lock-keywords coq-font-lock-keywords-1)coq-font-lock-keywords
1001,45993
(defun coq-init-syntax-table ()coq-init-syntax-table
1003,46051
(defconst coq-generic-expressioncoq-generic-expression
1028,46778

coq/coq-unicode-tokens.el,781
(defconst coq-token-format "%s")	; plain tokenscoq-token-format
39,1427
(defconst coq-token-match nil)coq-token-match
40,1475
(defconst coq-hexcode-match nil)coq-hexcode-match
41,1506
(defun coq-unicode-tokens-set (sym val)coq-unicode-tokens-set
43,1540
(defcustom coq-token-symbol-mapcoq-token-symbol-map
49,1768
(defcustom coq-shortcut-alistcoq-shortcut-alist
165,4719
(defconst coq-control-char-format-regexpcoq-control-char-format-regexp
254,6737
(defconst coq-control-char-format " %s ")coq-control-char-format
258,6862
(defconst coq-control-characterscoq-control-characters
260,6905
(defconst coq-control-region-format-regexp "\\(\s*%s\{\\)\\([^}]*\\)\\(\}\s*\\)")coq-control-region-format-regexp
264,6997
(defconst coq-control-regionscoq-control-regions
266,7080

hol98/hol98.el,194
(defvar hol98-keywords nil)hol98-keywords
17,419
(defvar hol98-rules nil)hol98-rules
18,447
(defvar hol98-tactics nil)hol98-tactics
19,472
(defvar hol98-tacticals nil)hol98-tacticals
20,499

isar/interface-setup.el,0

isar/isabelle-system.el,2188
(defgroup isabelle nilisabelle
28,797
(defcustom isabelle-web-pageisabelle-web-page
32,925
(defcustom isa-isabelle-commandisa-isabelle-command
41,1142
(defvar isabelle-not-found nilisabelle-not-found
59,1824
(defun isa-set-isabelle-command (&optional force)isa-set-isabelle-command
62,1939
(defun isa-shell-command-to-string (command)isa-shell-command-to-string
85,2957
(defun isa-getenv (envvar &optional default)isa-getenv
91,3181
(defcustom isabelle-program-name-override nilisabelle-program-name-override
111,3880
(defun isa-tool-list-logics ()isa-tool-list-logics
122,4226
(defcustom isabelle-logics-available nilisabelle-logics-available
129,4472
(defcustom isabelle-chosen-logic nilisabelle-chosen-logic
139,4809
(defvar isabelle-chosen-logic-prev nilisabelle-chosen-logic-prev
155,5393
(defun isabelle-hack-local-variables-function ()isabelle-hack-local-variables-function
158,5513
(defun isabelle-set-prog-name (&optional filename)isabelle-set-prog-name
170,5952
(defun isabelle-choose-logic (logic)isabelle-choose-logic
194,7072
(defun isa-view-doc (docname)isa-view-doc
213,7834
(defun isa-tool-list-docs ()isa-tool-list-docs
220,8060
(defconst isabelle-verbatim-regexp "\\`\^VERBATIM: \\(\\(.\\|\n\\)*\\)\\'"isabelle-verbatim-regexp
238,8790
(defun isabelle-verbatim (str)isabelle-verbatim
241,8932
(defcustom isabelle-refresh-logics tisabelle-refresh-logics
248,9093
(defvar isabelle-docs-menuisabelle-docs-menu
256,9421
(defvar isabelle-logics-menu-entries nilisabelle-logics-menu-entries
263,9706
(defun isabelle-logics-menu-calculate ()isabelle-logics-menu-calculate
266,9779
(defvar isabelle-time-to-refresh-logics tisabelle-time-to-refresh-logics
287,10421
(defun isabelle-logics-menu-refresh ()isabelle-logics-menu-refresh
291,10516
(defun isabelle-menu-bar-update-logics ()isabelle-menu-bar-update-logics
306,11149
(defun isabelle-load-isar-keywords (&optional kw)isabelle-load-isar-keywords
322,11778
(defun isabelle-create-span-menu (span idiom name)isabelle-create-span-menu
343,12506
(defun isabelle-xml-sml-escapes (xmlstring)isabelle-xml-sml-escapes
359,12937
(defun isabelle-process-pgip (xmlstring)isabelle-process-pgip
362,13038

isar/isar-autotest.el,50
(defvar isar-long-tests nilisar-long-tests
8,186

isar/isar.el,2692
(defcustom isar-keywords-name nilisar-keywords-name
39,915
(defpgdefault completion-table isar-keywords-major)completion-table
55,1426
(defcustom isar-web-pageisar-web-page
57,1479
(defun isar-strip-terminators ()isar-strip-terminators
71,1829
(defun isar-markup-ml (string)isar-markup-ml
83,2185
(defun isar-mode-config-set-variables ()isar-mode-config-set-variables
88,2320
(defun isar-shell-mode-config-set-variables ()isar-shell-mode-config-set-variables
153,5119
(defun isar-set-proof-find-theorems-command ()isar-set-proof-find-theorems-command
235,8305
(defpacustom use-find-theorems-form niluse-find-theorems-form
241,8489
(defun isar-set-undo-commands (&optional initp)isar-set-undo-commands
246,8655
(defpacustom use-linear-undo tuse-linear-undo
261,9288
(defun isar-configure-from-settings ()isar-configure-from-settings
266,9446
(defun isar-remove-file (name files cmp-base)isar-remove-file
274,9596
(defun isar-shell-compute-new-files-list ()isar-shell-compute-new-files-list
286,9900
(define-derived-mode isar-shell-mode proof-shell-modeisar-shell-mode
305,10470
(define-derived-mode isar-response-mode proof-response-modeisar-response-mode
310,10597
(define-derived-mode isar-goals-mode proof-goals-modeisar-goals-mode
315,10730
(define-derived-mode isar-mode proof-modeisar-mode
320,10856
(defpgdefault menu-entriesmenu-entries
372,12571
(defun isar-set-command ()isar-set-command
403,13765
(defpgdefault help-menu-entries isabelle-docs-menu)help-menu-entries
408,13895
(defun isar-count-undos (span)isar-count-undos
411,13971
(defun isar-find-and-forget (span)isar-find-and-forget
437,14937
(defun isar-goal-command-p (span)isar-goal-command-p
473,16280
(defun isar-global-save-command-p (span str)isar-global-save-command-p
478,16457
(defvar isar-current-goal 1isar-current-goal
499,17241
(defun isar-state-preserving-p (cmd)isar-state-preserving-p
502,17307
(defvar isar-shell-current-line-width nilisar-shell-current-line-width
527,18156
(defun isar-shell-adjust-line-width ()isar-shell-adjust-line-width
532,18348
(defsubst isar-string-wrapping (string)isar-string-wrapping
555,19113
(defsubst isar-positions-of (filename start end)isar-positions-of
564,19307
(defcustom isar-wrap-commands-singly tisar-wrap-commands-singly
570,19512
(defun isar-command-wrapping (filename start end string)isar-command-wrapping
576,19708
(defun isar-preprocessing ()isar-preprocessing
584,20022
(defun isar-mode-config ()isar-mode-config
602,20573
(defun isar-shell-mode-config ()isar-shell-mode-config
616,21226
(defun isar-response-mode-config ()isar-response-mode-config
626,21575
(defun isar-goals-mode-config ()isar-goals-mode-config
636,21910

isar/isar-find-theorems.el,1360
(defvar isar-find-theorems-data (listisar-find-theorems-data
19,565
(defun isar-find-theorems-minibuffer ()isar-find-theorems-minibuffer
35,1039
(defun isar-find-theorems-form ()isar-find-theorems-form
49,1658
(defvar isar-find-theorems-widget-number nilisar-find-theorems-widget-number
92,3532
(defvar isar-find-theorems-widget-pattern nilisar-find-theorems-widget-pattern
95,3630
(defvar isar-find-theorems-widget-intro nilisar-find-theorems-widget-intro
98,3722
(defvar isar-find-theorems-widget-elim nilisar-find-theorems-widget-elim
101,3808
(defvar isar-find-theorems-widget-dest nilisar-find-theorems-widget-dest
104,3892
(defvar isar-find-theorems-widget-name nilisar-find-theorems-widget-name
107,3976
(defvar isar-find-theorems-widget-simp nilisar-find-theorems-widget-simp
110,4063
(defun isar-find-theorems-create-searchformisar-find-theorems-create-searchform
115,4209
(defun isar-find-theorems-create-help ()isar-find-theorems-create-help
255,8752
(defun isar-find-theorems-submit-searchformisar-find-theorems-submit-searchform
298,10924
(defun isar-find-theorems-parse-criteria (option-string criteria-string)isar-find-theorems-parse-criteria
376,13294
(defun isar-find-theorems-parse-number (num)isar-find-theorems-parse-number
469,16275
(defun isar-find-theorems-filter-empty (strings)isar-find-theorems-filter-empty
479,16552

isar/isar-keywords.el,1662
(defconst isar-keywords-majorisar-keywords-major
7,222
(defconst isar-keywords-minorisar-keywords-minor
280,4856
(defconst isar-keywords-controlisar-keywords-control
339,5659
(defconst isar-keywords-diagisar-keywords-diag
360,6153
(defconst isar-keywords-theory-beginisar-keywords-theory-begin
434,7438
(defconst isar-keywords-theory-switchisar-keywords-theory-switch
437,7491
(defconst isar-keywords-theory-endisar-keywords-theory-end
440,7537
(defconst isar-keywords-theory-headingisar-keywords-theory-heading
443,7585
(defconst isar-keywords-theory-declisar-keywords-theory-decl
449,7692
(defconst isar-keywords-theory-scriptisar-keywords-theory-script
552,9481
(defconst isar-keywords-theory-goalisar-keywords-theory-goal
555,9544
(defconst isar-keywords-qedisar-keywords-qed
583,10059
(defconst isar-keywords-qed-blockisar-keywords-qed-block
590,10145
(defconst isar-keywords-qed-globalisar-keywords-qed-global
593,10192
(defconst isar-keywords-proof-headingisar-keywords-proof-heading
596,10241
(defconst isar-keywords-proof-goalisar-keywords-proof-goal
601,10324
(defconst isar-keywords-proof-blockisar-keywords-proof-block
606,10401
(defconst isar-keywords-proof-openisar-keywords-proof-open
610,10463
(defconst isar-keywords-proof-closeisar-keywords-proof-close
613,10509
(defconst isar-keywords-proof-chainisar-keywords-proof-chain
616,10556
(defconst isar-keywords-proof-declisar-keywords-proof-decl
623,10659
(defconst isar-keywords-proof-asmisar-keywords-proof-asm
635,10821
(defconst isar-keywords-proof-asm-goalisar-keywords-proof-asm-goal
642,10916
(defconst isar-keywords-proof-scriptisar-keywords-proof-script
648,11005

isar/isar-mmm.el,127
(defconst isar-start-latex-regexpisar-start-latex-regexp
24,744
(defconst isar-start-sml-regexpisar-start-sml-regexp
36,1172

isar/isar-profiling.el,0

isar/isar-syntax.el,6862
(defconst isar-script-syntax-table-entriesisar-script-syntax-table-entries
18,489
(defconst isar-script-syntax-table-alistisar-script-syntax-table-alist
42,891
(defun isar-init-syntax-table ()isar-init-syntax-table
51,1174
(defun isar-init-output-syntax-table ()isar-init-output-syntax-table
59,1421
(defconst isar-keyword-begin "begin")isar-keyword-begin
74,1863
(defconst isar-keyword-end "end")isar-keyword-end
75,1901
(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose
77,1936
(defconst isar-keywords-theoryisar-keywords-theory
82,2074
(defconst isar-keywords-saveisar-keywords-save
87,2205
(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose
92,2320
(defconst isar-keywords-proofisar-keywords-proof
98,2481
(defconst isar-keywords-proof-contextisar-keywords-proof-context
105,2658
(defconst isar-keywords-local-goalisar-keywords-local-goal
109,2765
(defconst isar-keywords-properisar-keywords-proper
113,2870
(defconst isar-keywords-improperisar-keywords-improper
118,2989
(defconst isar-keyword-level-alistisar-keyword-level-alist
123,3121
(defconst isar-keywords-outline isar-keywords-outline
138,3592
(defconst isar-keywords-indent-openisar-keywords-indent-open
141,3668
(defconst isar-keywords-indent-closeisar-keywords-indent-close
148,3854
(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose
153,3987
(defconst isar-ext-first "\\(?:\\\\<\\^?[A-Za-z]+>\\|[A-Za-z]\\)")isar-ext-first
163,4216
(defconst isar-ext-rest "\\(?:\\\\<\\^?[A-Za-z]+>\\|[A-Za-z0-9'_]\\)")isar-ext-rest
164,4283
(defconst isar-long-id-stuff (concat "\\(?:" isar-ext-rest "\\|\\.\\)+"))isar-long-id-stuff
166,4355
(defconst isar-id (concat "\\(" isar-ext-first isar-ext-rest "*\\)"))isar-id
167,4429
(defconst isar-idx (concat isar-id "\\(?:\\.[0-9]+\\)?"))isar-idx
168,4499
(defconst isar-string "\"\\(\\(?:[^\"]\\|\\\\\"\\)*\\)\"")isar-string
170,4558
(defun isar-ids-to-regexp (ids)isar-ids-to-regexp
172,4618
(defconst isar-any-command-regexpisar-any-command-regexp
204,6410
(defconst isar-name-regexpisar-name-regexp
211,6783
(defconst isar-improper-regexpisar-improper-regexp
217,7078
(defconst isar-save-command-regexpisar-save-command-regexp
221,7226
(defconst isar-global-save-command-regexpisar-global-save-command-regexp
224,7327
(defconst isar-goal-command-regexpisar-goal-command-regexp
227,7441
(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp
230,7549
(defconst isar-comment-start "(*")isar-comment-start
233,7662
(defconst isar-comment-end "*)")isar-comment-end
234,7697
(defconst isar-comment-start-regexp (regexp-quote isar-comment-start))isar-comment-start-regexp
235,7730
(defconst isar-comment-end-regexp (regexp-quote isar-comment-end))isar-comment-end-regexp
236,7801
(defconst isar-string-start-regexp "\"\\|`\\|{\\*")isar-string-start-regexp
238,7869
(defconst isar-string-end-regexp "\"\\|`\\|\\*}")isar-string-end-regexp
239,7921
(defun isar-syntactic-context ()isar-syntactic-context
241,7972
(defconst isar-antiq-regexpisar-antiq-regexp
256,8367
(defconst isar-nesting-regexpisar-nesting-regexp
262,8518
(defun isar-nesting ()isar-nesting
265,8616
(defun isar-match-nesting (limit)isar-match-nesting
277,9009
(defface isabelle-string-face isabelle-string-face
289,9343
(defface isabelle-quote-face isabelle-quote-face
297,9543
(defface isabelle-class-name-faceisabelle-class-name-face
305,9739
(defface isabelle-tfree-name-faceisabelle-tfree-name-face
313,9926
(defface isabelle-tvar-name-faceisabelle-tvar-name-face
321,10119
(defface isabelle-free-name-faceisabelle-free-name-face
329,10311
(defface isabelle-bound-name-faceisabelle-bound-name-face
337,10499
(defface isabelle-var-name-faceisabelle-var-name-face
345,10690
(defconst isabelle-string-face 'isabelle-string-face)isabelle-string-face
353,10881
(defconst isabelle-quote-face  'isabelle-quote-face)isabelle-quote-face
354,10935
(defconst isabelle-class-name-face 'isabelle-class-name-face)isabelle-class-name-face
355,10988
(defconst isabelle-tfree-name-face 'isabelle-tfree-name-face)isabelle-tfree-name-face
356,11050
(defconst isabelle-tvar-name-face  'isabelle-tvar-name-face)isabelle-tvar-name-face
357,11112
(defconst isabelle-free-name-face  'isabelle-free-name-face)isabelle-free-name-face
358,11173
(defconst isabelle-bound-name-face 'isabelle-bound-name-face)isabelle-bound-name-face
359,11234
(defconst isabelle-var-name-face   'isabelle-var-name-face)isabelle-var-name-face
360,11296
(defun isar-font-lock-fontify-syntactically-region isar-font-lock-fontify-syntactically-region
366,11445
(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1
401,12721
(defun isar-output-flkprops (start regexp end props)isar-output-flkprops
419,13729
(defun isar-output-flk (start regexp end face)isar-output-flk
425,13981
(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1
428,14090
(defun isar-strip-output-markup (string)isar-strip-output-markup
464,15513
(defconst isar-shell-font-lock-keywordsisar-shell-font-lock-keywords
468,15649
(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords
471,15733
(defconst isar-linear-undo "linear_undo")isar-linear-undo
505,16412
(defconst isar-undo "ProofGeneral.undo;")isar-undo
507,16455
(defconst isar-prisar-pr
509,16498
(defun isar-remove (name)isar-remove
516,16656
(defun isar-undos (linearp i)isar-undos
519,16731
(defun isar-cannot-undo (cmd)isar-cannot-undo
529,16965
(defconst isar-undo-commandsisar-undo-commands
532,17035
(defconst isar-theory-start-regexpisar-theory-start-regexp
540,17172
(defconst isar-end-regexpisar-end-regexp
546,17330
(defconst isar-undo-fail-regexpisar-undo-fail-regexp
550,17431
(defconst isar-undo-skip-regexpisar-undo-skip-regexp
554,17535
(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp
557,17656
(defconst isar-undo-remove-regexpisar-undo-remove-regexp
560,17721
(defconst isar-keywords-imenuisar-keywords-imenu
568,17878
(defconst isar-entity-regexp isar-entity-regexp
575,18069
(defconst isar-named-entity-regexpisar-named-entity-regexp
578,18165
(defconst isar-named-entity-name-match-numberisar-named-entity-name-match-number
583,18295
(defconst isar-generic-expressionisar-generic-expression
586,18396
(defconst isar-indent-any-regexpisar-indent-any-regexp
597,18630
(defconst isar-indent-inner-regexpisar-indent-inner-regexp
599,18723
(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp
601,18789
(defconst isar-indent-open-regexpisar-indent-open-regexp
603,18905
(defconst isar-indent-close-regexpisar-indent-close-regexp
605,19015
(defconst isar-outline-regexpisar-outline-regexp
611,19152
(defconst isar-outline-heading-end-regexp "\n")isar-outline-heading-end-regexp
615,19305
(defconst isar-outline-heading-alist isar-keyword-level-alist)isar-outline-heading-alist
617,19354

isar/isar-unicode-tokens.el,2310
(defgroup isabelle-tokens nilisabelle-tokens
25,672
(defun isar-set-and-restart-tokens (sym val)isar-set-and-restart-tokens
30,812
(defconst isar-control-region-format-regexpisar-control-region-format-regexp
43,1165
(defconst isar-control-char-format-regexpisar-control-char-format-regexp
46,1259
(defconst isar-control-char-format	   "\\<^%s>")isar-control-char-format
52,1406
(defconst isar-control-region-format-start "\\<^%s>")isar-control-region-format-start
53,1455
(defconst isar-control-region-format-end   "\\<^%s>")isar-control-region-format-end
54,1509
(defcustom isar-control-charactersisar-control-characters
57,1565
(defcustom isar-control-regionsisar-control-regions
71,1978
(defconst isar-token-format "\\<%s>")isar-token-format
97,2790
(defconst isar-token-variant-format-regexpisar-token-variant-format-regexp
101,2941
(defcustom isar-greek-letters-tokensisar-greek-letters-tokens
104,3055
(defcustom isar-misc-letters-tokensisar-misc-letters-tokens
144,3913
(defcustom isar-symbols-tokensisar-symbols-tokens
156,4231
(defcustom isar-extended-symbols-tokensisar-extended-symbols-tokens
362,9042
(defun isar-try-char (charset code1 code2)isar-try-char
431,10697
(defcustom isar-symbols-tokens-fallbacksisar-symbols-tokens-fallbacks
435,10841
(defcustom isar-bold-nums-tokensisar-bold-nums-tokens
462,11771
(defun isar-map-letters (f1 f2 &rest symbs)isar-map-letters
478,12160
(defconst isar-script-letters-tokens ; \<A> \<B> ...isar-script-letters-tokens
484,12308
(defconst isar-roman-letters-tokens ; \<a> \<b> ...isar-roman-letters-tokens
489,12462
(defconst isar-fraktur-uppercase-letters-tokens ; \<AA> \<BB> ..isar-fraktur-uppercase-letters-tokens
494,12636
(defconst isar-fraktur-lowercase-letters-tokens ; \<AA> \<BB> ..isar-fraktur-lowercase-letters-tokens
499,12805
(defcustom isar-token-symbol-map nilisar-token-symbol-map
504,12996
(defcustom isar-user-tokens nilisar-user-tokens
521,13537
(defun isar-init-token-symbol-map ()isar-init-token-symbol-map
535,13977
(defcustom isar-symbol-shortcutsisar-symbol-shortcuts
560,14626
(defcustom isar-shortcut-alist nilisar-shortcut-alist
632,16825
(defun isar-init-shortcut-alists ()isar-init-shortcut-alists
640,17084
(defconst isar-tokens-customizable-variablesisar-tokens-customizable-variables
661,17747

lego/lego.el,2849
(defcustom lego-tags "/usr/lib/lego/lib_Type/"lego-tags
21,534
(defcustom lego-test-all-name "test_all"lego-test-all-name
26,670
(defpgdefault help-menu-entrieshelp-menu-entries
32,828
(defpgdefault menu-entriesmenu-entries
36,988
(defvar lego-shell-handle-outputlego-shell-handle-output
47,1289
(defconst lego-process-configlego-process-config
55,1587
(defconst lego-pretty-set-width "Configure PrettyWidth %s; "lego-pretty-set-width
66,2018
(defconst lego-interrupt-regexp "Interrupt.."lego-interrupt-regexp
70,2160
(defcustom lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/"lego-www-home-page
75,2277
(defcustom lego-www-latest-releaselego-www-latest-release
80,2401
(defcustom lego-www-refcardlego-www-refcard
86,2576
(defcustom lego-library-www-pagelego-library-www-page
92,2725
(defvar lego-prog-name "lego"lego-prog-name
101,2941
(defvar lego-shell-cd "Cd \"%s\";"lego-shell-cd
104,3010
(defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*"lego-shell-proof-completed-regexp
107,3109
(defvar lego-save-command-regexplego-save-command-regexp
110,3249
(defvar lego-goal-command-regexplego-goal-command-regexp
112,3339
(defvar lego-kill-goal-command "KillRef;")lego-kill-goal-command
115,3430
(defvar lego-forget-id-command "Forget %s;")lego-forget-id-command
116,3473
(defvar lego-undoable-commands-regexplego-undoable-commands-regexp
118,3519
(defvar lego-goal-regexp "\\?\\([0-9]+\\)")lego-goal-regexp
127,3893
(defvar lego-outline-regexplego-outline-regexp
129,3938
(defvar lego-outline-heading-end-regexp ";\\|\\*)")lego-outline-heading-end-regexp
135,4113
(defvar lego-shell-outline-regexp lego-goal-regexp)lego-shell-outline-regexp
137,4166
(defvar lego-shell-outline-heading-end-regexp lego-goal-regexp)lego-shell-outline-heading-end-regexp
138,4218
(define-derived-mode lego-shell-mode proof-shell-modelego-shell-mode
144,4497
(define-derived-mode lego-mode proof-modelego-mode
151,4658
(define-derived-mode lego-goals-mode proof-goals-modelego-goals-mode
162,4968
(defun lego-count-undos (span)lego-count-undos
173,5394
(defun lego-goal-command-p (span)lego-goal-command-p
192,6131
(defun lego-find-and-forget (span)lego-find-and-forget
197,6302
(defun lego-goal-hyp ()lego-goal-hyp
239,8138
(defun lego-state-preserving-p (cmd)lego-state-preserving-p
248,8335
(defvar lego-shell-current-line-width nillego-shell-current-line-width
264,9038
(defun lego-shell-adjust-line-width ()lego-shell-adjust-line-width
272,9345
(defun lego-mode-config ()lego-mode-config
289,10046
(defun lego-equal-module-filename (module filename)lego-equal-module-filename
357,12097
(defun lego-shell-compute-new-files-list ()lego-shell-compute-new-files-list
363,12372
(defun lego-shell-mode-config ()lego-shell-mode-config
373,12755
(defun lego-goals-mode-config ()lego-goals-mode-config
420,14422

lego/lego-syntax.el,1148
(defconst lego-keywords-goal '("$?Goal"))lego-keywords-goal
15,358
(defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen"))lego-keywords-save
17,401
(defconst lego-commandslego-commands
19,472
(defconst lego-keywordslego-keywords
31,1030
(defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For"))lego-tacticals
36,1207
(defconst lego-error-regexp "^\\(cannot assume\\|Error\\|Lego parser\\)"lego-error-regexp
39,1315
(defvar lego-id proof-id)lego-id
42,1473
(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*")lego-ids
44,1500
(defconst lego-arg-list-regexp "\\s *\\(\\[[^]]+\\]\\s *\\)*"lego-arg-list-regexp
48,1696
(defun lego-decl-defn-regexp (char)lego-decl-defn-regexp
51,1812
(defconst lego-definiendum-alternative-regexplego-definiendum-alternative-regexp
59,2184
(defvar lego-font-lock-termslego-font-lock-terms
63,2368
(defconst lego-goal-with-hole-regexplego-goal-with-hole-regexp
89,3221
(defconst lego-save-with-hole-regexplego-save-with-hole-regexp
94,3443
(defvar lego-font-lock-keywords-1lego-font-lock-keywords-1
99,3660
(defun lego-init-syntax-table ()lego-init-syntax-table
110,4122

pgshell/pgshell.el,0

phox/phox.el,849
(defcustom phox-prog-name "phox -pg"phox-prog-name
32,916
(defcustom phox-web-pagephox-web-page
37,1018
(defcustom phox-doc-dirphox-doc-dir
43,1168
(defcustom phox-lib-dirphox-lib-dir
49,1315
(defcustom phox-tags-programphox-tags-program
55,1458
(defcustom phox-tags-docphox-tags-doc
61,1637
(defcustom phox-etagsphox-etags
67,1774
(defpgdefault menu-entriesmenu-entries
88,2224
(defun phox-config ()phox-config
102,2417
(defun phox-shell-config ()phox-shell-config
146,4343
(define-derived-mode phox-mode proof-modephox-mode
170,5205
(define-derived-mode phox-shell-mode proof-shell-modephox-shell-mode
186,5668
(define-derived-mode phox-response-mode proof-response-modephox-response-mode
191,5796
(define-derived-mode phox-goals-mode proof-goals-modephox-goals-mode
201,6157
(defpgdefault completion-tablecompletion-table
224,6943

phox/phox-extraction.el,672
(defvar phox-prog-orig "phox -pg" "original name of phox binary.")phox-prog-orig
19,619
(defun phox-prog-flags-modify(option)phox-prog-flags-modify
21,687
(defun phox-prog-flags-extract()phox-prog-flags-extract
50,1488
(defun phox-prog-flags-erase()phox-prog-flags-erase
61,1778
(defun phox-toggle-extraction()phox-toggle-extraction
69,1974
(defun phox-compile-theorem(name)phox-compile-theorem
81,2376
(defun phox-compile-theorem-on-cursor()phox-compile-theorem-on-cursor
87,2601
(defun phox-output ()phox-output
103,3079
(defun phox-output-theorem (name)phox-output-theorem
113,3291
(defun phox-output-theorem-on-cursor()phox-output-theorem-on-cursor
120,3590

phox/phox-font.el,458
(defvar phox-sym-lock-enabled nil)  ; da: for clean compilephox-sym-lock-enabled
1,0
(defvar phox-sym-lock-color nil)  ; da: for clean compilephox-sym-lock-color
2,60
(defvar phox-sym-lock-keywords nil)  ; da: for clean compilephox-sym-lock-keywords
3,118
(defconst phox-font-lock-keywordsphox-font-lock-keywords
11,511
(defconst phox-sym-lock-keywords-tablephox-sym-lock-keywords-table
70,2628
(defun phox-sym-lock-start ()phox-sym-lock-start
93,3202

phox/phox-fun.el,3113
(defconst phox-forget-id-command "del %s.\n")phox-forget-id-command
11,186
(defconst phox-forget-proof-command "del_proof %s.\n")phox-forget-proof-command
12,232
(defconst phox-forget-new-elim-command "edel elim %s.\n")phox-forget-new-elim-command
13,287
(defconst phox-forget-new-intro-command "edel intro %s.\n")phox-forget-new-intro-command
14,345
(defconst phox-forget-new-equation-command "edel equation %s.\n")phox-forget-new-equation-command
15,405
(defconst phox-forget-close-def-command "edel closed %s.\n")phox-forget-close-def-command
16,471
(defconst phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*")phox-comments-regexp
18,597
(defconst phox-strict-comments-regexp "\\([ \n\t\r]+\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*\\|\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)+\\)")phox-strict-comments-regexp
20,776
(defconst phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)")phox-ident-regexp
21,941
(defconst phox-inductive-option "\\(\\[[^]]*]\\)?")phox-inductive-option
22,1027
(defconst phox-spaces-regexp "[ \n\t\r]*")phox-spaces-regexp
23,1079
(defconst phox-sy-definition-regexp (concatphox-sy-definition-regexp
24,1122
(defconst phox-sy-inductive-regexp (concatphox-sy-inductive-regexp
28,1309
(defconst phox-inductive-regexp (concatphox-inductive-regexp
34,1522
(defconst phox-data-regexp (concatphox-data-regexp
40,1673
(defconst phox-definition-regexp (concatphox-definition-regexp
46,1827
(defconst phox-prove-claim-regexp (concatphox-prove-claim-regexp
50,1971
(defconst phox-new-elim-regexp (concatphox-new-elim-regexp
54,2077
(defconst phox-new-intro-regexp (concatphox-new-intro-regexp
57,2196
(defconst phox-new-rewrite-regexp (concatphox-new-rewrite-regexp
60,2317
(defconst phox-new-equation-regexp (concatphox-new-equation-regexp
63,2442
(defconst phox-close-def-regexp (concatphox-close-def-regexp
66,2569
(defun phox-init-syntax-table (&optional TABLE)phox-init-syntax-table
71,2706
(defvar phox-top-keywordsphox-top-keywords
87,3178
(defvar phox-proof-keywordsphox-proof-keywords
135,3633
(defun phox-find-and-forget (span)phox-find-and-forget
176,3983
(defalias 'phox-assert-next-command-interactive 'proof-assert-next-command-interactive)phox-assert-next-command-interactive
255,6399
(defun phox-depend-theorem(theorem)phox-depend-theorem
274,7365
(defun phox-eshow-extlist(extlist)phox-eshow-extlist
283,7654
(defun phox-flag-name(name)phox-flag-name
297,8251
(defun phox-path()phox-path
308,8553
(defun phox-print-expression(expr)phox-print-expression
319,8789
(defun phox-print-sort-expression(expr)phox-print-sort-expression
332,9245
(defun phox-priority-symbols-list(symblist)phox-priority-symbols-list
343,9557
(defun phox-search-string(string type)phox-search-string
355,9929
(defun phox-constraints()phox-constraints
370,10454
(defun phox-goals()phox-goals
381,10710
(defvar phox-state-menuphox-state-menu
393,10919
(defun phox-delete-symbol(symbol)phox-delete-symbol
418,11909
(defun phox-delete-symbol-on-cursor()phox-delete-symbol-on-cursor
424,12117

phox/phox-lang.el,517
(defvar phox-langphox-lang
9,306
(defun phox-lang-absurd ()phox-lang-absurd
17,535
(defun phox-lang-suppress (s)phox-lang-suppress
22,629
(defun phox-lang-opendef ()phox-lang-opendef
27,826
(defun phox-lang-instance (s)phox-lang-instance
32,944
(defun phox-lang-open-instance (s)phox-lang-open-instance
37,1073
(defun phox-lang-lock (s)phox-lang-lock
42,1222
(defun phox-lang-unlock (s)phox-lang-unlock
47,1352
(defun phox-lang-prove (s)phox-lang-prove
52,1488
(defun phox-lang-let (s)phox-lang-let
57,1622

phox/phox-outline.el,506
(defconst phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)")phox-outline-title-regexp
20,745
(defconst phox-outline-section-regexp "\\((\\*\\*+\\)")phox-outline-section-regexp
21,810
(defconst phox-outline-save-regexp "\\((\\*#\\)")phox-outline-save-regexp
22,866
(defconst phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)")phox-outline-heading-end-regexp
39,1409
(defun phox-outline-level()phox-outline-level
45,1584
(defun phox-setup-outline ()phox-setup-outline
59,2058

phox/phox-pbrpm.el,847
(defun phox-pbrpm-left-paren-p (char)phox-pbrpm-left-paren-p
39,1671
(defun phox-pbrpm-right-paren-p (char)phox-pbrpm-right-paren-p
46,1874
(defun phox-pbrpm-menu-from-string (order str)phox-pbrpm-menu-from-string
54,2078
(defun phox-pbrpm-rename-in-cmd (cmd spans)phox-pbrpm-rename-in-cmd
63,2410
(defun phox-pbrpm-get-region-name (region-info)phox-pbrpm-get-region-name
96,3658
(defun  phox-pbrpm-escape-string (str)phox-pbrpm-escape-string
99,3785
(defun phox-pbrpm-generate-menu (click-infos region-infos)phox-pbrpm-generate-menu
103,3920
(defalias 'proof-pbrpm-generate-menu 'phox-pbrpm-generate-menu)proof-pbrpm-generate-menu
310,11400
(defalias 'proof-pbrpm-left-paren-p 'phox-pbrpm-left-paren-p)proof-pbrpm-left-paren-p
311,11464
(defalias 'proof-pbrpm-right-paren-p 'phox-pbrpm-right-paren-p)proof-pbrpm-right-paren-p
312,11526

phox/phox-sym-lock.el,2530
(defcustom phox-sym-lock-enabled tphox-sym-lock-enabled
19,871
(defvar phox-sym-lock-sym-count 0phox-sym-lock-sym-count
59,2452
(defvar phox-sym-lock-ext-start nil "Temporary for atomicization.")phox-sym-lock-ext-start
62,2522
(defvar phox-sym-lock-ext-end nil "Temporary for atomicization.")phox-sym-lock-ext-end
64,2644
(defvar phox-sym-lock-font-size nilphox-sym-lock-font-size
67,2763
(defvar phox-sym-lock-keywords nilphox-sym-lock-keywords
72,2953
(defvar phox-sym-lock-enabled nilphox-sym-lock-enabled
77,3129
(defvar phox-sym-lock-color (face-foreground 'default)phox-sym-lock-color
82,3291
(defvar phox-sym-lock-mouse-face 'defaultphox-sym-lock-mouse-face
87,3509
(defvar phox-sym-lock-mouse-face-enabled tphox-sym-lock-mouse-face-enabled
92,3699
(defconst phox-sym-lock-with-mule (featurep 'mule)phox-sym-lock-with-mule
97,3889
(defun phox-sym-lock-gen-symbol (&optional prefix)phox-sym-lock-gen-symbol
100,3973
(defun phox-sym-lock-make-symbols-atomic (&optional begin end)phox-sym-lock-make-symbols-atomic
108,4275
(defun phox-sym-lock-compute-font-size ()phox-sym-lock-compute-font-size
135,5216
(defvar phox-sym-lock-font-namephox-sym-lock-font-name
173,6635
(defun phox-sym-lock-set-foreground ()phox-sym-lock-set-foreground
216,8233
(defun phox-sym-lock-translate-char (char)phox-sym-lock-translate-char
230,8842
(defun phox-sym-lock-translate-char-or-string (obj)phox-sym-lock-translate-char-or-string
239,9159
(defun phox-sym-lock-remap-face (pat pos obj atomic)phox-sym-lock-remap-face
246,9387
(defvar phox-sym-lock-clear-facephox-sym-lock-clear-face
266,10375
(defun phox-sym-lock (fl)phox-sym-lock
278,10794
(defun phox-sym-lock-rec (fl)phox-sym-lock-rec
287,11198
(defun phox-sym-lock-atom-face (pat num pos obj &optional override)phox-sym-lock-atom-face
293,11343
(defun phox-sym-lock-pre-idle-hook-first ()phox-sym-lock-pre-idle-hook-first
298,11639
(defun phox-sym-lock-pre-idle-hook-last ()phox-sym-lock-pre-idle-hook-last
308,12044
(defun phox-sym-lock-enable ()phox-sym-lock-enable
317,12419
(defun phox-sym-lock-disable ()phox-sym-lock-disable
330,12830
(defun phox-sym-lock-mouse-face-enable ()phox-sym-lock-mouse-face-enable
343,13246
(defun phox-sym-lock-mouse-face-disable ()phox-sym-lock-mouse-face-disable
350,13461
(defun phox-sym-lock-font-lock-hook ()phox-sym-lock-font-lock-hook
357,13680
(defun font-lock-set-defaults (&optional explicit-defaults)font-lock-set-defaults
372,14371
(defun phox-sym-lock-patch-keywords ()phox-sym-lock-patch-keywords
384,14798

phox/phox-tags.el,495
(defun phox-tags-add-table(table)phox-tags-add-table
26,869
(defun phox-tags-reset-table()phox-tags-reset-table
35,1264
(defun phox-tags-add-doc-table()phox-tags-add-doc-table
40,1374
(defun phox-tags-add-lib-table()phox-tags-add-lib-table
46,1523
(defun phox-tags-add-local-table()phox-tags-add-local-table
52,1658
(defun phox-tags-create-local-table()phox-tags-create-local-table
58,1841
(defun phox-complete-tag()phox-complete-tag
69,2091
(defvar phox-tags-menuphox-tags-menu
76,2200

generic/pg-assoc.el,135
(defun proof-associated-buffers ()proof-associated-buffers
33,973
(defun proof-associated-windows ()proof-associated-windows
43,1183

generic/pg-autotest.el,1629
(defvar pg-autotest-success tpg-autotest-success
29,690
(defvar pg-autotest-log tpg-autotest-log
32,777
(defun pg-autotest-find-file (file)pg-autotest-find-file
37,871
(defun pg-autotest-find-file-restart (file)pg-autotest-find-file-restart
44,1137
(defmacro pg-autotest-apply (fn &rest args)pg-autotest-apply
58,1611
(defmacro pg-autotest (fn &rest args)pg-autotest
72,2026
(defun pg-autotest-log (file)pg-autotest-log
89,2463
(defun pg-autotest-message (msg &rest args)pg-autotest-message
98,2726
(defun pg-autotest-remark (msg)pg-autotest-remark
107,3015
(defun pg-autotest-timestart (&optional clockname)pg-autotest-timestart
110,3096
(defun pg-autotest-timetaken (&optional clockname)pg-autotest-timetaken
115,3279
(defun pg-autotest-start (&optional debug)pg-autotest-start
129,3667
(defun pg-autotest-exit ()pg-autotest-exit
140,4121
(defun pg-autotest-test-process-wholefile (file)pg-autotest-test-process-wholefile
160,4904
(defun pg-autotest-test-script-wholefile (file)pg-autotest-test-script-wholefile
168,5191
(defun pg-autotest-test-script-randomjumps (file jumps)pg-autotest-test-script-randomjumps
193,6123
(defun pg-autotest-test-retract-file (file)pg-autotest-test-retract-file
242,7680
(defun pg-autotest-test-assert-processed (file)pg-autotest-test-assert-processed
248,7821
(defun pg-autotest-test-assert-full ()pg-autotest-test-assert-full
254,8047
(defun pg-autotest-test-assert-unprocessed (file)pg-autotest-test-assert-unprocessed
261,8288
(defun pg-autotest-test-eval (body)pg-autotest-test-eval
268,8553
(defun pg-autotest-test-quit-prover ()pg-autotest-test-quit-prover
272,8652

generic/pg-custom.el,1058
(defpgcustom script-indent tscript-indent
37,1199
(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default
42,1336
(defpgcustom toolbar-entries proof-toolbar-entries-defaulttoolbar-entries
70,3069
(defpgcustom prog-args nilprog-args
89,3802
(defpgcustom prog-env nilprog-env
101,4378
(defpgcustom quit-timeout quit-timeout
110,4805
(defpgcustom favourites nilfavourites
122,5232
(defpgcustom menu-entries nilmenu-entries
127,5421
(defpgcustom help-menu-entries nilhelp-menu-entries
134,5657
(defpgcustom keymap (make-keymap (concat proof-assistant " keymap"))keymap
141,5920
(defpgcustom completion-table nilcompletion-table
146,6091
(defpgcustom tags-program niltags-program
157,6465
(defpgcustom use-holes (eq proof-assistant-symbol 'coq)use-holes
166,6849
(defpgcustom one-command-per-lineone-command-per-line
173,7107
(defpgcustom maths-menu-enable nilmaths-menu-enable
184,7343
(defpgcustom unicode-tokens-enable (eq proof-assistant-symbol 'isar)unicode-tokens-enable
190,7523
(defpgcustom mmm-enable nilmmm-enable
196,7730

generic/pg-goals.el,540
(define-derived-mode proof-goals-mode proof-universal-keys-only-modeproof-goals-mode
29,734
(define-key proof-goals-mode-map [q] 'bury-buffer)proof-goals-mode-map
56,1592
(define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)proof-goals-mode-map
58,1708
(define-key proof-goals-mode-map [C-M-mouse-3]proof-goals-mode-map
59,1776
(defun proof-goals-config-done ()proof-goals-config-done
68,1923
(defun pg-goals-display (string)pg-goals-display
76,2189
(defun pg-goals-button-action (event)pg-goals-button-action
117,3493

generic/pg-movie.el,642
(defconst pg-movie-xml-header "<?xml version=\"1.0\"?>")pg-movie-xml-header
33,944
(defconst pg-movie-stylesheetpg-movie-stylesheet
35,1002
(defun pg-movie-stylesheet-location ()pg-movie-stylesheet-location
38,1101
(defvar pg-movie-frame 0 "Frame counter for movie.")pg-movie-frame
42,1209
(defun pg-movie-of-span (span)pg-movie-of-span
44,1263
(defun pg-movie-of-region (start end)pg-movie-of-region
80,2383
(defun pg-movie-export (&optional force)pg-movie-export
87,2571
(defun pg-movie-export-from (script &optional force)pg-movie-export-from
109,3175
(defun pg-movie-export-directory (dir extn)pg-movie-export-directory
120,3496

generic/pg-pamacs.el,887
(defmacro deflocal (var value &optional docstring)deflocal
35,1132
(deflocal proof-buffer-type nilproof-buffer-type
42,1370
(defmacro proof-ass-sym (sym)proof-ass-sym
50,1506
(defmacro proof-ass-symv (sym)proof-ass-symv
56,1765
(defmacro proof-ass (sym)proof-ass
62,2023
(defun proof-defpgcustom-fn (sym args)proof-defpgcustom-fn
68,2275
(defun undefpgcustom (sym)undefpgcustom
89,3145
(defmacro defpgcustom (sym &rest args)defpgcustom
95,3369
(defun proof-defpgdefault-fn (sym value)proof-defpgdefault-fn
106,3780
(defmacro defpgdefault (sym value)defpgdefault
120,4238
(defmacro defpgfun (name arglist &rest args)defpgfun
131,4600
(defun proof-defpacustom-fn (name val args)proof-defpacustom-fn
145,4999
(defmacro defpacustom (name val &rest args)defpacustom
212,7307
(defmacro proof-eval-when-ready-for-assistant (&rest body)proof-eval-when-ready-for-assistant
233,8262

generic/pg-pbrpm.el,3173
(defvar pg-pbrpm-use-buffer-menu tpg-pbrpm-use-buffer-menu
45,1207
(defvar pg-pbrpm-start-goal-regexp nilpg-pbrpm-start-goal-regexp
48,1329
(defvar pg-pbrpm-start-goal-regexp-par-num nilpg-pbrpm-start-goal-regexp-par-num
52,1486
(defvar pg-pbrpm-end-goal-regexp nilpg-pbrpm-end-goal-regexp
55,1609
(defvar pg-pbrpm-start-hyp-regexp nilpg-pbrpm-start-hyp-regexp
59,1761
(defvar pg-pbrpm-start-hyp-regexp-par-num nilpg-pbrpm-start-hyp-regexp-par-num
63,1922
(defvar pg-pbrpm-start-concl-regexp nilpg-pbrpm-start-concl-regexp
67,2129
(defvar pg-pbrpm-auto-select-regexp nilpg-pbrpm-auto-select-regexp
71,2293
(defvar pg-pbrpm-buffer-menu nil)pg-pbrpm-buffer-menu
78,2454
(defvar pg-pbrpm-spans nil)pg-pbrpm-spans
79,2488
(defvar pg-pbrpm-goal-description nil)pg-pbrpm-goal-description
80,2516
(defvar pg-pbrpm-windows-dialog-bug nil)pg-pbrpm-windows-dialog-bug
81,2555
(defvar pbrpm-menu-desc nil)pbrpm-menu-desc
82,2596
(defun pg-pbrpm-erase-buffer-menu ()pg-pbrpm-erase-buffer-menu
84,2626
(defun pg-pbrpm-menu-change-hook (start end len)pg-pbrpm-menu-change-hook
90,2798
(defun pg-pbrpm-create-reset-buffer-menu ()pg-pbrpm-create-reset-buffer-menu
108,3373
(defun pg-pbrpm-analyse-goal-buffer ()pg-pbrpm-analyse-goal-buffer
127,4215
(defun pg-pbrpm-button-action (event)pg-pbrpm-button-action
187,6620
(defun pg-pbrpm-exists (f l0)pg-pbrpm-exists
194,6846
(defun pg-pbrpm-eliminate-id (acc l)pg-pbrpm-eliminate-id
198,6958
(defun pg-pbrpm-build-menu (event start end)pg-pbrpm-build-menu
206,7204
(defun pg-pbrpm-setup-span (start end)pg-pbrpm-setup-span
269,9524
(defun pg-pbrpm-run-command (args)pg-pbrpm-run-command
329,11823
(defun pg-pbrpm-get-pos-info (pos)pg-pbrpm-get-pos-info
362,13348
(defun pg-pbrpm-get-region-info (start end)pg-pbrpm-get-region-info
404,14647
(defun pg-pbrpm-auto-select-around-point ()pg-pbrpm-auto-select-around-point
415,15059
(defun pg-pbrpm-translate-position (buffer pos)pg-pbrpm-translate-position
430,15583
(defun pg-pbrpm-process-click (event start end)pg-pbrpm-process-click
438,15837
(defvar pg-pbrpm-remember-region-selected-region nil)pg-pbrpm-remember-region-selected-region
458,16862
(defvar pg-pbrpm-regions-list nil)pg-pbrpm-regions-list
459,16916
(defun pg-pbrpm-erase-regions-list ()pg-pbrpm-erase-regions-list
461,16952
(defun pg-pbrpm-filter-regions-list ()pg-pbrpm-filter-regions-list
470,17260
(defface pg-pbrpm-multiple-selection-facepg-pbrpm-multiple-selection-face
477,17523
(defface pg-pbrpm-menu-input-facepg-pbrpm-menu-input-face
485,17725
(defun pg-pbrpm-do-remember-region (start end)pg-pbrpm-do-remember-region
493,17915
(defun pg-pbrpm-remember-region-drag-up-hook (event click-count)pg-pbrpm-remember-region-drag-up-hook
514,18763
(defun pg-pbrpm-remember-region-click-hook (event click-count)pg-pbrpm-remember-region-click-hook
518,18934
(defun pg-pbrpm-remember-region (event &optional delete)pg-pbrpm-remember-region
523,19119
(defun pg-pbrpm-process-region (span)pg-pbrpm-process-region
537,19833
(defun pg-pbrpm-process-regions-list ()pg-pbrpm-process-regions-list
555,20562
(defun pg-pbrpm-region-expression (buffer start end)pg-pbrpm-region-expression
559,20745

generic/pg-pgip.el,5070
(defalias 'pg-pgip-debug   'proof-debug)pg-pgip-debug
38,1032
(defalias 'pg-pgip-error   'error)pg-pgip-error
39,1073
(defalias 'pg-pgip-warning 'pg-internal-warning)pg-pgip-warning
40,1108
(defconst pg-pgip-version-supported "2.0"pg-pgip-version-supported
42,1158
(defun pg-pgip-process-packet (pgips)pg-pgip-process-packet
46,1264
(defvar pg-pgip-last-seen-id nil)pg-pgip-last-seen-id
56,1832
(defvar pg-pgip-last-seen-seq nil)pg-pgip-last-seen-seq
57,1866
(defun pg-pgip-process-pgip (pgip)pg-pgip-process-pgip
59,1902
(defun pg-pgip-process-msg (pgipmsg)pg-pgip-process-msg
78,2842
(defvar pg-pgip-post-process-functionspg-pgip-post-process-functions
93,3433
(defun pg-pgip-post-process (cmdname)pg-pgip-post-process
103,3908
(defun pg-pgip-process-askpgip (node)pg-pgip-process-askpgip
120,4523
(defun pg-pgip-process-usespgip (node)pg-pgip-process-usespgip
126,4727
(defun pg-pgip-process-usespgml (node)pg-pgip-process-usespgml
130,4891
(defun pg-pgip-process-pgmlconfig (node)pg-pgip-process-pgmlconfig
134,5055
(defun pg-pgip-process-proverinfo (node)pg-pgip-process-proverinfo
150,5672
(defun pg-pgip-process-hasprefs (node)pg-pgip-process-hasprefs
167,6337
(defun pg-pgip-haspref (name type prefcat descr default)pg-pgip-haspref
181,6969
(defun pg-pgip-process-prefval (node)pg-pgip-process-prefval
198,7671
(defun pg-pgip-process-guiconfig (node)pg-pgip-process-guiconfig
225,8379
(defvar proof-assistant-idtables nilproof-assistant-idtables
232,8496
(defun pg-pgip-process-ids (node)pg-pgip-process-ids
235,8613
(defun pg-complete-idtable-symbol ()pg-complete-idtable-symbol
261,9685
(defalias 'pg-pgip-process-setids 'pg-pgip-process-ids)pg-pgip-process-setids
266,9777
(defalias 'pg-pgip-process-addids 'pg-pgip-process-ids)pg-pgip-process-addids
267,9833
(defalias 'pg-pgip-process-delids 'pg-pgip-process-ids)pg-pgip-process-delids
268,9889
(defun pg-pgip-process-idvalue (node)pg-pgip-process-idvalue
271,9947
(defun pg-pgip-process-menuadd (node)pg-pgip-process-menuadd
283,10293
(defun pg-pgip-process-menudel (node)pg-pgip-process-menudel
286,10336
(defun pg-pgip-process-ready (node)pg-pgip-process-ready
295,10568
(defun pg-pgip-process-cleardisplay (node)pg-pgip-process-cleardisplay
298,10609
(defun pg-pgip-process-proofstate (node)pg-pgip-process-proofstate
312,11066
(defun pg-pgip-process-normalresponse (node)pg-pgip-process-normalresponse
316,11143
(defun pg-pgip-process-errorresponse (node)pg-pgip-process-errorresponse
320,11273
(defun pg-pgip-process-scriptinsert (node)pg-pgip-process-scriptinsert
324,11402
(defun pg-pgip-process-metainforesponse (node)pg-pgip-process-metainforesponse
329,11536
(defun pg-pgip-file-of-url (urlstr)pg-pgip-file-of-url
338,11776
(defun pg-pgip-process-informfileloaded (node)pg-pgip-process-informfileloaded
343,11911
(defun pg-pgip-process-informfileretracted (node)pg-pgip-process-informfileretracted
349,12143
(defun pg-pgip-process-brokerstatus (node)pg-pgip-process-brokerstatus
362,12590
(defun pg-pgip-process-proveravailmsg (node)pg-pgip-process-proveravailmsg
365,12638
(defun pg-pgip-process-newprovermsg (node)pg-pgip-process-newprovermsg
368,12688
(defun pg-pgip-process-proverstatusmsg (node)pg-pgip-process-proverstatusmsg
371,12736
(defvar pg-pgip-srcids nilpg-pgip-srcids
380,12982
(defun pg-pgip-process-newfile (node)pg-pgip-process-newfile
384,13089
(defun pg-pgip-process-filestatus (node)pg-pgip-process-filestatus
400,13671
(defun pg-pgip-process-newobj (node)pg-pgip-process-newobj
420,14325
(defun pg-pgip-process-delobj (node)pg-pgip-process-delobj
423,14367
(defun pg-pgip-process-objectstatus (node)pg-pgip-process-objectstatus
426,14409
(defun pg-pgip-process-parsescript (node)pg-pgip-process-parsescript
440,14761
(defun pg-pgip-get-pgiptype (node)pg-pgip-get-pgiptype
463,15635
(defun pg-pgip-default-for (type)pg-pgip-default-for
484,16498
(defun pg-pgip-subst-for (type)pg-pgip-subst-for
497,16893
(defun pg-pgip-interpret-value (value type)pg-pgip-interpret-value
510,17263
(defun pg-pgip-interpret-choice (choices value)pg-pgip-interpret-choice
529,17988
(defun pg-pgip-string-of-command (pgip &optional refseq refid otherclass)pg-pgip-string-of-command
560,19005
(defconst pg-pgip-idpg-pgip-id
577,19766
(defvar pg-pgip-refseq nilpg-pgip-refseq
583,20046
(defvar pg-pgip-refid nilpg-pgip-refid
585,20143
(defvar pg-pgip-seq 0 "Sequence number of messages sent out.")pg-pgip-seq
588,20235
(defun pg-pgip-assemble-packet (body &optional refseq refid otherclass)pg-pgip-assemble-packet
590,20299
(defun pg-pgip-issue (pgip &optional block refseq refid otherclass)pg-pgip-issue
608,21110
(defun pg-pgip-maybe-askpgip ()pg-pgip-maybe-askpgip
625,21722
(defun pg-pgip-askprefs ()pg-pgip-askprefs
631,21913
(defun pg-pgip-askids (&optional objtype thyname)pg-pgip-askids
635,22027
(defun pg-pgip-reset ()pg-pgip-reset
648,22315
(defconst pg-pgip-start-element-regexp "<pgip\\s-")pg-pgip-start-element-regexp
679,23013
(defconst pg-pgip-end-element-regexp   "</pgip>")pg-pgip-end-element-regexp
680,23065

generic/pg-response.el,2348
(deflocal pg-response-eagerly-raise tpg-response-eagerly-raise
32,788
(define-derived-mode proof-response-mode proof-universal-keys-only-modeproof-response-mode
42,1013
(define-key proof-response-mode-map [mouse-1] 'pg-goals-button-action)proof-response-mode-map
69,1950
(define-key proof-response-mode-map [q] 'bury-buffer)proof-response-mode-map
70,2021
(define-key proof-response-mode-map [c] 'pg-response-clear-displays)proof-response-mode-map
71,2075
(defun proof-response-config-done ()proof-response-config-done
75,2161
(defvar pg-response-special-display-regexp nilpg-response-special-display-regexp
86,2507
(defconst proof-multiframe-parametersproof-multiframe-parameters
90,2674
(defun proof-multiple-frames-enable ()proof-multiple-frames-enable
99,2964
(defun proof-three-window-enable ()proof-three-window-enable
109,3292
(defun proof-select-three-b (b1 b2 b3 &optional nohorizontalsplit)proof-select-three-b
112,3355
(defun proof-display-three-b (&optional nohorizontalsplit)proof-display-three-b
127,3846
(defvar pg-frame-configuration nilpg-frame-configuration
138,4236
(defun pg-cache-frame-configuration ()pg-cache-frame-configuration
142,4383
(defun proof-layout-windows (&optional nohorizontalsplit)proof-layout-windows
146,4554
(defun proof-delete-other-frames ()proof-delete-other-frames
186,6341
(defvar pg-response-erase-flag nilpg-response-erase-flag
217,7429
(defun pg-response-maybe-erasepg-response-maybe-erase
221,7558
(defun pg-response-display (str)pg-response-display
251,8662
(defun pg-response-display-with-face (str &optional face)pg-response-display-with-face
276,9445
(defun pg-response-clear-displays ()pg-response-clear-displays
304,10291
(defun pg-response-message (&rest args)pg-response-message
317,10810
(defun pg-response-warning (&rest args)pg-response-warning
323,11045
(defun proof-next-error (&optional argp)proof-next-error
338,11451
(defun pg-response-has-error-location ()pg-response-has-error-location
416,14260
(defvar proof-trace-last-fontify-pos nil)proof-trace-last-fontify-pos
438,15073
(defun proof-trace-fontify-pos ()proof-trace-fontify-pos
440,15116
(defun proof-trace-buffer-display (str)proof-trace-buffer-display
448,15429
(defun proof-trace-buffer-finish ()proof-trace-buffer-finish
459,15773
(defun pg-thms-buffer-clear ()pg-thms-buffer-clear
477,16116

generic/pg-user.el,6413
(defun proof-script-new-command-advance ()proof-script-new-command-advance
42,1231
(defun proof-maybe-follow-locked-end (&optional pos)proof-maybe-follow-locked-end
66,2156
(defun proof-goto-command-start ()proof-goto-command-start
92,2992
(defun proof-goto-command-end ()proof-goto-command-end
115,3939
(defun proof-forward-command (&optional num)proof-forward-command
130,4361
(defun proof-backward-command (&optional num)proof-backward-command
151,5082
(defun proof-goto-point ()proof-goto-point
162,5296
(defun proof-assert-next-command-interactive ()proof-assert-next-command-interactive
176,5730
(defun proof-assert-until-point-interactive ()proof-assert-until-point-interactive
188,6216
(defun proof-process-buffer ()proof-process-buffer
194,6446
(defun proof-undo-last-successful-command ()proof-undo-last-successful-command
212,6958
(defun proof-undo-and-delete-last-successful-command ()proof-undo-and-delete-last-successful-command
217,7120
(defun proof-undo-last-successful-command-1 (&optional undo-action)proof-undo-last-successful-command-1
229,7641
(defun proof-retract-buffer ()proof-retract-buffer
246,8305
(defun proof-retract-current-goal ()proof-retract-current-goal
255,8589
(defun proof-mouse-goto-point (event)proof-mouse-goto-point
274,9109
(defvar proof-minibuffer-history nilproof-minibuffer-history
289,9385
(defun proof-minibuffer-cmd (cmd)proof-minibuffer-cmd
292,9480
(defun proof-frob-locked-end ()proof-frob-locked-end
331,10887
(defmacro proof-if-setting-configured (var &rest body)proof-if-setting-configured
367,11988
(defmacro proof-define-assistant-command (fn doc cmdvar &optional body)proof-define-assistant-command
375,12257
(defmacro proof-define-assistant-command-witharg (fn doc cmdvar prompt &rest body)proof-define-assistant-command-witharg
388,12712
(defun proof-issue-new-command (cmd)proof-issue-new-command
408,13534
(defun proof-cd-sync ()proof-cd-sync
448,14757
(defun proof-electric-terminator-enable ()proof-electric-terminator-enable
499,16356
(defun proof-electric-terminator ()proof-electric-terminator
507,16660
(defun proof-add-completions ()proof-add-completions
531,17440
(defun proof-script-complete (&optional arg)proof-script-complete
554,18263
(defun pg-copy-span-contents (span)pg-copy-span-contents
568,18572
(defun pg-numth-span-higher-or-lower (span num &optional noerr)pg-numth-span-higher-or-lower
582,18996
(defun pg-control-span-of (span)pg-control-span-of
608,19742
(defun pg-move-span-contents (span num)pg-move-span-contents
614,19946
(defun pg-fixup-children-spans (new-parent start end)pg-fixup-children-spans
665,22064
(defun pg-move-region-down (&optional num)pg-move-region-down
675,22321
(defun pg-move-region-up (&optional num)pg-move-region-up
684,22614
(defun pg-pos-for-event (event)pg-pos-for-event
698,22888
(defun pg-span-for-event (event)pg-span-for-event
704,23109
(defun pg-span-context-menu (event)pg-span-context-menu
708,23253
(defun pg-toggle-visibility ()pg-toggle-visibility
724,23770
(defun pg-create-in-span-context-menu (span idiom name)pg-create-in-span-context-menu
733,24077
(defun pg-span-undo (span)pg-span-undo
758,25105
(defun pg-goals-buffers-hint ()pg-goals-buffers-hint
771,25343
(defun pg-slow-fontify-tracing-hint ()pg-slow-fontify-tracing-hint
775,25525
(defun pg-response-buffers-hint (&optional nextbuf)pg-response-buffers-hint
779,25696
(defun pg-jump-to-end-hint ()pg-jump-to-end-hint
791,26111
(defun pg-processing-complete-hint ()pg-processing-complete-hint
795,26240
(defun pg-next-error-hint ()pg-next-error-hint
812,26960
(defun pg-hint (hintmsg)pg-hint
817,27112
(defun pg-identifier-under-mouse-query (event)pg-identifier-under-mouse-query
828,27461
(defun pg-identifier-near-point-query ()pg-identifier-near-point-query
839,27785
(defvar proof-query-identifier-history nilproof-query-identifier-history
868,28708
(defun proof-query-identifier (string)proof-query-identifier
871,28795
(defun pg-identifier-query (identifier &optional ctxt callback)pg-identifier-query
882,29151
(defun proof-imenu-enable ()proof-imenu-enable
915,30299
(defvar pg-input-ring nilpg-input-ring
951,31602
(defvar pg-input-ring-index nilpg-input-ring-index
954,31659
(defvar pg-stored-incomplete-input nilpg-stored-incomplete-input
957,31731
(defun pg-previous-input (arg)pg-previous-input
960,31834
(defun pg-next-input (arg)pg-next-input
974,32297
(defun pg-delete-input ()pg-delete-input
979,32419
(defun pg-get-old-input ()pg-get-old-input
992,32757
(defun pg-restore-input ()pg-restore-input
1006,33148
(defun pg-search-start (arg)pg-search-start
1017,33438
(defun pg-regexp-arg (prompt)pg-regexp-arg
1029,33930
(defun pg-search-arg (arg)pg-search-arg
1041,34378
(defun pg-previous-matching-input-string-position (regexp arg &optional start)pg-previous-matching-input-string-position
1055,34795
(defun pg-previous-matching-input (regexp n)pg-previous-matching-input
1082,35960
(defun pg-next-matching-input (regexp n)pg-next-matching-input
1101,36810
(defvar pg-matching-input-from-input-string ""pg-matching-input-from-input-string
1109,37193
(defun pg-previous-matching-input-from-input (n)pg-previous-matching-input-from-input
1113,37307
(defun pg-next-matching-input-from-input (n)pg-next-matching-input-from-input
1131,38072
(defun pg-add-to-input-history (cmd)pg-add-to-input-history
1142,38451
(defun pg-remove-from-input-history (cmd)pg-remove-from-input-history
1154,38904
(defun  pg-clear-input-ring ()pg-clear-input-ring
1165,39284
(define-key proof-mode-map [remap undo] 'pg-protected-undo)proof-mode-map
1182,39754
(define-key proof-mode-map [remap advertised-undo] 'pg-protected-undo)proof-mode-map
1183,39814
(defun pg-protected-undo (&optional arg)pg-protected-undo
1185,39886
(defun pg-protected-undo-1 (arg)pg-protected-undo-1
1215,41180
(defun next-undo-elt (arg)next-undo-elt
1246,42617
(defvar proof-autosend-timer nil "Timer used by autosend.")proof-autosend-timer
1273,43573
(deflocal proof-autosend-modified-tick nilproof-autosend-modified-tick
1275,43634
(defun proof-autosend-enable (&optional nomsg)proof-autosend-enable
1279,43756
(defun proof-autosend-delay ()proof-autosend-delay
1293,44299
(defun proof-autosend-loop ()proof-autosend-loop
1297,44432
(defun proof-autosend-loop-all ()proof-autosend-loop-all
1311,44992
(defun proof-autosend-loop-next ()proof-autosend-loop-next
1335,45772

generic/pg-vars.el,2462
(defvar proof-assistant-cusgrp nilproof-assistant-cusgrp
22,388
(defvar proof-assistant-internals-cusgrp nilproof-assistant-internals-cusgrp
28,648
(defvar proof-assistant ""proof-assistant
34,918
(defvar proof-assistant-symbol nilproof-assistant-symbol
39,1141
(defvar proof-mode-for-shell nilproof-mode-for-shell
52,1683
(defvar proof-mode-for-response nilproof-mode-for-response
57,1873
(defvar proof-mode-for-goals nilproof-mode-for-goals
62,2099
(defvar proof-mode-for-script nilproof-mode-for-script
67,2288
(defvar proof-ready-for-assistant-hook nilproof-ready-for-assistant-hook
72,2465
(defvar proof-shell-busy nilproof-shell-busy
83,2753
(defvar proof-shell-last-queuemode nilproof-shell-last-queuemode
101,3424
(defvar proof-included-files-list nilproof-included-files-list
105,3579
(defvar proof-script-buffer nilproof-script-buffer
127,4598
(defvar proof-previous-script-buffer nilproof-previous-script-buffer
130,4690
(defvar proof-shell-buffer nilproof-shell-buffer
134,4863
(defvar proof-goals-buffer nilproof-goals-buffer
137,4949
(defvar proof-response-buffer nilproof-response-buffer
140,5004
(defvar proof-trace-buffer nilproof-trace-buffer
143,5065
(defvar proof-thms-buffer nilproof-thms-buffer
147,5219
(defvar proof-shell-error-or-interrupt-seen nilproof-shell-error-or-interrupt-seen
151,5374
(defvar pg-response-next-error nilpg-response-next-error
156,5598
(defvar proof-shell-proof-completed nilproof-shell-proof-completed
159,5705
(defvar proof-shell-silent nilproof-shell-silent
173,6090
(defvar proof-shell-last-prompt ""proof-shell-last-prompt
176,6178
(defvar proof-shell-last-output ""proof-shell-last-output
180,6348
(defvar proof-shell-last-output-kind nilproof-shell-last-output-kind
184,6488
(defvar proof-assistant-settings nilproof-assistant-settings
204,7252
(defvar pg-tracing-slow-mode nilpg-tracing-slow-mode
212,7731
(defvar proof-nesting-depth 0proof-nesting-depth
215,7820
(defvar proof-last-theorem-dependencies nilproof-last-theorem-dependencies
222,8055
(defvar proof-autosend-running nilproof-autosend-running
226,8217
(defvar proof-next-command-on-new-line nilproof-next-command-on-new-line
231,8416
(defcustom proof-general-name "Proof-General"proof-general-name
242,8650
(defcustom proof-general-home-pageproof-general-home-page
247,8807
(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name
253,8967
(defcustom proof-universal-keysproof-universal-keys
259,9151

generic/pg-xml.el,2460
(defalias 'pg-xml-error 'error)pg-xml-error
18,381
(defun pg-xml-parse-string (arg)pg-xml-parse-string
41,1023
(defun pg-xml-parse-buffer (&optional buffer nomsg start end)pg-xml-parse-buffer
51,1335
(defun pg-xml-get-attr (attribute node &optional optional defaultval)pg-xml-get-attr
70,1950
(defun pg-xml-child-elts (node)pg-xml-child-elts
78,2252
(defun pg-xml-child-elt (node)pg-xml-child-elt
83,2457
(defun pg-xml-get-child (child node)pg-xml-get-child
91,2739
(defun pg-xml-get-text-content (node)pg-xml-get-text-content
101,3106
(defmacro pg-xml-attr (name val) `(cons (quote ,name) ,val))pg-xml-attr
112,3456
(defmacro pg-xml-node (name atts children)pg-xml-node
114,3518
(defconst pg-xml-headerpg-xml-header
117,3610
(defun pg-xml-string-of (xmls)pg-xml-string-of
121,3686
(defun pg-xml-output-internal (xml indent-string outputfn)pg-xml-output-internal
132,4053
(defun pg-xml-cdata (str)pg-xml-cdata
166,5192
(defsubst pg-pgip-get-area (node &optional optional defaultval)pg-pgip-get-area
174,5385
(defun pg-pgip-get-icon (node &optional optional defaultval)pg-pgip-get-icon
177,5502
(defsubst pg-pgip-get-name (node &optional optional defaultval)pg-pgip-get-name
181,5650
(defsubst pg-pgip-get-version (node &optional optional defaultval)pg-pgip-get-version
184,5767
(defsubst pg-pgip-get-descr (node &optional optional defaultval)pg-pgip-get-descr
187,5890
(defsubst pg-pgip-get-thmname (node &optional optional defaultval)pg-pgip-get-thmname
190,6009
(defsubst pg-pgip-get-thyname (node &optional optional defaultval)pg-pgip-get-thyname
193,6132
(defsubst pg-pgip-get-url (node &optional optional defaultval)pg-pgip-get-url
196,6255
(defsubst pg-pgip-get-srcid (node &optional optional defaultval)pg-pgip-get-srcid
199,6370
(defsubst pg-pgip-get-proverid (node &optional optional defaultval)pg-pgip-get-proverid
202,6489
(defsubst pg-pgip-get-symname (node &optional optional defaultval)pg-pgip-get-symname
205,6614
(defsubst pg-pgip-get-prefcat (node &optional optional defaultval)pg-pgip-get-prefcat
208,6734
(defsubst pg-pgip-get-default (node &optional optional defaultval)pg-pgip-get-default
211,6862
(defsubst pg-pgip-get-objtype (node &optional optional defaultval)pg-pgip-get-objtype
214,6985
(defsubst pg-pgip-get-value (node)pg-pgip-get-value
217,7108
(defalias 'pg-pgip-get-displaytext 'pg-pgip-get-pgmltext)pg-pgip-get-displaytext
220,7178
(defun pg-pgip-get-pgmltext (node)pg-pgip-get-pgmltext
222,7237

generic/proof-autoloads.el,180
(defsubst proof-shell-live-buffer nil "\proof-shell-live-buffer
687,22209
(defsubst proof-replace-regexp-in-string (regexp rep string) "\proof-replace-regexp-in-string
840,27709

generic/proof-auxmodes.el,257
(defun proof-mmm-support-available ()proof-mmm-support-available
20,495
(defun proof-maths-menu-support-available ()proof-maths-menu-support-available
44,1114
(defun proof-unicode-tokens-support-available ()proof-unicode-tokens-support-available
58,1531

generic/proof-config.el,12929
(defgroup prover-config nilprover-config
80,2632
(defcustom proof-guess-command-line nilproof-guess-command-line
98,3482
(defcustom proof-assistant-home-page ""proof-assistant-home-page
113,3977
(defcustom proof-context-command nilproof-context-command
119,4147
(defcustom proof-info-command nilproof-info-command
124,4281
(defcustom proof-showproof-command nilproof-showproof-command
131,4552
(defcustom proof-goal-command nilproof-goal-command
136,4688
(defcustom proof-save-command nilproof-save-command
144,4985
(defcustom proof-find-theorems-command nilproof-find-theorems-command
152,5294
(defcustom proof-query-identifier-command nilproof-query-identifier-command
159,5602
(defcustom proof-assistant-true-value "true"proof-assistant-true-value
173,6291
(defcustom proof-assistant-false-value "false"proof-assistant-false-value
179,6481
(defcustom proof-assistant-format-int-fn 'int-to-stringproof-assistant-format-int-fn
185,6675
(defcustom proof-assistant-format-float-fn 'number-to-stringproof-assistant-format-float-fn
192,6924
(defcustom proof-assistant-format-string-fn  (lambda (value) value)proof-assistant-format-string-fn
199,7179
(defcustom proof-assistant-setting-format nilproof-assistant-setting-format
206,7446
(defgroup proof-script nilproof-script
228,8141
(defcustom proof-terminal-string nilproof-terminal-string
233,8271
(defcustom proof-electric-terminator-noterminator nilproof-electric-terminator-noterminator
243,8659
(defcustom proof-script-sexp-commands nilproof-script-sexp-commands
248,8831
(defcustom proof-script-command-end-regexp nilproof-script-command-end-regexp
259,9290
(defcustom proof-script-command-start-regexp nilproof-script-command-start-regexp
277,10111
(defcustom proof-script-integral-proofs nilproof-script-integral-proofs
288,10574
(defcustom proof-script-fly-past-comments nilproof-script-fly-past-comments
303,11230
(defcustom proof-script-parse-function nilproof-script-parse-function
308,11401
(defcustom proof-script-comment-start ""proof-script-comment-start
326,12046
(defcustom proof-script-comment-start-regexp nilproof-script-comment-start-regexp
337,12483
(defcustom proof-script-comment-end ""proof-script-comment-end
345,12802
(defcustom proof-script-comment-end-regexp nilproof-script-comment-end-regexp
357,13224
(defcustom proof-string-start-regexp "\""proof-string-start-regexp
365,13537
(defcustom proof-string-end-regexp "\""proof-string-end-regexp
370,13702
(defcustom proof-case-fold-search nilproof-case-fold-search
375,13863
(defcustom proof-save-command-regexp nilproof-save-command-regexp
384,14275
(defcustom proof-save-with-hole-regexp nilproof-save-with-hole-regexp
389,14385
(defcustom proof-save-with-hole-result 2proof-save-with-hole-result
400,14760
(defcustom proof-goal-command-regexp nilproof-goal-command-regexp
410,15200
(defcustom proof-goal-with-hole-regexp nilproof-goal-with-hole-regexp
418,15487
(defcustom proof-goal-with-hole-result 2proof-goal-with-hole-result
430,15930
(defcustom proof-non-undoables-regexp nilproof-non-undoables-regexp
439,16304
(defcustom proof-nested-undo-regexp nilproof-nested-undo-regexp
450,16759
(defcustom proof-ignore-for-undo-count nilproof-ignore-for-undo-count
466,17471
(defcustom proof-script-imenu-generic-expression nilproof-script-imenu-generic-expression
474,17774
(defcustom proof-goal-command-p 'proof-generic-goal-command-pproof-goal-command-p
482,18113
(defcustom proof-really-save-command-p (lambda (span cmd) t)proof-really-save-command-p
493,18604
(defcustom proof-completed-proof-behaviour nilproof-completed-proof-behaviour
502,18911
(defcustom proof-count-undos-fn 'proof-generic-count-undosproof-count-undos-fn
530,20260
(defcustom proof-find-and-forget-fn 'proof-generic-find-and-forgetproof-find-and-forget-fn
542,20811
(defcustom proof-forget-id-command nilproof-forget-id-command
559,21520
(defcustom pg-topterm-goalhyplit-fn nilpg-topterm-goalhyplit-fn
569,21878
(defcustom proof-kill-goal-command nilproof-kill-goal-command
581,22413
(defcustom proof-undo-n-times-cmd nilproof-undo-n-times-cmd
595,22917
(defcustom proof-nested-goals-history-p nilproof-nested-goals-history-p
609,23454
(defcustom proof-arbitrary-undo-positions nilproof-arbitrary-undo-positions
618,23791
(defcustom proof-state-preserving-p 'proof-generic-state-preserving-pproof-state-preserving-p
632,24372
(defcustom proof-activate-scripting-hook nilproof-activate-scripting-hook
642,24844
(defcustom proof-deactivate-scripting-hook nilproof-deactivate-scripting-hook
661,25625
(defcustom proof-no-fully-processed-buffer nilproof-no-fully-processed-buffer
670,25955
(defcustom proof-script-evaluate-elisp-comment-regexp "ELISP: -- \\(.*\\) --"proof-script-evaluate-elisp-comment-regexp
681,26453
(defcustom proof-indent 2proof-indent
699,27039
(defcustom proof-indent-hang nilproof-indent-hang
704,27146
(defcustom proof-indent-enclose-offset 1proof-indent-enclose-offset
709,27272
(defcustom proof-indent-open-offset 1proof-indent-open-offset
714,27414
(defcustom proof-indent-close-offset 1proof-indent-close-offset
719,27551
(defcustom proof-indent-any-regexp "\\s(\\|\\s)"proof-indent-any-regexp
724,27689
(defcustom proof-indent-inner-regexp nilproof-indent-inner-regexp
729,27849
(defcustom proof-indent-enclose-regexp nilproof-indent-enclose-regexp
734,28003
(defcustom proof-indent-open-regexp "\\s("proof-indent-open-regexp
739,28157
(defcustom proof-indent-close-regexp "\\s)"proof-indent-close-regexp
744,28309
(defcustom proof-script-font-lock-keywords nilproof-script-font-lock-keywords
750,28463
(defcustom proof-script-syntax-table-entries nilproof-script-syntax-table-entries
758,28815
(defcustom proof-script-span-context-menu-extensions nilproof-script-span-context-menu-extensions
776,29211
(defgroup proof-shell nilproof-shell
802,29971
(defcustom proof-prog-name nilproof-prog-name
812,30141
(defcustom proof-shell-auto-terminate-commands tproof-shell-auto-terminate-commands
824,30608
(defcustom proof-shell-pre-sync-init-cmd nilproof-shell-pre-sync-init-cmd
833,31013
(defcustom proof-shell-init-cmd nilproof-shell-init-cmd
847,31571
(defcustom proof-shell-init-hook nilproof-shell-init-hook
859,32117
(defcustom proof-shell-restart-cmd ""proof-shell-restart-cmd
864,32256
(defcustom proof-shell-quit-cmd nilproof-shell-quit-cmd
869,32411
(defcustom proof-shell-cd-cmd nilproof-shell-cd-cmd
874,32578
(defcustom proof-shell-start-silent-cmd nilproof-shell-start-silent-cmd
891,33249
(defcustom proof-shell-stop-silent-cmd nilproof-shell-stop-silent-cmd
900,33625
(defcustom proof-shell-silent-threshold 2proof-shell-silent-threshold
909,33960
(defcustom  proof-shell-inform-file-processed-cmd nilproof-shell-inform-file-processed-cmd
917,34294
(defcustom  proof-shell-inform-file-retracted-cmd nilproof-shell-inform-file-retracted-cmd
938,35222
(defcustom proof-auto-multiple-files nilproof-auto-multiple-files
966,36494
(defcustom proof-cannot-reopen-processed-files nilproof-cannot-reopen-processed-files
981,37215
(defcustom proof-shell-require-command-regexp nilproof-shell-require-command-regexp
995,37881
(defcustom proof-done-advancing-require-function nilproof-done-advancing-require-function
1006,38343
(defcustom proof-shell-annotated-prompt-regexp nilproof-shell-annotated-prompt-regexp
1018,38703
(defcustom proof-shell-error-regexp nilproof-shell-error-regexp
1033,39268
(defcustom proof-shell-truncate-before-error tproof-shell-truncate-before-error
1053,40070
(defcustom pg-next-error-regexp nilpg-next-error-regexp
1067,40609
(defcustom pg-next-error-filename-regexp nilpg-next-error-filename-regexp
1082,41218
(defcustom pg-next-error-extract-filename nilpg-next-error-extract-filename
1106,42251
(defcustom proof-shell-interrupt-regexp nilproof-shell-interrupt-regexp
1113,42494
(defcustom proof-shell-proof-completed-regexp nilproof-shell-proof-completed-regexp
1127,43089
(defcustom proof-shell-clear-response-regexp nilproof-shell-clear-response-regexp
1140,43597
(defcustom proof-shell-clear-goals-regexp nilproof-shell-clear-goals-regexp
1152,44049
(defcustom proof-shell-start-goals-regexp nilproof-shell-start-goals-regexp
1164,44495
(defcustom proof-shell-end-goals-regexp nilproof-shell-end-goals-regexp
1172,44862
(defcustom proof-shell-eager-annotation-start nilproof-shell-eager-annotation-start
1186,45435
(defcustom proof-shell-eager-annotation-start-length 10proof-shell-eager-annotation-start-length
1209,46454
(defcustom proof-shell-eager-annotation-end "\n"proof-shell-eager-annotation-end
1220,46880
(defcustom proof-shell-strip-output-markup 'identityproof-shell-strip-output-markup
1236,47555
(defcustom proof-shell-assumption-regexp nilproof-shell-assumption-regexp
1245,47940
(defcustom proof-shell-process-file nilproof-shell-process-file
1255,48344
(defcustom proof-shell-retract-files-regexp nilproof-shell-retract-files-regexp
1281,49420
(defcustom proof-shell-compute-new-files-list nilproof-shell-compute-new-files-list
1294,49908
(defcustom pg-special-char-regexp "[\200-\377]"pg-special-char-regexp
1309,50475
(defcustom proof-shell-set-elisp-variable-regexp nilproof-shell-set-elisp-variable-regexp
1314,50619
(defcustom proof-shell-match-pgip-cmd nilproof-shell-match-pgip-cmd
1352,52285
(defcustom proof-shell-issue-pgip-cmd nilproof-shell-issue-pgip-cmd
1366,52767
(defcustom proof-use-pgip-askprefs nilproof-use-pgip-askprefs
1371,52932
(defcustom proof-shell-query-dependencies-cmd nilproof-shell-query-dependencies-cmd
1379,53279
(defcustom proof-shell-theorem-dependency-list-regexp nilproof-shell-theorem-dependency-list-regexp
1386,53539
(defcustom proof-shell-theorem-dependency-list-split nilproof-shell-theorem-dependency-list-split
1402,54199
(defcustom proof-shell-show-dependency-cmd nilproof-shell-show-dependency-cmd
1411,54622
(defcustom proof-shell-trace-output-regexp nilproof-shell-trace-output-regexp
1433,55528
(defcustom proof-shell-thms-output-regexp nilproof-shell-thms-output-regexp
1451,56122
(defcustom proof-tokens-activate-command nilproof-tokens-activate-command
1464,56505
(defcustom proof-tokens-deactivate-command nilproof-tokens-deactivate-command
1471,56745
(defcustom proof-tokens-extra-modes nilproof-tokens-extra-modes
1478,56990
(defcustom proof-shell-unicode tproof-shell-unicode
1493,57495
(defcustom proof-shell-filename-escapes nilproof-shell-filename-escapes
1502,57885
(defcustom proof-shell-process-connection-type tproof-shell-process-connection-type
1519,58565
(defcustom proof-shell-strip-crs-from-input tproof-shell-strip-crs-from-input
1525,58756
(defcustom proof-shell-strip-crs-from-output (eq system-type 'cygwin32)proof-shell-strip-crs-from-output
1537,59239
(defcustom proof-shell-extend-queue-hook nilproof-shell-extend-queue-hook
1545,59607
(defcustom proof-shell-insert-hook nilproof-shell-insert-hook
1555,60037
(defcustom proof-script-preprocess nilproof-script-preprocess
1596,61997
(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook
1602,62148
(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook
1608,62363
(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook
1626,63109
(defcustom proof-shell-handle-output-system-specific nilproof-shell-handle-output-system-specific
1634,63380
(defcustom proof-state-change-hook nilproof-state-change-hook
1657,64353
(defcustom proof-shell-syntax-table-entries nilproof-shell-syntax-table-entries
1667,64746
(defgroup proof-goals nilproof-goals
1685,65117
(defcustom pg-subterm-first-special-char nilpg-subterm-first-special-char
1690,65238
(defcustom pg-subterm-anns-use-stack nilpg-subterm-anns-use-stack
1698,65550
(defcustom pg-goals-change-goal nilpg-goals-change-goal
1707,65849
(defcustom pbp-goal-command nilpbp-goal-command
1712,65965
(defcustom pbp-hyp-command nilpbp-hyp-command
1717,66121
(defcustom pg-subterm-help-cmd nilpg-subterm-help-cmd
1722,66283
(defcustom pg-goals-error-regexp nilpg-goals-error-regexp
1729,66519
(defcustom proof-shell-result-start nilproof-shell-result-start
1734,66679
(defcustom proof-shell-result-end ""proof-shell-result-end
1740,66913
(defcustom pg-subterm-start-char nilpg-subterm-start-char
1746,67126
(defcustom pg-subterm-sep-char nilpg-subterm-sep-char
1757,67600
(defcustom pg-subterm-end-char nilpg-subterm-end-char
1763,67779
(defcustom pg-topterm-regexp nilpg-topterm-regexp
1769,67936
(defcustom proof-goals-font-lock-keywords nilproof-goals-font-lock-keywords
1784,68536
(defcustom proof-response-font-lock-keywords nilproof-response-font-lock-keywords
1792,68895
(defcustom proof-shell-font-lock-keywords nilproof-shell-font-lock-keywords
1800,69257
(defcustom pg-before-fontify-output-hook nilpg-before-fontify-output-hook
1811,69771
(defcustom pg-after-fontify-output-hook nilpg-after-fontify-output-hook
1819,70132

generic/proof-depends.el,1643
(defvar proof-thm-names-of-files nilproof-thm-names-of-files
25,639
(defvar proof-def-names-of-files nilproof-def-names-of-files
31,923
(defun proof-depends-module-name-for-buffer ()proof-depends-module-name-for-buffer
42,1238
(defun proof-depends-module-of (name)proof-depends-module-of
52,1679
(defun proof-depends-names-in-same-file (names)proof-depends-names-in-same-file
60,1970
(defun proof-depends-process-dependencies (name gspan)proof-depends-process-dependencies
79,2578
(defun proof-dependency-in-span-context-menu (span)proof-dependency-in-span-context-menu
132,4313
(defun proof-dep-alldeps-menu (span)proof-dep-alldeps-menu
155,5203
(defun proof-dep-make-alldeps-menu (deps)proof-dep-make-alldeps-menu
161,5429
(defun proof-dep-split-deps (deps)proof-dep-split-deps
179,5924
(defun proof-dep-make-submenu (name namefn appfn list)proof-dep-make-submenu
198,6590
(defun proof-make-highlight-depts-menu (name fn span prop)proof-make-highlight-depts-menu
209,7001
(defun proof-goto-dependency (name span)proof-goto-dependency
220,7309
(defun proof-show-dependency (thm)proof-show-dependency
227,7561
(defconst pg-dep-span-priority 500)pg-dep-span-priority
234,7850
(defconst pg-ordinary-span-priority 100)pg-ordinary-span-priority
235,7886
(defun proof-highlight-depcs (name nmspans)proof-highlight-depcs
237,7928
(defun proof-highlight-depts (name nmspans)proof-highlight-depts
248,8394
(defun proof-depends-save-old-face (span)proof-depends-save-old-face
260,8904
(defun proof-depends-restore-old-face (span)proof-depends-restore-old-face
265,9081
(defun proof-dep-unhighlight ()proof-dep-unhighlight
271,9310

generic/proof-easy-config.el,350
(defconst proof-easy-config-derived-modes-tableproof-easy-config-derived-modes-table
16,544
(defun proof-easy-config-define-derived-modes ()proof-easy-config-define-derived-modes
23,950
(defun proof-easy-config-check-setup (sym name)proof-easy-config-check-setup
52,2135
(defmacro proof-easy-config (sym name &rest body)proof-easy-config
84,3465

generic/proof.el,0

generic/proof-faces.el,3822
(defgroup proof-faces nilproof-faces
29,809
(defconst pg-defface-window-systemspg-defface-window-systems
36,989
(defmacro proof-face-specs (bl bd ow)proof-face-specs
49,1551
(defface proof-queue-faceproof-queue-face
64,2003
(defface proof-locked-faceproof-locked-face
72,2281
(defface proof-declaration-name-faceproof-declaration-name-face
82,2602
(defface proof-tacticals-name-faceproof-tacticals-name-face
91,2888
(defface proof-tactics-name-faceproof-tactics-name-face
100,3150
(defface proof-error-faceproof-error-face
109,3415
(defface proof-warning-faceproof-warning-face
117,3636
(defface proof-eager-annotation-faceproof-eager-annotation-face
126,3893
(defface proof-debug-message-faceproof-debug-message-face
134,4111
(defface proof-boring-faceproof-boring-face
142,4310
(defface proof-mouse-highlight-faceproof-mouse-highlight-face
150,4502
(defface proof-command-mouse-highlight-faceproof-command-mouse-highlight-face
158,4720
(defface proof-region-mouse-highlight-faceproof-region-mouse-highlight-face
166,4959
(defface proof-highlight-dependent-faceproof-highlight-dependent-face
174,5201
(defface proof-highlight-dependency-faceproof-highlight-dependency-face
182,5408
(defface proof-active-area-faceproof-active-area-face
190,5605
(defface proof-script-sticky-error-faceproof-script-sticky-error-face
198,5917
(defface proof-script-highlight-error-faceproof-script-highlight-error-face
206,6146
(defconst proof-face-compat-doc "Evaluates to a face name, for compatibility.")proof-face-compat-doc
218,6491
(defconst proof-queue-face 'proof-queue-face proof-face-compat-doc)proof-queue-face
219,6571
(defconst proof-locked-face 'proof-locked-face proof-face-compat-doc)proof-locked-face
220,6639
(defconst proof-declaration-name-face 'proof-declaration-name-face proof-face-compat-doc)proof-declaration-name-face
221,6709
(defconst proof-tacticals-name-face 'proof-tacticals-name-face proof-face-compat-doc)proof-tacticals-name-face
222,6799
(defconst proof-tactics-name-face 'proof-tactics-name-face proof-face-compat-doc)proof-tactics-name-face
223,6885
(defconst proof-error-face 'proof-error-face proof-face-compat-doc)proof-error-face
224,6967
(defconst proof-script-sticky-error-face 'proof-script-sticky-error-face proof-face-compat-doc)proof-script-sticky-error-face
225,7035
(defconst proof-script-highlight-error-face 'proof-script-highlight-error-face proof-face-compat-doc)proof-script-highlight-error-face
226,7131
(defconst proof-warning-face 'proof-warning-face proof-face-compat-doc)proof-warning-face
227,7233
(defconst proof-eager-annotation-face 'proof-eager-annotation-face proof-face-compat-doc)proof-eager-annotation-face
228,7305
(defconst proof-debug-message-face 'proof-debug-message-face proof-face-compat-doc)proof-debug-message-face
229,7395
(defconst proof-boring-face 'proof-boring-face proof-face-compat-doc)proof-boring-face
230,7479
(defconst proof-mouse-highlight-face 'proof-mouse-highlight-face proof-face-compat-doc)proof-mouse-highlight-face
231,7549
(defconst proof-command-mouse-highlight-face 'proof-command-mouse-highlight-face proof-face-compat-doc)proof-command-mouse-highlight-face
232,7637
(defconst proof-region-mouse-highlight-face 'proof-region-mouse-highlight-face proof-face-compat-doc)proof-region-mouse-highlight-face
233,7741
(defconst proof-highlight-dependent-face 'proof-highlight-dependent-face proof-face-compat-doc)proof-highlight-dependent-face
234,7843
(defconst proof-highlight-dependency-face 'proof-highlight-dependency-face proof-face-compat-doc)proof-highlight-dependency-face
235,7939
(defconst proof-active-area-face 'proof-active-area-face proof-face-compat-doc)proof-active-area-face
236,8037
(defconst proof-script-error-face 'proof-script-errror-face-compat-doc)proof-script-error-face
237,8117

generic/proof-indent.el,448
(defun proof-indent-indent ()proof-indent-indent
19,449
(defun proof-indent-offset ()proof-indent-offset
28,715
(defun proof-indent-inner-p ()proof-indent-inner-p
45,1316
(defun proof-indent-goto-prev ()   ; Note: may change point, even in case of failure!proof-indent-goto-prev
54,1616
(defun proof-indent-calculate (indent inner)  ; Note: may change point!proof-indent-calculate
61,1949
(defun proof-indent-line ()proof-indent-line
82,2708

generic/proof-maths-menu.el,143
(defun proof-maths-menu-set-global (flag)proof-maths-menu-set-global
32,906
(defun proof-maths-menu-enable ()proof-maths-menu-enable
46,1357

generic/proof-menu.el,3776
(defvar proof-display-some-buffers-count 0)proof-display-some-buffers-count
36,815
(defun proof-display-some-buffers ()proof-display-some-buffers
38,860
(defun proof-menu-define-keys (map)proof-menu-define-keys
95,2987
(defun proof-menu-define-main ()proof-menu-define-main
153,5812
(defvar proof-menu-favourites nilproof-menu-favourites
162,5997
(defvar proof-menu-settings nilproof-menu-settings
165,6104
(defun proof-menu-define-specific ()proof-menu-define-specific
169,6193
(defun proof-assistant-menu-update ()proof-assistant-menu-update
212,7455
(defvar proof-help-menuproof-help-menu
226,7888
(defvar proof-show-hide-menuproof-show-hide-menu
234,8158
(defvar proof-buffer-menuproof-buffer-menu
245,8582
(defun proof-keep-response-history ()proof-keep-response-history
308,10898
(defconst proof-quick-opts-menuproof-quick-opts-menu
316,11208
(defun proof-quick-opts-vars ()proof-quick-opts-vars
534,20114
(defun proof-quick-opts-changed-from-defaults-p ()proof-quick-opts-changed-from-defaults-p
566,21054
(defun proof-quick-opts-changed-from-saved-p ()proof-quick-opts-changed-from-saved-p
570,21159
(defun proof-set-document-centred ()proof-set-document-centred
578,21315
(defun proof-set-non-document-centred ()proof-set-non-document-centred
591,21741
(defun proof-quick-opts-save ()proof-quick-opts-save
610,22452
(defun proof-quick-opts-reset ()proof-quick-opts-reset
615,22620
(defconst proof-config-menuproof-config-menu
627,22888
(defconst proof-advanced-menuproof-advanced-menu
634,23067
(defvar proof-menuproof-menu
652,23751
(defun proof-main-menu ()proof-main-menu
661,24033
(defun proof-aux-menu ()proof-aux-menu
673,24372
(defun proof-menu-define-favourites-menu ()proof-menu-define-favourites-menu
689,24718
(defun proof-def-favourite (command inscript menuname &optional key new)proof-def-favourite
709,25367
(defvar proof-make-favourite-cmd-history nilproof-make-favourite-cmd-history
736,26360
(defvar proof-make-favourite-menu-history nilproof-make-favourite-menu-history
739,26445
(defun proof-save-favourites ()proof-save-favourites
742,26531
(defun proof-del-favourite (menuname)proof-del-favourite
747,26679
(defun proof-read-favourite ()proof-read-favourite
764,27235
(defun proof-add-favourite (command inscript menuname &optional key)proof-add-favourite
788,28009
(defun proof-menu-define-settings-menu ()proof-menu-define-settings-menu
815,29054
(defun proof-menu-entry-name (symbol)proof-menu-entry-name
844,30046
(defun proof-menu-entry-for-setting (symbol setting type descr)proof-menu-entry-for-setting
854,30396
(defun proof-settings-vars ()proof-settings-vars
877,31034
(defun proof-settings-changed-from-defaults-p ()proof-settings-changed-from-defaults-p
882,31211
(defun proof-settings-changed-from-saved-p ()proof-settings-changed-from-saved-p
886,31317
(defun proof-settings-save ()proof-settings-save
890,31420
(defun proof-settings-reset ()proof-settings-reset
895,31587
(defun proof-assistant-invisible-command-ifposs (cmd)proof-assistant-invisible-command-ifposs
900,31750
(defun proof-maybe-askprefs ()proof-maybe-askprefs
922,32720
(defun proof-assistant-settings-cmd (setting)proof-assistant-settings-cmd
928,32913
(defun proof-assistant-settings-cmds ()proof-assistant-settings-cmds
936,33197
(defvar proof-assistant-format-tableproof-assistant-format-table
946,33539
(defun proof-assistant-format-bool (value)proof-assistant-format-bool
955,33965
(defun proof-assistant-format-int (value)proof-assistant-format-int
958,34078
(defun proof-assistant-format-float (value)proof-assistant-format-float
961,34170
(defun proof-assistant-format-string (value)proof-assistant-format-string
964,34266
(defun proof-assistant-format (string curvalue)proof-assistant-format
967,34364

generic/proof-mmm.el,116
(defun proof-mmm-set-global (flag)proof-mmm-set-global
43,1439
(defun proof-mmm-enable ()proof-mmm-enable
58,1978

generic/proof-script.el,10148
(deflocal proof-active-buffer-fake-minor-mode nilproof-active-buffer-fake-minor-mode
46,1413
(deflocal proof-script-buffer-file-name nilproof-script-buffer-file-name
49,1539
(deflocal pg-script-portions nilpg-script-portions
56,1949
(defun proof-next-element-count (idiom)proof-next-element-count
66,2169
(defun proof-element-id (idiom number)proof-element-id
72,2411
(defun proof-next-element-id (idiom)proof-next-element-id
76,2580
(deflocal proof-locked-span nilproof-locked-span
112,3884
(deflocal proof-queue-span nilproof-queue-span
119,4150
(deflocal proof-overlay-arrow nilproof-overlay-arrow
128,4636
(defun proof-span-give-warning (&rest args)proof-span-give-warning
134,4763
(defun proof-span-read-only (span &optional always)proof-span-read-only
140,4943
(defun proof-strict-read-only ()proof-strict-read-only
149,5316
(defsubst proof-set-queue-endpoints (start end)proof-set-queue-endpoints
159,5694
(defun proof-set-overlay-arrow (pos)proof-set-overlay-arrow
163,5835
(defsubst proof-set-locked-endpoints (start end)proof-set-locked-endpoints
174,6173
(defsubst proof-detach-queue ()proof-detach-queue
179,6349
(defsubst proof-detach-locked ()proof-detach-locked
184,6488
(defsubst proof-set-queue-start (start)proof-set-queue-start
191,6713
(defsubst proof-set-locked-end (end)proof-set-locked-end
195,6839
(defsubst proof-set-queue-end (end)proof-set-queue-end
207,7309
(defun proof-init-segmentation ()proof-init-segmentation
218,7606
(defun proof-colour-locked ()proof-colour-locked
248,8857
(defun proof-colour-locked-span ()proof-colour-locked-span
255,9130
(defun proof-sticky-errors ()proof-sticky-errors
261,9403
(defun proof-restart-buffers (buffers)proof-restart-buffers
274,9819
(defun proof-script-buffers-with-spans ()proof-script-buffers-with-spans
296,10638
(defun proof-script-remove-all-spans-and-deactivate ()proof-script-remove-all-spans-and-deactivate
306,10994
(defun proof-script-clear-queue-spans-on-error (badspan &optional interruptp)proof-script-clear-queue-spans-on-error
310,11184
(defun proof-script-delete-spans (beg end)proof-script-delete-spans
336,12201
(defun proof-script-delete-secondary-spans (beg end)proof-script-delete-secondary-spans
341,12400
(defun proof-unprocessed-begin ()proof-unprocessed-begin
354,12689
(defun proof-script-end ()proof-script-end
362,12943
(defun proof-queue-or-locked-end ()proof-queue-or-locked-end
371,13253
(defun proof-locked-region-full-p ()proof-locked-region-full-p
390,13846
(defun proof-locked-region-empty-p ()proof-locked-region-empty-p
399,14118
(defun proof-only-whitespace-to-locked-region-p ()proof-only-whitespace-to-locked-region-p
403,14268
(defun proof-in-locked-region-p ()proof-in-locked-region-p
413,14617
(defun proof-goto-end-of-locked (&optional switch)proof-goto-end-of-locked
425,14874
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window ()proof-goto-end-of-locked-if-pos-not-visible-in-window
442,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-window
453,16114
(defun proof-end-of-locked-visible-p ()proof-end-of-locked-visible-p
465,16654
(defconst pg-idioms '(proof)pg-idioms
484,17247
(defconst pg-all-idioms (append pg-idiomspg-all-idioms
487,17343
(defun pg-clear-script-portions ()pg-clear-script-portions
491,17464
(defun pg-remove-element (idiom id)pg-remove-element
497,17699
(defun pg-get-element (idiomsym id)pg-get-element
505,18002
(defun pg-add-element (idiomsym id span &optional name)pg-add-element
515,18317
(defun pg-invisible-prop (idiom)pg-invisible-prop
563,20279
(defun pg-set-element-span-invisible (span invisiblep)pg-set-element-span-invisible
568,20480
(defun pg-toggle-element-span-visibility (span)pg-toggle-element-span-visibility
581,21046
(defun pg-open-invisible-span (span &optional invisible)pg-open-invisible-span
586,21207
(defun pg-make-element-invisible (idiomsym id)pg-make-element-invisible
591,21378
(defun pg-make-element-visible (idiomsym id)pg-make-element-visible
596,21589
(defun pg-toggle-element-visibility (idiomsym id)pg-toggle-element-visibility
601,21783
(defun pg-show-all-portions (idiom &optional hide)pg-show-all-portions
607,22046
(defun pg-show-all-proofs ()pg-show-all-proofs
629,22790
(defun pg-hide-all-proofs ()pg-hide-all-proofs
634,22918
(defun pg-add-proof-element (name span controlspan)pg-add-proof-element
639,23049
(defun pg-span-name (span)pg-span-name
654,23836
(defvar pg-span-context-menu-keymappg-span-context-menu-keymap
687,25043
(defun pg-last-output-displayform ()pg-last-output-displayform
694,25281
(defun pg-set-span-helphighlights (span &optional mouseface face)pg-set-span-helphighlights
717,26172
(defun proof-complete-buffer-atomic (buffer)proof-complete-buffer-atomic
775,28149
(defun proof-register-possibly-new-processed-fileproof-register-possibly-new-processed-file
804,29419
(defun proof-query-save-this-buffer-p ()proof-query-save-this-buffer-p
850,31293
(defun proof-inform-prover-file-retracted (rfile)proof-inform-prover-file-retracted
855,31518
(defun proof-auto-retract-dependencies (cfile &optional informprover)proof-auto-retract-dependencies
875,32369
(defun proof-unregister-buffer-file-name (&optional informprover)proof-unregister-buffer-file-name
929,34919
(defsubst proof-action-completed (action)proof-action-completed
975,36744
(defun proof-protected-process-or-retract (action &optional buffer)proof-protected-process-or-retract
979,36914
(defun proof-deactivate-scripting-auto ()proof-deactivate-scripting-auto
1007,38145
(defun proof-deactivate-scripting-query-user-action ()proof-deactivate-scripting-query-user-action
1016,38503
(defun proof-deactivate-scripting-choose-action ()proof-deactivate-scripting-choose-action
1060,40012
(defun proof-deactivate-scripting (&optional forcedaction)proof-deactivate-scripting
1072,40397
(defun proof-activate-scripting (&optional nosaves queuemode)proof-activate-scripting
1169,44520
(defun proof-toggle-active-scripting (&optional arg)proof-toggle-active-scripting
1269,49045
(defun proof-done-advancing (span)proof-done-advancing
1308,50290
(defun proof-done-advancing-comment (span)proof-done-advancing-comment
1387,53275
(defun proof-done-advancing-save (span)proof-done-advancing-save
1421,54661
(defun proof-make-goalsaveproof-make-goalsave
1509,58025
(defun proof-get-name-from-goal (gspan)proof-get-name-from-goal
1527,58890
(defun proof-done-advancing-autosave (span)proof-done-advancing-autosave
1547,59915
(defun proof-done-advancing-other (span)proof-done-advancing-other
1611,62411
(defun proof-segment-up-to-parser (pos &optional next-command-end)proof-segment-up-to-parser
1640,63375
(defun proof-script-generic-parse-find-comment-end ()proof-script-generic-parse-find-comment-end
1709,65641
(defun proof-script-generic-parse-cmdend ()proof-script-generic-parse-cmdend
1718,66055
(defun proof-script-generic-parse-cmdstart ()proof-script-generic-parse-cmdstart
1769,67951
(defun proof-script-generic-parse-sexp ()proof-script-generic-parse-sexp
1808,69551
(defun proof-semis-to-vanillas (semis &optional queueflags)proof-semis-to-vanillas
1820,70017
(defun proof-next-command-new-line ()proof-next-command-new-line
1873,71690
(defun proof-script-next-command-advance ()proof-script-next-command-advance
1878,71896
(defun proof-assert-until-point (&optional displayflags)proof-assert-until-point
1897,72396
(defun proof-assert-electric-terminator ()proof-assert-electric-terminator
1912,73023
(defun proof-assert-semis (semis &optional displayflags)proof-assert-semis
1955,74655
(defun proof-retract-before-change (beg end)proof-retract-before-change
1969,75396
(defun proof-insert-pbp-command (cmd)proof-insert-pbp-command
1989,75992
(defun proof-insert-sendback-command (cmd)proof-insert-sendback-command
2004,76495
(defun proof-done-retracting (span)proof-done-retracting
2030,77398
(defun proof-setup-retract-action (start end proof-commands remove-action &optional proof-setup-retract-action
2065,78852
(defun proof-last-goal-or-goalsave ()proof-last-goal-or-goalsave
2077,79457
(defun proof-retract-target (target undo-action displayflags)proof-retract-target
2101,80369
(defun proof-retract-until-point-interactive (&optional delete-region)proof-retract-until-point-interactive
2180,83622
(defun proof-retract-until-point (&optional undo-action displayflags)proof-retract-until-point
2189,84029
(define-derived-mode proof-mode fundamental-modeproof-mode
2244,86037
(defun proof-script-set-visited-file-name ()proof-script-set-visited-file-name
2280,87419
(defun proof-script-set-buffer-hooks ()proof-script-set-buffer-hooks
2302,88432
(defun proof-script-kill-buffer-fn ()proof-script-kill-buffer-fn
2310,88850
(defun proof-config-done-related ()proof-config-done-related
2342,90167
(defun proof-generic-goal-command-p (span)proof-generic-goal-command-p
2407,92652
(defun proof-generic-state-preserving-p (cmd)proof-generic-state-preserving-p
2412,92865
(defun proof-generic-count-undos (span)proof-generic-count-undos
2421,93382
(defun proof-generic-find-and-forget (span)proof-generic-find-and-forget
2452,94510
(defconst proof-script-important-settingsproof-script-important-settings
2503,96282
(defun proof-config-done ()proof-config-done
2518,96828
(defun proof-setup-parsing-mechanism ()proof-setup-parsing-mechanism
2585,98993
(defun proof-setup-imenu ()proof-setup-imenu
2609,100065
(deflocal proof-segment-up-to-cache nil)proof-segment-up-to-cache
2636,100843
(deflocal proof-segment-up-to-cache-start 0)proof-segment-up-to-cache-start
2637,100884
(deflocal proof-last-edited-low-watermark nil)proof-last-edited-low-watermark
2638,100929
(defun proof-segment-up-to-using-cache (pos &rest args)proof-segment-up-to-using-cache
2648,101416
(defun proof-segment-cache-contents-for (pos)proof-segment-cache-contents-for
2676,102418
(defun proof-script-after-change-function (start end prelength)proof-script-after-change-function
2688,102787
(defun proof-script-set-after-change-functions ()proof-script-set-after-change-functions
2700,103294

generic/proof-shell.el,6424
(defvar proof-marker nilproof-marker
34,746
(defvar proof-action-list nilproof-action-list
37,842
(defsubst proof-shell-invoke-callback (listitem)proof-shell-invoke-callback
75,2315
(defvar proof-shell-last-goals-output ""proof-shell-last-goals-output
89,2807
(defvar proof-shell-last-response-output ""proof-shell-last-response-output
92,2887
(defvar proof-shell-delayed-output-start nilproof-shell-delayed-output-start
95,2974
(defvar proof-shell-delayed-output-end nilproof-shell-delayed-output-end
99,3156
(defvar proof-shell-delayed-output-flags nilproof-shell-delayed-output-flags
103,3336
(defvar proof-shell-interrupt-pending nilproof-shell-interrupt-pending
106,3461
(defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator
117,3756
(defun proof-shell-ready-prover (&optional queuemode)proof-shell-ready-prover
169,5340
(defsubst proof-shell-live-buffer ()proof-shell-live-buffer
183,5879
(defun proof-shell-available-p ()proof-shell-available-p
190,6099
(defun proof-grab-lock (&optional queuemode)proof-grab-lock
196,6321
(defun proof-release-lock ()proof-release-lock
206,6750
(defcustom proof-shell-fiddle-frames tproof-shell-fiddle-frames
216,6924
(defun proof-shell-set-text-representation ()proof-shell-set-text-representation
221,7082
(defun proof-shell-start ()proof-shell-start
229,7410
(defvar proof-shell-kill-function-hooks nilproof-shell-kill-function-hooks
412,13646
(defun proof-shell-kill-function ()proof-shell-kill-function
415,13744
(defun proof-shell-clear-state ()proof-shell-clear-state
476,15862
(defun proof-shell-exit (&optional dont-ask)proof-shell-exit
492,16337
(defun proof-shell-bail-out (process event)proof-shell-bail-out
512,17109
(defun proof-shell-restart ()proof-shell-restart
522,17631
(defvar proof-shell-urgent-message-marker nilproof-shell-urgent-message-marker
563,19003
(defvar proof-shell-urgent-message-scanner nilproof-shell-urgent-message-scanner
566,19124
(defun proof-shell-handle-error-output (start-regexp append-face)proof-shell-handle-error-output
570,19309
(defun proof-shell-handle-error-or-interrupt (err-or-int flags)proof-shell-handle-error-or-interrupt
596,20171
(defun proof-shell-error-or-interrupt-action (err-or-int)proof-shell-error-or-interrupt-action
639,21920
(defun proof-goals-pos (span maparg)proof-goals-pos
666,23017
(defun proof-pbp-focus-on-first-goal ()proof-pbp-focus-on-first-goal
671,23228
(defsubst proof-shell-string-match-safe (regexp string)proof-shell-string-match-safe
683,23644
(defun proof-shell-handle-immediate-output (cmd start end flags)proof-shell-handle-immediate-output
687,23805
(defun proof-interrupt-process ()proof-interrupt-process
754,26412
(defun proof-shell-insert (strings action &optional scriptspan)proof-shell-insert
788,27645
(defun proof-shell-action-list-item (cmd callback &optional flags)proof-shell-action-list-item
839,29471
(defun proof-shell-set-silent (span)proof-shell-set-silent
844,29713
(defun proof-shell-start-silent-item ()proof-shell-start-silent-item
850,29932
(defun proof-shell-clear-silent (span)proof-shell-clear-silent
856,30121
(defun proof-shell-stop-silent-item ()proof-shell-stop-silent-item
862,30343
(defsubst proof-shell-should-be-silent ()proof-shell-should-be-silent
868,30532
(defsubst proof-shell-insert-action-item (item)proof-shell-insert-action-item
879,31042
(defsubst proof-shell-slurp-comments ()proof-shell-slurp-comments
883,31217
(defun proof-add-to-queue (queueitems &optional queuemode)proof-add-to-queue
894,31622
(defun proof-start-queue (start end queueitems &optional queuemode)proof-start-queue
952,33646
(defun proof-extend-queue (end queueitems)proof-extend-queue
964,34041
(defun proof-shell-exec-loop ()proof-shell-exec-loop
983,34660
(defun proof-shell-insert-loopback-cmd  (cmd)proof-shell-insert-loopback-cmd
1051,36963
(defun proof-shell-process-urgent-message (start end)proof-shell-process-urgent-message
1076,38127
(defun proof-shell-process-urgent-message-default (start end)proof-shell-process-urgent-message-default
1125,39847
(defun proof-shell-process-urgent-message-trace (start end)proof-shell-process-urgent-message-trace
1141,40431
(defun proof-shell-process-urgent-message-retract (start end)proof-shell-process-urgent-message-retract
1154,40990
(defun proof-shell-process-urgent-message-elisp ()proof-shell-process-urgent-message-elisp
1175,41838
(defun proof-shell-process-urgent-message-thmdeps ()proof-shell-process-urgent-message-thmdeps
1190,42333
(defun proof-shell-strip-eager-annotations (start end)proof-shell-strip-eager-annotations
1204,42712
(defun proof-shell-filter (str)proof-shell-filter
1220,43212
(defun proof-shell-filter-first-command ()proof-shell-filter-first-command
1320,46584
(defun proof-shell-process-urgent-messages ()proof-shell-process-urgent-messages
1335,47127
(defun proof-shell-filter-manage-output (start end)proof-shell-filter-manage-output
1385,48693
(defsubst proof-shell-display-output-as-response (flags str)proof-shell-display-output-as-response
1417,49940
(defun proof-shell-handle-delayed-output ()proof-shell-handle-delayed-output
1423,50235
(defvar pg-last-tracing-output-time nilpg-last-tracing-output-time
1518,53694
(defconst pg-slow-mode-duration 2pg-slow-mode-duration
1521,53800
(defconst pg-fast-tracing-mode-threshold 50000pg-fast-tracing-mode-threshold
1524,53882
(defvar pg-tracing-cleanup-timer nil)pg-tracing-cleanup-timer
1527,54010
(defun pg-tracing-tight-loop ()pg-tracing-tight-loop
1529,54049
(defun pg-finish-tracing-display ()pg-finish-tracing-display
1572,55761
(defun proof-shell-wait (&optional interrupt-on-input timeoutsecs)proof-shell-wait
1590,56125
(defun proof-done-invisible (span)proof-done-invisible
1620,57336
(defun proof-shell-invisible-command (cmd &optional wait invisiblecallbackproof-shell-invisible-command
1626,57506
(defun proof-shell-invisible-cmd-get-result (cmd)proof-shell-invisible-cmd-get-result
1673,59098
(defun proof-shell-invisible-command-invisible-result (cmd)proof-shell-invisible-command-invisible-result
1685,59534
(defun pg-insert-last-output-as-comment ()pg-insert-last-output-as-comment
1705,60035
(define-derived-mode proof-shell-mode scomint-modeproof-shell-mode
1724,60507
(defconst proof-shell-important-settingsproof-shell-important-settings
1761,61534
(defun proof-shell-config-done ()proof-shell-config-done
1767,61649

generic/proof-site.el,1113
(defconst proof-assistant-table-defaultproof-assistant-table-default
26,771
(defconst proof-general-short-versionproof-general-short-version
59,1766
(defconst proof-general-version-year "2010")proof-general-version-year
65,1953
(defgroup proof-general nilproof-general
72,2106
(defgroup proof-general-internals nilproof-general-internals
77,2214
(defun proof-home-directory-fn ()proof-home-directory-fn
90,2602
(defcustom proof-home-directoryproof-home-directory
101,2974
(defcustom proof-images-directoryproof-images-directory
110,3340
(defcustom proof-info-directoryproof-info-directory
116,3542
(defcustom proof-assistant-tableproof-assistant-table
145,4519
(defcustom proof-assistants nilproof-assistants
182,5687
(defun proof-ready-for-assistant (assistantsym &optional assistant-name)proof-ready-for-assistant
211,6841
(defvar proof-general-configured-provers proof-general-configured-provers
263,9133
(defun proof-chose-prover (prompt)proof-chose-prover
333,11656
(defun proofgeneral (prover)proofgeneral
338,11788
(defun proof-visit-example-file (prover)proof-visit-example-file
347,12106

generic/proof-splash.el,1738
(defcustom proof-splash-enable tproof-splash-enable
34,1007
(defcustom proof-splash-time 8proof-splash-time
39,1159
(defcustom proof-splash-contentsproof-splash-contents
47,1443
(defconst proof-splash-startup-msgproof-splash-startup-msg
91,3008
(defconst proof-splash-welcome "*Proof General Welcome*"proof-splash-welcome
100,3386
(define-derived-mode proof-splash-mode fundamental-modeproof-splash-mode
103,3490
(define-key proof-splash-mode-map "q" 'bury-buffer)proof-splash-mode-map
109,3664
(define-key proof-splash-mode-map [mouse-3] 'bury-buffer)proof-splash-mode-map
110,3716
(defsubst proof-emacs-imagep (img)proof-emacs-imagep
115,3843
(defun proof-get-image (name &optional nojpeg default)proof-get-image
120,3968
(defvar proof-splash-timeout-conf nilproof-splash-timeout-conf
142,4768
(defun proof-splash-centre-spaces (glyph)proof-splash-centre-spaces
145,4881
(defun proof-splash-remove-screen (&optional nothing)proof-splash-remove-screen
172,6037
(defun proof-splash-remove-buffer ()proof-splash-remove-buffer
189,6693
(defvar proof-splash-seen nilproof-splash-seen
200,7081
(defun proof-splash-insert-contents ()proof-splash-insert-contents
203,7183
(defun proof-splash-display-screen (&optional timeout)proof-splash-display-screen
243,8313
(defalias 'pg-about 'proof-splash-display-screen)pg-about
279,9835
(defun proof-splash-message ()proof-splash-message
282,9901
(defun proof-splash-timeout-waiter ()proof-splash-timeout-waiter
295,10345
(defvar proof-splash-old-frame-title-format nil)proof-splash-old-frame-title-format
308,10903
(defun proof-splash-set-frame-titles ()proof-splash-set-frame-titles
310,10953
(defun proof-splash-unset-frame-titles ()proof-splash-unset-frame-titles
319,11268

generic/proof-syntax.el,2484
(defsubst proof-ids-to-regexp (l)proof-ids-to-regexp
22,516
(defsubst proof-anchor-regexp (e)proof-anchor-regexp
29,754
(defconst proof-no-regexp "\\<\\>"proof-no-regexp
33,859
(defsubst proof-regexp-alt (&rest args)proof-regexp-alt
36,950
(defsubst proof-regexp-alt-list (args)proof-regexp-alt-list
45,1262
(defsubst proof-re-search-forward-region (startre endre)proof-re-search-forward-region
49,1397
(defsubst proof-search-forward (string &optional bound noerror count)proof-search-forward
62,1895
(defsubst proof-replace-regexp-in-string (regexp rep string)proof-replace-regexp-in-string
69,2165
(defsubst proof-re-search-forward (regexp &optional bound noerror count)proof-re-search-forward
74,2416
(defsubst proof-re-search-backward (regexp &optional bound noerror count)proof-re-search-backward
79,2674
(defsubst proof-re-search-forward-safe (regexp &optional bound noerror count)proof-re-search-forward-safe
84,2935
(defsubst proof-string-match (regexp string &optional start)proof-string-match
90,3216
(defsubst proof-string-match-safe (regexp string &optional start)proof-string-match-safe
95,3445
(defsubst proof-stringfn-match (regexp-or-fn string)proof-stringfn-match
99,3649
(defsubst proof-looking-at (regexp)proof-looking-at
106,3912
(defsubst proof-looking-at-safe (regexp)proof-looking-at-safe
111,4099
(defun proof-buffer-syntactic-context (&optional buffer)proof-buffer-syntactic-context
120,4312
(defsubst proof-looking-at-syntactic-context-default ()proof-looking-at-syntactic-context-default
141,5174
(defun proof-looking-at-syntactic-context ()proof-looking-at-syntactic-context
150,5529
(defun proof-inside-comment (pos)proof-inside-comment
159,5991
(defun proof-inside-string (pos)proof-inside-string
165,6164
(defsubst proof-replace-string (string to-string)proof-replace-string
175,6363
(defsubst proof-replace-regexp (regexp to-string)proof-replace-regexp
180,6567
(defsubst proof-replace-regexp-nocasefold (regexp to-string)proof-replace-regexp-nocasefold
185,6776
(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)"proof-id
195,7064
(defsubst proof-ids (proof-id &optional sepregexp)proof-ids
201,7284
(defun proof-zap-commas (limit)proof-zap-commas
208,7536
(defadvice font-lock-fontify-keywords-regionfont-lock-fontify-keywords-region
234,8422
(defun proof-format (alist string)proof-format
250,9018
(defun proof-format-filename (string filename)proof-format-filename
269,9657
(defun proof-insert (text)proof-insert
316,11059

generic/proof-toolbar.el,3466
(defun proof-toolbar-function (token)proof-toolbar-function
33,812
(defun proof-toolbar-icon (token)proof-toolbar-icon
37,959
(defun proof-toolbar-enabler (token)proof-toolbar-enabler
41,1106
(defun proof-toolbar-make-icon (tle)proof-toolbar-make-icon
50,1308
(defun proof-toolbar-make-toolbar-items (map tles)proof-toolbar-make-toolbar-items
59,1616
(defvar proof-toolbar-map nilproof-toolbar-map
85,2492
(defun proof-toolbar-available-p ()proof-toolbar-available-p
88,2591
(defun proof-toolbar-setup ()proof-toolbar-setup
98,2897
(defun proof-toolbar-enable ()proof-toolbar-enable
119,3754
(defalias 'proof-toolbar-undo 'proof-undo-last-successful-command)proof-toolbar-undo
152,4812
(defun proof-toolbar-undo-enable-p ()proof-toolbar-undo-enable-p
154,4880
(defalias 'proof-toolbar-delete 'proof-undo-and-delete-last-successful-command)proof-toolbar-delete
161,5038
(defun proof-toolbar-delete-enable-p ()proof-toolbar-delete-enable-p
163,5119
(defalias 'proof-toolbar-home 'proof-goto-end-of-locked)proof-toolbar-home
171,5301
(defalias 'proof-toolbar-next 'proof-assert-next-command-interactive)proof-toolbar-next
175,5368
(defun proof-toolbar-next-enable-p ()proof-toolbar-next-enable-p
177,5439
(defalias 'proof-toolbar-goto 'proof-goto-point)proof-toolbar-goto
183,5555
(defun proof-toolbar-goto-enable-p ()proof-toolbar-goto-enable-p
185,5605
(defalias 'proof-toolbar-retract 'proof-retract-buffer)proof-toolbar-retract
190,5690
(defun proof-toolbar-retract-enable-p ()proof-toolbar-retract-enable-p
192,5747
(defalias 'proof-toolbar-use 'proof-process-buffer)proof-toolbar-use
198,5866
(defalias 'proof-toolbar-use-enable-p 'proof-toolbar-next-enable-p)proof-toolbar-use-enable-p
199,5918
(defalias 'proof-toolbar-restart 'proof-shell-restart)proof-toolbar-restart
203,5999
(defalias 'proof-toolbar-goal 'proof-issue-goal)proof-toolbar-goal
207,6064
(defalias 'proof-toolbar-qed 'proof-issue-save)proof-toolbar-qed
211,6122
(defun proof-toolbar-qed-enable-p ()proof-toolbar-qed-enable-p
213,6171
(defalias 'proof-toolbar-state 'proof-prf)proof-toolbar-state
221,6333
(defalias 'proof-toolbar-state-enable-p 'proof-shell-available-p)proof-toolbar-state-enable-p
222,6376
(defalias 'proof-toolbar-context 'proof-ctxt)proof-toolbar-context
226,6455
(defalias 'proof-toolbar-context-enable-p 'proof-shell-available-p)proof-toolbar-context-enable-p
227,6501
(defalias 'proof-toolbar-command 'proof-minibuffer-cmd)proof-toolbar-command
231,6582
(defalias 'proof-toolbar-command-enable-p 'proof-shell-available-p)proof-toolbar-command-enable-p
232,6638
(defun proof-toolbar-help ()proof-toolbar-help
236,6743
(defalias 'proof-toolbar-find 'proof-find-theorems)proof-toolbar-find
242,6823
(defalias 'proof-toolbar-find-enable-p 'proof-shell-available-p)proof-toolbar-find-enable-p
243,6875
(defalias 'proof-toolbar-info 'proof-query-identifier)proof-toolbar-info
247,6950
(defalias 'proof-toolbar-info-enable-p 'proof-shell-available-p)proof-toolbar-info-enable-p
248,7005
(defalias 'proof-toolbar-visibility 'pg-toggle-visibility)proof-toolbar-visibility
252,7103
(defun proof-toolbar-visibility-enable-p ()proof-toolbar-visibility-enable-p
254,7163
(defalias 'proof-toolbar-interrupt 'proof-interrupt-process)proof-toolbar-interrupt
259,7277
(defun proof-toolbar-interrupt-enable-p () proof-shell-busy)proof-toolbar-interrupt-enable-p
260,7338
(defun proof-toolbar-scripting-menu ()proof-toolbar-scripting-menu
268,7491

generic/proof-unicode-tokens.el,856
(defvar proof-unicode-tokens-initialised nilproof-unicode-tokens-initialised
31,827
(defun proof-unicode-tokens-init ()proof-unicode-tokens-init
34,934
(defun proof-unicode-tokens-configure ()proof-unicode-tokens-configure
48,1436
(defun proof-unicode-tokens-mode-if-enabled ()proof-unicode-tokens-mode-if-enabled
60,1882
(defun proof-unicode-tokens-set-global (flag)proof-unicode-tokens-set-global
66,2081
(defun proof-unicode-tokens-enable ()proof-unicode-tokens-enable
82,2651
(defun proof-unicode-tokens-reconfigure ()proof-unicode-tokens-reconfigure
102,3504
(defun proof-unicode-tokens-configure-prover ()proof-unicode-tokens-configure-prover
128,4392
(defun proof-unicode-tokens-activate-prover ()proof-unicode-tokens-activate-prover
133,4573
(defun proof-unicode-tokens-deactivate-prover ()proof-unicode-tokens-deactivate-prover
140,4819

generic/proof-useropts.el,2510
(defgroup proof-user-options nilproof-user-options
21,564
(defun proof-set-value (sym value)proof-set-value
29,743
(defcustom proof-electric-terminator-enable nilproof-electric-terminator-enable
62,1866
(defcustom proof-toolbar-enable tproof-toolbar-enable
74,2398
(defcustom proof-imenu-enable nilproof-imenu-enable
80,2571
(defcustom pg-show-hints tpg-show-hints
86,2742
(defcustom proof-shell-quiet-errors tproof-shell-quiet-errors
91,2875
(defcustom proof-trace-output-slow-catchup tproof-trace-output-slow-catchup
98,3146
(defcustom proof-strict-state-preserving tproof-strict-state-preserving
108,3643
(defcustom proof-strict-read-only 'retractproof-strict-read-only
121,4252
(defcustom proof-three-window-enable nilproof-three-window-enable
134,4831
(defcustom proof-multiple-frames-enable nilproof-multiple-frames-enable
153,5581
(defcustom proof-delete-empty-windows nilproof-delete-empty-windows
162,5914
(defcustom proof-shrink-windows-tofit nilproof-shrink-windows-tofit
173,6445
(defcustom proof-auto-raise-buffers tproof-auto-raise-buffers
180,6717
(defcustom proof-colour-locked tproof-colour-locked
187,6952
(defcustom proof-sticky-errors nilproof-sticky-errors
195,7202
(defcustom proof-query-file-save-when-activating-scriptingproof-query-file-save-when-activating-scripting
202,7419
(defcustom proof-prog-name-askproof-prog-name-ask
218,8139
(defcustom proof-prog-name-guessproof-prog-name-guess
224,8299
(defcustom proof-tidy-responseproof-tidy-response
232,8564
(defcustom proof-keep-response-historyproof-keep-response-history
246,9027
(defcustom pg-input-ring-size 32pg-input-ring-size
256,9415
(defcustom proof-general-debug nilproof-general-debug
261,9567
(defcustom proof-use-parser-cache tproof-use-parser-cache
270,9938
(defcustom proof-follow-mode 'lockedproof-follow-mode
277,10192
(defcustom proof-auto-action-when-deactivating-scripting nilproof-auto-action-when-deactivating-scripting
301,11369
(defcustom proof-rsh-command nilproof-rsh-command
329,12551
(defcustom proof-disappearing-proofs nilproof-disappearing-proofs
345,13101
(defcustom proof-full-annotation tproof-full-annotation
350,13262
(defcustom proof-minibuffer-messages nilproof-minibuffer-messages
359,13632
(defcustom proof-autosend-enable nilproof-autosend-enable
367,13941
(defcustom proof-autosend-delay 0.8proof-autosend-delay
373,14121
(defcustom proof-autosend-all nilproof-autosend-all
379,14279
(defcustom proof-fast-process-buffer proof-fast-process-buffer
384,14448

generic/proof-utils.el,3227
(defmacro proof-with-current-buffer-if-exists (buf &rest body)proof-with-current-buffer-if-exists
61,1729
(defmacro proof-with-script-buffer (&rest body)proof-with-script-buffer
70,2106
(defmacro proof-map-buffers (buflist &rest body)proof-map-buffers
81,2487
(defmacro proof-sym (string)proof-sym
86,2672
(defsubst proof-try-require (symbol)proof-try-require
91,2833
(defun proof-save-some-buffers (buffers)proof-save-some-buffers
104,3164
(defun proof-save-this-buffer ()proof-save-this-buffer
124,3760
(defun proof-file-truename (filename)proof-file-truename
137,4124
(defun proof-files-to-buffers (filenames)proof-files-to-buffers
141,4306
(defun proof-buffers-in-mode (mode &optional buflist)proof-buffers-in-mode
149,4545
(defun pg-save-from-death ()pg-save-from-death
163,4995
(defun proof-define-keys (map kbl)proof-define-keys
182,5611
(defun pg-remove-specials (&optional start end)pg-remove-specials
193,5896
(defun pg-remove-specials-in-string (string)pg-remove-specials-in-string
203,6232
(defun proof-safe-split-window-vertically ()proof-safe-split-window-vertically
213,6457
(defun proof-warn-if-unset (tag sym)proof-warn-if-unset
218,6637
(defun proof-get-window-for-buffer (buffer)proof-get-window-for-buffer
223,6855
(defun proof-display-and-keep-buffer (buffer &optional pos force)proof-display-and-keep-buffer
272,9165
(defun proof-clean-buffer (buffer)proof-clean-buffer
314,10888
(defun pg-internal-warning (message &rest args)pg-internal-warning
330,11544
(defun proof-debug (msg &rest args)proof-debug
338,11826
(defun proof-switch-to-buffer (buf &optional noselect)proof-switch-to-buffer
353,12370
(defun proof-resize-window-tofit (&optional window)proof-resize-window-tofit
375,13494
(defun proof-submit-bug-report ()proof-submit-bug-report
470,17342
(defun proof-deftoggle-fn (var &optional othername)proof-deftoggle-fn
505,18699
(defmacro proof-deftoggle (var &optional othername)proof-deftoggle
520,19365
(defun proof-defintset-fn (var &optional othername)proof-defintset-fn
531,19878
(defmacro proof-defintset (var &optional othername)proof-defintset
550,20702
(defun proof-deffloatset-fn (var &optional othername)proof-deffloatset-fn
557,21081
(defmacro proof-deffloatset (var &optional othername)proof-deffloatset
573,21795
(defun proof-defstringset-fn (var &optional othername)proof-defstringset-fn
580,22180
(defmacro proof-defstringset (var &optional othername)proof-defstringset
593,22806
(defun proof-escape-keymap-doc (string)proof-escape-keymap-doc
606,23262
(defmacro proof-defshortcut (fn string &optional key)proof-defshortcut
610,23416
(defmacro proof-definvisible (fn string &optional key)proof-definvisible
625,24014
(defun pg-custom-save-vars (&rest variables)pg-custom-save-vars
652,24943
(defun pg-custom-reset-vars (&rest variables)pg-custom-reset-vars
668,25587
(defun proof-locate-executable (progname &optional returnnopath extrapath)proof-locate-executable
681,25924
(defun pg-current-word-pos (&optional strict really-word)pg-current-word-pos
696,26474
(defsubst proof-shell-strip-output-markup (string &optional push)proof-shell-strip-output-markup
741,28129
(defun proof-minibuffer-message (str)proof-minibuffer-message
747,28393

lib/bufhist.el,2047
(defun bufhist-ring-update (ring index newitem)bufhist-ring-update
38,1391
(defgroup bufhist nilbufhist
47,1713
(defcustom bufhist-ring-size 30bufhist-ring-size
51,1794
(defvar bufhist-ring nilbufhist-ring
56,1905
(defvar bufhist-ring-pos nilbufhist-ring-pos
59,1979
(defvar bufhist-lastswitch-modified-tick nilbufhist-lastswitch-modified-tick
62,2058
(defvar bufhist-read-only-history tbufhist-read-only-history
65,2164
(defvar bufhist-saved-mode-line-format nilbufhist-saved-mode-line-format
68,2235
(defvar bufhist-normal-read-only nilbufhist-normal-read-only
71,2338
(defvar bufhist-top-point 0bufhist-top-point
74,2432
(defun bufhist-mode-line-format-entry ()bufhist-mode-line-format-entry
77,2522
(defconst bufhist-minor-mode-mapbufhist-minor-mode-map
106,3596
(define-minor-mode bufhist-modebufhist-mode
119,4073
(defun bufhist-get-buffer-contents ()bufhist-get-buffer-contents
141,4954
(defun bufhist-restore-buffer-contents (buf)bufhist-restore-buffer-contents
150,5296
(defun bufhist-checkpoint ()bufhist-checkpoint
159,5610
(defun bufhist-erase-buffer ()bufhist-erase-buffer
167,5979
(defun bufhist-checkpoint-and-erase ()bufhist-checkpoint-and-erase
178,6350
(defun bufhist-switch-to-index (n &optional nosave browsing)bufhist-switch-to-index
184,6536
(defun bufhist-first ()bufhist-first
223,8135
(defun bufhist-last ()bufhist-last
228,8294
(defun bufhist-prev (&optional n)bufhist-prev
233,8438
(defun bufhist-next (&optional n)bufhist-next
241,8661
(defun bufhist-delete ()bufhist-delete
246,8801
(defun bufhist-clear ()bufhist-clear
258,9342
(defun bufhist-init (&optional readwrite ringsize)bufhist-init
273,9737
(defun bufhist-exit ()bufhist-exit
301,10746
(defun bufhist-set-readwrite (readwrite)bufhist-set-readwrite
311,11010
(defun bufhist-before-change-function (&rest args)bufhist-before-change-function
326,11630
(define-button-type 'bufhist-nextbufhist-next
340,12053
(define-button-type 'bufhist-prevbufhist-prev
344,12150
(defun bufhist-insert-buttons ()bufhist-insert-buttons
351,12362

lib/holes.el,4313
(defvar holes-default-hole holes-default-hole
44,1121
(defvar holes-active-hole holes-default-holeholes-active-hole
50,1299
(defgroup holes nilholes
60,1496
(defcustom holes-empty-hole-string "#"holes-empty-hole-string
65,1595
(defcustom holes-empty-hole-regexp "#\\|@{\\([^{}]*\\)}"holes-empty-hole-regexp
70,1738
(defface active-hole-faceactive-hole-face
92,2440
(defface inactive-hole-faceinactive-hole-face
102,2856
(defvar hole-maphole-map
116,3297
(defvar holes-mode-mapholes-mode-map
126,3688
(defun holes-region-beginning-or-nil ()holes-region-beginning-or-nil
172,5425
(defun holes-region-end-or-nil ()holes-region-end-or-nil
176,5561
(defun holes-copy-active-region ()holes-copy-active-region
180,5679
(defun holes-is-hole-p (span)holes-is-hole-p
186,5889
(defun holes-hole-start-position (hole)holes-hole-start-position
190,5981
(defun holes-hole-end-position (hole)holes-hole-end-position
196,6164
(defun holes-hole-buffer (hole)holes-hole-buffer
201,6335
(defun holes-hole-at (&optional pos)holes-hole-at
207,6509
(defun holes-active-hole-exist-p ()holes-active-hole-exist-p
212,6679
(defun holes-active-hole-start-position ()holes-active-hole-start-position
219,6932
(defun holes-active-hole-end-position ()holes-active-hole-end-position
227,7300
(defun holes-active-hole-buffer ()holes-active-hole-buffer
236,7663
(defun holes-goto-active-hole ()holes-goto-active-hole
244,7964
(defun holes-highlight-hole-as-active (hole)holes-highlight-hole-as-active
253,8223
(defun holes-highlight-hole (hole)holes-highlight-hole
261,8531
(defun holes-disable-active-hole ()holes-disable-active-hole
269,8818
(defun holes-set-active-hole (hole)holes-set-active-hole
282,9350
(defun holes-is-in-hole-p (&optional pos)holes-is-in-hole-p
292,9695
(defun holes-make-hole (start end)holes-make-hole
296,9833
(defun holes-make-hole-at (&optional start end)holes-make-hole-at
314,10489
(defun holes-clear-hole (hole)holes-clear-hole
328,10942
(defun holes-clear-hole-at (&optional pos)holes-clear-hole-at
337,11200
(defun holes-map-holes (function &optional object from to)holes-map-holes
345,11456
(defun holes-clear-all-buffer-holes (&optional start end)holes-clear-all-buffer-holes
349,11610
(defun holes-next (pos buffer)holes-next
359,11911
(defun holes-next-after-active-hole ()holes-next-after-active-hole
366,12163
(defun holes-set-active-hole-next (&optional buffer pos)holes-set-active-hole-next
373,12379
(defun holes-replace-segment (start end str &optional buffer)holes-replace-segment
392,12916
(defun holes-replace (str &optional thehole)holes-replace
401,13269
(defun holes-replace-active-hole (&optional str)holes-replace-active-hole
429,14447
(defun holes-replace-update-active-hole (&optional str)holes-replace-update-active-hole
436,14738
(defun holes-delete-update-active-hole ()holes-delete-update-active-hole
454,15385
(defun holes-set-make-active-hole (&optional start end)holes-set-make-active-hole
462,15612
(defalias 'holes-track-mouse-selection 'mouse-drag-track)holes-track-mouse-selection
477,16167
(defsubst holes-track-mouse-clicks ()holes-track-mouse-clicks
478,16225
(defun holes-mouse-replace-active-hole (event)holes-mouse-replace-active-hole
482,16335
(defun holes-destroy-hole (&optional span)holes-destroy-hole
496,16806
(defsubst holes-hole-at-event (event)holes-hole-at-event
510,17188
(defun holes-mouse-destroy-hole (event)holes-mouse-destroy-hole
514,17288
(defun holes-mouse-forget-hole (event)holes-mouse-forget-hole
521,17509
(defun holes-mouse-set-make-active-hole (event)holes-mouse-set-make-active-hole
531,17801
(defun holes-mouse-set-active-hole (event)holes-mouse-set-active-hole
547,18300
(defun holes-set-point-next-hole-destroy ()holes-set-point-next-hole-destroy
556,18551
(defun holes-replace-string-by-holes-backward (limit)holes-replace-string-by-holes-backward
582,19532
(defun holes-skeleton-end-hook ()holes-skeleton-end-hook
600,20232
(defconst holes-jump-docholes-jump-doc
609,20670
(defun holes-replace-string-by-holes-backward-jump (pos &optional noindent)holes-replace-string-by-holes-backward-jump
616,20876
(define-minor-mode holes-mode holes-mode
633,21558
(defun holes-abbrev-complete ()holes-abbrev-complete
728,25040
(defun holes-insert-and-expand (s)holes-insert-and-expand
738,25383

lib/local-vars-list.el,665
(defconst local-vars-list-doc nillocal-vars-list-doc
28,825
(defun local-vars-list-insert-empty-zone ()local-vars-list-insert-empty-zone
44,1387
(defun local-vars-list-find ()local-vars-list-find
82,2090
(defun local-vars-list-goto-var (symb lpat rpat)local-vars-list-goto-var
101,2861
(defun local-vars-list-get-current (lpat rpat)local-vars-list-get-current
127,3908
(defun local-vars-list-set-current (val lpat rpat)local-vars-list-set-current
148,4758
(defun local-vars-list-get (symb)local-vars-list-get
171,5473
(defun local-vars-list-get-safe (symb)local-vars-list-get-safe
188,6003
(defun local-vars-list-set (symb val)local-vars-list-set
193,6197

lib/maths-menu.el,425
(defvar maths-menu-filter-predicate '(lambda (char) t)maths-menu-filter-predicate
56,2317
(defvar maths-menu-tokenise-insert '(lambda (char) (insert char))maths-menu-tokenise-insert
59,2426
(defun maths-menu-build-menu (spec)maths-menu-build-menu
62,2563
(defvar maths-menu-menumaths-menu-menu
84,3324
(defvar maths-menu-mode-mapmaths-menu-mode-map
344,12882
(define-minor-mode maths-menu-modemaths-menu-mode
352,13101

lib/pg-dev.el,319
(defconst pg-dev-lisp-font-lock-keywordspg-dev-lisp-font-lock-keywords
52,1587
(defun pg-loadpath ()pg-loadpath
78,2286
(defun unload-pg ()unload-pg
88,2457
(defun profile-pg ()profile-pg
119,3351
(defun elp-pack-number (number width)elp-pack-number
148,4378
(defun pg-bug-references ()pg-bug-references
157,4578

lib/pg-fontsets.el,352
(defcustom pg-fontsets-default-fontset nilpg-fontsets-default-fontset
24,722
(defvar pg-fontsets-names nilpg-fontsets-names
29,868
(defun pg-fontsets-make-fontsetsizes (basefont)pg-fontsets-make-fontsetsizes
32,949
(defconst pg-fontsets-base-fontspg-fontsets-base-fonts
51,1710
(defun pg-fontsets-make-fontsets ()pg-fontsets-make-fontsets
57,1840

lib/proof-compat.el,326
(defvar proof-running-on-win32 (memq system-type '(win32 windows-nt cygwin))proof-running-on-win32
32,980
(defun pg-custom-undeclare-variable (symbol)pg-custom-undeclare-variable
53,1782
(defmacro save-selected-frame (&rest body)save-selected-frame
85,2553
(defmacro declare-function (&rest args)declare-function
151,4561

lib/scomint.el,1525
(defvar scomint-buffer-maximum-size 800000scomint-buffer-maximum-size
19,493
(defvar scomint-output-filter-functions nilscomint-output-filter-functions
24,684
(defvar scomint-mode-mapscomint-mode-map
27,794
(defvar scomint-last-input-start nil)scomint-last-input-start
33,973
(defvar scomint-last-input-end nil)scomint-last-input-end
34,1011
(defvar scomint-last-output-start nil)scomint-last-output-start
35,1047
(defvar scomint-exec-hook nilscomint-exec-hook
37,1087
(define-derived-mode scomint-mode fundamental-mode "SComint"scomint-mode
46,1430
(defsubst scomint-check-proc (buffer)scomint-check-proc
65,2345
(defun scomint-make-in-buffer (name buffer program &optional startfile &rest switches)scomint-make-in-buffer
73,2685
(defun scomint-make (name program &optional startfile &rest switches)scomint-make
97,3952
(defun scomint-exec (buffer name command startfile switches)scomint-exec
110,4663
(defun scomint-exec-1 (name buffer command switches)scomint-exec-1
147,6256
(defalias 'scomint-send-string 'process-send-string)scomint-send-string
197,8386
(defun scomint-send-eof ()scomint-send-eof
199,8440
(defun scomint-send-input (&optional no-newline artificial)scomint-send-input
208,8673
(defun scomint-truncate-buffer (&optional string)scomint-truncate-buffer
234,9569
(defun scomint-strip-ctrl-m (&optional string)scomint-strip-ctrl-m
247,9963
(defun scomint-output-filter (process string)scomint-output-filter
261,10526
(defun scomint-interrupt-process ()scomint-interrupt-process
284,11281

lib/span.el,2711
(defalias 'span-start 'overlay-start)span-start
22,611
(defalias 'span-end 'overlay-end)span-end
23,649
(defalias 'span-set-property 'overlay-put)span-set-property
24,683
(defalias 'span-property 'overlay-get)span-property
25,726
(defalias 'span-make 'make-overlay)span-make
26,765
(defalias 'span-detach 'delete-overlay)span-detach
27,801
(defalias 'span-set-endpoints 'move-overlay)span-set-endpoints
28,841
(defalias 'span-buffer 'overlay-buffer)span-buffer
29,886
(defun span-read-only-hook (overlay after start end &optional len)span-read-only-hook
31,927
(defsubst span-read-only (span)span-read-only
36,1117
(defsubst span-read-write (span)span-read-write
43,1427
(defsubst span-write-warning (span fun)span-write-warning
48,1597
(defsubst span-lt (s u)span-lt
59,2121
(defsubst spans-at-point-prop (pt prop)spans-at-point-prop
64,2265
(defsubst spans-at-region-prop (start end prop)spans-at-region-prop
73,2456
(defsubst span-at (pt prop)span-at
83,2722
(defsubst span-delete (span)span-delete
87,2848
(defsubst span-add-delete-action (span action)span-add-delete-action
93,3044
(defsubst span-mapcar-spans (fn start end prop)span-mapcar-spans
99,3323
(defsubst span-mapc-spans (fn start end prop)span-mapc-spans
103,3498
(defsubst span-mapcar-spans-inorder (fn start end prop)span-mapcar-spans-inorder
107,3669
(defun span-at-before (pt prop)span-at-before
113,3874
(defsubst prev-span (span prop)prev-span
130,4598
(defsubst next-span (span prop)next-span
136,4751
(defsubst span-live-p (span)span-live-p
142,4965
(defsubst span-raise (span)span-raise
148,5131
(defsubst span-string (span)span-string
152,5264
(defsubst set-span-properties (span plist)set-span-properties
157,5424
(defsubst span-find-span (overlay-list &optional prop)span-find-span
163,5618
(defsubst span-at-event (event &optional prop)span-at-event
171,5930
(defun fold-spans (f &optional buffer from to maparg ignored-flags prop val)fold-spans
177,6127
(defsubst span-detached-p (span)span-detached-p
191,6660
(defsubst set-span-face (span face)set-span-face
195,6776
(defsubst set-span-keymap (span map)set-span-keymap
199,6874
(defsubst span-delete-spans (start end prop)span-delete-spans
207,7043
(defsubst span-property-safe (span name)span-property-safe
211,7205
(defsubst span-set-start (span value)span-set-start
215,7342
(defsubst span-set-end (span value)span-set-end
219,7474
(defun span-make-self-removing-span (beg end &rest props)span-make-self-removing-span
227,7634
(defun span-delete-self-modification-hook (span &rest args)span-delete-self-modification-hook
237,8002
(defun span-make-modifying-removing-span (beg end &rest props)span-make-modifying-removing-span
242,8176

lib/texi-docstring-magic.el,1112
(defun texi-docstring-magic-find-face (face)texi-docstring-magic-find-face
88,3027
(defun texi-docstring-magic-splice-sep (strings sep)texi-docstring-magic-splice-sep
93,3192
(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table
103,3497
(defun texi-docstring-magic-untabify (string)texi-docstring-magic-untabify
193,7260
(defun texi-docstring-magic-munge-docstring (docstring args)texi-docstring-magic-munge-docstring
200,7458
(defun texi-docstring-magic-texi (env grp name docstring args &optional endtext)texi-docstring-magic-texi
239,8739
(defun texi-docstring-magic-format-default (default)texi-docstring-magic-format-default
252,9179
(defun texi-docstring-magic-texi-for (symbol &optional noerror)texi-docstring-magic-texi-for
268,9812
(defconst texi-docstring-magic-commenttexi-docstring-magic-comment
326,11771
(defun texi-docstring-magic (&optional noerror)texi-docstring-magic
332,11925
(defun texi-docstring-magic-face-at-point ()texi-docstring-magic-face-at-point
366,13004
(defun texi-docstring-magic-insert-magic (symbol)texi-docstring-magic-insert-magic
381,13527

lib/unicode-chars.el,127
(defvar unicode-chars-alistunicode-chars-alist
12,348
(defun unicode-chars-list-chars ()unicode-chars-list-chars
5051,245975

lib/unicode-tokens.el,9990
(defgroup unicode-tokens-options nilunicode-tokens-options
55,1711
(defcustom unicode-tokens-add-help-echo tunicode-tokens-add-help-echo
60,1836
(defun unicode-tokens-toggle-add-help-echo ()unicode-tokens-toggle-add-help-echo
65,2003
(defvar unicode-tokens-token-symbol-map nilunicode-tokens-token-symbol-map
79,2409
(defvar unicode-tokens-token-format "%s"unicode-tokens-token-format
98,3068
(defvar unicode-tokens-token-variant-format-regexp nilunicode-tokens-token-variant-format-regexp
104,3317
(defvar unicode-tokens-shortcut-alist nilunicode-tokens-shortcut-alist
118,3850
(defvar unicode-tokens-shortcut-replacement-alist nilunicode-tokens-shortcut-replacement-alist
124,4127
(defvar unicode-tokens-control-region-format-regexp nilunicode-tokens-control-region-format-regexp
132,4333
(defvar unicode-tokens-control-char-format-regexp nilunicode-tokens-control-char-format-regexp
139,4701
(defvar unicode-tokens-control-regions nilunicode-tokens-control-regions
146,5062
(defvar unicode-tokens-control-characters nilunicode-tokens-control-characters
149,5138
(defvar unicode-tokens-control-char-format nilunicode-tokens-control-char-format
152,5220
(defvar unicode-tokens-control-region-format-start nilunicode-tokens-control-region-format-start
155,5333
(defvar unicode-tokens-control-region-format-end nilunicode-tokens-control-region-format-end
158,5450
(defvar unicode-tokens-tokens-customizable-variables nilunicode-tokens-tokens-customizable-variables
161,5563
(defconst unicode-tokens-configuration-variablesunicode-tokens-configuration-variables
168,5731
(defun unicode-tokens-config (sym)unicode-tokens-config
183,6130
(defun unicode-tokens-config-var (sym)unicode-tokens-config-var
187,6275
(defun unicode-tokens-copy-configuration-variables ()unicode-tokens-copy-configuration-variables
199,6715
(defvar unicode-tokens-token-list nilunicode-tokens-token-list
227,7931
(defvar unicode-tokens-hash-table nilunicode-tokens-hash-table
230,8051
(defvar unicode-tokens-token-match-regexp nilunicode-tokens-token-match-regexp
233,8167
(defvar unicode-tokens-uchar-hash-table nilunicode-tokens-uchar-hash-table
239,8450
(defvar unicode-tokens-uchar-regexp nilunicode-tokens-uchar-regexp
243,8637
(defgroup unicode-tokens-faces nilunicode-tokens-faces
251,8822
(defconst unicode-tokens-font-family-alternativesunicode-tokens-font-family-alternatives
261,9119
(defface unicode-tokens-symbol-font-faceunicode-tokens-symbol-font-face
276,9616
(defface unicode-tokens-script-font-faceunicode-tokens-script-font-face
286,9974
(defface unicode-tokens-fraktur-font-faceunicode-tokens-fraktur-font-face
291,10118
(defface unicode-tokens-serif-font-faceunicode-tokens-serif-font-face
296,10243
(defface unicode-tokens-sans-font-faceunicode-tokens-sans-font-face
301,10380
(defface unicode-tokens-highlight-faceunicode-tokens-highlight-face
306,10502
(defconst unicode-tokens-fontsunicode-tokens-fonts
315,10864
(defconst unicode-tokens-fontsymb-propertiesunicode-tokens-fontsymb-properties
324,11081
(define-widget 'unicode-tokens-token-symbol-map 'lazyunicode-tokens-token-symbol-map
352,12697
(define-widget 'unicode-tokens-shortcut-alist 'lazyunicode-tokens-shortcut-alist
370,13249
(defconst unicode-tokens-font-lock-extra-managed-propsunicode-tokens-font-lock-extra-managed-props
383,13580
(defun unicode-tokens-font-lock-keywords ()unicode-tokens-font-lock-keywords
387,13734
(defun unicode-tokens-calculate-token-match (toks)unicode-tokens-calculate-token-match
420,15105
(defun unicode-tokens-usable-composition (comp)unicode-tokens-usable-composition
450,16141
(defun unicode-tokens-help-echo ()unicode-tokens-help-echo
463,16520
(defvar unicode-tokens-show-symbols nilunicode-tokens-show-symbols
468,16722
(defun unicode-tokens-interpret-composition (comp)unicode-tokens-interpret-composition
471,16836
(defun unicode-tokens-font-lock-compose-symbol (match)unicode-tokens-font-lock-compose-symbol
489,17348
(defun unicode-tokens-prepend-text-properties-in-match (props matchno)unicode-tokens-prepend-text-properties-in-match
527,18880
(defun unicode-tokens-prepend-text-property (start end prop value &optional object)unicode-tokens-prepend-text-property
541,19458
(defun unicode-tokens-show-symbols (&optional arg)unicode-tokens-show-symbols
566,20603
(defun unicode-tokens-symbs-to-props (symbs &optional facenil)unicode-tokens-symbs-to-props
574,20913
(defvar unicode-tokens-show-controls nilunicode-tokens-show-controls
594,21612
(defun unicode-tokens-show-controls (&optional arg)unicode-tokens-show-controls
597,21703
(defun unicode-tokens-control-char (name s &rest props)unicode-tokens-control-char
609,22216
(defun unicode-tokens-control-region (name start end &rest props)unicode-tokens-control-region
618,22655
(defun unicode-tokens-control-font-lock-keywords ()unicode-tokens-control-font-lock-keywords
629,23202
(defvar unicode-tokens-use-shortcuts tunicode-tokens-use-shortcuts
640,23526
(defun unicode-tokens-use-shortcuts (&optional arg)unicode-tokens-use-shortcuts
643,23629
(defun unicode-tokens-map-ordering (s1 s2)unicode-tokens-map-ordering
659,24225
(defun unicode-tokens-quail-define-rules ()unicode-tokens-quail-define-rules
668,24578
(defun unicode-tokens-insert-token (tok)unicode-tokens-insert-token
691,25255
(defun unicode-tokens-annotate-region (name)unicode-tokens-annotate-region
700,25559
(defun unicode-tokens-insert-control (name)unicode-tokens-insert-control
724,26397
(defun unicode-tokens-insert-uchar-as-token (char)unicode-tokens-insert-uchar-as-token
734,26846
(defun unicode-tokens-delete-token-near-point ()unicode-tokens-delete-token-near-point
740,27067
(defun unicode-tokens-delete-backward-char (&optional arg)unicode-tokens-delete-backward-char
752,27508
(defun unicode-tokens-delete-char (&optional arg)unicode-tokens-delete-char
763,27889
(defun unicode-tokens-delete-backward-1 ()unicode-tokens-delete-backward-1
774,28243
(defun unicode-tokens-delete-1 ()unicode-tokens-delete-1
791,28839
(defun unicode-tokens-prev-token ()unicode-tokens-prev-token
807,29383
(defun unicode-tokens-rotate-token-forward (&optional n)unicode-tokens-rotate-token-forward
815,29680
(defun unicode-tokens-rotate-token-backward (&optional n)unicode-tokens-rotate-token-backward
842,30570
(defun unicode-tokens-replace-shortcut-match (&rest ignore)unicode-tokens-replace-shortcut-match
847,30772
(defun unicode-tokens-replace-shortcuts ()unicode-tokens-replace-shortcuts
856,31142
(defun unicode-tokens-replace-unicode-match (&rest ignore)unicode-tokens-replace-unicode-match
870,31740
(defun unicode-tokens-replace-unicode ()unicode-tokens-replace-unicode
877,32041
(defun unicode-tokens-copy-token (tokname)unicode-tokens-copy-token
894,32640
(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32861
(defun unicode-tokens-list-tokens ()unicode-tokens-list-tokens
907,33065
(defun unicode-tokens-list-shortcuts ()unicode-tokens-list-shortcuts
946,34249
(defalias 'unicode-tokens-list-unicode-chars 'unicode-chars-list-chars)unicode-tokens-list-unicode-chars
964,34887
(defun unicode-tokens-encode-in-temp-buffer (str fn)unicode-tokens-encode-in-temp-buffer
966,34960
(defun unicode-tokens-encode (beg end)unicode-tokens-encode
984,35616
(defun unicode-tokens-encode-str (str)unicode-tokens-encode-str
990,35852
(defun unicode-tokens-copy (beg end)unicode-tokens-copy
994,36014
(defun unicode-tokens-paste ()unicode-tokens-paste
1003,36420
(defvar unicode-tokens-highlight-unicode nilunicode-tokens-highlight-unicode
1022,37141
(defconst unicode-tokens-unicode-highlight-patternsunicode-tokens-unicode-highlight-patterns
1025,37233
(defun unicode-tokens-highlight-unicode ()unicode-tokens-highlight-unicode
1029,37402
(defun unicode-tokens-highlight-unicode-setkeywords ()unicode-tokens-highlight-unicode-setkeywords
1041,37865
(defun unicode-tokens-initialise ()unicode-tokens-initialise
1053,38234
(defvar unicode-tokens-mode-map (make-sparse-keymap)unicode-tokens-mode-map
1073,38905
(defvar unicode-tokens-display-tableunicode-tokens-display-table
1076,39002
(define-minor-mode unicode-tokens-modeunicode-tokens-mode
1083,39253
(defun unicode-tokens-set-font-var (fontvar)unicode-tokens-set-font-var
1219,43828
(defun unicode-tokens-set-font-var-aux (fontvar font)unicode-tokens-set-font-var-aux
1235,44317
(defun unicode-tokens-mouse-set-font ()unicode-tokens-mouse-set-font
1266,45478
(defsubst unicode-tokens-face-font-sym (fontsym)unicode-tokens-face-font-sym
1279,45992
(defun unicode-tokens-set-font-restart (fontsym)unicode-tokens-set-font-restart
1283,46172
(defun unicode-tokens-save-fonts ()unicode-tokens-save-fonts
1294,46482
(defun unicode-tokens-custom-save-faces (&rest faces)unicode-tokens-custom-save-faces
1302,46738
(define-key unicode-tokens-mode-mapunicode-tokens-mode-map
1319,47194
(define-key unicode-tokens-mode-mapunicode-tokens-mode-map
1322,47301
(defvar unicode-tokens-quail-translation-keymapunicode-tokens-quail-translation-keymap
1326,47391
(define-key unicode-tokens-quail-translation-keymapunicode-tokens-quail-translation-keymap
1333,47581
(defun unicode-tokens-quail-delete-last-char ()unicode-tokens-quail-delete-last-char
1337,47715
(define-key unicode-tokens-mode-map [(control ?,)]unicode-tokens-mode-map
1352,48142
(define-key unicode-tokens-mode-map [(control ?.)]unicode-tokens-mode-map
1354,48234
(define-key unicode-tokens-mode-mapunicode-tokens-mode-map
1356,48325
(define-key unicode-tokens-mode-mapunicode-tokens-mode-map
1358,48431
(define-key unicode-tokens-mode-mapunicode-tokens-mode-map
1361,48546
(define-key unicode-tokens-mode-mapunicode-tokens-mode-map
1363,48655
(define-key unicode-tokens-mode-mapunicode-tokens-mode-map
1365,48763
(define-key unicode-tokens-mode-mapunicode-tokens-mode-map
1367,48869
(defun unicode-tokens-customize-submenu ()unicode-tokens-customize-submenu
1375,48993
(defun unicode-tokens-define-menu ()unicode-tokens-define-menu
1382,49216

contrib/mmm/mmm-auto.el,563
(defvar mmm-autoloaded-classesmmm-autoloaded-classes
67,2676
(defun mmm-autoload-class (class file &optional private)mmm-autoload-class
89,3439
(defvar mmm-changed-buffers-list ()mmm-changed-buffers-list
129,4992
(defun mmm-major-mode-change ()mmm-major-mode-change
132,5099
(defun mmm-check-changed-buffers ()mmm-check-changed-buffers
145,5620
(defun mmm-mode-on-maybe ()mmm-mode-on-maybe
154,5970
(defalias 'mmm-add-find-file-hooks 'mmm-add-find-file-hook)mmm-add-find-file-hooks
166,6374
(defun mmm-add-find-file-hook ()mmm-add-find-file-hook
167,6434

contrib/mmm/mmm-class.el,773
(defun mmm-get-class-spec (class)mmm-get-class-spec
42,1296
(defun mmm-get-class-parameter (class param)mmm-get-class-parameter
59,1939
(defun mmm-set-class-parameter (class param value)mmm-set-class-parameter
63,2105
(defun* mmm-apply-classmmm-apply-class
75,2455
(defun* mmm-apply-classesmmm-apply-classes
90,3072
(defun* mmm-apply-all (&key (start (point-min)) (stop (point-max)))mmm-apply-all
110,3803
(defun* mmm-ifymmm-ify
124,4250
(defun* mmm-match-regionmmm-match-region
206,7095
(defun mmm-match->point (beginp offset match)mmm-match->point
269,9480
(defun mmm-match-and-verify (pos start stop &optional verify)mmm-match-and-verify
284,10050
(defun mmm-get-form (form)mmm-get-form
310,11101
(defun mmm-default-get-form ()mmm-default-get-form
321,11576

contrib/mmm/mmm-cmds.el,1292
(defun mmm-ify-by-class (class)mmm-ify-by-class
41,1210
(defun mmm-ify-region (submode front back)mmm-ify-region
63,1822
(defun mmm-ify-by-regexpmmm-ify-by-regexp
75,2243
(defun mmm-parse-buffer ()mmm-parse-buffer
97,2886
(defun mmm-parse-region (start stop)mmm-parse-region
106,3222
(defun mmm-parse-block (&optional lines)mmm-parse-block
115,3601
(defun mmm-get-block (lines)mmm-get-block
132,4352
(defun mmm-reparse-current-region ()mmm-reparse-current-region
146,4634
(defun mmm-clear-current-region ()mmm-clear-current-region
167,5210
(defun mmm-clear-regions (start stop)mmm-clear-regions
172,5374
(defun mmm-clear-all-regions ()mmm-clear-all-regions
177,5520
(defun* mmm-end-current-region (&optional arg)mmm-end-current-region
185,5680
(defun mmm-narrow-to-submode-region (&optional pos)mmm-narrow-to-submode-region
220,6928
(defun mmm-insert-region (arg)mmm-insert-region
239,7542
(defun mmm-insert-by-key (key &optional arg)mmm-insert-by-key
258,8348
(defun mmm-get-insertion-spec (key &optional classlist)mmm-get-insertion-spec
342,11613
(defun mmm-insertion-help ()mmm-insertion-help
369,12573
(defun mmm-display-insertion-key (spec)mmm-display-insertion-key
379,12936
(defun mmm-get-all-insertion-keys (&optional classlist)mmm-get-all-insertion-keys
401,13723

contrib/mmm/mmm-compat.el,739
(defvar mmm-xemacs (featurep 'xemacs)mmm-xemacs
40,1313
(defvar mmm-keywords-usedmmm-keywords-used
49,1616
(defmacro mmm-regexp-opt (strings paren)mmm-regexp-opt
91,2632
(defvar mmm-evaporate-propertymmm-evaporate-property
110,3281
(defmacro mmm-set-keymap-default (keymap binding)mmm-set-keymap-default
128,4047
(defmacro mmm-event-key (event)mmm-event-key
137,4489
(defvar skeleton-positions ())skeleton-positions
146,4708
(defun mmm-fixup-skeleton ()mmm-fixup-skeleton
147,4739
(defmacro mmm-make-temp-buffer (buffer name)mmm-make-temp-buffer
159,5162
(defvar mmm-font-lock-available-p (or window-system mmm-xemacs)mmm-font-lock-available-p
172,5558
(defmacro mmm-set-font-lock-defaults ()mmm-set-font-lock-defaults
179,5772

contrib/mmm/mmm-cweb.el,367
(defvar mmm-cweb-section-tagsmmm-cweb-section-tags
38,1117
(defvar mmm-cweb-section-regexpmmm-cweb-section-regexp
41,1164
(defvar mmm-cweb-c-part-tagsmmm-cweb-c-part-tags
44,1254
(defvar mmm-cweb-c-part-regexpmmm-cweb-c-part-regexp
47,1313
(defun mmm-cweb-in-limbo (pos)mmm-cweb-in-limbo
50,1397
(defun mmm-cweb-verify-brief-c ()mmm-cweb-verify-brief-c
57,1622

contrib/mmm/mmm-mason.el,665
(defvar mmm-mason-perl-tagsmmm-mason-perl-tags
41,1236
(defvar mmm-mason-pseudo-perl-tagsmmm-mason-pseudo-perl-tags
45,1377
(defvar mmm-mason-non-perl-tagsmmm-mason-non-perl-tags
48,1453
(defvar mmm-mason-perl-tags-regexpmmm-mason-perl-tags-regexp
51,1554
(defvar mmm-mason-pseudo-perl-tags-regexpmmm-mason-pseudo-perl-tags-regexp
56,1749
(defvar mmm-mason-tag-names-regexpmmm-mason-tag-names-regexp
61,1966
(defun mmm-mason-verify-inline ()mmm-mason-verify-inline
66,2186
(defun mmm-mason-start-line ()mmm-mason-start-line
156,4838
(defun mmm-mason-end-line ()mmm-mason-end-line
161,4903
(defun mmm-mason-set-mode-line ()mmm-mason-set-mode-line
168,4997

contrib/mmm/mmm-mode.el,1961
(defun mmm-mode (&optional arg)mmm-mode
101,3867
(defun mmm-mode-on ()mmm-mode-on
140,5372
(defun mmm-mode-off ()mmm-mode-off
181,7048
(defvar mmm-mode-map (make-sparse-keymap)mmm-mode-map
206,7760
(defvar mmm-mode-prefix-map (make-sparse-keymap)mmm-mode-prefix-map
209,7835
(defvar mmm-mode-menu-map (make-sparse-keymap "MMM")mmm-mode-menu-map
212,7945
(defun mmm-define-key (key binding &optional keymap)mmm-define-key
215,8036
(define-key mmm-mode-prefix-map [?h] 'mmm-insertion-help)mmm-mode-prefix-map
239,8791
(define-key mmm-mode-prefix-map (vector help-char) prefix-help-command)mmm-mode-prefix-map
246,9049
(define-key mmm-mode-map mmm-mode-prefix-key mmm-mode-prefix-map)mmm-mode-map
249,9160
(define-key mmm-mode-menu-map [off]mmm-mode-menu-map
252,9262
(define-key mmm-mode-menu-map [sep0] '(menu-item "----"))mmm-mode-menu-map
254,9334
(define-key mmm-mode-menu-map [clhist]mmm-mode-menu-map
256,9393
(define-key mmm-mode-menu-map [end]mmm-mode-menu-map
258,9474
(define-key mmm-mode-menu-map [clear]mmm-mode-menu-map
260,9555
(define-key mmm-mode-menu-map [reparse]mmm-mode-menu-map
262,9642
(define-key mmm-mode-menu-map [sep10] '(menu-item "----"))mmm-mode-menu-map
265,9736
(define-key mmm-mode-menu-map [ins-help]mmm-mode-menu-map
267,9796
(define-key mmm-mode-menu-map [sep20] '(menu-item "----"))mmm-mode-menu-map
270,9887
(define-key mmm-mode-menu-map [region]mmm-mode-menu-map
272,9947
(define-key mmm-mode-menu-map [regexp]mmm-mode-menu-map
274,10054
(define-key mmm-mode-menu-map [class]mmm-mode-menu-map
276,10139
(define-key mmm-mode-menu-map [sep30] '(menu-item "----"))mmm-mode-menu-map
279,10225
(define-key mmm-mode-menu-map [parse-region]mmm-mode-menu-map
281,10285
(define-key mmm-mode-menu-map [parse-buffer]mmm-mode-menu-map
283,10398
(define-key mmm-mode-menu-map [parse-block]mmm-mode-menu-map
285,10483
(define-key mmm-mode-map [menu-bar mmm] (cons "MMM" mmm-mode-menu-map))mmm-mode-map
288,10566

contrib/mmm/mmm-region.el,3064
(defsubst mmm-overlay-at (&optional pos type)mmm-overlay-at
54,1749
(defun mmm-overlays-at (&optional pos type)mmm-overlays-at
59,1934
(defun mmm-included-p (ovl pos &optional type)mmm-included-p
72,2387
(defun mmm-overlays-containing (start stop)mmm-overlays-containing
112,3876
(defun mmm-overlays-contained-in (start stop)mmm-overlays-contained-in
125,4314
(defun mmm-overlays-overlapping (start stop)mmm-overlays-overlapping
138,4754
(defun mmm-sort-overlays (overlays)mmm-sort-overlays
149,5117
(defvar mmm-current-overlay nilmmm-current-overlay
158,5359
(defvar mmm-previous-overlay nilmmm-previous-overlay
163,5574
(defvar mmm-current-submode nilmmm-current-submode
168,5762
(defvar mmm-previous-submode nilmmm-previous-submode
173,5962
(defun mmm-update-current-submode (&optional pos)mmm-update-current-submode
178,6135
(defun mmm-set-current-submode (mode &optional pos)mmm-set-current-submode
199,6930
(defun mmm-submode-at (&optional pos type)mmm-submode-at
210,7373
(defun mmm-match-front (ovl)mmm-match-front
219,7648
(defun mmm-match-back (ovl)mmm-match-back
238,8409
(defun mmm-front-start (ovl)mmm-front-start
257,9154
(defun mmm-back-end (ovl)mmm-back-end
265,9458
(defun mmm-valid-submode-region (submode beg end)mmm-valid-submode-region
278,9805
(defun* mmm-make-regionmmm-make-region
305,10961
(defun mmm-make-overlay (submode beg end name face beg-sticky end-sticky evapmmm-make-overlay
431,16311
(defun mmm-get-face (face submode &optional delim)mmm-get-face
459,17444
(defun mmm-clear-overlays (&optional start stop strict)mmm-clear-overlays
470,17736
(defun mmm-update-mode-info (mode &optional force)mmm-update-mode-info
486,18201
(defun mmm-update-submode-region ()mmm-update-submode-region
571,21841
(defun mmm-add-hooks ()mmm-add-hooks
588,22571
(defun mmm-remove-hooks ()mmm-remove-hooks
591,22668
(defun mmm-get-local-variables-list (type mode)mmm-get-local-variables-list
597,22795
(defun mmm-get-locals (type)mmm-get-locals
617,23491
(defun mmm-get-saved-local (mode var)mmm-get-saved-local
630,23988
(defun mmm-set-local-variables (mode)mmm-set-local-variables
634,24153
(defun mmm-get-saved-local-variables (mode)mmm-get-saved-local-variables
645,24531
(defun mmm-save-changed-local-variables (ovl mode)mmm-save-changed-local-variables
653,24806
(defun mmm-clear-local-variables ()mmm-clear-local-variables
672,25510
(defun mmm-enable-font-lock (mode)mmm-enable-font-lock
683,25775
(defun mmm-update-font-lock-buffer ()mmm-update-font-lock-buffer
691,26035
(defun mmm-refontify-maybe (&optional start stop)mmm-refontify-maybe
704,26446
(defun mmm-submode-changes-in (start stop)mmm-submode-changes-in
719,26926
(defun mmm-regions-in (start stop &optional flag delim)mmm-regions-in
730,27283
(defun mmm-regions-alist (start stop)mmm-regions-alist
744,27761
(defun mmm-fontify-region (start stop &optional loudly)mmm-fontify-region
761,28288
(defun mmm-fontify-region-list (mode regions)mmm-fontify-region-list
781,29284
(defun mmm-beginning-of-syntax ()mmm-beginning-of-syntax
803,30032

contrib/mmm/mmm-rpm.el,242
(defconst mmm-rpm-sh-start-tagsmmm-rpm-sh-start-tags
48,1618
(defvar mmm-rpm-sh-end-tagsmmm-rpm-sh-end-tags
53,1842
(defvar mmm-rpm-sh-start-regexpmmm-rpm-sh-start-regexp
57,2016
(defvar mmm-rpm-sh-end-regexpmmm-rpm-sh-end-regexp
61,2194

contrib/mmm/mmm-sample.el,289
(defvar mmm-here-doc-mode-alist '()mmm-here-doc-mode-alist
84,2601
(defun mmm-here-doc-get-mode (string)mmm-here-doc-get-mode
93,3086
(defun mmm-file-variables-verify ()mmm-file-variables-verify
208,6343
(defun mmm-file-variables-find-back (bound)mmm-file-variables-find-back
232,7148

contrib/mmm/mmm-univ.el,60
(defun mmm-univ-get-mode (string)mmm-univ-get-mode
38,1205

contrib/mmm/mmm-utils.el,555
(defmacro mmm-valid-buffer (&rest body)mmm-valid-buffer
42,1332
(defmacro mmm-save-all (&rest body)mmm-save-all
61,1941
(defun mmm-format-string (string arg-pairs)mmm-format-string
74,2223
(defun mmm-format-matches (string &optional on-string)mmm-format-matches
85,2661
(defmacro mmm-save-keyword (param)mmm-save-keyword
108,3419
(defmacro mmm-save-keywords (&rest params)mmm-save-keywords
116,3746
(defun mmm-looking-back-at (regexp &optional bound)mmm-looking-back-at
129,4244
(defun mmm-make-marker (pos beg-p sticky-p)mmm-make-marker
146,4784

contrib/mmm/mmm-vars.el,4660
(defgroup mmm nilmmm
104,3283
(defvar mmm-c-derived-modesmmm-c-derived-modes
111,3393
(defvar mmm-save-local-variablesmmm-save-local-variables
115,3512
(defvar mmm-buffer-saved-locals ()mmm-buffer-saved-locals
341,10293
(defvar mmm-region-saved-locals-defaults ()mmm-region-saved-locals-defaults
346,10493
(defvar mmm-region-saved-locals-for-dominant ()mmm-region-saved-locals-for-dominant
352,10753
(defgroup mmm-faces nilmmm-faces
362,11130
(defcustom mmm-submode-decoration-level 1mmm-submode-decoration-level
368,11301
(defface mmm-init-submode-face '((t (:background "Pink")))mmm-init-submode-face
386,12145
(defface mmm-cleanup-submode-face '((t (:background "Wheat")))mmm-cleanup-submode-face
390,12285
(defface mmm-declaration-submode-face '((t (:background "Aquamarine")))mmm-declaration-submode-face
394,12422
(defface mmm-comment-submode-face '((t (:background "SkyBlue")))mmm-comment-submode-face
398,12568
(defface mmm-output-submode-face '((t (:background "Plum")))mmm-output-submode-face
402,12721
(defface mmm-special-submode-face '((t (:background "MediumSpringGreen")))mmm-special-submode-face
406,12870
(defface mmm-code-submode-face '((t (:background "LightGray")))mmm-code-submode-face
410,13034
(defface mmm-default-submode-face '((t (:background "gray85")))mmm-default-submode-face
414,13173
(defface mmm-delimiter-face nilmmm-delimiter-face
419,13381
(defcustom mmm-mode-string " MMM"mmm-mode-string
426,13507
(defcustom mmm-submode-mode-line-format "~M[~m]"mmm-submode-mode-line-format
431,13638
(defvar mmm-primary-mode-display-name nilmmm-primary-mode-display-name
448,14293
(defvar mmm-buffer-mode-display-name nilmmm-buffer-mode-display-name
453,14507
(defun mmm-set-mode-line ()mmm-set-mode-line
459,14806
(defvar mmm-classes nilmmm-classes
483,15614
(defvar mmm-global-classes '(universal)mmm-global-classes
489,15859
(defcustom mmm-mode-ext-classes-alist nilmmm-mode-ext-classes-alist
496,16041
(defun mmm-add-mode-ext-class (mode ext class)mmm-add-mode-ext-class
515,16831
(defcustom mmm-major-mode-preferencesmmm-major-mode-preferences
524,17156
(defun mmm-add-to-major-mode-preferences (language mode &optional default)mmm-add-to-major-mode-preferences
542,17884
(defun mmm-ensure-modename (symbol)mmm-ensure-modename
558,18642
(defun mmm-modename->function (mode)mmm-modename->function
567,18945
(defcustom mmm-delimiter-mode 'fundamental-modemmm-delimiter-mode
581,19394
(defcustom mmm-mode-prefix-key [(control ?c) ?%]mmm-mode-prefix-key
591,19663
(defcustom mmm-command-modifiers '(control)mmm-command-modifiers
596,19790
(defcustom mmm-insert-modifiers '()mmm-insert-modifiers
610,20423
(defcustom mmm-use-old-command-keys nilmmm-use-old-command-keys
625,21101
(defun mmm-use-old-command-keys ()mmm-use-old-command-keys
635,21565
(defcustom mmm-mode-hook ()mmm-mode-hook
643,21757
(defun mmm-run-constructed-hook (body &optional suffix)mmm-run-constructed-hook
663,22564
(defun mmm-run-major-hook ()mmm-run-major-hook
671,22908
(defun mmm-run-submode-hook (submode)mmm-run-submode-hook
674,22985
(defvar mmm-class-hooks-run ()mmm-class-hooks-run
677,23072
(defun mmm-run-class-hook (class)mmm-run-class-hook
682,23244
(defvar mmm-primary-mode-entry-hook nilmmm-primary-mode-entry-hook
687,23416
(defcustom mmm-major-mode-hook ()mmm-major-mode-hook
702,24063
(defun mmm-run-major-mode-hook ()mmm-run-major-mode-hook
716,24694
(defcustom mmm-global-mode nilmmm-global-mode
729,25235
(defcustom mmm-never-modesmmm-never-modes
745,25902
(defvar mmm-set-file-name-for-modes '(mew-draft-mode)mmm-set-file-name-for-modes
763,26202
(defvar mmm-mode nilmmm-mode
774,26561
(defvar mmm-primary-mode nilmmm-primary-mode
782,26769
(defvar mmm-classes-alist nilmmm-classes-alist
793,27135
(defun mmm-add-classes (classes)mmm-add-classes
948,35342
(defun mmm-add-group (group classes)mmm-add-group
953,35507
(defun mmm-add-to-group (group classes)mmm-add-to-group
963,35880
(defconst mmm-version "0.4.8"mmm-version
977,36307
(defun mmm-version ()mmm-version
980,36372
(defvar mmm-temp-buffer-name " *mmm-temp*"mmm-temp-buffer-name
987,36515
(defvar mmm-interactive-history nilmmm-interactive-history
993,36645
(defun mmm-add-to-history (class)mmm-add-to-history
999,36914
(defun mmm-clear-history ()mmm-clear-history
1002,36997
(defvar mmm-mode-ext-classes ()mmm-mode-ext-classes
1010,37182
(defun mmm-get-mode-ext-classes ()mmm-get-mode-ext-classes
1015,37393
(defun mmm-clear-mode-ext-classes ()mmm-clear-mode-ext-classes
1024,37720
(defun mmm-mode-ext-applies (element)mmm-mode-ext-applies
1028,37845
(defun mmm-get-all-classes (global)mmm-get-all-classes
1042,38224