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,559
(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
(defun coq-build-abbrev-table-from-db 192,7323
(defun filter-state-preserving 209,7881
(defun filter-state-changing 214,8035
(defface coq-solve-tactics-face 221,8256
(defconst coq-solve-tactics-face 229,8513

coq/coq.el,6514
(defcustom coq-translate-to-v8 45,1299
(defun coq-build-prog-args 51,1479
(defcustom coq-compile-file-command 64,1859
(defcustom coq-use-makefile 72,2178
(defcustom coq-default-undo-limit 80,2401
(defconst coq-shell-init-cmd 85,2529
(defcustom coq-prog-env 97,2807
(defconst coq-shell-restart-cmd 105,3059
(defvar coq-shell-prompt-pattern 112,3319
(defvar coq-shell-cd 122,3712
(defvar coq-shell-abort-goal-regexp 126,3872
(defvar coq-shell-proof-completed-regexp 129,3998
(defvar coq-goal-regexp132,4150
(defun coq-library-directory 139,4264
(defcustom coq-tags 146,4444
(defconst coq-interrupt-regexp 151,4594
(defcustom coq-www-home-page 156,4715
(defvar coq-outline-regexp166,4886
(defvar coq-outline-heading-end-regexp 173,5100
(defvar coq-shell-outline-regexp 175,5154
(defvar coq-shell-outline-heading-end-regexp 176,5204
(defconst coq-kill-goal-command 181,5314
(defconst coq-forget-id-command 182,5357
(defconst coq-back-n-command 183,5404
(defconst coq-state-preserving-tactics-regexp 187,5548
(defconst coq-state-changing-commands-regexp189,5649
(defconst coq-state-preserving-commands-regexp 191,5756
(defconst coq-commands-regexp 193,5868
(defvar coq-retractable-instruct-regexp 195,5946
(defvar coq-non-retractable-instruct-regexp 197,6037
(defvar coq-keywords-section201,6177
(defvar coq-section-regexp 204,6271
(defun coq-set-undo-limit 241,7417
(defconst coq-keywords-decl-defn-regexp252,7856
(defun coq-proof-mode-p 256,8006
(defun coq-is-comment-or-proverprocp 267,8414
(defun coq-is-goalsave-p 269,8518
(defun coq-is-module-equal-p 270,8593
(defun coq-is-def-p 273,8789
(defun coq-is-decl-defn-p 275,8897
(defun coq-state-preserving-command-p 280,9064
(defun coq-command-p 283,9198
(defun coq-state-preserving-tactic-p 286,9298
(defun coq-state-changing-tactic-p 291,9446
(defun coq-state-changing-command-p 298,9680
(defun coq-section-or-module-start-p 305,10026
(defun build-list-id-from-string 314,10267
(defun coq-last-prompt-info 327,10797
(defun coq-last-prompt-info-safe 339,11338
(defvar coq-last-but-one-statenum 345,11595
(defvar coq-last-but-one-proofnum 351,11893
(defvar coq-last-but-one-proofstack 354,11991
(defun coq-get-span-statenum 357,12101
(defun coq-get-span-proofnum 362,12216
(defun coq-get-span-proofstack 367,12331
(defun coq-set-span-statenum 372,12475
(defun coq-get-span-goalcmd 377,12606
(defun coq-set-span-goalcmd 382,12720
(defun coq-set-span-proofnum 387,12850
(defun coq-set-span-proofstack 392,12981
(defun proof-last-locked-span 397,13141
(defun coq-set-state-infos 412,13745
(defun count-not-intersection 452,15824
(defun  coq-find-and-forget-v81 483,17078
(defun coq-find-and-forget-v80 511,18210
(defun coq-find-and-forget 606,22909
(defvar coq-current-goal 619,23449
(defun coq-goal-hyp 622,23514
(defun coq-state-preserving-p 635,23947
(defconst notation-print-kinds-table 649,24452
(defun coq-PrintScope 653,24620
(defun coq-guess-or-ask-for-string 671,25175
(defun coq-ask-do 685,25743
(defun coq-SearchIsos 694,26131
(defun coq-SearchConstant 700,26364
(defun coq-SearchRewrite 704,26457
(defun coq-SearchAbout 708,26555
(defun coq-Print 712,26647
(defun coq-About 716,26769
(defun coq-LocateConstant 720,26886
(defun coq-LocateLibrary 726,27021
(defun coq-addquotes 732,27171
(defun coq-LocateNotation 734,27219
(defun coq-Pwd 741,27418
(defun coq-Inspect 747,27550
(defun coq-PrintSection(751,27650
(defun coq-Print-implicit 755,27743
(defun coq-Check 760,27894
(defun coq-Show 765,28002
(defun coq-Compile 779,28445
(defun coq-guess-command-line 793,28765
(defun coq-mode-config 831,30481
(defvar coq-last-hybrid-pre-string 939,34435
(defun coq-hybrid-ouput-goals-response-p 942,34614
(defun coq-hybrid-ouput-goals-response 948,34872
(defun coq-shell-mode-config 969,35832
(defun coq-goals-mode-config 1014,37947
(defun coq-response-config 1021,38191
(defpacustom print-fully-explicit 1046,39016
(defpacustom print-implicit 1051,39164
(defpacustom print-coercions 1056,39330
(defpacustom print-match-wildcards 1061,39474
(defpacustom print-elim-types 1066,39654
(defpacustom printing-depth 1071,39820
(defpacustom undo-depth 1076,39981
(defpacustom time-commands 1081,40128
(defpacustom undo-limit 1085,40238
(defpacustom auto-compile-vos 1090,40340
(defun coq-maybe-compile-buffer 1119,41456
(defun coq-ancestors-of 1156,42990
(defun coq-all-ancestors-of 1179,43957
(defconst coq-require-command-regexp 1191,44350
(defun coq-process-require-command 1196,44559
(defun coq-included-children 1201,44686
(defun coq-process-file 1222,45525
(defun coq-preprocessing 1237,46064
(defun coq-fake-constant-markup 1252,46483
(defun coq-create-span-menu 1273,47289
(defconst module-kinds-table 1290,47788
(defconst modtype-kinds-table1294,47938
(defun coq-insert-section-or-module 1298,48067
(defconst reqkinds-kinds-table1321,48927
(defun coq-insert-requires 1326,49072
(defun coq-end-Section 1342,49578
(defun coq-insert-intros 1360,50162
(defun coq-insert-infoH-hook 1373,50687
(defun coq-insert-as 1377,50765
(defun coq-insert-match 1398,51514
(defun coq-insert-tactic 1430,52692
(defun coq-insert-tactical 1436,52931
(defun coq-insert-command 1442,53180
(defun coq-insert-term 1448,53424
(define-key coq-keymap 1454,53621
(define-key coq-keymap 1455,53679
(define-key coq-keymap 1456,53736
(define-key coq-keymap 1457,53805
(define-key coq-keymap 1458,53861
(define-key coq-keymap 1459,53910
(define-key coq-keymap 1460,53968
(define-key coq-keymap 1462,54029
(define-key coq-keymap 1463,54088
(define-key coq-keymap 1465,54152
(define-key coq-keymap 1466,54212
(define-key coq-keymap 1468,54268
(define-key coq-keymap 1469,54318
(define-key coq-keymap 1470,54368
(define-key coq-keymap 1471,54418
(define-key coq-keymap 1472,54472
(define-key coq-keymap 1473,54531
(defvar last-coq-error-location 1481,54662
(defun coq-get-last-error-location 1490,55061
(defun coq-highlight-error 1537,57446
(defvar coq-allow-highlight-error 1573,58749
(defun coq-decide-highlight-error 1579,59015
(defun coq-highlight-error-hook 1583,59137
(defun first-word-of-buffer 1594,59530
(defun coq-show-first-goal 1602,59733
(defvar coq-modeline-string2 1619,60428
(defvar coq-modeline-string1 1620,60472
(defvar coq-modeline-string0 1621,60515
(defun coq-build-subgoals-string 1622,60560
(defun coq-update-minor-mode-alist 1627,60728
(defun is-not-split-vertic 1653,61796
(defun optim-resp-windows 1662,62235

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,2831
(defun coq-read-directory 86,3304
(defun coq-extract-directories-from-args 110,4407
(defun coq-ask-prog-args 125,4959
(defun coq-ask-prog-name 147,6063
(defun coq-ask-insert-coq-prog-name 165,6818

coq/coq-syntax.el,2666
(defcustom coq-prog-name 13,421
(defvar coq-version-is-V8 34,1420
(defvar coq-version-is-V8-0 36,1499
(defvar coq-version-is-V8-1 43,1877
(defun coq-determine-version 52,2310
(defcustom coq-user-tactics-db 98,4216
(defcustom coq-user-commands-db 115,4729
(defcustom coq-user-tacticals-db 131,5248
(defcustom coq-user-solve-tactics-db 147,5769
(defcustom coq-user-reserved-db 165,6290
(defvar coq-tactics-db183,6821
(defvar coq-solve-tactics-db338,14889
(defvar coq-tacticals-db362,15736
(defvar coq-decl-db386,16623
(defvar coq-defn-db408,17841
(defvar coq-goal-starters-db461,21827
(defvar coq-other-commands-db488,23382
(defvar coq-commands-db612,32579
(defvar coq-terms-db619,32805
(defun coq-count-match 683,35457
(defun coq-goal-command-str-v80-p 702,36320
(defun coq-module-opening-p 725,37193
(defun coq-section-command-p 736,37609
(defun coq-goal-command-str-v81-p 740,37706
(defun coq-goal-command-p-v81 755,38375
(defun coq-goal-command-str-p 765,38715
(defun coq-goal-command-p 775,39081
(defvar coq-keywords-save-strict783,39393
(defvar coq-keywords-save792,39506
(defun coq-save-command-p 796,39584
(defvar coq-keywords-kill-goal 805,39878
(defvar coq-keywords-state-changing-misc-commands809,39969
(defvar coq-keywords-goal812,40094
(defvar coq-keywords-decl815,40177
(defvar coq-keywords-defn818,40251
(defvar coq-keywords-state-changing-commands822,40326
(defvar coq-keywords-state-preserving-commands831,40587
(defvar coq-keywords-commands836,40803
(defvar coq-solve-tactics841,40952
(defvar coq-tacticals845,41073
(defvar coq-reserved851,41212
(defvar coq-state-changing-tactics862,41541
(defvar coq-state-preserving-tactics865,41650
(defvar coq-tactics869,41764
(defvar coq-retractable-instruct872,41853
(defvar coq-non-retractable-instruct875,41963
(defvar coq-keywords879,42091
(defvar coq-symbols886,42259
(defvar coq-error-regexp 905,42472
(defvar coq-id 908,42700
(defvar coq-id-shy 909,42725
(defvar coq-ids 911,42779
(defun coq-first-abstr-regexp 913,42820
(defcustom coq-variable-highlight-enable 916,42915
(defvar coq-font-lock-terms922,43042
(defconst coq-save-command-regexp-strict943,44042
(defconst coq-save-command-regexp947,44209
(defconst coq-save-with-hole-regexp951,44362
(defconst coq-goal-command-regexp955,44521
(defconst coq-goal-with-hole-regexp958,44621
(defconst coq-decl-with-hole-regexp962,44754
(defconst coq-defn-with-hole-regexp969,45003
(defconst coq-with-with-hole-regexp979,45292
(defvar coq-font-lock-keywords-1985,45585
(defvar coq-font-lock-keywords 1011,46901
(defun coq-init-syntax-table 1013,46959
(defconst coq-generic-expression1042,47858

coq/coq-unicode-tokens.el,458
(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
(defcustom coq-fontsymb-properties 200,4998

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,1311
(defcustom isar-keywords-name 31,721
(defpgdefault completion-table 48,1244
(defcustom isar-web-page50,1297
(defun isar-strip-terminators 64,1647
(defun isar-markup-ml 77,2024
(defun isar-mode-config-set-variables 82,2159
(defun isar-shell-mode-config-set-variables 151,5143
(defun isar-configure-from-settings 241,8638
(defun isar-set-proof-find-theorems-command 244,8720
(defpacustom use-find-theorems-form 250,8905
(defun isar-remove-file 259,9109
(defun isar-shell-compute-new-files-list 269,9472
(define-derived-mode isar-shell-mode 285,9993
(define-derived-mode isar-response-mode 290,10116
(define-derived-mode isar-goals-mode 295,10298
(define-derived-mode isar-mode 300,10473
(defpgdefault menu-entries357,12497
(defpgdefault help-menu-entries 387,13780
(defun isar-count-undos 390,13856
(defun isar-find-and-forget 417,14970
(defun isar-goal-command-p 456,16550
(defun isar-global-save-command-p 461,16727
(defvar isar-current-goal 482,17588
(defun isar-state-preserving-p 485,17654
(defvar isar-shell-current-line-width 510,18851
(defun isar-shell-adjust-line-width 515,19043
(defun isar-preprocessing 540,19947
(defun isar-mode-config 552,20494
(defun isar-shell-mode-config 563,21052
(defun isar-response-mode-config 569,21249
(defun isar-goals-mode-config 578,21540

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,3576
(defconst isar-script-syntax-table-entries19,424
(defconst isar-script-syntax-table-alist43,826
(defun isar-init-syntax-table 52,1116
(defun isar-init-output-syntax-table 60,1363
(defconst isar-keyword-begin 76,1810
(defconst isar-keyword-end 77,1848
(defconst isar-keywords-theory-enclose79,1883
(defconst isar-keywords-theory84,2028
(defconst isar-keywords-save89,2173
(defconst isar-keywords-proof-enclose94,2302
(defconst isar-keywords-proof100,2484
(defconst isar-keywords-proof-context107,2689
(defconst isar-keywords-local-goal111,2803
(defconst isar-keywords-proper115,2915
(defconst isar-keywords-improper120,3048
(defconst isar-keywords-outline125,3194
(defconst isar-keywords-fume128,3259
(defconst isar-keywords-indent-open135,3477
(defconst isar-keywords-indent-close141,3661
(defconst isar-keywords-indent-enclose145,3766
(defun isar-regexp-simple-alt 154,3981
(defun isar-ids-to-regexp 174,4741
(defconst isar-ext-first 208,6147
(defconst isar-ext-rest 209,6214
(defconst isar-long-id-stuff 211,6286
(defconst isar-id 212,6360
(defconst isar-idx 213,6430
(defconst isar-string 215,6489
(defconst isar-any-command-regexp217,6549
(defconst isar-name-regexp221,6683
(defconst isar-improper-regexp227,6978
(defconst isar-save-command-regexp231,7126
(defconst isar-global-save-command-regexp234,7227
(defconst isar-goal-command-regexp237,7341
(defconst isar-local-goal-command-regexp240,7449
(defconst isar-comment-start 243,7562
(defconst isar-comment-end 244,7597
(defconst isar-comment-start-regexp 245,7630
(defconst isar-comment-end-regexp 246,7701
(defconst isar-string-start-regexp 248,7769
(defconst isar-string-end-regexp 249,7821
(defconst isar-antiq-regexp 254,7892
(defconst isar-nesting-regexp260,8045
(defun isar-nesting 263,8143
(defun isar-match-nesting 275,8564
(defface isabelle-class-name-face287,8895
(defface isabelle-tfree-name-face295,9078
(defface isabelle-tvar-name-face303,9267
(defface isabelle-free-name-face311,9455
(defface isabelle-bound-name-face319,9639
(defface isabelle-var-name-face327,9826
(defconst isabelle-class-name-face 335,10013
(defconst isabelle-tfree-name-face 336,10075
(defconst isabelle-tvar-name-face 337,10137
(defconst isabelle-free-name-face 338,10198
(defconst isabelle-bound-name-face 339,10259
(defconst isabelle-var-name-face 340,10321
(defvar isar-font-lock-keywords-1343,10383
(defun isar-output-flkprops 361,11393
(defun isar-output-flk 367,11645
(defvar isar-output-font-lock-keywords-1370,11754
(defun isar-strip-output-markup 391,12957
(defvar isar-goals-font-lock-keywords395,13093
(defconst isar-linear-undo 429,13772
(defconst isar-undo 431,13815
(defun isar-remove 433,13858
(defun isar-undos 436,13933
(defun isar-cannot-undo 440,14039
(defconst isar-theory-start-regexp443,14109
(defconst isar-end-regexp449,14274
(defconst isar-undo-fail-regexp453,14375
(defconst isar-undo-skip-regexp457,14479
(defconst isar-undo-ignore-regexp460,14600
(defconst isar-undo-remove-regexp463,14665
(defconst isar-any-entity-regexp471,14840
(defconst isar-named-entity-regexp476,15027
(defconst isar-unnamed-entity-regexp481,15204
(defconst isar-next-entity-regexps484,15306
(defconst isar-generic-expression492,15617
(defconst isar-indent-any-regexp503,15934
(defconst isar-indent-inner-regexp505,16027
(defconst isar-indent-enclose-regexp507,16093
(defconst isar-indent-open-regexp509,16209
(defconst isar-indent-close-regexp511,16319
(defconst isar-outline-regexp517,16456
(defconst isar-outline-heading-end-regexp 521,16609

isar/isar-unicode-tokens.el,825
(defconst isar-control-region-format-regexp20,505
(defconst isar-control-char-format-regexp 23,599
(defconst isar-control-char-format 26,695
(defconst isar-control-characters28,742
(defconst isar-control-regions37,997
(defcustom isar-fontsymb-properties 47,1322
(defconst isar-token-format 63,1833
(defconst isar-token-variant-format-regexp 67,1985
(defconst isar-greek-letters-tokens70,2100
(defconst isar-misc-letters-tokens106,2796
(defconst isar-symbols-tokens114,2947
(defun isar-try-char 383,9079
(defconst isar-symbols-tokens-fallbacks387,9223
(defconst isar-bold-nums-tokens 411,10052
(defun isar-map-letters 423,10308
(defconst isar-script-letters-tokens429,10457
(defconst isar-roman-letters-tokens434,10595
(defconst isar-fraktur-letters-tokens439,10731
(defconst isar-symbol-shortcuts482,12193

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,18085
(defun plastic-small-bar 522,18379
(defun plastic-large-bar 524,18468
(defun plastic-preprocessing 526,18606
(defun plastic-all-ctxt 577,20434
(defun plastic-send-one-undo 584,20612
(defun plastic-minibuf-cmd 594,20940
(defun plastic-minibuf 606,21419
(defun plastic-synchro 613,21625
(defun plastic-send-minibuf 618,21766
(defun plastic-had-error 626,22095
(defun plastic-reset-error 630,22270
(defun plastic-call-if-no-error 633,22409
(defun plastic-show-shell 638,22613
(define-key plastic-keymap 647,22875
(define-key plastic-keymap 648,22936
(define-key plastic-keymap 649,22997
(define-key plastic-keymap 650,23057
(define-key plastic-keymap 651,23116
(define-key plastic-keymap 652,23175
(defalias 'proof-toolbar-command proof-toolbar-command
662,23425
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
663,23476

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 32,1066
(defpgcustom unicode-tokens-enable 38,1246
(defpgcustom mmm-enable 44,1423
(defpgcustom script-indent 53,1777
(defconst proof-toolbar-entries-default58,1914
(defpgcustom toolbar-entries 85,3581
(defpgcustom prog-args 104,4314
(defpgcustom prog-env 117,4889
(defpgcustom favourites 126,5315
(defpgcustom menu-entries 131,5504
(defpgcustom help-menu-entries 138,5740
(defpgcustom keymap 145,6003
(defpgcustom completion-table 150,6175
(defpgcustom tags-program 161,6549
(defpgcustom use-holes 170,6933

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,1724
(defvar pg-pgip-last-seen-seq 54,1758
(defun pg-pgip-process-pgip 56,1794
(defun pg-pgip-process-msg 75,2725
(defvar pg-pgip-post-process-functions89,3295
(defun pg-pgip-post-process 99,3783
(defun pg-pgip-process-askpgip 115,4394
(defun pg-pgip-process-usespgip 121,4599
(defun pg-pgip-process-usespgml 125,4763
(defun pg-pgip-process-pgmlconfig 129,4927
(defun pg-pgip-process-proverinfo 145,5544
(defun pg-pgip-process-hasprefs 162,6209
(defun pg-pgip-haspref 176,6841
(defun pg-pgip-process-prefval 193,7543
(defun pg-pgip-process-guiconfig 220,8252
(defvar proof-assistant-idtables 227,8369
(defun pg-pgip-process-ids 230,8486
(defun pg-complete-idtable-symbol 256,9562
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
261,9654
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
262,9710
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
263,9766
(defun pg-pgip-process-idvalue 266,9824
(defun pg-pgip-process-menuadd 278,10160
(defun pg-pgip-process-menudel 281,10203
(defun pg-pgip-process-ready 290,10436
(defun pg-pgip-process-cleardisplay 293,10477
(defun pg-pgip-process-proofstate 307,10934
(defun pg-pgip-process-normalresponse 311,11011
(defun pg-pgip-process-errorresponse 315,11135
(defun pg-pgip-process-scriptinsert 319,11258
(defun pg-pgip-process-metainforesponse 324,11392
(defun pg-pgip-process-informfileloaded 333,11633
(defun pg-pgip-process-informfileretracted 339,11899
(defun pg-pgip-process-brokerstatus 352,12376
(defun pg-pgip-process-proveravailmsg 355,12424
(defun pg-pgip-process-newprovermsg 358,12474
(defun pg-pgip-process-proverstatusmsg 361,12522
(defvar pg-pgip-srcids 370,12769
(defun pg-pgip-process-newfile 374,12876
(defun pg-pgip-process-filestatus 390,13464
(defun pg-pgip-process-newobj 410,14119
(defun pg-pgip-process-delobj 413,14161
(defun pg-pgip-process-objectstatus 416,14203
(defun pg-pgip-process-parsescript 430,14558
(defun pg-pgip-get-pgiptype 453,15433
(defun pg-pgip-default-for 473,16226
(defun pg-pgip-subst-for 486,16621
(defun pg-pgip-interpret-value 498,16964
(defun pg-pgip-interpret-choice 516,17649
(defun pg-pgip-string-of-command 547,18666
(defconst pg-pgip-id564,19427
(defvar pg-pgip-refseq 570,19707
(defvar pg-pgip-refid 572,19804
(defvar pg-pgip-seq 575,19896
(defun pg-pgip-assemble-packet 577,19960
(defun pg-pgip-issue 595,20772
(defun pg-pgip-maybe-askpgip 612,21384
(defun pg-pgip-askprefs 618,21575
(defun pg-pgip-askids 622,21689
(defun pg-pgip-reset 635,21977
(defconst pg-pgip-start-element-regexp 666,22675
(defconst pg-pgip-end-element-regexp 667,22727

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-span.el,138
(defconst pg-beingprocessed 9,136
(defconst pg-processed 10,181
(defconst pg-outdated 11,216
(defun pg-edit-set-span-for-state 17,258

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,3203
(defmacro proof-maybe-save-point 31,807
(defun proof-maybe-follow-locked-end 41,1104
(defun proof-assert-next-command-interactive 55,1469
(defun proof-process-buffer 65,1840
(defun proof-undo-last-successful-command 79,2157
(defun proof-undo-and-delete-last-successful-command 84,2319
(defun proof-undo-last-successful-command-1 98,2882
(defun proof-retract-buffer 114,3447
(defun proof-retract-current-goal 123,3727
(defun proof-interrupt-process 142,4233
(defun proof-goto-command-start 169,5222
(defun proof-goto-command-end 192,6162
(defun proof-mouse-goto-point 213,6797
(defvar proof-minibuffer-history 229,7040
(defun proof-minibuffer-cmd 232,7135
(defun proof-frob-locked-end 276,8750
(defmacro proof-if-setting-configured 337,10678
(defmacro proof-define-assistant-command 345,10947
(defmacro proof-define-assistant-command-witharg 358,11402
(defun proof-issue-new-command 378,12225
(defun proof-cd-sync 422,13668
(defun proof-electric-terminator-enable 476,15388
(defun proof-electric-term-incomment-fn 484,15690
(defun proof-process-electric-terminator 504,16477
(defun proof-electric-terminator 529,17542
(defun proof-add-completions 551,18188
(defun proof-script-complete 575,19048
(defun pg-insert-last-output-as-comment 589,19434
(defun pg-copy-span-contents 603,19832
(defun pg-numth-span-higher-or-lower 620,20390
(defun pg-control-span-of 646,21136
(defun pg-move-span-contents 652,21340
(defun pg-fixup-children-spans 704,23520
(defun pg-move-region-down 714,23783
(defun pg-move-region-up 723,24076
(defun proof-forward-command 753,24914
(defun proof-backward-command 774,25635
(defun pg-pos-for-event 796,25986
(defun pg-span-for-event 802,26207
(defun pg-span-context-menu 806,26351
(defun pg-toggle-visibility 821,26806
(defun pg-create-in-span-context-menu 831,27128
(defun pg-span-undo 861,28330
(defun pg-goals-buffers-hint 907,29740
(defun pg-slow-fontify-tracing-hint 911,29922
(defun pg-response-buffers-hint 915,30093
(defun pg-jump-to-end-hint 925,30455
(defun pg-processing-complete-hint 929,30586
(defun pg-next-error-hint 946,31285
(defun pg-hint 951,31437
(defun pg-identifier-under-mouse-query 967,32027
(defun pg-identifier-near-point-query 976,32270
(defun proof-query-identifier 990,32773
(defun pg-identifier-query 994,32883
(defun proof-imenu-enable 1022,33856
(defvar pg-input-ring 1053,34902
(defvar pg-input-ring-index 1056,34959
(defvar pg-stored-incomplete-input 1059,35031
(defun pg-previous-input 1062,35134
(defun pg-next-input 1076,35591
(defun pg-delete-input 1081,35713
(defun pg-get-old-input 1094,36051
(defun pg-restore-input 1108,36442
(defun pg-search-start 1119,36732
(defun pg-regexp-arg 1131,37224
(defun pg-search-arg 1143,37672
(defun pg-previous-matching-input-string-position 1157,38089
(defun pg-previous-matching-input 1184,39254
(defun pg-next-matching-input 1203,40104
(defvar pg-matching-input-from-input-string 1211,40487
(defun pg-previous-matching-input-from-input 1215,40601
(defun pg-next-matching-input-from-input 1233,41366
(defun pg-add-to-input-history 1244,41745
(defun pg-remove-from-input-history 1256,42198
(defun  pg-clear-input-ring 1267,42580

generic/pg-vars.el,1106
(defvar proof-assistant-cusgrp 20,380
(defvar proof-assistant-internals-cusgrp 26,642
(defvar proof-assistant 32,913
(defvar proof-assistant-symbol 37,1135
(defvar proof-mode-for-shell 50,1679
(defvar proof-mode-for-response 55,1871
(defvar proof-mode-for-goals 60,2098
(defvar proof-mode-for-script 65,2288
(defvar proof-ready-for-assistant-hook 70,2466
(defvar proof-shell-busy 80,2753
(defvar proof-included-files-list 85,2909
(defvar proof-script-buffer 107,3922
(defvar proof-previous-script-buffer 110,4014
(defvar proof-shell-buffer 114,4185
(defvar proof-goals-buffer 117,4271
(defvar proof-response-buffer 120,4326
(defvar proof-trace-buffer 123,4387
(defvar proof-thms-buffer 127,4541
(defvar proof-shell-error-or-interrupt-seen 131,4696
(defvar pg-response-next-error 136,4920
(defvar proof-shell-proof-completed 139,5027
(defvar proof-terminal-string 151,5571
(defvar proof-shell-last-output 161,5761
(defvar proof-assistant-settings 165,5902
(defvar pg-tracing-slow-mode 173,6351
(defvar proof-nesting-depth 176,6440
(defvar proof-last-theorem-dependencies 183,6675

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,11039
(defgroup proof-user-options 84,2964
(defun proof-set-value 92,3143
(defcustom proof-electric-terminator-enable 125,4266
(defcustom proof-toolbar-enable 137,4798
(defcustom proof-imenu-enable 143,4971
(defcustom pg-show-hints 149,5142
(defcustom proof-trace-output-slow-catchup 155,5337
(defcustom proof-strict-state-preserving 165,5834
(defcustom proof-strict-read-only 178,6443
(defcustom proof-allow-undo-in-read-only 190,6956
(defcustom proof-three-window-enable 198,7289
(defcustom proof-multiple-frames-enable 217,8039
(defcustom proof-delete-empty-windows 226,8372
(defcustom proof-shrink-windows-tofit 237,8903
(defcustom proof-auto-raise-buffers 244,9175
(defcustom proof-colour-locked 251,9410
(defcustom proof-query-file-save-when-activating-scripting259,9660
(defcustom proof-one-command-per-line275,10380
(defcustom proof-prog-name-ask282,10607
(defcustom proof-prog-name-guess288,10767
(defcustom proof-tidy-response296,11032
(defcustom proof-keep-response-history310,11495
(defcustom pg-input-ring-size 320,11883
(defcustom proof-general-debug 325,12035
(defcustom proof-use-parser-cache 336,12444
(defcustom proof-follow-mode 346,12739
(defcustom proof-auto-action-when-deactivating-scripting 370,13916
(defcustom proof-script-command-separator 393,14865
(defcustom proof-rsh-command 401,15157
(defcustom proof-disappearing-proofs 417,15707
(defcustom proof-full-annotation 422,15868
(defgroup proof-faces 453,16723
(defconst pg-defface-window-systems460,16905
(defmacro proof-face-specs 473,17458
(defface proof-queue-face488,17910
(defface proof-locked-face496,18188
(defface proof-declaration-name-face506,18509
(defface proof-tacticals-name-face515,18795
(defface proof-tactics-name-face524,19057
(defface proof-error-face533,19322
(defface proof-warning-face541,19512
(defface proof-eager-annotation-face550,19769
(defface proof-debug-message-face558,19987
(defface proof-boring-face566,20186
(defface proof-mouse-highlight-face574,20378
(defface proof-highlight-dependent-face582,20574
(defface proof-highlight-dependency-face590,20783
(defface proof-active-area-face598,20980
(defconst proof-face-compat-doc 607,21370
(defconst proof-queue-face 608,21450
(defconst proof-locked-face 609,21518
(defconst proof-declaration-name-face 610,21588
(defconst proof-tacticals-name-face 611,21678
(defconst proof-tactics-name-face 612,21764
(defconst proof-error-face 613,21846
(defconst proof-warning-face 614,21914
(defconst proof-eager-annotation-face 615,21986
(defconst proof-debug-message-face 616,22076
(defconst proof-boring-face 617,22160
(defconst proof-mouse-highlight-face 618,22230
(defconst proof-highlight-dependent-face 619,22318
(defconst proof-highlight-dependency-face 620,22414
(defconst proof-active-area-face 621,22512
(defgroup prover-config 634,22656
(defcustom proof-guess-command-line 676,23985
(defcustom proof-assistant-home-page 691,24480
(defcustom proof-context-command 697,24650
(defcustom proof-info-command 702,24784
(defcustom proof-showproof-command 709,25055
(defcustom proof-goal-command 714,25191
(defcustom proof-save-command 722,25488
(defcustom proof-find-theorems-command 730,25797
(defcustom proof-query-identifier-command 737,26105
(defcustom proof-assistant-true-value 751,26794
(defcustom proof-assistant-false-value 757,26984
(defcustom proof-assistant-format-int-fn 763,27178
(defcustom proof-assistant-format-string-fn 770,27427
(defcustom proof-assistant-setting-format 777,27694
(defgroup proof-script 799,28389
(defcustom proof-terminal-char 804,28519
(defcustom proof-electric-terminator-noterminator 814,28906
(defcustom proof-script-sexp-commands 819,29078
(defcustom proof-script-command-end-regexp 830,29535
(defcustom proof-script-command-start-regexp 848,30354
(defcustom proof-script-use-old-parser 859,30815
(defcustom proof-script-integral-proofs 871,31301
(defcustom proof-script-fly-past-comments 886,31957
(defcustom proof-script-parse-function 891,32128
(defcustom proof-script-comment-start 909,32771
(defcustom proof-script-comment-start-regexp 920,33208
(defcustom proof-script-comment-end 928,33527
(defcustom proof-script-comment-end-regexp 940,33949
(defcustom proof-string-start-regexp 948,34260
(defcustom proof-string-end-regexp 953,34425
(defcustom proof-case-fold-search 958,34586
(defcustom proof-save-command-regexp 967,34998
(defcustom proof-save-with-hole-regexp 972,35108
(defcustom proof-save-with-hole-result 984,35562
(defcustom proof-goal-command-regexp 994,36010
(defcustom proof-goal-with-hole-regexp 1003,36398
(defcustom proof-goal-with-hole-result 1015,36841
(defcustom proof-non-undoables-regexp 1024,37225
(defcustom proof-nested-undo-regexp 1035,37680
(defcustom proof-ignore-for-undo-count 1051,38392
(defcustom proof-script-next-entity-regexps 1059,38695
(defcustom proof-script-find-next-entity-fn1103,40436
(defcustom proof-script-imenu-generic-expression 1123,41276
(defcustom proof-goal-command-p 1131,41615
(defcustom proof-really-save-command-p 1142,42106
(defcustom proof-completed-proof-behaviour 1151,42413
(defcustom proof-count-undos-fn 1179,43769
(defconst proof-no-command 1191,44318
(defcustom proof-find-and-forget-fn 1196,44525
(defcustom proof-forget-id-command 1213,45239
(defcustom pg-topterm-goalhyplit-fn 1223,45597
(defcustom proof-kill-goal-command 1235,46132
(defcustom proof-undo-n-times-cmd 1249,46635
(defcustom proof-nested-goals-history-p 1263,47183
(defcustom proof-state-preserving-p 1272,47520
(defcustom proof-activate-scripting-hook 1282,47992
(defcustom proof-deactivate-scripting-hook 1301,48773
(defcustom proof-indent 1314,49138
(defcustom proof-indent-hang 1319,49245
(defcustom proof-indent-enclose-offset 1324,49371
(defcustom proof-indent-open-offset 1329,49513
(defcustom proof-indent-close-offset 1334,49650
(defcustom proof-indent-any-regexp 1339,49788
(defcustom proof-indent-inner-regexp 1344,49948
(defcustom proof-indent-enclose-regexp 1349,50102
(defcustom proof-indent-open-regexp 1354,50256
(defcustom proof-indent-close-regexp 1359,50408
(defcustom proof-script-font-lock-keywords 1365,50562
(defcustom proof-script-syntax-table-entries 1373,50879
(defcustom proof-script-span-context-menu-extensions 1391,51276
(defgroup proof-shell 1417,52036
(defcustom proof-prog-name 1427,52207
(defcustom proof-shell-auto-terminate-commands 1438,52627
(defcustom proof-shell-pre-sync-init-cmd 1447,53028
(defcustom proof-shell-init-cmd 1461,53586
(defcustom proof-shell-init-hook 1473,54115
(defcustom proof-shell-restart-cmd 1478,54254
(defcustom proof-shell-quit-cmd 1483,54409
(defcustom proof-shell-quit-timeout 1488,54576
(defcustom proof-shell-cd-cmd 1498,55026
(defcustom proof-shell-start-silent-cmd 1515,55697
(defcustom proof-shell-stop-silent-cmd 1524,56073
(defcustom proof-shell-silent-threshold 1533,56408
(defcustom  proof-shell-inform-file-processed-cmd 1541,56742
(defcustom  proof-shell-inform-file-retracted-cmd 1562,57670
(defcustom proof-auto-multiple-files 1590,58942
(defcustom proof-cannot-reopen-processed-files 1605,59663
(defcustom proof-shell-require-command-regexp 1619,60329
(defcustom proof-done-advancing-require-function 1630,60791
(defcustom proof-shell-quiet-errors 1636,61026
(defcustom proof-shell-prompt-pattern 1649,61360
(defcustom proof-shell-wakeup-char 1659,61781
(defcustom proof-shell-annotated-prompt-regexp 1665,62012
(defcustom proof-shell-abort-goal-regexp 1681,62648
(defcustom proof-shell-error-regexp 1686,62783
(defcustom proof-shell-truncate-before-error 1706,63583
(defcustom pg-next-error-regexp 1720,64122
(defcustom pg-next-error-filename-regexp 1735,64731
(defcustom pg-next-error-extract-filename 1759,65764
(defcustom proof-shell-interrupt-regexp 1766,66007
(defcustom proof-shell-proof-completed-regexp 1780,66602
(defcustom proof-shell-clear-response-regexp 1793,67110
(defcustom proof-shell-clear-goals-regexp 1800,67409
(defcustom proof-shell-start-goals-regexp 1807,67702
(defcustom proof-shell-end-goals-regexp 1815,68069
(defcustom proof-shell-eager-annotation-start 1821,68313
(defcustom proof-shell-eager-annotation-start-length 1844,69332
(defcustom proof-shell-eager-annotation-end 1855,69758
(defcustom proof-shell-strip-output-markup 1871,70433
(defcustom proof-shell-assumption-regexp 1880,70819
(defcustom proof-shell-process-file 1890,71223
(defcustom proof-shell-retract-files-regexp 1912,72179
(defcustom proof-shell-compute-new-files-list 1921,72515
(defcustom pg-use-specials-for-fontify 1933,73063
(defcustom pg-special-char-regexp 1941,73411
(defcustom proof-shell-set-elisp-variable-regexp 1947,73556
(defcustom proof-shell-match-pgip-cmd 1980,75069
(defcustom proof-shell-issue-pgip-cmd 1989,75398
(defcustom proof-use-pgip-askprefs 1994,75563
(defcustom proof-shell-query-dependencies-cmd 2002,75910
(defcustom proof-shell-theorem-dependency-list-regexp 2009,76170
(defcustom proof-shell-theorem-dependency-list-split 2025,76830
(defcustom proof-shell-show-dependency-cmd 2034,77253
(defcustom proof-shell-trace-output-regexp 2056,78159
(defcustom proof-shell-thms-output-regexp 2070,78617
(defcustom proof-tokens-activate-command 2083,79000
(defcustom proof-tokens-deactivate-command 2090,79241
(defcustom proof-tokens-extra-modes 2097,79488
(defcustom proof-shell-unicode 2112,79995
(defcustom proof-shell-filename-escapes 2120,80315
(defcustom proof-shell-process-connection-type2137,80995
(defcustom proof-shell-strip-crs-from-input 2160,82041
(defcustom proof-shell-strip-crs-from-output 2172,82526
(defcustom proof-shell-insert-hook 2180,82894
(defcustom proof-shell-handle-delayed-output-hook2218,84754
(defcustom proof-shell-handle-error-or-interrupt-hook2224,84969
(defcustom proof-shell-pre-interrupt-hook2242,85722
(defcustom proof-shell-process-output-system-specific 2250,85993
(defcustom proof-state-change-hook 2269,86857
(defcustom proof-shell-syntax-table-entries 2279,87238
(defgroup proof-goals 2297,87610
(defcustom pg-subterm-first-special-char 2302,87731
(defcustom pg-subterm-anns-use-stack 2310,88043
(defcustom pg-goals-change-goal 2319,88342
(defcustom pbp-goal-command 2324,88458
(defcustom pbp-hyp-command 2329,88614
(defcustom pg-subterm-help-cmd 2334,88776
(defcustom pg-goals-error-regexp 2341,89012
(defcustom proof-shell-result-start 2346,89172
(defcustom proof-shell-result-end 2352,89406
(defcustom pg-subterm-start-char 2358,89619
(defcustom pg-subterm-sep-char 2372,90205
(defcustom pg-subterm-end-char 2378,90384
(defcustom pg-topterm-regexp 2384,90541
(defcustom proof-goals-font-lock-keywords 2399,91141
(defcustom proof-resp-font-lock-keywords 2407,91468
(defcustom pg-before-fontify-output-hook 2415,91797
(defcustom pg-after-fontify-output-hook 2423,92158
(defcustom proof-general-name 2435,92407
(defcustom proof-general-home-page2440,92564
(defcustom proof-unnamed-theorem-name2446,92724
(defcustom proof-universal-keys2452,92908

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-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 134,5425
(defvar proof-menu-favourites 143,5613
(defun proof-menu-define-specific 147,5735
(defun proof-assistant-menu-update 185,6753
(defvar proof-help-menu199,7186
(defvar proof-show-hide-menu207,7464
(defvar proof-buffer-menu216,7777
(defun proof-retract-on-edit-toggle 277,10007
(defun proof-keep-response-history 284,10185
(defconst proof-quick-opts-menu292,10495
(defun proof-quick-opts-vars 459,17446
(defun proof-quick-opts-changed-from-defaults-p 487,18282
(defun proof-quick-opts-changed-from-saved-p 491,18387
(defun proof-quick-opts-save 502,18739
(defun proof-quick-opts-reset 507,18907
(defconst proof-config-menu519,19175
(defconst proof-advanced-menu526,19354
(defvar proof-menu 539,19789
(defun proof-main-menu 548,20073
(defun proof-aux-menu 559,20339
(defun proof-menu-define-favourites-menu 575,20686
(defun proof-def-favourite 595,21342
(defvar proof-make-favourite-cmd-history 618,22317
(defvar proof-make-favourite-menu-history 621,22402
(defun proof-save-favourites 624,22488
(defun proof-del-favourite 629,22636
(defun proof-read-favourite 646,23197
(defun proof-add-favourite 670,23981
(defvar proof-menu-settings 697,25032
(defun proof-menu-define-settings-menu 700,25106
(defun proof-menu-entry-name 733,26238
(defun proof-menu-entry-for-setting 743,26580
(defun proof-settings-vars 762,27115
(defun proof-settings-changed-from-defaults-p 767,27292
(defun proof-settings-changed-from-saved-p 771,27398
(defun proof-settings-save 775,27501
(defun proof-settings-reset 780,27668
(defun proof-defpacustom-fn 787,27913
(defmacro defpacustom 853,30205
(defun proof-assistant-invisible-command-ifposs 868,31032
(defun proof-maybe-askprefs 890,32007
(defun proof-assistant-settings-cmd 896,32201
(defvar proof-assistant-format-table 913,32861
(defun proof-assistant-format-bool 921,33230
(defun proof-assistant-format-int 924,33343
(defun proof-assistant-format-string 927,33435
(defun proof-assistant-format 930,33533

generic/proof-mmm.el,70
(defun proof-mmm-set-global 41,1517
(defun proof-mmm-enable 56,2058

generic/proof-script.el,5746
(defvar proof-element-counters 28,714
(deflocal proof-active-buffer-fake-minor-mode 34,854
(deflocal proof-script-buffer-file-name 37,980
(deflocal pg-script-portions 44,1390
(defun proof-next-element-count 54,1626
(defun proof-element-id 63,1961
(defun proof-next-element-id 67,2130
(deflocal proof-script-last-entity 81,2447
(defun proof-script-find-next-entity 88,2727
(deflocal proof-locked-span 164,5469
(deflocal proof-queue-span 171,5735
(deflocal proof-overlay-arrow 180,6221
(defun proof-span-give-warning 186,6348
(defun proof-span-read-only 190,6462
(defun proof-strict-read-only 199,6894
(defsubst proof-set-locked-endpoints 237,8625
(defsubst proof-detach-queue 249,9018
(defsubst proof-detach-locked 254,9158
(defsubst proof-set-queue-start 261,9384
(defsubst proof-set-locked-end 265,9510
(defsubst proof-set-queue-end 277,9980
(defun proof-init-segmentation 288,10277
(defun proof-colour-locked 322,11775
(defun proof-restart-buffers 332,12122
(defun proof-script-buffers-with-spans 353,12950
(defun proof-script-remove-all-spans-and-deactivate 363,13306
(defun proof-script-clear-queue-spans 367,13494
(defun proof-script-delete-spans 377,13936
(defun proof-unprocessed-begin 391,14215
(defun proof-script-end 399,14469
(defun proof-queue-or-locked-end 408,14770
(defun proof-locked-end 423,15448
(defun proof-locked-region-full-p 440,15833
(defun proof-locked-region-empty-p 449,16105
(defun proof-only-whitespace-to-locked-region-p 453,16255
(defun proof-in-locked-region-p 466,16891
(defun proof-goto-end-of-locked 478,17154
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 495,17913
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 506,18394
(defun proof-end-of-locked-visible-p 520,19016
(defun proof-goto-end-of-queue-or-locked-if-not-visible 529,19467
(defvar pg-idioms 548,20117
(defvar pg-visibility-specs 551,20213
(defconst pg-default-invisibility-spec 556,20420
(defun pg-clear-script-portions 560,20560
(defun pg-add-script-element 567,20808
(defun pg-remove-script-element 570,20884
(defsubst pg-visname 578,21178
(defun pg-add-element 582,21323
(defun pg-open-invisible-span 616,22952
(defun pg-remove-element 627,23315
(defun pg-make-element-invisible 634,23585
(defun pg-make-element-visible 640,23829
(defun pg-toggle-element-visibility 644,23972
(defun pg-redisplay-for-gnuemacs 651,24259
(defun pg-show-all-portions 655,24405
(defun pg-show-all-proofs 673,25076
(defun pg-hide-all-proofs 678,25204
(defun pg-add-proof-element 683,25335
(defun pg-span-name 697,25955
(defvar pg-span-context-menu-keymap718,26662
(defun pg-set-span-helphighlights 726,26915
(defun proof-complete-buffer-atomic 768,28442
(defun proof-register-possibly-new-processed-file 809,30357
(defun proof-inform-prover-file-retracted 860,32485
(defun proof-auto-retract-dependencies 879,33271
(defun proof-unregister-buffer-file-name 933,35811
(defun proof-protected-process-or-retract 979,37634
(defun proof-deactivate-scripting-auto 1006,38804
(defun proof-deactivate-scripting 1015,39162
(defun proof-activate-scripting 1148,44435
(defun proof-toggle-active-scripting 1268,49813
(defun proof-done-advancing 1309,51174
(defun proof-done-advancing-comment 1404,54822
(defun proof-done-advancing-save 1423,55564
(defun proof-make-goalsave 1516,59179
(defun proof-get-name-from-goal 1531,59922
(defun proof-done-advancing-autosave 1550,60948
(defun proof-done-advancing-other 1615,63494
(defun proof-segment-up-to-parser 1643,64453
(defun proof-script-generic-parse-find-comment-end 1707,66537
(defun proof-script-generic-parse-cmdend 1716,66953
(defun proof-script-generic-parse-cmdstart 1741,67848
(defun proof-script-generic-parse-sexp 1804,70556
(defun proof-cmdstart-add-segment-for-cmd 1828,71492
(defun proof-segment-up-to-cmdstart 1880,73705
(defun proof-segment-up-to-cmdend 1941,76065
(defun proof-semis-to-vanillas 2013,78744
(defun proof-script-new-command-advance 2052,80073
(defun proof-script-next-command-advance 2094,81814
(defun proof-assert-until-point-interactive 2106,82255
(defun proof-assert-until-point 2135,83380
(defun proof-assert-next-command2188,85824
(defun proof-retract-before-change 2236,88074
(defun proof-inside-comment 2245,88412
(defun proof-goto-point 2250,88543
(defun proof-insert-pbp-command 2268,89084
(defun proof-insert-sendback-command 2282,89553
(defun proof-done-retracting 2308,90457
(defun proof-setup-retract-action 2343,91907
(defun proof-last-goal-or-goalsave 2353,92390
(defun proof-retract-target 2376,93230
(defun proof-retract-until-point-interactive 2461,96871
(defun proof-retract-until-point 2469,97256
(define-derived-mode proof-mode 2512,99005
(defun proof-script-set-visited-file-name 2549,100374
(defun proof-script-set-buffer-hooks 2573,101376
(defun proof-script-kill-buffer-fn 2581,101794
(defun proof-config-done-related 2613,103108
(defun proof-generic-goal-command-p 2681,105636
(defun proof-generic-state-preserving-p 2686,105848
(defun proof-generic-count-undos 2695,106365
(defun proof-generic-find-and-forget 2724,107395
(defconst proof-script-important-settings2775,109220
(defun proof-config-done 2790,109773
(defun proof-setup-parsing-mechanism 2859,112079
(defun proof-setup-imenu 2903,113932
(defun proof-setup-func-menu 2920,114537
(deflocal proof-segment-up-to-cache 2982,116763
(deflocal proof-segment-up-to-cache-start 2983,116804
(deflocal proof-last-edited-low-watermark 2984,116849
(defun proof-segment-up-to-using-cache 2994,117337
(defun proof-segment-cache-contents-for 3020,118380
(defun proof-script-after-change-function 3032,118751
(defun proof-script-set-after-change-functions 3038,118991

generic/proof-shell.el,3213
(defvar proof-marker 28,650
(defvar proof-action-list 31,747
(defvar proof-shell-silent 39,923
(defvar proof-shell-last-prompt 46,1214
(defvar proof-shell-last-output-kind 50,1385
(defvar proof-shell-delayed-output 71,2207
(defvar proof-shell-delayed-output-kind 74,2328
(defcustom proof-shell-active-scripting-indicator83,2531
(defun proof-shell-ready-prover 133,3922
(defun proof-shell-live-buffer 147,4462
(defun proof-shell-available-p 154,4697
(defun proof-grab-lock 160,4920
(defun proof-release-lock 172,5479
(defcustom proof-shell-fiddle-frames 187,5878
(defun proof-shell-set-text-representation 193,6101
(defun proof-shell-start 204,6563
(defvar proof-shell-kill-function-hooks 410,13915
(defun proof-shell-kill-function 413,14013
(defun proof-shell-clear-state 502,17816
(defun proof-shell-exit 517,18259
(defun proof-shell-bail-out 529,18704
(defun proof-shell-restart 538,19181
(defvar proof-shell-no-response-display 580,20565
(defvar proof-shell-urgent-message-marker 583,20669
(defvar proof-shell-urgent-message-scanner 586,20790
(defun proof-shell-handle-output 590,20917
(defun proof-shell-handle-delayed-output 625,22236
(defsubst proof-shell-strip-output-markup 647,23177
(defvar proof-shell-no-error-display 658,23500
(defun proof-shell-handle-error 664,23704
(defun proof-shell-handle-interrupt 680,24437
(defun proof-shell-error-or-interrupt-action 694,25050
(defun proof-goals-pos 720,26245
(defun proof-pbp-focus-on-first-goal 725,26450
(defsubst proof-shell-string-match-safe 737,26877
(defun proof-shell-process-output 742,27045
(defun proof-shell-insert 855,31762
(defun proof-shell-command-queue-item 908,33863
(defun proof-shell-set-silent 913,34020
(defun proof-shell-start-silent-item 919,34239
(defun proof-shell-clear-silent 925,34431
(defun proof-shell-stop-silent-item 931,34653
(defun proof-shell-should-be-silent 938,34925
(defun proof-append-alist 952,35519
(defun proof-start-queue 1011,37756
(defun proof-extend-queue 1022,38105
(defun proof-shell-exec-loop 1031,38484
(defun proof-shell-insert-loopback-cmd 1096,41072
(defun proof-shell-message 1124,42398
(defun proof-shell-process-urgent-message 1131,42651
(defun proof-shell-strip-eager-annotations 1261,47788
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1272,48124
(defun proof-shell-minibuffer-urgent-interactive-input 1274,48194
(defun proof-shell-process-urgent-messages 1284,48553
(defun proof-shell-filter 1358,51657
(defun proof-shell-filter-process-output 1514,58021
(defvar pg-last-tracing-output-time 1567,60075
(defconst pg-slow-mode-duration 1570,60181
(defconst pg-fast-tracing-mode-threshold 1573,60263
(defvar pg-tracing-cleanup-timer 1576,60391
(defun pg-tracing-tight-loop 1578,60430
(defun pg-finish-tracing-display 1621,62148
(defun proof-shell-wait 1643,62518
(defun proof-done-invisible 1662,63427
(defun proof-shell-invisible-command 1668,63599
(defun proof-shell-invisible-cmd-get-result 1702,64864
(defun proof-shell-invisible-command-invisible-result 1720,65560
(define-derived-mode proof-shell-mode 1739,65990
(defconst proof-shell-important-settings1797,68288
(defun proof-shell-config-done 1803,68403

generic/proof-site.el,504
(defconst proof-assistant-table-default22,727
(defconst proof-general-short-version 60,2143
(defconst proof-general-version-year 66,2331
(defgroup proof-general 73,2484
(defgroup proof-general-internals 78,2592
(defun proof-home-directory-fn 91,2980
(defcustom proof-home-directory102,3351
(defcustom proof-images-directory111,3718
(defcustom proof-info-directory117,3920
(defcustom proof-assistant-table145,5107
(defcustom proof-assistants 180,6223
(defun proof-ready-for-assistant 208,7368

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,981
(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,1086
(defun proof-re-search-forward-region 46,1509
(defun proof-search-forward 59,2004
(defun proof-replace-regexp-in-string 65,2256
(defun proof-re-search-forward 71,2510
(defun proof-re-search-backward 77,2771
(defun proof-string-match 83,3035
(defun proof-string-match-safe 89,3267
(defun proof-stringfn-match 93,3472
(defun proof-looking-at 100,3732
(defun proof-looking-at-safe 106,3922
(defun proof-looking-at-syntactic-context 110,4062
(defsubst proof-replace-string 122,4425
(defsubst proof-replace-regexp 127,4629
(defsubst proof-replace-regexp-nocasefold 132,4838
(defvar proof-id 140,5120
(defun proof-ids 146,5340
(defun proof-zap-commas 159,5896
(defun proof-format 175,6392
(defun proof-format-filename 194,7031
(defun proof-insert 241,8431
(defun proof-splice-separator 278,9447

generic/proof-toolbar.el,2280
(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,3470
(defalias 'proof-toolbar-undo proof-toolbar-undo
142,4450
(defun proof-toolbar-undo-enable-p 144,4518
(defalias 'proof-toolbar-delete proof-toolbar-delete
151,4676
(defun proof-toolbar-delete-enable-p 153,4757
(defalias 'proof-toolbar-home proof-toolbar-home
161,4939
(defalias 'proof-toolbar-next proof-toolbar-next
165,5006
(defun proof-toolbar-next-enable-p 167,5077
(defalias 'proof-toolbar-goto proof-toolbar-goto
173,5193
(defun proof-toolbar-goto-enable-p 175,5243
(defalias 'proof-toolbar-retract proof-toolbar-retract
180,5328
(defun proof-toolbar-retract-enable-p 182,5385
(defalias 'proof-toolbar-use proof-toolbar-use
188,5504
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
189,5556
(defalias 'proof-toolbar-restart proof-toolbar-restart
193,5637
(defalias 'proof-toolbar-goal proof-toolbar-goal
197,5702
(defalias 'proof-toolbar-qed proof-toolbar-qed
201,5760
(defun proof-toolbar-qed-enable-p 203,5809
(defalias 'proof-toolbar-state proof-toolbar-state
211,5971
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
212,6014
(defalias 'proof-toolbar-context proof-toolbar-context
216,6093
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
217,6139
(defalias 'proof-toolbar-info proof-toolbar-info
221,6217
(defalias 'proof-toolbar-command proof-toolbar-command
225,6273
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
226,6329
(defun proof-toolbar-help 230,6408
(defalias 'proof-toolbar-find proof-toolbar-find
236,6489
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
237,6541
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
241,6639
(defun proof-toolbar-visibility-enable-p 243,6699
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
248,6813
(defun proof-toolbar-interrupt-enable-p 249,6874
(defun proof-toolbar-scripting-menu 257,7027

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-utils.el,1873
(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 765,29445
(defun pg-custom-reset-vars 783,30168
(defun proof-locate-executable 796,30505

lib/bufhist.el,1099
(defun bufhist-ring-update 32,1227
(defgroup bufhist 41,1549
(defcustom bufhist-ring-size 45,1630
(defvar bufhist-ring 50,1741
(defvar bufhist-ring-pos 53,1815
(defvar bufhist-lastswitch-modified-tick 56,1894
(defvar bufhist-read-only-history 59,2000
(defvar bufhist-saved-mode-line-format 62,2071
(defun bufhist-mode-line-format-entry 65,2172
(defun bufhist-get-buffer-contents 97,3448
(defun bufhist-restore-buffer-contents 109,3932
(defun bufhist-checkpoint 117,4219
(defun bufhist-erase-buffer 125,4588
(defun bufhist-checkpoint-and-erase 135,4933
(defun bufhist-switch-to-index 141,5119
(defun bufhist-first 180,6723
(defun bufhist-last 185,6882
(defun bufhist-prev 190,7028
(defun bufhist-next 198,7251
(defun bufhist-delete 203,7391
(defun bufhist-clear 215,7934
(defun bufhist-init 230,8330
(defun bufhist-exit 255,9267
(defun bufhist-set-readwrite 265,9531
(defun bufhist-before-change-function 280,10151
(defun bufhist-make-buttons 292,10567
(defconst bufhist-minor-mode-map310,11006
(define-minor-mode bufhist-mode322,11468
(defun bufhist-toggle-fn 342,12253

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,75
(defconst pg-dev-lisp-font-lock-keywords36,1103
(defun unload-pg 70,2040

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 57,1797

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,3666
(defvar unicode-tokens-token-symbol-map 49,1676
(defvar unicode-tokens-token-format 62,2105
(defvar unicode-tokens-token-variant-format-regexp 68,2354
(defvar unicode-tokens-fontsymb-properties 81,2831
(defvar unicode-tokens-shortcut-alist 86,3065
(defvar unicode-tokens-control-region-format-regexp 96,3308
(defvar unicode-tokens-control-char-format-regexp 103,3676
(defvar unicode-tokens-control-regions 110,4037
(defvar unicode-tokens-control-characters 113,4113
(defvar unicode-tokens-control-char-format 116,4195
(defconst unicode-tokens-configuration-variables123,4348
(defun unicode-tokens-config 135,4644
(defun unicode-tokens-config-var 138,4737
(defun unicode-tokens-copy-configuration-variables 148,5110
(defun unicode-tokens-customize 162,5856
(defvar unicode-tokens-token-list 176,6112
(defvar unicode-tokens-hash-table 179,6232
(defvar unicode-tokens-token-match-regexp 182,6348
(defvar unicode-tokens-uchar-hash-table 185,6460
(defvar unicode-tokens-uchar-regexp 189,6647
(defgroup unicode-tokens-faces 214,7258
(defface unicode-tokens-script-font-face218,7354
(defface unicode-tokens-fraktur-font-face229,7652
(defface unicode-tokens-serif-font-face240,7977
(defface unicode-tokens-highlight-face251,8270
(defconst unicode-tokens-font-lock-extra-managed-props 260,8632
(defun unicode-tokens-font-lock-keywords 268,8804
(defun unicode-tokens-usable-composition 308,10464
(defun unicode-tokens-help-echo 319,10740
(defvar unicode-tokens-show-symbols 323,10903
(defun unicode-tokens-font-lock-compose-symbol 326,11017
(defun unicode-tokens-show-symbols 343,11733
(defun unicode-tokens-symbs-to-props 351,12034
(defvar unicode-tokens-show-controls 367,12488
(defun unicode-tokens-show-controls 370,12579
(defun unicode-tokens-control-char 383,13155
(defun unicode-tokens-control-region 388,13412
(defun unicode-tokens-control-font-lock-keywords 395,13778
(defvar unicode-tokens-use-shortcuts 406,14108
(defun unicode-tokens-use-shortcuts 409,14211
(defun unicode-tokens-map-ordering 427,14808
(defun unicode-tokens-quail-define-rules 431,14958
(defun unicode-tokens-insert-token 454,15637
(defun unicode-tokens-annotate-region 463,15942
(defun unicode-tokens-insert-control 487,16778
(defun unicode-tokens-insert-uchar-as-token 496,17140
(defun unicode-tokens-delete-token-at-point 503,17370
(defun unicode-tokens-prev-token 510,17665
(defun unicode-tokens-rotate-token-forward 518,17930
(defun unicode-tokens-rotate-token-backward 545,18822
(defun unicode-tokens-copy-token 550,19024
(define-button-type 'unicode-tokens-listunicode-tokens-list
556,19199
(defun unicode-tokens-list-tokens 562,19404
(defun unicode-tokens-list-shortcuts 584,20141
(defun unicode-tokens-encode-in-temp-buffer 605,20795
(defun unicode-tokens-encode 625,21559
(defun unicode-tokens-encode-str 630,21770
(defun unicode-tokens-copy 634,21940
(defun unicode-tokens-paste 643,22347
(defvar unicode-tokens-highlight-unicode 659,22890
(defconst unicode-tokens-unicode-highlight-patterns662,22982
(defun unicode-tokens-highlight-unicode 666,23151
(defun unicode-tokens-highlight-unicode-setkeywords 678,23615
(defun unicode-tokens-initialise 689,23899
(defvar unicode-tokens-mode-map 698,24197
(define-minor-mode unicode-tokens-mode701,24294
(define-key unicode-tokens-mode-map 786,27262
(define-key unicode-tokens-mode-map 788,27354
(define-key unicode-tokens-mode-map 790,27445
(define-key unicode-tokens-mode-map 792,27552
(define-key unicode-tokens-mode-map 794,27662
(define-key unicode-tokens-mode-map 796,27771
(define-key unicode-tokens-mode-map 798,27878
(defun unicode-tokens-define-menu 806,28007

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,5692
@node Top164,4907
@node Preface201,6014
@node News for Version 4.0News for Version 4.0
224,6603
@node Future249,7451
@node Credits280,8750
@node Introducing Proof GeneralIntroducing Proof General
385,12392
@node Installing Proof GeneralInstalling Proof General
440,14370
@node Quick start guideQuick start guide
454,14819
@node Features of Proof GeneralFeatures of Proof General
498,16940
@node Supported proof assistantsSupported proof assistants
587,20877
@node Prerequisites for this manualPrerequisites for this manual
636,22766
@node Organization of this manualOrganization of this manual
680,24385
@node Basic Script ManagementBasic Script Management
706,25213
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
725,25813
@node Proof scriptsProof scripts
991,36046
@node Script buffersScript buffers
1034,38166
@node Locked queue and editing regionsLocked queue and editing regions
1056,38743
@node Goal-save sequencesGoal-save sequences
1112,40890
@node Active scripting bufferActive scripting buffer
1149,42376
@node Summary of Proof General buffersSummary of Proof General buffers
1218,45796
@node Script editing commandsScript editing commands
1281,48536
@node Script processing commandsScript processing commands
1361,51494
@node Proof assistant commandsProof assistant commands
1489,56794
@node Toolbar commandsToolbar commands
1655,62573
@node Interrupting during trace outputInterrupting during trace output
1679,63502
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1718,65423
@node Goals buffer commandsGoals buffer commands
1732,65923
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1821,69487
@node Document centric workingDocument centric working
1853,70702
@node Visibility of completed proofsVisibility of completed proofs
1904,72163
@node Switching between proof scriptsSwitching between proof scripts
1959,74086
@node View of processed files View of processed files 
1996,76058
@node Retracting across filesRetracting across files
2056,79109
@node Asserting across filesAsserting across files
2069,79740
@node Automatic multiple file handlingAutomatic multiple file handling
2082,80306
@node Escaping script managementEscaping script management
2107,81340
@node Editing featuresEditing features
2165,83543
@node Support for other PackagesSupport for other Packages
2236,86335
@node Syntax highlightingSyntax highlighting
2268,87209
@node Unicode supportUnicode support
2297,88213
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2443,94104
@node Support for outline modeSupport for outline mode
2498,96148
@node Support for completionSupport for completion
2523,97277
@node Support for tagsSupport for tags
2580,99439
@node Customizing Proof GeneralCustomizing Proof General
2632,101767
@node Basic optionsBasic options
2672,103437
@node How to customizeHow to customize
2696,104195
@node Display customizationDisplay customization
2743,106162
@node User optionsUser options
2897,112562
@node Changing facesChanging faces
3139,121105
@node Tweaking configuration settingsTweaking configuration settings
3214,123774
@node Hints and TipsHints and Tips
3271,126300
@node Adding your own keybindingsAdding your own keybindings
3290,126901
@node Using file variablesUsing file variables
3354,129488
@node Using abbreviationsUsing abbreviations
3413,131674
@node LEGO Proof GeneralLEGO Proof General
3452,133089
@node LEGO specific commandsLEGO specific commands
3493,134458
@node LEGO tagsLEGO tags
3513,134913
@node LEGO customizationsLEGO customizations
3523,135160
@node Coq Proof GeneralCoq Proof General
3555,136079
@node Coq-specific commandsCoq-specific commands
3571,136488
@node Coq-specific variablesCoq-specific variables
3593,136995
@node Editing multiple proofsEditing multiple proofs
3615,137653
@node User-loaded tacticsUser-loaded tactics
3639,138761
@node Holes featureHoles feature
3703,141235
@node Isabelle Proof GeneralIsabelle Proof General
3730,142522
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3761,143691
@node Isabelle commandsIsabelle commands
3830,146499
@node Isabelle settingsIsabelle settings
3973,150652
@node Isabelle customizationsIsabelle customizations
3987,151234
@node HOL Proof GeneralHOL Proof General
4010,151721
@node Shell Proof GeneralShell Proof General
4052,153543
@node Obtaining and InstallingObtaining and Installing
4088,155002
@node Obtaining Proof GeneralObtaining Proof General
4104,155415
@node Installing Proof General from tarballInstalling Proof General from tarball
4135,156654
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4160,157486
@node Setting the names of binariesSetting the names of binaries
4175,157894
@node Notes for syssiesNotes for syssies
4203,158834
@node Bugs and EnhancementsBugs and Enhancements
4278,161870
@node References4299,162685
@node History of Proof GeneralHistory of Proof General
4339,163708
@node Old News for 3.0Old News for 3.0
4433,167873
@node Old News for 3.1Old News for 3.1
4503,171567
@node Old News for 3.2Old News for 3.2
4529,172739
@node Old News for 3.3Old News for 3.3
4590,175742
@node Old News for 3.4Old News for 3.4
4609,176639
@node Old News for 3.5Old News for 3.5
4631,177694
@node Old News for 3.6Old News for 3.6
4635,177751
@node Old News for 3.7Old News for 3.7
4640,177851
@node Function IndexFunction Index
4684,179749
@node Variable IndexVariable Index
4688,179825
@node Keystroke IndexKeystroke Index
4692,179905
@node Concept IndexConcept Index
4696,179971

doc/PG-adapting.texi,3772
@node Top155,4691
@node Introduction192,5800
@node Future233,7453
@node Credits269,9049
@node Beginning with a New ProverBeginning with a New Prover
279,9341
@node Overview of adding a new proverOverview of adding a new prover
320,11290
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
398,14598
@node Major modes used by Proof GeneralMajor modes used by Proof General
467,17989
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
500,19340
@node Settings for generic user-level commandsSettings for generic user-level commands
515,19886
@node Menu configurationMenu configuration
560,21618
@node Toolbar configurationToolbar configuration
584,22535
@node Proof Script SettingsProof Script Settings
643,24772
@node Recognizing commands and commentsRecognizing commands and comments
665,25352
@node Recognizing proofsRecognizing proofs
790,31068
@node Recognizing other elementsRecognizing other elements
899,35749
@node Configuring undo behaviourConfiguring undo behaviour
1025,41288
@node Nested proofsNested proofs
1162,46696
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1202,48322
@node Activate scripting hookActivate scripting hook
1225,49275
@node Automatic multiple filesAutomatic multiple files
1249,50145
@node Completions1271,50992
@node Proof Shell SettingsProof Shell Settings
1312,52482
@node Proof shell commandsProof shell commands
1343,53764
@node Script input to the shellScript input to the shell
1507,60808
@node Settings for matching various output from proof processSettings for matching various output from proof process
1572,63766
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1703,69551
@node Hooks and other settingsHooks and other settings
1918,79428
@node Goals Buffer SettingsGoals Buffer Settings
1999,82810
@node Splash Screen SettingsSplash Screen Settings
2076,85917
@node Global ConstantsGlobal Constants
2102,86675
@node Handling Multiple FilesHandling Multiple Files
2128,87516
@node Configuring Editing SyntaxConfiguring Editing Syntax
2280,95299
@node Configuring Font LockConfiguring Font Lock
2339,97420
@node Configuring TokensConfiguring Tokens
2411,100775
@node Writing More Lisp CodeWriting More Lisp Code
2449,102276
@node Default values for generic settingsDefault values for generic settings
2466,102921
@node Adding prover-specific configurationsAdding prover-specific configurations
2496,104004
@node Useful variablesUseful variables
2539,105286
@node Useful functions and macrosUseful functions and macros
2554,105785
@node Internals of Proof GeneralInternals of Proof General
2657,109740
@node Spans2685,110648
@node Proof General site configurationProof General site configuration
2697,110970
@node Configuration variable mechanismsConfiguration variable mechanisms
2777,114016
@node Global variablesGlobal variables
2898,119460
@node Proof script modeProof script mode
2968,122008
@node Proof shell modeProof shell mode
3227,133663
@node Debugging3634,149745
@node Plans and IdeasPlans and Ideas
3677,150621
@node Proof by pointing and similar featuresProof by pointing and similar features
3698,151343
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3736,153001
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3781,155226
@node Demonstration InstantiationsDemonstration Instantiations
3811,156257
@node demoisa-easy.el3827,156688
@node demoisa.el3890,158927
@node Function IndexFunction Index
4045,163912
@node Variable IndexVariable Index
4049,163988
@node Concept IndexConcept Index
4058,164167

generic/proof.el,0

generic/proof-autoloads.el,0

generic/comptest.el,0

pgshell/pgshell.el,0

isar/test.el,0

isar/isar-templates.el,0

isar/isar-autotest.el,0

isar/interface-setup.el,0

isar/comptest.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