coq/coq-abbrev.el,495
(defun holes-show-doc 10,310
(defun coq-local-vars-list-show-doc 14,386
(defconst coq-tactics-menu19,486
(defconst coq-tactics-abbrev-table24,663
(defconst coq-tacticals-menu27,780
(defconst coq-tacticals-abbrev-table31,889
(defconst coq-commands-menu34,980
(defconst coq-commands-abbrev-table41,1203
(defconst coq-terms-menu44,1292
(defconst coq-terms-abbrev-table49,1430
(defun coq-install-abbrevs 56,1624
(defpgdefault menu-entries76,2361
(defpgdefault help-menu-entries169,5947

coq/coq-db.el,601
(defconst coq-syntax-db 22,534
(defvar coq-user-tactics-db58,1907
(defun coq-insert-from-db 68,2256
(defun coq-build-regexp-list-from-db 86,3037
(defun max-length-db 108,4090
(defun coq-build-menu-from-db-internal 120,4365
(defun coq-build-title-menu 155,5988
(defun coq-sort-menu-entries 164,6356
(defun coq-build-menu-from-db 170,6486
(defcustom coq-holes-minor-mode 192,7323
(defun coq-build-abbrev-table-from-db 198,7467
(defun filter-state-preserving 217,8105
(defun filter-state-changing 222,8259
(defface coq-solve-tactics-face 229,8480
(defconst coq-solve-tactics-face 237,8737

coq/coq.el,6556
(defcustom coq-translate-to-v8 45,1301
(defun coq-build-prog-args 51,1481
(defcustom coq-compile-file-command 64,1861
(defcustom coq-use-makefile 72,2180
(defcustom coq-default-undo-limit 80,2403
(defconst coq-shell-init-cmd 85,2531
(defcustom coq-prog-env 97,2809
(defconst coq-shell-restart-cmd 105,3061
(defvar coq-shell-prompt-pattern 112,3321
(defvar coq-shell-cd 122,3714
(defvar coq-shell-abort-goal-regexp 126,3874
(defvar coq-shell-proof-completed-regexp 129,4000
(defvar coq-goal-regexp132,4152
(defun coq-library-directory 139,4266
(defcustom coq-tags 146,4446
(defconst coq-interrupt-regexp 151,4596
(defcustom coq-www-home-page 156,4717
(defvar coq-outline-regexp166,4888
(defvar coq-outline-heading-end-regexp 173,5102
(defvar coq-shell-outline-regexp 175,5156
(defvar coq-shell-outline-heading-end-regexp 176,5206
(defconst coq-kill-goal-command 181,5316
(defconst coq-forget-id-command 182,5359
(defconst coq-back-n-command 183,5406
(defconst coq-state-preserving-tactics-regexp 187,5550
(defconst coq-state-changing-commands-regexp189,5651
(defconst coq-state-preserving-commands-regexp 191,5758
(defconst coq-commands-regexp 193,5870
(defvar coq-retractable-instruct-regexp 195,5948
(defvar coq-non-retractable-instruct-regexp 197,6039
(defvar coq-keywords-section201,6179
(defvar coq-section-regexp 204,6273
(defun coq-set-undo-limit 241,7419
(defconst coq-keywords-decl-defn-regexp252,7858
(defun coq-proof-mode-p 256,8008
(defun coq-is-comment-or-proverprocp 267,8416
(defun coq-is-goalsave-p 269,8520
(defun coq-is-module-equal-p 270,8595
(defun coq-is-def-p 273,8791
(defun coq-is-decl-defn-p 275,8899
(defun coq-state-preserving-command-p 280,9066
(defun coq-command-p 283,9200
(defun coq-state-preserving-tactic-p 286,9300
(defun coq-state-changing-tactic-p 291,9448
(defun coq-state-changing-command-p 298,9682
(defun coq-section-or-module-start-p 305,10028
(defun build-list-id-from-string 314,10269
(defun coq-last-prompt-info 327,10799
(defun coq-last-prompt-info-safe 339,11340
(defvar coq-last-but-one-statenum 345,11597
(defvar coq-last-but-one-proofnum 351,11895
(defvar coq-last-but-one-proofstack 354,11993
(defun coq-get-span-statenum 357,12103
(defun coq-get-span-proofnum 362,12218
(defun coq-get-span-proofstack 367,12333
(defun coq-set-span-statenum 372,12477
(defun coq-get-span-goalcmd 377,12608
(defun coq-set-span-goalcmd 382,12722
(defun coq-set-span-proofnum 387,12852
(defun coq-set-span-proofstack 392,12983
(defun proof-last-locked-span 397,13143
(defun coq-set-state-infos 412,13747
(defun count-not-intersection 452,15826
(defun  coq-find-and-forget-v81 483,17080
(defun coq-find-and-forget-v80 511,18212
(defun coq-find-and-forget 606,22911
(defvar coq-current-goal 619,23451
(defun coq-goal-hyp 622,23516
(defun coq-state-preserving-p 635,23949
(defconst notation-print-kinds-table 649,24454
(defun coq-PrintScope 653,24622
(defun coq-guess-or-ask-for-string 671,25177
(defun coq-ask-do 685,25745
(defun coq-SearchIsos 694,26133
(defun coq-SearchConstant 700,26366
(defun coq-SearchRewrite 704,26459
(defun coq-SearchAbout 708,26557
(defun coq-Print 712,26649
(defun coq-About 716,26771
(defun coq-LocateConstant 720,26888
(defun coq-LocateLibrary 726,27023
(defun coq-addquotes 732,27173
(defun coq-LocateNotation 734,27221
(defun coq-Pwd 741,27420
(defun coq-Inspect 747,27552
(defun coq-PrintSection(751,27652
(defun coq-Print-implicit 755,27745
(defun coq-Check 760,27896
(defun coq-Show 765,28004
(defun coq-Compile 779,28447
(defun coq-guess-command-line 793,28767
(defpacustom use-editing-holes 832,30474
(defun coq-mode-config 842,30811
(defvar coq-last-hybrid-pre-string 950,34765
(defun coq-hybrid-ouput-goals-response-p 953,34944
(defun coq-hybrid-ouput-goals-response 959,35203
(defun coq-shell-mode-config 980,36165
(defun coq-goals-mode-config 1025,38281
(defun coq-response-config 1032,38525
(defpacustom print-fully-explicit 1057,39350
(defpacustom print-implicit 1062,39498
(defpacustom print-coercions 1067,39664
(defpacustom print-match-wildcards 1072,39808
(defpacustom print-elim-types 1077,39988
(defpacustom printing-depth 1082,40154
(defpacustom undo-depth 1087,40315
(defpacustom time-commands 1092,40462
(defpacustom undo-limit 1096,40572
(defpacustom auto-compile-vos 1101,40674
(defun coq-maybe-compile-buffer 1130,41790
(defun coq-ancestors-of 1167,43324
(defun coq-all-ancestors-of 1190,44291
(defconst coq-require-command-regexp 1202,44684
(defun coq-process-require-command 1207,44893
(defun coq-included-children 1212,45020
(defun coq-process-file 1233,45859
(defun coq-preprocessing 1248,46398
(defun coq-fake-constant-markup 1263,46817
(defun coq-create-span-menu 1284,47623
(defconst module-kinds-table 1301,48122
(defconst modtype-kinds-table1305,48272
(defun coq-insert-section-or-module 1309,48401
(defconst reqkinds-kinds-table1332,49261
(defun coq-insert-requires 1337,49406
(defun coq-end-Section 1353,49912
(defun coq-insert-intros 1371,50496
(defun coq-insert-infoH-hook 1384,51021
(defun coq-insert-as 1388,51099
(defun coq-insert-match 1409,51848
(defun coq-insert-tactic 1441,53026
(defun coq-insert-tactical 1447,53265
(defun coq-insert-command 1453,53514
(defun coq-insert-term 1459,53758
(define-key coq-keymap 1465,53955
(define-key coq-keymap 1466,54013
(define-key coq-keymap 1467,54070
(define-key coq-keymap 1468,54139
(define-key coq-keymap 1469,54195
(define-key coq-keymap 1470,54244
(define-key coq-keymap 1471,54302
(define-key coq-keymap 1473,54363
(define-key coq-keymap 1474,54422
(define-key coq-keymap 1476,54486
(define-key coq-keymap 1477,54546
(define-key coq-keymap 1479,54602
(define-key coq-keymap 1480,54652
(define-key coq-keymap 1481,54702
(define-key coq-keymap 1482,54752
(define-key coq-keymap 1483,54806
(define-key coq-keymap 1484,54865
(defvar last-coq-error-location 1492,54996
(defun coq-get-last-error-location 1501,55395
(defun coq-highlight-error 1548,57733
(defvar coq-allow-highlight-error 1583,58952
(defun coq-decide-highlight-error 1590,59279
(defun coq-highlight-error-hook 1594,59401
(defun first-word-of-buffer 1605,59794
(defun coq-show-first-goal 1613,59997
(defvar coq-modeline-string2 1630,60692
(defvar coq-modeline-string1 1631,60736
(defvar coq-modeline-string0 1632,60779
(defun coq-build-subgoals-string 1633,60824
(defun coq-update-minor-mode-alist 1638,60992
(defun is-not-split-vertic 1664,62060
(defun optim-resp-windows 1673,62499

coq/coq-indent.el,2222
(defconst coq-any-command-regexp17,315
(defconst coq-indent-inner-regexp20,406
(defconst coq-comment-start-regexp 31,794
(defconst coq-comment-end-regexp 32,837
(defconst coq-comment-start-or-end-regexp33,878
(defconst coq-indent-open-regexp35,986
(defconst coq-indent-close-regexp40,1160
(defconst coq-indent-closepar-regexp 45,1341
(defconst coq-indent-closematch-regexp 46,1386
(defconst coq-indent-openpar-regexp 47,1457
(defconst coq-indent-openmatch-regexp 48,1501
(defconst coq-indent-any-regexp49,1581
(defconst coq-indent-kw54,1859
(defconst coq-indent-pattern-regexp 64,2313
(defun coq-indent-goal-command-p 68,2416
(defconst coq-end-command-regexp90,3471
(defun coq-search-comment-delimiter-forward 95,3623
(defun coq-search-comment-delimiter-backward 104,3953
(defun coq-skip-until-one-comment-backward 111,4227
(defun coq-skip-until-one-comment-forward 126,4934
(defun coq-looking-at-comment 137,5452
(defun coq-find-comment-start 141,5593
(defun coq-find-comment-end 152,6026
(defun coq-looking-at-syntactic-context 164,6519
(defconst coq-end-command-or-comment-regexp170,6741
(defconst coq-end-command-or-comment-start-regexp173,6850
(defun coq-find-not-in-comment-backward 177,6968
(defun coq-find-not-in-comment-forward 197,7869
(defun coq-find-command-end-backward 221,9011
(defun coq-find-command-end-forward 230,9402
(defun coq-find-command-end 239,9779
(defun coq-find-current-start 247,10111
(defun coq-find-real-start 256,10402
(defun coq-command-at-point 263,10621
(defun coq-indent-only-spaces-on-line 270,10898
(defun coq-indent-find-reg 276,11175
(defun coq-find-no-syntactic-on-line 290,11711
(defun coq-back-to-indentation-prevline 303,12184
(defun coq-find-unclosed 347,14098
(defun coq-find-at-same-level-zero 377,15399
(defun coq-find-unopened 405,16564
(defun coq-find-last-unopened 448,18014
(defun coq-end-offset 459,18411
(defun coq-indent-command-offset 484,19202
(defun coq-indent-expr-offset 531,21026
(defun coq-indent-comment-offset 647,25729
(defun coq-indent-offset 679,27187
(defun coq-indent-calculate 697,28050
(defun coq-indent-line 700,28138
(defun coq-indent-line-not-comments 710,28504
(defun coq-indent-region 720,28893

coq/coq-local-vars.el,280
(defconst coq-local-vars-doc 17,305
(defun coq-insert-coq-prog-name 75,2833
(defun coq-read-directory 86,3306
(defun coq-extract-directories-from-args 110,4409
(defun coq-ask-prog-args 125,4961
(defun coq-ask-prog-name 147,6065
(defun coq-ask-insert-coq-prog-name 165,6820

coq/coq-syntax.el,2666
(defcustom coq-prog-name 13,431
(defvar coq-version-is-V8 34,1430
(defvar coq-version-is-V8-0 36,1509
(defvar coq-version-is-V8-1 43,1887
(defun coq-determine-version 52,2320
(defcustom coq-user-tactics-db 97,4178
(defcustom coq-user-commands-db 114,4691
(defcustom coq-user-tacticals-db 130,5210
(defcustom coq-user-solve-tactics-db 146,5731
(defcustom coq-user-reserved-db 164,6252
(defvar coq-tactics-db182,6783
(defvar coq-solve-tactics-db337,14851
(defvar coq-tacticals-db361,15698
(defvar coq-decl-db385,16585
(defvar coq-defn-db407,17803
(defvar coq-goal-starters-db460,21789
(defvar coq-other-commands-db487,23344
(defvar coq-commands-db611,32541
(defvar coq-terms-db618,32767
(defun coq-count-match 682,35419
(defun coq-goal-command-str-v80-p 701,36282
(defun coq-module-opening-p 724,37155
(defun coq-section-command-p 735,37571
(defun coq-goal-command-str-v81-p 739,37668
(defun coq-goal-command-p-v81 754,38337
(defun coq-goal-command-str-p 764,38677
(defun coq-goal-command-p 774,39043
(defvar coq-keywords-save-strict782,39355
(defvar coq-keywords-save791,39468
(defun coq-save-command-p 795,39546
(defvar coq-keywords-kill-goal 804,39840
(defvar coq-keywords-state-changing-misc-commands808,39931
(defvar coq-keywords-goal811,40056
(defvar coq-keywords-decl814,40139
(defvar coq-keywords-defn817,40213
(defvar coq-keywords-state-changing-commands821,40288
(defvar coq-keywords-state-preserving-commands830,40549
(defvar coq-keywords-commands835,40765
(defvar coq-solve-tactics840,40914
(defvar coq-tacticals844,41035
(defvar coq-reserved850,41174
(defvar coq-state-changing-tactics861,41503
(defvar coq-state-preserving-tactics864,41612
(defvar coq-tactics868,41726
(defvar coq-retractable-instruct871,41815
(defvar coq-non-retractable-instruct874,41925
(defvar coq-keywords878,42053
(defvar coq-symbols885,42221
(defvar coq-error-regexp 904,42434
(defvar coq-id 907,42662
(defvar coq-id-shy 908,42687
(defvar coq-ids 910,42741
(defun coq-first-abstr-regexp 912,42782
(defcustom coq-variable-highlight-enable 915,42878
(defvar coq-font-lock-terms921,43005
(defconst coq-save-command-regexp-strict942,44005
(defconst coq-save-command-regexp946,44172
(defconst coq-save-with-hole-regexp950,44325
(defconst coq-goal-command-regexp954,44484
(defconst coq-goal-with-hole-regexp957,44584
(defconst coq-decl-with-hole-regexp961,44717
(defconst coq-defn-with-hole-regexp968,44966
(defconst coq-with-with-hole-regexp978,45255
(defvar coq-font-lock-keywords-1984,45548
(defvar coq-font-lock-keywords 1011,46878
(defun coq-init-syntax-table 1013,46936
(defconst coq-generic-expression1042,47835

coq/coq-unicode-tokens.el,413
(defconst coq-token-format 18,631
(defconst coq-token-match 19,664
(defconst coq-hexcode-match 20,695
(defcustom coq-token-symbol-map22,729
(defcustom coq-shortcut-alist88,2382
(defconst coq-control-char-format-regexp 177,4396
(defconst coq-control-char-format 181,4522
(defconst coq-control-characters 183,4565
(defconst coq-control-region-format-regexp 187,4659
(defconst coq-control-regions 189,4742

demoisa/demoisa.el,349
(defcustom isabelledemo-prog-name 54,1810
(defcustom isabelledemo-web-page59,1932
(defun demoisa-config 70,2162
(defun demoisa-shell-config 91,2954
(define-derived-mode demoisa-mode 117,3931
(define-derived-mode demoisa-shell-mode 122,4054
(define-derived-mode demoisa-response-mode 127,4197
(define-derived-mode demoisa-goals-mode 131,4324

isar/isabelle-system.el,1347
(defgroup isabelle 26,782
(defcustom isabelle-web-page30,910
(defcustom isa-isabelle-command39,1127
(defvar isabelle-not-found 57,1810
(defun isa-set-isabelle-command 60,1925
(defun isa-shell-command-to-string 83,2933
(defun isa-getenv 89,3157
(defcustom isabelle-program-name-override 109,3849
(defvar isabelle-prog-name 120,4195
(defun isa-tool-list-logics 123,4305
(defcustom isabelle-logics-available 130,4544
(defcustom isabelle-chosen-logic 140,4881
(defvar isabelle-chosen-logic-prev 156,5465
(defun isabelle-hack-local-variables-function 159,5587
(defun isabelle-set-prog-name 171,6028
(defun isabelle-choose-logic 196,7220
(defun isa-view-doc 215,7982
(defun isa-tool-list-docs 224,8248
(defconst isabelle-verbatim-regexp 242,8971
(defun isabelle-verbatim 245,9113
(defcustom isabelle-refresh-logics 252,9274
(defvar isabelle-docs-menu 260,9602
(defvar isabelle-logics-menu-entries 267,9888
(defun isabelle-logics-menu-calculate 270,9961
(defvar isabelle-time-to-refresh-logics 291,10603
(defun isabelle-logics-menu-refresh 295,10698
(defun isabelle-menu-bar-update-logics 310,11331
(defun isabelle-load-isar-keywords 326,11961
(defun isabelle-convert-idmarkup-to-subterm 347,12677
(defun isabelle-create-span-menu 371,13688
(defun isabelle-xml-sml-escapes 387,14130
(defun isabelle-process-pgip 390,14231

isar/isar.el,1523
(defcustom isar-keywords-name 33,765
(defpgdefault completion-table 50,1288
(defcustom isar-web-page52,1341
(defun isar-strip-terminators 66,1691
(defun isar-markup-ml 79,2068
(defun isar-mode-config-set-variables 84,2203
(defun isar-shell-mode-config-set-variables 157,5307
(defun isar-configure-from-settings 242,8678
(defpacustom use-find-theorems-form 245,8760
(defun isar-set-proof-find-theorems-command 250,8926
(defun isar-remove-file 260,9148
(defun isar-shell-compute-new-files-list 270,9545
(define-derived-mode isar-shell-mode 288,10131
(define-derived-mode isar-response-mode 293,10254
(define-derived-mode isar-goals-mode 298,10382
(define-derived-mode isar-mode 303,10503
(defpgdefault menu-entries360,12525
(defalias 'isar-set-command isar-set-command
390,13808
(defpgdefault help-menu-entries 392,13864
(defun isar-count-undos 395,13940
(defun isar-find-and-forget 422,15054
(defun isar-goal-command-p 461,16634
(defun isar-global-save-command-p 466,16811
(defvar isar-current-goal 487,17672
(defun isar-state-preserving-p 490,17738
(defvar isar-shell-current-line-width 515,18935
(defun isar-shell-adjust-line-width 520,19127
(defconst isar-nonwrap-regexp545,20024
(defun isar-string-wrapping 550,20209
(defun isar-positions-of 559,20406
(defun isar-command-wrapping 583,21149
(defun isar-preprocessing 592,21465
(defun isar-mode-config 610,22015
(defun isar-shell-mode-config 621,22573
(defun isar-response-mode-config 627,22770
(defun isar-goals-mode-config 637,23105

isar/isar-find-theorems.el,778
(defun isar-find-theorems-minibuffer 18,713
(defun isar-find-theorems-form 32,1332
(defvar isar-find-theorems-data 74,3132
(defvar isar-find-theorems-widget-number 88,3467
(defvar isar-find-theorems-widget-pattern 91,3565
(defvar isar-find-theorems-widget-intro 94,3657
(defvar isar-find-theorems-widget-elim 97,3743
(defvar isar-find-theorems-widget-dest 100,3827
(defvar isar-find-theorems-widget-name 103,3911
(defvar isar-find-theorems-widget-simp 106,3998
(defun isar-find-theorems-create-searchform111,4144
(defun isar-find-theorems-create-help 251,8759
(defun isar-find-theorems-submit-searchform294,10931
(defun isar-find-theorems-parse-criteria 372,13308
(defun isar-find-theorems-parse-number 465,16408
(defun isar-find-theorems-filter-empty 475,16685

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,482
(defconst isar-keywords-minor206,3642
(defconst isar-keywords-control262,4396
(defconst isar-keywords-diag282,4873
(defconst isar-keywords-theory-begin338,5832
(defconst isar-keywords-theory-switch341,5885
(defconst isar-keywords-theory-end344,5940
(defconst isar-keywords-theory-heading347,5988
(defconst isar-keywords-theory-decl353,6095
(defconst isar-keywords-theory-script412,7076
(defconst isar-keywords-theory-goal416,7153
(defconst isar-keywords-qed429,7370
(defconst isar-keywords-qed-block436,7456
(defconst isar-keywords-qed-global439,7503
(defconst isar-keywords-proof-heading442,7552
(defconst isar-keywords-proof-goal447,7635
(defconst isar-keywords-proof-block454,7734
(defconst isar-keywords-proof-open458,7796
(defconst isar-keywords-proof-close461,7842
(defconst isar-keywords-proof-chain464,7889
(defconst isar-keywords-proof-decl471,7992
(defconst isar-keywords-proof-asm480,8113
(defconst isar-keywords-proof-asm-goal487,8208
(defconst isar-keywords-proof-script490,8263

isar/isar-mmm.el,83
(defconst isar-start-latex-regexp 23,698
(defconst isar-start-sml-regexp 35,1131

isar/isar-syntax.el,3656
(defconst isar-script-syntax-table-entries18,424
(defconst isar-script-syntax-table-alist42,826
(defun isar-init-syntax-table 51,1116
(defun isar-init-output-syntax-table 59,1363
(defconst isar-keyword-begin 75,1810
(defconst isar-keyword-end 76,1848
(defconst isar-keywords-theory-enclose78,1883
(defconst isar-keywords-theory83,2028
(defconst isar-keywords-save88,2173
(defconst isar-keywords-proof-enclose93,2302
(defconst isar-keywords-proof99,2484
(defconst isar-keywords-proof-context106,2689
(defconst isar-keywords-local-goal110,2803
(defconst isar-keywords-proper114,2915
(defconst isar-keywords-improper119,3048
(defconst isar-keywords-outline124,3194
(defconst isar-keywords-fume127,3259
(defconst isar-keywords-indent-open134,3477
(defconst isar-keywords-indent-close140,3661
(defconst isar-keywords-indent-enclose144,3766
(defun isar-regexp-simple-alt 153,3981
(defun isar-ids-to-regexp 173,4741
(defconst isar-ext-first 207,6147
(defconst isar-ext-rest 208,6214
(defconst isar-long-id-stuff 210,6286
(defconst isar-id 211,6360
(defconst isar-idx 212,6430
(defconst isar-string 214,6489
(defconst isar-any-command-regexp216,6549
(defconst isar-name-regexp220,6683
(defconst isar-improper-regexp226,6978
(defconst isar-save-command-regexp230,7126
(defconst isar-global-save-command-regexp233,7227
(defconst isar-goal-command-regexp236,7341
(defconst isar-local-goal-command-regexp239,7449
(defconst isar-comment-start 242,7562
(defconst isar-comment-end 243,7597
(defconst isar-comment-start-regexp 244,7630
(defconst isar-comment-end-regexp 245,7701
(defconst isar-string-start-regexp 247,7769
(defconst isar-string-end-regexp 248,7821
(defun isar-syntactic-context 250,7872
(defconst isar-antiq-regexp 265,8270
(defconst isar-nesting-regexp271,8423
(defun isar-nesting 274,8521
(defun isar-match-nesting 286,8942
(defface isabelle-class-name-face298,9273
(defface isabelle-tfree-name-face306,9456
(defface isabelle-tvar-name-face314,9645
(defface isabelle-free-name-face322,9833
(defface isabelle-bound-name-face330,10017
(defface isabelle-var-name-face338,10204
(defconst isabelle-class-name-face 346,10391
(defconst isabelle-tfree-name-face 347,10453
(defconst isabelle-tvar-name-face 348,10515
(defconst isabelle-free-name-face 349,10576
(defconst isabelle-bound-name-face 350,10637
(defconst isabelle-var-name-face 351,10699
(defvar isar-font-lock-keywords-1354,10761
(defun isar-output-flkprops 372,11771
(defun isar-output-flk 378,12023
(defvar isar-output-font-lock-keywords-1381,12132
(defun isar-strip-output-markup 417,13569
(defvar isar-goals-font-lock-keywords421,13705
(defconst isar-linear-undo 455,14384
(defconst isar-undo 457,14427
(defun isar-remove 459,14470
(defun isar-undos 462,14545
(defun isar-cannot-undo 466,14651
(defconst isar-undo-commands469,14721
(defconst isar-theory-start-regexp477,14860
(defconst isar-end-regexp483,15025
(defconst isar-undo-fail-regexp487,15126
(defconst isar-undo-skip-regexp491,15230
(defconst isar-undo-ignore-regexp494,15351
(defconst isar-undo-remove-regexp497,15416
(defconst isar-any-entity-regexp505,15591
(defconst isar-named-entity-regexp510,15778
(defconst isar-unnamed-entity-regexp515,15955
(defconst isar-next-entity-regexps518,16057
(defconst isar-generic-expression526,16368
(defconst isar-indent-any-regexp537,16685
(defconst isar-indent-inner-regexp539,16778
(defconst isar-indent-enclose-regexp541,16844
(defconst isar-indent-open-regexp543,16960
(defconst isar-indent-close-regexp545,17070
(defconst isar-outline-regexp551,17207
(defconst isar-outline-heading-end-regexp 555,17360

isar/isar-unicode-tokens.el,1188
(defgroup isabelle-tokens 20,510
(defun isar-set-and-restart-tokens 25,650
(defconst isar-control-region-format-regexp38,1003
(defconst isar-control-char-format-regexp 41,1097
(defconst isar-control-char-format	44,1193
(defconst isar-control-region-format-start 45,1242
(defconst isar-control-region-format-end 46,1296
(defcustom isar-control-characters49,1352
(defcustom isar-control-regions62,1727
(defconst isar-token-format 86,2448
(defconst isar-token-variant-format-regexp 90,2600
(defcustom isar-greek-letters-tokens93,2715
(defcustom isar-misc-letters-tokens133,3556
(defcustom isar-symbols-tokens145,3860
(defun isar-try-char 419,10132
(defcustom isar-symbols-tokens-fallbacks423,10276
(defcustom isar-bold-nums-tokens 450,11209
(defun isar-map-letters 466,11599
(defconst isar-script-letters-tokens472,11748
(defconst isar-roman-letters-tokens477,11886
(defconst isar-fraktur-letters-tokens482,12022
(defcustom isar-token-symbol-map 487,12164
(defcustom isar-user-tokens 503,12629
(defun isar-init-token-symbol-map 509,12841
(defcustom isar-symbol-shortcuts529,13298
(defcustom isar-shortcut-alist 600,15435
(defun isar-init-shortcut-alists 608,15694

lclam/lclam.el,524
(defcustom lclam-prog-name 15,386
(defcustom lclam-web-page21,534
(defun lclam-config 32,764
(defun lclam-shell-config 54,1558
(define-derived-mode lclam-proofscript-mode 74,2217
(define-derived-mode lclam-shell-mode 79,2340
(define-derived-mode lclam-response-mode 84,2474
(define-derived-mode lclam-goals-mode 88,2597
(defun lclam-mode 96,2825
(define-derived-mode thy-mode 133,3671
(defvar thy-mode-map 136,3769
(defun thy-add-menus 138,3796
(defun process-thy-file 177,5682
(defun update-thy-only 183,5883

lego/lego.el,1727
(defcustom lego-tags 19,494
(defcustom lego-test-all-name 24,630
(defpgdefault help-menu-entries30,788
(defpgdefault menu-entries34,948
(defvar lego-shell-process-output45,1250
(defconst lego-process-config53,1573
(defconst lego-pretty-set-width 64,2004
(defconst lego-interrupt-regexp 68,2147
(defcustom lego-www-home-page 73,2264
(defcustom lego-www-latest-release78,2388
(defcustom lego-www-refcard84,2566
(defcustom lego-library-www-page90,2715
(defvar lego-prog-name 99,2931
(defvar lego-shell-prompt-pattern 102,3000
(defvar lego-shell-cd 105,3121
(defvar lego-shell-abort-goal-regexp 108,3221
(defvar lego-shell-proof-completed-regexp 113,3413
(defvar lego-save-command-regexp116,3553
(defvar lego-goal-command-regexp118,3643
(defvar lego-kill-goal-command 121,3734
(defvar lego-forget-id-command 122,3777
(defvar lego-undoable-commands-regexp124,3823
(defvar lego-goal-regexp 133,4197
(defvar lego-outline-regexp135,4242
(defvar lego-outline-heading-end-regexp 141,4418
(defvar lego-shell-outline-regexp 143,4471
(defvar lego-shell-outline-heading-end-regexp 144,4523
(define-derived-mode lego-shell-mode 150,4802
(define-derived-mode lego-mode 157,4963
(define-derived-mode lego-goals-mode 168,5260
(defun lego-count-undos 179,5686
(defun lego-goal-command-p 199,6505
(defun lego-find-and-forget 204,6676
(defun lego-goal-hyp 246,8512
(defun lego-state-preserving-p 255,8710
(defvar lego-shell-current-line-width 271,9413
(defun lego-shell-adjust-line-width 279,9720
(defun lego-mode-config 298,10459
(defun lego-equal-module-filename 366,12520
(defun lego-shell-compute-new-files-list 372,12795
(defun lego-shell-mode-config 386,13321
(defun lego-goals-mode-config 435,15257

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,359
(defconst lego-keywords-save 17,402
(defconst lego-commands19,473
(defconst lego-keywords31,1033
(defconst lego-tacticals 36,1210
(defconst lego-error-regexp 39,1318
(defvar lego-id 42,1477
(defvar lego-ids 44,1504
(defconst lego-arg-list-regexp 48,1700
(defun lego-decl-defn-regexp 51,1816
(defconst lego-definiendum-alternative-regexp59,2188
(defvar lego-font-lock-terms63,2372
(defconst lego-goal-with-hole-regexp89,3228
(defconst lego-save-with-hole-regexp94,3451
(defvar lego-font-lock-keywords-199,3668
(defun lego-init-syntax-table 110,4135

phox/phox.el,602
(defcustom phox-prog-name 31,917
(defcustom phox-sym-lock-enabled 36,1019
(defcustom phox-web-page42,1128
(defcustom phox-doc-dir 48,1278
(defcustom phox-lib-dir 54,1426
(defcustom phox-tags-program 60,1570
(defcustom phox-tags-doc 66,1750
(defcustom phox-etags 72,1888
(defpgdefault menu-entries93,2340
(defun phox-config 107,2533
(defun phox-shell-config 148,4424
(define-derived-mode phox-mode 173,5353
(define-derived-mode phox-shell-mode 189,5819
(define-derived-mode phox-response-mode 194,5947
(define-derived-mode phox-goals-mode 207,6389
(defpgdefault completion-table233,7273

phox/phox-extraction.el,382
(defvar phox-prog-orig 11,481
(defun phox-prog-flags-modify(13,549
(defun phox-prog-flags-extract(42,1353
(defun phox-prog-flags-erase(53,1644
(defun phox-toggle-extraction(61,1840
(defun phox-compile-theorem(73,2242
(defun phox-compile-theorem-on-cursor(79,2468
(defun phox-output 95,2947
(defun phox-output-theorem 105,3161
(defun phox-output-theorem-on-cursor(112,3461

phox/phox-font.el,123
(defconst phox-font-lock-keywords6,282
(defconst phox-sym-lock-keywords-table65,2401
(defun phox-sym-lock-start 88,2975

phox/phox-fun.el,679
(defun phox-init-syntax-table 67,2393
(defvar phox-top-keywords83,2866
(defvar phox-proof-keywords131,3321
(defun phox-find-and-forget 172,3671
(defun phox-assert-next-command-interactive 251,6096
(defun phox-depend-theorem(270,6927
(defun phox-eshow-extlist(279,7217
(defun phox-flag-name(293,7816
(defun phox-path(304,8119
(defun phox-print-expression(315,8356
(defun phox-print-sort-expression(328,8814
(defun phox-priority-symbols-list(339,9127
(defun phox-search-string(351,9500
(defun phox-constraints(366,10028
(defun phox-goals(377,10285
(defvar phox-state-menu389,10495
(defun phox-delete-symbol(414,11485
(defun phox-delete-symbol-on-cursor(420,11694

phox/phox-lang.el,283
(defvar phox-lang8,279
(defun phox-lang-absurd 17,496
(defun phox-lang-suppress 22,591
(defun phox-lang-opendef 27,790
(defun phox-lang-instance 32,909
(defun phox-lang-lock 37,1038
(defun phox-lang-unlock 42,1175
(defun phox-lang-prove 47,1318
(defun phox-lang-let 52,1455

phox/phox-outline.el,70
(defun phox-outline-level(32,1113
(defun phox-setup-outline 46,1587

phox/phox-pbrpm.el,512
(defun phox-pbrpm-left-paren-p 27,1189
(defun phox-pbrpm-right-paren-p 34,1392
(defun phox-pbrpm-menu-from-string 42,1596
(defun phox-pbrpm-rename-in-cmd 51,1930
(defun phox-pbrpm-get-region-name 84,3184
(defun  phox-pbrpm-escape-string 87,3311
(defun phox-pbrpm-generate-menu 91,3446
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
289,10635
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
290,10699
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
291,10761

phox/phox-sym-lock.el,1353
(defvar phox-sym-lock-sym-count 34,1598
(defvar phox-sym-lock-ext-start 37,1668
(defvar phox-sym-lock-ext-end 39,1790
(defvar phox-sym-lock-font-size 42,1909
(defvar phox-sym-lock-keywords 47,2099
(defvar phox-sym-lock-enabled 52,2275
(defvar phox-sym-lock-color 57,2437
(defvar phox-sym-lock-mouse-face 62,2655
(defvar phox-sym-lock-mouse-face-enabled 67,2845
(defconst phox-sym-lock-with-mule 72,3035
(defun phox-sym-lock-gen-symbol 75,3119
(defun phox-sym-lock-make-symbols-atomic 83,3422
(defun phox-sym-lock-compute-font-size 110,4364
(defvar phox-sym-lock-font-name148,5784
(defun phox-sym-lock-set-foreground 190,7270
(defun phox-sym-lock-translate-char 204,7879
(defun phox-sym-lock-translate-char-or-string 212,8147
(defun phox-sym-lock-remap-face 219,8374
(defvar phox-sym-lock-clear-face239,9364
(defun phox-sym-lock 251,9786
(defun phox-sym-lock-rec 260,10190
(defun phox-sym-lock-atom-face 266,10343
(defun phox-sym-lock-pre-idle-hook-first 271,10639
(defun phox-sym-lock-pre-idle-hook-last 279,10997
(defun phox-sym-lock-enable 288,11372
(defun phox-sym-lock-disable 301,11785
(defun phox-sym-lock-mouse-face-enable 314,12203
(defun phox-sym-lock-mouse-face-disable 321,12418
(defun phox-sym-lock-font-lock-hook 328,12637
(defun font-lock-set-defaults 343,13330
(defun phox-sym-lock-patch-keywords 354,13708

phox/phox-tags.el,305
(defun phox-tags-add-table(21,767
(defun phox-tags-reset-table(29,1096
(defun phox-tags-add-doc-table(34,1206
(defun phox-tags-add-lib-table(40,1355
(defun phox-tags-add-local-table(46,1491
(defun phox-tags-create-local-table(52,1674
(defun phox-complete-tag(63,1926
(defvar phox-tags-menu70,2035

plastic/plastic.el,2863
(defcustom plastic-tags 22,491
(defcustom plastic-test-all-name 27,623
(defvar plastic-lit-string 34,814
(defcustom plastic-help-menu-list38,928
(defvar plastic-shell-process-output52,1422
(defconst plastic-process-config 60,1748
(defconst plastic-pretty-set-width 67,1998
(defconst plastic-interrupt-regexp 71,2147
(defcustom plastic-www-home-page 77,2268
(defcustom plastic-www-latest-release82,2405
(defcustom plastic-www-refcard88,2578
(defcustom plastic-library-www-page94,2709
(defcustom plastic-base 104,2924
(defvar plastic-prog-name 112,3096
(defun plastic-set-default-env-vars 116,3204
(defvar plastic-shell-prompt-pattern 124,3442
(defvar plastic-shell-cd 127,3567
(defvar plastic-shell-abort-goal-regexp 131,3709
(defvar plastic-shell-proof-completed-regexp 135,3877
(defvar plastic-save-command-regexp138,4020
(defvar plastic-goal-command-regexp140,4116
(defvar plastic-kill-goal-command 143,4213
(defvar plastic-forget-id-command 145,4314
(defvar plastic-undoable-commands-regexp148,4395
(defvar plastic-goal-regexp 160,4842
(defvar plastic-outline-regexp162,4890
(defvar plastic-outline-heading-end-regexp 168,5069
(defvar plastic-shell-outline-regexp 170,5125
(defvar plastic-shell-outline-heading-end-regexp 171,5183
(defvar plastic-error-occurred 173,5254
(define-derived-mode plastic-shell-mode 182,5586
(define-derived-mode plastic-mode 188,5768
(define-derived-mode plastic-goals-mode 204,6288
(defun plastic-count-undos 213,6633
(defun plastic-goal-command-p 233,7509
(defun plastic-find-and-forget 238,7702
(defun plastic-goal-hyp 273,9050
(defun plastic-state-preserving-p 284,9300
(defvar plastic-shell-current-line-width 307,10276
(defun plastic-shell-adjust-line-width 315,10592
(defun plastic-mode-config 342,11687
(defun plastic-show-shell-buffer 431,14962
(defun plastic-equal-module-filename 437,15065
(defun plastic-shell-compute-new-files-list 443,15343
(defun plastic-shell-mode-config 459,15880
(defun plastic-goals-mode-config 510,18086
(defun plastic-small-bar 522,18380
(defun plastic-large-bar 524,18469
(defun plastic-preprocessing 526,18607
(defun plastic-all-ctxt 577,20435
(defun plastic-send-one-undo 584,20613
(defun plastic-minibuf-cmd 594,20941
(defun plastic-minibuf 606,21420
(defun plastic-synchro 613,21626
(defun plastic-send-minibuf 618,21767
(defun plastic-had-error 626,22096
(defun plastic-reset-error 630,22271
(defun plastic-call-if-no-error 633,22410
(defun plastic-show-shell 638,22614
(define-key plastic-keymap 647,22876
(define-key plastic-keymap 648,22937
(define-key plastic-keymap 649,22998
(define-key plastic-keymap 650,23058
(define-key plastic-keymap 651,23117
(define-key plastic-keymap 652,23176
(defalias 'proof-toolbar-command proof-toolbar-command
662,23426
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
663,23477

plastic/plastic-syntax.el,648
(defconst plastic-keywords-goal 18,537
(defconst plastic-keywords-save 20,583
(defconst plastic-commands22,657
(defconst plastic-keywords35,1267
(defconst plastic-tacticals 40,1450
(defconst plastic-error-regexp 43,1561
(defvar plastic-id 46,1695
(defvar plastic-ids 48,1725
(defconst plastic-arg-list-regexp 52,1933
(defun plastic-decl-defn-regexp 55,2052
(defconst plastic-definiendum-alternative-regexp63,2433
(defvar plastic-font-lock-terms67,2626
(defconst plastic-goal-with-hole-regexp89,3339
(defconst plastic-save-with-hole-regexp94,3566
(defvar plastic-font-lock-keywords-199,3792
(defun plastic-init-syntax-table 108,4184

twelf/twelf.el,463
(defcustom twelf-root-dir25,592
(defcustom twelf-info-dir31,750
(defun twelf-add-read-declaration 100,3260
(defun twelf-set-syntax 113,3595
(defun twelf-set-word 115,3692
(defun twelf-set-symbol 116,3754
(defun twelf-map-string 118,3818
(defun twelf-mode-extra-config 165,5880
(defconst twelf-syntax-menu171,6086
(defpacustom chatter 185,6453
(defpacustom double-check 190,6546
(defpacustom print-implicit 194,6683
(defpgdefault menu-entries206,6827

twelf/twelf-font.el,917
(defun twelf-font-create-face 31,837
(defvar twelf-font-dark-background 38,1095
(defvar twelf-font-patterns64,2453
(defun twelf-font-fontify-decl 105,4303
(defun twelf-font-fontify-buffer 115,4600
(defun twelf-font-unfontify 122,4859
(defvar font-lock-message-threshold 127,5033
(defun twelf-font-fontify-region 129,5111
(defun twelf-font-highlight 195,7611
(defun twelf-font-find-delimited-comment 204,8068
(defun twelf-font-find-decl 223,8748
(defun twelf-font-find-binder 239,9238
(defun twelf-font-find-parm 301,11095
(defun twelf-font-find-evar 308,11418
(defun twelf-current-decl 330,12160
(defun twelf-next-decl 357,13316
(defconst *whitespace* 382,14338
(defconst *twelf-comment-start* 385,14436
(defconst *twelf-id-chars* 388,14565
(defun skip-twelf-comments-and-whitespace 391,14683
(defun twelf-end-of-par 403,15157
(defun skip-ahead 426,15931
(defun current-line-absolute 438,16353

twelf/twelf-old.el,6958
(defvar twelf-indent 212,8772
(defvar twelf-infix-regexp 215,8832
(defvar twelf-server-program 219,9027
(defvar twelf-info-file 222,9108
(defvar twelf-server-display-commands 225,9181
(defvar twelf-highlight-range-function 230,9429
(defvar twelf-focus-function 235,9712
(defvar twelf-server-echo-commands 241,9992
(defvar twelf-save-silently 244,10113
(defvar twelf-server-timeout 248,10285
(defvar twelf-sml-program 252,10432
(defvar twelf-sml-args 255,10504
(defvar twelf-sml-display-queries 258,10570
(defvar twelf-mode-hook 261,10678
(defvar twelf-server-mode-hook 264,10772
(defvar twelf-config-mode-hook 267,10880
(defvar twelf-sml-mode-hook 270,10994
(defvar twelf-to-twelf-sml-mode 273,11075
(defvar twelf-config-mode 276,11167
(defvar *twelf-server-buffer-name* 283,11431
(defvar *twelf-server-buffer* 286,11535
(defvar *twelf-server-process-name* 289,11623
(defvar *twelf-config-buffer* 292,11714
(defvar *twelf-config-time* 295,11808
(defvar *twelf-config-list* 298,11921
(defvar *twelf-server-last-process-mark* 301,12033
(defvar *twelf-last-region-sent* 304,12151
(defvar *twelf-last-input-buffer* 311,12475
(defvar *twelf-error-pos* 315,12598
(defconst *twelf-read-functions*318,12674
(defconst *twelf-parm-table*325,12912
(defvar twelf-chatter 338,13288
(defvar twelf-double-check 346,13505
(defvar twelf-print-implicit 349,13592
(defconst *twelf-track-parms*352,13684
(defun install-basic-twelf-keybindings 363,14108
(defun install-twelf-keybindings 388,15077
(defvar twelf-mode-map 404,15842
(defvar twelf-mode-syntax-table 416,16278
(defun set-twelf-syntax 419,16357
(defun set-word 421,16454
(defun set-symbol 422,16509
(defun map-string 424,16567
(defconst *whitespace* 456,18044
(defconst *twelf-comment-start* 459,18142
(defconst *twelf-id-chars* 462,18271
(defun skip-twelf-comments-and-whitespace 465,18389
(defun twelf-end-of-par 477,18863
(defun twelf-current-decl 500,19637
(defun twelf-mark-decl 527,20793
(defun twelf-indent-decl 536,21059
(defun twelf-indent-region 545,21345
(defun twelf-indent-lines 556,21669
(defun twelf-comment-indent 564,21842
(defun looked-at 575,22198
(defun twelf-indent-line 580,22370
(defun twelf-indent-line-to 613,24113
(defun twelf-calculate-indent 626,24568
(defun twelf-dsb 641,25192
(defun twelf-mode-variables 667,26604
(defun twelf-mode 689,27417
(defun twelf-info 904,35799
(defconst twelf-error-regexp918,36339
(defconst twelf-error-fields-regexp922,36450
(defconst twelf-error-decl-regexp928,36663
(defun looked-at-nth 932,36812
(defun looked-at-nth-int 938,36994
(defun twelf-error-parser 943,37112
(defun twelf-error-decl 957,37715
(defun twelf-mark-relative 963,37894
(defun twelf-mark-absolute 979,38564
(defun twelf-find-decl 1004,39450
(defun twelf-next-error 1019,40006
(defun twelf-goto-error 1087,42816
(defun twelf-convert-standard-filename 1101,43354
(defun string-member 1113,43849
(defun twelf-config-proceed-p 1125,44341
(defun twelf-save-if-config 1132,44603
(defun twelf-config-save-some-buffers 1145,45075
(defun twelf-save-check-config 1149,45240
(defun twelf-check-config 1164,45796
(defun twelf-save-check-file 1176,46236
(defun twelf-buffer-substring 1192,46959
(defun twelf-buffer-substring-dot 1198,47221
(defun twelf-check-declaration 1204,47487
(defun twelf-highlight-range-zmacs 1227,48547
(defun twelf-focus 1233,48797
(defun twelf-focus-noop 1239,49063
(defun twelf-type-const 1322,52685
(defvar twelf-server-mode-map 1439,57827
(defconst twelf-server-cd-regexp 1451,58379
(defun looked-at-string 1454,58519
(defun twelf-server-directory-tracker 1458,58660
(defun twelf-input-filter 1480,59840
(defun twelf-server-mode 1486,60095
(defun twelf-parse-config 1519,61312
(defun twelf-server-read-config 1537,62204
(defun twelf-server-sync-config 1546,62541
(defun twelf-get-server-buffer 1576,64047
(defun twelf-init-variables 1593,64721
(defun twelf-server 1600,64934
(defun twelf-server-process 1642,66848
(defun twelf-server-display 1651,67254
(defun display-server-buffer 1658,67528
(defun twelf-server-send-command 1673,68260
(defun twelf-accept-process-output 1694,69220
(defun twelf-server-wait 1703,69659
(defun twelf-server-quit 1745,71797
(defun twelf-server-interrupt 1750,71918
(defun twelf-reset 1755,72054
(defun twelf-config-directory 1760,72198
(defun twelf-server-configure 1771,72612
(defun natp 1844,75904
(defun twelf-read-nat 1848,76005
(defun twelf-read-bool 1857,76272
(defun twelf-read-limit 1863,76420
(defun twelf-read-strategy 1873,76723
(defun twelf-read-value 1879,76875
(defun twelf-set 1883,77038
(defun twelf-set-parm 1896,77515
(defun track-parm 1905,77812
(defun twelf-toggle-double-check 1910,77986
(defun twelf-toggle-print-implicit 1916,78189
(defun twelf-get 1922,78402
(defun twelf-timers-reset 1936,79028
(defun twelf-timers-show 1941,79148
(defun twelf-timers-check 1947,79299
(defun twelf-server-restart 1953,79464
(defun twelf-config-mode 1969,80141
(defun twelf-config-mode-check 1985,80740
(defun twelf-tag 1994,81190
(defun twelf-tag-files 2022,82454
(default: *tags-errors*)2026,82757
(defun twelf-tag-file 2047,83508
(defun twelf-next-decl 2082,84730
(defun skip-ahead 2107,85752
(defun current-line-absolute 2119,86174
(defun new-temp-buffer 2124,86384
(defun rev-relativize 2135,86768
(defvar twelf-sml-mode-map 2149,87228
(defconst twelf-sml-prompt-regexp 2159,87606
(defun expand-dir 2161,87661
(defun twelf-sml-cd 2168,87922
(defconst twelf-sml-cd-regexp 2180,88411
(defun twelf-sml-directory-tracker 2183,88545
(defun twelf-sml-mode 2199,89390
(defun twelf-sml 2250,91324
(defun switch-to-twelf-sml 2270,92284
(defun display-twelf-sml-buffer 2281,92633
(defun twelf-sml-send-string 2297,93349
(defun twelf-sml-send-region 2302,93553
(defun twelf-sml-send-query 2326,94759
(defun twelf-sml-send-newline 2336,95156
(defun twelf-sml-send-semicolon 2344,95484
(defun twelf-sml-status 2352,95818
(defvar twelf-sml-init 2374,96765
(defun twelf-sml-set-mode 2377,96942
(defun twelf-sml-quit 2403,98119
(defun twelf-sml-process-buffer 2408,98231
(defun twelf-sml-process 2412,98347
(defvar twelf-to-twelf-sml-mode 2424,98863
(defun install-twelf-to-twelf-sml-keybindings 2427,98948
(defvar twelf-to-twelf-sml-mode-map 2437,99333
(defun twelf-to-twelf-sml-mode 2448,99846
(defconst twelf-at-point-menu2498,101713
(defconst twelf-server-state-menu2508,102085
(defconst twelf-error-menu2518,102402
(defconst twelf-tags-menu2524,102546
(defun twelf-toggle-server-display-commands 2534,102831
(defconst twelf-options-menu2537,102955
(defconst twelf-timers-menu2572,104693
(defconst twelf-syntax-menu2585,105187
(defun twelf-add-menu 2612,106053
(defun twelf-remove-menu 2616,106155
(defun twelf-reset-menu 2620,106253
(defun twelf-server-add-menu 2647,107152
(defun twelf-server-remove-menu 2651,107275
(defun twelf-server-reset-menu 2655,107387

generic/pg-assoc.el,82
(defun proof-associated-buffers 36,1066
(defun proof-associated-windows 46,1278

generic/pg-autotest.el,442
(defvar pg-autotest-success 24,544
(defun pg-autotest-find-file 28,628
(defun pg-autotest-find-file-restart 35,908
(defmacro pg-autotest 48,1356
(defun pg-autotest-script-wholefile 62,1703
(defun pg-autotest-retract-file 79,2316
(defun pg-autotest-assert-processed 85,2452
(defun pg-autotest-assert-unprocessed 92,2706
(defun pg-autotest-message 99,2966
(defun pg-autotest-quit-prover 106,3159
(defun pg-autotest-finished 112,3340

generic/pg-custom.el,554
(defpgcustom maths-menu-enable 36,1137
(defpgcustom unicode-tokens-enable 42,1317
(defpgcustom mmm-enable 48,1494
(defpgcustom script-indent 57,1848
(defconst proof-toolbar-entries-default62,1985
(defpgcustom toolbar-entries 90,3757
(defpgcustom prog-args 109,4490
(defpgcustom prog-env 122,5065
(defpgcustom favourites 131,5491
(defpgcustom menu-entries 136,5680
(defpgcustom help-menu-entries 143,5916
(defpgcustom keymap 150,6179
(defpgcustom completion-table 155,6351
(defpgcustom tags-program 166,6725
(defpgcustom use-holes 175,7109

generic/pg-goals.el,285
(define-derived-mode proof-goals-mode 30,654
(define-key proof-goals-mode-map 58,1529
(define-key proof-goals-mode-map 60,1645
(define-key proof-goals-mode-map 61,1713
(defun proof-goals-config-done 70,1859
(defun pg-goals-display 78,2125
(defun pg-goals-button-action 117,3449

generic/pg-pbrpm.el,1803
(defvar pg-pbrpm-use-buffer-menu 22,548
(defvar pg-pbrpm-start-goal-regexp 25,670
(defvar pg-pbrpm-start-goal-regexp-par-num 29,827
(defvar pg-pbrpm-end-goal-regexp 32,950
(defvar pg-pbrpm-start-hyp-regexp 36,1102
(defvar pg-pbrpm-start-hyp-regexp-par-num 40,1263
(defvar pg-pbrpm-start-concl-regexp 44,1470
(defvar pg-pbrpm-auto-select-regexp 48,1634
(defvar pg-pbrpm-buffer-menu 55,1795
(defvar pg-pbrpm-spans 56,1829
(defvar pg-pbrpm-goal-description 57,1857
(defvar pg-pbrpm-windows-dialog-bug 58,1896
(defvar pbrpm-menu-desc 59,1937
(defun pg-pbrpm-erase-buffer-menu 61,1967
(defun pg-pbrpm-menu-change-hook 68,2151
(defun pg-pbrpm-create-reset-buffer-menu 86,2727
(defun pg-pbrpm-analyse-goal-buffer 101,3356
(defun pg-pbrpm-button-action 161,5766
(defun pg-pbrpm-exists 168,5992
(defun pg-pbrpm-eliminate-id 172,6104
(defun pg-pbrpm-build-menu 180,6350
(defun pg-pbrpm-setup-span 243,8676
(defun pg-pbrpm-run-command 303,10994
(defun pg-pbrpm-get-pos-info 332,12304
(defun pg-pbrpm-get-region-info 374,13611
(defun pg-pbrpm-auto-select-around-point 385,14025
(defun pg-pbrpm-translate-position 400,14555
(defun pg-pbrpm-process-click 408,14813
(defvar pg-pbrpm-remember-region-selected-region 428,15838
(defvar pg-pbrpm-regions-list 429,15892
(defun pg-pbrpm-erase-regions-list 431,15928
(defun pg-pbrpm-filter-regions-list 440,16236
(defface pg-pbrpm-multiple-selection-face447,16499
(defface pg-pbrpm-menu-input-face455,16701
(defun pg-pbrpm-do-remember-region 463,16891
(defun pg-pbrpm-remember-region-drag-up-hook 484,17739
(defun pg-pbrpm-remember-region-click-hook 488,17910
(defun pg-pbrpm-remember-region 493,18095
(defun pg-pbrpm-process-region 507,18810
(defun pg-pbrpm-process-regions-list 525,19539
(defun pg-pbrpm-region-expression 529,19722

generic/pg-pgip.el,2889
(defalias 'pg-pgip-debug pg-pgip-debug
35,920
(defalias 'pg-pgip-error pg-pgip-error
36,961
(defalias 'pg-pgip-warning pg-pgip-warning
37,996
(defconst pg-pgip-version-supported 39,1046
(defun pg-pgip-process-packet 43,1152
(defvar pg-pgip-last-seen-id 53,1720
(defvar pg-pgip-last-seen-seq 54,1754
(defun pg-pgip-process-pgip 56,1790
(defun pg-pgip-process-msg 75,2721
(defvar pg-pgip-post-process-functions89,3291
(defun pg-pgip-post-process 99,3779
(defun pg-pgip-process-askpgip 115,4390
(defun pg-pgip-process-usespgip 121,4595
(defun pg-pgip-process-usespgml 125,4759
(defun pg-pgip-process-pgmlconfig 129,4923
(defun pg-pgip-process-proverinfo 145,5540
(defun pg-pgip-process-hasprefs 162,6205
(defun pg-pgip-haspref 176,6837
(defun pg-pgip-process-prefval 193,7539
(defun pg-pgip-process-guiconfig 220,8248
(defvar proof-assistant-idtables 227,8365
(defun pg-pgip-process-ids 230,8482
(defun pg-complete-idtable-symbol 256,9554
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
261,9646
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
262,9702
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
263,9758
(defun pg-pgip-process-idvalue 266,9816
(defun pg-pgip-process-menuadd 278,10152
(defun pg-pgip-process-menudel 281,10195
(defun pg-pgip-process-ready 290,10428
(defun pg-pgip-process-cleardisplay 293,10469
(defun pg-pgip-process-proofstate 307,10926
(defun pg-pgip-process-normalresponse 311,11003
(defun pg-pgip-process-errorresponse 315,11127
(defun pg-pgip-process-scriptinsert 319,11250
(defun pg-pgip-process-metainforesponse 324,11384
(defun pg-pgip-process-informfileloaded 333,11625
(defun pg-pgip-process-informfileretracted 339,11891
(defun pg-pgip-process-brokerstatus 352,12368
(defun pg-pgip-process-proveravailmsg 355,12416
(defun pg-pgip-process-newprovermsg 358,12466
(defun pg-pgip-process-proverstatusmsg 361,12514
(defvar pg-pgip-srcids 370,12761
(defun pg-pgip-process-newfile 374,12868
(defun pg-pgip-process-filestatus 390,13456
(defun pg-pgip-process-newobj 410,14111
(defun pg-pgip-process-delobj 413,14153
(defun pg-pgip-process-objectstatus 416,14195
(defun pg-pgip-process-parsescript 430,14550
(defun pg-pgip-get-pgiptype 453,15425
(defun pg-pgip-default-for 473,16218
(defun pg-pgip-subst-for 486,16613
(defun pg-pgip-interpret-value 498,16956
(defun pg-pgip-interpret-choice 516,17641
(defun pg-pgip-string-of-command 547,18658
(defconst pg-pgip-id564,19419
(defvar pg-pgip-refseq 570,19699
(defvar pg-pgip-refid 572,19796
(defvar pg-pgip-seq 575,19888
(defun pg-pgip-assemble-packet 577,19952
(defun pg-pgip-issue 595,20764
(defun pg-pgip-maybe-askpgip 612,21376
(defun pg-pgip-askprefs 618,21567
(defun pg-pgip-askids 622,21681
(defun pg-pgip-reset 635,21969
(defconst pg-pgip-start-element-regexp 666,22667
(defconst pg-pgip-end-element-regexp 667,22719

generic/pg-response.el,1214
(deflocal pg-response-eagerly-raise 31,731
(define-derived-mode proof-response-mode 41,956
(define-key proof-response-mode-map 68,1882
(define-key proof-response-mode-map 69,1953
(define-key proof-response-mode-map 70,2007
(defun proof-response-config-done 74,2093
(defvar pg-response-special-display-regexp 85,2440
(defconst proof-multiframe-parameters89,2607
(defun proof-multiple-frames-enable 98,2906
(defun proof-three-window-enable 108,3235
(defun proof-select-three-b 111,3298
(defun proof-display-three-b 126,3767
(defvar pg-frame-configuration 138,4176
(defun pg-cache-frame-configuration 142,4323
(defun proof-layout-windows 146,4494
(defun proof-delete-other-frames 186,6281
(defvar pg-response-erase-flag 217,7371
(defun pg-response-maybe-erase221,7500
(defun pg-response-display 252,8685
(defun pg-response-display-with-face 277,9472
(defun pg-response-clear-displays 307,10398
(defun proof-next-error 326,10985
(defun pg-response-has-error-location 407,13901
(defvar proof-trace-last-fontify-pos 430,14734
(defun proof-trace-fontify-pos 432,14777
(defun proof-trace-buffer-display 440,15090
(defun proof-trace-buffer-finish 465,16036
(defun pg-thms-buffer-clear 487,16607

generic/pg-thymodes.el,152
(defmacro pg-defthymode 23,500
(defmacro pg-do-unless-null 71,2311
(defun pg-symval 76,2398
(defun pg-modesym 82,2553
(defun pg-modesymval 86,2667

generic/pg-user.el,3221
(defun proof-maybe-follow-locked-end 32,793
(defun proof-assert-next-command-interactive 53,1412
(defun proof-process-buffer 63,1777
(defun proof-undo-last-successful-command 77,2088
(defun proof-undo-and-delete-last-successful-command 82,2250
(defun proof-undo-last-successful-command-1 96,2813
(defun proof-retract-buffer 113,3426
(defun proof-retract-current-goal 122,3710
(defun proof-goto-command-start 141,4271
(defun proof-goto-command-end 164,5211
(defun proof-mouse-goto-point 181,5592
(defvar proof-minibuffer-history 196,5870
(defun proof-minibuffer-cmd 199,5965
(defun proof-frob-locked-end 243,7580
(defmacro proof-if-setting-configured 304,9508
(defmacro proof-define-assistant-command 312,9777
(defmacro proof-define-assistant-command-witharg 325,10232
(defun proof-issue-new-command 345,11055
(defun proof-cd-sync 389,12498
(defun proof-electric-terminator-enable 443,14218
(defun proof-electric-term-incomment-fn 451,14520
(defun proof-process-electric-terminator 471,15307
(defun proof-electric-terminator 496,16372
(defun proof-add-completions 518,17018
(defun proof-script-complete 542,17878
(defun pg-insert-last-output-as-comment 556,18264
(defun pg-copy-span-contents 570,18662
(defun pg-numth-span-higher-or-lower 587,19220
(defun pg-control-span-of 613,19966
(defun pg-move-span-contents 619,20170
(defun pg-fixup-children-spans 671,22346
(defun pg-move-region-down 681,22609
(defun pg-move-region-up 690,22902
(defun proof-forward-command 720,23740
(defun proof-backward-command 741,24461
(defun pg-pos-for-event 763,24812
(defun pg-span-for-event 769,25033
(defun pg-span-context-menu 773,25177
(defun pg-toggle-visibility 788,25632
(defun pg-create-in-span-context-menu 798,25954
(defun pg-span-undo 828,27163
(defun pg-goals-buffers-hint 874,28573
(defun pg-slow-fontify-tracing-hint 878,28755
(defun pg-response-buffers-hint 882,28926
(defun pg-jump-to-end-hint 892,29288
(defun pg-processing-complete-hint 896,29419
(defun pg-next-error-hint 913,30118
(defun pg-hint 918,30270
(defun pg-identifier-under-mouse-query 934,30860
(defun pg-identifier-near-point-query 943,31103
(defvar proof-query-identifier-collection 968,31835
(defvar proof-query-identifier-history 969,31882
(defun proof-query-identifier 971,31927
(defun pg-identifier-query 981,32197
(defun proof-imenu-enable 1012,33275
(defvar pg-input-ring 1043,34321
(defvar pg-input-ring-index 1046,34378
(defvar pg-stored-incomplete-input 1049,34450
(defun pg-previous-input 1052,34553
(defun pg-next-input 1066,35010
(defun pg-delete-input 1071,35132
(defun pg-get-old-input 1084,35470
(defun pg-restore-input 1098,35861
(defun pg-search-start 1109,36151
(defun pg-regexp-arg 1121,36643
(defun pg-search-arg 1133,37091
(defun pg-previous-matching-input-string-position 1147,37508
(defun pg-previous-matching-input 1174,38673
(defun pg-next-matching-input 1193,39523
(defvar pg-matching-input-from-input-string 1201,39906
(defun pg-previous-matching-input-from-input 1205,40020
(defun pg-next-matching-input-from-input 1223,40785
(defun pg-add-to-input-history 1234,41164
(defun pg-remove-from-input-history 1246,41617
(defun  pg-clear-input-ring 1257,41999

generic/pg-vars.el,1326
(defvar proof-assistant-cusgrp 22,383
(defvar proof-assistant-internals-cusgrp 28,645
(defvar proof-assistant 34,916
(defvar proof-assistant-symbol 39,1138
(defvar proof-mode-for-shell 52,1682
(defvar proof-mode-for-response 57,1874
(defvar proof-mode-for-goals 62,2101
(defvar proof-mode-for-script 67,2291
(defvar proof-ready-for-assistant-hook 72,2469
(defvar proof-shell-busy 83,2758
(defvar proof-included-files-list 88,2914
(defvar proof-script-buffer 110,3927
(defvar proof-previous-script-buffer 113,4019
(defvar proof-shell-buffer 117,4190
(defvar proof-goals-buffer 120,4276
(defvar proof-response-buffer 123,4331
(defvar proof-trace-buffer 126,4392
(defvar proof-thms-buffer 130,4546
(defvar proof-shell-error-or-interrupt-seen 134,4701
(defvar proof-shell-interrupt-pending 139,4925
(defvar pg-response-next-error 143,5091
(defvar proof-shell-proof-completed 146,5198
(defvar proof-terminal-string 158,5742
(defvar proof-shell-last-output 169,5934
(defvar proof-assistant-settings 173,6075
(defvar pg-tracing-slow-mode 181,6524
(defvar proof-nesting-depth 184,6613
(defvar proof-last-theorem-dependencies 191,6848
(defcustom proof-general-name 200,7084
(defcustom proof-general-home-page205,7241
(defcustom proof-unnamed-theorem-name211,7401
(defcustom proof-universal-keys217,7585

generic/pg-xml.el,1140
(defalias 'pg-xml-error pg-xml-error
16,366
(defun pg-xml-parse-string 39,1008
(defun pg-xml-parse-buffer 50,1334
(defun pg-xml-get-attr 72,2067
(defun pg-xml-child-elts 80,2369
(defun pg-xml-child-elt 85,2574
(defun pg-xml-get-child 93,2856
(defun pg-xml-get-text-content 103,3228
(defmacro pg-xml-attr 114,3578
(defmacro pg-xml-node 116,3640
(defconst pg-xml-header119,3732
(defun pg-xml-string-of 123,3808
(defun pg-xml-output-internal 134,4175
(defun pg-xml-cdata 168,5325
(defun pg-pgip-get-icon 176,5518
(defsubst pg-pgip-get-name 180,5666
(defsubst pg-pgip-get-version 183,5783
(defsubst pg-pgip-get-descr 186,5906
(defsubst pg-pgip-get-thmname 189,6025
(defsubst pg-pgip-get-thyname 192,6148
(defsubst pg-pgip-get-url 195,6271
(defsubst pg-pgip-get-srcid 198,6386
(defsubst pg-pgip-get-proverid 201,6505
(defsubst pg-pgip-get-symname 204,6630
(defsubst pg-pgip-get-prefcat 207,6750
(defsubst pg-pgip-get-default 210,6878
(defsubst pg-pgip-get-objtype 213,7001
(defsubst pg-pgip-get-value 216,7124
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
219,7194
(defun pg-pgip-get-pgmltext 221,7253

generic/proof-auxmodes.el,149
(defun proof-mmm-support-available 21,550
(defun proof-maths-menu-support-available 45,1168
(defun proof-unicode-tokens-support-available 59,1586

generic/proof-config.el,7974
(defgroup prover-config 79,2604
(defcustom proof-guess-command-line 99,3456
(defcustom proof-assistant-home-page 114,3951
(defcustom proof-context-command 120,4121
(defcustom proof-info-command 125,4255
(defcustom proof-showproof-command 132,4526
(defcustom proof-goal-command 137,4662
(defcustom proof-save-command 145,4959
(defcustom proof-find-theorems-command 153,5268
(defcustom proof-query-identifier-command 160,5576
(defcustom proof-assistant-true-value 174,6265
(defcustom proof-assistant-false-value 180,6455
(defcustom proof-assistant-format-int-fn 186,6649
(defcustom proof-assistant-format-string-fn 193,6898
(defcustom proof-assistant-setting-format 200,7165
(defgroup proof-script 222,7860
(defcustom proof-terminal-char 227,7990
(defcustom proof-electric-terminator-noterminator 237,8377
(defcustom proof-script-sexp-commands 242,8549
(defcustom proof-script-command-end-regexp 253,9006
(defcustom proof-script-command-start-regexp 271,9825
(defcustom proof-script-use-old-parser 282,10286
(defcustom proof-script-integral-proofs 294,10772
(defcustom proof-script-fly-past-comments 309,11428
(defcustom proof-script-parse-function 314,11599
(defcustom proof-script-comment-start 332,12242
(defcustom proof-script-comment-start-regexp 343,12679
(defcustom proof-script-comment-end 351,12998
(defcustom proof-script-comment-end-regexp 363,13420
(defcustom proof-string-start-regexp 371,13731
(defcustom proof-string-end-regexp 376,13896
(defcustom proof-case-fold-search 381,14057
(defcustom proof-save-command-regexp 390,14469
(defcustom proof-save-with-hole-regexp 395,14579
(defcustom proof-save-with-hole-result 407,15033
(defcustom proof-goal-command-regexp 417,15481
(defcustom proof-goal-with-hole-regexp 426,15869
(defcustom proof-goal-with-hole-result 438,16312
(defcustom proof-non-undoables-regexp 447,16696
(defcustom proof-nested-undo-regexp 458,17151
(defcustom proof-ignore-for-undo-count 474,17863
(defcustom proof-script-next-entity-regexps 482,18166
(defcustom proof-script-find-next-entity-fn526,19907
(defcustom proof-script-imenu-generic-expression 546,20747
(defcustom proof-goal-command-p 554,21086
(defcustom proof-really-save-command-p 565,21577
(defcustom proof-completed-proof-behaviour 574,21884
(defcustom proof-count-undos-fn 602,23240
(defconst proof-no-command 614,23789
(defcustom proof-find-and-forget-fn 619,23996
(defcustom proof-forget-id-command 636,24710
(defcustom pg-topterm-goalhyplit-fn 646,25068
(defcustom proof-kill-goal-command 658,25603
(defcustom proof-undo-n-times-cmd 672,26106
(defcustom proof-nested-goals-history-p 686,26654
(defcustom proof-state-preserving-p 695,26991
(defcustom proof-activate-scripting-hook 705,27463
(defcustom proof-deactivate-scripting-hook 724,28244
(defcustom proof-indent 737,28609
(defcustom proof-indent-hang 742,28716
(defcustom proof-indent-enclose-offset 747,28842
(defcustom proof-indent-open-offset 752,28984
(defcustom proof-indent-close-offset 757,29121
(defcustom proof-indent-any-regexp 762,29259
(defcustom proof-indent-inner-regexp 767,29419
(defcustom proof-indent-enclose-regexp 772,29573
(defcustom proof-indent-open-regexp 777,29727
(defcustom proof-indent-close-regexp 782,29879
(defcustom proof-script-font-lock-keywords 788,30033
(defcustom proof-script-syntax-table-entries 796,30385
(defcustom proof-script-span-context-menu-extensions 814,30782
(defgroup proof-shell 840,31542
(defcustom proof-prog-name 850,31713
(defcustom proof-shell-auto-terminate-commands 861,32133
(defcustom proof-shell-pre-sync-init-cmd 870,32534
(defcustom proof-shell-init-cmd 884,33092
(defcustom proof-shell-init-hook 896,33621
(defcustom proof-shell-restart-cmd 901,33760
(defcustom proof-shell-quit-cmd 906,33915
(defcustom proof-shell-quit-timeout 911,34082
(defcustom proof-shell-cd-cmd 921,34532
(defcustom proof-shell-start-silent-cmd 938,35203
(defcustom proof-shell-stop-silent-cmd 947,35579
(defcustom proof-shell-silent-threshold 956,35914
(defcustom  proof-shell-inform-file-processed-cmd 964,36248
(defcustom  proof-shell-inform-file-retracted-cmd 985,37176
(defcustom proof-auto-multiple-files 1013,38448
(defcustom proof-cannot-reopen-processed-files 1028,39169
(defcustom proof-shell-require-command-regexp 1042,39835
(defcustom proof-done-advancing-require-function 1053,40297
(defcustom proof-shell-quiet-errors 1059,40532
(defcustom proof-shell-prompt-pattern 1072,40866
(defcustom proof-shell-wakeup-char 1082,41287
(defcustom proof-shell-annotated-prompt-regexp 1088,41518
(defcustom proof-shell-abort-goal-regexp 1104,42154
(defcustom proof-shell-error-regexp 1109,42289
(defcustom proof-shell-truncate-before-error 1129,43089
(defcustom pg-next-error-regexp 1143,43628
(defcustom pg-next-error-filename-regexp 1158,44237
(defcustom pg-next-error-extract-filename 1182,45270
(defcustom proof-shell-interrupt-regexp 1189,45513
(defcustom proof-shell-proof-completed-regexp 1203,46108
(defcustom proof-shell-clear-response-regexp 1216,46616
(defcustom proof-shell-clear-goals-regexp 1223,46915
(defcustom proof-shell-start-goals-regexp 1230,47208
(defcustom proof-shell-end-goals-regexp 1238,47575
(defcustom proof-shell-eager-annotation-start 1244,47819
(defcustom proof-shell-eager-annotation-start-length 1267,48838
(defcustom proof-shell-eager-annotation-end 1278,49264
(defcustom proof-shell-strip-output-markup 1294,49939
(defcustom proof-shell-assumption-regexp 1303,50325
(defcustom proof-shell-process-file 1313,50729
(defcustom proof-shell-retract-files-regexp 1335,51685
(defcustom proof-shell-compute-new-files-list 1344,52021
(defcustom pg-use-specials-for-fontify 1356,52569
(defcustom pg-special-char-regexp 1364,52917
(defcustom proof-shell-set-elisp-variable-regexp 1370,53062
(defcustom proof-shell-match-pgip-cmd 1403,54575
(defcustom proof-shell-issue-pgip-cmd 1412,54904
(defcustom proof-use-pgip-askprefs 1417,55069
(defcustom proof-shell-query-dependencies-cmd 1425,55416
(defcustom proof-shell-theorem-dependency-list-regexp 1432,55676
(defcustom proof-shell-theorem-dependency-list-split 1448,56336
(defcustom proof-shell-show-dependency-cmd 1457,56759
(defcustom proof-shell-trace-output-regexp 1479,57665
(defcustom proof-shell-thms-output-regexp 1493,58123
(defcustom proof-tokens-activate-command 1506,58506
(defcustom proof-tokens-deactivate-command 1513,58747
(defcustom proof-tokens-extra-modes 1520,58994
(defcustom proof-shell-unicode 1535,59501
(defcustom proof-shell-filename-escapes 1543,59821
(defcustom proof-shell-process-connection-type1560,60501
(defcustom proof-shell-strip-crs-from-input 1583,61547
(defcustom proof-shell-strip-crs-from-output 1595,62032
(defcustom proof-shell-insert-hook 1603,62400
(defcustom proof-shell-handle-delayed-output-hook1641,64260
(defcustom proof-shell-handle-error-or-interrupt-hook1647,64475
(defcustom proof-shell-pre-interrupt-hook1665,65228
(defcustom proof-shell-classify-output-system-specific 1673,65499
(defcustom proof-state-change-hook 1692,66367
(defcustom proof-shell-syntax-table-entries 1702,66748
(defgroup proof-goals 1720,67120
(defcustom pg-subterm-first-special-char 1725,67241
(defcustom pg-subterm-anns-use-stack 1733,67553
(defcustom pg-goals-change-goal 1742,67852
(defcustom pbp-goal-command 1747,67968
(defcustom pbp-hyp-command 1752,68124
(defcustom pg-subterm-help-cmd 1757,68286
(defcustom pg-goals-error-regexp 1764,68522
(defcustom proof-shell-result-start 1769,68682
(defcustom proof-shell-result-end 1775,68916
(defcustom pg-subterm-start-char 1781,69129
(defcustom pg-subterm-sep-char 1795,69715
(defcustom pg-subterm-end-char 1801,69894
(defcustom pg-topterm-regexp 1807,70051
(defcustom proof-goals-font-lock-keywords 1822,70651
(defcustom proof-response-font-lock-keywords 1830,71010
(defcustom pg-before-fontify-output-hook 1838,71372
(defcustom pg-after-fontify-output-hook 1846,71733

generic/proof-depends.el,824
(defvar proof-thm-names-of-files 23,625
(defvar proof-def-names-of-files 29,909
(defun proof-depends-module-name-for-buffer 38,1213
(defun proof-depends-module-of 48,1655
(defun proof-depends-names-in-same-file 56,1949
(defun proof-depends-process-dependencies 75,2569
(defun proof-dependency-in-span-context-menu 128,4318
(defun proof-dep-alldeps-menu 151,5221
(defun proof-dep-make-alldeps-menu 157,5448
(defun proof-dep-split-deps 175,5944
(defun proof-dep-make-submenu 196,6643
(defun proof-make-highlight-depts-menu 206,6996
(defun proof-goto-dependency 216,7300
(defun proof-show-dependency 222,7523
(defconst pg-dep-span-priority 229,7813
(defconst pg-ordinary-span-priority 230,7849
(defun proof-highlight-depcs 232,7891
(defun proof-highlight-depts 242,8321
(defun proof-dep-unhighlight 253,8795

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table16,544
(defun proof-easy-config-define-derived-modes 23,950
(defun proof-easy-config-check-setup 52,2133
(defmacro proof-easy-config 84,3468

generic/proof-faces.el,1344
(defgroup proof-faces 28,748
(defconst pg-defface-window-systems35,930
(defmacro proof-face-specs 48,1492
(defface proof-queue-face63,1944
(defface proof-locked-face71,2222
(defface proof-declaration-name-face81,2543
(defface proof-tacticals-name-face90,2829
(defface proof-tactics-name-face99,3091
(defface proof-error-face108,3356
(defface proof-warning-face116,3546
(defface proof-eager-annotation-face125,3803
(defface proof-debug-message-face133,4021
(defface proof-boring-face141,4220
(defface proof-mouse-highlight-face149,4412
(defface proof-highlight-dependent-face157,4608
(defface proof-highlight-dependency-face165,4817
(defface proof-active-area-face173,5014
(defconst proof-face-compat-doc 184,5406
(defconst proof-queue-face 185,5486
(defconst proof-locked-face 186,5554
(defconst proof-declaration-name-face 187,5624
(defconst proof-tacticals-name-face 188,5714
(defconst proof-tactics-name-face 189,5800
(defconst proof-error-face 190,5882
(defconst proof-warning-face 191,5950
(defconst proof-eager-annotation-face 192,6022
(defconst proof-debug-message-face 193,6112
(defconst proof-boring-face 194,6196
(defconst proof-mouse-highlight-face 195,6266
(defconst proof-highlight-dependent-face 196,6354
(defconst proof-highlight-dependency-face 197,6450
(defconst proof-active-area-face 198,6548

generic/proof-indent.el,219
(defun proof-indent-indent 14,412
(defun proof-indent-offset 23,678
(defun proof-indent-inner-p 40,1278
(defun proof-indent-goto-prev 49,1585
(defun proof-indent-calculate 56,1918
(defun proof-indent-line 76,2640

generic/proof-maths-menu.el,83
(defun proof-maths-menu-set-global 30,959
(defun proof-maths-menu-enable 44,1415

generic/proof-menu.el,2148
(defvar proof-display-some-buffers-count 17,438
(defun proof-display-some-buffers 19,483
(defun proof-menu-define-keys 78,2685
(defun proof-menu-define-main 135,5494
(defvar proof-menu-favourites 144,5682
(defun proof-menu-define-specific 148,5804
(defun proof-assistant-menu-update 191,7013
(defvar proof-help-menu205,7446
(defvar proof-show-hide-menu213,7724
(defvar proof-buffer-menu222,8037
(defun proof-retract-on-edit-toggle 283,10267
(defun proof-keep-response-history 290,10445
(defconst proof-quick-opts-menu298,10755
(defun proof-quick-opts-vars 465,17706
(defun proof-quick-opts-changed-from-defaults-p 493,18542
(defun proof-quick-opts-changed-from-saved-p 497,18647
(defun proof-quick-opts-save 508,18999
(defun proof-quick-opts-reset 513,19167
(defconst proof-config-menu525,19435
(defconst proof-advanced-menu532,19614
(defvar proof-menu 545,20049
(defun proof-main-menu 554,20333
(defun proof-aux-menu 565,20599
(defun proof-menu-define-favourites-menu 581,20946
(defun proof-def-favourite 601,21602
(defvar proof-make-favourite-cmd-history 624,22577
(defvar proof-make-favourite-menu-history 627,22662
(defun proof-save-favourites 630,22748
(defun proof-del-favourite 635,22896
(defun proof-read-favourite 652,23457
(defun proof-add-favourite 676,24241
(defvar proof-menu-settings 703,25292
(defun proof-menu-define-settings-menu 706,25366
(defun proof-menu-entry-name 739,26498
(defun proof-menu-entry-for-setting 749,26840
(defun proof-settings-vars 768,27375
(defun proof-settings-changed-from-defaults-p 773,27552
(defun proof-settings-changed-from-saved-p 777,27658
(defun proof-settings-save 781,27761
(defun proof-settings-reset 786,27928
(defun proof-defpacustom-fn 793,28173
(defmacro defpacustom 859,30465
(defun proof-assistant-invisible-command-ifposs 874,31292
(defun proof-maybe-askprefs 896,32267
(defun proof-assistant-settings-cmd 902,32461
(defvar proof-assistant-format-table 919,33121
(defun proof-assistant-format-bool 927,33490
(defun proof-assistant-format-int 930,33603
(defun proof-assistant-format-string 933,33695
(defun proof-assistant-format 936,33793

generic/proof-mmm.el,70
(defun proof-mmm-set-global 41,1517
(defun proof-mmm-enable 56,2058

generic/proof-script.el,5766
(defvar proof-element-counters 32,857
(deflocal proof-active-buffer-fake-minor-mode 38,997
(deflocal proof-script-buffer-file-name 41,1123
(deflocal pg-script-portions 48,1533
(defun proof-next-element-count 58,1769
(defun proof-element-id 67,2104
(defun proof-next-element-id 71,2273
(deflocal proof-script-last-entity 85,2590
(defun proof-script-find-next-entity 92,2870
(deflocal proof-locked-span 168,5612
(deflocal proof-queue-span 175,5878
(deflocal proof-overlay-arrow 184,6364
(defun proof-span-give-warning 190,6491
(defun proof-span-read-only 195,6640
(defun proof-strict-read-only 204,7081
(defun proof-set-overlay-arrow 242,8820
(defsubst proof-set-locked-endpoints 253,9158
(defsubst proof-detach-queue 258,9334
(defsubst proof-detach-locked 263,9473
(defsubst proof-set-queue-start 270,9698
(defsubst proof-set-locked-end 274,9824
(defsubst proof-set-queue-end 286,10294
(defun proof-init-segmentation 297,10591
(defun proof-colour-locked 331,12089
(defun proof-restart-buffers 342,12523
(defun proof-script-buffers-with-spans 363,13351
(defun proof-script-remove-all-spans-and-deactivate 373,13707
(defun proof-script-clear-queue-spans 377,13897
(defun proof-script-delete-spans 387,14339
(defun proof-unprocessed-begin 402,14656
(defun proof-script-end 410,14910
(defun proof-queue-or-locked-end 419,15213
(defun proof-locked-end 434,15891
(defun proof-locked-region-full-p 451,16276
(defun proof-locked-region-empty-p 460,16548
(defun proof-only-whitespace-to-locked-region-p 464,16698
(defun proof-in-locked-region-p 477,17320
(defun proof-goto-end-of-locked 489,17583
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 506,18342
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 517,18823
(defun proof-end-of-locked-visible-p 531,19443
(defvar pg-idioms 549,20066
(defvar pg-visibility-specs 552,20162
(defconst pg-default-invisibility-spec557,20369
(defun pg-clear-script-portions 561,20508
(defun pg-add-script-element 568,20755
(defun pg-remove-script-element 571,20831
(defsubst pg-visname 579,21125
(defun pg-add-element 583,21270
(defun pg-open-invisible-span 617,22899
(defun pg-remove-element 628,23262
(defun pg-make-element-invisible 635,23532
(defun pg-make-element-visible 641,23776
(defun pg-toggle-element-visibility 645,23919
(defun pg-redisplay-for-gnuemacs 652,24206
(defun pg-show-all-portions 656,24353
(defun pg-show-all-proofs 674,25050
(defun pg-hide-all-proofs 679,25178
(defun pg-add-proof-element 684,25309
(defun pg-span-name 698,25968
(defvar pg-span-context-menu-keymap719,26675
(defun pg-last-output-displayform 726,26913
(defun pg-set-span-helphighlights 739,27390
(defun proof-complete-buffer-atomic 776,28707
(defun proof-register-possibly-new-processed-file 817,30613
(defun proof-inform-prover-file-retracted 868,32741
(defun proof-auto-retract-dependencies 888,33592
(defun proof-unregister-buffer-file-name 942,36136
(defun proof-protected-process-or-retract 988,37961
(defun proof-deactivate-scripting-auto 1015,39131
(defun proof-deactivate-scripting 1024,39489
(defun proof-activate-scripting 1157,44762
(defun proof-toggle-active-scripting 1277,50140
(defun proof-done-advancing 1318,51501
(defun proof-done-advancing-comment 1414,55164
(defun proof-done-advancing-save 1433,55936
(defun proof-make-goalsave 1526,59581
(defun proof-get-name-from-goal 1542,60366
(defun proof-done-advancing-autosave 1561,61392
(defun proof-done-advancing-other 1626,63936
(defun proof-segment-up-to-parser 1654,64895
(defun proof-script-generic-parse-find-comment-end 1718,66979
(defun proof-script-generic-parse-cmdend 1727,67395
(defun proof-script-generic-parse-cmdstart 1752,68290
(defun proof-script-generic-parse-sexp 1815,70998
(defun proof-cmdstart-add-segment-for-cmd 1839,71934
(defun proof-segment-up-to-cmdstart 1891,74147
(defun proof-segment-up-to-cmdend 1952,76507
(defun proof-semis-to-vanillas 2024,79186
(defun proof-script-new-command-advance 2063,80515
(defun proof-script-next-command-advance 2105,82256
(defun proof-assert-until-point-interactive 2117,82697
(defun proof-assert-until-point 2146,83822
(defun proof-assert-next-command2199,86266
(defun proof-retract-before-change 2247,88516
(defun proof-inside-comment 2256,88854
(defun proof-goto-point 2261,88980
(defun proof-insert-pbp-command 2279,89525
(defun proof-insert-sendback-command 2293,90004
(defun proof-done-retracting 2319,90907
(defun proof-setup-retract-action 2354,92355
(defun proof-last-goal-or-goalsave 2364,92838
(defun proof-retract-target 2388,93743
(defun proof-retract-until-point-interactive 2473,97384
(defun proof-retract-until-point 2481,97769
(define-derived-mode proof-mode 2524,99518
(defun proof-script-set-visited-file-name 2561,100886
(defun proof-script-set-buffer-hooks 2585,101895
(defun proof-script-kill-buffer-fn 2593,102313
(defun proof-config-done-related 2625,103631
(defun proof-generic-goal-command-p 2693,106159
(defun proof-generic-state-preserving-p 2698,106372
(defun proof-generic-count-undos 2707,106889
(defun proof-generic-find-and-forget 2736,107917
(defconst proof-script-important-settings2787,109742
(defun proof-config-done 2802,110295
(defun proof-setup-parsing-mechanism 2871,112601
(defun proof-setup-imenu 2915,114454
(defun proof-setup-func-menu 2932,115058
(deflocal proof-segment-up-to-cache 2994,117284
(deflocal proof-segment-up-to-cache-start 2995,117325
(deflocal proof-last-edited-low-watermark 2996,117370
(defun proof-segment-up-to-using-cache 3006,117857
(defun proof-segment-cache-contents-for 3035,119005
(defun proof-script-after-change-function 3047,119374
(defun proof-script-set-after-change-functions 3059,119888

generic/proof-shell.el,3401
(defvar proof-marker 36,808
(defvar proof-action-list 39,904
(defvar proof-shell-silent 57,1554
(defvar proof-shell-last-prompt 64,1845
(defvar proof-shell-last-output-kind 68,2016
(defvar proof-shell-delayed-output 89,2843
(defvar proof-shell-delayed-output-kind 92,2965
(defvar proof-shell-delayed-output-flags 95,3098
(defcustom proof-shell-active-scripting-indicator104,3295
(defun proof-shell-ready-prover 154,4681
(defun proof-shell-live-buffer 168,5220
(defun proof-shell-available-p 175,5455
(defun proof-grab-lock 181,5677
(defun proof-release-lock 194,6279
(defcustom proof-shell-fiddle-frames 209,6676
(defun proof-shell-set-text-representation 215,6898
(defun proof-shell-start 226,7359
(defvar proof-shell-kill-function-hooks 409,13579
(defun proof-shell-kill-function 412,13679
(defun proof-shell-clear-state 501,17482
(defun proof-shell-exit 516,17925
(defun proof-shell-bail-out 528,18370
(defun proof-shell-restart 537,18847
(defvar proof-shell-urgent-message-marker 577,20134
(defvar proof-shell-urgent-message-scanner 580,20255
(defun proof-shell-handle-output 584,20382
(defsubst proof-shell-strip-output-markup 621,21702
(defvar proof-shell-no-error-display 633,22068
(defun proof-shell-handle-error 639,22271
(defun proof-shell-handle-interrupt 656,23079
(defun proof-shell-error-or-interrupt-action 671,23752
(defun proof-goals-pos 701,24948
(defun proof-pbp-focus-on-first-goal 706,25159
(defsubst proof-shell-string-match-safe 718,25586
(defun proof-shell-classify-output 723,25754
(defvar proof-shell-expecting-output 840,30641
(defvar proof-shell-interrupt-pending 844,30800
(defun proof-interrupt-process 850,31025
(defun proof-shell-insert 888,32480
(defun proof-shell-action-list-item 950,34844
(defun proof-shell-set-silent 956,35089
(defun proof-shell-start-silent-item 962,35308
(defun proof-shell-clear-silent 968,35497
(defun proof-shell-stop-silent-item 974,35719
(defun proof-shell-should-be-silent 981,35988
(defsubst proof-shell-invoke-callback 995,36582
(defun proof-append-alist 999,36748
(defun proof-start-queue 1058,38990
(defun proof-extend-queue 1069,39339
(defun proof-shell-exec-loop 1078,39718
(defun proof-shell-insert-loopback-cmd 1149,42161
(defun proof-shell-message 1177,43483
(defun proof-shell-process-urgent-message 1184,43735
(defun proof-shell-strip-eager-annotations 1314,48852
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1325,49187
(defun proof-shell-minibuffer-urgent-interactive-input 1327,49257
(defun proof-shell-filter 1344,49725
(defun proof-shell-process-urgent-messages 1496,55694
(defun proof-shell-filter-manage-output 1573,58637
(defun proof-shell-handle-delayed-output 1610,60102
(defvar pg-last-tracing-output-time 1651,61651
(defconst pg-slow-mode-duration 1654,61757
(defconst pg-fast-tracing-mode-threshold 1657,61839
(defvar pg-tracing-cleanup-timer 1660,61967
(defun pg-tracing-tight-loop 1662,62006
(defun pg-finish-tracing-display 1705,63719
(defun proof-shell-wait 1723,64083
(defun proof-done-invisible 1742,64991
(defun proof-shell-invisible-command 1748,65161
(defun proof-shell-invisible-cmd-get-result 1795,66705
(defun proof-shell-invisible-command-invisible-result 1807,67141
(define-derived-mode proof-shell-mode 1826,67580
(defconst proof-shell-important-settings1884,69872
(defun proof-shell-config-done 1890,69987

generic/proof-site.el,504
(defconst proof-assistant-table-default22,728
(defconst proof-general-short-version 60,2144
(defconst proof-general-version-year 66,2332
(defgroup proof-general 73,2485
(defgroup proof-general-internals 78,2593
(defun proof-home-directory-fn 91,2981
(defcustom proof-home-directory102,3352
(defcustom proof-images-directory111,3719
(defcustom proof-info-directory117,3921
(defcustom proof-assistant-table145,5108
(defcustom proof-assistants 180,6224
(defun proof-ready-for-assistant 208,7369

generic/proof-splash.el,764
(defcustom proof-splash-enable 17,320
(defcustom proof-splash-time 22,472
(defcustom proof-splash-contents30,757
(defconst proof-splash-startup-msg 70,2102
(defconst proof-splash-welcome 79,2481
(defsubst proof-emacs-imagep 86,2656
(defun proof-get-image 91,2781
(defvar proof-splash-timeout-conf 116,3741
(defun proof-splash-centre-spaces 119,3854
(defun proof-splash-remove-screen 144,4940
(defun proof-splash-remove-buffer 161,5596
(defvar proof-splash-seen 177,6260
(defun proof-splash-display-screen 181,6377
(defun proof-splash-message 263,9713
(defun proof-splash-timeout-waiter 276,10157
(defvar proof-splash-old-frame-title-format 289,10715
(defun proof-splash-set-frame-titles 291,10765
(defun proof-splash-unset-frame-titles 300,11081

generic/proof-syntax.el,1041
(defun proof-ids-to-regexp 15,436
(defun proof-anchor-regexp 19,605
(defconst proof-no-regexp23,707
(defun proof-regexp-alt 28,800
(defun proof-regexp-region 37,1106
(defun proof-re-search-forward-region 46,1529
(defun proof-search-forward 59,2024
(defun proof-replace-regexp-in-string 65,2276
(defun proof-re-search-forward 71,2530
(defun proof-re-search-backward 77,2791
(defun proof-string-match 83,3055
(defun proof-string-match-safe 89,3287
(defun proof-stringfn-match 93,3492
(defun proof-looking-at 100,3752
(defun proof-looking-at-safe 106,3942
(defun proof-looking-at-syntactic-context-default 110,4082
(defun proof-looking-at-syntactic-context 119,4435
(defsubst proof-replace-string 131,4921
(defsubst proof-replace-regexp 136,5125
(defsubst proof-replace-regexp-nocasefold 141,5334
(defvar proof-id 149,5616
(defun proof-ids 155,5836
(defun proof-zap-commas 168,6392
(defun proof-format 184,6888
(defun proof-format-filename 203,7527
(defun proof-insert 250,8927
(defun proof-splice-separator 287,9943

generic/proof-toolbar.el,2357
(defun proof-toolbar-function 35,839
(defun proof-toolbar-icon 38,936
(defun proof-toolbar-enabler 41,1037
(defun proof-toolbar-make-icon 48,1190
(defun proof-toolbar-make-toolbar-items 57,1498
(defvar proof-toolbar-map 82,2304
(defun proof-toolbar-available-p 85,2403
(defun proof-toolbar-setup 94,2679
(defalias 'proof-toolbar-enable proof-toolbar-enable
112,3468
(defalias 'proof-toolbar-undo proof-toolbar-undo
142,4448
(defun proof-toolbar-undo-enable-p 144,4516
(defalias 'proof-toolbar-delete proof-toolbar-delete
151,4674
(defun proof-toolbar-delete-enable-p 153,4755
(defalias 'proof-toolbar-home proof-toolbar-home
161,4937
(defalias 'proof-toolbar-next proof-toolbar-next
165,5004
(defun proof-toolbar-next-enable-p 167,5075
(defalias 'proof-toolbar-goto proof-toolbar-goto
173,5191
(defun proof-toolbar-goto-enable-p 175,5241
(defalias 'proof-toolbar-retract proof-toolbar-retract
180,5326
(defun proof-toolbar-retract-enable-p 182,5383
(defalias 'proof-toolbar-use proof-toolbar-use
188,5502
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
189,5554
(defalias 'proof-toolbar-restart proof-toolbar-restart
193,5635
(defalias 'proof-toolbar-goal proof-toolbar-goal
197,5700
(defalias 'proof-toolbar-qed proof-toolbar-qed
201,5758
(defun proof-toolbar-qed-enable-p 203,5807
(defalias 'proof-toolbar-state proof-toolbar-state
211,5969
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
212,6012
(defalias 'proof-toolbar-context proof-toolbar-context
216,6091
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
217,6137
(defalias 'proof-toolbar-command proof-toolbar-command
221,6218
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
222,6274
(defun proof-toolbar-help 226,6380
(defalias 'proof-toolbar-find proof-toolbar-find
232,6461
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
233,6513
(defalias 'proof-toolbar-info proof-toolbar-info
237,6589
(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
238,6644
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
242,6742
(defun proof-toolbar-visibility-enable-p 244,6802
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
249,6916
(defun proof-toolbar-interrupt-enable-p 250,6977
(defun proof-toolbar-scripting-menu 258,7130

generic/proof-unicode-tokens.el,496
(defvar proof-unicode-tokens-initialised 28,761
(defun proof-unicode-tokens-init 31,868
(defun proof-unicode-tokens-configure 45,1370
(defun proof-unicode-tokens-enable 57,1818
(defun proof-unicode-tokens-mode-if-enabled 71,2505
(defun proof-unicode-tokens-set-global 77,2704
(defun proof-unicode-tokens-reconfigure 95,3344
(defun proof-unicode-tokens-configure-prover 121,4232
(defun proof-unicode-tokens-activate-prover 126,4413
(defun proof-unicode-tokens-deactivate-prover 133,4659

generic/proof-useropts.el,1416
(defgroup proof-user-options 21,552
(defun proof-set-value 29,731
(defcustom proof-electric-terminator-enable 62,1854
(defcustom proof-toolbar-enable 74,2386
(defcustom proof-imenu-enable 80,2559
(defcustom pg-show-hints 86,2730
(defcustom proof-trace-output-slow-catchup 92,2925
(defcustom proof-strict-state-preserving 102,3422
(defcustom proof-strict-read-only 115,4031
(defcustom proof-allow-undo-in-read-only 127,4541
(defcustom proof-three-window-enable 135,4819
(defcustom proof-multiple-frames-enable 154,5569
(defcustom proof-delete-empty-windows 163,5902
(defcustom proof-shrink-windows-tofit 174,6433
(defcustom proof-auto-raise-buffers 181,6705
(defcustom proof-colour-locked 188,6940
(defcustom proof-query-file-save-when-activating-scripting196,7190
(defcustom proof-one-command-per-line212,7910
(defcustom proof-prog-name-ask219,8134
(defcustom proof-prog-name-guess225,8294
(defcustom proof-tidy-response233,8559
(defcustom proof-keep-response-history247,9022
(defcustom pg-input-ring-size 257,9410
(defcustom proof-general-debug 262,9562
(defcustom proof-use-parser-cache 273,9971
(defcustom proof-follow-mode 283,10268
(defcustom proof-auto-action-when-deactivating-scripting 307,11445
(defcustom proof-script-command-separator 330,12394
(defcustom proof-rsh-command 338,12686
(defcustom proof-disappearing-proofs 354,13236
(defcustom proof-full-annotation 359,13397

generic/proof-utils.el,1911
(defmacro deflocal 62,1812
(defmacro proof-with-current-buffer-if-exists 69,2050
(deflocal proof-buffer-type 75,2260
(defmacro proof-with-script-buffer 81,2540
(defmacro proof-map-buffers 92,2927
(defmacro proof-sym 97,3112
(defsubst proof-try-require 102,3273
(defun proof-save-some-buffers 115,3604
(defmacro proof-ass-sym 164,5205
(defmacro proof-ass-symv 170,5464
(defmacro proof-ass 176,5722
(defun proof-defpgcustom-fn 182,5974
(defun undefpgcustom 203,6845
(defmacro defpgcustom 209,7069
(defun proof-defpgdefault-fn 220,7487
(defmacro defpgdefault 234,7945
(defmacro defpgfun 245,8307
(defmacro proof-eval-when-ready-for-assistant 255,8572
(defun proof-file-truename 268,8967
(defun proof-file-to-buffer 272,9150
(defun proof-files-to-buffers 283,9479
(defun proof-buffers-in-mode 290,9762
(defun pg-save-from-death 304,10212
(defun proof-define-keys 323,10829
(defun pg-remove-specials 334,11121
(defun pg-remove-specials-in-string 344,11459
(defun proof-warn-if-unset 355,11687
(defun proof-get-window-for-buffer 360,11905
(defun proof-display-and-keep-buffer 411,14213
(defun proof-clean-buffer 453,16104
(defun proof-message 468,16725
(defun proof-warning 473,16938
(defun pg-internal-warning 479,17220
(defun proof-debug 487,17539
(defun proof-switch-to-buffer 496,17889
(defun proof-resize-window-tofit 518,19015
(defun proof-submit-bug-report 612,23190
(defun proof-deftoggle-fn 647,24547
(defmacro proof-deftoggle 662,25200
(defun proof-defintset-fn 669,25574
(defmacro proof-defintset 685,26278
(defun proof-defstringset-fn 692,26655
(defmacro proof-defstringset 705,27281
(defun proof-escape-keymap-doc 718,27737
(defmacro proof-defshortcut 722,27870
(defmacro proof-definvisible 737,28468
(defun pg-custom-save-vars 764,29389
(defun pg-custom-reset-vars 780,30034
(defun proof-locate-executable 793,30371
(defun pg-current-word-pos 817,31151

lib/bufhist.el,1099
(defun bufhist-ring-update 34,1244
(defgroup bufhist 43,1566
(defcustom bufhist-ring-size 47,1647
(defvar bufhist-ring 52,1758
(defvar bufhist-ring-pos 55,1832
(defvar bufhist-lastswitch-modified-tick 58,1911
(defvar bufhist-read-only-history 61,2017
(defvar bufhist-saved-mode-line-format 64,2088
(defun bufhist-mode-line-format-entry 67,2189
(defun bufhist-get-buffer-contents 99,3465
(defun bufhist-restore-buffer-contents 111,3949
(defun bufhist-checkpoint 119,4236
(defun bufhist-erase-buffer 127,4605
(defun bufhist-checkpoint-and-erase 137,4950
(defun bufhist-switch-to-index 143,5136
(defun bufhist-first 182,6740
(defun bufhist-last 187,6899
(defun bufhist-prev 192,7045
(defun bufhist-next 200,7268
(defun bufhist-delete 205,7408
(defun bufhist-clear 217,7951
(defun bufhist-init 232,8347
(defun bufhist-exit 257,9284
(defun bufhist-set-readwrite 267,9548
(defun bufhist-before-change-function 282,10168
(defun bufhist-make-buttons 294,10584
(defconst bufhist-minor-mode-map308,10902
(define-minor-mode bufhist-mode321,11379
(defun bufhist-toggle-fn 341,12164

lib/holes.el,2447
(defvar holes-doc 38,1074
(defvar holes-default-hole 133,4672
(defvar holes-active-hole 137,4841
(defcustom holes-empty-hole-string 144,5050
(defcustom holes-empty-hole-regexp 147,5161
(defcustom holes-search-limit 154,5452
(defface active-hole-face166,5828
(defface inactive-hole-face175,6228
(defun holes-region-beginning-or-nil 187,6655
(defun holes-region-end-or-nil 191,6750
(defun holes-copy-active-region 195,6833
(defun holes-is-hole-p 201,7017
(defun holes-hole-start-position 206,7121
(defun holes-hole-end-position 212,7307
(defun holes-hole-buffer 219,7491
(defun holes-hole-at 226,7666
(defun holes-active-hole-exist-p 233,7841
(defun holes-active-hole-start-position 243,8099
(defun holes-active-hole-end-position 253,8471
(defun holes-active-hole-buffer 264,8840
(defun holes-goto-active-hole 275,9146
(defun holes-highlight-hole-as-active 287,9414
(defun holes-highlight-hole 297,9726
(defun holes-disable-active-hole 308,10018
(defun holes-set-active-hole 326,10561
(defun holes-is-in-hole-p 339,10907
(defun holes-make-hole 346,11050
(defun holes-make-hole-at 372,11796
(defun holes-clear-hole 392,12272
(defun holes-clear-hole-at 404,12561
(defun holes-map-holes 413,12820
(defun holes-mapcar-holes 421,13003
(defun holes-clear-all-buffer-holes 427,13175
(defun holes-next 438,13475
(defun holes-next-after-active-hole 445,13726
(defun holes-set-active-hole-next 453,13945
(defun holes-replace-segment 475,14498
(defun holes-replace 485,14852
(defun holes-replace-active-hole 516,16047
(defun holes-replace-update-active-hole 525,16343
(defun holes-delete-update-active-hole 546,17016
(defun holes-set-make-active-hole 555,17246
(defun holes-mouse-replace-active-hole 602,18971
(defun holes-destroy-hole 622,19481
(defun holes-hole-at-event 639,19892
(defun holes-mouse-destroy-hole 644,20005
(defun holes-mouse-forget-hole 654,20245
(defun holes-mouse-set-make-active-hole 670,20555
(defun holes-mouse-set-active-hole 692,21092
(defun holes-set-point-next-hole-destroy 704,21356
(defvar hole-map720,21806
(defvar holes-mode-map730,22189
(defun holes-replace-string-by-holes-backward 767,23664
(defun holes-skeleton-end-hook 785,24365
(defconst holes-jump-doc 794,24803
(defun holes-replace-string-by-holes-backward-jump 801,25010
(defun holes-abbrev-complete 818,25692
(defun holes-insert-and-expand 827,26013
(defvar holes-mode 838,26445
(defun holes-mode 844,26641

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,828
(defun local-vars-list-insert-empty-zone 44,1391
(defun local-vars-list-find 82,2099
(defun local-vars-list-goto-var 101,2874
(defun local-vars-list-get-current 127,3924
(defun local-vars-list-set-current 148,4774
(defun local-vars-list-get 171,5491
(defun local-vars-list-get-safe 188,6023
(defun local-vars-list-set 193,6217

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 56,2317
(defvar maths-menu-tokenise-insert 59,2426
(defun maths-menu-build-menu 62,2565
(defvar maths-menu-menu84,3329
(defvar maths-menu-mode-map344,12887
(define-minor-mode maths-menu-mode352,13106

lib/pg-dev.el,102
(defconst pg-dev-lisp-font-lock-keywords36,1103
(defun unload-pg 70,2040
(defun profile-pg 98,2901

lib/pg-fontsets.el,176
(defcustom pg-fontsets-default-fontset 28,782
(defun pg-fontsets-make-fontsetsizes 33,928
(defconst pg-fontsets-base-fonts 52,1692
(defun pg-fontsets-make-fontsets 58,1824

lib/proof-compat.el,412
(defvar proof-running-on-win32 31,978
(defun pg-custom-undeclare-variable 51,1756
(defmacro save-selected-frame 83,2532
(defun proof-buffer-syntactic-context-emulate 99,3182
(defvar read-shell-command-map127,4392
(defun read-shell-command 145,5080
(defun frames-of-buffer 155,5508
(defmacro with-selected-window 199,6921
(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
236,8026

lib/span.el,1353
(defalias 'span-start span-start
22,612
(defalias 'span-end span-end
23,650
(defalias 'span-set-property span-set-property
24,684
(defalias 'span-property span-property
25,727
(defalias 'span-make span-make
26,766
(defalias 'span-detach span-detach
27,802
(defalias 'span-set-endpoints span-set-endpoints
28,842
(defalias 'span-buffer span-buffer
29,887
(defun span-read-only-hook 31,928
(defun span-read-only 36,1118
(defun span-read-write 43,1425
(defun span-give-warning 48,1592
(defun span-write-warning 53,1735
(defun span-lt 65,2319
(defun spans-at-point-prop 70,2460
(defun spans-at-region-prop 76,2625
(defun span-at 85,2937
(defsubst span-delete 91,3153
(defsubst span-mapcar-spans 98,3375
(defun span-at-before 103,3634
(defun prev-span 120,4360
(defun next-span 126,4511
(defsubst span-live-p 133,4723
(defun span-raise 139,4889
(defalias 'span-object span-object
143,5019
(defun span-string 145,5060
(defun set-span-properties 150,5198
(defun span-find-span 160,5445
(defsubst span-at-event 167,5751
(defun make-detached-span 171,5872
(defun fold-spans 176,5968
(defsubst span-detached-p 190,6501
(defsubst set-span-face 194,6617
(defun set-span-keymap 198,6715
(defsubst span-delete-spans 207,6918
(defsubst span-property-safe 211,7082
(defsubst span-set-start 215,7221
(defsubst span-set-end 219,7353

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3035
(defun texi-docstring-magic-splice-sep 93,3200
(defconst texi-docstring-magic-munge-table103,3505
(defun texi-docstring-magic-untabify 193,7272
(defun texi-docstring-magic-munge-docstring 203,7587
(defun texi-docstring-magic-texi 242,8874
(defun texi-docstring-magic-format-default 255,9314
(defun texi-docstring-magic-texi-for 271,9949
(defconst texi-docstring-magic-comment329,11909
(defun texi-docstring-magic 335,12063
(defun texi-docstring-magic-face-at-point 369,13143
(defun texi-docstring-magic-insert-magic 384,13666

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,349
(defun unicode-chars-list-chars 5050,245961

lib/unicode-tokens.el,4802
(defvar unicode-tokens-token-symbol-map 55,1770
(defvar unicode-tokens-token-format 74,2393
(defvar unicode-tokens-token-variant-format-regexp 80,2642
(defvar unicode-tokens-shortcut-alist 91,3024
(defvar unicode-tokens-shortcut-replacement-alist 97,3302
(defvar unicode-tokens-control-region-format-regexp 105,3508
(defvar unicode-tokens-control-char-format-regexp 112,3876
(defvar unicode-tokens-control-regions 119,4237
(defvar unicode-tokens-control-characters 122,4313
(defvar unicode-tokens-control-char-format 125,4395
(defvar unicode-tokens-control-region-format-start 128,4508
(defvar unicode-tokens-control-region-format-end 131,4625
(defconst unicode-tokens-configuration-variables138,4778
(defun unicode-tokens-config 152,5143
(defun unicode-tokens-config-var 156,5288
(defun unicode-tokens-copy-configuration-variables 168,5729
(defun unicode-tokens-customize 185,6613
(defvar unicode-tokens-token-list 198,6943
(defvar unicode-tokens-hash-table 201,7063
(defvar unicode-tokens-token-match-regexp 204,7179
(defvar unicode-tokens-uchar-hash-table 207,7291
(defvar unicode-tokens-uchar-regexp 211,7478
(defgroup unicode-tokens-faces 236,8084
(defconst unicode-tokens-font-family-alternatives246,8381
(defface unicode-tokens-symbol-font-face260,8832
(defface unicode-tokens-script-font-face278,9472
(defface unicode-tokens-fraktur-font-face283,9616
(defface unicode-tokens-serif-font-face288,9741
(defface unicode-tokens-sans-font-face293,9868
(defface unicode-tokens-highlight-face298,9990
(defconst unicode-tokens-fonts307,10352
(defconst unicode-tokens-fontsymb-properties 316,10569
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
342,12106
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
360,12668
(defconst unicode-tokens-font-lock-extra-managed-props373,12999
(defun unicode-tokens-font-lock-keywords 377,13153
(defun unicode-tokens-usable-composition 417,14806
(defun unicode-tokens-help-echo 430,15185
(defvar unicode-tokens-show-symbols 434,15349
(defun unicode-tokens-font-lock-compose-symbol 437,15463
(defun unicode-tokens-prepend-text-properties-in-match 465,16641
(defun unicode-tokens-prepend-text-property 479,17220
(defun unicode-tokens-show-symbols 504,18389
(defun unicode-tokens-symbs-to-props 512,18699
(defvar unicode-tokens-show-controls 532,19399
(defun unicode-tokens-show-controls 535,19490
(defun unicode-tokens-control-char 548,20075
(defun unicode-tokens-control-region 557,20514
(defun unicode-tokens-control-font-lock-keywords 567,21056
(defvar unicode-tokens-use-shortcuts 578,21386
(defun unicode-tokens-use-shortcuts 581,21489
(defun unicode-tokens-map-ordering 599,22095
(defun unicode-tokens-quail-define-rules 603,22245
(defun unicode-tokens-insert-token 626,22922
(defun unicode-tokens-annotate-region 635,23226
(defun unicode-tokens-insert-control 659,24064
(defun unicode-tokens-insert-uchar-as-token 669,24513
(defun unicode-tokens-delete-token-near-point 675,24734
(defun unicode-tokens-prev-token 689,25296
(defun unicode-tokens-rotate-token-forward 698,25646
(defun unicode-tokens-rotate-token-backward 725,26537
(defun unicode-tokens-replace-shortcut-match 730,26739
(defun unicode-tokens-replace-shortcuts 738,27041
(defun unicode-tokens-copy-token 755,27658
(define-button-type 'unicode-tokens-listunicode-tokens-list
762,27879
(defun unicode-tokens-list-tokens 768,28083
(defun unicode-tokens-list-shortcuts 807,29269
(defun unicode-tokens-encode-in-temp-buffer 827,29912
(defun unicode-tokens-encode 847,30674
(defun unicode-tokens-encode-str 852,30895
(defun unicode-tokens-copy 856,31057
(defun unicode-tokens-paste 865,31463
(defvar unicode-tokens-highlight-unicode 881,32006
(defconst unicode-tokens-unicode-highlight-patterns884,32098
(defun unicode-tokens-highlight-unicode 888,32267
(defun unicode-tokens-highlight-unicode-setkeywords 900,32730
(defun unicode-tokens-initialise 912,33100
(defvar unicode-tokens-mode-map 924,33552
(define-minor-mode unicode-tokens-mode927,33649
(defun unicode-tokens-set-font-var 1016,36674
(defun unicode-tokens-mouse-set-font 1055,38125
(defsubst unicode-tokens-face-font-sym 1068,38640
(defun unicode-tokens-set-font-restart 1072,38820
(defun unicode-tokens-save-fonts 1079,39100
(defun unicode-tokens-custom-save-faces 1088,39382
(define-key unicode-tokens-mode-map 1104,39839
(define-key unicode-tokens-mode-map 1106,39931
(define-key unicode-tokens-mode-map1108,40022
(define-key unicode-tokens-mode-map1110,40128
(define-key unicode-tokens-mode-map1113,40243
(define-key unicode-tokens-mode-map1115,40352
(define-key unicode-tokens-mode-map1117,40460
(define-key unicode-tokens-mode-map1119,40566
(defun unicode-tokens-define-menu 1127,40694

mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2676
(defun mmm-autoload-class 89,3439
(defvar mmm-changed-buffers-list 129,5006
(defun mmm-major-mode-change 132,5113
(defun mmm-check-changed-buffers 145,5634
(defun mmm-mode-on-maybe 155,6007
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6425
(defun mmm-add-find-file-hook 168,6485

mmm/mmm-class.el,416
(defun mmm-get-class-spec 42,1296
(defun mmm-get-class-parameter 59,2009
(defun mmm-set-class-parameter 63,2175
(defun* mmm-apply-class75,2539
(defun* mmm-apply-classes90,3177
(defun* mmm-apply-all 110,3943
(defun* mmm-ify124,4390
(defun* mmm-match-region206,7473
(defun mmm-match->point 267,10162
(defun mmm-match-and-verify 281,10684
(defun mmm-get-form 307,11742
(defun mmm-default-get-form 318,12238

mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1210
(defun mmm-ify-region 63,1934
(defun mmm-ify-by-regexp75,2362
(defun mmm-parse-buffer 97,3038
(defun mmm-parse-region 106,3374
(defun mmm-parse-block 115,3753
(defun mmm-get-block 132,4504
(defun mmm-reparse-current-region 146,4835
(defun mmm-clear-current-region 167,5509
(defun mmm-clear-regions 172,5673
(defun mmm-clear-all-regions 177,5819
(defun* mmm-end-current-region 185,5979
(defun mmm-narrow-to-submode-region 220,7402
(defun mmm-insert-region 239,8016
(defun mmm-insert-by-key 258,8878
(defun mmm-get-insertion-spec 342,12438
(defun mmm-insertion-help 369,13517
(defun mmm-display-insertion-key 379,13887
(defun mmm-get-all-insertion-keys 401,14709

mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1313
(defvar mmm-keywords-used49,1616
(defmacro mmm-regexp-opt 91,2662
(defvar mmm-evaporate-property110,3311
(defmacro mmm-set-keymap-default 128,4077
(defmacro mmm-event-key 137,4519
(defvar skeleton-positions 146,4738
(defun mmm-fixup-skeleton 147,4769
(defmacro mmm-make-temp-buffer 159,5206
(defvar mmm-font-lock-available-p 172,5602
(defmacro mmm-set-font-lock-defaults 179,5816

mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1117
(defvar mmm-cweb-section-regexp41,1164
(defvar mmm-cweb-c-part-tags44,1254
(defvar mmm-cweb-c-part-regexp47,1313
(defun mmm-cweb-in-limbo 50,1397
(defun mmm-cweb-verify-brief-c 57,1622

mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1236
(defvar mmm-mason-pseudo-perl-tags45,1377
(defvar mmm-mason-non-perl-tags48,1453
(defvar mmm-mason-perl-tags-regexp51,1554
(defvar mmm-mason-pseudo-perl-tags-regexp56,1749
(defvar mmm-mason-tag-names-regexp61,1966
(defun mmm-mason-verify-inline 66,2186
(defun mmm-mason-start-line 156,5090
(defun mmm-mason-end-line 161,5155
(defun mmm-mason-set-mode-line 168,5249

mmm/mmm-mode.el,1024
(defun mmm-mode 101,3867
(defun mmm-mode-on 140,5372
(defun mmm-mode-off 181,7132
(defvar mmm-mode-map 206,7865
(defvar mmm-mode-prefix-map 209,7940
(defvar mmm-mode-menu-map 212,8050
(defun mmm-define-key 215,8141
(define-key mmm-mode-prefix-map 239,8896
(define-key mmm-mode-prefix-map 246,9154
(define-key mmm-mode-map 249,9265
(define-key mmm-mode-menu-map 252,9367
(define-key mmm-mode-menu-map 254,9439
(define-key mmm-mode-menu-map 256,9498
(define-key mmm-mode-menu-map 258,9579
(define-key mmm-mode-menu-map 260,9660
(define-key mmm-mode-menu-map 262,9747
(define-key mmm-mode-menu-map 265,9841
(define-key mmm-mode-menu-map 267,9901
(define-key mmm-mode-menu-map 270,9992
(define-key mmm-mode-menu-map 272,10052
(define-key mmm-mode-menu-map 274,10159
(define-key mmm-mode-menu-map 276,10244
(define-key mmm-mode-menu-map 279,10330
(define-key mmm-mode-menu-map 281,10390
(define-key mmm-mode-menu-map 283,10503
(define-key mmm-mode-menu-map 285,10588
(define-key mmm-mode-map 288,10671

mmm/mmm-noweb.el,1291
(defvar mmm-noweb-code-mode 44,1352
(defvar mmm-noweb-quote-mode 50,1649
(defvar mmm-noweb-quote-string 54,1806
(defvar mmm-noweb-quote-number 58,1929
(defvar mmm-noweb-narrowing 62,2045
(defun mmm-noweb-chunk 68,2176
(defun mmm-noweb-quote 84,2876
(defun mmm-noweb-quote-name 89,3042
(defun mmm-noweb-chunk-name 95,3302
(defun mmm-noweb-regions 140,4748
(defun mmm-noweb-narrow-to-doc-chunk 166,5616
(defun mmm-noweb-fill-chunk 189,6386
(defun mmm-noweb-fill-paragraph-chunk 208,7070
(defun mmm-noweb-fill-named-chunk 222,7487
(defun mmm-noweb-auto-fill-doc-chunk 238,8064
(defun mmm-noweb-auto-fill-doc-mode 246,8283
(defun mmm-noweb-auto-fill-code-mode 251,8473
(defun mmm-noweb-complete-chunk 259,8685
(defvar mmm-noweb-chunk-history 292,9689
(defun mmm-noweb-goto-chunk 295,9767
(defun mmm-noweb-goto-next 307,10091
(defun mmm-noweb-goto-previous 319,10448
(defvar mmm-noweb-map 336,10852
(defvar mmm-noweb-prefix-map 337,10896
(define-key mmm-noweb-map 338,10947
(define-key mmm-noweb-prefix-map 347,11390
(defun mmm-noweb-bind-keys 352,11656
(defun mmm-syntax-region-list 368,12070
(defun mmm-syntax-other-regions 377,12426
(defun mmm-word-other-regions 389,12897
(defun mmm-space-other-regions 395,13066
(defun mmm-undo-syntax-other-regions 401,13237

mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1749
(defun mmm-overlays-at 59,1934
(defun mmm-included-p 72,2387
(defun mmm-overlays-containing 112,3876
(defun mmm-overlays-contained-in 125,4314
(defun mmm-overlays-overlapping 138,4754
(defun mmm-sort-overlays 149,5117
(defvar mmm-current-overlay 158,5387
(defvar mmm-previous-overlay 163,5602
(defvar mmm-current-submode 168,5790
(defvar mmm-previous-submode 173,5990
(defun mmm-update-current-submode 178,6163
(defun mmm-set-current-submode 199,6979
(defun mmm-submode-at 210,7471
(defun mmm-match-front 219,7746
(defun mmm-match-back 238,8507
(defun mmm-front-start 257,9252
(defun mmm-back-end 265,9556
(defun mmm-valid-submode-region 278,9903
(defun* mmm-make-region305,11059
(defun mmm-make-overlay 431,16430
(defun mmm-get-face 459,17563
(defun mmm-clear-overlays 470,17855
(defun mmm-update-mode-info 486,18322
(defun mmm-update-submode-region 571,22607
(defun mmm-add-hooks 588,23365
(defun mmm-remove-hooks 592,23500
(defun mmm-get-local-variables-list 598,23627
(defun mmm-get-locals 618,24547
(defun mmm-get-saved-local 631,25128
(defun mmm-set-local-variables 635,25293
(defun mmm-get-saved-local-variables 646,25734
(defun mmm-save-changed-local-variables 654,26051
(defun mmm-clear-local-variables 673,26909
(defun mmm-enable-font-lock 684,27188
(defun mmm-update-font-lock-buffer 692,27448
(defun mmm-refontify-maybe 705,27880
(defun mmm-submode-changes-in 720,28402
(defun mmm-regions-in 731,28850
(defun mmm-regions-alist 745,29420
(defun mmm-fontify-region 762,30066
(defun mmm-fontify-region-list 782,31097
(defun mmm-beginning-of-syntax 804,32013

mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1618
(defvar mmm-rpm-sh-end-tags53,1842
(defvar mmm-rpm-sh-start-regexp57,2016
(defvar mmm-rpm-sh-end-regexp61,2194

mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2615
(defun mmm-here-doc-get-mode 93,3100
(defun mmm-file-variables-verify 208,6818
(defun mmm-file-variables-find-back 232,7854

mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 41,1310
(defmacro mmm-save-all 60,1954
(defun mmm-format-string 73,2243
(defun mmm-format-matches 84,2695
(defmacro mmm-save-keyword 107,3488
(defmacro mmm-save-keywords 115,3815
(defun mmm-looking-back-at 128,4348
(defun mmm-make-marker 145,4916

mmm/mmm-vars.el,2667
(defgroup mmm 99,3073
(defvar mmm-c-derived-modes106,3183
(defvar mmm-save-local-variables 110,3302
(defvar mmm-buffer-saved-locals 336,10162
(defvar mmm-region-saved-locals-defaults 341,10362
(defvar mmm-region-saved-locals-for-dominant 347,10622
(defgroup mmm-faces 357,10999
(defcustom mmm-submode-decoration-level 363,11170
(defface mmm-init-submode-face 381,12042
(defface mmm-cleanup-submode-face 385,12182
(defface mmm-declaration-submode-face 389,12319
(defface mmm-comment-submode-face 393,12465
(defface mmm-output-submode-face 397,12618
(defface mmm-special-submode-face 401,12767
(defface mmm-code-submode-face 405,12931
(defface mmm-default-submode-face 409,13070
(defface mmm-delimiter-face 414,13278
(defcustom mmm-mode-string 421,13404
(defcustom mmm-submode-mode-line-format 426,13535
(defvar mmm-primary-mode-display-name 443,14190
(defvar mmm-buffer-mode-display-name 448,14404
(defun mmm-set-mode-line 454,14703
(defvar mmm-classes 478,15511
(defvar mmm-global-classes 484,15756
(defcustom mmm-mode-ext-classes-alist 491,15938
(defun mmm-add-mode-ext-class 510,16756
(defcustom mmm-major-mode-preferences519,17081
(defun mmm-add-to-major-mode-preferences 537,17879
(defun mmm-ensure-modename 553,18665
(defun mmm-modename->function 562,18975
(defcustom mmm-delimiter-mode 576,19438
(defcustom mmm-mode-prefix-key 586,19707
(defcustom mmm-command-modifiers 591,19834
(defcustom mmm-insert-modifiers 605,20467
(defcustom mmm-use-old-command-keys 620,21145
(defun mmm-use-old-command-keys 630,21609
(defcustom mmm-mode-hook 638,21808
(defun mmm-run-constructed-hook 658,22615
(defun mmm-run-major-hook 666,23001
(defun mmm-run-submode-hook 669,23078
(defvar mmm-class-hooks-run 672,23165
(defun mmm-run-class-hook 677,23337
(defvar mmm-primary-mode-entry-hook 682,23509
(defcustom mmm-major-mode-hook 697,24156
(defun mmm-run-major-mode-hook 711,24787
(defcustom mmm-global-mode 724,25328
(defcustom mmm-never-modes740,26023
(defvar mmm-set-file-name-for-modes 758,26323
(defvar mmm-mode 769,26682
(defvar mmm-primary-mode 777,26890
(defvar mmm-classes-alist 788,27256
(defun mmm-add-classes 943,35463
(defun mmm-add-group 948,35628
(defun mmm-add-to-group 958,36078
(defconst mmm-version 972,36575
(defun mmm-version 975,36640
(defvar mmm-temp-buffer-name 982,36783
(defvar mmm-interactive-history 988,36913
(defun mmm-add-to-history 994,37182
(defun mmm-clear-history 997,37265
(defvar mmm-mode-ext-classes 1005,37450
(defun mmm-get-mode-ext-classes 1010,37661
(defun mmm-clear-mode-ext-classes 1019,38037
(defun mmm-mode-ext-applies 1023,38162
(defun mmm-get-all-classes 1037,38646

doc/ProofGeneral.texi,5693
@node Top164,4909
@node Preface201,6016
@node News for Version 4.0News for Version 4.0
224,6605
@node Future249,7453
@node Credits280,8752
@node Introducing Proof GeneralIntroducing Proof General
385,12394
@node Installing Proof GeneralInstalling Proof General
440,14372
@node Quick start guideQuick start guide
454,14821
@node Features of Proof GeneralFeatures of Proof General
498,16942
@node Supported proof assistantsSupported proof assistants
587,20879
@node Prerequisites for this manualPrerequisites for this manual
636,22768
@node Organization of this manualOrganization of this manual
680,24387
@node Basic Script ManagementBasic Script Management
706,25215
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
725,25815
@node Proof scriptsProof scripts
991,36048
@node Script buffersScript buffers
1034,38168
@node Locked queue and editing regionsLocked queue and editing regions
1056,38745
@node Goal-save sequencesGoal-save sequences
1112,40892
@node Active scripting bufferActive scripting buffer
1149,42378
@node Summary of Proof General buffersSummary of Proof General buffers
1218,45798
@node Script editing commandsScript editing commands
1281,48538
@node Script processing commandsScript processing commands
1361,51496
@node Proof assistant commandsProof assistant commands
1489,56810
@node Toolbar commandsToolbar commands
1661,62916
@node Interrupting during trace outputInterrupting during trace output
1685,63845
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1724,65766
@node Goals buffer commandsGoals buffer commands
1738,66266
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1827,69830
@node Document centred workingDocument centred working
1859,71045
@node Visibility of completed proofsVisibility of completed proofs
1923,72976
@node Switching between proof scriptsSwitching between proof scripts
1978,74899
@node View of processed files View of processed files 
2015,76871
@node Retracting across filesRetracting across files
2075,79922
@node Asserting across filesAsserting across files
2088,80553
@node Automatic multiple file handlingAutomatic multiple file handling
2101,81119
@node Escaping script managementEscaping script management
2126,82153
@node Editing featuresEditing features
2184,84356
@node Support for other PackagesSupport for other Packages
2255,87148
@node Syntax highlightingSyntax highlighting
2287,88022
@node Unicode supportUnicode support
2316,89026
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2472,95261
@node Support for outline modeSupport for outline mode
2527,97305
@node Support for completionSupport for completion
2552,98434
@node Support for tagsSupport for tags
2609,100596
@node Customizing Proof GeneralCustomizing Proof General
2661,102924
@node Basic optionsBasic options
2701,104594
@node How to customizeHow to customize
2725,105352
@node Display customizationDisplay customization
2772,107319
@node User optionsUser options
2926,113719
@node Changing facesChanging faces
3168,122255
@node Tweaking configuration settingsTweaking configuration settings
3243,124924
@node Hints and TipsHints and Tips
3300,127450
@node Adding your own keybindingsAdding your own keybindings
3319,128051
@node Using file variablesUsing file variables
3383,130638
@node Using abbreviationsUsing abbreviations
3442,132824
@node LEGO Proof GeneralLEGO Proof General
3481,134239
@node LEGO specific commandsLEGO specific commands
3522,135608
@node LEGO tagsLEGO tags
3542,136063
@node LEGO customizationsLEGO customizations
3552,136310
@node Coq Proof GeneralCoq Proof General
3584,137229
@node Coq-specific commandsCoq-specific commands
3600,137638
@node Coq-specific variablesCoq-specific variables
3622,138145
@node Editing multiple proofsEditing multiple proofs
3644,138803
@node User-loaded tacticsUser-loaded tactics
3668,139911
@node Holes featureHoles feature
3732,142385
@node Isabelle Proof GeneralIsabelle Proof General
3759,143672
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3790,144841
@node Isabelle commandsIsabelle commands
3859,147649
@node Isabelle settingsIsabelle settings
4002,151802
@node Isabelle customizationsIsabelle customizations
4016,152384
@node HOL Proof GeneralHOL Proof General
4039,152871
@node Shell Proof GeneralShell Proof General
4081,154693
@node Obtaining and InstallingObtaining and Installing
4117,156152
@node Obtaining Proof GeneralObtaining Proof General
4133,156565
@node Installing Proof General from tarballInstalling Proof General from tarball
4164,157804
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4189,158636
@node Setting the names of binariesSetting the names of binaries
4204,159044
@node Notes for syssiesNotes for syssies
4232,159984
@node Bugs and EnhancementsBugs and Enhancements
4307,163020
@node References4328,163835
@node History of Proof GeneralHistory of Proof General
4368,164858
@node Old News for 3.0Old News for 3.0
4462,169023
@node Old News for 3.1Old News for 3.1
4532,172717
@node Old News for 3.2Old News for 3.2
4558,173889
@node Old News for 3.3Old News for 3.3
4619,176892
@node Old News for 3.4Old News for 3.4
4638,177789
@node Old News for 3.5Old News for 3.5
4660,178844
@node Old News for 3.6Old News for 3.6
4664,178901
@node Old News for 3.7Old News for 3.7
4669,179001
@node Function IndexFunction Index
4713,180899
@node Variable IndexVariable Index
4717,180975
@node Keystroke IndexKeystroke Index
4721,181055
@node Concept IndexConcept Index
4725,181121

doc/PG-adapting.texi,3772
@node Top155,4687
@node Introduction192,5796
@node Future233,7449
@node Credits269,9045
@node Beginning with a New ProverBeginning with a New Prover
279,9337
@node Overview of adding a new proverOverview of adding a new prover
319,11279
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
397,14587
@node Major modes used by Proof GeneralMajor modes used by Proof General
466,17978
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
509,19688
@node Settings for generic user-level commandsSettings for generic user-level commands
524,20234
@node Menu configurationMenu configuration
569,21966
@node Toolbar configurationToolbar configuration
593,22883
@node Proof Script SettingsProof Script Settings
652,25120
@node Recognizing commands and commentsRecognizing commands and comments
674,25700
@node Recognizing proofsRecognizing proofs
811,32137
@node Recognizing other elementsRecognizing other elements
920,36818
@node Configuring undo behaviourConfiguring undo behaviour
1046,42357
@node Nested proofsNested proofs
1183,47769
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1223,49395
@node Activate scripting hookActivate scripting hook
1246,50348
@node Automatic multiple filesAutomatic multiple files
1270,51218
@node Completions1292,52065
@node Proof Shell SettingsProof Shell Settings
1333,53555
@node Proof shell commandsProof shell commands
1364,54837
@node Script input to the shellScript input to the shell
1528,61881
@node Settings for matching various output from proof processSettings for matching various output from proof process
1593,64839
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1724,70624
@node Hooks and other settingsHooks and other settings
1939,80501
@node Goals Buffer SettingsGoals Buffer Settings
2020,83888
@node Splash Screen SettingsSplash Screen Settings
2097,86995
@node Global ConstantsGlobal Constants
2123,87753
@node Handling Multiple FilesHandling Multiple Files
2149,88594
@node Configuring Editing SyntaxConfiguring Editing Syntax
2301,96377
@node Configuring Font LockConfiguring Font Lock
2360,98498
@node Configuring TokensConfiguring Tokens
2432,101992
@node Writing More Lisp CodeWriting More Lisp Code
2470,103493
@node Default values for generic settingsDefault values for generic settings
2487,104138
@node Adding prover-specific configurationsAdding prover-specific configurations
2517,105221
@node Useful variablesUseful variables
2560,106503
@node Useful functions and macrosUseful functions and macros
2575,107002
@node Internals of Proof GeneralInternals of Proof General
2684,111218
@node Spans2712,112114
@node Proof General site configurationProof General site configuration
2724,112436
@node Configuration variable mechanismsConfiguration variable mechanisms
2804,115482
@node Global variablesGlobal variables
2925,120926
@node Proof script modeProof script mode
2995,123474
@node Proof shell modeProof shell mode
3254,135140
@node Debugging3684,152105
@node Plans and IdeasPlans and Ideas
3727,152981
@node Proof by pointing and similar featuresProof by pointing and similar features
3748,153703
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3786,155361
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3831,157586
@node Demonstration InstantiationsDemonstration Instantiations
3861,158617
@node demoisa-easy.el3877,159048
@node demoisa.el3940,161287
@node Function IndexFunction Index
4095,166272
@node Variable IndexVariable Index
4099,166348
@node Concept IndexConcept Index
4108,166527

generic/proof.el,0

generic/proof-autoloads.el,0

pgshell/pgshell.el,0

isar/isar-autotest.el,0

isar/interface-setup.el,0

hol98/hol98.el,0

demoisa/demoisa-easy.el,0

coq/coq-mmm.el,0

coq/coq-autotest.el,0

ccc/ccc.el,0

acl2/acl2.el,0