path: root/TAGS


acl2/acl2.el,0

acl2/x-symbol-acl2.el,0

coq/coq-abbrev.el,152
(defun holes-show-doc holes-show-doc
4,90
(defpgdefault menu-entriesmenu-entries
151,7985
(defpgdefault help-menu-entrieshelp-menu-entries
349,19008

coq/coq-autotest.el,0

coq/coq.el,6716
(defun proofstack proofstack
23,436
(defun proofstack proofstack
24,508
(defun proofstack proofstack
25,580
(defcustom coq-prog-name coq-prog-name
28,670
(defcustom coq-compile-file-command coq-compile-file-command
33,779
(defcustom coq-default-undo-limit coq-default-undo-limit
43,1148
(defconst coq-shell-init-cmd coq-shell-init-cmd
48,1276
(defconst coq-shell-restart-cmd coq-shell-restart-cmd
58,1535
(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern
66,1836
(defvar coq-shell-cd coq-shell-cd
73,2112
(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp
77,2267
(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp
80,2393
(defvar coq-goal-regexpcoq-goal-regexp
83,2524
(defun coq-library-directory coq-library-directory
92,2713
(defcustom coq-tags coq-tags
99,2893
(defconst coq-interrupt-regexp coq-interrupt-regexp
104,3043
(defcustom coq-www-home-page coq-www-home-page
109,3164
(defun coq-insert-section coq-insert-section
119,3351
(defconst module-kinds-table module-kinds-table
128,3591
(defconst modtype-kinds-tablemodtype-kinds-table
132,3727
(defun coq-insert-module coq-insert-module
136,3856
(defvar coq-outline-regexpcoq-outline-regexp
156,4534
(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp
161,4943
(defvar coq-shell-outline-regexp coq-shell-outline-regexp
163,5002
(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp
164,5052
(defconst coq-kill-goal-command coq-kill-goal-command
169,5162
(defconst coq-forget-id-command coq-forget-id-command
170,5205
(defconst coq-back-n-command coq-back-n-command
171,5251
(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp
174,5295
(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp
176,5396
(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp
178,5503
(defconst coq-commands-regexp coq-commands-regexp
180,5615
(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp
182,5693
(defvar coq-keywords-sectioncoq-keywords-section
185,5785
(defvar coq-section-regexp coq-section-regexp
188,5878
(defun coq-set-undo-limit coq-set-undo-limit
222,6977
(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp
233,7415
(defun coq-proof-mode-p coq-proof-mode-p
237,7565
(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp
248,7975
(defun coq-is-goalsave-p coq-is-goalsave-p
250,8079
(defun coq-is-module-equal-p coq-is-module-equal-p
251,8154
(defun coq-is-def-p coq-is-def-p
254,8350
(defun coq-is-decl-defn-p coq-is-decl-defn-p
256,8458
(defun coq-state-preserving-command-p coq-state-preserving-command-p
261,8625
(defun coq-command-p coq-command-p
264,8759
(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p
267,8859
(defun coq-state-changing-tactic-p coq-state-changing-tactic-p
272,9007
(defun coq-state-changing-command-p coq-state-changing-command-p
279,9241
(defun coq-section-or-module-start-p coq-section-or-module-start-p
285,9549
(defun build-list-id-from-string build-list-id-from-string
294,9790
(defun coq-last-prompt-info coq-last-prompt-info
307,10320
(defun coq-last-prompt-info-safe coq-last-prompt-info-safe
324,10937
(defvar coq-last-but-one-statenum coq-last-but-one-statenum
334,11452
(defvar coq-last-but-one-proofnum coq-last-but-one-proofnum
336,11519
(defvar coq-last-but-one-proofstack coq-last-but-one-proofstack
338,11582
(defun coq-get-span-statenum coq-get-span-statenum
340,11624
(defun coq-get-span-proofnum coq-get-span-proofnum
345,11739
(defun coq-get-span-proofstack coq-get-span-proofstack
350,11854
(defun coq-set-span-statenum coq-set-span-statenum
355,11998
(defun coq-set-span-proofnum coq-set-span-proofnum
360,12129
(defun coq-set-span-proofstack coq-set-span-proofstack
365,12260
(defun proof-last-locked-span proof-last-locked-span
370,12420
(defun coq-set-state-infos coq-set-state-infos
385,13024
(defun count-not-intersection count-not-intersection
416,14627
(defun  coq-find-and-forget-v81 coq-find-and-forget-v81
447,15881
(defun coq-find-and-forget-v80 coq-find-and-forget-v80
471,16748
(defun coq-find-and-forget coq-find-and-forget
566,21443
(defvar coq-current-goal coq-current-goal
578,21897
(defun coq-goal-hyp coq-goal-hyp
581,21962
(defun coq-state-preserving-p coq-state-preserving-p
595,22425
(defun coq-SearchIsos coq-SearchIsos
602,22742
(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string
612,23094
(defun coq-ask-do coq-ask-do
622,23415
(defun coq-Print coq-Print
631,23676
(defun coq-About coq-About
635,23800
(defun coq-Print-implicit coq-Print-implicit
639,23919
(defun coq-Check coq-Check
644,24072
(defun coq-Show coq-Show
649,24182
(defun coq-PrintHint coq-PrintHint
664,24619
(defun coq-end-Section coq-end-Section
670,24763
(defun coq-Compile coq-Compile
688,25347
(defun coq-intros coq-intros
695,25528
(define-key coq-keymap coq-keymap
712,26205
(define-key coq-keymap coq-keymap
713,26256
(define-key coq-keymap coq-keymap
714,26315
(define-key coq-keymap coq-keymap
715,26373
(define-key coq-keymap coq-keymap
716,26429
(define-key coq-keymap coq-keymap
717,26484
(define-key coq-keymap coq-keymap
718,26534
(define-key coq-keymap coq-keymap
719,26584
(define-key coq-keymap coq-keymap
720,26634
(defun coq-guess-command-line coq-guess-command-line
739,27486
(defun coq-pre-shell-start coq-pre-shell-start
761,28293
(defun coq-mode-config coq-mode-config
773,28817
(defun coq-shell-mode-config coq-shell-mode-config
873,32330
(defun coq-goals-mode-config coq-goals-mode-config
912,33981
(defun coq-response-config coq-response-config
920,34229
(defun coq-maybe-compile-buffer coq-maybe-compile-buffer
941,34956
(defun coq-ancestors-of coq-ancestors-of
978,36490
(defun coq-all-ancestors-of coq-all-ancestors-of
1001,37457
(defconst coq-require-command-regexp coq-require-command-regexp
1013,37850
(defun coq-process-require-command coq-process-require-command
1018,38059
(defun coq-included-children coq-included-children
1023,38186
(defun coq-process-file coq-process-file
1044,39025
(defpacustom print-fully-explicit print-fully-explicit
1066,39823
(defpacustom print-coercions print-coercions
1071,39972
(defpacustom print-match-wildcards print-match-wildcards
1076,40117
(defpacustom time-commands time-commands
1082,40301
(defpacustom auto-compile-vos auto-compile-vos
1086,40412
(defpacustom translate-to-v8 translate-to-v8
1108,41367
(defun coq-preprocessing coq-preprocessing
1117,41583
(defun coq-fake-constant-markup coq-fake-constant-markup
1132,42002
(defun coq-create-span-menu coq-create-span-menu
1154,42809

coq/coq-indent.el,1791
(defconst coq-any-command-regexpcoq-any-command-regexp
11,262
(defconst coq-indent-inner-regexpcoq-indent-inner-regexp
15,354
(defconst coq-indent-open-regexpcoq-indent-open-regexp
43,1113
(defconst coq-indent-close-regexpcoq-indent-close-regexp
48,1283
(defconst coq-indent-closepar-regexp coq-indent-closepar-regexp
53,1441
(defconst coq-indent-closematch-regexp coq-indent-closematch-regexp
55,1487
(defconst coq-indent-openpar-regexp coq-indent-openpar-regexp
57,1559
(defconst coq-indent-openmatch-regexp coq-indent-openmatch-regexp
59,1604
(defconst coq-indent-any-regexpcoq-indent-any-regexp
61,1685
(defconst coq-indent-kw coq-indent-kw
70,1914
(defconst coq-indent-pattern-regexp coq-indent-pattern-regexp
81,2331
(defun coq-find-command-start coq-find-command-start
86,2418
(defun coq-find-real-start coq-find-real-start
95,2694
(defun coq-find-end coq-find-end
107,3088
(defun coq-current-command-string coq-current-command-string
118,3486
(defun is-at-a-space-or-tab is-at-a-space-or-tab
126,3685
(defun only-spaces-on-line only-spaces-on-line
132,3889
(defun find-reg find-reg
139,4137
(defun coq-back-to-indentation-prevline coq-back-to-indentation-prevline
154,4534
(defun coq-find-unclosed coq-find-unclosed
183,5787
(defun coq-find-at-same-level-zero coq-find-at-same-level-zero
210,6968
(defun coq-find-unopened coq-find-unopened
238,8052
(defun coq-find-last-unopened coq-find-last-unopened
284,9405
(defun coq-end-offset coq-end-offset
297,9809
(defun coq-indent-command-offset coq-indent-command-offset
325,10628
(defun coq-indent-expr-offset coq-indent-expr-offset
370,12387
(defun coq-indent-offset coq-indent-offset
482,16590
(defun coq-indent-calculate coq-indent-calculate
502,17253
(defun proof-indent-line proof-indent-line
516,17700

coq/coq-syntax.el,2992
(defvar coq-version-is-V8 coq-version-is-V8
19,648
(defvar coq-version-is-V8-0 coq-version-is-V8-0
21,727
(defvar coq-version-is-V8-1 coq-version-is-V8-1
28,1099
(defvar coq-keywords-declcoq-keywords-decl
75,2947
(defvar coq-keywords-defncoq-keywords-defn
90,3303
(defvar coq-keywords-goalcoq-keywords-goal
109,3728
(defun coq-count-match coq-count-match
152,5363
(defun coq-goal-command-p coq-goal-command-p
164,5783
(defvar coq-keywords-save-strictcoq-keywords-save-strict
182,6365
(defvar coq-keywords-savecoq-keywords-save
190,6462
(defun coq-save-command-p coq-save-command-p
194,6538
(defvar coq-keywords-kill-goal coq-keywords-kill-goal
202,6817
(defcustom coq-user-state-changing-commands coq-user-state-changing-commands
208,6867
(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands
220,7264
(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands
233,7704
(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands
281,8831
(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands
354,10812
(defvar coq-keywords-commandscoq-keywords-commands
364,11009
(defvar coq-tacticalscoq-tacticals
369,11158
(defvar coq-reservedcoq-reserved
381,11359
(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics
406,11618
(defvar coq-state-changing-tacticscoq-state-changing-tactics
417,12044
(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics
525,13628
(defvar coq-state-preserving-tacticscoq-state-preserving-tactics
536,14042
(defvar coq-tacticscoq-tactics
540,14140
(defvar coq-retractable-instructcoq-retractable-instruct
543,14229
(defvar coq-non-retractable-instructcoq-non-retractable-instruct
546,14339
(defvar coq-keywordscoq-keywords
550,14461
(defvar coq-symbolscoq-symbols
557,14628
(defvar coq-error-regexp coq-error-regexp
575,14832
(defvar coq-id coq-id
578,15061
(defvar coq-id-shy coq-id-shy
579,15086
(defvar coq-ids coq-ids
581,15140
(defun coq-first-abstr-regexp coq-first-abstr-regexp
583,15177
(defun coq-next-abstr-regexp coq-next-abstr-regexp
586,15265
(defvar coq-font-lock-termscoq-font-lock-terms
589,15343
(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict
604,15996
(defconst coq-save-command-regexpcoq-save-command-regexp
606,16109
(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp
608,16208
(defconst coq-goal-command-regexpcoq-goal-command-regexp
611,16346
(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp
613,16445
(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp
619,16734
(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp
622,16867
(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1
625,17007
(defvar coq-font-lock-keywords coq-font-lock-keywords
646,18050
(defun coq-init-syntax-table coq-init-syntax-table
648,18108
(defconst coq-generic-expressioncoq-generic-expression
677,19006

coq/x-symbol-coq.el,2822
(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts
16,384
(defvar x-symbol-coq-name x-symbol-coq-name
24,785
(defvar x-symbol-coq-modeline-name x-symbol-coq-modeline-name
25,825
(defcustom x-symbol-coq-header-groups-alist x-symbol-coq-header-groups-alist
27,868
(defcustom x-symbol-coq-electric-ignore x-symbol-coq-electric-ignore
34,1086
(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts
41,1331
(defvar x-symbol-coq-extra-menu-items x-symbol-coq-extra-menu-items
44,1430
(defvar x-symbol-coq-token-grammarx-symbol-coq-token-grammar
48,1518
(defun x-symbol-coq-default-token-list x-symbol-coq-default-token-list
64,2184
(defvar x-symbol-coq-user-table x-symbol-coq-user-table
76,2472
(defvar x-symbol-coq-generated-data x-symbol-coq-generated-data
79,2578
(defvar x-symbol-coq-master-directory x-symbol-coq-master-directory
87,2816
(defvar x-symbol-coq-image-searchpath x-symbol-coq-image-searchpath
88,2864
(defvar x-symbol-coq-image-cached-dirs x-symbol-coq-image-cached-dirs
89,2911
(defvar x-symbol-coq-image-file-truename-alist x-symbol-coq-image-file-truename-alist
90,2976
(defvar x-symbol-coq-image-keywords x-symbol-coq-image-keywords
91,3028
(defcustom x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher
98,3256
(defcustom x-symbol-coq-font-lock-regexp x-symbol-coq-font-lock-regexp
104,3488
(defcustom x-symbol-coq-font-lock-limit-regexp x-symbol-coq-font-lock-limit-regexp
109,3660
(defcustom x-symbol-coq-font-lock-contents-regexp x-symbol-coq-font-lock-contents-regexp
115,3848
(defcustom x-symbol-coq-single-char-regexp x-symbol-coq-single-char-regexp
122,4102
(defun x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher
127,4250
(defun coq-match-subscript coq-match-subscript
162,5939
(defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces
169,6113
(defcustom x-symbol-coq-class-alistx-symbol-coq-class-alist
174,6338
(defcustom x-symbol-coq-class-face-alist x-symbol-coq-class-face-alist
185,6716
(defvar x-symbol-coq-font-lock-keywords x-symbol-coq-font-lock-keywords
195,7026
(defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces
197,7072
(defvar x-symbol-coq-case-insensitive x-symbol-coq-case-insensitive
203,7296
(defvar x-symbol-coq-token-shape x-symbol-coq-token-shape
204,7339
(defvar x-symbol-coq-input-token-ignore x-symbol-coq-input-token-ignore
205,7377
(defvar x-symbol-coq-token-list x-symbol-coq-token-list
206,7422
(defvar x-symbol-coq-symbol-table x-symbol-coq-symbol-table
208,7466
(defvar x-symbol-coq-xsymbol-table x-symbol-coq-xsymbol-table
312,9885
(defun x-symbol-coq-prepare-table x-symbol-coq-prepare-table
459,13753
(defvar x-symbol-coq-tablex-symbol-coq-table
468,14020
(defcustom x-symbol-coq-auto-stylex-symbol-coq-auto-style
475,14181

demoisa/demoisa-easy.el,0

demoisa/demoisa.el,568
(defcustom isabelledemo-prog-name isabelledemo-prog-name
54,1809
(defcustom isabelledemo-web-pageisabelledemo-web-page
59,1931
(defun demoisa-config demoisa-config
70,2161
(defun demoisa-shell-config demoisa-shell-config
90,2910
(define-derived-mode demoisa-mode demoisa-mode
119,3994
(define-derived-mode demoisa-shell-mode demoisa-shell-mode
124,4117
(define-derived-mode demoisa-response-mode demoisa-response-mode
129,4260
(define-derived-mode demoisa-goals-mode demoisa-goals-mode
133,4387
(defun demoisa-pre-shell-start demoisa-pre-shell-start
152,5169

generic/pg-assoc.el,408
(define-derived-mode proof-universal-keys-only-mode proof-universal-keys-only-mode
20,563
(defun proof-associated-buffers proof-associated-buffers
32,987
(defun pg-assoc-strip-subterm-markup pg-assoc-strip-subterm-markup
46,1287
(defun pg-assoc-strip-subterm-markup-buf pg-assoc-strip-subterm-markup-buf
72,2220
(defun pg-assoc-strip-subterm-markup-buf-old pg-assoc-strip-subterm-markup-buf-old
94,2969

generic/pg-autotest.el,705
(defvar pg-autotest-success pg-autotest-success
20,514
(defun pg-autotest-find-file pg-autotest-find-file
24,598
(defun pg-autotest-find-file-restart pg-autotest-find-file-restart
31,869
(defmacro pg-autotest pg-autotest
44,1317
(defun pg-autotest-script-wholefile pg-autotest-script-wholefile
58,1665
(defun pg-autotest-retract-file pg-autotest-retract-file
75,2278
(defun pg-autotest-assert-processed pg-autotest-assert-processed
81,2414
(defun pg-autotest-assert-unprocessed pg-autotest-assert-unprocessed
88,2660
(defun pg-autotest-message pg-autotest-message
95,2907
(defun pg-autotest-quit-prover pg-autotest-quit-prover
102,3100
(defun pg-autotest-finished pg-autotest-finished
108,3282

generic/pg-goals.el,1075
(define-derived-mode proof-goals-mode proof-goals-mode
28,651
(define-key proof-goals-mode-map proof-goals-mode-map
48,1341
(define-key proof-goals-mode-map proof-goals-mode-map
51,1424
(define-key proof-goals-mode-map proof-goals-mode-map
52,1494
(define-key proof-goals-mode-map proof-goals-mode-map
60,2084
(define-key proof-goals-mode-map proof-goals-mode-map
62,2157
(define-key proof-goals-mode-map proof-goals-mode-map
63,2225
(define-key proof-goals-mode-map proof-goals-mode-map
69,2659
(defun proof-goals-config-done proof-goals-config-done
84,2923
(defun pg-goals-display pg-goals-display
94,3211
(defun pg-goals-analyse-structure pg-goals-analyse-structure
143,5154
(defun pg-goals-make-top-span pg-goals-make-top-span
267,10000
(defun pg-goals-yank-subterm pg-goals-yank-subterm
297,11007
(defun pg-goals-button-action pg-goals-button-action
324,11907
(defun proof-expand-path proof-expand-path
345,12880
(defun pg-goals-construct-command pg-goals-construct-command
354,13124
(defun pg-goals-get-subterm-help pg-goals-get-subterm-help
378,13976

generic/pg-metadata.el,204
(defcustom pg-metadata-default-directory pg-metadata-default-directory
23,628
(defface proof-preparsed-span proof-preparsed-span
28,802
(defun pg-metadata-filename-for pg-metadata-filename-for
39,1065

generic/pg-pbrpm.el,2734
(defvar pg-pbrpm-use-buffer-menu pg-pbrpm-use-buffer-menu
11,259
(defvar pg-pbrpm-buffer-menu pg-pbrpm-buffer-menu
13,378
(defvar pg-pbrpm-spans pg-pbrpm-spans
14,412
(defvar pg-pbrpm-goal-description pg-pbrpm-goal-description
15,440
(defun pg-pbrpm-erase-buffer-menu pg-pbrpm-erase-buffer-menu
17,480
(defun pg-pbrpm-menu-change-hook pg-pbrpm-menu-change-hook
24,685
(defun pg-pbrpm-create-reset-buffer-menu pg-pbrpm-create-reset-buffer-menu
42,1262
(defun pg-pbrpm-analyse-goal-buffer pg-pbrpm-analyse-goal-buffer
57,1914
(defun pg-pbrpm-button-action pg-pbrpm-button-action
118,4334
(defun pg-pbrpm-exists pg-pbrpm-exists
125,4560
(defun pg-pbrpm-eliminate-id pg-pbrpm-eliminate-id
129,4672
(defun pg-pbrpm-build-menu pg-pbrpm-build-menu
137,4920
(defun pg-pbrpm-setup-span pg-pbrpm-setup-span
193,7110
(defun pg-pbrpm-run-command pg-pbrpm-run-command
253,9477
(defun pg-pbrpm-get-pos-info pg-pbrpm-get-pos-info
281,10753
(defun pg-pbrpm-get-region-info pg-pbrpm-get-region-info
317,11895
(defun auto-select-arround-pos auto-select-arround-pos
327,12220
(defun pg-pbrpm-translate-position pg-pbrpm-translate-position
339,12664
(defun pg-pbrpm-process-click pg-pbrpm-process-click
345,12888
(defvar pg-pbrpm-remember-region-selected-region pg-pbrpm-remember-region-selected-region
365,13892
(defvar pg-pbrpm-regions-list pg-pbrpm-regions-list
366,13946
(defun pg-pbrpm-erase-regions-list pg-pbrpm-erase-regions-list
368,13982
(defun pg-pbrpm-filter-regions-list pg-pbrpm-filter-regions-list
377,14291
(defface pg-pbrpm-multiple-selection-facepg-pbrpm-multiple-selection-face
384,14554
(defface pg-pbrpm-menu-input-facepg-pbrpm-menu-input-face
392,14759
(defun pg-pbrpm-do-remember-region pg-pbrpm-do-remember-region
400,14952
(defun pg-pbrpm-remember-region-drag-up-hook pg-pbrpm-remember-region-drag-up-hook
421,15793
(defun pg-pbrpm-remember-region-click-hook pg-pbrpm-remember-region-click-hook
425,15964
(defun pg-pbrpm-remember-region pg-pbrpm-remember-region
430,16149
(defun pg-pbrpm-process-region pg-pbrpm-process-region
444,16864
(defun pg-pbrpm-process-regions-list pg-pbrpm-process-regions-list
461,17587
(defun pg-pbrpm-region-expression pg-pbrpm-region-expression
465,17770
(define-key proof-goals-mode-map proof-goals-mode-map
489,18706
(define-key proof-goals-mode-map proof-goals-mode-map
490,18776
(define-key proof-goals-mode-map proof-goals-mode-map
491,18853
(define-key pg-span-context-menu-keymap pg-span-context-menu-keymap
492,18933
(define-key pg-span-context-menu-keymap pg-span-context-menu-keymap
493,19010
(define-key proof-mode-map proof-mode-map
494,19093
(define-key proof-mode-map proof-mode-map
495,19157
(define-key proof-mode-map proof-mode-map
496,19228

generic/pg-pgip.el,5296
(defalias 'pg-pgip-debug pg-pgip-debug
29,894
(defalias 'pg-pgip-error pg-pgip-error
30,935
(defalias 'pg-pgip-warning pg-pgip-warning
31,970
(defconst pg-pgip-version-supported pg-pgip-version-supported
33,1020
(defun pg-pgip-process-packet pg-pgip-process-packet
37,1126
(defvar pg-pgip-last-seen-id pg-pgip-last-seen-id
47,1699
(defvar pg-pgip-last-seen-seq pg-pgip-last-seen-seq
48,1733
(defun pg-pgip-process-pgip pg-pgip-process-pgip
50,1769
(defun pg-pgip-process-msg pg-pgip-process-msg
69,2696
(defvar pg-pgip-post-process-functionspg-pgip-post-process-functions
83,3266
(defun pg-pgip-post-process pg-pgip-post-process
93,3750
(defun pg-pgip-process-askpgip pg-pgip-process-askpgip
109,4361
(defun pg-pgip-process-usespgip pg-pgip-process-usespgip
114,4520
(defun pg-pgip-process-usespgml pg-pgip-process-usespgml
118,4684
(defun pg-pgip-process-pgmlconfig pg-pgip-process-pgmlconfig
122,4848
(defun pg-pgip-process-proverinfo pg-pgip-process-proverinfo
138,5456
(defun pg-pgip-process-hasprefs pg-pgip-process-hasprefs
155,6121
(defun pg-pgip-haspref pg-pgip-haspref
169,6753
(defun pg-pgip-process-prefval pg-pgip-process-prefval
188,7532
(defun pg-pgip-process-guiconfig pg-pgip-process-guiconfig
215,8241
(defvar proof-assistant-idtables proof-assistant-idtables
222,8358
(defun pg-pgip-process-ids pg-pgip-process-ids
225,8475
(defun pg-complete-idtable-symbol pg-complete-idtable-symbol
251,9554
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
256,9646
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
257,9702
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
258,9758
(defun pg-pgip-process-idvalue pg-pgip-process-idvalue
261,9816
(defun pg-pgip-process-menuadd pg-pgip-process-menuadd
273,10153
(defun pg-pgip-process-menudel pg-pgip-process-menudel
276,10196
(defun pg-pgip-process-ready pg-pgip-process-ready
285,10429
(defun pg-pgip-process-cleardisplay pg-pgip-process-cleardisplay
288,10470
(defun pg-pgip-process-proofstate pg-pgip-process-proofstate
302,10947
(defun pg-pgip-process-normalresponse pg-pgip-process-normalresponse
306,11024
(defun pg-pgip-process-errorresponse pg-pgip-process-errorresponse
310,11148
(defun pg-pgip-process-scriptinsert pg-pgip-process-scriptinsert
314,11271
(defun pg-pgip-process-metainforesponse pg-pgip-process-metainforesponse
319,11405
(defun pg-pgip-process-informfileloaded pg-pgip-process-informfileloaded
328,11646
(defun pg-pgip-process-informfileretracted pg-pgip-process-informfileretracted
334,11912
(defun pg-pgip-process-brokerstatus pg-pgip-process-brokerstatus
347,12386
(defun pg-pgip-process-proveravailmsg pg-pgip-process-proveravailmsg
350,12434
(defun pg-pgip-process-newprovermsg pg-pgip-process-newprovermsg
353,12484
(defun pg-pgip-process-proverstatusmsg pg-pgip-process-proverstatusmsg
356,12532
(defvar pg-pgip-srcids pg-pgip-srcids
365,12779
(defun pg-pgip-process-newfile pg-pgip-process-newfile
369,12886
(defun pg-pgip-process-filestatus pg-pgip-process-filestatus
385,13474
(defun pg-pgip-process-newobj pg-pgip-process-newobj
405,14129
(defun pg-pgip-process-delobj pg-pgip-process-delobj
408,14171
(defun pg-pgip-process-objectstatus pg-pgip-process-objectstatus
411,14213
(defun pg-pgip-process-parsescript pg-pgip-process-parsescript
425,14569
(defun pg-pgip-get-pgiptype pg-pgip-get-pgiptype
448,15444
(defun pg-pgip-default-for pg-pgip-default-for
468,16239
(defun pg-pgip-subst-for pg-pgip-subst-for
481,16634
(defun pg-pgip-interpret-value pg-pgip-interpret-value
493,16977
(defun pg-pgip-interpret-choice pg-pgip-interpret-choice
511,17660
(defun pg-pgip-get-icon pg-pgip-get-icon
542,18733
(defsubst pg-pgip-get-name pg-pgip-get-name
546,18881
(defsubst pg-pgip-get-version pg-pgip-get-version
549,18998
(defsubst pg-pgip-get-descr pg-pgip-get-descr
552,19121
(defsubst pg-pgip-get-thmname pg-pgip-get-thmname
555,19240
(defsubst pg-pgip-get-thyname pg-pgip-get-thyname
558,19363
(defsubst pg-pgip-get-url pg-pgip-get-url
561,19486
(defsubst pg-pgip-get-srcid pg-pgip-get-srcid
564,19601
(defsubst pg-pgip-get-proverid pg-pgip-get-proverid
567,19720
(defsubst pg-pgip-get-symname pg-pgip-get-symname
570,19845
(defsubst pg-pgip-get-prefcat pg-pgip-get-prefcat
573,19965
(defsubst pg-pgip-get-default pg-pgip-get-default
576,20093
(defsubst pg-pgip-get-objtype pg-pgip-get-objtype
579,20216
(defsubst pg-pgip-get-value pg-pgip-get-value
582,20339
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
585,20409
(defun pg-pgip-get-pgmltext pg-pgip-get-pgmltext
587,20468
(defun pg-pgip-string-of-command pg-pgip-string-of-command
596,20703
(defconst pg-pgip-idpg-pgip-id
613,21464
(defvar pg-pgip-refseq pg-pgip-refseq
619,21744
(defvar pg-pgip-refid pg-pgip-refid
621,21842
(defvar pg-pgip-seq pg-pgip-seq
624,21936
(defun pg-pgip-assemble-packet pg-pgip-assemble-packet
626,22000
(defun pg-pgip-issue pg-pgip-issue
644,22815
(defun pg-pgip-maybe-askpgip pg-pgip-maybe-askpgip
661,23428
(defun pg-pgip-askprefs pg-pgip-askprefs
667,23619
(defun pg-pgip-askids pg-pgip-askids
671,23733
(defun pg-pgip-reset pg-pgip-reset
684,24024
(defconst pg-pgip-start-element-regexp pg-pgip-start-element-regexp
715,24722
(defconst pg-pgip-end-element-regexp pg-pgip-end-element-regexp
716,24774

generic/pg-pgip-old.el,734
(defun pg-pgip-process-oldhaspref pg-pgip-process-oldhaspref
18,633
(defun pg-pgip-process-haspref pg-pgip-process-haspref
21,730
(defun pg-pgip-old-interpret-bool pg-pgip-old-interpret-bool
57,2158
(defun pg-pgip-old-interpret-int pg-pgip-old-interpret-int
66,2442
(defun pg-pgip-old-interpret-string pg-pgip-old-interpret-string
71,2609
(defun pg-pgip-old-interpret-choice pg-pgip-old-interpret-choice
74,2663
(defun pg-pgip-old-interpret-value pg-pgip-old-interpret-value
94,3382
(defun pg-pgip-old-default-for pg-pgip-old-default-for
113,3928
(defun pg-pgip-old-subst-for pg-pgip-old-subst-for
124,4252
(defun pg-pgip-old-get-type pg-pgip-old-get-type
131,4417
(defun pg-pgip-old-pgiptype pg-pgip-old-pgiptype
138,4633

generic/pg-response.el,1890
(define-derived-mode proof-response-mode proof-response-mode
24,597
(defun proof-response-config-done proof-response-config-done
47,1490
(defvar proof-shell-special-display-regexp proof-shell-special-display-regexp
68,2265
(defconst proof-multiframe-specifiers proof-multiframe-specifiers
76,2670
(defun proof-map-multiple-frame-specifiers proof-map-multiple-frame-specifiers
85,3034
(defconst proof-multiframe-parametersproof-multiframe-parameters
95,3496
(defun proof-multiple-frames-enable proof-multiple-frames-enable
104,3795
(defun proof-three-window-enable proof-three-window-enable
126,4515
(defun proof-select-three-b proof-select-three-b
130,4579
(defun proof-display-three-b proof-display-three-b
145,5048
(defvar pg-frame-configuration pg-frame-configuration
159,5542
(defun pg-cache-frame-configuration pg-cache-frame-configuration
163,5689
(defun proof-layout-windows proof-layout-windows
167,5860
(defun proof-delete-other-frames proof-delete-other-frames
208,7673
(defvar pg-response-erase-flag pg-response-erase-flag
239,8768
(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response
242,8883
(defun pg-response-display pg-response-display
272,10033
(defun pg-response-display-with-face pg-response-display-with-face
289,10855
(defun pg-response-clear-displays pg-response-clear-displays
324,12212
(defvar pg-response-next-error pg-response-next-error
341,12742
(defun proof-next-error proof-next-error
345,12864
(defun pg-response-has-error-location pg-response-has-error-location
425,15798
(defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos
448,16631
(defun proof-trace-fontify-pos proof-trace-fontify-pos
450,16674
(defun proof-trace-buffer-display proof-trace-buffer-display
458,16988
(defun proof-trace-buffer-finish proof-trace-buffer-finish
482,17961
(defun pg-thms-buffer-clear pg-thms-buffer-clear
503,18486

generic/pg-thymodes.el,219
(defmacro pg-defthymode pg-defthymode
19,466
(defmacro pg-do-unless-null pg-do-unless-null
67,2277
(defun pg-symval pg-symval
72,2364
(defun pg-modesym pg-modesym
78,2520
(defun pg-modesymval pg-modesymval
82,2634

generic/pg-user.el,3655
(defmacro proof-maybe-save-point proof-maybe-save-point
21,410
(defun proof-maybe-follow-locked-end proof-maybe-follow-locked-end
29,612
(defun proof-assert-next-command-interactive proof-assert-next-command-interactive
43,977
(defun proof-process-buffer proof-process-buffer
53,1348
(defun proof-undo-last-successful-command proof-undo-last-successful-command
67,1665
(defun proof-undo-and-delete-last-successful-command proof-undo-and-delete-last-successful-command
72,1827
(defun proof-undo-last-successful-command-1 proof-undo-last-successful-command-1
94,2799
(defun proof-retract-buffer proof-retract-buffer
110,3364
(defun proof-retract-current-goal proof-retract-current-goal
119,3644
(defun proof-interrupt-process proof-interrupt-process
137,4135
(defun proof-goto-command-start proof-goto-command-start
164,5120
(defun proof-goto-command-end proof-goto-command-end
187,6062
(defun proof-mouse-goto-point proof-mouse-goto-point
212,6842
(defun proof-mouse-track-insert proof-mouse-track-insert
227,7416
(defvar proof-minibuffer-history proof-minibuffer-history
262,8526
(defun proof-minibuffer-cmd proof-minibuffer-cmd
265,8620
(defun proof-frob-locked-end proof-frob-locked-end
313,10426
(defmacro proof-if-setting-configured proof-if-setting-configured
406,13340
(defmacro proof-define-assistant-command proof-define-assistant-command
414,13610
(defmacro proof-define-assistant-command-witharg proof-define-assistant-command-witharg
427,14076
(defun proof-issue-new-command proof-issue-new-command
447,14901
(defun proof-cd-sync proof-cd-sync
492,16400
(deflocal proof-electric-terminator proof-electric-terminator
543,17869
(defun proof-electric-terminator-enable proof-electric-terminator-enable
553,18216
(defun proof-electric-term-incomment-fn proof-electric-term-incomment-fn
564,18703
(defun proof-process-electric-terminator proof-process-electric-terminator
584,19459
(defun proof-electric-terminator proof-electric-terminator
611,20610
(defun proof-add-completions proof-add-completions
633,21248
(defun proof-script-complete proof-script-complete
653,22005
(defun pg-insert-last-output-as-comment pg-insert-last-output-as-comment
681,22596
(defun pg-copy-span-contents pg-copy-span-contents
712,23824
(defun pg-numth-span-higher-or-lower pg-numth-span-higher-or-lower
729,24384
(defun pg-control-span-of pg-control-span-of
755,25135
(defun pg-move-span-contents pg-move-span-contents
761,25339
(defun pg-fixup-children-span pg-fixup-children-span
815,27563
(defun pg-move-region-down pg-move-region-down
822,27771
(defun pg-move-region-up pg-move-region-up
831,28065
(defun proof-forward-command proof-forward-command
861,28905
(defun proof-backward-command proof-backward-command
882,29627
(defvar pg-span-context-menu-keymappg-span-context-menu-keymap
898,29871
(defun pg-span-for-event pg-span-for-event
914,30298
(defun pg-span-context-menu pg-span-context-menu
925,30682
(defun pg-toggle-visibility pg-toggle-visibility
940,31142
(defun pg-create-in-span-context-menu pg-create-in-span-context-menu
950,31464
(defun pg-goals-buffers-hint pg-goals-buffers-hint
1022,34017
(defun pg-slow-fontify-tracing-hint pg-slow-fontify-tracing-hint
1025,34184
(defun pg-response-buffers-hint pg-response-buffers-hint
1028,34340
(defun pg-jump-to-end-hint pg-jump-to-end-hint
1037,34689
(defun pg-processing-complete-hint pg-processing-complete-hint
1040,34805
(defun pg-next-error-hint pg-next-error-hint
1056,35491
(defun pg-hint pg-hint
1060,35628
(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query
1079,36304
(defun proof-imenu-enable proof-imenu-enable
1124,37931

generic/pg-xhtml.el,573
(defvar pg-xhtml-dir pg-xhtml-dir
17,423
(defun pg-xhtml-dir pg-xhtml-dir
20,489
(defvar pg-xhtml-file-count pg-xhtml-file-count
32,856
(defun pg-xhtml-next-file pg-xhtml-next-file
35,928
(defvar pg-xhtml-header pg-xhtml-header
47,1159
(defmacro pg-xhtml-write-tempfile pg-xhtml-write-tempfile
53,1400
(defun pg-xhtml-cleanup-tempdir pg-xhtml-cleanup-tempdir
71,1990
(defvar pg-mozilla-prog-name pg-mozilla-prog-name
75,2121
(defun pg-xhtml-display-file-mozilla pg-xhtml-display-file-mozilla
79,2229
(defalias 'pg-xhtml-display-file pg-xhtml-display-file
84,2402

generic/pg-xml.el,670
(defun pg-xml-parse-string pg-xml-parse-string
38,1118
(defun pg-xml-parse-buffer pg-xml-parse-buffer
49,1452
(defun pg-xml-get-attr pg-xml-get-attr
71,2185
(defun pg-xml-child-elts pg-xml-child-elts
79,2489
(defun pg-xml-child-elt pg-xml-child-elt
84,2694
(defun pg-xml-get-child pg-xml-get-child
92,2977
(defun pg-xml-get-text-content pg-xml-get-text-content
102,3349
(defmacro pg-xml-attr pg-xml-attr
113,3699
(defmacro pg-xml-node pg-xml-node
115,3761
(defconst pg-xml-header pg-xml-header
118,3854
(defun pg-xml-string-of pg-xml-string-of
122,3931
(defun pg-xml-output-internal pg-xml-output-internal
133,4303
(defun pg-xml-cdata pg-xml-cdata
167,5453

generic/_pkg.el,0

generic/proof-autoloads.el,79
(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
246,9930

generic/proof-config.el,16776
(defgroup proof-user-options proof-user-options
84,3173
(defcustom proof-electric-terminator-enable proof-electric-terminator-enable
89,3287
(defcustom proof-toolbar-enable proof-toolbar-enable
101,3821
(defcustom proof-imenu-enable proof-imenu-enable
107,3994
(defpgcustom x-symbol-enable x-symbol-enable
113,4165
(defpgcustom mmm-enable mmm-enable
122,4515
(defcustom pg-show-hints pg-show-hints
131,4869
(defcustom proof-output-fontify-enable proof-output-fontify-enable
136,5004
(defcustom proof-trace-output-slow-catchup proof-trace-output-slow-catchup
146,5386
(defcustom proof-strict-state-preserving proof-strict-state-preserving
156,5884
(defcustom proof-strict-read-only proof-strict-read-only
169,6493
(defcustom proof-three-window-enable proof-three-window-enable
179,6843
(defcustom proof-multiple-frames-enable proof-multiple-frames-enable
198,7598
(defcustom proof-delete-empty-windows proof-delete-empty-windows
207,7934
(defcustom proof-shrink-windows-tofit proof-shrink-windows-tofit
218,8465
(defcustom proof-toolbar-use-button-enablers proof-toolbar-use-button-enablers
225,8737
(defcustom proof-query-file-save-when-activating-scripting proof-query-file-save-when-activating-scripting
248,9609
(defpgcustom script-indent script-indent
264,10332
(defcustom proof-one-command-per-line proof-one-command-per-line
270,10520
(defcustom proof-prog-name-ask proof-prog-name-ask
278,10740
(defcustom proof-prog-name-guess proof-prog-name-guess
284,10901
(defcustom proof-tidy-responseproof-tidy-response
292,11161
(defcustom proof-show-debug-messages proof-show-debug-messages
306,11628
(defcustom proof-experimental-features proof-experimental-features
315,12006
(defcustom proof-follow-mode proof-follow-mode
333,12768
(defcustom proof-auto-action-when-deactivating-scripting proof-auto-action-when-deactivating-scripting
359,13963
(defcustom proof-script-command-separator proof-script-command-separator
382,14914
(defcustom proof-rsh-command proof-rsh-command
390,15207
(defcustom proof-disappearing-proofs proof-disappearing-proofs
406,15744
(defgroup proof-faces proof-faces
433,16394
(defmacro proof-face-specs proof-face-specs
438,16500
(defface proof-queue-face proof-queue-face
453,16946
(defface proof-locked-faceproof-locked-face
461,17226
(defface proof-declaration-name-faceproof-declaration-name-face
474,17729
(defconst proof-declaration-name-face proof-declaration-name-face
486,18122
(defface proof-tacticals-name-faceproof-tacticals-name-face
491,18358
(defconst proof-tacticals-name-face proof-tacticals-name-face
500,18620
(defface proof-tactics-name-faceproof-tactics-name-face
505,18850
(defconst proof-tactics-name-face proof-tactics-name-face
514,19115
(defface proof-error-face proof-error-face
519,19339
(defface proof-warning-faceproof-warning-face
527,19546
(defface proof-eager-annotation-faceproof-eager-annotation-face
536,19803
(defface proof-debug-message-faceproof-debug-message-face
544,20021
(defface proof-boring-faceproof-boring-face
552,20220
(defface proof-mouse-highlight-faceproof-mouse-highlight-face
560,20412
(defface proof-highlight-dependent-faceproof-highlight-dependent-face
568,20608
(defface proof-highlight-dependency-faceproof-highlight-dependency-face
576,20817
(defgroup prover-config prover-config
594,21076
(defcustom proof-mode-for-shell proof-mode-for-shell
628,22195
(defcustom proof-mode-for-response proof-mode-for-response
635,22442
(defcustom proof-mode-for-goals proof-mode-for-goals
642,22725
(defcustom proof-mode-for-script proof-mode-for-script
649,22980
(defcustom proof-guess-command-line proof-guess-command-line
660,23414
(defcustom proof-assistant-home-page proof-assistant-home-page
675,23911
(defcustom proof-context-command proof-context-command
681,24081
(defcustom proof-info-command proof-info-command
686,24215
(defcustom proof-showproof-command proof-showproof-command
693,24487
(defcustom proof-goal-command proof-goal-command
698,24623
(defcustom proof-save-command proof-save-command
706,24921
(defcustom proof-find-theorems-command proof-find-theorems-command
714,25231
(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default
721,25540
(defpgcustom toolbar-entries toolbar-entries
752,27272
(defcustom proof-assistant-true-value proof-assistant-true-value
770,27993
(defcustom proof-assistant-false-value proof-assistant-false-value
776,28183
(defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn
782,28377
(defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn
789,28626
(defcustom proof-assistant-setting-format proof-assistant-setting-format
796,28893
(defgroup proof-script proof-script
818,29588
(defcustom proof-terminal-char proof-terminal-char
823,29718
(defcustom proof-script-sexp-commands proof-script-sexp-commands
833,30122
(defcustom proof-script-command-end-regexp proof-script-command-end-regexp
844,30592
(defcustom proof-script-command-start-regexp proof-script-command-start-regexp
862,31411
(defcustom proof-script-use-old-parser proof-script-use-old-parser
873,31873
(defcustom proof-script-integral-proofs proof-script-integral-proofs
885,32362
(defcustom proof-script-fly-past-comments proof-script-fly-past-comments
900,33018
(defcustom proof-script-parse-function proof-script-parse-function
907,33335
(defcustom proof-script-comment-start proof-script-comment-start
925,33981
(defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp
936,34416
(defcustom proof-script-comment-end proof-script-comment-end
944,34733
(defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp
956,35151
(defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn
964,35462
(defcustom proof-string-start-regexp proof-string-start-regexp
970,35714
(defcustom proof-string-end-regexp proof-string-end-regexp
975,35879
(defcustom proof-case-fold-search proof-case-fold-search
980,36040
(defcustom proof-save-command-regexp proof-save-command-regexp
989,36456
(defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp
994,36567
(defcustom proof-save-with-hole-result proof-save-with-hole-result
1006,37019
(defcustom proof-goal-command-regexp proof-goal-command-regexp
1017,37483
(defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp
1026,37875
(defcustom proof-goal-with-hole-result proof-goal-with-hole-result
1038,38319
(defcustom proof-non-undoables-regexp proof-non-undoables-regexp
1048,38718
(defcustom proof-nested-undo-regexp proof-nested-undo-regexp
1059,39174
(defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count
1075,39886
(defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps
1083,40189
(defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn
1127,41923
(defcustom proof-script-imenu-generic-expression proof-script-imenu-generic-expression
1147,42753
(defcustom proof-goal-command-p proof-goal-command-p
1162,43414
(defcustom proof-really-save-command-p proof-really-save-command-p
1189,44850
(defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour
1201,45311
(defcustom proof-count-undos-fn proof-count-undos-fn
1229,46671
(defconst proof-no-command proof-no-command
1264,48272
(defcustom proof-find-and-forget-fn proof-find-and-forget-fn
1269,48476
(defcustom proof-forget-id-command proof-forget-id-command
1286,49187
(defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn
1296,49545
(defcustom proof-kill-goal-command proof-kill-goal-command
1308,50026
(defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd
1322,50536
(defcustom proof-nested-goals-history-p proof-nested-goals-history-p
1336,51085
(defcustom proof-state-preserving-p proof-state-preserving-p
1345,51423
(defcustom proof-activate-scripting-hook proof-activate-scripting-hook
1355,51893
(defcustom proof-deactivate-scripting-hook proof-deactivate-scripting-hook
1374,52671
(defcustom proof-indent proof-indent
1387,53036
(defcustom proof-indent-pad-eol proof-indent-pad-eol
1393,53210
(defcustom proof-indent-hang proof-indent-hang
1400,53450
(defcustom proof-indent-enclose-offset proof-indent-enclose-offset
1405,53576
(defcustom proof-indent-open-offset proof-indent-open-offset
1410,53718
(defcustom proof-indent-close-offset proof-indent-close-offset
1415,53855
(defcustom proof-indent-any-regexp proof-indent-any-regexp
1420,53993
(defcustom proof-indent-inner-regexp proof-indent-inner-regexp
1425,54153
(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp
1430,54307
(defcustom proof-indent-open-regexp proof-indent-open-regexp
1435,54461
(defcustom proof-indent-close-regexp proof-indent-close-regexp
1440,54613
(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords
1446,54767
(defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries
1454,55090
(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions
1472,55487
(defgroup proof-shell proof-shell
1498,56276
(defcustom proof-prog-name proof-prog-name
1508,56447
(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands
1517,56802
(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd
1526,57199
(defcustom proof-shell-init-cmd proof-shell-init-cmd
1540,57758
(defcustom proof-shell-restart-cmd proof-shell-restart-cmd
1551,58228
(defcustom proof-shell-quit-cmd proof-shell-quit-cmd
1556,58383
(defcustom proof-shell-quit-timeout proof-shell-quit-timeout
1561,58550
(defcustom proof-shell-cd-cmd proof-shell-cd-cmd
1571,58998
(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd
1588,59665
(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd
1597,60041
(defcustom proof-shell-silent-threshold proof-shell-silent-threshold
1606,60378
(defcustom  proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd
1614,60712
(defcustom  proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd
1635,61635
(defcustom proof-auto-multiple-files proof-auto-multiple-files
1663,62906
(defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files
1678,63627
(defcustom proof-shell-require-command-regexp proof-shell-require-command-regexp
1692,64294
(defcustom proof-done-advancing-require-function proof-done-advancing-require-function
1703,64756
(defcustom proof-shell-quiet-errors proof-shell-quiet-errors
1709,64996
(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern
1726,65334
(defcustom proof-shell-wakeup-char proof-shell-wakeup-char
1736,65756
(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp
1742,65987
(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp
1758,66627
(defcustom proof-shell-error-regexp proof-shell-error-regexp
1763,66762
(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error
1783,67556
(defcustom pg-next-error-regexp pg-next-error-regexp
1797,68099
(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp
1812,68709
(defcustom pg-next-error-extract-filename pg-next-error-extract-filename
1836,69747
(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp
1843,69990
(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp
1857,70582
(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp
1870,71090
(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp
1877,71389
(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp
1884,71682
(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp
1892,72049
(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start
1898,72291
(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length
1916,73029
(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end
1927,73456
(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp
1943,74132
(defcustom proof-shell-process-file proof-shell-process-file
1953,74544
(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp
1975,75496
(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list
1984,75832
(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify
1996,76377
(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp
2004,76701
(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd
2037,78173
(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd
2046,78503
(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd
2055,78859
(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp
2062,79119
(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split
2078,79779
(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd
2087,80204
(defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd
2094,80473
(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp
2117,81554
(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp
2133,82098
(defcustom proof-shell-filename-escapes proof-shell-filename-escapes
2145,82483
(defcustom proof-shell-process-connection-type proof-shell-process-connection-type
2162,83163
(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input
2185,84210
(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output
2197,84699
(defcustom proof-shell-insert-hook proof-shell-insert-hook
2205,85067
(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook
2245,87031
(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook
2261,87503
(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook
2267,87718
(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook
2282,88332
(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific
2292,88702
(defcustom proof-state-change-hook proof-state-change-hook
2311,89567
(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords
2322,89949
(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries
2330,90277
(defgroup proof-goals proof-goals
2348,90649
(defcustom pg-subterm-first-special-char pg-subterm-first-special-char
2353,90770
(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack
2361,91082
(defcustom pg-goals-change-goal pg-goals-change-goal
2370,91386
(defcustom pbp-goal-command pbp-goal-command
2375,91501
(defcustom pbp-hyp-command pbp-hyp-command
2380,91657
(defcustom pg-subterm-help-cmd pg-subterm-help-cmd
2385,91819
(defcustom pg-goals-error-regexp pg-goals-error-regexp
2392,92055
(defcustom proof-shell-result-start proof-shell-result-start
2397,92215
(defcustom proof-shell-result-end proof-shell-result-end
2403,92449
(defcustom pg-subterm-start-char pg-subterm-start-char
2409,92662
(defcustom pg-subterm-sep-char pg-subterm-sep-char
2423,93244
(defcustom pg-subterm-end-char pg-subterm-end-char
2429,93423
(defcustom pg-topterm-char pg-topterm-char
2435,93580
(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords
2452,94186
(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords
2466,94865
(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook
2478,95443
(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook
2486,95803
(defgroup proof-x-symbol proof-x-symbol
2498,96057
(defcustom proof-xsym-extra-modes proof-xsym-extra-modes
2503,96185
(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords
2516,96814
(defcustom proof-xsym-activate-command proof-xsym-activate-command
2524,97191
(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command
2531,97427
(defpgcustom x-symbol-language x-symbol-language
2538,97669
(defpgcustom favourites favourites
2553,98116
(defpgcustom menu-entries menu-entries
2558,98306
(defpgcustom help-menu-entries help-menu-entries
2565,98543
(defpgcustom keymap keymap
2572,98806
(defpgcustom completion-table completion-table
2577,98977
(defpgcustom tags-program tags-program
2587,99342
(defcustom proof-general-name proof-general-name
2599,99515
(defcustom proof-general-home-pageproof-general-home-page
2604,99672
(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name
2610,99831
(defcustom proof-universal-keysproof-universal-keys
2618,100107

generic/proof-depends.el,1325
(defvar proof-thm-names-of-files proof-thm-names-of-files
19,540
(defvar proof-def-names-of-files proof-def-names-of-files
25,824
(defun proof-depends-module-name-for-buffer proof-depends-module-name-for-buffer
34,1128
(defun proof-depends-module-of proof-depends-module-of
44,1570
(defun proof-depends-names-in-same-file proof-depends-names-in-same-file
52,1864
(defun proof-depends-process-dependencies proof-depends-process-dependencies
71,2484
(defun proof-dependency-in-span-context-menu proof-dependency-in-span-context-menu
124,4226
(defun proof-dep-alldeps-menu proof-dep-alldeps-menu
147,5129
(defun proof-dep-make-alldeps-menu proof-dep-make-alldeps-menu
153,5356
(defun proof-dep-split-deps proof-dep-split-deps
171,5852
(defun proof-dep-make-submenu proof-dep-make-submenu
192,6551
(defun proof-make-highlight-depts-menu proof-make-highlight-depts-menu
202,6904
(defun proof-goto-dependency proof-goto-dependency
212,7208
(defun proof-show-dependency proof-show-dependency
218,7431
(defconst pg-dep-span-priority pg-dep-span-priority
225,7721
(defconst pg-ordinary-span-priority pg-ordinary-span-priority
226,7757
(defun proof-highlight-depcs proof-highlight-depcs
228,7799
(defun proof-highlight-depts proof-highlight-depts
238,8229
(defun proof-dep-unhighlight proof-dep-unhighlight
249,8703

generic/proof-easy-config.el,317
(defconst proof-easy-config-derived-modes-tableproof-easy-config-derived-modes-table
15,492
(defun proof-easy-config-define-derived-modes proof-easy-config-define-derived-modes
22,898
(defun proof-easy-config-check-setup proof-easy-config-check-setup
59,2510
(defmacro proof-easy-config proof-easy-config
91,3835

generic/proof.el,809
(deflocal proof-buffer-type proof-buffer-type
35,900
(defvar proof-shell-busy proof-shell-busy
38,1013
(defvar proof-included-files-list proof-included-files-list
43,1169
(defvar proof-script-buffer proof-script-buffer
66,2185
(defvar proof-previous-script-buffer proof-previous-script-buffer
70,2325
(defvar proof-shell-buffer proof-shell-buffer
75,2579
(defvar proof-goals-buffer proof-goals-buffer
78,2665
(defvar proof-response-buffer proof-response-buffer
81,2720
(defvar proof-trace-buffer proof-trace-buffer
84,2781
(defvar proof-thms-buffer proof-thms-buffer
88,2935
(defvar proof-shell-error-or-interrupt-seen proof-shell-error-or-interrupt-seen
92,3090
(defvar proof-shell-proof-completed proof-shell-proof-completed
97,3315
(defvar proof-terminal-string proof-terminal-string
109,3860

generic/proof-indent.el,475
(defun proof-indent-indent proof-indent-indent
13,353
(defun proof-indent-offset proof-indent-offset
22,619
(defun proof-indent-inner-p proof-indent-inner-p
39,1219
(defun proof-indent-goto-prev proof-indent-goto-prev
48,1526
(defun proof-indent-calculate proof-indent-calculate
55,1859
(defun proof-indent-line proof-indent-line
74,2575
(defun proof-indent-pad-eol proof-indent-pad-eol
98,3376
(defun proof-indent-pad-eol-region proof-indent-pad-eol-region
116,3970

generic/proof-menu.el,4166
(defvar proof-display-some-buffers-count proof-display-some-buffers-count
19,467
(defun proof-display-some-buffers proof-display-some-buffers
21,512
(defun proof-menu-define-keys proof-menu-define-keys
80,2714
(define-key map map
83,2862
(define-key map map
84,2914
(define-key map map
85,2965
(define-key map map
86,3018
(define-key map map
87,3072
(define-key map map
88,3134
(define-key map map
89,3194
(define-key map map
90,3256
(define-key map map
92,3377
(define-key map map
93,3441
(define-key map map
96,3619
(define-key map map
97,3690
(define-key map map
98,3744
(define-key map map
99,3809
(define-key map map
100,3883
(define-key map map
103,4064
(define-key map map
104,4130
(define-key map map
106,4280
(define-key map map
107,4350
(define-key map map
108,4416
(define-key map map
110,4531
(define-key map map
111,4594
(define-key map map
113,4679
(define-key map map
120,5005
(define-key map map
121,5064
(defun proof-menu-define-main proof-menu-define-main
141,5654
(defun proof-menu-define-specific proof-menu-define-specific
151,5855
(defun proof-assistant-menu-update proof-assistant-menu-update
186,6872
(defvar proof-help-menuproof-help-menu
200,7303
(defvar proof-show-hide-menuproof-show-hide-menu
208,7581
(defvar proof-buffer-menuproof-buffer-menu
217,7894
(defconst proof-quick-opts-menuproof-quick-opts-menu
272,9886
(defun proof-quick-opts-vars proof-quick-opts-vars
380,14317
(defun proof-quick-opts-changed-from-defaults-p proof-quick-opts-changed-from-defaults-p
403,14999
(defun proof-quick-opts-changed-from-saved-p proof-quick-opts-changed-from-saved-p
407,15104
(defun proof-quick-opts-save proof-quick-opts-save
418,15456
(defun proof-quick-opts-reset proof-quick-opts-reset
423,15624
(defconst proof-config-menuproof-config-menu
435,15892
(defconst proof-advanced-menuproof-advanced-menu
442,16071
(defvar proof-menu proof-menu
458,16650
(defvar proof-main-menuproof-main-menu
467,16934
(defvar proof-aux-menuproof-aux-menu
477,17160
(defvar proof-menu-favourites proof-menu-favourites
493,17482
(defun proof-menu-define-favourites-menu proof-menu-define-favourites-menu
496,17589
(defmacro proof-defshortcut proof-defshortcut
517,18260
(defmacro proof-definvisible proof-definvisible
533,18915
(defun proof-def-favourite proof-def-favourite
554,19740
(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history
577,20715
(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history
580,20800
(defun proof-save-favourites proof-save-favourites
583,20886
(defun proof-del-favourite proof-del-favourite
588,21034
(defun proof-read-favourite proof-read-favourite
605,21595
(defun proof-add-favourite proof-add-favourite
630,22398
(defvar proof-assistant-settings proof-assistant-settings
657,23449
(defvar proof-menu-settings proof-menu-settings
664,23812
(defun proof-menu-define-settings-menu proof-menu-define-settings-menu
667,23886
(defun proof-menu-entry-name proof-menu-entry-name
687,24630
(defun proof-menu-entry-for-setting proof-menu-entry-for-setting
699,25102
(defun proof-settings-vars proof-settings-vars
717,25592
(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p
722,25769
(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p
726,25875
(defun proof-settings-save proof-settings-save
730,25978
(defun proof-settings-reset proof-settings-reset
735,26145
(defun proof-defpacustom-fn proof-defpacustom-fn
743,26391
(defmacro defpacustom defpacustom
819,29275
(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs
830,29916
(defun proof-maybe-askprefs proof-maybe-askprefs
852,30891
(defun proof-assistant-settings-cmd proof-assistant-settings-cmd
859,31095
(defun proof-assistant-format proof-assistant-format
876,31755
(defvar proof-assistant-format-table proof-assistant-format-table
900,32814
(defun proof-assistant-format-bool proof-assistant-format-bool
908,33183
(defun proof-assistant-format-int proof-assistant-format-int
911,33296
(defun proof-assistant-format-string proof-assistant-format-string
914,33388

generic/proof-mmm.el,179
(defun proof-mmm-support-available proof-mmm-support-available
25,909
(defun proof-mmm-set-global proof-mmm-set-global
49,1757
(defun proof-mmm-enable proof-mmm-enable
64,2298

generic/proof-script.el,8107
(defvar proof-last-theorem-dependencies proof-last-theorem-dependencies
41,1046
(defvar proof-nesting-depth proof-nesting-depth
45,1208
(defvar proof-element-counters proof-element-counters
52,1439
(deflocal proof-active-buffer-fake-minor-mode proof-active-buffer-fake-minor-mode
58,1579
(deflocal proof-script-buffer-file-name proof-script-buffer-file-name
61,1705
(defun proof-next-element-count proof-next-element-count
75,2229
(defun proof-element-id proof-element-id
84,2556
(defun proof-next-element-id proof-next-element-id
88,2725
(deflocal proof-script-last-entity proof-script-last-entity
102,3041
(defun proof-script-find-next-entity proof-script-find-next-entity
109,3321
(deflocal proof-locked-span proof-locked-span
185,6063
(deflocal proof-queue-span proof-queue-span
192,6329
(defun proof-span-read-only proof-span-read-only
204,6843
(defun proof-strict-read-only proof-strict-read-only
211,7100
(defsubst proof-set-queue-endpoints proof-set-queue-endpoints
230,7987
(defsubst proof-set-locked-endpoints proof-set-locked-endpoints
234,8128
(defsubst proof-detach-queue proof-detach-queue
238,8272
(defsubst proof-detach-locked proof-detach-locked
242,8404
(defsubst proof-set-queue-start proof-set-queue-start
246,8540
(defsubst proof-set-locked-end proof-set-locked-end
250,8666
(defsubst proof-set-queue-end proof-set-queue-end
265,9213
(defun proof-init-segmentation proof-init-segmentation
275,9469
(defun proof-restart-buffers proof-restart-buffers
307,10840
(defun proof-script-buffers-with-spans proof-script-buffers-with-spans
329,11762
(defun proof-script-remove-all-spans-and-deactivate proof-script-remove-all-spans-and-deactivate
339,12118
(defun proof-script-clear-queue-spans proof-script-clear-queue-spans
343,12306
(defun proof-unprocessed-begin proof-unprocessed-begin
361,12847
(defun proof-script-end proof-script-end
369,13101
(defun proof-queue-or-locked-end proof-queue-or-locked-end
378,13402
(defun proof-locked-end proof-locked-end
392,14065
(defun proof-locked-region-full-p proof-locked-region-full-p
408,14435
(defun proof-locked-region-empty-p proof-locked-region-empty-p
416,14692
(defun proof-only-whitespace-to-locked-region-p proof-only-whitespace-to-locked-region-p
420,14842
(defun proof-in-locked-region-p proof-in-locked-region-p
433,15478
(defun proof-goto-end-of-locked proof-goto-end-of-locked
445,15741
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window
462,16500
(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
473,16981
(defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p
487,17634
(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible
496,18085
(defvar pg-idioms pg-idioms
515,18735
(defvar pg-visibility-specs pg-visibility-specs
518,18831
(deflocal pg-script-portions pg-script-portions
523,19038
(defun pg-clear-script-portions pg-clear-script-portions
526,19160
(defun pg-add-script-element pg-add-script-element
544,19824
(defun pg-remove-script-element pg-remove-script-element
547,19900
(defsubst pg-visname pg-visname
555,20178
(defun pg-add-element pg-add-element
559,20323
(defun pg-open-invisible-span pg-open-invisible-span
593,21952
(defun pg-remove-element pg-remove-element
604,22315
(defun pg-make-element-invisible pg-make-element-invisible
611,22585
(defun pg-make-element-visible pg-make-element-visible
617,22842
(defun pg-toggle-element-visibility pg-toggle-element-visibility
622,23021
(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs
630,23351
(defun pg-show-all-portions pg-show-all-portions
637,23622
(defun pg-show-all-proofs pg-show-all-proofs
655,24293
(defun pg-hide-all-proofs pg-hide-all-proofs
660,24421
(defun pg-add-proof-element pg-add-proof-element
665,24552
(defun pg-span-name pg-span-name
679,25172
(defun pg-set-span-helphighlights pg-set-span-helphighlights
700,25879
(defun proof-complete-buffer-atomic proof-complete-buffer-atomic
725,26703
(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file
766,28618
(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted
817,30746
(defun proof-auto-retract-dependencies proof-auto-retract-dependencies
836,31532
(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name
890,34072
(defun proof-protected-process-or-retract proof-protected-process-or-retract
936,35895
(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto
963,37065
(defun proof-deactivate-scripting proof-deactivate-scripting
972,37423
(defun proof-activate-scripting proof-activate-scripting
1109,42828
(defun proof-toggle-active-scripting proof-toggle-active-scripting
1237,48582
(defun proof-done-advancing proof-done-advancing
1278,49943
(defun proof-done-advancing-comment proof-done-advancing-comment
1363,53348
(defun proof-done-advancing-save proof-done-advancing-save
1382,54090
(defun proof-make-goalsave proof-make-goalsave
1475,57703
(defun proof-get-name-from-goal proof-get-name-from-goal
1490,58446
(defun proof-done-advancing-autosave proof-done-advancing-autosave
1509,59472
(defun proof-done-advancing-other proof-done-advancing-other
1573,61989
(defun proof-segment-up-to-parser proof-segment-up-to-parser
1601,62969
(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end
1664,65045
(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend
1673,65461
(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart
1698,66356
(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp
1761,69064
(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd
1785,70000
(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart
1837,72199
(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend
1898,74559
(defun proof-semis-to-vanillas proof-semis-to-vanillas
1969,77206
(defun proof-script-new-command-advance proof-script-new-command-advance
2008,78532
(defun proof-script-next-command-advance proof-script-next-command-advance
2050,80273
(defun proof-assert-until-point-interactive proof-assert-until-point-interactive
2062,80714
(defun proof-assert-until-point proof-assert-until-point
2088,81836
(defun proof-assert-next-commandproof-assert-next-command
2141,84268
(defun proof-goto-point proof-goto-point
2189,86531
(defun proof-insert-pbp-command proof-insert-pbp-command
2206,87057
(defun proof-done-retracting proof-done-retracting
2238,88130
(defun proof-setup-retract-action proof-setup-retract-action
2265,89241
(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave
2275,89724
(defun proof-retract-target proof-retract-target
2299,90593
(defun proof-retract-until-point-interactive proof-retract-until-point-interactive
2384,94234
(defun proof-retract-until-point proof-retract-until-point
2392,94619
(define-derived-mode proof-mode proof-mode
2437,96480
(defun proof-script-set-visited-file-name proof-script-set-visited-file-name
2473,97966
(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks
2497,98968
(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn
2507,99464
(defun proof-config-done-related proof-config-done-related
2551,101286
(defun proof-generic-goal-command-p proof-generic-goal-command-p
2623,103854
(defun proof-generic-state-preserving-p proof-generic-state-preserving-p
2627,104029
(defun proof-generic-count-undos proof-generic-count-undos
2636,104546
(defun proof-generic-find-and-forget proof-generic-find-and-forget
2665,105576
(defconst proof-script-important-settingsproof-script-important-settings
2716,107401
(defun proof-config-done proof-config-done
2729,107938
(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism
2826,111486
(defun proof-setup-imenu proof-setup-imenu
2870,113339
(defun proof-setup-func-menu proof-setup-func-menu
2887,113944

generic/proof-shell.el,5296
(defvar proof-shell-last-output proof-shell-last-output
19,464
(defvar proof-marker proof-marker
63,1720
(defvar proof-action-list proof-action-list
66,1817
(defvar proof-shell-silent proof-shell-silent
74,1993
(defvar proof-shell-last-prompt proof-shell-last-prompt
88,2476
(defvar proof-shell-last-output-kind proof-shell-last-output-kind
93,2706
(defvar proof-shell-delayed-output proof-shell-delayed-output
114,3528
(defvar proof-shell-delayed-output-kind proof-shell-delayed-output-kind
117,3649
(defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator
126,3852
(defun proof-shell-ready-prover proof-shell-ready-prover
179,5328
(defun proof-shell-live-buffer proof-shell-live-buffer
193,5868
(defun proof-shell-available-p proof-shell-available-p
200,6103
(defun proof-grab-lock proof-grab-lock
206,6326
(defun proof-release-lock proof-release-lock
223,7043
(defcustom proof-shell-fiddle-frames proof-shell-fiddle-frames
243,7599
(deflocal proof-eagerly-raise proof-eagerly-raise
250,7840
(defun proof-shell-start proof-shell-start
253,7946
(defvar proof-shell-kill-function-hooks proof-shell-kill-function-hooks
445,15498
(defun proof-shell-kill-function proof-shell-kill-function
448,15596
(defun proof-shell-clear-state proof-shell-clear-state
539,19456
(defun proof-shell-exit proof-shell-exit
554,19899
(defun proof-shell-bail-out proof-shell-bail-out
566,20344
(defun proof-shell-restart proof-shell-restart
575,20821
(defvar proof-shell-no-response-display proof-shell-no-response-display
617,22205
(defvar proof-shell-urgent-message-marker proof-shell-urgent-message-marker
620,22309
(defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner
623,22430
(defun proof-shell-handle-output proof-shell-handle-output
627,22557
(defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output
700,25880
(defvar proof-shell-no-error-display proof-shell-no-error-display
735,27302
(defun proof-shell-handle-error proof-shell-handle-error
741,27508
(defun proof-shell-handle-interrupt proof-shell-handle-interrupt
759,28344
(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action
773,28966
(defun proof-goals-pos proof-goals-pos
800,30171
(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal
805,30376
(defsubst proof-shell-string-match-safe proof-shell-string-match-safe
817,30911
(defun proof-shell-process-output proof-shell-process-output
822,31079
(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge
933,35719
(defun proof-shell-insert proof-shell-insert
942,36028
(defun proof-shell-command-queue-item proof-shell-command-queue-item
1016,38940
(defun proof-shell-set-silent proof-shell-set-silent
1021,39097
(defun proof-shell-start-silent-item proof-shell-start-silent-item
1027,39316
(defun proof-shell-clear-silent proof-shell-clear-silent
1033,39508
(defun proof-shell-stop-silent-item proof-shell-stop-silent-item
1039,39730
(defun proof-shell-should-be-silent proof-shell-should-be-silent
1046,40002
(defun proof-append-alist proof-append-alist
1059,40558
(defun proof-start-queue proof-start-queue
1115,42685
(defun proof-extend-queue proof-extend-queue
1126,43034
(defun proof-shell-exec-loop proof-shell-exec-loop
1137,43415
(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd
1202,46003
(defun proof-shell-message proof-shell-message
1239,47711
(defun proof-shell-process-urgent-message proof-shell-process-urgent-message
1245,47927
(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history
1453,56775
(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input
1455,56845
(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages
1467,57215
(defun proof-shell-filter proof-shell-filter
1539,60385
(defun proof-shell-filter-process-output proof-shell-filter-process-output
1692,66722
(defvar pg-last-tracing-output-time pg-last-tracing-output-time
1745,68776
(defvar pg-tracing-slow-mode pg-tracing-slow-mode
1748,68882
(defconst pg-slow-mode-duration pg-slow-mode-duration
1751,68971
(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold
1754,69053
(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer
1757,69181
(defun pg-tracing-tight-loop pg-tracing-tight-loop
1759,69220
(defun pg-finish-tracing-display pg-finish-tracing-display
1802,70938
(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations
1815,71244
(defun proof-shell-show-annotations proof-shell-show-annotations
1831,71779
(defun proof-shell-wait proof-shell-wait
1852,72276
(defun proof-done-invisible proof-done-invisible
1872,73186
(defun proof-shell-invisible-command proof-shell-invisible-command
1915,74909
(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result
1948,76159
(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result
1965,76840
(define-derived-mode proof-shell-mode proof-shell-mode
1985,77344
(defconst proof-shell-important-settingsproof-shell-important-settings
2053,79897
(defun proof-shell-config-done proof-shell-config-done
2058,79997

generic/proof-site.el,1030
(defgroup proof-general proof-general
20,594
(defgroup proof-general-internals proof-general-internals
33,1010
(defun proof-home-directory-fn proof-home-directory-fn
42,1203
(defcustom proof-home-directoryproof-home-directory
53,1573
(defcustom proof-images-directoryproof-images-directory
62,1939
(defcustom proof-info-directoryproof-info-directory
68,2140
(defcustom proof-assistant-tableproof-assistant-table
97,3389
(defun proof-string-to-list proof-string-to-list
163,5571
(defcustom proof-assistants proof-assistants
179,6062
(defun proof-ready-for-assistant proof-ready-for-assistant
215,7475
(defconst proof-general-version proof-general-version
328,11684
(defconst proof-general-short-version proof-general-short-version
331,11825
(defcustom proof-assistant-cusgrp proof-assistant-cusgrp
348,12407
(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp
356,12710
(defcustom proof-assistant proof-assistant
364,13022
(defcustom proof-assistant-symbol proof-assistant-symbol
372,13291

generic/proof-splash.el,1149
(defcustom proof-splash-enable proof-splash-enable
14,379
(defcustom proof-splash-time proof-splash-time
19,531
(defcustom proof-splash-contentsproof-splash-contents
27,816
(defconst proof-splash-startup-msg proof-splash-startup-msg
56,1895
(defconst proof-splash-welcome proof-splash-welcome
65,2274
(defun proof-get-image proof-get-image
84,2838
(defvar proof-splash-timeout-conf proof-splash-timeout-conf
136,4662
(defun proof-splash-centre-spaces proof-splash-centre-spaces
139,4775
(defun proof-splash-remove-screen proof-splash-remove-screen
167,5944
(defun proof-splash-remove-buffer proof-splash-remove-buffer
188,6693
(defvar proof-splash-seen proof-splash-seen
204,7357
(defun proof-splash-display-screen proof-splash-display-screen
208,7474
(defun proof-splash-message proof-splash-message
283,10633
(defun proof-splash-timeout-waiter proof-splash-timeout-waiter
293,10996
(defvar proof-splash-old-frame-title-format proof-splash-old-frame-title-format
310,11735
(defun proof-splash-set-frame-titles proof-splash-set-frame-titles
312,11785
(defun proof-splash-unset-frame-titles proof-splash-unset-frame-titles
321,12101

generic/proof-syntax.el,1297
(defun proof-ids-to-regexp proof-ids-to-regexp
16,445
(defun proof-anchor-regexp proof-anchor-regexp
22,701
(defconst proof-no-regexpproof-no-regexp
26,803
(defun proof-regexp-alt proof-regexp-alt
31,898
(defun proof-regexp-region proof-regexp-region
40,1184
(defun proof-re-search-forward-region proof-re-search-forward-region
49,1607
(defun proof-re-search-forward proof-re-search-forward
62,2102
(defun proof-re-search-backward proof-re-search-backward
68,2363
(defun proof-string-match proof-string-match
74,2627
(defun proof-string-match-safe proof-string-match-safe
80,2859
(defun proof-stringfn-match proof-stringfn-match
84,3064
(defun proof-looking-at proof-looking-at
91,3324
(defun proof-looking-at-safe proof-looking-at-safe
97,3514
(defun proof-looking-at-syntactic-context proof-looking-at-syntactic-context
101,3654
(defun proof-replace-string proof-replace-string
113,3986
(defun proof-replace-regexp proof-replace-regexp
118,4171
(defvar proof-id proof-id
126,4384
(defun proof-ids proof-ids
132,4604
(defun proof-zap-commas proof-zap-commas
145,5165
(defun proof-format proof-format
163,5728
(defun proof-format-filename proof-format-filename
182,6367
(defun proof-insert proof-insert
231,7845
(defun proof-splice-separator proof-splice-separator
267,8854

generic/proof-system.el,0

generic/proof-toolbar.el,3888
(defun proof-toolbar-function proof-toolbar-function
57,1920
(defun proof-toolbar-icon proof-toolbar-icon
60,2017
(defun proof-toolbar-enabler proof-toolbar-enabler
63,2118
(defun proof-toolbar-function-with-enabler proof-toolbar-function-with-enabler
66,2226
(defun proof-toolbar-make-icon proof-toolbar-make-icon
73,2399
(defun proof-toolbar-make-toolbar-item proof-toolbar-make-toolbar-item
91,2999
(defvar proof-toolbar proof-toolbar
130,4380
(deflocal proof-toolbar-itimer proof-toolbar-itimer
134,4509
(defun proof-toolbar-setup proof-toolbar-setup
138,4619
(defun proof-toolbar-build proof-toolbar-build
183,6235
(defalias 'proof-toolbar-enable proof-toolbar-enable
257,8796
(defun proof-toolbar-setup-refresh proof-toolbar-setup-refresh
266,9035
(defun proof-toolbar-disable-refresh proof-toolbar-disable-refresh
287,9805
(deflocal proof-toolbar-refresh-flag proof-toolbar-refresh-flag
294,10127
(defun proof-toolbar-refresh proof-toolbar-refresh
300,10398
(defvar proof-toolbar-enablersproof-toolbar-enablers
304,10543
(defvar proof-toolbar-enablers-last-stateproof-toolbar-enablers-last-state
310,10719
(defun proof-toolbar-really-refresh proof-toolbar-really-refresh
314,10810
(defun proof-toolbar-undo-enable-p proof-toolbar-undo-enable-p
367,12640
(defalias 'proof-toolbar-undo proof-toolbar-undo
372,12788
(defun proof-toolbar-delete-enable-p proof-toolbar-delete-enable-p
378,12907
(defalias 'proof-toolbar-delete proof-toolbar-delete
384,13081
(defun proof-toolbar-lockedend-enable-p proof-toolbar-lockedend-enable-p
391,13217
(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
394,13267
(defun proof-toolbar-next-enable-p proof-toolbar-next-enable-p
403,13355
(defalias 'proof-toolbar-next proof-toolbar-next
407,13462
(defun proof-toolbar-goto-enable-p proof-toolbar-goto-enable-p
414,13556
(defalias 'proof-toolbar-goto proof-toolbar-goto
417,13629
(defun proof-toolbar-retract-enable-p proof-toolbar-retract-enable-p
424,13705
(defalias 'proof-toolbar-retract proof-toolbar-retract
428,13816
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
435,13895
(defalias 'proof-toolbar-use proof-toolbar-use
436,13963
(defun proof-toolbar-restart-enable-p proof-toolbar-restart-enable-p
442,14041
(defalias 'proof-toolbar-restart proof-toolbar-restart
447,14202
(defun proof-toolbar-goal-enable-p proof-toolbar-goal-enable-p
453,14280
(defalias 'proof-toolbar-goal proof-toolbar-goal
460,14513
(defun proof-toolbar-qed-enable-p proof-toolbar-qed-enable-p
467,14585
(defalias 'proof-toolbar-qed proof-toolbar-qed
473,14737
(defun proof-toolbar-state-enable-p proof-toolbar-state-enable-p
479,14809
(defalias 'proof-toolbar-state proof-toolbar-state
482,14880
(defun proof-toolbar-context-enable-p proof-toolbar-context-enable-p
488,14949
(defalias 'proof-toolbar-context proof-toolbar-context
491,15022
(defun proof-toolbar-info-enable-p proof-toolbar-info-enable-p
499,15182
(defalias 'proof-toolbar-info proof-toolbar-info
502,15226
(defun proof-toolbar-command-enable-p proof-toolbar-command-enable-p
508,15295
(defalias 'proof-toolbar-command proof-toolbar-command
511,15366
(defun proof-toolbar-help-enable-p proof-toolbar-help-enable-p
517,15446
(defun proof-toolbar-help proof-toolbar-help
520,15491
(defun proof-toolbar-find-enable-p proof-toolbar-find-enable-p
528,15585
(defalias 'proof-toolbar-find proof-toolbar-find
531,15654
(defun proof-toolbar-visibility-enable-p proof-toolbar-visibility-enable-p
537,15752
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
540,15852
(defun proof-toolbar-interrupt-enable-p proof-toolbar-interrupt-enable-p
546,15940
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
549,16004
(defun proof-toolbar-make-menu-item proof-toolbar-make-menu-item
558,16193
(defconst proof-toolbar-scripting-menuproof-toolbar-scripting-menu
580,16881

generic/proof-utils.el,3150
(defmacro deflocal deflocal
18,471
(defmacro proof-with-current-buffer-if-exists proof-with-current-buffer-if-exists
25,709
(defmacro proof-with-script-buffer proof-with-script-buffer
34,1086
(defmacro proof-map-buffers proof-map-buffers
45,1473
(defmacro proof-sym proof-sym
50,1658
(defun proof-try-require proof-try-require
55,1819
(defun proof-save-some-buffers proof-save-some-buffers
68,2147
(defun proof-set-value proof-set-value
92,2838
(defun proof-ass-symv proof-ass-symv
152,5015
(defmacro proof-ass-sym proof-ass-sym
157,5202
(defun proof-defpgcustom-fn proof-defpgcustom-fn
161,5341
(defun undefpgcustom undefpgcustom
186,6425
(defmacro defpgcustom defpgcustom
192,6649
(defmacro proof-ass proof-ass
201,7066
(defun proof-defpgdefault-fn proof-defpgdefault-fn
206,7242
(defmacro defpgdefault defpgdefault
220,7701
(defmacro defpgfun defpgfun
231,8063
(defun proof-file-truename proof-file-truename
246,8357
(defun proof-file-to-buffer proof-file-to-buffer
250,8540
(defun proof-files-to-buffers proof-files-to-buffers
261,8869
(defun proof-buffers-in-mode proof-buffers-in-mode
268,9152
(defun pg-save-from-death pg-save-from-death
282,9603
(defun proof-define-keys proof-define-keys
301,10213
(deflocal proof-font-lock-keywords proof-font-lock-keywords
330,11214
(deflocal proof-font-lock-keywords-case-fold-search proof-font-lock-keywords-case-fold-search
336,11479
(defun proof-font-lock-configure-defaults proof-font-lock-configure-defaults
339,11602
(defun proof-font-lock-clear-font-lock-vars proof-font-lock-clear-font-lock-vars
387,13915
(defun proof-font-lock-set-font-lock-vars proof-font-lock-set-font-lock-vars
398,14288
(defun proof-fontify-region proof-fontify-region
405,14501
(defconst pg-special-char-regexp pg-special-char-regexp
464,16730
(defun pg-remove-specials pg-remove-specials
468,16842
(defun proof-fontify-buffer proof-fontify-buffer
482,17267
(defun proof-warn-if-unset proof-warn-if-unset
495,17508
(defun proof-get-window-for-buffer proof-get-window-for-buffer
500,17726
(defun proof-display-and-keep-buffer proof-display-and-keep-buffer
537,19364
(defun proof-clean-buffer proof-clean-buffer
569,20673
(defun proof-message proof-message
583,21210
(defun proof-warning proof-warning
588,21423
(defun pg-internal-warning pg-internal-warning
594,21705
(defun proof-debug proof-debug
602,22024
(defun proof-switch-to-buffer proof-switch-to-buffer
617,22707
(defun proof-resize-window-tofit proof-resize-window-tofit
650,24399
(defun proof-submit-bug-report proof-submit-bug-report
750,28411
(defun proof-deftoggle-fn proof-deftoggle-fn
775,29277
(defmacro proof-deftoggle proof-deftoggle
790,29932
(defun proof-defintset-fn proof-defintset-fn
797,30306
(defmacro proof-defintset proof-defintset
811,30961
(defun proof-defstringset-fn proof-defstringset-fn
818,31338
(defmacro proof-defstringset proof-defstringset
831,31965
(defun pg-custom-save-vars pg-custom-save-vars
845,32430
(defun pg-custom-reset-vars pg-custom-reset-vars
863,33156
(defun proof-locate-executable proof-locate-executable
876,33493
(defconst proof-extra-flsproof-extra-fls
905,34674

generic/proof-x-symbol.el,960
(defvar proof-x-symbol-initialized proof-x-symbol-initialized
54,2151
(defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file
57,2246
(defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available
63,2428
(defun proof-x-symbol-initialize proof-x-symbol-initialize
83,3173
(defun proof-x-symbol-enable proof-x-symbol-enable
178,7036
(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers
208,8353
(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers
223,9107
(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
245,9811
(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input
247,9877
(defun proof-x-symbol-set-language proof-x-symbol-set-language
264,10468
(defun proof-x-symbol-shell-config proof-x-symbol-shell-config
269,10639
(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer
317,12806

hol98/hol98.el,0

hol98/x-symbol-hol98.el,0

isa/interface-setup.el,0

isa/isabelle-system.el,3268
(defconst isa-running-isar isa-running-isar
17,537
(defgroup isabelle isabelle
23,719
(defcustom isabelle-web-pageisabelle-web-page
27,848
(defcustom isa-isatool-commandisa-isatool-command
38,1143
(defvar isatool-not-found isatool-not-found
65,2088
(defun isa-set-isatool-command isa-set-isatool-command
68,2201
(defun isa-shell-command-to-string isa-shell-command-to-string
88,2985
(defun isa-getenv isa-getenv
94,3209
(defcustom isabelle-program-name isabelle-program-name
113,3866
(defvar isabelle-prog-name isabelle-prog-name
139,4814
(defun isabelle-command-line isabelle-command-line
142,4941
(defun isabelle-choose-logic isabelle-choose-logic
165,5849
(defun isa-tool-list-logics isa-tool-list-logics
187,6821
(defun isa-view-doc isa-view-doc
194,7059
(defvar isabelle-version-string isabelle-version-string
201,7283
(defun isa-version isa-version
203,7324
(defconst isa-supports-pgip isa-supports-pgip
216,7807
(defun isa-tool-list-docs isa-tool-list-docs
224,8037
(defun isa-quit isa-quit
242,8759
(defconst isabelle-verbatim-regexp isabelle-verbatim-regexp
249,8954
(defun isabelle-verbatim isabelle-verbatim
252,9095
(defcustom isabelle-refresh-logics isabelle-refresh-logics
268,9686
(defcustom isabelle-logics-available isabelle-logics-available
276,10013
(defcustom isabelle-chosen-logic isabelle-chosen-logic
284,10313
(defconst isabelle-docs-menu isabelle-docs-menu
297,10781
(defun isabelle-logics-menu-calculate isabelle-logics-menu-calculate
307,11174
(defvar isabelle-time-to-refresh-logics isabelle-time-to-refresh-logics
323,11683
(defun isabelle-logics-menu-refresh isabelle-logics-menu-refresh
326,11776
(defun isabelle-logics-menu-filter isabelle-logics-menu-filter
343,12475
(defun isabelle-menu-bar-update-logics isabelle-menu-bar-update-logics
349,12685
(defvar isabelle-logics-menu-entries isabelle-logics-menu-entries
360,13041
(defvar isabelle-logics-menu isabelle-logics-menu
362,13113
(defun isabelle-load-isar-keywords isabelle-load-isar-keywords
375,13731
(defpacustom show-types show-types
402,14686
(defpacustom show-sorts show-sorts
407,14802
(defpacustom show-consts show-consts
412,14918
(defpacustom long-names long-names
417,15052
(defpacustom eta-contract eta-contract
422,15184
(defpacustom trace-simplifier trace-simplifier
427,15325
(defpacustom trace-rules trace-rules
432,15457
(defpacustom quick-and-dirty quick-and-dirty
437,15589
(defpacustom full-proofs full-proofs
442,15725
(defpacustom global-timing global-timing
448,16034
(defpacustom theorem-dependencies theorem-dependencies
454,16192
(defpacustom goals-limit goals-limit
460,16457
(defpacustom prems-limit prems-limit
465,16596
(defpacustom print-depth print-depth
470,16756
(defpgdefault menu-entriesmenu-entries
482,17045
(defpgdefault help-menu-entries help-menu-entries
489,17207
(defpgdefault x-symbol-language x-symbol-language
497,17401
(defun isabelle-convert-idmarkup-to-subterm isabelle-convert-idmarkup-to-subterm
520,18016
(defun isabelle-create-span-menu isabelle-create-span-menu
545,19055
(defun isabelle-xml-sml-escapes isabelle-xml-sml-escapes
562,19549
(defun isabelle-process-pgip isabelle-process-pgip
565,19650
(defun isabelle-parse-syntax-dump isabelle-parse-syntax-dump
582,20236

isa/isa.el,2283
(defcustom isa-outline-regexpisa-outline-regexp
43,1354
(defcustom isa-outline-heading-end-regexp isa-outline-heading-end-regexp
50,1591
(defvar isa-shell-outline-regexp isa-shell-outline-regexp
55,1743
(defvar isa-shell-outline-heading-end-regexp isa-shell-outline-heading-end-regexp
56,1805
(defun isa-mode-config-set-variables isa-mode-config-set-variables
59,1857
(defun isa-shell-mode-config-set-variables isa-shell-mode-config-set-variables
141,5266
(defun isa-update-thy-only isa-update-thy-only
283,11186
(defun isa-shell-update-thy isa-shell-update-thy
295,11694
(defun isa-remove-file isa-remove-file
320,12897
(defun isa-shell-compute-new-files-list isa-shell-compute-new-files-list
330,13215
(define-derived-mode isa-shell-mode isa-shell-mode
346,13727
(define-derived-mode isa-response-mode isa-response-mode
351,13852
(define-derived-mode isa-goals-mode isa-goals-mode
356,14021
(define-derived-mode isa-proofscript-mode isa-proofscript-mode
361,14178
(defun isa-mode isa-mode
370,14359
(define-key map map
414,15899
(define-key map map
415,15949
(defun isa-process-thy-file isa-process-thy-file
419,16106
(defcustom isa-retract-thy-file-command isa-retract-thy-file-command
425,16315
(defun isa-retract-thy-file isa-retract-thy-file
431,16552
(defgroup thy thy
447,17181
(defun isa-splice-separator isa-splice-separator
459,17511
(defun isa-file-name-cons-extension isa-file-name-cons-extension
468,17763
(defun isa-format isa-format
475,18029
(define-key isa-proofscript-mode-map isa-proofscript-mode-map
487,18404
(defcustom isa-not-undoable-commands-regexpisa-not-undoable-commands-regexp
497,18537
(defun isa-count-undos isa-count-undos
504,18790
(defun isa-goal-command-p isa-goal-command-p
534,19955
(defun isa-find-and-forget isa-find-and-forget
547,20600
(defun isa-state-preserving-p isa-state-preserving-p
550,20655
(defun isa-pre-shell-start isa-pre-shell-start
559,21023
(defun isa-mode-config isa-mode-config
566,21300
(defun isa-shell-mode-config isa-shell-mode-config
594,22443
(defun isa-response-mode-config isa-response-mode-config
601,22692
(defun isa-goals-mode-config isa-goals-mode-config
606,22853
(defun isa-preprocessing isa-preprocessing
614,23177
(defpgdefault completion-tablecompletion-table
628,23681

isa/isa-syntax.el,3046
(defun isa-init-syntax-table isa-init-syntax-table
14,312
(defun isa-init-output-syntax-table isa-init-output-syntax-table
34,960
(defgroup isa-syntax isa-syntax
71,2172
(defcustom isa-keywords-defnisa-keywords-defn
75,2274
(defcustom isa-keywords-goalisa-keywords-goal
82,2469
(defcustom isa-keywords-saveisa-keywords-save
88,2676
(defcustom isa-keywords-commandsisa-keywords-commands
97,2968
(defcustom isa-keywords-smlisa-keywords-sml
109,3357
(defcustom isa-keyword-symbolsisa-keyword-symbols
119,3826
(defcustom isa-sml-names-keywordsisa-sml-names-keywords
125,4021
(defcustom isa-sml-typenames-keywordsisa-sml-typenames-keywords
131,4194
(defconst isa-keywordsisa-keywords
140,4490
(defconst isa-keywords-proof-commandsisa-keywords-proof-commands
146,4671
(defconst isa-tacticalsisa-tacticals
151,4865
(defconst isa-id isa-id
159,5132
(defconst isa-idx isa-idx
160,5181
(defconst isa-ids isa-ids
162,5236
(defconst isa-string isa-string
165,5347
(defcustom isa-save-command-regexpisa-save-command-regexp
167,5406
(defconst isa-save-with-hole-regexpisa-save-with-hole-regexp
181,5810
(defcustom isa-goal-command-regexpisa-goal-command-regexp
185,5945
(defconst isa-string-regexpisa-string-regexp
197,6329
(defconst isa-goal-with-hole-regexpisa-goal-with-hole-regexp
201,6460
(defconst isa-proof-command-regexpisa-proof-command-regexp
209,6702
(defface isabelle-class-name-faceisabelle-class-name-face
216,6913
(defface isabelle-tfree-name-faceisabelle-tfree-name-face
226,7198
(defface isabelle-tvar-name-faceisabelle-tvar-name-face
236,7485
(defface isabelle-free-name-faceisabelle-free-name-face
246,7775
(defface isabelle-bound-name-faceisabelle-bound-name-face
256,8061
(defface isabelle-var-name-faceisabelle-var-name-face
266,8350
(defface isabelle-sml-symbol-faceisabelle-sml-symbol-face
277,8687
(defconst isabelle-class-name-face isabelle-class-name-face
287,9063
(defconst isabelle-tfree-name-face isabelle-tfree-name-face
288,9125
(defconst isabelle-tvar-name-face isabelle-tvar-name-face
289,9187
(defconst isabelle-free-name-face isabelle-free-name-face
290,9247
(defconst isabelle-bound-name-face isabelle-bound-name-face
291,9307
(defconst isabelle-var-name-face isabelle-var-name-face
292,9369
(defconst isabelle-sml-symbol-face isabelle-sml-symbol-face
293,9427
(defconst isa-sml-function-var-names-regexp isa-sml-function-var-names-regexp
296,9555
(defconst isa-sml-type-names-regexp isa-sml-type-names-regexp
301,9815
(defvar isa-font-lock-keywords-1isa-font-lock-keywords-1
305,9983
(defvar isa-output-font-lock-keywords-1isa-output-font-lock-keywords-1
315,10540
(defvar isa-goals-font-lock-keywords isa-goals-font-lock-keywords
327,11111
(defconst isa-indent-any-regexpisa-indent-any-regexp
341,11386
(defconst isa-indent-inner-regexpisa-indent-inner-regexp
343,11489
(defconst isa-indent-enclose-regexpisa-indent-enclose-regexp
345,11559
(defconst isa-indent-open-regexpisa-indent-open-regexp
347,11638
(defconst isa-indent-close-regexpisa-indent-close-regexp
349,11740

isa/thy-mode.el,2895
(defcustom thy-heading-indent thy-heading-indent
27,816
(defcustom thy-indent-level thy-indent-level
32,920
(defcustom thy-indent-strings thy-indent-strings
37,1047
(defcustom thy-use-sml-mode thy-use-sml-mode
44,1272
(defcustom thy-sectionsthy-sections
55,1680
(defcustom thy-id-headerthy-id-header
108,3357
(defcustom thy-templatethy-template
120,3657
(defvar thy-mode-map thy-mode-map
145,4085
(defvar thy-mode-syntax-table thy-mode-syntax-table
147,4112
(defun thy-add-menus thy-add-menus
182,5672
(defun thy-mode thy-mode
220,7068
(defun thy-mode-quiet thy-mode-quiet
275,8827
(defun thy-proofgeneral-send-string thy-proofgeneral-send-string
355,11587
(defun isa-sml-hook isa-sml-hook
434,14194
(defun isa-sml-mode isa-sml-mode
448,14789
(defcustom isa-ml-file-extension isa-ml-file-extension
453,14921
(defun thy-find-other-file thy-find-other-file
458,15043
(defvar thy-minor-sml-mode-map thy-minor-sml-mode-map
481,15925
(defun thy-install-sml-mode thy-install-sml-mode
483,15962
(defun thy-minor-sml-mode thy-minor-sml-mode
492,16348
(defun thy-do-sml-indent thy-do-sml-indent
510,16998
(defun thy-insert-name thy-insert-name
520,17395
(defun thy-insert-class thy-insert-class
526,17593
(defun thy-insert-default-sort thy-insert-default-sort
536,17865
(defun thy-insert-type thy-insert-type
544,18037
(defun thy-insert-arity thy-insert-arity
567,18607
(defun thy-insert-const thy-insert-const
580,18982
(defun thy-insert-rule thy-insert-rule
592,19371
(defun thy-insert-template thy-insert-template
601,19553
(defun isa-read-idlist isa-read-idlist
633,20432
(defun isa-read-id isa-read-id
642,20719
(defun isa-read-string isa-read-string
650,20948
(defun isa-read-num isa-read-num
658,21185
(defun thy-read-thy-name thy-read-thy-name
669,21477
(defun thy-read-logic-image thy-read-logic-image
678,21779
(defun thy-insert-header thy-insert-header
688,22043
(defun thy-insert-id-header thy-insert-id-header
706,22608
(defun thy-check-mode thy-check-mode
718,22967
(defconst thy-headings-regexpthy-headings-regexp
723,23072
(defvar thy-mode-font-lock-keywordsthy-mode-font-lock-keywords
733,23331
(defun thy-goto-next-section thy-goto-next-section
755,24091
(defun thy-goto-prev-section thy-goto-prev-section
783,25068
(defun thy-goto-top-of-section thy-goto-top-of-section
790,25381
(defun thy-current-section thy-current-section
797,25578
(defun thy-kill-line thy-kill-line
815,26041
(defun thy-indent-line thy-indent-line
877,28125
(defun thy-calculate-indentation thy-calculate-indentation
904,29159
(defun thy-long-comment-string-indentation thy-long-comment-string-indentation
924,29818
(defun thy-string-indentation thy-string-indentation
959,30802
(defun thy-indentation-for thy-indentation-for
978,31452
(defun thy-string-start thy-string-start
984,31611
(defun thy-comment-or-string-start thy-comment-or-string-start
998,32148

isa/x-symbol-isabelle.el,3169
(defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts
20,624
(defvar x-symbol-isabelle-name x-symbol-isabelle-name
28,1028
(defvar x-symbol-isabelle-modeline-name x-symbol-isabelle-modeline-name
29,1078
(defcustom x-symbol-isabelle-header-groups-alist x-symbol-isabelle-header-groups-alist
31,1126
(defcustom x-symbol-isabelle-electric-ignore x-symbol-isabelle-electric-ignore
38,1354
(defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts
46,1610
(defvar x-symbol-isabelle-extra-menu-items x-symbol-isabelle-extra-menu-items
49,1719
(defvar x-symbol-isabelle-token-grammarx-symbol-isabelle-token-grammar
53,1817
(defun x-symbol-isabelle-token-list x-symbol-isabelle-token-list
60,2023
(defvar x-symbol-isabelle-user-table x-symbol-isabelle-user-table
63,2112
(defvar x-symbol-isabelle-generated-data x-symbol-isabelle-generated-data
66,2233
(defvar x-symbol-isabelle-master-directory x-symbol-isabelle-master-directory
74,2476
(defvar x-symbol-isabelle-image-searchpath x-symbol-isabelle-image-searchpath
75,2529
(defvar x-symbol-isabelle-image-cached-dirs x-symbol-isabelle-image-cached-dirs
76,2581
(defvar x-symbol-isabelle-image-file-truename-alist x-symbol-isabelle-image-file-truename-alist
77,2651
(defvar x-symbol-isabelle-image-keywords x-symbol-isabelle-image-keywords
78,2708
(defcustom x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher
88,3052
(defcustom x-symbol-isabelle-font-lock-regexp x-symbol-isabelle-font-lock-regexp
94,3299
(defcustom x-symbol-isabelle-font-lock-limit-regexp x-symbol-isabelle-font-lock-limit-regexp
99,3483
(defcustom x-symbol-isabelle-font-lock-contents-regexp x-symbol-isabelle-font-lock-contents-regexp
105,3701
(defcustom x-symbol-isabelle-single-char-regexp x-symbol-isabelle-single-char-regexp
115,4078
(defun x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher
121,4288
(defun isabelle-match-subscript isabelle-match-subscript
155,5963
(defvar x-symbol-isabelle-font-lock-keywordsx-symbol-isabelle-font-lock-keywords
164,6358
(defvar x-symbol-isabelle-font-lock-allowed-faces x-symbol-isabelle-font-lock-allowed-faces
171,6626
(defcustom x-symbol-isabelle-class-alistx-symbol-isabelle-class-alist
178,6858
(defcustom x-symbol-isabelle-class-face-alist x-symbol-isabelle-class-face-alist
189,7283
(defvar x-symbol-isabelle-case-insensitive x-symbol-isabelle-case-insensitive
204,7811
(defvar x-symbol-isabelle-token-shape x-symbol-isabelle-token-shape
205,7859
(defvar x-symbol-isabelle-input-token-ignore x-symbol-isabelle-input-token-ignore
206,7902
(defvar x-symbol-isabelle-token-list x-symbol-isabelle-token-list
207,7952
(defvar x-symbol-isabelle-symbol-table x-symbol-isabelle-symbol-table
209,8001
(defvar x-symbol-isabelle-xsymbol-table x-symbol-isabelle-xsymbol-table
309,10737
(defun x-symbol-isabelle-prepare-table x-symbol-isabelle-prepare-table
454,15139
(defvar x-symbol-isabelle-tablex-symbol-isabelle-table
466,15550
(defcustom x-symbol-isabelle-auto-stylex-symbol-isabelle-auto-style
480,15903
(defcustom x-symbol-isabelle-auto-coding-alist x-symbol-isabelle-auto-coding-alist
494,16413

isa/x-symbol-isa.el,0

isar/isar-autotest.el,0

isar/isar.el,1927
(defcustom isar-keywords-name isar-keywords-name
28,631
(defpgdefault completion-table completion-table
45,1155
(defcustom isar-web-pageisar-web-page
47,1208
(defun isar-detect-header isar-detect-header
65,1572
(defun isar-strip-terminators isar-strip-terminators
100,2835
(defun isar-markup-ml isar-markup-ml
113,3206
(defun isar-mode-config-set-variables isar-mode-config-set-variables
118,3341
(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables
182,6172
(defun isar-remove-file isar-remove-file
296,10939
(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list
306,11302
(defun isar-activate-scripting isar-activate-scripting
317,11768
(define-derived-mode isar-shell-mode isar-shell-mode
326,11938
(define-derived-mode isar-response-mode isar-response-mode
331,12061
(define-derived-mode isar-goals-mode isar-goals-mode
336,12243
(define-derived-mode isar-mode isar-mode
341,12418
(define-key (proof-ass proof-ass
363,12999
(defpgdefault menu-entriesmenu-entries
398,14550
(defun isar-count-undos isar-count-undos
428,15872
(defun isar-find-and-forget isar-find-and-forget
454,16973
(defun isar-goal-command-p isar-goal-command-p
501,18818
(defun isar-global-save-command-p isar-global-save-command-p
505,18950
(defvar isar-current-goal isar-current-goal
526,19787
(defun isar-state-preserving-p isar-state-preserving-p
529,19853
(defvar isar-shell-current-line-width isar-shell-current-line-width
552,20887
(defun isar-shell-adjust-line-width isar-shell-adjust-line-width
558,21105
(defun isar-pre-shell-start isar-pre-shell-start
578,21988
(defun isar-preprocessing isar-preprocessing
590,22324
(defun isar-mode-config isar-mode-config
613,23535
(defun isar-shell-mode-config isar-shell-mode-config
625,24105
(defun isar-response-mode-config isar-response-mode-config
636,24475
(defun isar-goals-mode-config isar-goals-mode-config
645,24732

isar/isar-keywords.el,1650
(defconst isar-keywords-majorisar-keywords-major
14,378
(defconst isar-keywords-minorisar-keywords-minor
169,2840
(defconst isar-keywords-controlisar-keywords-control
207,3351
(defconst isar-keywords-diagisar-keywords-diag
225,3768
(defconst isar-keywords-theory-beginisar-keywords-theory-begin
268,4490
(defconst isar-keywords-theory-switchisar-keywords-theory-switch
271,4543
(defconst isar-keywords-theory-endisar-keywords-theory-end
274,4598
(defconst isar-keywords-theory-headingisar-keywords-theory-heading
277,4646
(defconst isar-keywords-theory-declisar-keywords-theory-decl
283,4753
(defconst isar-keywords-theory-scriptisar-keywords-theory-script
326,5463
(defconst isar-keywords-theory-goalisar-keywords-theory-goal
330,5540
(defconst isar-keywords-qedisar-keywords-qed
337,5650
(defconst isar-keywords-qed-blockisar-keywords-qed-block
344,5736
(defconst isar-keywords-qed-globalisar-keywords-qed-global
347,5783
(defconst isar-keywords-proof-headingisar-keywords-proof-heading
350,5832
(defconst isar-keywords-proof-goalisar-keywords-proof-goal
355,5915
(defconst isar-keywords-proof-blockisar-keywords-proof-block
361,5998
(defconst isar-keywords-proof-openisar-keywords-proof-open
365,6060
(defconst isar-keywords-proof-closeisar-keywords-proof-close
368,6106
(defconst isar-keywords-proof-chainisar-keywords-proof-chain
371,6153
(defconst isar-keywords-proof-declisar-keywords-proof-decl
378,6256
(defconst isar-keywords-proof-asmisar-keywords-proof-asm
386,6365
(defconst isar-keywords-proof-asm-goalisar-keywords-proof-asm-goal
393,6460
(defconst isar-keywords-proof-scriptisar-keywords-proof-script
396,6515

isar/isar-mmm.el,129
(defconst isar-start-latex-regexp isar-start-latex-regexp
23,697
(defconst isar-start-sml-regexp isar-start-sml-regexp
35,1130

isar/isar-syntax.el,4921
(defconst isar-script-syntax-table-entries isar-script-syntax-table-entries
18,414
(defconst isar-script-syntax-table-alistisar-script-syntax-table-alist
58,1362
(defun isar-init-syntax-table isar-init-syntax-table
67,1645
(defun isar-init-output-syntax-table isar-init-output-syntax-table
75,1893
(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose
90,2308
(defconst isar-keywords-theoryisar-keywords-theory
95,2460
(defconst isar-keywords-saveisar-keywords-save
100,2605
(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose
105,2734
(defconst isar-keywords-proofisar-keywords-proof
111,2916
(defconst isar-keywords-proof-contextisar-keywords-proof-context
118,3114
(defconst isar-keywords-local-goalisar-keywords-local-goal
122,3228
(defconst isar-keywords-improperisar-keywords-improper
126,3340
(defconst isar-keywords-outlineisar-keywords-outline
131,3479
(defconst isar-keywords-fumeisar-keywords-fume
134,3544
(defconst isar-keywords-indent-openisar-keywords-indent-open
141,3762
(defconst isar-keywords-indent-closeisar-keywords-indent-close
147,3946
(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose
151,4051
(defun isar-regexp-simple-alt isar-regexp-simple-alt
159,4230
(defun isar-ids-to-regexp isar-ids-to-regexp
179,4991
(defconst isar-ext-first isar-ext-first
213,6259
(defconst isar-ext-rest isar-ext-rest
214,6326
(defconst isar-long-id-stuff isar-long-id-stuff
216,6398
(defconst isar-id isar-id
217,6472
(defconst isar-idx isar-idx
218,6542
(defconst isar-string isar-string
220,6601
(defconst isar-any-command-regexpisar-any-command-regexp
222,6661
(defconst isar-name-regexpisar-name-regexp
226,6795
(defconst isar-tac-regexpisar-tac-regexp
232,7090
(defconst isar-save-command-regexpisar-save-command-regexp
236,7198
(defconst isar-global-save-command-regexpisar-global-save-command-regexp
239,7299
(defconst isar-goal-command-regexpisar-goal-command-regexp
242,7413
(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp
245,7521
(defconst isar-comment-start isar-comment-start
248,7634
(defconst isar-comment-end isar-comment-end
249,7669
(defconst isar-comment-start-regexp isar-comment-start-regexp
250,7702
(defconst isar-comment-end-regexp isar-comment-end-regexp
251,7773
(defconst isar-string-start-regexp isar-string-start-regexp
253,7841
(defconst isar-string-end-regexp isar-string-end-regexp
254,7889
(defconst isar-antiq-regexpisar-antiq-regexp
263,8139
(defface isabelle-class-name-faceisabelle-class-name-face
270,8319
(defface isabelle-tfree-name-faceisabelle-tfree-name-face
280,8594
(defface isabelle-tvar-name-faceisabelle-tvar-name-face
290,8875
(defface isabelle-free-name-faceisabelle-free-name-face
300,9155
(defface isabelle-bound-name-faceisabelle-bound-name-face
310,9431
(defface isabelle-var-name-faceisabelle-var-name-face
320,9710
(defconst isabelle-class-name-face isabelle-class-name-face
330,9989
(defconst isabelle-tfree-name-face isabelle-tfree-name-face
331,10051
(defconst isabelle-tvar-name-face isabelle-tvar-name-face
332,10113
(defconst isabelle-free-name-face isabelle-free-name-face
333,10174
(defconst isabelle-bound-name-face isabelle-bound-name-face
334,10235
(defconst isabelle-var-name-face isabelle-var-name-face
335,10297
(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1
337,10358
(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1
351,11287
(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords
365,12077
(defconst isar-undo isar-undo
396,12711
(defconst isar-kill isar-kill
397,12773
(defun isar-remove isar-remove
399,12803
(defun isar-undos isar-undos
402,12878
(defun isar-cannot-undo isar-cannot-undo
406,12984
(defconst isar-undo-fail-regexpisar-undo-fail-regexp
410,13055
(defconst isar-undo-skip-regexpisar-undo-skip-regexp
414,13193
(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp
417,13314
(defconst isar-undo-remove-regexpisar-undo-remove-regexp
420,13379
(defconst isar-undo-kill-regexpisar-undo-kill-regexp
425,13519
(defconst isar-any-entity-regexpisar-any-entity-regexp
431,13661
(defconst isar-named-entity-regexpisar-named-entity-regexp
436,13848
(defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp
441,14025
(defconst isar-next-entity-regexpsisar-next-entity-regexps
444,14127
(defconst isar-generic-expressionisar-generic-expression
452,14434
(defconst isar-indent-any-regexpisar-indent-any-regexp
463,14668
(defconst isar-indent-inner-regexpisar-indent-inner-regexp
465,14761
(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp
467,14827
(defconst isar-indent-open-regexpisar-indent-open-regexp
469,14943
(defconst isar-indent-close-regexpisar-indent-close-regexp
471,15053
(defconst isar-outline-regexpisar-outline-regexp
477,15190
(defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp
481,15343

isar/x-symbol-isar.el,0

lclam/lclam.el,805
(defcustom lclam-prog-name lclam-prog-name
15,385
(defcustom lclam-web-pagelclam-web-page
21,533
(defun lclam-config lclam-config
32,763
(defun lclam-shell-config lclam-shell-config
52,1477
(define-derived-mode lclam-proofscript-mode lclam-proofscript-mode
72,2136
(define-derived-mode lclam-shell-mode lclam-shell-mode
77,2259
(define-derived-mode lclam-response-mode lclam-response-mode
82,2393
(define-derived-mode lclam-goals-mode lclam-goals-mode
86,2516
(defun lclam-mode lclam-mode
94,2744
(defun lclam-pre-shell-start lclam-pre-shell-start
107,3027
(define-derived-mode thy-mode thy-mode
141,3970
(defvar thy-mode-map thy-mode-map
144,4068
(defun thy-add-menus thy-add-menus
146,4095
(defun process-thy-file process-thy-file
186,6009
(defun update-thy-only update-thy-only
192,6210

lego/lego.el,2717
(defcustom lego-tags lego-tags
19,493
(defcustom lego-test-all-name lego-test-all-name
24,629
(defpgdefault help-menu-entrieshelp-menu-entries
30,787
(defpgdefault menu-entriesmenu-entries
34,947
(defvar lego-shell-process-outputlego-shell-process-output
45,1249
(defconst lego-process-configlego-process-config
53,1572
(defconst lego-pretty-set-width lego-pretty-set-width
64,2003
(defconst lego-interrupt-regexp lego-interrupt-regexp
68,2146
(defcustom lego-www-home-page lego-www-home-page
73,2263
(defcustom lego-www-latest-releaselego-www-latest-release
78,2387
(defcustom lego-www-refcardlego-www-refcard
84,2565
(defcustom lego-library-www-pagelego-library-www-page
90,2714
(defvar lego-prog-name lego-prog-name
99,2930
(defvar lego-shell-prompt-pattern lego-shell-prompt-pattern
102,2999
(defvar lego-shell-cd lego-shell-cd
105,3120
(defvar lego-shell-abort-goal-regexp lego-shell-abort-goal-regexp
108,3220
(defvar lego-shell-proof-completed-regexp lego-shell-proof-completed-regexp
113,3412
(defvar lego-save-command-regexplego-save-command-regexp
116,3552
(defvar lego-goal-command-regexplego-goal-command-regexp
118,3642
(defvar lego-kill-goal-command lego-kill-goal-command
121,3733
(defvar lego-forget-id-command lego-forget-id-command
122,3776
(defvar lego-undoable-commands-regexplego-undoable-commands-regexp
124,3822
(defvar lego-goal-regexp lego-goal-regexp
133,4196
(defvar lego-outline-regexplego-outline-regexp
135,4241
(defvar lego-outline-heading-end-regexp lego-outline-heading-end-regexp
141,4417
(defvar lego-shell-outline-regexp lego-shell-outline-regexp
143,4470
(defvar lego-shell-outline-heading-end-regexp lego-shell-outline-heading-end-regexp
144,4522
(define-derived-mode lego-shell-mode lego-shell-mode
150,4801
(define-derived-mode lego-mode lego-mode
156,4974
(define-derived-mode lego-goals-mode lego-goals-mode
167,5271
(defun lego-count-undos lego-count-undos
178,5697
(defun lego-goal-command-p lego-goal-command-p
198,6516
(defun lego-find-and-forget lego-find-and-forget
202,6648
(defun lego-goal-hyp lego-goal-hyp
244,8484
(defun lego-state-preserving-p lego-state-preserving-p
253,8682
(defvar lego-shell-current-line-width lego-shell-current-line-width
269,9385
(defun lego-shell-adjust-line-width lego-shell-adjust-line-width
277,9692
(defun lego-pre-shell-start lego-pre-shell-start
296,10429
(defun lego-mode-config lego-mode-config
303,10626
(defun lego-equal-module-filename lego-equal-module-filename
372,12721
(defun lego-shell-compute-new-files-list lego-shell-compute-new-files-list
378,12996
(defun lego-shell-mode-config lego-shell-mode-config
392,13522
(defun lego-goals-mode-config lego-goals-mode-config
438,15365

lego/lego-syntax.el,919
(defconst lego-keywords-goal lego-keywords-goal
15,358
(defconst lego-keywords-save lego-keywords-save
17,401
(defconst lego-commandslego-commands
19,472
(defconst lego-keywordslego-keywords
31,1032
(defconst lego-tacticals lego-tacticals
36,1209
(defconst lego-error-regexp lego-error-regexp
39,1317
(defvar lego-id lego-id
42,1476
(defvar lego-ids lego-ids
44,1503
(defconst lego-arg-list-regexp lego-arg-list-regexp
48,1699
(defun lego-decl-defn-regexp lego-decl-defn-regexp
51,1815
(defconst lego-definiendum-alternative-regexplego-definiendum-alternative-regexp
59,2187
(defvar lego-font-lock-termslego-font-lock-terms
63,2371
(defconst lego-goal-with-hole-regexplego-goal-with-hole-regexp
89,3227
(defconst lego-save-with-hole-regexplego-save-with-hole-regexp
94,3450
(defvar lego-font-lock-keywords-1lego-font-lock-keywords-1
99,3667
(defun lego-init-syntax-table lego-init-syntax-table
110,4134

lego/x-symbol-lego.el,0

phox/phox.el,898
(defcustom phox-prog-name phox-prog-name
31,931
(defcustom phox-web-pagephox-web-page
44,1329
(defcustom phox-doc-dir phox-doc-dir
50,1479
(defcustom phox-lib-dir phox-lib-dir
56,1627
(defcustom phox-tags-program phox-tags-program
62,1771
(defcustom phox-tags-doc phox-tags-doc
68,1951
(defcustom phox-etags phox-etags
74,2089
(defpgdefault menu-entriesmenu-entries
95,2541
(defun phox-config phox-config
109,2734
(defun phox-shell-config phox-shell-config
151,4658
(define-derived-mode phox-mode phox-mode
176,5584
(define-derived-mode phox-shell-mode phox-shell-mode
190,6002
(define-derived-mode phox-response-mode phox-response-mode
195,6130
(define-derived-mode phox-goals-mode phox-goals-mode
202,6377
(defun phox-pre-shell-start phox-pre-shell-start
224,7278
(defpgdefault completion-tablecompletion-table
238,7792
(defpgdefault x-symbol-language x-symbol-language
246,7897

phox/phox-extraction.el,603
(defvar phox-prog-orig phox-prog-orig
11,480
(defun phox-prog-flags-modify(phox-prog-flags-modify
13,548
(defun phox-prog-flags-extract(phox-prog-flags-extract
42,1352
(defun phox-prog-flags-erase(phox-prog-flags-erase
53,1643
(defun phox-toggle-extraction(phox-toggle-extraction
61,1839
(defun phox-compile-theorem(phox-compile-theorem
73,2241
(defun phox-compile-theorem-on-cursor(phox-compile-theorem-on-cursor
79,2467
(defun phox-output phox-output
95,2946
(defun phox-output-theorem phox-output-theorem
105,3160
(defun phox-output-theorem-on-cursor(phox-output-theorem-on-cursor
112,3460

phox/phox-font.el,64
(defconst phox-font-lock-keywordsphox-font-lock-keywords
6,282

phox/phox-fun.el,1049
(defun phox-init-syntax-table phox-init-syntax-table
67,2392
(defvar phox-top-keywordsphox-top-keywords
83,2865
(defvar phox-proof-keywordsphox-proof-keywords
131,3320
(defun phox-find-and-forget phox-find-and-forget
172,3670
(defun phox-assert-next-command-interactive phox-assert-next-command-interactive
251,6095
(defun phox-depend-theorem(phox-depend-theorem
270,6926
(defun phox-eshow-extlist(phox-eshow-extlist
279,7216
(defun phox-flag-name(phox-flag-name
293,7815
(defun phox-path(phox-path
304,8118
(defun phox-print-expression(phox-print-expression
315,8355
(defun phox-print-sort-expression(phox-print-sort-expression
328,8813
(defun phox-priority-symbols-list(phox-priority-symbols-list
339,9126
(defun phox-search-string(phox-search-string
351,9499
(defun phox-constraints(phox-constraints
366,10027
(defun phox-goals(phox-goals
377,10284
(defvar phox-state-menuphox-state-menu
389,10494
(defun phox-delete-symbol(phox-delete-symbol
414,11484
(defun phox-delete-symbol-on-cursor(phox-delete-symbol-on-cursor
420,11693

phox/phox-lang.el,0

phox/phox-outline.el,108
(defun phox-outline-level(phox-outline-level
32,1113
(defun phox-setup-outline phox-setup-outline
46,1587

phox/phox-pbrpm.el,551
(defun phox-pbrpm-left-paren-p phox-pbrpm-left-paren-p
25,1169
(defun phox-pbrpm-right-paren-p phox-pbrpm-right-paren-p
32,1372
(defun phox-pbrpm-menu-from-string phox-pbrpm-menu-from-string
40,1576
(defun phox-pbrpm-rename-in-cmd phox-pbrpm-rename-in-cmd
49,1910
(defun phox-pbrpm-generate-menu phox-pbrpm-generate-menu
82,3166
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
250,8785
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
251,8849
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
252,8911

phox/phox-tags.el,483
(defun phox-tags-add-table(phox-tags-add-table
21,766
(defun phox-tags-reset-table(phox-tags-reset-table
38,1359
(defun phox-tags-add-doc-table(phox-tags-add-doc-table
48,1629
(defun phox-tags-add-lib-table(phox-tags-add-lib-table
54,1778
(defun phox-tags-add-local-table(phox-tags-add-local-table
60,1914
(defun phox-tags-create-local-table(phox-tags-create-local-table
66,2097
(defun phox-complete-tag(phox-complete-tag
77,2349
(defvar phox-tags-menuphox-tags-menu
96,2904

phox/x-symbol-phox.el,2614
(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts
14,449
(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist
29,1056
(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore
36,1276
(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts
43,1492
(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items
46,1593
(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar
49,1682
(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar
63,2473
(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list
69,2728
(defvar x-symbol-phox-user-table x-symbol-phox-user-table
81,3046
(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data
84,3155
(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory
92,3394
(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath
93,3443
(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs
94,3491
(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist
95,3557
(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords
96,3610
(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist
103,3831
(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist
114,4213
(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords
124,4526
(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces
126,4573
(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive
132,4798
(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape
133,4842
(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore
134,4881
(defvar x-symbol-phox-token-list x-symbol-phox-token-list
141,5120
(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table
143,5165
(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table
164,5624
(defvar x-symbol-phox-tablex-symbol-phox-table
172,5800
(defcustom x-symbol-phox-auto-stylex-symbol-phox-auto-style
183,6118
(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist
209,7068
(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist
211,7158
(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree
214,7249
(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist
216,7342
(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist
218,7439
(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec
222,7596
(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec
224,7696

plastic/plastic.el,4425
(defcustom plastic-tags plastic-tags
28,805
(defcustom plastic-test-all-name plastic-test-all-name
33,937
(defvar plastic-lit-string plastic-lit-string
39,1110
(defcustom plastic-help-menu-listplastic-help-menu-list
43,1223
(defvar plastic-shell-process-outputplastic-shell-process-output
57,1717
(defconst plastic-process-config plastic-process-config
65,2043
(defconst plastic-pretty-set-width plastic-pretty-set-width
72,2293
(defconst plastic-interrupt-regexp plastic-interrupt-regexp
76,2442
(defcustom plastic-www-home-page plastic-www-home-page
82,2563
(defcustom plastic-www-latest-releaseplastic-www-latest-release
87,2700
(defcustom plastic-www-refcardplastic-www-refcard
93,2873
(defcustom plastic-library-www-pageplastic-library-www-page
99,3004
(defcustom plastic-base plastic-base
109,3219
(defvar plastic-prog-name plastic-prog-name
117,3391
(defun plastic-set-default-env-vars plastic-set-default-env-vars
121,3499
(defvar plastic-shell-prompt-pattern plastic-shell-prompt-pattern
129,3737
(defvar plastic-shell-cd plastic-shell-cd
132,3862
(defvar plastic-shell-abort-goal-regexp plastic-shell-abort-goal-regexp
136,4004
(defvar plastic-shell-proof-completed-regexp plastic-shell-proof-completed-regexp
140,4172
(defvar plastic-save-command-regexpplastic-save-command-regexp
143,4315
(defvar plastic-goal-command-regexpplastic-goal-command-regexp
145,4411
(defvar plastic-kill-goal-command plastic-kill-goal-command
148,4508
(defvar plastic-forget-id-command plastic-forget-id-command
150,4609
(defvar plastic-undoable-commands-regexpplastic-undoable-commands-regexp
153,4690
(defvar plastic-goal-regexp plastic-goal-regexp
165,5137
(defvar plastic-outline-regexpplastic-outline-regexp
167,5185
(defvar plastic-outline-heading-end-regexp plastic-outline-heading-end-regexp
173,5364
(defvar plastic-shell-outline-regexp plastic-shell-outline-regexp
175,5420
(defvar plastic-shell-outline-heading-end-regexp plastic-shell-outline-heading-end-regexp
176,5478
(defvar plastic-error-occurred plastic-error-occurred
178,5549
(define-derived-mode plastic-shell-mode plastic-shell-mode
187,5881
(define-derived-mode plastic-mode plastic-mode
193,6063
(define-derived-mode plastic-goals-mode plastic-goals-mode
207,6516
(defun plastic-count-undos plastic-count-undos
216,6861
(defun plastic-goal-command-p plastic-goal-command-p
236,7737
(defun plastic-find-and-forget plastic-find-and-forget
240,7890
(defun plastic-goal-hyp plastic-goal-hyp
275,9238
(defun plastic-state-preserving-p plastic-state-preserving-p
286,9488
(defvar plastic-shell-current-line-width plastic-shell-current-line-width
308,10416
(defun plastic-shell-adjust-line-width plastic-shell-adjust-line-width
316,10732
(defun plastic-pre-shell-start plastic-pre-shell-start
337,11611
(defun plastic-mode-config plastic-mode-config
352,12177
(defun plastic-show-shell-buffer plastic-show-shell-buffer
449,15819
(defun plastic-equal-module-filename plastic-equal-module-filename
455,15922
(defun plastic-shell-compute-new-files-list plastic-shell-compute-new-files-list
461,16200
(defun plastic-shell-mode-config plastic-shell-mode-config
477,16737
(defun plastic-goals-mode-config plastic-goals-mode-config
528,18927
(defun plastic-small-bar plastic-small-bar
540,19209
(defun plastic-large-bar plastic-large-bar
542,19298
(defun plastic-preprocessing plastic-preprocessing
544,19436
(defun plastic-all-ctxt plastic-all-ctxt
595,21264
(defun plastic-send-one-undo plastic-send-one-undo
602,21442
(defun plastic-minibuf-cmd plastic-minibuf-cmd
612,21770
(defun plastic-minibuf plastic-minibuf
624,22249
(defun plastic-synchro plastic-synchro
631,22455
(defun plastic-send-minibuf plastic-send-minibuf
636,22596
(defun plastic-had-error plastic-had-error
644,22925
(defun plastic-reset-error plastic-reset-error
648,23100
(defun plastic-call-if-no-error plastic-call-if-no-error
651,23239
(defun plastic-show-shell plastic-show-shell
656,23443
(define-key plastic-keymap plastic-keymap
665,23705
(define-key plastic-keymap plastic-keymap
666,23766
(define-key plastic-keymap plastic-keymap
667,23827
(define-key plastic-keymap plastic-keymap
668,23887
(define-key plastic-keymap plastic-keymap
669,23946
(define-key plastic-keymap plastic-keymap
670,24005
(defalias 'proof-toolbar-command proof-toolbar-command
680,24255
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
681,24306

plastic/plastic-syntax.el,1015
(defconst plastic-keywords-goal plastic-keywords-goal
18,537
(defconst plastic-keywords-save plastic-keywords-save
20,583
(defconst plastic-commandsplastic-commands
22,657
(defconst plastic-keywordsplastic-keywords
35,1267
(defconst plastic-tacticals plastic-tacticals
40,1450
(defconst plastic-error-regexp plastic-error-regexp
43,1561
(defvar plastic-id plastic-id
46,1695
(defvar plastic-ids plastic-ids
48,1725
(defconst plastic-arg-list-regexp plastic-arg-list-regexp
52,1933
(defun plastic-decl-defn-regexp plastic-decl-defn-regexp
55,2052
(defconst plastic-definiendum-alternative-regexpplastic-definiendum-alternative-regexp
63,2433
(defvar plastic-font-lock-termsplastic-font-lock-terms
67,2626
(defconst plastic-goal-with-hole-regexpplastic-goal-with-hole-regexp
89,3339
(defconst plastic-save-with-hole-regexpplastic-save-with-hole-regexp
94,3566
(defvar plastic-font-lock-keywords-1plastic-font-lock-keywords-1
99,3792
(defun plastic-init-syntax-table plastic-init-syntax-table
108,4184

twelf/twelf.el,677
(defcustom twelf-root-dirtwelf-root-dir
25,591
(defcustom twelf-info-dirtwelf-info-dir
31,749
(defun twelf-add-read-declaration twelf-add-read-declaration
100,3259
(defun twelf-set-syntax twelf-set-syntax
113,3594
(defun twelf-set-word twelf-set-word
115,3691
(defun twelf-set-symbol twelf-set-symbol
116,3753
(defun twelf-map-string twelf-map-string
118,3817
(defun twelf-mode-extra-config twelf-mode-extra-config
165,5879
(defconst twelf-syntax-menutwelf-syntax-menu
171,6085
(defpacustom chatter chatter
185,6452
(defpacustom double-check double-check
190,6545
(defpacustom print-implicit print-implicit
194,6682
(defpgdefault menu-entriesmenu-entries
206,6826

twelf/twelf-font.el,1425
(defun twelf-font-create-face twelf-font-create-face
31,836
(defvar twelf-font-dark-background twelf-font-dark-background
38,1094
(defvar twelf-font-patternstwelf-font-patterns
64,2452
(defun twelf-font-fontify-decl twelf-font-fontify-decl
105,4302
(defun twelf-font-fontify-buffer twelf-font-fontify-buffer
115,4599
(defun twelf-font-unfontify twelf-font-unfontify
122,4858
(defvar font-lock-message-threshold font-lock-message-threshold
127,5032
(defun twelf-font-fontify-region twelf-font-fontify-region
129,5110
(defun twelf-font-highlight twelf-font-highlight
195,7610
(defun twelf-font-find-delimited-comment twelf-font-find-delimited-comment
204,8067
(defun twelf-font-find-decl twelf-font-find-decl
223,8747
(defun twelf-font-find-binder twelf-font-find-binder
239,9237
(defun twelf-font-find-parm twelf-font-find-parm
301,11094
(defun twelf-font-find-evar twelf-font-find-evar
308,11417
(defun twelf-current-decl twelf-current-decl
330,12159
(defun twelf-next-decl twelf-next-decl
357,13315
(defconst *whitespace* *whitespace*
382,14337
(defconst *twelf-comment-start* *twelf-comment-start*
385,14435
(defconst *twelf-id-chars* *twelf-id-chars*
388,14564
(defun skip-twelf-comments-and-whitespace skip-twelf-comments-and-whitespace
391,14682
(defun twelf-end-of-par twelf-end-of-par
403,15156
(defun skip-ahead skip-ahead
426,15930
(defun current-line-absolute current-line-absolute
438,16352

twelf/twelf-old.el,10513
(defvar twelf-indent twelf-indent
212,8771
(defvar twelf-infix-regexp twelf-infix-regexp
215,8831
(defvar twelf-server-program twelf-server-program
219,9026
(defvar twelf-info-file twelf-info-file
222,9107
(defvar twelf-server-display-commands twelf-server-display-commands
225,9180
(defvar twelf-highlight-range-function twelf-highlight-range-function
230,9428
(defvar twelf-focus-function twelf-focus-function
235,9711
(defvar twelf-server-echo-commands twelf-server-echo-commands
241,9991
(defvar twelf-save-silently twelf-save-silently
244,10112
(defvar twelf-server-timeout twelf-server-timeout
248,10284
(defvar twelf-sml-program twelf-sml-program
252,10431
(defvar twelf-sml-args twelf-sml-args
255,10503
(defvar twelf-sml-display-queries twelf-sml-display-queries
258,10569
(defvar twelf-mode-hook twelf-mode-hook
261,10677
(defvar twelf-server-mode-hook twelf-server-mode-hook
264,10771
(defvar twelf-config-mode-hook twelf-config-mode-hook
267,10879
(defvar twelf-sml-mode-hook twelf-sml-mode-hook
270,10993
(defvar twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode
273,11074
(defvar twelf-config-mode twelf-config-mode
276,11166
(defvar *twelf-server-buffer-name* *twelf-server-buffer-name*
283,11430
(defvar *twelf-server-buffer* *twelf-server-buffer*
286,11534
(defvar *twelf-server-process-name* *twelf-server-process-name*
289,11622
(defvar *twelf-config-buffer* *twelf-config-buffer*
292,11713
(defvar *twelf-config-time* *twelf-config-time*
295,11807
(defvar *twelf-config-list* *twelf-config-list*
298,11920
(defvar *twelf-server-last-process-mark* *twelf-server-last-process-mark*
301,12032
(defvar *twelf-last-region-sent* *twelf-last-region-sent*
304,12150
(defvar *twelf-last-input-buffer* *twelf-last-input-buffer*
311,12474
(defvar *twelf-error-pos* *twelf-error-pos*
315,12597
(defconst *twelf-read-functions**twelf-read-functions*
318,12673
(defconst *twelf-parm-table**twelf-parm-table*
325,12911
(defvar twelf-chatter twelf-chatter
338,13287
(defvar twelf-double-check twelf-double-check
346,13504
(defvar twelf-print-implicit twelf-print-implicit
349,13591
(defconst *twelf-track-parms**twelf-track-parms*
352,13683
(defun install-basic-twelf-keybindings install-basic-twelf-keybindings
363,14107
(defun install-twelf-keybindings install-twelf-keybindings
388,15076
(defvar twelf-mode-map twelf-mode-map
404,15841
(defvar twelf-mode-syntax-table twelf-mode-syntax-table
416,16277
(defun set-twelf-syntax set-twelf-syntax
419,16356
(defun set-word set-word
421,16453
(defun set-symbol set-symbol
422,16508
(defun map-string map-string
424,16566
(defconst *whitespace* *whitespace*
456,18043
(defconst *twelf-comment-start* *twelf-comment-start*
459,18141
(defconst *twelf-id-chars* *twelf-id-chars*
462,18270
(defun skip-twelf-comments-and-whitespace skip-twelf-comments-and-whitespace
465,18388
(defun twelf-end-of-par twelf-end-of-par
477,18862
(defun twelf-current-decl twelf-current-decl
500,19636
(defun twelf-mark-decl twelf-mark-decl
527,20792
(defun twelf-indent-decl twelf-indent-decl
536,21058
(defun twelf-indent-region twelf-indent-region
545,21344
(defun twelf-indent-lines twelf-indent-lines
556,21668
(defun twelf-comment-indent twelf-comment-indent
564,21841
(defun looked-at looked-at
575,22197
(defun twelf-indent-line twelf-indent-line
580,22369
(defun twelf-indent-line-to twelf-indent-line-to
613,24112
(defun twelf-calculate-indent twelf-calculate-indent
626,24567
(defun twelf-dsb twelf-dsb
641,25191
(defun twelf-mode-variables twelf-mode-variables
667,26603
(defun twelf-mode twelf-mode
689,27416
(defun twelf-info twelf-info
904,35798
(defconst twelf-error-regexptwelf-error-regexp
918,36338
(defconst twelf-error-fields-regexptwelf-error-fields-regexp
922,36449
(defconst twelf-error-decl-regexptwelf-error-decl-regexp
928,36662
(defun looked-at-nth looked-at-nth
932,36811
(defun looked-at-nth-int looked-at-nth-int
938,36993
(defun twelf-error-parser twelf-error-parser
943,37108
(defun twelf-error-decl twelf-error-decl
957,37711
(defun twelf-mark-relative twelf-mark-relative
963,37890
(defun twelf-mark-absolute twelf-mark-absolute
979,38560
(defun twelf-find-decl twelf-find-decl
1004,39446
(defun twelf-next-error twelf-next-error
1019,40002
(defun twelf-goto-error twelf-goto-error
1087,42812
(defun twelf-convert-standard-filename twelf-convert-standard-filename
1101,43350
(defun string-member string-member
1113,43845
(defun twelf-config-proceed-p twelf-config-proceed-p
1125,44337
(defun twelf-save-if-config twelf-save-if-config
1132,44599
(defun twelf-config-save-some-buffers twelf-config-save-some-buffers
1145,45071
(defun twelf-save-check-config twelf-save-check-config
1149,45236
(defun twelf-check-config twelf-check-config
1164,45792
(defun twelf-save-check-file twelf-save-check-file
1176,46232
(defun twelf-buffer-substring twelf-buffer-substring
1192,46955
(defun twelf-buffer-substring-dot twelf-buffer-substring-dot
1198,47217
(defun twelf-check-declaration twelf-check-declaration
1204,47483
(defun twelf-highlight-range-zmacs twelf-highlight-range-zmacs
1227,48543
(defun twelf-focus twelf-focus
1233,48793
(defun twelf-focus-noop twelf-focus-noop
1239,49059
(defun twelf-type-const twelf-type-const
1322,52681
(defvar twelf-server-mode-map twelf-server-mode-map
1439,57823
(defconst twelf-server-cd-regexp twelf-server-cd-regexp
1451,58375
(defun looked-at-string looked-at-string
1454,58515
(defun twelf-server-directory-tracker twelf-server-directory-tracker
1458,58656
(defun twelf-input-filter twelf-input-filter
1480,59830
(defun twelf-server-mode twelf-server-mode
1486,60085
(defun twelf-parse-config twelf-parse-config
1519,61302
(defun twelf-server-read-config twelf-server-read-config
1537,62194
(defun twelf-server-sync-config twelf-server-sync-config
1546,62531
(defun twelf-get-server-buffer twelf-get-server-buffer
1576,64037
(defun twelf-init-variables twelf-init-variables
1593,64711
(defun twelf-server twelf-server
1600,64924
(defun twelf-server-process twelf-server-process
1642,66838
(defun twelf-server-display twelf-server-display
1651,67244
(defun display-server-buffer display-server-buffer
1658,67518
(defun twelf-server-send-command twelf-server-send-command
1673,68250
(defun twelf-accept-process-output twelf-accept-process-output
1694,69210
(defun twelf-server-wait twelf-server-wait
1703,69649
(defun twelf-server-quit twelf-server-quit
1745,71787
(defun twelf-server-interrupt twelf-server-interrupt
1750,71908
(defun twelf-reset twelf-reset
1755,72044
(defun twelf-config-directory twelf-config-directory
1760,72188
(defun twelf-server-configure twelf-server-configure
1771,72602
(defun natp natp
1844,75894
(defun twelf-read-nat twelf-read-nat
1848,75995
(defun twelf-read-bool twelf-read-bool
1857,76262
(defun twelf-read-limit twelf-read-limit
1863,76410
(defun twelf-read-strategy twelf-read-strategy
1873,76710
(defun twelf-read-value twelf-read-value
1879,76862
(defun twelf-set twelf-set
1883,77025
(defun twelf-set-parm twelf-set-parm
1896,77502
(defun track-parm track-parm
1905,77799
(defun twelf-toggle-double-check twelf-toggle-double-check
1910,77973
(defun twelf-toggle-print-implicit twelf-toggle-print-implicit
1916,78176
(defun twelf-get twelf-get
1922,78389
(defun twelf-timers-reset twelf-timers-reset
1936,79015
(defun twelf-timers-show twelf-timers-show
1941,79135
(defun twelf-timers-check twelf-timers-check
1947,79286
(defun twelf-server-restart twelf-server-restart
1953,79451
(defun twelf-config-mode twelf-config-mode
1969,80128
(defun twelf-config-mode-check twelf-config-mode-check
1985,80727
(defun twelf-tag twelf-tag
1994,81177
(defun twelf-tag-files twelf-tag-files
2022,82441
(default: *tags-errors*)*tags-errors*
2026,82744
(defun twelf-tag-file twelf-tag-file
2047,83495
(defun twelf-next-decl twelf-next-decl
2082,84717
(defun skip-ahead skip-ahead
2107,85739
(defun current-line-absolute current-line-absolute
2119,86161
(defun new-temp-buffer new-temp-buffer
2124,86371
(defun rev-relativize rev-relativize
2135,86755
(defvar twelf-sml-mode-map twelf-sml-mode-map
2149,87215
(defconst twelf-sml-prompt-regexp twelf-sml-prompt-regexp
2159,87593
(defun expand-dir expand-dir
2161,87648
(defun twelf-sml-cd twelf-sml-cd
2168,87909
(defconst twelf-sml-cd-regexp twelf-sml-cd-regexp
2180,88398
(defun twelf-sml-directory-tracker twelf-sml-directory-tracker
2183,88532
(defun twelf-sml-mode twelf-sml-mode
2199,89377
(defun twelf-sml twelf-sml
2250,91311
(defun switch-to-twelf-sml switch-to-twelf-sml
2270,92271
(defun display-twelf-sml-buffer display-twelf-sml-buffer
2281,92620
(defun twelf-sml-send-string twelf-sml-send-string
2297,93336
(defun twelf-sml-send-region twelf-sml-send-region
2302,93540
(defun twelf-sml-send-query twelf-sml-send-query
2326,94746
(defun twelf-sml-send-newline twelf-sml-send-newline
2336,95143
(defun twelf-sml-send-semicolon twelf-sml-send-semicolon
2344,95471
(defun twelf-sml-status twelf-sml-status
2352,95805
(defvar twelf-sml-init twelf-sml-init
2374,96752
(defun twelf-sml-set-mode twelf-sml-set-mode
2377,96929
(defun twelf-sml-quit twelf-sml-quit
2403,98106
(defun twelf-sml-process-buffer twelf-sml-process-buffer
2408,98218
(defun twelf-sml-process twelf-sml-process
2412,98334
(defvar twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode
2424,98850
(defun install-twelf-to-twelf-sml-keybindings install-twelf-to-twelf-sml-keybindings
2427,98935
(defvar twelf-to-twelf-sml-mode-map twelf-to-twelf-sml-mode-map
2437,99320
(defun twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode
2448,99833
(defconst twelf-at-point-menutwelf-at-point-menu
2498,101700
(defconst twelf-server-state-menutwelf-server-state-menu
2508,102072
(defconst twelf-error-menutwelf-error-menu
2518,102389
(defconst twelf-tags-menutwelf-tags-menu
2524,102533
(defun twelf-toggle-server-display-commands twelf-toggle-server-display-commands
2534,102818
(defconst twelf-options-menutwelf-options-menu
2537,102942
(defconst twelf-timers-menutwelf-timers-menu
2572,104680
(defconst twelf-syntax-menutwelf-syntax-menu
2585,105174
(defun twelf-add-menu twelf-add-menu
2612,106040
(defun twelf-remove-menu twelf-remove-menu
2616,106142
(defun twelf-reset-menu twelf-reset-menu
2620,106240
(defun twelf-server-add-menu twelf-server-add-menu
2647,107139
(defun twelf-server-remove-menu twelf-server-remove-menu
2651,107262
(defun twelf-server-reset-menu twelf-server-reset-menu
2655,107374

twelf/x-symbol-twelf.el,0

lib/holes.el,3711
(defvar holes-doc holes-doc
35,993
(defvar holes-default-hole holes-default-hole
143,4976
(defvar holes-active-hole holes-active-hole
147,5145
(defcustom holes-empty-hole-string holes-empty-hole-string
154,5354
(defcustom holes-empty-hole-regexp holes-empty-hole-regexp
157,5465
(defcustom holes-search-limit holes-search-limit
164,5756
(defface active-hole-faceactive-hole-face
176,6132
(defface inactive-hole-faceinactive-hole-face
188,6580
(defun holes-region-beginning-or-nil holes-region-beginning-or-nil
203,7056
(defun holes-region-end-or-nil holes-region-end-or-nil
208,7166
(defun holes-copy-active-region holes-copy-active-region
213,7264
(defun holes-is-hole-p holes-is-hole-p
220,7463
(defun holes-hole-start-position holes-hole-start-position
226,7570
(defun holes-hole-end-position holes-hole-end-position
233,7759
(defun holes-hole-buffer holes-hole-buffer
240,7943
(defun holes-hole-at holes-hole-at
247,8118
(defun holes-active-hole-exist-p holes-active-hole-exist-p
254,8293
(defun holes-active-hole-start-position holes-active-hole-start-position
264,8551
(defun holes-active-hole-end-position holes-active-hole-end-position
274,8923
(defun holes-active-hole-buffer holes-active-hole-buffer
285,9292
(defun holes-goto-active-hole holes-goto-active-hole
296,9598
(defun holes-highlight-hole-as-active holes-highlight-hole-as-active
308,9866
(defun holes-highlight-hole holes-highlight-hole
318,10178
(defun holes-disable-active-hole holes-disable-active-hole
329,10470
(defun holes-set-active-hole holes-set-active-hole
347,11013
(defun holes-is-in-hole-p holes-is-in-hole-p
360,11359
(defun holes-make-hole holes-make-hole
367,11502
(defun holes-make-hole-at holes-make-hole-at
393,12248
(defun holes-clear-hole holes-clear-hole
413,12724
(defun holes-clear-hole-at holes-clear-hole-at
425,13013
(defun holes-map-holes holes-map-holes
434,13272
(defun holes-mapcar-holes holes-mapcar-holes
442,13455
(defun holes-clear-all-buffer-holes holes-clear-all-buffer-holes
448,13622
(defun holes-next holes-next
459,13922
(defun holes-next-after-active-hole holes-next-after-active-hole
466,14173
(defun holes-set-active-hole-next holes-set-active-hole-next
474,14392
(defun holes-replace-segment holes-replace-segment
496,14945
(defun holes-replace holes-replace
506,15299
(defun holes-replace-active-hole holes-replace-active-hole
537,16494
(defun holes-replace-update-active-hole holes-replace-update-active-hole
546,16795
(defun holes-delete-update-active-hole holes-delete-update-active-hole
567,17485
(defun holes-set-make-active-hole holes-set-make-active-hole
574,17699
(defun holes-mouse-replace-active-hole holes-mouse-replace-active-hole
609,18825
(defun holes-destroy-hole holes-destroy-hole
629,19364
(defun holes-hole-at-event holes-hole-at-event
646,19775
(defun holes-mouse-destroy-hole holes-mouse-destroy-hole
651,19888
(defun holes-mouse-forget-hole holes-mouse-forget-hole
661,20128
(defun holes-mouse-set-make-active-hole holes-mouse-set-make-active-hole
677,20438
(defun holes-mouse-set-active-hole holes-mouse-set-active-hole
699,20999
(defun holes-set-point-next-hole-destroy holes-set-point-next-hole-destroy
711,21263
(defvar hole-maphole-map
727,21713
(defvar holes-mode-mapholes-mode-map
743,22333
(defun holes-replace-string-by-holes-backward holes-replace-string-by-holes-backward
780,23798
(defun holes-skeleton-end-hook holes-skeleton-end-hook
798,24499
(defconst holes-jump-doc holes-jump-doc
806,24863
(defun holes-abbrev-complete holes-abbrev-complete
811,25068
(defun holes-insert-and-expand holes-insert-and-expand
829,25764
(defvar holes-mode holes-mode
839,26183
(defun holes-mode holes-mode
845,26379

lib/holes-load.el,0

lib/proof-compat.el,1194
(defvar proof-running-on-XEmacs proof-running-on-XEmacs
24,760
(defvar proof-running-on-Emacs21 proof-running-on-Emacs21
26,882
(defvar proof-running-on-win32 proof-running-on-win32
30,1129
(defun pg-custom-undeclare-variable pg-custom-undeclare-variable
41,1562
(defun subst-char-in-string subst-char-in-string
112,3702
(defun replace-regexp-in-string replace-regexp-in-string
126,4256
(defconst menuvisiblep menuvisiblep
188,6969
(defun set-window-text-height set-window-text-height
205,7588
(defmacro save-selected-frame save-selected-frame
231,8538
(defun warn warn
270,9840
(defun redraw-modeline redraw-modeline
277,10095
(defun replace-in-string replace-in-string
292,10662
(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate
341,12180
(defvar read-shell-command-mapread-shell-command-map
374,13487
(defun read-shell-command read-shell-command
392,14189
(defun remassq remassq
404,14670
(defun remassoc remassoc
416,15059
(defun frames-of-buffer frames-of-buffer
429,15504
(defmacro with-selected-window with-selected-window
468,16767
(defun pg-pop-to-buffer pg-pop-to-buffer
504,17892
(defun process-live-p process-live-p
555,19744

lib/span.el,192
(defsubst delete-spans delete-spans
24,499
(defsubst span-property-safe span-property-safe
28,653
(defsubst set-span-start set-span-start
32,792
(defsubst set-span-end set-span-end
36,924

lib/span-extent.el,1346
(defsubst make-span make-span
16,557
(defsubst detach-span detach-span
20,679
(defsubst set-span-endpoints set-span-endpoints
24,766
(defsubst set-span-property set-span-property
28,899
(defsubst span-read-only span-read-only
32,1026
(defsubst span-read-write span-read-write
36,1130
(defun span-give-warning span-give-warning
40,1237
(defun span-write-warning span-write-warning
44,1335
(defsubst span-property span-property
49,1535
(defsubst delete-span delete-span
53,1650
(defsubst mapcar-spans mapcar-spans
59,1821
(defsubst span-at span-at
63,2027
(defsubst span-at-before span-at-before
67,2144
(defsubst span-start span-start
72,2341
(defsubst span-end span-end
76,2470
(defsubst prev-span prev-span
80,2593
(defsubst next-span next-span
84,2739
(defsubst span-live-p span-live-p
88,2881
(defun span-raise span-raise
96,3153
(defalias 'span-object span-object
100,3252
(defalias 'span-string span-string
101,3291
(defsubst make-detached-span make-detached-span
104,3377
(defsubst span-buffer span-buffer
109,3439
(defsubst span-detached-p span-detached-p
114,3531
(defsubst set-span-face set-span-face
119,3643
(defsubst fold-spans fold-spans
124,3739
(defsubst set-span-properties set-span-properties
129,3937
(defsubst set-span-keymap set-span-keymap
134,4046
(defsubst span-at-event span-at-event
139,4161

lib/span-overlay.el,1566
(defalias 'span-start span-start
16,543
(defalias 'span-end span-end
17,581
(defalias 'set-span-property set-span-property
18,615
(defalias 'span-property span-property
19,658
(defalias 'make-span make-span
20,697
(defalias 'detach-span detach-span
21,733
(defalias 'set-span-endpoints set-span-endpoints
22,773
(defalias 'span-buffer span-buffer
23,818
(defun span-read-only-hook span-read-only-hook
25,859
(defun span-read-only span-read-only
29,991
(defun span-read-write span-read-write
44,1767
(defun span-give-warning span-give-warning
50,1986
(defun span-write-warning span-write-warning
54,2094
(defun span-lt span-lt
61,2420
(defun spans-at-point-prop spans-at-point-prop
66,2561
(defun spans-at-region-prop spans-at-region-prop
72,2726
(defun span-at span-at
80,2970
(defsubst delete-span delete-span
86,3184
(defsubst mapcar-spans mapcar-spans
93,3406
(defun span-at-before span-at-before
97,3610
(defun prev-span prev-span
114,4336
(defun next-span next-span
120,4487
(defsubst span-live-p span-live-p
149,5712
(defun span-raise span-raise
155,5878
(defalias 'span-object span-object
161,6121
(defun span-string span-string
163,6162
(defun set-span-properties set-span-properties
169,6344
(defun span-find-span span-find-span
181,6599
(defsubst span-at-event span-at-event
188,6906
(defun make-detached-span make-detached-span
193,7030
(defun fold-spans fold-spans
198,7126
(defsubst span-detached-p span-detached-p
213,7660
(defsubst set-span-face set-span-face
217,7775
(defun set-span-keymap set-span-keymap
221,7872

lib/texi-docstring-magic.el,958
(defun texi-docstring-magic-find-face texi-docstring-magic-find-face
85,2996
(defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep
90,3161
(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table
100,3466
(defun texi-docstring-magic-untabify texi-docstring-magic-untabify
190,7186
(defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring
200,7501
(defun texi-docstring-magic-texi texi-docstring-magic-texi
239,8788
(defun texi-docstring-magic-format-default texi-docstring-magic-format-default
252,9228
(defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for
268,9863
(defconst texi-docstring-magic-commenttexi-docstring-magic-comment
326,11823
(defun texi-docstring-magic texi-docstring-magic
332,11977
(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point
366,13057
(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic
381,13580

lib/xml.el,790
(defsubst xml-node-name xml-node-name
82,2907
(defsubst xml-node-attributes xml-node-attributes
87,3026
(defsubst xml-node-children xml-node-children
92,3144
(defun xml-get-children xml-get-children
97,3280
(defun xml-get-attribute xml-get-attribute
107,3603
(defun xml-parse-file xml-parse-file
123,4067
(defun xml-parse-region xml-parse-region
144,4651
(defun xml-parse-tag xml-parse-tag
179,5696
(defun xml-parse-attlist xml-parse-attlist
284,9165
(defun xml-skip-dtd xml-skip-dtd
321,10555
(defun xml-parse-dtd xml-parse-dtd
338,11191
(defun xml-parse-elem-type xml-parse-elem-type
408,13269
(defun xml-substitute-special xml-substitute-special
449,14424
(defun xml-debug-print xml-debug-print
470,15231
(defun xml-debug-print-internal xml-debug-print-internal
474,15323

mmm/mmm-auto.el,499
(defvar mmm-autoloaded-classesmmm-autoloaded-classes
67,2675
(defun mmm-autoload-class mmm-autoload-class
85,3320
(defvar mmm-changed-buffers-list mmm-changed-buffers-list
125,4887
(defun mmm-major-mode-change mmm-major-mode-change
128,4994
(defun mmm-check-changed-buffers mmm-check-changed-buffers
141,5515
(defun mmm-mode-on-maybe mmm-mode-on-maybe
151,5888
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
163,6306
(defun mmm-add-find-file-hook mmm-add-find-file-hook
164,6366

mmm/mmm-class.el,626
(defun mmm-get-class-spec mmm-get-class-spec
41,1254
(defun mmm-get-class-parameter mmm-get-class-parameter
58,1967
(defun mmm-set-class-parameter mmm-set-class-parameter
62,2133
(defun* mmm-apply-classmmm-apply-class
74,2497
(defun* mmm-apply-classesmmm-apply-classes
86,3010
(defun* mmm-apply-all mmm-apply-all
106,3776
(defun* mmm-ifymmm-ify
118,4203
(defun* mmm-match-regionmmm-match-region
184,6890
(defun mmm-match->point mmm-match->point
228,8982
(defun mmm-match-and-verify mmm-match-and-verify
241,9525
(defun mmm-get-form mmm-get-form
267,10583
(defun mmm-default-get-form mmm-default-get-form
278,11079

mmm/mmm-cmds.el,1027
(defun mmm-ify-by-class mmm-ify-by-class
40,1179
(defun mmm-ify-region mmm-ify-region
68,2165
(defun mmm-ify-by-regexpmmm-ify-by-regexp
80,2593
(defun mmm-parse-buffer mmm-parse-buffer
100,3244
(defun mmm-parse-region mmm-parse-region
109,3580
(defun mmm-parse-block mmm-parse-block
118,3959
(defun mmm-get-block mmm-get-block
135,4710
(defun mmm-clear-current-region mmm-clear-current-region
151,5095
(defun mmm-clear-regions mmm-clear-regions
156,5259
(defun mmm-clear-all-regions mmm-clear-all-regions
161,5405
(defun mmm-reparse-current-region mmm-reparse-current-region
169,5569
(defun* mmm-end-current-region mmm-end-current-region
188,6185
(defun mmm-insert-region mmm-insert-region
226,7768
(defun mmm-insert-by-key mmm-insert-by-key
245,8630
(defun mmm-get-insertion-spec mmm-get-insertion-spec
291,10888
(defun mmm-insertion-help mmm-insertion-help
318,11967
(defun mmm-display-insertion-key mmm-display-insertion-key
328,12337
(defun mmm-get-all-insertion-keys mmm-get-all-insertion-keys
350,13159

mmm/mmm-compat.el,634
(defvar mmm-xemacs mmm-xemacs
40,1291
(defvar mmm-keywords-usedmmm-keywords-used
49,1594
(defmacro mmm-regexp-opt mmm-regexp-opt
90,2591
(defvar mmm-evaporate-propertymmm-evaporate-property
109,3240
(defmacro mmm-set-keymap-default mmm-set-keymap-default
127,4006
(defmacro mmm-event-key mmm-event-key
136,4448
(defvar skeleton-positions skeleton-positions
145,4667
(defun mmm-fixup-skeleton mmm-fixup-skeleton
146,4698
(defmacro mmm-make-temp-buffer mmm-make-temp-buffer
158,5135
(defvar mmm-font-lock-available-p mmm-font-lock-available-p
171,5531
(defmacro mmm-set-font-lock-defaults mmm-set-font-lock-defaults
178,5745

mmm/mmm-mason.el,592
(defvar mmm-mason-perl-tagsmmm-mason-perl-tags
41,1225
(defvar mmm-mason-pseudo-perl-tagsmmm-mason-pseudo-perl-tags
45,1366
(defvar mmm-mason-non-perl-tagsmmm-mason-non-perl-tags
48,1442
(defvar mmm-mason-perl-tags-regexpmmm-mason-perl-tags-regexp
51,1543
(defvar mmm-mason-pseudo-perl-tags-regexpmmm-mason-pseudo-perl-tags-regexp
56,1738
(defvar mmm-mason-tag-names-regexpmmm-mason-tag-names-regexp
61,1955
(defun mmm-mason-verify-inline mmm-mason-verify-inline
66,2175
(defun mmm-mason-start-line mmm-mason-start-line
154,5041
(defun mmm-mason-end-line mmm-mason-end-line
159,5106

mmm/mmm-mode.el,1496
(defun mmm-mode mmm-mode
106,4116
(defun mmm-mode-on mmm-mode-on
312,13247
(defun mmm-mode-off mmm-mode-off
352,14969
(defvar mmm-mode-map mmm-mode-map
375,15634
(defvar mmm-mode-prefix-map mmm-mode-prefix-map
378,15709
(defvar mmm-mode-menu-map mmm-mode-menu-map
381,15819
(defun mmm-define-key mmm-define-key
384,15910
(define-key mmm-mode-prefix-map mmm-mode-prefix-map
406,16585
(define-key mmm-mode-prefix-map mmm-mode-prefix-map
413,16843
(define-key mmm-mode-map mmm-mode-map
416,16954
(define-key mmm-mode-menu-map mmm-mode-menu-map
419,17056
(define-key mmm-mode-menu-map mmm-mode-menu-map
421,17128
(define-key mmm-mode-menu-map mmm-mode-menu-map
423,17187
(define-key mmm-mode-menu-map mmm-mode-menu-map
425,17268
(define-key mmm-mode-menu-map mmm-mode-menu-map
427,17349
(define-key mmm-mode-menu-map mmm-mode-menu-map
429,17436
(define-key mmm-mode-menu-map mmm-mode-menu-map
432,17530
(define-key mmm-mode-menu-map mmm-mode-menu-map
434,17590
(define-key mmm-mode-menu-map mmm-mode-menu-map
437,17681
(define-key mmm-mode-menu-map mmm-mode-menu-map
439,17741
(define-key mmm-mode-menu-map mmm-mode-menu-map
441,17848
(define-key mmm-mode-menu-map mmm-mode-menu-map
443,17933
(define-key mmm-mode-menu-map mmm-mode-menu-map
446,18019
(define-key mmm-mode-menu-map mmm-mode-menu-map
448,18079
(define-key mmm-mode-menu-map mmm-mode-menu-map
450,18192
(define-key mmm-mode-menu-map mmm-mode-menu-map
452,18277
(define-key mmm-mode-map mmm-mode-map
455,18360

mmm/mmm-region.el,2300
(defun mmm-overlay-at mmm-overlay-at
51,1642
(defun mmm-overlays-at mmm-overlays-at
56,1843
(defun mmm-included-p mmm-included-p
69,2525
(defun mmm-overlays-in mmm-overlays-in
82,2903
(defun mmm-sort-overlays mmm-sort-overlays
100,3840
(defvar mmm-current-overlay mmm-current-overlay
109,4110
(defvar mmm-previous-overlay mmm-previous-overlay
114,4325
(defvar mmm-current-submode mmm-current-submode
119,4513
(defvar mmm-previous-submode mmm-previous-submode
124,4713
(defun mmm-update-current-submode mmm-update-current-submode
129,4886
(defun mmm-set-current-submode mmm-set-current-submode
141,5364
(defun mmm-submode-at mmm-submode-at
152,5856
(defun mmm-match-front mmm-match-front
161,6139
(defun mmm-match-back mmm-match-back
177,6780
(defun mmm-front-start mmm-front-start
195,7402
(defun mmm-back-end mmm-back-end
203,7672
(defun mmm-make-marker mmm-make-marker
216,7969
(defun* mmm-make-regionmmm-make-region
228,8428
(defun mmm-get-face mmm-get-face
286,11150
(defun mmm-clear-overlays mmm-clear-overlays
300,11459
(defun mmm-update-mode-info mmm-update-mode-info
314,11871
(defun mmm-update-submode-region mmm-update-submode-region
397,16038
(defun mmm-add-hooks mmm-add-hooks
417,16958
(defun mmm-remove-hooks mmm-remove-hooks
421,17093
(defun mmm-get-local-variables-list mmm-get-local-variables-list
427,17220
(defun mmm-get-locals mmm-get-locals
447,18140
(defun mmm-get-saved-local mmm-get-saved-local
460,18721
(defun mmm-set-local-variables mmm-set-local-variables
464,18886
(defun mmm-get-saved-local-variables mmm-get-saved-local-variables
475,19327
(defun mmm-save-changed-local-variables mmm-save-changed-local-variables
483,19644
(defun mmm-clear-local-variables mmm-clear-local-variables
502,20502
(defun mmm-enable-font-lock mmm-enable-font-lock
513,20781
(defun mmm-update-font-lock-buffer mmm-update-font-lock-buffer
521,21041
(defun mmm-refontify-maybe mmm-refontify-maybe
534,21564
(defun mmm-submode-changes-in mmm-submode-changes-in
545,21921
(defun mmm-regions-in mmm-regions-in
558,22406
(defun mmm-regions-alist mmm-regions-alist
572,22954
(defun mmm-fontify-region mmm-fontify-region
589,23600
(defun mmm-fontify-region-list mmm-fontify-region-list
607,24494
(defun mmm-beginning-of-syntax mmm-beginning-of-syntax
629,25412

mmm/mmm-rpm.el,242
(defconst mmm-rpm-sh-start-tagsmmm-rpm-sh-start-tags
48,1617
(defvar mmm-rpm-sh-end-tagsmmm-rpm-sh-end-tags
53,1841
(defvar mmm-rpm-sh-start-regexpmmm-rpm-sh-start-regexp
57,2015
(defvar mmm-rpm-sh-end-regexpmmm-rpm-sh-end-regexp
61,2193

mmm/mmm-sample.el,269
(defvar mmm-here-doc-mode-alist mmm-here-doc-mode-alist
81,2448
(defun mmm-here-doc-get-mode mmm-here-doc-get-mode
90,2933
(defun mmm-file-variables-verify mmm-file-variables-verify
196,6459
(defun mmm-file-variables-find-back mmm-file-variables-find-back
220,7495

mmm/mmm-univ.el,52
(defun mmm-univ-get-mode mmm-univ-get-mode
38,1205

mmm/mmm-utils.el,371
(defmacro mmm-valid-buffer mmm-valid-buffer
41,1299
(defmacro mmm-save-all mmm-save-all
60,1943
(defun mmm-format-string mmm-format-string
73,2232
(defun mmm-format-matches mmm-format-matches
84,2684
(defmacro mmm-save-keyword mmm-save-keyword
105,3362
(defmacro mmm-save-keywords mmm-save-keywords
113,3690
(defun mmm-looking-back-at mmm-looking-back-at
126,4224

mmm/mmm-vars.el,3586
(defgroup mmm mmm
86,2527
(defvar mmm-c-derived-modesmmm-c-derived-modes
93,2637
(defvar mmm-save-local-variables mmm-save-local-variables
96,2743
(defvar mmm-buffer-saved-locals mmm-buffer-saved-locals
176,6248
(defvar mmm-region-saved-locals-defaults mmm-region-saved-locals-defaults
181,6448
(defvar mmm-region-saved-locals-for-dominant mmm-region-saved-locals-for-dominant
187,6708
(defgroup mmm-faces mmm-faces
197,7085
(defcustom mmm-submode-decoration-level mmm-submode-decoration-level
203,7256
(defface mmm-init-submode-face mmm-init-submode-face
217,7966
(defface mmm-cleanup-submode-face mmm-cleanup-submode-face
221,8106
(defface mmm-declaration-submode-face mmm-declaration-submode-face
225,8243
(defface mmm-comment-submode-face mmm-comment-submode-face
229,8389
(defface mmm-output-submode-face mmm-output-submode-face
233,8542
(defface mmm-special-submode-face mmm-special-submode-face
237,8691
(defface mmm-code-submode-face mmm-code-submode-face
241,8855
(defface mmm-default-submode-face mmm-default-submode-face
245,8994
(defcustom mmm-mode-string mmm-mode-string
253,9232
(defcustom mmm-submode-mode-line-format mmm-submode-mode-line-format
258,9363
(defvar mmm-classes mmm-classes
268,9635
(defvar mmm-global-classes mmm-global-classes
274,9880
(defcustom mmm-mode-ext-classes-alist mmm-mode-ext-classes-alist
281,10062
(defun mmm-add-mode-ext-class mmm-add-mode-ext-class
300,10880
(defcustom mmm-major-mode-preferencesmmm-major-mode-preferences
309,11205
(defun mmm-add-to-major-mode-preferences mmm-add-to-major-mode-preferences
327,12003
(defun mmm-ensure-modename mmm-ensure-modename
343,12789
(defun mmm-modename->function mmm-modename->function
352,13099
(defcustom mmm-mode-prefix-key mmm-mode-prefix-key
366,13557
(defcustom mmm-command-modifiers mmm-command-modifiers
371,13684
(defcustom mmm-insert-modifiers mmm-insert-modifiers
385,14317
(defcustom mmm-use-old-command-keys mmm-use-old-command-keys
400,14995
(defun mmm-use-old-command-keys mmm-use-old-command-keys
410,15459
(defcustom mmm-mode-hook mmm-mode-hook
418,15658
(defun mmm-run-constructed-hook mmm-run-constructed-hook
438,16468
(defun mmm-run-major-hook mmm-run-major-hook
446,16854
(defun mmm-run-submode-hook mmm-run-submode-hook
449,16931
(defvar mmm-class-hooks-run mmm-class-hooks-run
452,17018
(defun mmm-run-class-hook mmm-run-class-hook
457,17190
(defcustom mmm-major-mode-hook mmm-major-mode-hook
465,17391
(defun mmm-run-major-mode-hook mmm-run-major-mode-hook
479,18022
(defcustom mmm-global-mode mmm-global-mode
486,18160
(defcustom mmm-never-modesmmm-never-modes
503,18748
(defvar mmm-set-file-name-for-modes mmm-set-file-name-for-modes
521,19048
(defvar mmm-mode mmm-mode
532,19369
(defvar mmm-primary-mode mmm-primary-mode
540,19577
(defvar mmm-classes-alist mmm-classes-alist
548,19795
(defun mmm-add-classes mmm-add-classes
668,26175
(defun mmm-add-group mmm-add-group
673,26340
(defconst mmm-version mmm-version
686,26804
(defun mmm-version mmm-version
689,26869
(defvar mmm-temp-buffer-name mmm-temp-buffer-name
696,27012
(defvar mmm-interactive-history mmm-interactive-history
702,27142
(defun mmm-add-to-history mmm-add-to-history
708,27411
(defun mmm-clear-history mmm-clear-history
711,27494
(defvar mmm-mode-ext-classes mmm-mode-ext-classes
719,27679
(defun mmm-get-mode-ext-classes mmm-get-mode-ext-classes
724,27890
(defun mmm-clear-mode-ext-classes mmm-clear-mode-ext-classes
733,28266
(defun mmm-mode-ext-applies mmm-mode-ext-applies
737,28391
(defun mmm-get-all-classes mmm-get-all-classes
751,28875

TODO.developer,1307
   function to to
387,15630
$Id: TODO.developer,2,21
This is an outline file.   Use C-c C-n,4,77
X 55,1529
*** C Improved configurability of command settings,186,7011
  We should let command settings,187,7068
  We should let command settings, etc,187,7068
  - XEmacs pg forces on font-lock,337,13217
    Save foo;413,16753
*** A Doc new bits: font lock keywords,483,19454
*** A Doc new bits: font lock keywords, filename %e,483,19454
  Added proof-{script,484,19511
  Added proof-{script,shell,484,19511
  Added proof-{script,shell,goals,484,19511
  Presently used only in proof-easy-config,485,19571
  - Mention configuring function menus,496,19907
  - document mouse functions,498,19993
  - document mouse functions, proof-cd,498,19993
  - document mouse functions, proof-cd, process quit timeout,498,19993
    X-Symbol,499,20056
    X-Symbol, prog-name-guess,499,20056
*** D Fix INFO-DIR-ENTRY in 513,20564
*** C Fixing up errors caused by pbp-generated commands; currently,579,23041
  should mean generates an error.  With LEGO pbp,582,23247
  tactic which always succeeds,583,23311
  decodes annotations eagerly. Lazily would be faster,591,23667
  the tech report claims --- djs: probably not much faster,592,23736
***  6. Update Emacs and prover versions in texi,681,26739

doc/ProofGeneral.texi,5799
@node TopTop
166,5021
@node PrefacePreface
203,6128
@node Latest news for 3.5 and 3.6Latest news for 3.5 and 3.6
226,6724
@node FutureFuture
265,8412
@node CreditsCredits
300,9962
@node Introducing Proof GeneralIntroducing Proof General
398,13377
@node Quick start guideQuick start guide
453,15369
@node Features of Proof GeneralFeatures of Proof General
507,17938
@node Supported proof assistantsSupported proof assistants
596,21863
@node Prerequisites for this manualPrerequisites for this manual
648,23859
@node Organization of this manualOrganization of this manual
692,25485
@node Basic Script ManagementBasic Script Management
718,26312
@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar
737,26917
@node Proof scriptsProof scripts
964,35452
@node Script buffersScript buffers
1007,37572
@node Locked queue and editing regionsLocked queue and editing regions
1029,38149
@node Goal-save sequencesGoal-save sequences
1085,40296
@node Active scripting bufferActive scripting buffer
1122,41782
@node Summary of Proof General buffersSummary of Proof General buffers
1191,45202
@node Script editing commandsScript editing commands
1253,47876
@node Script processing commandsScript processing commands
1331,50734
@node Proof assistant commandsProof assistant commands
1459,56035
@node Toolbar commandsToolbar commands
1605,60922
@node Interrupting during trace outputInterrupting during trace output
1629,61851
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1668,63774
@node Goals buffer commandsGoals buffer commands
1682,64274
@node Advanced Script ManagementAdvanced Script Management
1771,67806
@node Visibility of completed proofsVisibility of completed proofs
1802,68960
@node Switching between proof scriptsSwitching between proof scripts
1857,70883
@node View of processed files View of processed files 
1894,72855
@node Retracting across filesRetracting across files
1954,75906
@node Asserting across filesAsserting across files
1967,76537
@node Automatic multiple file handlingAutomatic multiple file handling
1980,77103
@node Escaping script managementEscaping script management
2005,78137
@node Experimental featuresExperimental features
2063,80340
@node Support for other PackagesSupport for other Packages
2097,81602
@node Syntax highlightingSyntax highlighting
2129,82477
@node X-Symbol supportX-Symbol support
2168,84098
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2227,86644
@node Support for outline modeSupport for outline mode
2286,88774
@node Support for completionSupport for completion
2312,89904
@node Support for tagsSupport for tags
2369,92069
@node Customizing Proof GeneralCustomizing Proof General
2421,94397
@node Basic optionsBasic options
2461,96067
@node How to customizeHow to customize
2485,96825
@node Display customizationDisplay customization
2536,98927
@node User optionsUser options
2661,104161
@node Changing facesChanging faces
2915,113167
@node Tweaking configuration settingsTweaking configuration settings
2990,115836
@node Hints and TipsHints and Tips
3047,118361
@node Adding your own keybindingsAdding your own keybindings
3066,118962
@node Using file variablesUsing file variables
3122,121495
@node Using abbreviationsUsing abbreviations
3175,123318
@node LEGO Proof GeneralLEGO Proof General
3214,124733
@node LEGO specific commandsLEGO specific commands
3255,126102
@node LEGO tagsLEGO tags
3275,126557
@node LEGO customizationsLEGO customizations
3285,126804
@node Coq Proof GeneralCoq Proof General
3317,127722
@node Coq-specific commandsCoq-specific commands
3333,128131
@node Coq-specific variablesCoq-specific variables
3355,128638
@node Editing multiple proofsEditing multiple proofs
3377,129296
@node User-loaded tacticsUser-loaded tactics
3401,130404
@node Holes featureHoles feature
3465,132878
@node Isabelle Proof GeneralIsabelle Proof General
3492,134164
@node Classic IsabelleClassic Isabelle
3561,137487
@node ML filesML files
3577,137925
@node Theory filesTheory files
3648,140350
@node General commands for IsabelleGeneral commands for Isabelle
3702,142821
@node Specific commands for IsabelleSpecific commands for Isabelle
3714,143303
@node Isabelle customizationsIsabelle customizations
3743,144243
@node Isabelle/IsarIsabelle/Isar
3808,146341
@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar
3829,147104
@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar
3836,147358
@node Logics and SettingsLogics and Settings
3923,149886
@node HOL Proof GeneralHOL Proof General
3964,151574
@node Shell Proof GeneralShell Proof General
4005,153358
@node Obtaining and InstallingObtaining and Installing
4041,154816
@node Obtaining Proof GeneralObtaining Proof General
4057,155229
@node Installing Proof General from tarballInstalling Proof General from tarball
4088,156468
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4113,157300
@node Setting the names of binariesSetting the names of binaries
4128,157708
@node Notes for syssiesNotes for syssies
4156,158648
@node Known BugsKnown Bugs
4229,161581
@node ReferencesReferences
4242,161982
@node History of Proof GeneralHistory of Proof General
4282,163006
@node Old News for 3.0Old News for 3.0
4373,167108
@node Old News for 3.1Old News for 3.1
4443,170802
@node Old News for 3.2Old News for 3.2
4469,171974
@node Old News for 3.3Old News for 3.3
4530,174977
@node Old News for 3.4Old News for 3.4
4549,175874
@node Function IndexFunction Index
4572,176930
@node Variable IndexVariable Index
4576,177006
@node Keystroke IndexKeystroke Index
4580,177086
@node Concept IndexConcept Index
4584,177152

doc/PG-adapting.texi,3863
@node TopTop
157,4773
@node IntroductionIntroduction
195,5918
@node FutureFuture
236,7571
@node CreditsCredits
272,9167
@node Beginning with a New ProverBeginning with a New Prover
282,9459
@node Overview of adding a new proverOverview of adding a new prover
323,11408
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
397,14829
@node Major modes used by Proof GeneralMajor modes used by Proof General
466,18220
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
539,21303
@node Settings for generic user-level commandsSettings for generic user-level commands
554,21849
@node Menu configurationMenu configuration
599,23585
@node Toolbar configurationToolbar configuration
623,24503
@node Proof Script SettingsProof Script Settings
681,26748
@node Recognizing commands and commentsRecognizing commands and comments
703,27328
@node Recognizing proofsRecognizing proofs
824,32855
@node Recognizing other elementsRecognizing other elements
936,37669
@node Configuring undo behaviourConfiguring undo behaviour
1062,43147
@node Nested proofsNested proofs
1200,48488
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1240,50115
@node Activate scripting hookActivate scripting hook
1263,51061
@node Automatic multiple filesAutomatic multiple files
1287,51925
@node CompletionsCompletions
1309,52772
@node Proof Shell SettingsProof Shell Settings
1349,54250
@node Proof shell commandsProof shell commands
1380,55532
@node Script input to the shellScript input to the shell
1543,62407
@node Settings for matching various output from proof processSettings for matching various output from proof process
1610,65450
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1741,71214
@node Hooks and other settingsHooks and other settings
1951,80767
@node Goals Buffer SettingsGoals Buffer Settings
2047,84600
@node Splash Screen SettingsSplash Screen Settings
2124,87708
@node Global ConstantsGlobal Constants
2150,88466
@node Handling Multiple FilesHandling Multiple Files
2176,89315
@node Configuring Editing SyntaxConfiguring Editing Syntax
2328,97099
@node Configuring Font LockConfiguring Font Lock
2385,99216
@node Configuring X-SymbolConfiguring X-Symbol
2472,103459
@node Writing More Lisp CodeWriting More Lisp Code
2532,105982
@node Default values for generic settingsDefault values for generic settings
2549,106627
@node Adding prover-specific configurationsAdding prover-specific configurations
2579,107710
@node Useful variablesUseful variables
2622,108980
@node Useful functions and macrosUseful functions and macros
2648,109774
@node Internals of Proof GeneralInternals of Proof General
2750,113651
@node SpansSpans
2778,114559
@node Proof General site configurationProof General site configuration
2791,114933
@node Configuration variable mechanismsConfiguration variable mechanisms
2871,118077
@node Global variablesGlobal variables
2989,123313
@node Proof script modeProof script mode
3059,125863
@node Proof shell modeProof shell mode
3318,137518
@node DebuggingDebugging
3724,153565
@node Plans and IdeasPlans and Ideas
3767,154460
@node Proof by pointing and similar featuresProof by pointing and similar features
3788,155182
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3826,156840
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3871,159065
@node Demonstration InstantiationsDemonstration Instantiations
3901,160096
@node demoisa-easy.eldemoisa-easy.el
3917,160527
@node demoisa.eldemoisa.el
3980,162765
@node Function IndexFunction Index
4148,168281
@node Variable IndexVariable Index
4152,168357
@node Concept IndexConcept Index
4161,168536