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,8518

coq/coq.el,6513
(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 120,3648
(defvar coq-shell-abort-goal-regexp 124,3803
(defvar coq-shell-proof-completed-regexp 127,3929
(defvar coq-goal-regexp130,4081
(defun coq-library-directory 137,4195
(defcustom coq-tags 144,4375
(defconst coq-interrupt-regexp 149,4525
(defcustom coq-www-home-page 154,4646
(defvar coq-outline-regexp164,4817
(defvar coq-outline-heading-end-regexp 171,5031
(defvar coq-shell-outline-regexp 173,5085
(defvar coq-shell-outline-heading-end-regexp 174,5135
(defconst coq-kill-goal-command 179,5245
(defconst coq-forget-id-command 180,5288
(defconst coq-back-n-command 181,5335
(defconst coq-state-preserving-tactics-regexp 185,5479
(defconst coq-state-changing-commands-regexp187,5580
(defconst coq-state-preserving-commands-regexp 189,5687
(defconst coq-commands-regexp 191,5799
(defvar coq-retractable-instruct-regexp 193,5877
(defvar coq-non-retractable-instruct-regexp 195,5968
(defvar coq-keywords-section199,6108
(defvar coq-section-regexp 202,6202
(defun coq-set-undo-limit 239,7348
(defconst coq-keywords-decl-defn-regexp250,7787
(defun coq-proof-mode-p 254,7937
(defun coq-is-comment-or-proverprocp 265,8345
(defun coq-is-goalsave-p 267,8449
(defun coq-is-module-equal-p 268,8524
(defun coq-is-def-p 271,8720
(defun coq-is-decl-defn-p 273,8828
(defun coq-state-preserving-command-p 278,8995
(defun coq-command-p 281,9129
(defun coq-state-preserving-tactic-p 284,9229
(defun coq-state-changing-tactic-p 289,9377
(defun coq-state-changing-command-p 296,9611
(defun coq-section-or-module-start-p 303,9957
(defun build-list-id-from-string 312,10198
(defun coq-last-prompt-info 325,10728
(defun coq-last-prompt-info-safe 337,11269
(defvar coq-last-but-one-statenum 343,11526
(defvar coq-last-but-one-proofnum 349,11824
(defvar coq-last-but-one-proofstack 352,11922
(defun coq-get-span-statenum 355,12032
(defun coq-get-span-proofnum 360,12147
(defun coq-get-span-proofstack 365,12262
(defun coq-set-span-statenum 370,12406
(defun coq-get-span-goalcmd 375,12537
(defun coq-set-span-goalcmd 380,12651
(defun coq-set-span-proofnum 385,12781
(defun coq-set-span-proofstack 390,12912
(defun proof-last-locked-span 395,13072
(defun coq-set-state-infos 410,13676
(defun count-not-intersection 450,15755
(defun  coq-find-and-forget-v81 481,17009
(defun coq-find-and-forget-v80 509,18141
(defun coq-find-and-forget 604,22840
(defvar coq-current-goal 617,23380
(defun coq-goal-hyp 620,23445
(defun coq-state-preserving-p 633,23878
(defconst notation-print-kinds-table 647,24383
(defun coq-PrintScope 651,24551
(defun coq-guess-or-ask-for-string 670,25107
(defun coq-ask-do 684,25650
(defun coq-SearchIsos 693,26038
(defun coq-SearchConstant 699,26271
(defun coq-SearchRewrite 703,26364
(defun coq-SearchAbout 707,26462
(defun coq-Print 711,26554
(defun coq-About 715,26676
(defun coq-LocateConstant 719,26793
(defun coq-LocateLibrary 725,26928
(defun coq-addquotes 731,27078
(defun coq-LocateNotation 733,27126
(defun coq-Pwd 740,27325
(defun coq-Inspect 746,27457
(defun coq-PrintSection(750,27557
(defun coq-Print-implicit 754,27650
(defun coq-Check 759,27801
(defun coq-Show 764,27909
(defun coq-Compile 778,28352
(defun coq-guess-command-line 792,28672
(defun coq-mode-config 828,30322
(defvar coq-last-hybrid-pre-string 936,34276
(defun coq-hybrid-ouput-goals-response-p 939,34455
(defun coq-hybrid-ouput-goals-response 945,34713
(defun coq-shell-mode-config 966,35673
(defun coq-goals-mode-config 1011,37788
(defun coq-response-config 1018,38032
(defpacustom print-fully-explicit 1043,38857
(defpacustom print-implicit 1048,39006
(defpacustom print-coercions 1053,39173
(defpacustom print-match-wildcards 1058,39318
(defpacustom print-elim-types 1063,39499
(defpacustom printing-depth 1068,39666
(defpacustom undo-depth 1073,39828
(defpacustom time-commands 1078,39976
(defpacustom undo-limit 1082,40087
(defpacustom auto-compile-vos 1087,40190
(defun coq-maybe-compile-buffer 1116,41306
(defun coq-ancestors-of 1153,42840
(defun coq-all-ancestors-of 1176,43807
(defconst coq-require-command-regexp 1188,44200
(defun coq-process-require-command 1193,44409
(defun coq-included-children 1198,44536
(defun coq-process-file 1219,45375
(defun coq-preprocessing 1234,45914
(defun coq-fake-constant-markup 1249,46333
(defun coq-create-span-menu 1270,47139
(defconst module-kinds-table 1287,47638
(defconst modtype-kinds-table1291,47788
(defun coq-insert-section-or-module 1295,47917
(defconst reqkinds-kinds-table1318,48777
(defun coq-insert-requires 1323,48922
(defun coq-end-Section 1339,49428
(defun coq-insert-intros 1357,50012
(defun coq-insert-infoH-hook 1370,50537
(defun coq-insert-as 1374,50615
(defun coq-insert-match 1395,51364
(defun coq-insert-tactic 1427,52542
(defun coq-insert-tactical 1433,52781
(defun coq-insert-command 1439,53030
(defun coq-insert-term 1445,53274
(define-key coq-keymap 1451,53471
(define-key coq-keymap 1452,53529
(define-key coq-keymap 1453,53586
(define-key coq-keymap 1454,53655
(define-key coq-keymap 1455,53711
(define-key coq-keymap 1456,53760
(define-key coq-keymap 1457,53818
(define-key coq-keymap 1459,53879
(define-key coq-keymap 1460,53938
(define-key coq-keymap 1462,54002
(define-key coq-keymap 1463,54062
(define-key coq-keymap 1465,54118
(define-key coq-keymap 1466,54168
(define-key coq-keymap 1467,54218
(define-key coq-keymap 1468,54268
(define-key coq-keymap 1469,54322
(define-key coq-keymap 1470,54381
(defvar last-coq-error-location 1478,54512
(defun coq-get-last-error-location 1487,54911
(defun coq-highlight-error 1534,57296
(defvar coq-allow-highlight-error 1570,58599
(defun coq-decide-highlight-error 1576,58865
(defun coq-highlight-error-hook 1580,58987
(defun first-word-of-buffer 1591,59380
(defun coq-show-first-goal 1599,59583
(defvar coq-modeline-string2 1616,60278
(defvar coq-modeline-string1 1617,60322
(defvar coq-modeline-string0 1618,60365
(defun coq-build-subgoals-string 1619,60410
(defun coq-update-minor-mode-alist 1624,60578
(defun is-not-split-vertic 1650,61646
(defun optim-resp-windows 1659,62085

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,306
(defun coq-insert-coq-prog-name 75,2832
(defun coq-read-directory 86,3305
(defun coq-extract-directories-from-args 110,4408
(defun coq-ask-prog-args 125,4960
(defun coq-ask-prog-name 147,6064
(defun coq-ask-insert-coq-prog-name 165,6819

coq/coq-syntax.el,2666
(defcustom coq-prog-name 13,422
(defvar coq-version-is-V8 34,1421
(defvar coq-version-is-V8-0 36,1500
(defvar coq-version-is-V8-1 43,1878
(defun coq-determine-version 52,2311
(defcustom coq-user-tactics-db 98,4217
(defcustom coq-user-commands-db 115,4730
(defcustom coq-user-tacticals-db 131,5249
(defcustom coq-user-solve-tactics-db 147,5770
(defcustom coq-user-reserved-db 165,6291
(defvar coq-tactics-db183,6822
(defvar coq-solve-tactics-db338,14890
(defvar coq-tacticals-db362,15737
(defvar coq-decl-db386,16624
(defvar coq-defn-db408,17842
(defvar coq-goal-starters-db461,21828
(defvar coq-other-commands-db488,23383
(defvar coq-commands-db612,32580
(defvar coq-terms-db619,32806
(defun coq-count-match 683,35458
(defun coq-goal-command-str-v80-p 702,36321
(defun coq-module-opening-p 725,37194
(defun coq-section-command-p 736,37610
(defun coq-goal-command-str-v81-p 740,37707
(defun coq-goal-command-p-v81 755,38376
(defun coq-goal-command-str-p 765,38716
(defun coq-goal-command-p 775,39082
(defvar coq-keywords-save-strict783,39394
(defvar coq-keywords-save792,39507
(defun coq-save-command-p 796,39585
(defvar coq-keywords-kill-goal 805,39879
(defvar coq-keywords-state-changing-misc-commands809,39970
(defvar coq-keywords-goal812,40095
(defvar coq-keywords-decl815,40178
(defvar coq-keywords-defn818,40252
(defvar coq-keywords-state-changing-commands822,40327
(defvar coq-keywords-state-preserving-commands831,40588
(defvar coq-keywords-commands836,40804
(defvar coq-solve-tactics841,40953
(defvar coq-tacticals845,41074
(defvar coq-reserved851,41213
(defvar coq-state-changing-tactics862,41542
(defvar coq-state-preserving-tactics865,41651
(defvar coq-tactics869,41765
(defvar coq-retractable-instruct872,41854
(defvar coq-non-retractable-instruct875,41964
(defvar coq-keywords879,42092
(defvar coq-symbols886,42260
(defvar coq-error-regexp 905,42473
(defvar coq-id 908,42701
(defvar coq-id-shy 909,42726
(defvar coq-ids 911,42780
(defun coq-first-abstr-regexp 913,42821
(defcustom coq-variable-highlight-enable 916,42916
(defvar coq-font-lock-terms922,43043
(defconst coq-save-command-regexp-strict943,44043
(defconst coq-save-command-regexp947,44210
(defconst coq-save-with-hole-regexp951,44363
(defconst coq-goal-command-regexp955,44522
(defconst coq-goal-with-hole-regexp958,44622
(defconst coq-decl-with-hole-regexp962,44755
(defconst coq-defn-with-hole-regexp969,45004
(defconst coq-with-with-hole-regexp979,45293
(defvar coq-font-lock-keywords-1985,45586
(defvar coq-font-lock-keywords 1011,46902
(defun coq-init-syntax-table 1013,46960
(defconst coq-generic-expression1042,47859

coq/coq-unicode-tokens.el,290
(defconst coq-token-format 18,631
(defconst coq-charref-format 19,664
(defconst coq-token-prefix 20,698
(defconst coq-token-suffix 21,730
(defconst coq-token-match 22,762
(defconst coq-hexcode-match 23,793
(defcustom coq-token-name-alist 25,827
(defcustom coq-shortcut-alist44,1557

demoisa/demoisa.el,349
(defcustom isabelledemo-prog-name 54,1809
(defcustom isabelledemo-web-page59,1931
(defun demoisa-config 70,2161
(defun demoisa-shell-config 91,2953
(define-derived-mode demoisa-mode 117,3930
(define-derived-mode demoisa-shell-mode 122,4053
(define-derived-mode demoisa-response-mode 127,4196
(define-derived-mode demoisa-goals-mode 131,4323

isar/isabelle-system.el,1347
(defgroup isabelle 26,775
(defcustom isabelle-web-page30,903
(defcustom isa-isatool-command39,1120
(defvar isatool-not-found 57,1779
(defun isa-set-isatool-command 60,1892
(defun isa-shell-command-to-string 83,2888
(defun isa-getenv 89,3112
(defcustom isabelle-program-name-override 109,3799
(defvar isabelle-prog-name 126,4383
(defun isa-tool-list-logics 129,4493
(defcustom isabelle-logics-available 136,4730
(defcustom isabelle-chosen-logic 146,5066
(defvar isabelle-chosen-logic-prev 162,5650
(defun isabelle-hack-local-variables-function 165,5772
(defun isabelle-set-prog-name 177,6213
(defun isabelle-choose-logic 202,7372
(defun isa-view-doc 221,8134
(defun isa-tool-list-docs 230,8398
(defconst isabelle-verbatim-regexp 257,9430
(defun isabelle-verbatim 260,9572
(defcustom isabelle-refresh-logics 267,9733
(defvar isabelle-docs-menu 275,10060
(defvar isabelle-logics-menu-entries 282,10346
(defun isabelle-logics-menu-calculate 285,10419
(defvar isabelle-time-to-refresh-logics 304,10982
(defun isabelle-logics-menu-refresh 308,11077
(defun isabelle-menu-bar-update-logics 323,11710
(defun isabelle-load-isar-keywords 339,12340
(defun isabelle-convert-idmarkup-to-subterm 360,13056
(defun isabelle-create-span-menu 384,14067
(defun isabelle-xml-sml-escapes 400,14509
(defun isabelle-process-pgip 403,14610

isar/isar.el,1204
(defcustom isar-keywords-name 31,724
(defpgdefault completion-table 48,1247
(defcustom isar-web-page50,1300
(defun isar-strip-terminators 64,1650
(defun isar-markup-ml 77,2027
(defun isar-mode-config-set-variables 82,2162
(defun isar-shell-mode-config-set-variables 151,5341
(defun isar-remove-file 242,9084
(defun isar-shell-compute-new-files-list 252,9447
(define-derived-mode isar-shell-mode 268,9968
(define-derived-mode isar-response-mode 273,10091
(define-derived-mode isar-goals-mode 278,10273
(define-derived-mode isar-mode 283,10448
(defpgdefault menu-entries340,12483
(defpgdefault help-menu-entries 370,13765
(defun isar-count-undos 373,13841
(defun isar-find-and-forget 400,14955
(defun isar-goal-command-p 439,16535
(defun isar-global-save-command-p 444,16712
(defvar isar-current-goal 465,17573
(defun isar-state-preserving-p 468,17639
(defvar isar-shell-current-line-width 493,18836
(defun isar-shell-adjust-line-width 498,19028
(defun isar-preprocessing 523,19932
(defun isar-mode-config 546,21199
(defun isar-shell-mode-config 557,21757
(defun isar-response-mode-config 563,21954
(defun isar-goals-mode-config 569,22135
(defun isar-goalhyplit-test 577,22402

isar/isar-find-theorems.el,778
(defun isar-find-theorems-minibuffer 18,712
(defun isar-find-theorems-form 32,1331
(defvar isar-find-theorems-data 74,3131
(defvar isar-find-theorems-widget-number 88,3466
(defvar isar-find-theorems-widget-pattern 91,3564
(defvar isar-find-theorems-widget-intro 94,3656
(defvar isar-find-theorems-widget-elim 97,3742
(defvar isar-find-theorems-widget-dest 100,3826
(defvar isar-find-theorems-widget-name 103,3910
(defvar isar-find-theorems-widget-simp 106,3997
(defun isar-find-theorems-create-searchform111,4143
(defun isar-find-theorems-create-help 251,8758
(defun isar-find-theorems-submit-searchform294,10930
(defun isar-find-theorems-parse-criteria 372,13307
(defun isar-find-theorems-parse-number 465,16407
(defun isar-find-theorems-filter-empty 475,16684

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,481
(defconst isar-keywords-minor206,3641
(defconst isar-keywords-control262,4395
(defconst isar-keywords-diag282,4872
(defconst isar-keywords-theory-begin338,5831
(defconst isar-keywords-theory-switch341,5884
(defconst isar-keywords-theory-end344,5939
(defconst isar-keywords-theory-heading347,5987
(defconst isar-keywords-theory-decl353,6094
(defconst isar-keywords-theory-script412,7075
(defconst isar-keywords-theory-goal416,7152
(defconst isar-keywords-qed429,7369
(defconst isar-keywords-qed-block436,7455
(defconst isar-keywords-qed-global439,7502
(defconst isar-keywords-proof-heading442,7551
(defconst isar-keywords-proof-goal447,7634
(defconst isar-keywords-proof-block454,7733
(defconst isar-keywords-proof-open458,7795
(defconst isar-keywords-proof-close461,7841
(defconst isar-keywords-proof-chain464,7888
(defconst isar-keywords-proof-decl471,7991
(defconst isar-keywords-proof-asm480,8112
(defconst isar-keywords-proof-asm-goal487,8207
(defconst isar-keywords-proof-script490,8262

isar/isar-mmm.el,83
(defconst isar-start-latex-regexp 23,697
(defconst isar-start-sml-regexp 35,1130

isar/isar-syntax.el,3456
(defconst isar-script-syntax-table-entries20,475
(defconst isar-script-syntax-table-alist44,877
(defun isar-init-syntax-table 53,1167
(defun isar-init-output-syntax-table 61,1414
(defconst isar-keyword-begin 77,1861
(defconst isar-keyword-end 78,1899
(defconst isar-keywords-theory-enclose80,1934
(defconst isar-keywords-theory85,2079
(defconst isar-keywords-save90,2224
(defconst isar-keywords-proof-enclose95,2353
(defconst isar-keywords-proof101,2535
(defconst isar-keywords-proof-context108,2740
(defconst isar-keywords-local-goal112,2854
(defconst isar-keywords-proper116,2966
(defconst isar-keywords-improper121,3099
(defconst isar-keywords-outline126,3245
(defconst isar-keywords-fume129,3310
(defconst isar-keywords-indent-open136,3528
(defconst isar-keywords-indent-close142,3712
(defconst isar-keywords-indent-enclose146,3817
(defun isar-regexp-simple-alt 155,4032
(defun isar-ids-to-regexp 175,4792
(defconst isar-ext-first 209,6198
(defconst isar-ext-rest 210,6265
(defconst isar-long-id-stuff 212,6337
(defconst isar-id 213,6411
(defconst isar-idx 214,6481
(defconst isar-string 216,6540
(defconst isar-any-command-regexp218,6600
(defconst isar-name-regexp222,6734
(defconst isar-improper-regexp228,7029
(defconst isar-save-command-regexp232,7177
(defconst isar-global-save-command-regexp235,7278
(defconst isar-goal-command-regexp238,7392
(defconst isar-local-goal-command-regexp241,7500
(defconst isar-comment-start 244,7613
(defconst isar-comment-end 245,7648
(defconst isar-comment-start-regexp 246,7681
(defconst isar-comment-end-regexp 247,7752
(defconst isar-string-start-regexp 249,7820
(defconst isar-string-end-regexp 250,7872
(defconst isar-antiq-regexp259,8125
(defconst isar-nesting-regexp266,8286
(defun isar-nesting 269,8384
(defun isar-match-nesting 281,8805
(defface isabelle-class-name-face293,9136
(defface isabelle-tfree-name-face301,9319
(defface isabelle-tvar-name-face309,9508
(defface isabelle-free-name-face317,9696
(defface isabelle-bound-name-face325,9880
(defface isabelle-var-name-face333,10067
(defconst isabelle-class-name-face 341,10254
(defconst isabelle-tfree-name-face 342,10316
(defconst isabelle-tvar-name-face 343,10378
(defconst isabelle-free-name-face 344,10439
(defconst isabelle-bound-name-face 345,10500
(defconst isabelle-var-name-face 346,10562
(defvar isar-font-lock-keywords-1349,10624
(defun isar-output-flk 366,11675
(defvar isar-output-font-lock-keywords-1372,11927
(defvar isar-goals-font-lock-keywords390,13029
(defconst isar-undo 424,13708
(defun isar-remove 426,13751
(defun isar-undos 429,13826
(defun isar-cannot-undo 433,13932
(defconst isar-theory-start-regexp436,14002
(defconst isar-end-regexp442,14167
(defconst isar-undo-fail-regexp446,14268
(defconst isar-undo-skip-regexp450,14372
(defconst isar-undo-ignore-regexp453,14493
(defconst isar-undo-remove-regexp456,14558
(defconst isar-any-entity-regexp464,14733
(defconst isar-named-entity-regexp469,14920
(defconst isar-unnamed-entity-regexp474,15097
(defconst isar-next-entity-regexps477,15199
(defconst isar-generic-expression485,15510
(defconst isar-indent-any-regexp496,15827
(defconst isar-indent-inner-regexp498,15920
(defconst isar-indent-enclose-regexp500,15986
(defconst isar-indent-open-regexp502,16102
(defconst isar-indent-close-regexp504,16212
(defconst isar-outline-regexp510,16349
(defconst isar-outline-heading-end-regexp 514,16502

isar/isar-unicode-tokens.el,1008
(defconst isar-control-region-format-regexp20,505
(defconst isar-control-char-format-regexp 23,599
(defconst isar-control-region-format-beg 26,695
(defconst isar-control-region-format-end 27,747
(defconst isar-control-char-format 28,799
(defconst isar-control-characters31,847
(defconst isar-control-regions40,1102
(defcustom isar-fontsymb-properties 50,1427
(defconst isar-token-format 66,1938
(defconst isar-token-variant-format-regexp 70,2090
(defconst isar-greek-letters-tokens73,2212
(defconst isar-misc-letters-tokens109,2908
(defconst isar-symbols-tokens117,3059
(defun isar-try-char 386,9191
(defconst isar-symbols-tokens-fallbacks390,9335
(defconst isar-bold-nums-tokens 414,10166
(defun isar-map-letters 426,10422
(defconst isar-script-letters-tokens432,10571
(defconst isar-roman-letters-tokens437,10709
(defconst isar-fraktur-letters-tokens442,10845
(defcustom isar-token-symbol-map447,10989
(defconst isar-symbol-shortcuts472,11805
(defcustom isar-shortcut-alist528,13363

lclam/lclam.el,524
(defcustom lclam-prog-name 15,389
(defcustom lclam-web-page21,537
(defun lclam-config 32,767
(defun lclam-shell-config 54,1561
(define-derived-mode lclam-proofscript-mode 74,2220
(define-derived-mode lclam-shell-mode 79,2343
(define-derived-mode lclam-response-mode 84,2477
(define-derived-mode lclam-goals-mode 88,2600
(defun lclam-mode 96,2828
(define-derived-mode thy-mode 133,3674
(defvar thy-mode-map 136,3772
(defun thy-add-menus 138,3799
(defun process-thy-file 177,5685
(defun update-thy-only 183,5886

lego/lego.el,1727
(defcustom lego-tags 19,497
(defcustom lego-test-all-name 24,633
(defpgdefault help-menu-entries30,791
(defpgdefault menu-entries34,951
(defvar lego-shell-process-output45,1253
(defconst lego-process-config53,1576
(defconst lego-pretty-set-width 64,2007
(defconst lego-interrupt-regexp 68,2150
(defcustom lego-www-home-page 73,2267
(defcustom lego-www-latest-release78,2391
(defcustom lego-www-refcard84,2569
(defcustom lego-library-www-page90,2718
(defvar lego-prog-name 99,2934
(defvar lego-shell-prompt-pattern 102,3003
(defvar lego-shell-cd 105,3124
(defvar lego-shell-abort-goal-regexp 108,3224
(defvar lego-shell-proof-completed-regexp 113,3416
(defvar lego-save-command-regexp116,3556
(defvar lego-goal-command-regexp118,3646
(defvar lego-kill-goal-command 121,3737
(defvar lego-forget-id-command 122,3780
(defvar lego-undoable-commands-regexp124,3826
(defvar lego-goal-regexp 133,4200
(defvar lego-outline-regexp135,4245
(defvar lego-outline-heading-end-regexp 141,4421
(defvar lego-shell-outline-regexp 143,4474
(defvar lego-shell-outline-heading-end-regexp 144,4526
(define-derived-mode lego-shell-mode 150,4805
(define-derived-mode lego-mode 157,4966
(define-derived-mode lego-goals-mode 168,5263
(defun lego-count-undos 179,5689
(defun lego-goal-command-p 199,6508
(defun lego-find-and-forget 204,6679
(defun lego-goal-hyp 246,8515
(defun lego-state-preserving-p 255,8713
(defvar lego-shell-current-line-width 271,9416
(defun lego-shell-adjust-line-width 279,9723
(defun lego-mode-config 298,10462
(defun lego-equal-module-filename 366,12523
(defun lego-shell-compute-new-files-list 372,12798
(defun lego-shell-mode-config 386,13324
(defun lego-goals-mode-config 435,15260

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,358
(defconst lego-keywords-save 17,401
(defconst lego-commands19,472
(defconst lego-keywords31,1032
(defconst lego-tacticals 36,1209
(defconst lego-error-regexp 39,1317
(defvar lego-id 42,1476
(defvar lego-ids 44,1503
(defconst lego-arg-list-regexp 48,1699
(defun lego-decl-defn-regexp 51,1815
(defconst lego-definiendum-alternative-regexp59,2187
(defvar lego-font-lock-terms63,2371
(defconst lego-goal-with-hole-regexp89,3227
(defconst lego-save-with-hole-regexp94,3450
(defvar lego-font-lock-keywords-199,3667
(defun lego-init-syntax-table 110,4134

phox/phox.el,602
(defcustom phox-prog-name 31,920
(defcustom phox-sym-lock-enabled 36,1022
(defcustom phox-web-page42,1131
(defcustom phox-doc-dir 48,1281
(defcustom phox-lib-dir 54,1429
(defcustom phox-tags-program 60,1573
(defcustom phox-tags-doc 66,1753
(defcustom phox-etags 72,1891
(defpgdefault menu-entries93,2343
(defun phox-config 107,2536
(defun phox-shell-config 148,4427
(define-derived-mode phox-mode 173,5356
(define-derived-mode phox-shell-mode 189,5822
(define-derived-mode phox-response-mode 194,5950
(define-derived-mode phox-goals-mode 207,6392
(defpgdefault completion-table233,7276

phox/phox-extraction.el,382
(defvar phox-prog-orig 11,480
(defun phox-prog-flags-modify(13,548
(defun phox-prog-flags-extract(42,1352
(defun phox-prog-flags-erase(53,1643
(defun phox-toggle-extraction(61,1839
(defun phox-compile-theorem(73,2241
(defun phox-compile-theorem-on-cursor(79,2467
(defun phox-output 95,2946
(defun phox-output-theorem 105,3160
(defun phox-output-theorem-on-cursor(112,3460

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,2392
(defvar phox-top-keywords83,2865
(defvar phox-proof-keywords131,3320
(defun phox-find-and-forget 172,3670
(defun phox-assert-next-command-interactive 251,6095
(defun phox-depend-theorem(270,6926
(defun phox-eshow-extlist(279,7216
(defun phox-flag-name(293,7815
(defun phox-path(304,8118
(defun phox-print-expression(315,8355
(defun phox-print-sort-expression(328,8813
(defun phox-priority-symbols-list(339,9126
(defun phox-search-string(351,9499
(defun phox-constraints(366,10027
(defun phox-goals(377,10284
(defvar phox-state-menu389,10494
(defun phox-delete-symbol(414,11484
(defun phox-delete-symbol-on-cursor(420,11693

phox/phox-lang.el,283
(defvar phox-lang8,278
(defun phox-lang-absurd 17,495
(defun phox-lang-suppress 22,590
(defun phox-lang-opendef 27,789
(defun phox-lang-instance 32,908
(defun phox-lang-lock 37,1037
(defun phox-lang-unlock 42,1174
(defun phox-lang-prove 47,1317
(defun phox-lang-let 52,1454

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,1188
(defun phox-pbrpm-right-paren-p 34,1391
(defun phox-pbrpm-menu-from-string 42,1595
(defun phox-pbrpm-rename-in-cmd 51,1929
(defun phox-pbrpm-get-region-name 84,3183
(defun  phox-pbrpm-escape-string 87,3310
(defun phox-pbrpm-generate-menu 91,3445
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
289,10634
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
290,10698
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
291,10760

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,770
(defun phox-tags-reset-table(29,1099
(defun phox-tags-add-doc-table(34,1209
(defun phox-tags-add-lib-table(40,1358
(defun phox-tags-add-local-table(46,1494
(defun phox-tags-create-local-table(52,1677
(defun phox-complete-tag(63,1929
(defvar phox-tags-menu70,2038

plastic/plastic.el,2866
(defcustom plastic-tags 29,821
(defcustom plastic-test-all-name 34,953
(defvar plastic-lit-string 41,1144
(defcustom plastic-help-menu-list45,1258
(defvar plastic-shell-process-output59,1752
(defconst plastic-process-config 67,2078
(defconst plastic-pretty-set-width 74,2328
(defconst plastic-interrupt-regexp 78,2477
(defcustom plastic-www-home-page 84,2598
(defcustom plastic-www-latest-release89,2735
(defcustom plastic-www-refcard95,2908
(defcustom plastic-library-www-page101,3039
(defcustom plastic-base 111,3254
(defvar plastic-prog-name 119,3426
(defun plastic-set-default-env-vars 123,3534
(defvar plastic-shell-prompt-pattern 131,3772
(defvar plastic-shell-cd 134,3897
(defvar plastic-shell-abort-goal-regexp 138,4039
(defvar plastic-shell-proof-completed-regexp 142,4207
(defvar plastic-save-command-regexp145,4350
(defvar plastic-goal-command-regexp147,4446
(defvar plastic-kill-goal-command 150,4543
(defvar plastic-forget-id-command 152,4644
(defvar plastic-undoable-commands-regexp155,4725
(defvar plastic-goal-regexp 167,5172
(defvar plastic-outline-regexp169,5220
(defvar plastic-outline-heading-end-regexp 175,5399
(defvar plastic-shell-outline-regexp 177,5455
(defvar plastic-shell-outline-heading-end-regexp 178,5513
(defvar plastic-error-occurred 180,5584
(define-derived-mode plastic-shell-mode 189,5916
(define-derived-mode plastic-mode 195,6098
(define-derived-mode plastic-goals-mode 211,6618
(defun plastic-count-undos 220,6963
(defun plastic-goal-command-p 240,7839
(defun plastic-find-and-forget 245,8032
(defun plastic-goal-hyp 280,9380
(defun plastic-state-preserving-p 291,9630
(defvar plastic-shell-current-line-width 314,10606
(defun plastic-shell-adjust-line-width 322,10922
(defun plastic-mode-config 349,12017
(defun plastic-show-shell-buffer 438,15292
(defun plastic-equal-module-filename 444,15395
(defun plastic-shell-compute-new-files-list 450,15673
(defun plastic-shell-mode-config 466,16210
(defun plastic-goals-mode-config 517,18415
(defun plastic-small-bar 529,18709
(defun plastic-large-bar 531,18798
(defun plastic-preprocessing 533,18936
(defun plastic-all-ctxt 584,20764
(defun plastic-send-one-undo 591,20942
(defun plastic-minibuf-cmd 601,21270
(defun plastic-minibuf 613,21749
(defun plastic-synchro 620,21955
(defun plastic-send-minibuf 625,22096
(defun plastic-had-error 633,22425
(defun plastic-reset-error 637,22600
(defun plastic-call-if-no-error 640,22739
(defun plastic-show-shell 645,22943
(define-key plastic-keymap 654,23205
(define-key plastic-keymap 655,23266
(define-key plastic-keymap 656,23327
(define-key plastic-keymap 657,23387
(define-key plastic-keymap 658,23446
(define-key plastic-keymap 659,23505
(defalias 'proof-toolbar-command proof-toolbar-command
669,23755
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
670,23806

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,591
(defcustom twelf-info-dir31,749
(defun twelf-add-read-declaration 100,3259
(defun twelf-set-syntax 113,3594
(defun twelf-set-word 115,3691
(defun twelf-set-symbol 116,3753
(defun twelf-map-string 118,3817
(defun twelf-mode-extra-config 165,5879
(defconst twelf-syntax-menu171,6085
(defpacustom chatter 185,6452
(defpacustom double-check 190,6545
(defpacustom print-implicit 194,6682
(defpgdefault menu-entries206,6826

twelf/twelf-font.el,917
(defun twelf-font-create-face 31,836
(defvar twelf-font-dark-background 38,1094
(defvar twelf-font-patterns64,2452
(defun twelf-font-fontify-decl 105,4302
(defun twelf-font-fontify-buffer 115,4599
(defun twelf-font-unfontify 122,4858
(defvar font-lock-message-threshold 127,5032
(defun twelf-font-fontify-region 129,5110
(defun twelf-font-highlight 195,7610
(defun twelf-font-find-delimited-comment 204,8067
(defun twelf-font-find-decl 223,8747
(defun twelf-font-find-binder 239,9237
(defun twelf-font-find-parm 301,11094
(defun twelf-font-find-evar 308,11417
(defun twelf-current-decl 330,12159
(defun twelf-next-decl 357,13315
(defconst *whitespace* 382,14337
(defconst *twelf-comment-start* 385,14435
(defconst *twelf-id-chars* 388,14564
(defun skip-twelf-comments-and-whitespace 391,14682
(defun twelf-end-of-par 403,15156
(defun skip-ahead 426,15930
(defun current-line-absolute 438,16352

twelf/twelf-old.el,6958
(defvar twelf-indent 212,8771
(defvar twelf-infix-regexp 215,8831
(defvar twelf-server-program 219,9026
(defvar twelf-info-file 222,9107
(defvar twelf-server-display-commands 225,9180
(defvar twelf-highlight-range-function 230,9428
(defvar twelf-focus-function 235,9711
(defvar twelf-server-echo-commands 241,9991
(defvar twelf-save-silently 244,10112
(defvar twelf-server-timeout 248,10284
(defvar twelf-sml-program 252,10431
(defvar twelf-sml-args 255,10503
(defvar twelf-sml-display-queries 258,10569
(defvar twelf-mode-hook 261,10677
(defvar twelf-server-mode-hook 264,10771
(defvar twelf-config-mode-hook 267,10879
(defvar twelf-sml-mode-hook 270,10993
(defvar twelf-to-twelf-sml-mode 273,11074
(defvar twelf-config-mode 276,11166
(defvar *twelf-server-buffer-name* 283,11430
(defvar *twelf-server-buffer* 286,11534
(defvar *twelf-server-process-name* 289,11622
(defvar *twelf-config-buffer* 292,11713
(defvar *twelf-config-time* 295,11807
(defvar *twelf-config-list* 298,11920
(defvar *twelf-server-last-process-mark* 301,12032
(defvar *twelf-last-region-sent* 304,12150
(defvar *twelf-last-input-buffer* 311,12474
(defvar *twelf-error-pos* 315,12597
(defconst *twelf-read-functions*318,12673
(defconst *twelf-parm-table*325,12911
(defvar twelf-chatter 338,13287
(defvar twelf-double-check 346,13504
(defvar twelf-print-implicit 349,13591
(defconst *twelf-track-parms*352,13683
(defun install-basic-twelf-keybindings 363,14107
(defun install-twelf-keybindings 388,15076
(defvar twelf-mode-map 404,15841
(defvar twelf-mode-syntax-table 416,16277
(defun set-twelf-syntax 419,16356
(defun set-word 421,16453
(defun set-symbol 422,16508
(defun map-string 424,16566
(defconst *whitespace* 456,18043
(defconst *twelf-comment-start* 459,18141
(defconst *twelf-id-chars* 462,18270
(defun skip-twelf-comments-and-whitespace 465,18388
(defun twelf-end-of-par 477,18862
(defun twelf-current-decl 500,19636
(defun twelf-mark-decl 527,20792
(defun twelf-indent-decl 536,21058
(defun twelf-indent-region 545,21344
(defun twelf-indent-lines 556,21668
(defun twelf-comment-indent 564,21841
(defun looked-at 575,22197
(defun twelf-indent-line 580,22369
(defun twelf-indent-line-to 613,24112
(defun twelf-calculate-indent 626,24567
(defun twelf-dsb 641,25191
(defun twelf-mode-variables 667,26603
(defun twelf-mode 689,27416
(defun twelf-info 904,35798
(defconst twelf-error-regexp918,36338
(defconst twelf-error-fields-regexp922,36449
(defconst twelf-error-decl-regexp928,36662
(defun looked-at-nth 932,36811
(defun looked-at-nth-int 938,36993
(defun twelf-error-parser 943,37111
(defun twelf-error-decl 957,37714
(defun twelf-mark-relative 963,37893
(defun twelf-mark-absolute 979,38563
(defun twelf-find-decl 1004,39449
(defun twelf-next-error 1019,40005
(defun twelf-goto-error 1087,42815
(defun twelf-convert-standard-filename 1101,43353
(defun string-member 1113,43848
(defun twelf-config-proceed-p 1125,44340
(defun twelf-save-if-config 1132,44602
(defun twelf-config-save-some-buffers 1145,45074
(defun twelf-save-check-config 1149,45239
(defun twelf-check-config 1164,45795
(defun twelf-save-check-file 1176,46235
(defun twelf-buffer-substring 1192,46958
(defun twelf-buffer-substring-dot 1198,47220
(defun twelf-check-declaration 1204,47486
(defun twelf-highlight-range-zmacs 1227,48546
(defun twelf-focus 1233,48796
(defun twelf-focus-noop 1239,49062
(defun twelf-type-const 1322,52684
(defvar twelf-server-mode-map 1439,57826
(defconst twelf-server-cd-regexp 1451,58378
(defun looked-at-string 1454,58518
(defun twelf-server-directory-tracker 1458,58659
(defun twelf-input-filter 1480,59839
(defun twelf-server-mode 1486,60094
(defun twelf-parse-config 1519,61311
(defun twelf-server-read-config 1537,62203
(defun twelf-server-sync-config 1546,62540
(defun twelf-get-server-buffer 1576,64046
(defun twelf-init-variables 1593,64720
(defun twelf-server 1600,64933
(defun twelf-server-process 1642,66847
(defun twelf-server-display 1651,67253
(defun display-server-buffer 1658,67527
(defun twelf-server-send-command 1673,68259
(defun twelf-accept-process-output 1694,69219
(defun twelf-server-wait 1703,69658
(defun twelf-server-quit 1745,71796
(defun twelf-server-interrupt 1750,71917
(defun twelf-reset 1755,72053
(defun twelf-config-directory 1760,72197
(defun twelf-server-configure 1771,72611
(defun natp 1844,75903
(defun twelf-read-nat 1848,76004
(defun twelf-read-bool 1857,76271
(defun twelf-read-limit 1863,76419
(defun twelf-read-strategy 1873,76722
(defun twelf-read-value 1879,76874
(defun twelf-set 1883,77037
(defun twelf-set-parm 1896,77514
(defun track-parm 1905,77811
(defun twelf-toggle-double-check 1910,77985
(defun twelf-toggle-print-implicit 1916,78188
(defun twelf-get 1922,78401
(defun twelf-timers-reset 1936,79027
(defun twelf-timers-show 1941,79147
(defun twelf-timers-check 1947,79298
(defun twelf-server-restart 1953,79463
(defun twelf-config-mode 1969,80140
(defun twelf-config-mode-check 1985,80739
(defun twelf-tag 1994,81189
(defun twelf-tag-files 2022,82453
(default: *tags-errors*)2026,82756
(defun twelf-tag-file 2047,83507
(defun twelf-next-decl 2082,84729
(defun skip-ahead 2107,85751
(defun current-line-absolute 2119,86173
(defun new-temp-buffer 2124,86383
(defun rev-relativize 2135,86767
(defvar twelf-sml-mode-map 2149,87227
(defconst twelf-sml-prompt-regexp 2159,87605
(defun expand-dir 2161,87660
(defun twelf-sml-cd 2168,87921
(defconst twelf-sml-cd-regexp 2180,88410
(defun twelf-sml-directory-tracker 2183,88544
(defun twelf-sml-mode 2199,89389
(defun twelf-sml 2250,91323
(defun switch-to-twelf-sml 2270,92283
(defun display-twelf-sml-buffer 2281,92632
(defun twelf-sml-send-string 2297,93348
(defun twelf-sml-send-region 2302,93552
(defun twelf-sml-send-query 2326,94758
(defun twelf-sml-send-newline 2336,95155
(defun twelf-sml-send-semicolon 2344,95483
(defun twelf-sml-status 2352,95817
(defvar twelf-sml-init 2374,96764
(defun twelf-sml-set-mode 2377,96941
(defun twelf-sml-quit 2403,98118
(defun twelf-sml-process-buffer 2408,98230
(defun twelf-sml-process 2412,98346
(defvar twelf-to-twelf-sml-mode 2424,98862
(defun install-twelf-to-twelf-sml-keybindings 2427,98947
(defvar twelf-to-twelf-sml-mode-map 2437,99332
(defun twelf-to-twelf-sml-mode 2448,99845
(defconst twelf-at-point-menu2498,101712
(defconst twelf-server-state-menu2508,102084
(defconst twelf-error-menu2518,102401
(defconst twelf-tags-menu2524,102545
(defun twelf-toggle-server-display-commands 2534,102830
(defconst twelf-options-menu2537,102954
(defconst twelf-timers-menu2572,104692
(defconst twelf-syntax-menu2585,105186
(defun twelf-add-menu 2612,106052
(defun twelf-remove-menu 2616,106154
(defun twelf-reset-menu 2620,106252
(defun twelf-server-add-menu 2647,107151
(defun twelf-server-remove-menu 2651,107274
(defun twelf-server-reset-menu 2655,107386

generic/pg-assoc.el,82
(defun proof-associated-buffers 36,1069
(defun proof-associated-windows 46,1281

generic/pg-autotest.el,442
(defvar pg-autotest-success 24,543
(defun pg-autotest-find-file 28,627
(defun pg-autotest-find-file-restart 35,907
(defmacro pg-autotest 48,1355
(defun pg-autotest-script-wholefile 62,1702
(defun pg-autotest-retract-file 79,2315
(defun pg-autotest-assert-processed 85,2451
(defun pg-autotest-assert-unprocessed 92,2705
(defun pg-autotest-message 99,2965
(defun pg-autotest-quit-prover 106,3158
(defun pg-autotest-finished 112,3339

generic/pg-custom.el,554
(defpgcustom maths-menu-enable 32,1069
(defpgcustom unicode-tokens-enable 38,1249
(defpgcustom mmm-enable 44,1426
(defpgcustom script-indent 53,1780
(defconst proof-toolbar-entries-default58,1917
(defpgcustom toolbar-entries 85,3576
(defpgcustom prog-args 104,4309
(defpgcustom prog-env 117,4884
(defpgcustom favourites 126,5310
(defpgcustom menu-entries 131,5499
(defpgcustom help-menu-entries 138,5735
(defpgcustom keymap 145,5998
(defpgcustom completion-table 150,6170
(defpgcustom tags-program 161,6544
(defpgcustom use-holes 170,6928

generic/pg-goals.el,287
(define-derived-mode proof-goals-mode 30,642
(define-key proof-goals-mode-map 59,1518
(define-key proof-goals-mode-map 61,1570
(define-key proof-goals-mode-map 62,1638
(define-key proof-goals-mode-map 68,2071
(defun proof-goals-config-done 76,2188
(defun pg-goals-display 84,2454

generic/pg-pbrpm.el,1803
(defvar pg-pbrpm-use-buffer-menu 22,551
(defvar pg-pbrpm-start-goal-regexp 25,673
(defvar pg-pbrpm-start-goal-regexp-par-num 29,830
(defvar pg-pbrpm-end-goal-regexp 32,953
(defvar pg-pbrpm-start-hyp-regexp 36,1105
(defvar pg-pbrpm-start-hyp-regexp-par-num 40,1266
(defvar pg-pbrpm-start-concl-regexp 44,1473
(defvar pg-pbrpm-auto-select-regexp 48,1637
(defvar pg-pbrpm-buffer-menu 55,1798
(defvar pg-pbrpm-spans 56,1832
(defvar pg-pbrpm-goal-description 57,1860
(defvar pg-pbrpm-windows-dialog-bug 58,1899
(defvar pbrpm-menu-desc 59,1940
(defun pg-pbrpm-erase-buffer-menu 61,1970
(defun pg-pbrpm-menu-change-hook 68,2154
(defun pg-pbrpm-create-reset-buffer-menu 86,2730
(defun pg-pbrpm-analyse-goal-buffer 101,3359
(defun pg-pbrpm-button-action 161,5769
(defun pg-pbrpm-exists 168,5995
(defun pg-pbrpm-eliminate-id 172,6107
(defun pg-pbrpm-build-menu 180,6353
(defun pg-pbrpm-setup-span 243,8679
(defun pg-pbrpm-run-command 303,10997
(defun pg-pbrpm-get-pos-info 332,12307
(defun pg-pbrpm-get-region-info 374,13614
(defun pg-pbrpm-auto-select-around-point 385,14028
(defun pg-pbrpm-translate-position 400,14558
(defun pg-pbrpm-process-click 408,14816
(defvar pg-pbrpm-remember-region-selected-region 428,15841
(defvar pg-pbrpm-regions-list 429,15895
(defun pg-pbrpm-erase-regions-list 431,15931
(defun pg-pbrpm-filter-regions-list 440,16239
(defface pg-pbrpm-multiple-selection-face447,16502
(defface pg-pbrpm-menu-input-face455,16704
(defun pg-pbrpm-do-remember-region 463,16894
(defun pg-pbrpm-remember-region-drag-up-hook 484,17742
(defun pg-pbrpm-remember-region-click-hook 488,17913
(defun pg-pbrpm-remember-region 493,18098
(defun pg-pbrpm-process-region 507,18813
(defun pg-pbrpm-process-regions-list 525,19542
(defun pg-pbrpm-region-expression 529,19725

generic/pg-pgip.el,2889
(defalias 'pg-pgip-debug pg-pgip-debug
35,919
(defalias 'pg-pgip-error pg-pgip-error
36,960
(defalias 'pg-pgip-warning pg-pgip-warning
37,995
(defconst pg-pgip-version-supported 39,1045
(defun pg-pgip-process-packet 43,1151
(defvar pg-pgip-last-seen-id 53,1723
(defvar pg-pgip-last-seen-seq 54,1757
(defun pg-pgip-process-pgip 56,1793
(defun pg-pgip-process-msg 75,2724
(defvar pg-pgip-post-process-functions89,3294
(defun pg-pgip-post-process 99,3782
(defun pg-pgip-process-askpgip 115,4393
(defun pg-pgip-process-usespgip 121,4598
(defun pg-pgip-process-usespgml 125,4762
(defun pg-pgip-process-pgmlconfig 129,4926
(defun pg-pgip-process-proverinfo 145,5543
(defun pg-pgip-process-hasprefs 162,6208
(defun pg-pgip-haspref 176,6840
(defun pg-pgip-process-prefval 195,7616
(defun pg-pgip-process-guiconfig 222,8325
(defvar proof-assistant-idtables 229,8442
(defun pg-pgip-process-ids 232,8559
(defun pg-complete-idtable-symbol 258,9635
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
263,9727
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
264,9783
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
265,9839
(defun pg-pgip-process-idvalue 268,9897
(defun pg-pgip-process-menuadd 280,10233
(defun pg-pgip-process-menudel 283,10276
(defun pg-pgip-process-ready 292,10509
(defun pg-pgip-process-cleardisplay 295,10550
(defun pg-pgip-process-proofstate 309,11007
(defun pg-pgip-process-normalresponse 313,11084
(defun pg-pgip-process-errorresponse 317,11208
(defun pg-pgip-process-scriptinsert 321,11331
(defun pg-pgip-process-metainforesponse 326,11465
(defun pg-pgip-process-informfileloaded 335,11706
(defun pg-pgip-process-informfileretracted 341,11972
(defun pg-pgip-process-brokerstatus 354,12449
(defun pg-pgip-process-proveravailmsg 357,12497
(defun pg-pgip-process-newprovermsg 360,12547
(defun pg-pgip-process-proverstatusmsg 363,12595
(defvar pg-pgip-srcids 372,12842
(defun pg-pgip-process-newfile 376,12949
(defun pg-pgip-process-filestatus 392,13537
(defun pg-pgip-process-newobj 412,14192
(defun pg-pgip-process-delobj 415,14234
(defun pg-pgip-process-objectstatus 418,14276
(defun pg-pgip-process-parsescript 432,14631
(defun pg-pgip-get-pgiptype 455,15506
(defun pg-pgip-default-for 475,16299
(defun pg-pgip-subst-for 488,16694
(defun pg-pgip-interpret-value 500,17037
(defun pg-pgip-interpret-choice 518,17722
(defun pg-pgip-string-of-command 549,18739
(defconst pg-pgip-id566,19500
(defvar pg-pgip-refseq 572,19780
(defvar pg-pgip-refid 574,19877
(defvar pg-pgip-seq 577,19969
(defun pg-pgip-assemble-packet 579,20033
(defun pg-pgip-issue 597,20845
(defun pg-pgip-maybe-askpgip 614,21457
(defun pg-pgip-askprefs 620,21648
(defun pg-pgip-askids 624,21762
(defun pg-pgip-reset 637,22050
(defconst pg-pgip-start-element-regexp 668,22748
(defconst pg-pgip-end-element-regexp 669,22800

generic/pg-response.el,1078
(deflocal pg-response-eagerly-raise 31,734
(define-derived-mode proof-response-mode 41,959
(defun proof-response-config-done 65,1969
(defvar pg-response-special-display-regexp 76,2316
(defconst proof-multiframe-parameters80,2483
(defun proof-multiple-frames-enable 89,2782
(defun proof-three-window-enable 99,3111
(defun proof-select-three-b 102,3174
(defun proof-display-three-b 117,3643
(defvar pg-frame-configuration 129,4052
(defun pg-cache-frame-configuration 133,4199
(defun proof-layout-windows 137,4370
(defun proof-delete-other-frames 177,6135
(defvar pg-response-erase-flag 208,7225
(defun pg-response-maybe-erase212,7354
(defun pg-response-display 243,8539
(defun pg-response-display-with-face 273,9627
(defun pg-response-clear-displays 299,10421
(defun proof-next-error 318,11008
(defun pg-response-has-error-location 399,13924
(defvar proof-trace-last-fontify-pos 422,14757
(defun proof-trace-fontify-pos 424,14800
(defun proof-trace-buffer-display 432,15113
(defun proof-trace-buffer-finish 457,16059
(defun pg-thms-buffer-clear 479,16630

generic/pg-thymodes.el,152
(defmacro pg-defthymode 23,503
(defmacro pg-do-unless-null 71,2314
(defun pg-symval 76,2401
(defun pg-modesym 82,2556
(defun pg-modesymval 86,2670

generic/pg-user.el,3075
(defmacro proof-maybe-save-point 31,810
(defun proof-maybe-follow-locked-end 41,1107
(defun proof-assert-next-command-interactive 55,1472
(defun proof-process-buffer 65,1843
(defun proof-undo-last-successful-command 79,2160
(defun proof-undo-and-delete-last-successful-command 84,2322
(defun proof-undo-last-successful-command-1 98,2885
(defun proof-retract-buffer 114,3450
(defun proof-retract-current-goal 123,3730
(defun proof-interrupt-process 142,4236
(defun proof-goto-command-start 169,5225
(defun proof-goto-command-end 192,6165
(defun proof-mouse-goto-point 213,6800
(defvar proof-minibuffer-history 229,7043
(defun proof-minibuffer-cmd 232,7138
(defun proof-frob-locked-end 276,8753
(defmacro proof-if-setting-configured 337,10681
(defmacro proof-define-assistant-command 345,10950
(defmacro proof-define-assistant-command-witharg 358,11405
(defun proof-issue-new-command 378,12228
(defun proof-cd-sync 422,13671
(defun proof-electric-terminator-enable 481,15436
(defun proof-electric-term-incomment-fn 489,15738
(defun proof-process-electric-terminator 509,16491
(defun proof-electric-terminator 536,17639
(defun proof-add-completions 558,18285
(defun proof-script-complete 578,19039
(defun pg-insert-last-output-as-comment 606,19630
(defun pg-copy-span-contents 625,20236
(defun pg-numth-span-higher-or-lower 642,20794
(defun pg-control-span-of 668,21540
(defun pg-move-span-contents 674,21744
(defun pg-fixup-children-spans 726,23924
(defun pg-move-region-down 736,24187
(defun pg-move-region-up 745,24480
(defun proof-forward-command 775,25318
(defun proof-backward-command 796,26039
(defun pg-pos-for-event 818,26390
(defun pg-span-for-event 824,26611
(defun pg-span-context-menu 828,26755
(defun pg-toggle-visibility 843,27210
(defun pg-create-in-span-context-menu 853,27532
(defun pg-span-undo 886,28876
(defun pg-goals-buffers-hint 932,30286
(defun pg-slow-fontify-tracing-hint 936,30468
(defun pg-response-buffers-hint 940,30639
(defun pg-jump-to-end-hint 950,31001
(defun pg-processing-complete-hint 954,31132
(defun pg-next-error-hint 971,31831
(defun pg-hint 976,31983
(defun pg-identifier-under-mouse-query 991,32517
(defun proof-imenu-enable 1032,34001
(defvar pg-input-ring 1063,35047
(defvar pg-input-ring-index 1066,35104
(defvar pg-stored-incomplete-input 1069,35176
(defun pg-previous-input 1072,35279
(defun pg-next-input 1086,35736
(defun pg-delete-input 1091,35858
(defun pg-get-old-input 1104,36196
(defun pg-restore-input 1118,36587
(defun pg-search-start 1129,36877
(defun pg-regexp-arg 1141,37369
(defun pg-search-arg 1153,37817
(defun pg-previous-matching-input-string-position 1167,38234
(defun pg-previous-matching-input 1194,39399
(defun pg-next-matching-input 1213,40249
(defvar pg-matching-input-from-input-string 1221,40632
(defun pg-previous-matching-input-from-input 1225,40746
(defun pg-next-matching-input-from-input 1243,41511
(defun pg-add-to-input-history 1254,41890
(defun pg-remove-from-input-history 1266,42343
(defun  pg-clear-input-ring 1277,42725

generic/pg-vars.el,1106
(defvar proof-assistant-cusgrp 20,379
(defvar proof-assistant-internals-cusgrp 26,641
(defvar proof-assistant 32,912
(defvar proof-assistant-symbol 37,1134
(defvar proof-mode-for-shell 50,1678
(defvar proof-mode-for-response 55,1870
(defvar proof-mode-for-goals 60,2097
(defvar proof-mode-for-script 65,2287
(defvar proof-ready-for-assistant-hook 70,2465
(defvar proof-shell-busy 80,2752
(defvar proof-included-files-list 85,2908
(defvar proof-script-buffer 107,3921
(defvar proof-previous-script-buffer 110,4013
(defvar proof-shell-buffer 114,4184
(defvar proof-goals-buffer 117,4270
(defvar proof-response-buffer 120,4325
(defvar proof-trace-buffer 123,4386
(defvar proof-thms-buffer 127,4540
(defvar proof-shell-error-or-interrupt-seen 131,4695
(defvar pg-response-next-error 136,4919
(defvar proof-shell-proof-completed 139,5026
(defvar proof-terminal-string 151,5570
(defvar proof-shell-last-output 161,5760
(defvar proof-assistant-settings 165,5901
(defvar pg-tracing-slow-mode 172,6264
(defvar proof-nesting-depth 175,6353
(defvar proof-last-theorem-dependencies 182,6588

generic/pg-xml.el,1140
(defalias 'pg-xml-error pg-xml-error
16,369
(defun pg-xml-parse-string 39,1011
(defun pg-xml-parse-buffer 50,1337
(defun pg-xml-get-attr 72,2070
(defun pg-xml-child-elts 80,2372
(defun pg-xml-child-elt 85,2577
(defun pg-xml-get-child 93,2859
(defun pg-xml-get-text-content 103,3231
(defmacro pg-xml-attr 114,3581
(defmacro pg-xml-node 116,3643
(defconst pg-xml-header119,3735
(defun pg-xml-string-of 123,3811
(defun pg-xml-output-internal 134,4178
(defun pg-xml-cdata 168,5328
(defun pg-pgip-get-icon 176,5521
(defsubst pg-pgip-get-name 180,5669
(defsubst pg-pgip-get-version 183,5786
(defsubst pg-pgip-get-descr 186,5909
(defsubst pg-pgip-get-thmname 189,6028
(defsubst pg-pgip-get-thyname 192,6151
(defsubst pg-pgip-get-url 195,6274
(defsubst pg-pgip-get-srcid 198,6389
(defsubst pg-pgip-get-proverid 201,6508
(defsubst pg-pgip-get-symname 204,6633
(defsubst pg-pgip-get-prefcat 207,6753
(defsubst pg-pgip-get-default 210,6881
(defsubst pg-pgip-get-objtype 213,7004
(defsubst pg-pgip-get-value 216,7127
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
219,7197
(defun pg-pgip-get-pgmltext 221,7256

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 63,1729

generic/proof-config.el,10808
(defgroup proof-user-options 88,3074
(defun proof-set-value 96,3253
(defcustom proof-electric-terminator-enable 129,4376
(defcustom proof-toolbar-enable 141,4908
(defcustom proof-imenu-enable 147,5081
(defcustom pg-show-hints 153,5252
(defcustom proof-trace-output-slow-catchup 159,5447
(defcustom proof-strict-state-preserving 169,5944
(defcustom proof-strict-read-only 182,6553
(defcustom proof-allow-undo-in-read-only 191,6946
(defcustom proof-three-window-enable 199,7279
(defcustom proof-multiple-frames-enable 218,8029
(defcustom proof-delete-empty-windows 227,8362
(defcustom proof-shrink-windows-tofit 238,8893
(defcustom proof-query-file-save-when-activating-scripting245,9165
(defcustom proof-one-command-per-line261,9885
(defcustom proof-prog-name-ask268,10112
(defcustom proof-prog-name-guess274,10272
(defcustom proof-tidy-response282,10537
(defcustom proof-keep-response-history296,11000
(defcustom pg-input-ring-size 306,11388
(defcustom proof-general-debug 311,11540
(defcustom proof-experimental-features 321,11912
(defcustom proof-follow-mode 335,12447
(defcustom proof-auto-action-when-deactivating-scripting 359,13624
(defcustom proof-script-command-separator 382,14573
(defcustom proof-rsh-command 390,14865
(defcustom proof-disappearing-proofs 406,15415
(defgroup proof-faces 433,16061
(defconst pg-defface-window-systems440,16243
(defmacro proof-face-specs 453,16796
(defface proof-queue-face468,17248
(defface proof-locked-face476,17526
(defface proof-declaration-name-face489,18029
(defface proof-tacticals-name-face498,18315
(defface proof-tactics-name-face507,18577
(defface proof-error-face516,18842
(defface proof-warning-face524,19032
(defface proof-eager-annotation-face533,19289
(defface proof-debug-message-face541,19507
(defface proof-boring-face549,19706
(defface proof-mouse-highlight-face557,19898
(defface proof-highlight-dependent-face565,20094
(defface proof-highlight-dependency-face573,20303
(defface proof-active-area-face581,20500
(defconst proof-face-compat-doc 590,20890
(defconst proof-queue-face 591,20970
(defconst proof-locked-face 592,21038
(defconst proof-declaration-name-face 593,21108
(defconst proof-tacticals-name-face 594,21198
(defconst proof-tactics-name-face 595,21284
(defconst proof-error-face 596,21366
(defconst proof-warning-face 597,21434
(defconst proof-eager-annotation-face 598,21506
(defconst proof-debug-message-face 599,21596
(defconst proof-boring-face 600,21680
(defconst proof-mouse-highlight-face 601,21750
(defconst proof-highlight-dependent-face 602,21838
(defconst proof-highlight-dependency-face 603,21934
(defconst proof-active-area-face 604,22032
(defgroup prover-config 617,22176
(defcustom proof-guess-command-line 659,23505
(defcustom proof-assistant-home-page 674,24000
(defcustom proof-context-command 680,24170
(defcustom proof-info-command 685,24304
(defcustom proof-showproof-command 692,24575
(defcustom proof-goal-command 697,24711
(defcustom proof-save-command 705,25008
(defcustom proof-find-theorems-command 713,25317
(defcustom proof-assistant-true-value 720,25627
(defcustom proof-assistant-false-value 726,25817
(defcustom proof-assistant-format-int-fn 732,26011
(defcustom proof-assistant-format-string-fn 739,26260
(defcustom proof-assistant-setting-format 746,26527
(defgroup proof-script 768,27222
(defcustom proof-terminal-char 773,27352
(defcustom proof-script-sexp-commands 783,27739
(defcustom proof-script-command-end-regexp 794,28196
(defcustom proof-script-command-start-regexp 812,29015
(defcustom proof-script-use-old-parser 823,29476
(defcustom proof-script-integral-proofs 835,29962
(defcustom proof-script-fly-past-comments 850,30618
(defcustom proof-script-parse-function 855,30789
(defcustom proof-script-comment-start 873,31432
(defcustom proof-script-comment-start-regexp 884,31869
(defcustom proof-script-comment-end 892,32188
(defcustom proof-script-comment-end-regexp 904,32610
(defcustom pg-insert-output-as-comment-fn 912,32921
(defcustom proof-string-start-regexp 918,33173
(defcustom proof-string-end-regexp 923,33338
(defcustom proof-case-fold-search 928,33499
(defcustom proof-save-command-regexp 937,33911
(defcustom proof-save-with-hole-regexp 942,34021
(defcustom proof-save-with-hole-result 954,34475
(defcustom proof-goal-command-regexp 964,34923
(defcustom proof-goal-with-hole-regexp 973,35311
(defcustom proof-goal-with-hole-result 985,35754
(defcustom proof-non-undoables-regexp 994,36138
(defcustom proof-nested-undo-regexp 1005,36593
(defcustom proof-ignore-for-undo-count 1021,37305
(defcustom proof-script-next-entity-regexps 1029,37608
(defcustom proof-script-find-next-entity-fn1073,39349
(defcustom proof-script-imenu-generic-expression 1093,40189
(defcustom proof-goal-command-p 1101,40528
(defcustom proof-really-save-command-p 1112,41019
(defcustom proof-completed-proof-behaviour 1121,41326
(defcustom proof-count-undos-fn 1149,42682
(defconst proof-no-command 1161,43231
(defcustom proof-find-and-forget-fn 1166,43438
(defcustom proof-forget-id-command 1183,44152
(defcustom pg-topterm-goalhyplit-fn 1193,44510
(defcustom proof-kill-goal-command 1205,45045
(defcustom proof-undo-n-times-cmd 1219,45548
(defcustom proof-nested-goals-history-p 1233,46096
(defcustom proof-state-preserving-p 1242,46433
(defcustom proof-activate-scripting-hook 1252,46905
(defcustom proof-deactivate-scripting-hook 1271,47686
(defcustom proof-indent 1284,48051
(defcustom proof-indent-hang 1289,48158
(defcustom proof-indent-enclose-offset 1294,48284
(defcustom proof-indent-open-offset 1299,48426
(defcustom proof-indent-close-offset 1304,48563
(defcustom proof-indent-any-regexp 1309,48701
(defcustom proof-indent-inner-regexp 1314,48861
(defcustom proof-indent-enclose-regexp 1319,49015
(defcustom proof-indent-open-regexp 1324,49169
(defcustom proof-indent-close-regexp 1329,49321
(defcustom proof-script-font-lock-keywords 1335,49475
(defcustom proof-script-syntax-table-entries 1343,49792
(defcustom proof-script-span-context-menu-extensions 1361,50189
(defgroup proof-shell 1387,50949
(defcustom proof-prog-name 1397,51120
(defcustom proof-shell-auto-terminate-commands 1408,51540
(defcustom proof-shell-pre-sync-init-cmd 1417,51941
(defcustom proof-shell-init-cmd 1431,52499
(defcustom proof-shell-init-hook 1443,53028
(defcustom proof-shell-restart-cmd 1448,53167
(defcustom proof-shell-quit-cmd 1453,53322
(defcustom proof-shell-quit-timeout 1458,53489
(defcustom proof-shell-cd-cmd 1468,53939
(defcustom proof-shell-start-silent-cmd 1485,54610
(defcustom proof-shell-stop-silent-cmd 1494,54986
(defcustom proof-shell-silent-threshold 1503,55321
(defcustom  proof-shell-inform-file-processed-cmd 1511,55655
(defcustom  proof-shell-inform-file-retracted-cmd 1532,56583
(defcustom proof-auto-multiple-files 1560,57855
(defcustom proof-cannot-reopen-processed-files 1575,58576
(defcustom proof-shell-require-command-regexp 1589,59242
(defcustom proof-done-advancing-require-function 1600,59704
(defcustom proof-shell-quiet-errors 1606,59939
(defcustom proof-shell-prompt-pattern 1619,60273
(defcustom proof-shell-wakeup-char 1629,60694
(defcustom proof-shell-annotated-prompt-regexp 1635,60925
(defcustom proof-shell-abort-goal-regexp 1651,61561
(defcustom proof-shell-error-regexp 1656,61696
(defcustom proof-shell-truncate-before-error 1676,62496
(defcustom pg-next-error-regexp 1690,63035
(defcustom pg-next-error-filename-regexp 1705,63644
(defcustom pg-next-error-extract-filename 1729,64677
(defcustom proof-shell-interrupt-regexp 1736,64920
(defcustom proof-shell-proof-completed-regexp 1750,65515
(defcustom proof-shell-clear-response-regexp 1763,66023
(defcustom proof-shell-clear-goals-regexp 1770,66322
(defcustom proof-shell-start-goals-regexp 1777,66615
(defcustom proof-shell-end-goals-regexp 1785,66982
(defcustom proof-shell-eager-annotation-start 1791,67226
(defcustom proof-shell-eager-annotation-start-length 1814,68245
(defcustom proof-shell-eager-annotation-end 1825,68671
(defcustom proof-shell-assumption-regexp 1841,69346
(defcustom proof-shell-process-file 1851,69749
(defcustom proof-shell-retract-files-regexp 1873,70705
(defcustom proof-shell-compute-new-files-list 1882,71041
(defcustom pg-use-specials-for-fontify 1894,71589
(defcustom pg-special-char-regexp 1902,71937
(defcustom proof-shell-set-elisp-variable-regexp 1908,72082
(defcustom proof-shell-match-pgip-cmd 1941,73595
(defcustom proof-shell-issue-pgip-cmd 1950,73924
(defcustom proof-shell-query-dependencies-cmd 1959,74280
(defcustom proof-shell-theorem-dependency-list-regexp 1966,74540
(defcustom proof-shell-theorem-dependency-list-split 1982,75200
(defcustom proof-shell-show-dependency-cmd 1991,75623
(defcustom proof-shell-identifier-under-mouse-cmd 1998,75892
(defcustom proof-shell-trace-output-regexp 2021,76973
(defcustom proof-shell-thms-output-regexp 2035,77431
(defcustom proof-tokens-activate-command 2048,77814
(defcustom proof-tokens-deactivate-command 2055,78055
(defcustom proof-tokens-extra-modes 2062,78302
(defcustom proof-shell-unicode 2077,78809
(defcustom proof-shell-filename-escapes 2085,79129
(defcustom proof-shell-process-connection-type2102,79809
(defcustom proof-shell-strip-crs-from-input 2125,80855
(defcustom proof-shell-strip-crs-from-output 2137,81340
(defcustom proof-shell-insert-hook 2145,81708
(defcustom proof-shell-handle-delayed-output-hook2183,83568
(defcustom proof-shell-handle-error-or-interrupt-hook2189,83783
(defcustom proof-shell-pre-interrupt-hook2207,84536
(defcustom proof-shell-process-output-system-specific 2215,84807
(defcustom proof-state-change-hook 2234,85671
(defcustom proof-shell-syntax-table-entries 2244,86052
(defgroup proof-goals 2262,86424
(defcustom pg-subterm-first-special-char 2267,86545
(defcustom pg-subterm-anns-use-stack 2275,86857
(defcustom pg-goals-change-goal 2284,87156
(defcustom pbp-goal-command 2289,87272
(defcustom pbp-hyp-command 2294,87428
(defcustom pg-subterm-help-cmd 2299,87590
(defcustom pg-goals-error-regexp 2306,87826
(defcustom proof-shell-result-start 2311,87986
(defcustom proof-shell-result-end 2317,88220
(defcustom pg-subterm-start-char 2323,88433
(defcustom pg-subterm-sep-char 2337,89019
(defcustom pg-subterm-end-char 2343,89198
(defcustom pg-topterm-regexp 2349,89355
(defcustom proof-goals-font-lock-keywords 2364,89955
(defcustom proof-resp-font-lock-keywords 2372,90282
(defcustom pg-before-fontify-output-hook 2380,90611
(defcustom pg-after-fontify-output-hook 2388,90972
(defcustom proof-general-name 2400,91221
(defcustom proof-general-home-page2405,91378
(defcustom proof-unnamed-theorem-name2411,91538
(defcustom proof-universal-keys2417,91722

generic/proof-depends.el,824
(defvar proof-thm-names-of-files 23,624
(defvar proof-def-names-of-files 29,908
(defun proof-depends-module-name-for-buffer 38,1212
(defun proof-depends-module-of 48,1654
(defun proof-depends-names-in-same-file 56,1948
(defun proof-depends-process-dependencies 75,2568
(defun proof-dependency-in-span-context-menu 128,4317
(defun proof-dep-alldeps-menu 151,5220
(defun proof-dep-make-alldeps-menu 157,5447
(defun proof-dep-split-deps 175,5943
(defun proof-dep-make-submenu 196,6642
(defun proof-make-highlight-depts-menu 206,6995
(defun proof-goto-dependency 216,7299
(defun proof-show-dependency 222,7522
(defconst pg-dep-span-priority 229,7812
(defconst pg-ordinary-span-priority 230,7848
(defun proof-highlight-depcs 232,7890
(defun proof-highlight-depts 242,8320
(defun proof-dep-unhighlight 253,8794

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table16,547
(defun proof-easy-config-define-derived-modes 23,953
(defun proof-easy-config-check-setup 52,2136
(defmacro proof-easy-config 84,3471

generic/proof-indent.el,219
(defun proof-indent-indent 14,411
(defun proof-indent-offset 23,677
(defun proof-indent-inner-p 40,1277
(defun proof-indent-goto-prev 49,1584
(defun proof-indent-calculate 56,1917
(defun proof-indent-line 76,2639

generic/proof-maths-menu.el,83
(defun proof-maths-menu-set-global 30,962
(defun proof-maths-menu-enable 44,1418

generic/proof-menu.el,2100
(defvar proof-display-some-buffers-count 17,440
(defun proof-display-some-buffers 19,485
(defun proof-menu-define-keys 78,2687
(defun proof-menu-define-main 137,5516
(defvar proof-menu-favourites 146,5704
(defun proof-menu-define-specific 150,5826
(defun proof-assistant-menu-update 188,6844
(defvar proof-help-menu202,7277
(defvar proof-show-hide-menu210,7555
(defvar proof-buffer-menu219,7868
(defun proof-keep-response-history 278,9954
(defconst proof-quick-opts-menu286,10264
(defun proof-quick-opts-vars 435,16396
(defun proof-quick-opts-changed-from-defaults-p 460,17153
(defun proof-quick-opts-changed-from-saved-p 464,17258
(defun proof-quick-opts-save 475,17610
(defun proof-quick-opts-reset 480,17778
(defconst proof-config-menu492,18046
(defconst proof-advanced-menu499,18225
(defvar proof-menu 512,18660
(defun proof-main-menu 521,18944
(defun proof-aux-menu 532,19210
(defun proof-menu-define-favourites-menu 548,19557
(defun proof-def-favourite 568,20213
(defvar proof-make-favourite-cmd-history 591,21188
(defvar proof-make-favourite-menu-history 594,21273
(defun proof-save-favourites 597,21359
(defun proof-del-favourite 602,21507
(defun proof-read-favourite 619,22068
(defun proof-add-favourite 644,22871
(defvar proof-menu-settings 671,23922
(defun proof-menu-define-settings-menu 674,23996
(defun proof-menu-entry-name 694,24740
(defun proof-menu-entry-for-setting 706,25212
(defun proof-settings-vars 724,25702
(defun proof-settings-changed-from-defaults-p 729,25879
(defun proof-settings-changed-from-saved-p 733,25985
(defun proof-settings-save 737,26088
(defun proof-settings-reset 742,26255
(defun proof-defpacustom-fn 749,26500
(defmacro defpacustom 825,29391
(defun proof-assistant-invisible-command-ifposs 840,30218
(defun proof-maybe-askprefs 862,31193
(defun proof-assistant-settings-cmd 869,31397
(defvar proof-assistant-format-table 886,32057
(defun proof-assistant-format-bool 894,32426
(defun proof-assistant-format-int 897,32539
(defun proof-assistant-format-string 900,32631
(defun proof-assistant-format 903,32729

generic/proof-mmm.el,70
(defun proof-mmm-set-global 41,1516
(defun proof-mmm-enable 56,2057

generic/proof-script.el,5199
(defvar proof-element-counters 28,717
(deflocal proof-active-buffer-fake-minor-mode 34,857
(deflocal proof-script-buffer-file-name 37,983
(deflocal pg-script-portions 44,1393
(defun proof-next-element-count 54,1629
(defun proof-element-id 63,1964
(defun proof-next-element-id 67,2133
(deflocal proof-script-last-entity 81,2450
(defun proof-script-find-next-entity 88,2730
(deflocal proof-locked-span 164,5472
(deflocal proof-queue-span 171,5738
(defun proof-span-give-warning 183,6252
(defun proof-span-read-only 187,6366
(defun proof-strict-read-only 196,6798
(defsubst proof-set-locked-endpoints 234,8529
(defsubst proof-detach-queue 238,8673
(defsubst proof-detach-locked 242,8805
(defsubst proof-set-queue-start 246,8941
(defsubst proof-set-locked-end 250,9067
(defsubst proof-set-queue-end 263,9552
(defun proof-init-segmentation 274,9849
(defun proof-restart-buffers 307,11244
(defun proof-script-buffers-with-spans 329,12176
(defun proof-script-remove-all-spans-and-deactivate 339,12532
(defun proof-script-clear-queue-spans 343,12720
(defun proof-unprocessed-begin 362,13281
(defun proof-script-end 370,13535
(defun proof-queue-or-locked-end 379,13836
(defun proof-locked-end 394,14514
(defun proof-locked-region-full-p 411,14899
(defun proof-locked-region-empty-p 420,15171
(defun proof-only-whitespace-to-locked-region-p 424,15321
(defun proof-in-locked-region-p 437,15957
(defun proof-goto-end-of-locked 449,16220
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 466,16979
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 477,17460
(defun proof-end-of-locked-visible-p 491,18113
(defun proof-goto-end-of-queue-or-locked-if-not-visible 500,18564
(defvar pg-idioms 519,19214
(defvar pg-visibility-specs 522,19310
(defconst pg-default-invisibility-spec 527,19517
(defun pg-clear-script-portions 531,19657
(defun pg-add-script-element 538,19905
(defun pg-remove-script-element 541,19981
(defsubst pg-visname 549,20275
(defun pg-add-element 553,20420
(defun pg-open-invisible-span 587,22049
(defun pg-remove-element 598,22412
(defun pg-make-element-invisible 605,22682
(defun pg-make-element-visible 611,22926
(defun pg-toggle-element-visibility 615,23069
(defun pg-redisplay-for-gnuemacs 622,23356
(defun pg-show-all-portions 626,23502
(defun pg-show-all-proofs 644,24173
(defun pg-hide-all-proofs 649,24301
(defun pg-add-proof-element 654,24432
(defun pg-span-name 668,25052
(defvar pg-span-context-menu-keymap689,25759
(defun pg-set-span-helphighlights 698,26013
(defun proof-complete-buffer-atomic 724,26880
(defun proof-register-possibly-new-processed-file 765,28795
(defun proof-inform-prover-file-retracted 816,30923
(defun proof-auto-retract-dependencies 835,31709
(defun proof-unregister-buffer-file-name 889,34249
(defun proof-protected-process-or-retract 935,36072
(defun proof-deactivate-scripting-auto 962,37242
(defun proof-deactivate-scripting 971,37600
(defun proof-activate-scripting 1104,42873
(defun proof-toggle-active-scripting 1224,48251
(defun proof-done-advancing 1265,49612
(defun proof-done-advancing-comment 1360,53260
(defun proof-done-advancing-save 1379,54002
(defun proof-make-goalsave 1472,57617
(defun proof-get-name-from-goal 1487,58360
(defun proof-done-advancing-autosave 1506,59386
(defun proof-done-advancing-other 1571,61932
(defun proof-segment-up-to-parser 1599,62891
(defun proof-script-generic-parse-find-comment-end 1663,64961
(defun proof-script-generic-parse-cmdend 1672,65377
(defun proof-script-generic-parse-cmdstart 1697,66272
(defun proof-script-generic-parse-sexp 1760,68980
(defun proof-cmdstart-add-segment-for-cmd 1784,69916
(defun proof-segment-up-to-cmdstart 1836,72115
(defun proof-segment-up-to-cmdend 1897,74475
(defun proof-semis-to-vanillas 1969,77140
(defun proof-script-new-command-advance 2008,78466
(defun proof-script-next-command-advance 2050,80207
(defun proof-assert-until-point-interactive 2062,80648
(defun proof-assert-until-point 2088,81770
(defun proof-assert-next-command2141,84202
(defun proof-retract-before-change 2189,86440
(defun proof-goto-point 2196,86659
(defun proof-insert-pbp-command 2214,87200
(defun proof-insert-sendback-command 2228,87669
(defun proof-done-retracting 2254,88559
(defun proof-setup-retract-action 2290,90045
(defun proof-last-goal-or-goalsave 2300,90528
(defun proof-retract-target 2323,91368
(defun proof-retract-until-point-interactive 2408,95009
(defun proof-retract-until-point 2416,95394
(define-derived-mode proof-mode 2459,97143
(defun proof-script-set-visited-file-name 2492,98368
(defun proof-script-set-buffer-hooks 2516,99370
(defun proof-script-kill-buffer-fn 2524,99788
(defun proof-config-done-related 2556,101102
(defun proof-generic-goal-command-p 2624,103630
(defun proof-generic-state-preserving-p 2629,103842
(defun proof-generic-count-undos 2638,104359
(defun proof-generic-find-and-forget 2667,105389
(defconst proof-script-important-settings2718,107214
(defun proof-config-done 2733,107767
(defun proof-setup-parsing-mechanism 2802,110073
(defun proof-setup-imenu 2846,111926
(defun proof-setup-func-menu 2863,112531

generic/proof-shell.el,3159
(defvar proof-marker 28,653
(defvar proof-action-list 31,750
(defvar proof-shell-silent 39,926
(defvar proof-shell-last-prompt 46,1217
(defvar proof-shell-last-output-kind 50,1388
(defvar proof-shell-delayed-output 71,2210
(defvar proof-shell-delayed-output-kind 74,2331
(defcustom proof-shell-active-scripting-indicator83,2534
(defun proof-shell-ready-prover 133,3925
(defun proof-shell-live-buffer 147,4465
(defun proof-shell-available-p 154,4700
(defun proof-grab-lock 160,4923
(defun proof-release-lock 172,5482
(defcustom proof-shell-fiddle-frames 187,5881
(defun proof-shell-set-text-representation 193,6104
(defun proof-shell-start 204,6566
(defvar proof-shell-kill-function-hooks 405,13770
(defun proof-shell-kill-function 408,13868
(defun proof-shell-clear-state 497,17671
(defun proof-shell-exit 512,18114
(defun proof-shell-bail-out 524,18559
(defun proof-shell-restart 533,19036
(defvar proof-shell-no-response-display 575,20420
(defvar proof-shell-urgent-message-marker 578,20524
(defvar proof-shell-urgent-message-scanner 581,20645
(defun proof-shell-handle-output 585,20772
(defun proof-shell-handle-delayed-output 620,22091
(defvar proof-shell-no-error-display 648,23134
(defun proof-shell-handle-error 654,23338
(defun proof-shell-handle-interrupt 670,24071
(defun proof-shell-error-or-interrupt-action 684,24684
(defun proof-goals-pos 709,25829
(defun proof-pbp-focus-on-first-goal 714,26034
(defsubst proof-shell-string-match-safe 726,26461
(defun proof-shell-process-output 731,26629
(defun proof-shell-insert 843,31284
(defun proof-shell-command-queue-item 896,33385
(defun proof-shell-set-silent 901,33542
(defun proof-shell-start-silent-item 907,33761
(defun proof-shell-clear-silent 913,33953
(defun proof-shell-stop-silent-item 919,34175
(defun proof-shell-should-be-silent 926,34447
(defun proof-append-alist 939,35003
(defun proof-start-queue 998,37240
(defun proof-extend-queue 1009,37589
(defun proof-shell-exec-loop 1018,37968
(defun proof-shell-insert-loopback-cmd 1083,40556
(defun proof-shell-message 1111,41882
(defun proof-shell-process-urgent-message 1117,42098
(defun proof-shell-strip-eager-annotations 1244,47164
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1255,47500
(defun proof-shell-minibuffer-urgent-interactive-input 1257,47570
(defun proof-shell-process-urgent-messages 1267,47929
(defun proof-shell-filter 1341,51033
(defun proof-shell-filter-process-output 1497,57397
(defvar pg-last-tracing-output-time 1550,59451
(defconst pg-slow-mode-duration 1553,59557
(defconst pg-fast-tracing-mode-threshold 1556,59639
(defvar pg-tracing-cleanup-timer 1559,59767
(defun pg-tracing-tight-loop 1561,59806
(defun pg-finish-tracing-display 1604,61524
(defun proof-shell-wait 1626,61894
(defun proof-done-invisible 1645,62803
(defun proof-shell-invisible-command 1651,62975
(defun proof-shell-invisible-cmd-get-result 1685,64240
(defun proof-shell-invisible-command-invisible-result 1703,64936
(define-derived-mode proof-shell-mode 1722,65366
(defconst proof-shell-important-settings1777,67537
(defun proof-shell-config-done 1783,67652

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,761
(defcustom proof-splash-enable 17,323
(defcustom proof-splash-time 22,475
(defcustom proof-splash-contents30,760
(defconst proof-splash-startup-msg 58,1779
(defconst proof-splash-welcome 67,2158
(defsubst proof-emacs-imagep 74,2333
(defun proof-get-image 79,2458
(defvar proof-splash-timeout-conf 104,3418
(defun proof-splash-centre-spaces 107,3531
(defun proof-splash-remove-screen 132,4617
(defun proof-splash-remove-buffer 149,5273
(defvar proof-splash-seen 165,5937
(defun proof-splash-display-screen 169,6054
(defun proof-splash-message 236,8891
(defun proof-splash-timeout-waiter 249,9335
(defvar proof-splash-old-frame-title-format 262,9893
(defun proof-splash-set-frame-titles 264,9943
(defun proof-splash-unset-frame-titles 273,10259

generic/proof-syntax.el,981
(defun proof-ids-to-regexp 15,435
(defun proof-anchor-regexp 19,604
(defconst proof-no-regexp23,706
(defun proof-regexp-alt 28,799
(defun proof-regexp-region 37,1085
(defun proof-re-search-forward-region 46,1508
(defun proof-search-forward 59,2003
(defun proof-replace-regexp-in-string 65,2255
(defun proof-re-search-forward 71,2509
(defun proof-re-search-backward 77,2770
(defun proof-string-match 83,3034
(defun proof-string-match-safe 89,3266
(defun proof-stringfn-match 93,3471
(defun proof-looking-at 100,3731
(defun proof-looking-at-safe 106,3921
(defun proof-looking-at-syntactic-context 110,4061
(defsubst proof-replace-string 122,4424
(defsubst proof-replace-regexp 127,4628
(defsubst proof-replace-regexp-nocasefold 132,4837
(defvar proof-id 140,5119
(defun proof-ids 146,5339
(defun proof-zap-commas 159,5895
(defun proof-format 175,6391
(defun proof-format-filename 194,7030
(defun proof-insert 241,8430
(defun proof-splice-separator 278,9446

generic/proof-toolbar.el,2290
(defun proof-toolbar-function 35,842
(defun proof-toolbar-icon 38,939
(defun proof-toolbar-enabler 41,1040
(defun proof-toolbar-make-icon 48,1193
(defun proof-toolbar-make-toolbar-items 57,1501
(defvar proof-toolbar-map 82,2307
(defun proof-toolbar-available-p 85,2406
(defun proof-toolbar-setup 94,2682
(defalias 'proof-toolbar-enable proof-toolbar-enable
112,3473
(defalias 'proof-toolbar-undo proof-toolbar-undo
142,4453
(defun proof-toolbar-undo-enable-p 144,4521
(defalias 'proof-toolbar-delete proof-toolbar-delete
151,4679
(defun proof-toolbar-delete-enable-p 153,4760
(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
161,4947
(defalias 'proof-toolbar-next proof-toolbar-next
165,5019
(defun proof-toolbar-next-enable-p 167,5090
(defalias 'proof-toolbar-goto proof-toolbar-goto
173,5206
(defun proof-toolbar-goto-enable-p 175,5256
(defalias 'proof-toolbar-retract proof-toolbar-retract
180,5341
(defun proof-toolbar-retract-enable-p 182,5398
(defalias 'proof-toolbar-use proof-toolbar-use
188,5517
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
189,5569
(defalias 'proof-toolbar-restart proof-toolbar-restart
193,5650
(defalias 'proof-toolbar-goal proof-toolbar-goal
197,5715
(defalias 'proof-toolbar-qed proof-toolbar-qed
201,5773
(defun proof-toolbar-qed-enable-p 203,5822
(defalias 'proof-toolbar-state proof-toolbar-state
211,5984
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
212,6027
(defalias 'proof-toolbar-context proof-toolbar-context
216,6106
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
217,6152
(defalias 'proof-toolbar-info proof-toolbar-info
221,6230
(defalias 'proof-toolbar-command proof-toolbar-command
225,6286
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
226,6342
(defun proof-toolbar-help 230,6421
(defalias 'proof-toolbar-find proof-toolbar-find
236,6502
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
237,6554
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
241,6652
(defun proof-toolbar-visibility-enable-p 243,6712
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
248,6826
(defun proof-toolbar-interrupt-enable-p 249,6887
(defun proof-toolbar-scripting-menu 257,7040

generic/proof-unicode-tokens.el,496
(defvar proof-unicode-tokens-initialised 28,764
(defun proof-unicode-tokens-init 31,871
(defun proof-unicode-tokens-configure 45,1373
(defun proof-unicode-tokens-enable 58,1837
(defun proof-unicode-tokens-mode-if-enabled 72,2524
(defun proof-unicode-tokens-set-global 78,2723
(defun proof-unicode-tokens-reconfigure 96,3363
(defun proof-unicode-tokens-configure-prover 121,4207
(defun proof-unicode-tokens-activate-prover 126,4388
(defun proof-unicode-tokens-deactivate-prover 133,4634

generic/proof-utils.el,1873
(defmacro deflocal 62,1815
(defmacro proof-with-current-buffer-if-exists 69,2053
(deflocal proof-buffer-type 75,2263
(defmacro proof-with-script-buffer 81,2543
(defmacro proof-map-buffers 92,2930
(defmacro proof-sym 97,3115
(defsubst proof-try-require 102,3276
(defun proof-save-some-buffers 115,3607
(defmacro proof-ass-sym 164,5208
(defmacro proof-ass-symv 170,5467
(defmacro proof-ass 176,5725
(defun proof-defpgcustom-fn 182,5977
(defun undefpgcustom 203,6848
(defmacro defpgcustom 209,7072
(defun proof-defpgdefault-fn 220,7490
(defmacro defpgdefault 234,7948
(defmacro defpgfun 245,8310
(defmacro proof-eval-when-ready-for-assistant 255,8575
(defun proof-file-truename 268,8970
(defun proof-file-to-buffer 272,9153
(defun proof-files-to-buffers 283,9482
(defun proof-buffers-in-mode 290,9765
(defun pg-save-from-death 304,10215
(defun proof-define-keys 323,10832
(defun pg-remove-specials 334,11124
(defun pg-remove-specials-in-string 344,11462
(defun proof-warn-if-unset 355,11690
(defun proof-get-window-for-buffer 360,11908
(defun proof-display-and-keep-buffer 411,14216
(defun proof-clean-buffer 452,16056
(defun proof-message 467,16677
(defun proof-warning 472,16890
(defun pg-internal-warning 478,17172
(defun proof-debug 486,17491
(defun proof-switch-to-buffer 495,17841
(defun proof-resize-window-tofit 517,18967
(defun proof-submit-bug-report 611,23142
(defun proof-deftoggle-fn 646,24499
(defmacro proof-deftoggle 661,25152
(defun proof-defintset-fn 668,25526
(defmacro proof-defintset 684,26230
(defun proof-defstringset-fn 691,26607
(defmacro proof-defstringset 704,27233
(defun proof-escape-keymap-doc 717,27689
(defmacro proof-defshortcut 721,27822
(defmacro proof-definvisible 736,28420
(defun pg-custom-save-vars 764,29397
(defun pg-custom-reset-vars 782,30120
(defun proof-locate-executable 795,30457

lib/bufhist.el,1099
(defun bufhist-ring-update 32,1230
(defgroup bufhist 41,1552
(defcustom bufhist-ring-size 45,1633
(defvar bufhist-ring 50,1744
(defvar bufhist-ring-pos 53,1818
(defvar bufhist-lastswitch-modified-tick 56,1897
(defvar bufhist-read-only-history 59,2003
(defvar bufhist-saved-mode-line-format 62,2074
(defun bufhist-mode-line-format-entry 65,2175
(defun bufhist-get-buffer-contents 97,3451
(defun bufhist-restore-buffer-contents 109,3935
(defun bufhist-checkpoint 117,4222
(defun bufhist-erase-buffer 125,4591
(defun bufhist-checkpoint-and-erase 135,4936
(defun bufhist-switch-to-index 141,5122
(defun bufhist-first 180,6726
(defun bufhist-last 185,6885
(defun bufhist-prev 190,7031
(defun bufhist-next 198,7254
(defun bufhist-delete 203,7394
(defun bufhist-clear 215,7937
(defun bufhist-init 230,8333
(defun bufhist-exit 255,9270
(defun bufhist-set-readwrite 265,9534
(defun bufhist-before-change-function 280,10154
(defun bufhist-make-buttons 292,10570
(defconst bufhist-minor-mode-map310,11009
(define-minor-mode bufhist-mode322,11471
(defun bufhist-toggle-fn 342,12256

lib/holes.el,2447
(defvar holes-doc 38,1073
(defvar holes-default-hole 133,4671
(defvar holes-active-hole 137,4840
(defcustom holes-empty-hole-string 144,5049
(defcustom holes-empty-hole-regexp 147,5160
(defcustom holes-search-limit 154,5451
(defface active-hole-face166,5827
(defface inactive-hole-face178,6275
(defun holes-region-beginning-or-nil 193,6751
(defun holes-region-end-or-nil 198,6849
(defun holes-copy-active-region 203,6935
(defun holes-is-hole-p 210,7122
(defun holes-hole-start-position 216,7229
(defun holes-hole-end-position 223,7418
(defun holes-hole-buffer 230,7602
(defun holes-hole-at 237,7777
(defun holes-active-hole-exist-p 244,7952
(defun holes-active-hole-start-position 254,8210
(defun holes-active-hole-end-position 264,8582
(defun holes-active-hole-buffer 275,8951
(defun holes-goto-active-hole 286,9257
(defun holes-highlight-hole-as-active 298,9525
(defun holes-highlight-hole 308,9837
(defun holes-disable-active-hole 319,10129
(defun holes-set-active-hole 337,10672
(defun holes-is-in-hole-p 350,11018
(defun holes-make-hole 357,11161
(defun holes-make-hole-at 383,11907
(defun holes-clear-hole 403,12383
(defun holes-clear-hole-at 415,12672
(defun holes-map-holes 424,12931
(defun holes-mapcar-holes 432,13114
(defun holes-clear-all-buffer-holes 438,13286
(defun holes-next 449,13586
(defun holes-next-after-active-hole 456,13837
(defun holes-set-active-hole-next 464,14056
(defun holes-replace-segment 486,14609
(defun holes-replace 496,14963
(defun holes-replace-active-hole 527,16158
(defun holes-replace-update-active-hole 536,16454
(defun holes-delete-update-active-hole 557,17127
(defun holes-set-make-active-hole 566,17357
(defun holes-mouse-replace-active-hole 613,19082
(defun holes-destroy-hole 633,19592
(defun holes-hole-at-event 650,20003
(defun holes-mouse-destroy-hole 655,20116
(defun holes-mouse-forget-hole 665,20356
(defun holes-mouse-set-make-active-hole 681,20666
(defun holes-mouse-set-active-hole 703,21203
(defun holes-set-point-next-hole-destroy 715,21467
(defvar hole-map731,21917
(defvar holes-mode-map741,22300
(defun holes-replace-string-by-holes-backward 778,23775
(defun holes-skeleton-end-hook 796,24476
(defconst holes-jump-doc 805,24914
(defun holes-replace-string-by-holes-backward-jump 812,25121
(defun holes-abbrev-complete 830,25767
(defun holes-insert-and-expand 839,26088
(defvar holes-mode 850,26520
(defun holes-mode 856,26716

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,831
(defun local-vars-list-insert-empty-zone 44,1394
(defun local-vars-list-find 82,2102
(defun local-vars-list-goto-var 101,2877
(defun local-vars-list-get-current 127,3927
(defun local-vars-list-set-current 148,4777
(defun local-vars-list-get 171,5494
(defun local-vars-list-get-safe 188,6026
(defun local-vars-list-set 193,6220

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 53,2240
(defvar maths-menu-tokenise-insert 56,2349
(defun maths-menu-build-menu 59,2488
(defvar maths-menu-menu76,3098
(defvar maths-menu-mode-map336,12656
(define-minor-mode maths-menu-mode344,12875

lib/pg-dev.el,75
(defconst pg-dev-lisp-font-lock-keywords36,1106
(defun unload-pg 70,2043

lib/pg-fontsets.el,176
(defcustom pg-fontsets-default-fontset 28,785
(defun pg-fontsets-make-fontsetsizes 33,931
(defconst pg-fontsets-base-fonts 52,1715
(defun pg-fontsets-make-fontsets 57,1820

lib/proof-compat.el,445
(defvar proof-running-on-win32 31,981
(defun pg-custom-undeclare-variable 51,1759
(defmacro save-selected-frame 97,2925
(defun proof-buffer-syntactic-context-emulate 123,3886
(defvar read-shell-command-map151,5096
(defun read-shell-command 169,5784
(defun frames-of-buffer 179,6212
(defmacro with-selected-window 223,7625
(defun process-live-p 255,8644
(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
266,8916

lib/span.el,1353
(defalias 'span-start span-start
22,615
(defalias 'span-end span-end
23,653
(defalias 'span-set-property span-set-property
24,687
(defalias 'span-property span-property
25,730
(defalias 'span-make span-make
26,769
(defalias 'span-detach span-detach
27,805
(defalias 'span-set-endpoints span-set-endpoints
28,845
(defalias 'span-buffer span-buffer
29,890
(defun span-read-only-hook 31,931
(defun span-read-only 36,1121
(defun span-read-write 43,1428
(defun span-give-warning 48,1595
(defun span-write-warning 53,1738
(defun span-lt 65,2322
(defun spans-at-point-prop 70,2463
(defun spans-at-region-prop 76,2628
(defun span-at 85,2940
(defsubst span-delete 91,3156
(defsubst span-mapcar-spans 98,3378
(defun span-at-before 103,3637
(defun prev-span 120,4363
(defun next-span 126,4514
(defsubst span-live-p 133,4726
(defun span-raise 139,4892
(defalias 'span-object span-object
143,5022
(defun span-string 145,5063
(defun set-span-properties 150,5201
(defun span-find-span 160,5448
(defsubst span-at-event 167,5754
(defun make-detached-span 171,5875
(defun fold-spans 176,5971
(defsubst span-detached-p 190,6504
(defsubst set-span-face 194,6620
(defun set-span-keymap 198,6718
(defsubst span-delete-spans 207,6921
(defsubst span-property-safe 211,7085
(defsubst span-set-start 215,7224
(defsubst span-set-end 219,7356

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3034
(defun texi-docstring-magic-splice-sep 93,3199
(defconst texi-docstring-magic-munge-table103,3504
(defun texi-docstring-magic-untabify 193,7271
(defun texi-docstring-magic-munge-docstring 203,7586
(defun texi-docstring-magic-texi 242,8873
(defun texi-docstring-magic-format-default 255,9313
(defun texi-docstring-magic-texi-for 271,9948
(defconst texi-docstring-magic-comment329,11908
(defun texi-docstring-magic 335,12062
(defun texi-docstring-magic-face-at-point 369,13142
(defun texi-docstring-magic-insert-magic 384,13665

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,348
(defun unicode-chars-list-chars 5050,245960

lib/unicode-tokens.el,3137
(defvar unicode-tokens-token-symbol-map 46,1575
(defvar unicode-tokens-token-format 59,2004
(defvar unicode-tokens-token-variant-format-regexp 65,2253
(defvar unicode-tokens-fontsymb-properties 78,2730
(defvar unicode-tokens-shortcut-alist 83,2964
(defvar unicode-tokens-control-region-format-regexp 94,3230
(defvar unicode-tokens-control-char-format-regexp 95,3287
(defvar unicode-tokens-control-regions 96,3342
(defvar unicode-tokens-control-characters 97,3386
(defvar unicode-tokens-control-region-format-beg 99,3434
(defvar unicode-tokens-control-region-format-end 100,3488
(defvar unicode-tokens-control-char-format 101,3542
(defconst unicode-tokens-configuration-variables107,3631
(defvar unicode-tokens-token-list 125,4024
(defvar unicode-tokens-hash-table 128,4144
(defvar unicode-tokens-token-match-regexp 131,4260
(defvar unicode-tokens-uchar-hash-table 134,4366
(defvar unicode-tokens-uchar-regexp 138,4553
(defgroup unicode-tokens-faces 148,4744
(defface unicode-tokens-script-font-face152,4840
(defface unicode-tokens-fraktur-font-face163,5138
(defface unicode-tokens-serif-font-face174,5463
(defconst unicode-tokens-font-lock-extra-managed-props 185,5756
(defun unicode-tokens-font-lock-keywords 193,5928
(defun unicode-tokens-usable-composition 233,7583
(defun unicode-tokens-help-echo 244,7859
(defvar unicode-tokens-show-symbols 248,8022
(defun unicode-tokens-font-lock-compose-symbol 251,8136
(defun unicode-tokens-show-symbols 268,8852
(defun unicode-tokens-symbs-to-props 276,9153
(defvar unicode-tokens-show-controls 294,9674
(defun unicode-tokens-show-controls 297,9765
(defun unicode-tokens-control-char 308,10250
(defun unicode-tokens-control-region 313,10492
(defun unicode-tokens-control-font-lock-keywords 319,10821
(defvar unicode-tokens-use-shortcuts 330,11151
(defun unicode-tokens-use-shortcuts 333,11254
(defun unicode-tokens-map-ordering 351,11851
(defun unicode-tokens-quail-define-rules 355,12001
(defun unicode-tokens-insert-token 378,12680
(defun unicode-tokens-annotate-region 388,12979
(defun unicode-tokens-insert-control 411,13747
(defun unicode-tokens-insert-uchar-as-token 417,13971
(defun unicode-tokens-delete-token-at-point 424,14201
(defvar unicode-tokens-rotate-token-last-token 429,14374
(defun unicode-tokens-prev-token 431,14427
(defun unicode-tokens-rotate-token-forward 439,14697
(defun unicode-tokens-rotate-token-backward 464,15622
(defun unicode-tokens-copy-token 469,15824
(define-button-type 'unicode-tokens-listunicode-tokens-list
475,15999
(defun unicode-tokens-list-tokens 482,16245
(defun unicode-tokens-copy 503,16862
(defun unicode-tokens-paste 530,18013
(defun unicode-tokens-initialise 550,18517
(defvar unicode-tokens-mode-map 557,18734
(define-minor-mode unicode-tokens-mode561,18846
(define-key unicode-tokens-mode-map 617,20799
(define-key unicode-tokens-mode-map 619,20891
(define-key unicode-tokens-mode-map 621,20982
(define-key unicode-tokens-mode-map 623,21089
(define-key unicode-tokens-mode-map 625,21199
(define-key unicode-tokens-mode-map 627,21308
(define-key unicode-tokens-mode-map 629,21415

mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2675
(defun mmm-autoload-class 89,3438
(defvar mmm-changed-buffers-list 129,5005
(defun mmm-major-mode-change 132,5112
(defun mmm-check-changed-buffers 145,5633
(defun mmm-mode-on-maybe 155,6006
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6424
(defun mmm-add-find-file-hook 168,6484

mmm/mmm-class.el,416
(defun mmm-get-class-spec 42,1295
(defun mmm-get-class-parameter 59,2008
(defun mmm-set-class-parameter 63,2174
(defun* mmm-apply-class75,2538
(defun* mmm-apply-classes90,3176
(defun* mmm-apply-all 110,3942
(defun* mmm-ify124,4389
(defun* mmm-match-region206,7472
(defun mmm-match->point 267,10161
(defun mmm-match-and-verify 281,10683
(defun mmm-get-form 307,11741
(defun mmm-default-get-form 318,12237

mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1209
(defun mmm-ify-region 63,1933
(defun mmm-ify-by-regexp75,2361
(defun mmm-parse-buffer 97,3037
(defun mmm-parse-region 106,3373
(defun mmm-parse-block 115,3752
(defun mmm-get-block 132,4503
(defun mmm-reparse-current-region 146,4834
(defun mmm-clear-current-region 167,5508
(defun mmm-clear-regions 172,5672
(defun mmm-clear-all-regions 177,5818
(defun* mmm-end-current-region 185,5978
(defun mmm-narrow-to-submode-region 220,7401
(defun mmm-insert-region 239,8015
(defun mmm-insert-by-key 258,8877
(defun mmm-get-insertion-spec 342,12437
(defun mmm-insertion-help 369,13516
(defun mmm-display-insertion-key 379,13886
(defun mmm-get-all-insertion-keys 401,14708

mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1312
(defvar mmm-keywords-used49,1615
(defmacro mmm-regexp-opt 91,2661
(defvar mmm-evaporate-property110,3310
(defmacro mmm-set-keymap-default 128,4076
(defmacro mmm-event-key 137,4518
(defvar skeleton-positions 146,4737
(defun mmm-fixup-skeleton 147,4768
(defmacro mmm-make-temp-buffer 159,5205
(defvar mmm-font-lock-available-p 172,5601
(defmacro mmm-set-font-lock-defaults 179,5815

mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1116
(defvar mmm-cweb-section-regexp41,1163
(defvar mmm-cweb-c-part-tags44,1253
(defvar mmm-cweb-c-part-regexp47,1312
(defun mmm-cweb-in-limbo 50,1396
(defun mmm-cweb-verify-brief-c 57,1621

mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1235
(defvar mmm-mason-pseudo-perl-tags45,1376
(defvar mmm-mason-non-perl-tags48,1452
(defvar mmm-mason-perl-tags-regexp51,1553
(defvar mmm-mason-pseudo-perl-tags-regexp56,1748
(defvar mmm-mason-tag-names-regexp61,1965
(defun mmm-mason-verify-inline 66,2185
(defun mmm-mason-start-line 156,5089
(defun mmm-mason-end-line 161,5154
(defun mmm-mason-set-mode-line 168,5248

mmm/mmm-mode.el,1024
(defun mmm-mode 101,3866
(defun mmm-mode-on 140,5371
(defun mmm-mode-off 181,7131
(defvar mmm-mode-map 206,7864
(defvar mmm-mode-prefix-map 209,7939
(defvar mmm-mode-menu-map 212,8049
(defun mmm-define-key 215,8140
(define-key mmm-mode-prefix-map 239,8895
(define-key mmm-mode-prefix-map 246,9153
(define-key mmm-mode-map 249,9264
(define-key mmm-mode-menu-map 252,9366
(define-key mmm-mode-menu-map 254,9438
(define-key mmm-mode-menu-map 256,9497
(define-key mmm-mode-menu-map 258,9578
(define-key mmm-mode-menu-map 260,9659
(define-key mmm-mode-menu-map 262,9746
(define-key mmm-mode-menu-map 265,9840
(define-key mmm-mode-menu-map 267,9900
(define-key mmm-mode-menu-map 270,9991
(define-key mmm-mode-menu-map 272,10051
(define-key mmm-mode-menu-map 274,10158
(define-key mmm-mode-menu-map 276,10243
(define-key mmm-mode-menu-map 279,10329
(define-key mmm-mode-menu-map 281,10389
(define-key mmm-mode-menu-map 283,10502
(define-key mmm-mode-menu-map 285,10587
(define-key mmm-mode-map 288,10670

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,1748
(defun mmm-overlays-at 59,1933
(defun mmm-included-p 72,2386
(defun mmm-overlays-containing 112,3875
(defun mmm-overlays-contained-in 125,4313
(defun mmm-overlays-overlapping 138,4753
(defun mmm-sort-overlays 149,5116
(defvar mmm-current-overlay 158,5386
(defvar mmm-previous-overlay 163,5601
(defvar mmm-current-submode 168,5789
(defvar mmm-previous-submode 173,5989
(defun mmm-update-current-submode 178,6162
(defun mmm-set-current-submode 199,6978
(defun mmm-submode-at 210,7470
(defun mmm-match-front 219,7745
(defun mmm-match-back 238,8506
(defun mmm-front-start 257,9251
(defun mmm-back-end 265,9555
(defun mmm-valid-submode-region 278,9902
(defun* mmm-make-region305,11058
(defun mmm-make-overlay 431,16429
(defun mmm-get-face 459,17562
(defun mmm-clear-overlays 470,17854
(defun mmm-update-mode-info 486,18321
(defun mmm-update-submode-region 571,22606
(defun mmm-add-hooks 588,23364
(defun mmm-remove-hooks 592,23499
(defun mmm-get-local-variables-list 598,23626
(defun mmm-get-locals 618,24546
(defun mmm-get-saved-local 631,25127
(defun mmm-set-local-variables 635,25292
(defun mmm-get-saved-local-variables 646,25733
(defun mmm-save-changed-local-variables 654,26050
(defun mmm-clear-local-variables 673,26908
(defun mmm-enable-font-lock 684,27187
(defun mmm-update-font-lock-buffer 692,27447
(defun mmm-refontify-maybe 705,27879
(defun mmm-submode-changes-in 720,28401
(defun mmm-regions-in 731,28849
(defun mmm-regions-alist 745,29419
(defun mmm-fontify-region 762,30065
(defun mmm-fontify-region-list 782,31096
(defun mmm-beginning-of-syntax 804,32012

mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1617
(defvar mmm-rpm-sh-end-tags53,1841
(defvar mmm-rpm-sh-start-regexp57,2015
(defvar mmm-rpm-sh-end-regexp61,2193

mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2614
(defun mmm-here-doc-get-mode 93,3099
(defun mmm-file-variables-verify 208,6817
(defun mmm-file-variables-find-back 232,7853

mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 41,1309
(defmacro mmm-save-all 60,1953
(defun mmm-format-string 73,2242
(defun mmm-format-matches 84,2694
(defmacro mmm-save-keyword 107,3487
(defmacro mmm-save-keywords 115,3814
(defun mmm-looking-back-at 128,4347
(defun mmm-make-marker 145,4915

mmm/mmm-vars.el,2667
(defgroup mmm 99,3072
(defvar mmm-c-derived-modes106,3182
(defvar mmm-save-local-variables 110,3301
(defvar mmm-buffer-saved-locals 336,10161
(defvar mmm-region-saved-locals-defaults 341,10361
(defvar mmm-region-saved-locals-for-dominant 347,10621
(defgroup mmm-faces 357,10998
(defcustom mmm-submode-decoration-level 363,11169
(defface mmm-init-submode-face 381,12041
(defface mmm-cleanup-submode-face 385,12181
(defface mmm-declaration-submode-face 389,12318
(defface mmm-comment-submode-face 393,12464
(defface mmm-output-submode-face 397,12617
(defface mmm-special-submode-face 401,12766
(defface mmm-code-submode-face 405,12930
(defface mmm-default-submode-face 409,13069
(defface mmm-delimiter-face 414,13277
(defcustom mmm-mode-string 421,13403
(defcustom mmm-submode-mode-line-format 426,13534
(defvar mmm-primary-mode-display-name 443,14189
(defvar mmm-buffer-mode-display-name 448,14403
(defun mmm-set-mode-line 454,14702
(defvar mmm-classes 478,15510
(defvar mmm-global-classes 484,15755
(defcustom mmm-mode-ext-classes-alist 491,15937
(defun mmm-add-mode-ext-class 510,16755
(defcustom mmm-major-mode-preferences519,17080
(defun mmm-add-to-major-mode-preferences 537,17878
(defun mmm-ensure-modename 553,18664
(defun mmm-modename->function 562,18974
(defcustom mmm-delimiter-mode 576,19437
(defcustom mmm-mode-prefix-key 586,19706
(defcustom mmm-command-modifiers 591,19833
(defcustom mmm-insert-modifiers 605,20466
(defcustom mmm-use-old-command-keys 620,21144
(defun mmm-use-old-command-keys 630,21608
(defcustom mmm-mode-hook 638,21807
(defun mmm-run-constructed-hook 658,22614
(defun mmm-run-major-hook 666,23000
(defun mmm-run-submode-hook 669,23077
(defvar mmm-class-hooks-run 672,23164
(defun mmm-run-class-hook 677,23336
(defvar mmm-primary-mode-entry-hook 682,23508
(defcustom mmm-major-mode-hook 697,24155
(defun mmm-run-major-mode-hook 711,24786
(defcustom mmm-global-mode 724,25327
(defcustom mmm-never-modes740,26022
(defvar mmm-set-file-name-for-modes 758,26322
(defvar mmm-mode 769,26681
(defvar mmm-primary-mode 777,26889
(defvar mmm-classes-alist 788,27255
(defun mmm-add-classes 943,35462
(defun mmm-add-group 948,35627
(defun mmm-add-to-group 958,36077
(defconst mmm-version 972,36574
(defun mmm-version 975,36639
(defvar mmm-temp-buffer-name 982,36782
(defvar mmm-interactive-history 988,36912
(defun mmm-add-to-history 994,37181
(defun mmm-clear-history 997,37264
(defvar mmm-mode-ext-classes 1005,37449
(defun mmm-get-mode-ext-classes 1010,37660
(defun mmm-clear-mode-ext-classes 1019,38036
(defun mmm-mode-ext-applies 1023,38161
(defun mmm-get-all-classes 1037,38645

doc/ProofGeneral.texi,5548
@node Top166,5060
@node Preface203,6165
@node Latest news for version 3.7.1Latest news for version 3.7.1
226,6763
@node Future269,8708
@node Credits300,10007
@node Introducing Proof GeneralIntroducing Proof General
406,13776
@node Installing Proof GeneralInstalling Proof General
462,15818
@node Quick start guideQuick start guide
476,16267
@node Features of Proof GeneralFeatures of Proof General
520,18388
@node Supported proof assistantsSupported proof assistants
609,22325
@node Prerequisites for this manualPrerequisites for this manual
658,24245
@node Organization of this manualOrganization of this manual
702,25871
@node Basic Script ManagementBasic Script Management
728,26699
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
747,27299
@node Proof scriptsProof scripts
998,36952
@node Script buffersScript buffers
1041,39072
@node Locked queue and editing regionsLocked queue and editing regions
1063,39649
@node Goal-save sequencesGoal-save sequences
1119,41796
@node Active scripting bufferActive scripting buffer
1156,43282
@node Summary of Proof General buffersSummary of Proof General buffers
1225,46702
@node Script editing commandsScript editing commands
1287,49376
@node Script processing commandsScript processing commands
1365,52235
@node Proof assistant commandsProof assistant commands
1493,57536
@node Toolbar commandsToolbar commands
1659,63315
@node Interrupting during trace outputInterrupting during trace output
1683,64244
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1722,66168
@node Goals buffer commandsGoals buffer commands
1736,66668
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1825,70232
@node Visibility of completed proofsVisibility of completed proofs
1857,71444
@node Switching between proof scriptsSwitching between proof scripts
1912,73367
@node View of processed files View of processed files 
1949,75339
@node Retracting across filesRetracting across files
2009,78390
@node Asserting across filesAsserting across files
2022,79021
@node Automatic multiple file handlingAutomatic multiple file handling
2035,79587
@node Escaping script managementEscaping script management
2060,80621
@node Editing featuresEditing features
2118,82824
@node Experimental featuresExperimental features
2182,85496
@node Support for other PackagesSupport for other Packages
2216,86760
@node Syntax highlightingSyntax highlighting
2248,87634
@node Unicode supportUnicode support
2277,88638
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2363,91749
@node Support for outline modeSupport for outline mode
2422,93879
@node Support for completionSupport for completion
2448,95009
@node Support for tagsSupport for tags
2506,97185
@node Customizing Proof GeneralCustomizing Proof General
2558,99514
@node Basic optionsBasic options
2598,101184
@node How to customizeHow to customize
2622,101942
@node Display customizationDisplay customization
2673,104044
@node User optionsUser options
2798,109282
@node Changing facesChanging faces
3040,117873
@node Tweaking configuration settingsTweaking configuration settings
3115,120542
@node Hints and TipsHints and Tips
3172,123068
@node Adding your own keybindingsAdding your own keybindings
3191,123669
@node Using file variablesUsing file variables
3248,126268
@node Using abbreviationsUsing abbreviations
3307,128454
@node LEGO Proof GeneralLEGO Proof General
3346,129870
@node LEGO specific commandsLEGO specific commands
3387,131239
@node LEGO tagsLEGO tags
3407,131694
@node LEGO customizationsLEGO customizations
3417,131941
@node Coq Proof GeneralCoq Proof General
3449,132860
@node Coq-specific commandsCoq-specific commands
3465,133269
@node Coq-specific variablesCoq-specific variables
3487,133776
@node Editing multiple proofsEditing multiple proofs
3509,134434
@node User-loaded tacticsUser-loaded tactics
3533,135542
@node Holes featureHoles feature
3597,138016
@node Isabelle Proof GeneralIsabelle Proof General
3624,139303
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3655,140472
@node Isabelle commandsIsabelle commands
3730,143521
@node Isabelle settingsIsabelle settings
3873,147674
@node Isabelle customizationsIsabelle customizations
3887,148256
@node HOL Proof GeneralHOL Proof General
3910,148743
@node Shell Proof GeneralShell Proof General
3952,150565
@node Obtaining and InstallingObtaining and Installing
3988,152024
@node Obtaining Proof GeneralObtaining Proof General
4004,152437
@node Installing Proof General from tarballInstalling Proof General from tarball
4035,153676
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4060,154508
@node Setting the names of binariesSetting the names of binaries
4075,154916
@node Notes for syssiesNotes for syssies
4103,155856
@node Bugs and EnhancementsBugs and Enhancements
4178,158892
@node References4199,159707
@node History of Proof GeneralHistory of Proof General
4239,160730
@node Old News for 3.0Old News for 3.0
4330,164832
@node Old News for 3.1Old News for 3.1
4400,168526
@node Old News for 3.2Old News for 3.2
4426,169698
@node Old News for 3.3Old News for 3.3
4487,172701
@node Old News for 3.4Old News for 3.4
4506,173598
@node Function IndexFunction Index
4529,174654
@node Variable IndexVariable Index
4533,174730
@node Keystroke IndexKeystroke Index
4537,174810
@node Concept IndexConcept Index
4541,174876

doc/PG-adapting.texi,3772
@node Top156,4734
@node Introduction194,5877
@node Future235,7530
@node Credits271,9126
@node Beginning with a New ProverBeginning with a New Prover
281,9418
@node Overview of adding a new proverOverview of adding a new prover
322,11367
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
400,14675
@node Major modes used by Proof GeneralMajor modes used by Proof General
469,18066
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
502,19417
@node Settings for generic user-level commandsSettings for generic user-level commands
517,19963
@node Menu configurationMenu configuration
562,21697
@node Toolbar configurationToolbar configuration
586,22614
@node Proof Script SettingsProof Script Settings
644,24863
@node Recognizing commands and commentsRecognizing commands and comments
666,25443
@node Recognizing proofsRecognizing proofs
787,30964
@node Recognizing other elementsRecognizing other elements
896,35645
@node Configuring undo behaviourConfiguring undo behaviour
1022,41184
@node Nested proofsNested proofs
1159,46592
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1199,48218
@node Activate scripting hookActivate scripting hook
1222,49171
@node Automatic multiple filesAutomatic multiple files
1246,50041
@node Completions1268,50888
@node Proof Shell SettingsProof Shell Settings
1309,52377
@node Proof shell commandsProof shell commands
1340,53659
@node Script input to the shellScript input to the shell
1504,60703
@node Settings for matching various output from proof processSettings for matching various output from proof process
1569,63661
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1700,69445
@node Hooks and other settingsHooks and other settings
1915,79322
@node Goals Buffer SettingsGoals Buffer Settings
1996,82704
@node Splash Screen SettingsSplash Screen Settings
2073,85811
@node Global ConstantsGlobal Constants
2099,86569
@node Handling Multiple FilesHandling Multiple Files
2125,87410
@node Configuring Editing SyntaxConfiguring Editing Syntax
2277,95193
@node Configuring Font LockConfiguring Font Lock
2336,97314
@node Configuring TokensConfiguring Tokens
2408,100669
@node Writing More Lisp CodeWriting More Lisp Code
2450,102342
@node Default values for generic settingsDefault values for generic settings
2467,102987
@node Adding prover-specific configurationsAdding prover-specific configurations
2497,104070
@node Useful variablesUseful variables
2540,105352
@node Useful functions and macrosUseful functions and macros
2555,105851
@node Internals of Proof GeneralInternals of Proof General
2658,109806
@node Spans2686,110714
@node Proof General site configurationProof General site configuration
2699,111088
@node Configuration variable mechanismsConfiguration variable mechanisms
2779,114134
@node Global variablesGlobal variables
2900,119578
@node Proof script modeProof script mode
2970,122126
@node Proof shell modeProof shell mode
3229,133781
@node Debugging3636,149863
@node Plans and IdeasPlans and Ideas
3679,150739
@node Proof by pointing and similar featuresProof by pointing and similar features
3700,151461
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3738,153119
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3783,155344
@node Demonstration InstantiationsDemonstration Instantiations
3813,156375
@node demoisa-easy.el3829,156806
@node demoisa.el3892,159048
@node Function IndexFunction Index
4047,164036
@node Variable IndexVariable Index
4051,164112
@node Concept IndexConcept Index
4060,164291

generic/proof.el,0

pgshell/pgshell.el,0

isar/isar-autotest.el,0

isar/interface-setup.el,0

hol98/hol98.el,0

demoisa/demoisa-easy.el,0

coq/coq-mmm.el,0

coq/coq-autotest.el,0

ccc/ccc.el,0

acl2/acl2.el,0