path: root/TAGS


coq/coq-abbrev.el,495
(defun holes-show-doc 10,310
(defun coq-local-vars-list-show-doc 14,386
(defconst coq-tactics-menu19,486
(defconst coq-tactics-abbrev-table24,663
(defconst coq-tacticals-menu27,780
(defconst coq-tacticals-abbrev-table31,889
(defconst coq-commands-menu34,980
(defconst coq-commands-abbrev-table41,1203
(defconst coq-terms-menu44,1292
(defconst coq-terms-abbrev-table49,1430
(defun coq-install-abbrevs 56,1624
(defpgdefault menu-entries76,2361
(defpgdefault help-menu-entries169,5947

coq/coq-db.el,559
(defconst coq-syntax-db 22,534
(defvar coq-user-tactics-db58,1907
(defun coq-insert-from-db 68,2256
(defun coq-build-regexp-list-from-db 86,3037
(defun max-length-db 108,4090
(defun coq-build-menu-from-db-internal 120,4365
(defun coq-build-title-menu 155,5988
(defun coq-sort-menu-entries 164,6356
(defun coq-build-menu-from-db 170,6486
(defun coq-build-abbrev-table-from-db 192,7323
(defun filter-state-preserving 209,7881
(defun filter-state-changing 214,8035
(defface coq-solve-tactics-face 221,8256
(defconst coq-solve-tactics-face 229,8513

coq/coq.el,6514
(defcustom coq-translate-to-v8 45,1301
(defun coq-build-prog-args 51,1481
(defcustom coq-compile-file-command 64,1861
(defcustom coq-use-makefile 72,2180
(defcustom coq-default-undo-limit 80,2403
(defconst coq-shell-init-cmd 85,2531
(defcustom coq-prog-env 97,2809
(defconst coq-shell-restart-cmd 105,3061
(defvar coq-shell-prompt-pattern 112,3321
(defvar coq-shell-cd 122,3714
(defvar coq-shell-abort-goal-regexp 126,3874
(defvar coq-shell-proof-completed-regexp 129,4000
(defvar coq-goal-regexp132,4152
(defun coq-library-directory 139,4266
(defcustom coq-tags 146,4446
(defconst coq-interrupt-regexp 151,4596
(defcustom coq-www-home-page 156,4717
(defvar coq-outline-regexp166,4888
(defvar coq-outline-heading-end-regexp 173,5102
(defvar coq-shell-outline-regexp 175,5156
(defvar coq-shell-outline-heading-end-regexp 176,5206
(defconst coq-kill-goal-command 181,5316
(defconst coq-forget-id-command 182,5359
(defconst coq-back-n-command 183,5406
(defconst coq-state-preserving-tactics-regexp 187,5550
(defconst coq-state-changing-commands-regexp189,5651
(defconst coq-state-preserving-commands-regexp 191,5758
(defconst coq-commands-regexp 193,5870
(defvar coq-retractable-instruct-regexp 195,5948
(defvar coq-non-retractable-instruct-regexp 197,6039
(defvar coq-keywords-section201,6179
(defvar coq-section-regexp 204,6273
(defun coq-set-undo-limit 241,7419
(defconst coq-keywords-decl-defn-regexp252,7858
(defun coq-proof-mode-p 256,8008
(defun coq-is-comment-or-proverprocp 267,8416
(defun coq-is-goalsave-p 269,8520
(defun coq-is-module-equal-p 270,8595
(defun coq-is-def-p 273,8791
(defun coq-is-decl-defn-p 275,8899
(defun coq-state-preserving-command-p 280,9066
(defun coq-command-p 283,9200
(defun coq-state-preserving-tactic-p 286,9300
(defun coq-state-changing-tactic-p 291,9448
(defun coq-state-changing-command-p 298,9682
(defun coq-section-or-module-start-p 305,10028
(defun build-list-id-from-string 314,10269
(defun coq-last-prompt-info 327,10799
(defun coq-last-prompt-info-safe 339,11340
(defvar coq-last-but-one-statenum 345,11597
(defvar coq-last-but-one-proofnum 351,11895
(defvar coq-last-but-one-proofstack 354,11993
(defun coq-get-span-statenum 357,12103
(defun coq-get-span-proofnum 362,12218
(defun coq-get-span-proofstack 367,12333
(defun coq-set-span-statenum 372,12477
(defun coq-get-span-goalcmd 377,12608
(defun coq-set-span-goalcmd 382,12722
(defun coq-set-span-proofnum 387,12852
(defun coq-set-span-proofstack 392,12983
(defun proof-last-locked-span 397,13143
(defun coq-set-state-infos 412,13747
(defun count-not-intersection 452,15826
(defun  coq-find-and-forget-v81 483,17080
(defun coq-find-and-forget-v80 511,18212
(defun coq-find-and-forget 606,22911
(defvar coq-current-goal 619,23451
(defun coq-goal-hyp 622,23516
(defun coq-state-preserving-p 635,23949
(defconst notation-print-kinds-table 649,24454
(defun coq-PrintScope 653,24622
(defun coq-guess-or-ask-for-string 681,25392
(defun coq-ask-do 695,25935
(defun coq-SearchIsos 704,26323
(defun coq-SearchConstant 710,26556
(defun coq-SearchRewrite 714,26649
(defun coq-SearchAbout 718,26747
(defun coq-Print 722,26839
(defun coq-About 726,26961
(defun coq-LocateConstant 730,27078
(defun coq-LocateLibrary 736,27213
(defun coq-addquotes 742,27363
(defun coq-LocateNotation 744,27411
(defun coq-Pwd 751,27610
(defun coq-Inspect 757,27742
(defun coq-PrintSection(761,27842
(defun coq-Print-implicit 765,27935
(defun coq-Check 770,28086
(defun coq-Show 775,28194
(defun coq-Compile 789,28637
(defun coq-guess-command-line 803,28957
(defun coq-mode-config 841,30673
(defvar coq-last-hybrid-pre-string 949,34627
(defun coq-hybrid-ouput-goals-response-p 952,34806
(defun coq-hybrid-ouput-goals-response 958,35064
(defun coq-shell-mode-config 979,36024
(defun coq-goals-mode-config 1024,38139
(defun coq-response-config 1031,38383
(defpacustom print-fully-explicit 1056,39208
(defpacustom print-implicit 1061,39357
(defpacustom print-coercions 1066,39524
(defpacustom print-match-wildcards 1071,39669
(defpacustom print-elim-types 1076,39850
(defpacustom printing-depth 1081,40017
(defpacustom undo-depth 1086,40179
(defpacustom time-commands 1091,40327
(defpacustom undo-limit 1095,40438
(defpacustom auto-compile-vos 1100,40541
(defun coq-maybe-compile-buffer 1129,41657
(defun coq-ancestors-of 1166,43191
(defun coq-all-ancestors-of 1189,44158
(defconst coq-require-command-regexp 1201,44551
(defun coq-process-require-command 1206,44760
(defun coq-included-children 1211,44887
(defun coq-process-file 1232,45726
(defun coq-preprocessing 1247,46265
(defun coq-fake-constant-markup 1262,46684
(defun coq-create-span-menu 1283,47490
(defconst module-kinds-table 1300,47989
(defconst modtype-kinds-table1304,48139
(defun coq-insert-section-or-module 1308,48268
(defconst reqkinds-kinds-table1331,49128
(defun coq-insert-requires 1336,49273
(defun coq-end-Section 1352,49779
(defun coq-insert-intros 1370,50363
(defun coq-insert-infoH-hook 1383,50888
(defun coq-insert-as 1387,50966
(defun coq-insert-match 1408,51715
(defun coq-insert-tactic 1440,52893
(defun coq-insert-tactical 1446,53132
(defun coq-insert-command 1452,53381
(defun coq-insert-term 1458,53625
(define-key coq-keymap 1464,53822
(define-key coq-keymap 1465,53880
(define-key coq-keymap 1466,53937
(define-key coq-keymap 1467,54006
(define-key coq-keymap 1468,54062
(define-key coq-keymap 1469,54111
(define-key coq-keymap 1470,54169
(define-key coq-keymap 1472,54230
(define-key coq-keymap 1473,54289
(define-key coq-keymap 1475,54353
(define-key coq-keymap 1476,54413
(define-key coq-keymap 1478,54469
(define-key coq-keymap 1479,54519
(define-key coq-keymap 1480,54569
(define-key coq-keymap 1481,54619
(define-key coq-keymap 1482,54673
(define-key coq-keymap 1483,54732
(defvar last-coq-error-location 1491,54863
(defun coq-get-last-error-location 1500,55262
(defun coq-highlight-error 1547,57647
(defvar coq-allow-highlight-error 1583,58950
(defun coq-decide-highlight-error 1589,59216
(defun coq-highlight-error-hook 1593,59338
(defun first-word-of-buffer 1604,59731
(defun coq-show-first-goal 1612,59934
(defvar coq-modeline-string2 1629,60629
(defvar coq-modeline-string1 1630,60673
(defvar coq-modeline-string0 1631,60716
(defun coq-build-subgoals-string 1632,60761
(defun coq-update-minor-mode-alist 1637,60929
(defun is-not-split-vertic 1663,61997
(defun optim-resp-windows 1672,62436

coq/coq-indent.el,2222
(defconst coq-any-command-regexp17,315
(defconst coq-indent-inner-regexp20,406
(defconst coq-comment-start-regexp 31,794
(defconst coq-comment-end-regexp 32,837
(defconst coq-comment-start-or-end-regexp33,878
(defconst coq-indent-open-regexp35,986
(defconst coq-indent-close-regexp40,1160
(defconst coq-indent-closepar-regexp 45,1341
(defconst coq-indent-closematch-regexp 46,1386
(defconst coq-indent-openpar-regexp 47,1457
(defconst coq-indent-openmatch-regexp 48,1501
(defconst coq-indent-any-regexp49,1581
(defconst coq-indent-kw54,1859
(defconst coq-indent-pattern-regexp 64,2313
(defun coq-indent-goal-command-p 68,2416
(defconst coq-end-command-regexp90,3471
(defun coq-search-comment-delimiter-forward 95,3623
(defun coq-search-comment-delimiter-backward 104,3953
(defun coq-skip-until-one-comment-backward 111,4227
(defun coq-skip-until-one-comment-forward 126,4934
(defun coq-looking-at-comment 137,5452
(defun coq-find-comment-start 141,5593
(defun coq-find-comment-end 152,6026
(defun coq-looking-at-syntactic-context 164,6519
(defconst coq-end-command-or-comment-regexp170,6741
(defconst coq-end-command-or-comment-start-regexp173,6850
(defun coq-find-not-in-comment-backward 177,6968
(defun coq-find-not-in-comment-forward 197,7869
(defun coq-find-command-end-backward 221,9011
(defun coq-find-command-end-forward 230,9402
(defun coq-find-command-end 239,9779
(defun coq-find-current-start 247,10111
(defun coq-find-real-start 256,10402
(defun coq-command-at-point 263,10621
(defun coq-indent-only-spaces-on-line 270,10898
(defun coq-indent-find-reg 276,11175
(defun coq-find-no-syntactic-on-line 290,11711
(defun coq-back-to-indentation-prevline 303,12184
(defun coq-find-unclosed 347,14098
(defun coq-find-at-same-level-zero 377,15399
(defun coq-find-unopened 405,16564
(defun coq-find-last-unopened 448,18014
(defun coq-end-offset 459,18411
(defun coq-indent-command-offset 484,19202
(defun coq-indent-expr-offset 531,21026
(defun coq-indent-comment-offset 647,25729
(defun coq-indent-offset 679,27187
(defun coq-indent-calculate 697,28050
(defun coq-indent-line 700,28138
(defun coq-indent-line-not-comments 710,28504
(defun coq-indent-region 720,28893

coq/coq-local-vars.el,280
(defconst coq-local-vars-doc 17,305
(defun coq-insert-coq-prog-name 75,2831
(defun coq-read-directory 86,3304
(defun coq-extract-directories-from-args 110,4407
(defun coq-ask-prog-args 125,4959
(defun coq-ask-prog-name 147,6063
(defun coq-ask-insert-coq-prog-name 165,6818

coq/coq-syntax.el,2666
(defcustom coq-prog-name 13,421
(defvar coq-version-is-V8 34,1420
(defvar coq-version-is-V8-0 36,1499
(defvar coq-version-is-V8-1 43,1877
(defun coq-determine-version 52,2310
(defcustom coq-user-tactics-db 98,4216
(defcustom coq-user-commands-db 115,4729
(defcustom coq-user-tacticals-db 131,5248
(defcustom coq-user-solve-tactics-db 147,5769
(defcustom coq-user-reserved-db 165,6290
(defvar coq-tactics-db183,6821
(defvar coq-solve-tactics-db338,14889
(defvar coq-tacticals-db362,15736
(defvar coq-decl-db386,16623
(defvar coq-defn-db408,17841
(defvar coq-goal-starters-db461,21827
(defvar coq-other-commands-db488,23382
(defvar coq-commands-db612,32579
(defvar coq-terms-db619,32805
(defun coq-count-match 683,35457
(defun coq-goal-command-str-v80-p 702,36320
(defun coq-module-opening-p 725,37193
(defun coq-section-command-p 736,37609
(defun coq-goal-command-str-v81-p 740,37706
(defun coq-goal-command-p-v81 755,38375
(defun coq-goal-command-str-p 765,38715
(defun coq-goal-command-p 775,39081
(defvar coq-keywords-save-strict783,39393
(defvar coq-keywords-save792,39506
(defun coq-save-command-p 796,39584
(defvar coq-keywords-kill-goal 805,39878
(defvar coq-keywords-state-changing-misc-commands809,39969
(defvar coq-keywords-goal812,40094
(defvar coq-keywords-decl815,40177
(defvar coq-keywords-defn818,40251
(defvar coq-keywords-state-changing-commands822,40326
(defvar coq-keywords-state-preserving-commands831,40587
(defvar coq-keywords-commands836,40803
(defvar coq-solve-tactics841,40952
(defvar coq-tacticals845,41073
(defvar coq-reserved851,41212
(defvar coq-state-changing-tactics862,41541
(defvar coq-state-preserving-tactics865,41650
(defvar coq-tactics869,41764
(defvar coq-retractable-instruct872,41853
(defvar coq-non-retractable-instruct875,41963
(defvar coq-keywords879,42091
(defvar coq-symbols886,42259
(defvar coq-error-regexp 905,42472
(defvar coq-id 908,42700
(defvar coq-id-shy 909,42725
(defvar coq-ids 911,42779
(defun coq-first-abstr-regexp 913,42820
(defcustom coq-variable-highlight-enable 916,42915
(defvar coq-font-lock-terms922,43042
(defconst coq-save-command-regexp-strict943,44042
(defconst coq-save-command-regexp947,44209
(defconst coq-save-with-hole-regexp951,44362
(defconst coq-goal-command-regexp955,44521
(defconst coq-goal-with-hole-regexp958,44621
(defconst coq-decl-with-hole-regexp962,44754
(defconst coq-defn-with-hole-regexp969,45003
(defconst coq-with-with-hole-regexp979,45292
(defvar coq-font-lock-keywords-1985,45585
(defvar coq-font-lock-keywords 1011,46901
(defun coq-init-syntax-table 1013,46959
(defconst coq-generic-expression1042,47858

coq/coq-unicode-tokens.el,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,1810
(defcustom isabelledemo-web-page59,1932
(defun demoisa-config 70,2162
(defun demoisa-shell-config 91,2954
(define-derived-mode demoisa-mode 117,3931
(define-derived-mode demoisa-shell-mode 122,4054
(define-derived-mode demoisa-response-mode 127,4197
(define-derived-mode demoisa-goals-mode 131,4324

isar/isabelle-system.el,1347
(defgroup isabelle 26,776
(defcustom isabelle-web-page30,904
(defcustom isa-isatool-command39,1121
(defvar isatool-not-found 57,1780
(defun isa-set-isatool-command 60,1893
(defun isa-shell-command-to-string 83,2889
(defun isa-getenv 89,3113
(defcustom isabelle-program-name-override 109,3800
(defvar isabelle-prog-name 126,4384
(defun isa-tool-list-logics 129,4494
(defcustom isabelle-logics-available 136,4731
(defcustom isabelle-chosen-logic 146,5067
(defvar isabelle-chosen-logic-prev 162,5651
(defun isabelle-hack-local-variables-function 165,5773
(defun isabelle-set-prog-name 177,6214
(defun isabelle-choose-logic 202,7373
(defun isa-view-doc 221,8135
(defun isa-tool-list-docs 230,8399
(defconst isabelle-verbatim-regexp 257,9431
(defun isabelle-verbatim 260,9573
(defcustom isabelle-refresh-logics 267,9734
(defvar isabelle-docs-menu 275,10061
(defvar isabelle-logics-menu-entries 282,10347
(defun isabelle-logics-menu-calculate 285,10420
(defvar isabelle-time-to-refresh-logics 306,11062
(defun isabelle-logics-menu-refresh 310,11157
(defun isabelle-menu-bar-update-logics 325,11790
(defun isabelle-load-isar-keywords 341,12420
(defun isabelle-convert-idmarkup-to-subterm 362,13136
(defun isabelle-create-span-menu 386,14147
(defun isabelle-xml-sml-escapes 402,14589
(defun isabelle-process-pgip 405,14690

isar/isar.el,1202
(defcustom isar-keywords-name 31,727
(defpgdefault completion-table 48,1250
(defcustom isar-web-page50,1303
(defun isar-strip-terminators 64,1653
(defun isar-markup-ml 77,2030
(defun isar-mode-config-set-variables 82,2165
(defun isar-shell-mode-config-set-variables 151,5337
(defun isar-remove-file 239,8775
(defun isar-shell-compute-new-files-list 249,9138
(define-derived-mode isar-shell-mode 265,9659
(define-derived-mode isar-response-mode 270,9782
(define-derived-mode isar-goals-mode 275,9964
(define-derived-mode isar-mode 280,10139
(defpgdefault menu-entries337,12174
(defpgdefault help-menu-entries 367,13456
(defun isar-count-undos 370,13532
(defun isar-find-and-forget 397,14646
(defun isar-goal-command-p 436,16226
(defun isar-global-save-command-p 441,16403
(defvar isar-current-goal 462,17264
(defun isar-state-preserving-p 465,17330
(defvar isar-shell-current-line-width 490,18527
(defun isar-shell-adjust-line-width 495,18719
(defun isar-preprocessing 520,19623
(defun isar-mode-config 543,20890
(defun isar-shell-mode-config 554,21448
(defun isar-response-mode-config 560,21645
(defun isar-goals-mode-config 566,21826
(defun isar-goalhyplit-test 574,22093

isar/isar-find-theorems.el,778
(defun isar-find-theorems-minibuffer 18,713
(defun isar-find-theorems-form 32,1332
(defvar isar-find-theorems-data 74,3132
(defvar isar-find-theorems-widget-number 88,3467
(defvar isar-find-theorems-widget-pattern 91,3565
(defvar isar-find-theorems-widget-intro 94,3657
(defvar isar-find-theorems-widget-elim 97,3743
(defvar isar-find-theorems-widget-dest 100,3827
(defvar isar-find-theorems-widget-name 103,3911
(defvar isar-find-theorems-widget-simp 106,3998
(defun isar-find-theorems-create-searchform111,4144
(defun isar-find-theorems-create-help 251,8759
(defun isar-find-theorems-submit-searchform294,10931
(defun isar-find-theorems-parse-criteria 372,13308
(defun isar-find-theorems-parse-number 465,16408
(defun isar-find-theorems-filter-empty 475,16685

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,482
(defconst isar-keywords-minor206,3642
(defconst isar-keywords-control262,4396
(defconst isar-keywords-diag282,4873
(defconst isar-keywords-theory-begin338,5832
(defconst isar-keywords-theory-switch341,5885
(defconst isar-keywords-theory-end344,5940
(defconst isar-keywords-theory-heading347,5988
(defconst isar-keywords-theory-decl353,6095
(defconst isar-keywords-theory-script412,7076
(defconst isar-keywords-theory-goal416,7153
(defconst isar-keywords-qed429,7370
(defconst isar-keywords-qed-block436,7456
(defconst isar-keywords-qed-global439,7503
(defconst isar-keywords-proof-heading442,7552
(defconst isar-keywords-proof-goal447,7635
(defconst isar-keywords-proof-block454,7734
(defconst isar-keywords-proof-open458,7796
(defconst isar-keywords-proof-close461,7842
(defconst isar-keywords-proof-chain464,7889
(defconst isar-keywords-proof-decl471,7992
(defconst isar-keywords-proof-asm480,8113
(defconst isar-keywords-proof-asm-goal487,8208
(defconst isar-keywords-proof-script490,8263

isar/isar-mmm.el,83
(defconst isar-start-latex-regexp 23,698
(defconst isar-start-sml-regexp 35,1131

isar/isar-syntax.el,3494
(defconst isar-script-syntax-table-entries20,478
(defconst isar-script-syntax-table-alist44,880
(defun isar-init-syntax-table 53,1170
(defun isar-init-output-syntax-table 61,1417
(defconst isar-keyword-begin 77,1864
(defconst isar-keyword-end 78,1902
(defconst isar-keywords-theory-enclose80,1937
(defconst isar-keywords-theory85,2082
(defconst isar-keywords-save90,2227
(defconst isar-keywords-proof-enclose95,2356
(defconst isar-keywords-proof101,2538
(defconst isar-keywords-proof-context108,2743
(defconst isar-keywords-local-goal112,2857
(defconst isar-keywords-proper116,2969
(defconst isar-keywords-improper121,3102
(defconst isar-keywords-outline126,3248
(defconst isar-keywords-fume129,3313
(defconst isar-keywords-indent-open136,3531
(defconst isar-keywords-indent-close142,3715
(defconst isar-keywords-indent-enclose146,3820
(defun isar-regexp-simple-alt 155,4035
(defun isar-ids-to-regexp 175,4795
(defconst isar-ext-first 209,6201
(defconst isar-ext-rest 210,6268
(defconst isar-long-id-stuff 212,6340
(defconst isar-id 213,6414
(defconst isar-idx 214,6484
(defconst isar-string 216,6543
(defconst isar-any-command-regexp218,6603
(defconst isar-name-regexp222,6737
(defconst isar-improper-regexp228,7032
(defconst isar-save-command-regexp232,7180
(defconst isar-global-save-command-regexp235,7281
(defconst isar-goal-command-regexp238,7395
(defconst isar-local-goal-command-regexp241,7503
(defconst isar-comment-start 244,7616
(defconst isar-comment-end 245,7651
(defconst isar-comment-start-regexp 246,7684
(defconst isar-comment-end-regexp 247,7755
(defconst isar-string-start-regexp 249,7823
(defconst isar-string-end-regexp 250,7875
(defconst isar-antiq-regexp 255,7946
(defconst isar-nesting-regexp261,8099
(defun isar-nesting 264,8197
(defun isar-match-nesting 276,8618
(defface isabelle-class-name-face288,8949
(defface isabelle-tfree-name-face296,9132
(defface isabelle-tvar-name-face304,9321
(defface isabelle-free-name-face312,9509
(defface isabelle-bound-name-face320,9693
(defface isabelle-var-name-face328,9880
(defconst isabelle-class-name-face 336,10067
(defconst isabelle-tfree-name-face 337,10129
(defconst isabelle-tvar-name-face 338,10191
(defconst isabelle-free-name-face 339,10252
(defconst isabelle-bound-name-face 340,10313
(defconst isabelle-var-name-face 341,10375
(defvar isar-font-lock-keywords-1344,10437
(defun isar-output-flk 361,11488
(defvar isar-output-font-lock-keywords-1367,11740
(defvar isar-goals-font-lock-keywords385,12810
(defconst isar-linear-undo 419,13489
(defconst isar-undo 421,13532
(defun isar-remove 423,13575
(defun isar-undos 426,13650
(defun isar-cannot-undo 430,13756
(defconst isar-theory-start-regexp433,13826
(defconst isar-end-regexp439,13991
(defconst isar-undo-fail-regexp443,14092
(defconst isar-undo-skip-regexp447,14196
(defconst isar-undo-ignore-regexp450,14317
(defconst isar-undo-remove-regexp453,14382
(defconst isar-any-entity-regexp461,14557
(defconst isar-named-entity-regexp466,14744
(defconst isar-unnamed-entity-regexp471,14921
(defconst isar-next-entity-regexps474,15023
(defconst isar-generic-expression482,15334
(defconst isar-indent-any-regexp493,15651
(defconst isar-indent-inner-regexp495,15744
(defconst isar-indent-enclose-regexp497,15810
(defconst isar-indent-open-regexp499,15926
(defconst isar-indent-close-regexp501,16036
(defconst isar-outline-regexp507,16173
(defconst isar-outline-heading-end-regexp 511,16326

isar/isar-unicode-tokens.el,909
(defconst isar-control-region-format-regexp20,505
(defconst isar-control-char-format-regexp 23,599
(defconst isar-control-char-format 26,695
(defconst isar-control-characters28,742
(defconst isar-control-regions37,997
(defcustom isar-fontsymb-properties 47,1322
(defconst isar-token-format 63,1833
(defconst isar-token-variant-format-regexp 67,1985
(defconst isar-greek-letters-tokens70,2100
(defconst isar-misc-letters-tokens106,2796
(defconst isar-symbols-tokens114,2947
(defun isar-try-char 383,9079
(defconst isar-symbols-tokens-fallbacks387,9223
(defconst isar-bold-nums-tokens 411,10052
(defun isar-map-letters 423,10308
(defconst isar-script-letters-tokens429,10457
(defconst isar-roman-letters-tokens434,10595
(defconst isar-fraktur-letters-tokens439,10731
(defcustom isar-token-symbol-map444,10875
(defconst isar-symbol-shortcuts469,11691
(defcustom isar-shortcut-alist525,13249

lclam/lclam.el,524
(defcustom lclam-prog-name 15,386
(defcustom lclam-web-page21,534
(defun lclam-config 32,764
(defun lclam-shell-config 54,1558
(define-derived-mode lclam-proofscript-mode 74,2217
(define-derived-mode lclam-shell-mode 79,2340
(define-derived-mode lclam-response-mode 84,2474
(define-derived-mode lclam-goals-mode 88,2597
(defun lclam-mode 96,2825
(define-derived-mode thy-mode 133,3671
(defvar thy-mode-map 136,3769
(defun thy-add-menus 138,3796
(defun process-thy-file 177,5682
(defun update-thy-only 183,5883

lego/lego.el,1727
(defcustom lego-tags 19,494
(defcustom lego-test-all-name 24,630
(defpgdefault help-menu-entries30,788
(defpgdefault menu-entries34,948
(defvar lego-shell-process-output45,1250
(defconst lego-process-config53,1573
(defconst lego-pretty-set-width 64,2004
(defconst lego-interrupt-regexp 68,2147
(defcustom lego-www-home-page 73,2264
(defcustom lego-www-latest-release78,2388
(defcustom lego-www-refcard84,2566
(defcustom lego-library-www-page90,2715
(defvar lego-prog-name 99,2931
(defvar lego-shell-prompt-pattern 102,3000
(defvar lego-shell-cd 105,3121
(defvar lego-shell-abort-goal-regexp 108,3221
(defvar lego-shell-proof-completed-regexp 113,3413
(defvar lego-save-command-regexp116,3553
(defvar lego-goal-command-regexp118,3643
(defvar lego-kill-goal-command 121,3734
(defvar lego-forget-id-command 122,3777
(defvar lego-undoable-commands-regexp124,3823
(defvar lego-goal-regexp 133,4197
(defvar lego-outline-regexp135,4242
(defvar lego-outline-heading-end-regexp 141,4418
(defvar lego-shell-outline-regexp 143,4471
(defvar lego-shell-outline-heading-end-regexp 144,4523
(define-derived-mode lego-shell-mode 150,4802
(define-derived-mode lego-mode 157,4963
(define-derived-mode lego-goals-mode 168,5260
(defun lego-count-undos 179,5686
(defun lego-goal-command-p 199,6505
(defun lego-find-and-forget 204,6676
(defun lego-goal-hyp 246,8512
(defun lego-state-preserving-p 255,8710
(defvar lego-shell-current-line-width 271,9413
(defun lego-shell-adjust-line-width 279,9720
(defun lego-mode-config 298,10459
(defun lego-equal-module-filename 366,12520
(defun lego-shell-compute-new-files-list 372,12795
(defun lego-shell-mode-config 386,13321
(defun lego-goals-mode-config 435,15257

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,359
(defconst lego-keywords-save 17,402
(defconst lego-commands19,473
(defconst lego-keywords31,1033
(defconst lego-tacticals 36,1210
(defconst lego-error-regexp 39,1318
(defvar lego-id 42,1477
(defvar lego-ids 44,1504
(defconst lego-arg-list-regexp 48,1700
(defun lego-decl-defn-regexp 51,1816
(defconst lego-definiendum-alternative-regexp59,2188
(defvar lego-font-lock-terms63,2372
(defconst lego-goal-with-hole-regexp89,3228
(defconst lego-save-with-hole-regexp94,3451
(defvar lego-font-lock-keywords-199,3668
(defun lego-init-syntax-table 110,4135

phox/phox.el,602
(defcustom phox-prog-name 31,917
(defcustom phox-sym-lock-enabled 36,1019
(defcustom phox-web-page42,1128
(defcustom phox-doc-dir 48,1278
(defcustom phox-lib-dir 54,1426
(defcustom phox-tags-program 60,1570
(defcustom phox-tags-doc 66,1750
(defcustom phox-etags 72,1888
(defpgdefault menu-entries93,2340
(defun phox-config 107,2533
(defun phox-shell-config 148,4424
(define-derived-mode phox-mode 173,5353
(define-derived-mode phox-shell-mode 189,5819
(define-derived-mode phox-response-mode 194,5947
(define-derived-mode phox-goals-mode 207,6389
(defpgdefault completion-table233,7273

phox/phox-extraction.el,382
(defvar phox-prog-orig 11,481
(defun phox-prog-flags-modify(13,549
(defun phox-prog-flags-extract(42,1353
(defun phox-prog-flags-erase(53,1644
(defun phox-toggle-extraction(61,1840
(defun phox-compile-theorem(73,2242
(defun phox-compile-theorem-on-cursor(79,2468
(defun phox-output 95,2947
(defun phox-output-theorem 105,3161
(defun phox-output-theorem-on-cursor(112,3461

phox/phox-font.el,123
(defconst phox-font-lock-keywords6,282
(defconst phox-sym-lock-keywords-table65,2401
(defun phox-sym-lock-start 88,2975

phox/phox-fun.el,679
(defun phox-init-syntax-table 67,2393
(defvar phox-top-keywords83,2866
(defvar phox-proof-keywords131,3321
(defun phox-find-and-forget 172,3671
(defun phox-assert-next-command-interactive 251,6096
(defun phox-depend-theorem(270,6927
(defun phox-eshow-extlist(279,7217
(defun phox-flag-name(293,7816
(defun phox-path(304,8119
(defun phox-print-expression(315,8356
(defun phox-print-sort-expression(328,8814
(defun phox-priority-symbols-list(339,9127
(defun phox-search-string(351,9500
(defun phox-constraints(366,10028
(defun phox-goals(377,10285
(defvar phox-state-menu389,10495
(defun phox-delete-symbol(414,11485
(defun phox-delete-symbol-on-cursor(420,11694

phox/phox-lang.el,283
(defvar phox-lang8,279
(defun phox-lang-absurd 17,496
(defun phox-lang-suppress 22,591
(defun phox-lang-opendef 27,790
(defun phox-lang-instance 32,909
(defun phox-lang-lock 37,1038
(defun phox-lang-unlock 42,1175
(defun phox-lang-prove 47,1318
(defun phox-lang-let 52,1455

phox/phox-outline.el,70
(defun phox-outline-level(32,1113
(defun phox-setup-outline 46,1587

phox/phox-pbrpm.el,512
(defun phox-pbrpm-left-paren-p 27,1189
(defun phox-pbrpm-right-paren-p 34,1392
(defun phox-pbrpm-menu-from-string 42,1596
(defun phox-pbrpm-rename-in-cmd 51,1930
(defun phox-pbrpm-get-region-name 84,3184
(defun  phox-pbrpm-escape-string 87,3311
(defun phox-pbrpm-generate-menu 91,3446
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
289,10635
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
290,10699
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
291,10761

phox/phox-sym-lock.el,1353
(defvar phox-sym-lock-sym-count 34,1598
(defvar phox-sym-lock-ext-start 37,1668
(defvar phox-sym-lock-ext-end 39,1790
(defvar phox-sym-lock-font-size 42,1909
(defvar phox-sym-lock-keywords 47,2099
(defvar phox-sym-lock-enabled 52,2275
(defvar phox-sym-lock-color 57,2437
(defvar phox-sym-lock-mouse-face 62,2655
(defvar phox-sym-lock-mouse-face-enabled 67,2845
(defconst phox-sym-lock-with-mule 72,3035
(defun phox-sym-lock-gen-symbol 75,3119
(defun phox-sym-lock-make-symbols-atomic 83,3422
(defun phox-sym-lock-compute-font-size 110,4364
(defvar phox-sym-lock-font-name148,5784
(defun phox-sym-lock-set-foreground 190,7270
(defun phox-sym-lock-translate-char 204,7879
(defun phox-sym-lock-translate-char-or-string 212,8147
(defun phox-sym-lock-remap-face 219,8374
(defvar phox-sym-lock-clear-face239,9364
(defun phox-sym-lock 251,9786
(defun phox-sym-lock-rec 260,10190
(defun phox-sym-lock-atom-face 266,10343
(defun phox-sym-lock-pre-idle-hook-first 271,10639
(defun phox-sym-lock-pre-idle-hook-last 279,10997
(defun phox-sym-lock-enable 288,11372
(defun phox-sym-lock-disable 301,11785
(defun phox-sym-lock-mouse-face-enable 314,12203
(defun phox-sym-lock-mouse-face-disable 321,12418
(defun phox-sym-lock-font-lock-hook 328,12637
(defun font-lock-set-defaults 343,13330
(defun phox-sym-lock-patch-keywords 354,13708

phox/phox-tags.el,305
(defun phox-tags-add-table(21,767
(defun phox-tags-reset-table(29,1096
(defun phox-tags-add-doc-table(34,1206
(defun phox-tags-add-lib-table(40,1355
(defun phox-tags-add-local-table(46,1491
(defun phox-tags-create-local-table(52,1674
(defun phox-complete-tag(63,1926
(defvar phox-tags-menu70,2035

plastic/plastic.el,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,592
(defcustom twelf-info-dir31,750
(defun twelf-add-read-declaration 100,3260
(defun twelf-set-syntax 113,3595
(defun twelf-set-word 115,3692
(defun twelf-set-symbol 116,3754
(defun twelf-map-string 118,3818
(defun twelf-mode-extra-config 165,5880
(defconst twelf-syntax-menu171,6086
(defpacustom chatter 185,6453
(defpacustom double-check 190,6546
(defpacustom print-implicit 194,6683
(defpgdefault menu-entries206,6827

twelf/twelf-font.el,917
(defun twelf-font-create-face 31,837
(defvar twelf-font-dark-background 38,1095
(defvar twelf-font-patterns64,2453
(defun twelf-font-fontify-decl 105,4303
(defun twelf-font-fontify-buffer 115,4600
(defun twelf-font-unfontify 122,4859
(defvar font-lock-message-threshold 127,5033
(defun twelf-font-fontify-region 129,5111
(defun twelf-font-highlight 195,7611
(defun twelf-font-find-delimited-comment 204,8068
(defun twelf-font-find-decl 223,8748
(defun twelf-font-find-binder 239,9238
(defun twelf-font-find-parm 301,11095
(defun twelf-font-find-evar 308,11418
(defun twelf-current-decl 330,12160
(defun twelf-next-decl 357,13316
(defconst *whitespace* 382,14338
(defconst *twelf-comment-start* 385,14436
(defconst *twelf-id-chars* 388,14565
(defun skip-twelf-comments-and-whitespace 391,14683
(defun twelf-end-of-par 403,15157
(defun skip-ahead 426,15931
(defun current-line-absolute 438,16353

twelf/twelf-old.el,6958
(defvar twelf-indent 212,8772
(defvar twelf-infix-regexp 215,8832
(defvar twelf-server-program 219,9027
(defvar twelf-info-file 222,9108
(defvar twelf-server-display-commands 225,9181
(defvar twelf-highlight-range-function 230,9429
(defvar twelf-focus-function 235,9712
(defvar twelf-server-echo-commands 241,9992
(defvar twelf-save-silently 244,10113
(defvar twelf-server-timeout 248,10285
(defvar twelf-sml-program 252,10432
(defvar twelf-sml-args 255,10504
(defvar twelf-sml-display-queries 258,10570
(defvar twelf-mode-hook 261,10678
(defvar twelf-server-mode-hook 264,10772
(defvar twelf-config-mode-hook 267,10880
(defvar twelf-sml-mode-hook 270,10994
(defvar twelf-to-twelf-sml-mode 273,11075
(defvar twelf-config-mode 276,11167
(defvar *twelf-server-buffer-name* 283,11431
(defvar *twelf-server-buffer* 286,11535
(defvar *twelf-server-process-name* 289,11623
(defvar *twelf-config-buffer* 292,11714
(defvar *twelf-config-time* 295,11808
(defvar *twelf-config-list* 298,11921
(defvar *twelf-server-last-process-mark* 301,12033
(defvar *twelf-last-region-sent* 304,12151
(defvar *twelf-last-input-buffer* 311,12475
(defvar *twelf-error-pos* 315,12598
(defconst *twelf-read-functions*318,12674
(defconst *twelf-parm-table*325,12912
(defvar twelf-chatter 338,13288
(defvar twelf-double-check 346,13505
(defvar twelf-print-implicit 349,13592
(defconst *twelf-track-parms*352,13684
(defun install-basic-twelf-keybindings 363,14108
(defun install-twelf-keybindings 388,15077
(defvar twelf-mode-map 404,15842
(defvar twelf-mode-syntax-table 416,16278
(defun set-twelf-syntax 419,16357
(defun set-word 421,16454
(defun set-symbol 422,16509
(defun map-string 424,16567
(defconst *whitespace* 456,18044
(defconst *twelf-comment-start* 459,18142
(defconst *twelf-id-chars* 462,18271
(defun skip-twelf-comments-and-whitespace 465,18389
(defun twelf-end-of-par 477,18863
(defun twelf-current-decl 500,19637
(defun twelf-mark-decl 527,20793
(defun twelf-indent-decl 536,21059
(defun twelf-indent-region 545,21345
(defun twelf-indent-lines 556,21669
(defun twelf-comment-indent 564,21842
(defun looked-at 575,22198
(defun twelf-indent-line 580,22370
(defun twelf-indent-line-to 613,24113
(defun twelf-calculate-indent 626,24568
(defun twelf-dsb 641,25192
(defun twelf-mode-variables 667,26604
(defun twelf-mode 689,27417
(defun twelf-info 904,35799
(defconst twelf-error-regexp918,36339
(defconst twelf-error-fields-regexp922,36450
(defconst twelf-error-decl-regexp928,36663
(defun looked-at-nth 932,36812
(defun looked-at-nth-int 938,36994
(defun twelf-error-parser 943,37112
(defun twelf-error-decl 957,37715
(defun twelf-mark-relative 963,37894
(defun twelf-mark-absolute 979,38564
(defun twelf-find-decl 1004,39450
(defun twelf-next-error 1019,40006
(defun twelf-goto-error 1087,42816
(defun twelf-convert-standard-filename 1101,43354
(defun string-member 1113,43849
(defun twelf-config-proceed-p 1125,44341
(defun twelf-save-if-config 1132,44603
(defun twelf-config-save-some-buffers 1145,45075
(defun twelf-save-check-config 1149,45240
(defun twelf-check-config 1164,45796
(defun twelf-save-check-file 1176,46236
(defun twelf-buffer-substring 1192,46959
(defun twelf-buffer-substring-dot 1198,47221
(defun twelf-check-declaration 1204,47487
(defun twelf-highlight-range-zmacs 1227,48547
(defun twelf-focus 1233,48797
(defun twelf-focus-noop 1239,49063
(defun twelf-type-const 1322,52685
(defvar twelf-server-mode-map 1439,57827
(defconst twelf-server-cd-regexp 1451,58379
(defun looked-at-string 1454,58519
(defun twelf-server-directory-tracker 1458,58660
(defun twelf-input-filter 1480,59840
(defun twelf-server-mode 1486,60095
(defun twelf-parse-config 1519,61312
(defun twelf-server-read-config 1537,62204
(defun twelf-server-sync-config 1546,62541
(defun twelf-get-server-buffer 1576,64047
(defun twelf-init-variables 1593,64721
(defun twelf-server 1600,64934
(defun twelf-server-process 1642,66848
(defun twelf-server-display 1651,67254
(defun display-server-buffer 1658,67528
(defun twelf-server-send-command 1673,68260
(defun twelf-accept-process-output 1694,69220
(defun twelf-server-wait 1703,69659
(defun twelf-server-quit 1745,71797
(defun twelf-server-interrupt 1750,71918
(defun twelf-reset 1755,72054
(defun twelf-config-directory 1760,72198
(defun twelf-server-configure 1771,72612
(defun natp 1844,75904
(defun twelf-read-nat 1848,76005
(defun twelf-read-bool 1857,76272
(defun twelf-read-limit 1863,76420
(defun twelf-read-strategy 1873,76723
(defun twelf-read-value 1879,76875
(defun twelf-set 1883,77038
(defun twelf-set-parm 1896,77515
(defun track-parm 1905,77812
(defun twelf-toggle-double-check 1910,77986
(defun twelf-toggle-print-implicit 1916,78189
(defun twelf-get 1922,78402
(defun twelf-timers-reset 1936,79028
(defun twelf-timers-show 1941,79148
(defun twelf-timers-check 1947,79299
(defun twelf-server-restart 1953,79464
(defun twelf-config-mode 1969,80141
(defun twelf-config-mode-check 1985,80740
(defun twelf-tag 1994,81190
(defun twelf-tag-files 2022,82454
(default: *tags-errors*)2026,82757
(defun twelf-tag-file 2047,83508
(defun twelf-next-decl 2082,84730
(defun skip-ahead 2107,85752
(defun current-line-absolute 2119,86174
(defun new-temp-buffer 2124,86384
(defun rev-relativize 2135,86768
(defvar twelf-sml-mode-map 2149,87228
(defconst twelf-sml-prompt-regexp 2159,87606
(defun expand-dir 2161,87661
(defun twelf-sml-cd 2168,87922
(defconst twelf-sml-cd-regexp 2180,88411
(defun twelf-sml-directory-tracker 2183,88545
(defun twelf-sml-mode 2199,89390
(defun twelf-sml 2250,91324
(defun switch-to-twelf-sml 2270,92284
(defun display-twelf-sml-buffer 2281,92633
(defun twelf-sml-send-string 2297,93349
(defun twelf-sml-send-region 2302,93553
(defun twelf-sml-send-query 2326,94759
(defun twelf-sml-send-newline 2336,95156
(defun twelf-sml-send-semicolon 2344,95484
(defun twelf-sml-status 2352,95818
(defvar twelf-sml-init 2374,96765
(defun twelf-sml-set-mode 2377,96942
(defun twelf-sml-quit 2403,98119
(defun twelf-sml-process-buffer 2408,98231
(defun twelf-sml-process 2412,98347
(defvar twelf-to-twelf-sml-mode 2424,98863
(defun install-twelf-to-twelf-sml-keybindings 2427,98948
(defvar twelf-to-twelf-sml-mode-map 2437,99333
(defun twelf-to-twelf-sml-mode 2448,99846
(defconst twelf-at-point-menu2498,101713
(defconst twelf-server-state-menu2508,102085
(defconst twelf-error-menu2518,102402
(defconst twelf-tags-menu2524,102546
(defun twelf-toggle-server-display-commands 2534,102831
(defconst twelf-options-menu2537,102955
(defconst twelf-timers-menu2572,104693
(defconst twelf-syntax-menu2585,105187
(defun twelf-add-menu 2612,106053
(defun twelf-remove-menu 2616,106155
(defun twelf-reset-menu 2620,106253
(defun twelf-server-add-menu 2647,107152
(defun twelf-server-remove-menu 2651,107275
(defun twelf-server-reset-menu 2655,107387

generic/pg-assoc.el,82
(defun proof-associated-buffers 36,1066
(defun proof-associated-windows 46,1278

generic/pg-autotest.el,442
(defvar pg-autotest-success 24,544
(defun pg-autotest-find-file 28,628
(defun pg-autotest-find-file-restart 35,908
(defmacro pg-autotest 48,1356
(defun pg-autotest-script-wholefile 62,1703
(defun pg-autotest-retract-file 79,2316
(defun pg-autotest-assert-processed 85,2452
(defun pg-autotest-assert-unprocessed 92,2706
(defun pg-autotest-message 99,2966
(defun pg-autotest-quit-prover 106,3159
(defun pg-autotest-finished 112,3340

generic/pg-custom.el,554
(defpgcustom maths-menu-enable 32,1066
(defpgcustom unicode-tokens-enable 38,1246
(defpgcustom mmm-enable 44,1423
(defpgcustom script-indent 53,1777
(defconst proof-toolbar-entries-default58,1914
(defpgcustom toolbar-entries 85,3573
(defpgcustom prog-args 104,4306
(defpgcustom prog-env 117,4881
(defpgcustom favourites 126,5307
(defpgcustom menu-entries 131,5496
(defpgcustom help-menu-entries 138,5732
(defpgcustom keymap 145,5995
(defpgcustom completion-table 150,6167
(defpgcustom tags-program 161,6541
(defpgcustom use-holes 170,6925

generic/pg-goals.el,287
(define-derived-mode proof-goals-mode 30,639
(define-key proof-goals-mode-map 59,1515
(define-key proof-goals-mode-map 61,1567
(define-key proof-goals-mode-map 62,1635
(define-key proof-goals-mode-map 68,2068
(defun proof-goals-config-done 76,2185
(defun pg-goals-display 84,2451

generic/pg-pbrpm.el,1803
(defvar pg-pbrpm-use-buffer-menu 22,548
(defvar pg-pbrpm-start-goal-regexp 25,670
(defvar pg-pbrpm-start-goal-regexp-par-num 29,827
(defvar pg-pbrpm-end-goal-regexp 32,950
(defvar pg-pbrpm-start-hyp-regexp 36,1102
(defvar pg-pbrpm-start-hyp-regexp-par-num 40,1263
(defvar pg-pbrpm-start-concl-regexp 44,1470
(defvar pg-pbrpm-auto-select-regexp 48,1634
(defvar pg-pbrpm-buffer-menu 55,1795
(defvar pg-pbrpm-spans 56,1829
(defvar pg-pbrpm-goal-description 57,1857
(defvar pg-pbrpm-windows-dialog-bug 58,1896
(defvar pbrpm-menu-desc 59,1937
(defun pg-pbrpm-erase-buffer-menu 61,1967
(defun pg-pbrpm-menu-change-hook 68,2151
(defun pg-pbrpm-create-reset-buffer-menu 86,2727
(defun pg-pbrpm-analyse-goal-buffer 101,3356
(defun pg-pbrpm-button-action 161,5766
(defun pg-pbrpm-exists 168,5992
(defun pg-pbrpm-eliminate-id 172,6104
(defun pg-pbrpm-build-menu 180,6350
(defun pg-pbrpm-setup-span 243,8676
(defun pg-pbrpm-run-command 303,10994
(defun pg-pbrpm-get-pos-info 332,12304
(defun pg-pbrpm-get-region-info 374,13611
(defun pg-pbrpm-auto-select-around-point 385,14025
(defun pg-pbrpm-translate-position 400,14555
(defun pg-pbrpm-process-click 408,14813
(defvar pg-pbrpm-remember-region-selected-region 428,15838
(defvar pg-pbrpm-regions-list 429,15892
(defun pg-pbrpm-erase-regions-list 431,15928
(defun pg-pbrpm-filter-regions-list 440,16236
(defface pg-pbrpm-multiple-selection-face447,16499
(defface pg-pbrpm-menu-input-face455,16701
(defun pg-pbrpm-do-remember-region 463,16891
(defun pg-pbrpm-remember-region-drag-up-hook 484,17739
(defun pg-pbrpm-remember-region-click-hook 488,17910
(defun pg-pbrpm-remember-region 493,18095
(defun pg-pbrpm-process-region 507,18810
(defun pg-pbrpm-process-regions-list 525,19539
(defun pg-pbrpm-region-expression 529,19722

generic/pg-pgip.el,2889
(defalias 'pg-pgip-debug pg-pgip-debug
35,920
(defalias 'pg-pgip-error pg-pgip-error
36,961
(defalias 'pg-pgip-warning pg-pgip-warning
37,996
(defconst pg-pgip-version-supported 39,1046
(defun pg-pgip-process-packet 43,1152
(defvar pg-pgip-last-seen-id 53,1724
(defvar pg-pgip-last-seen-seq 54,1758
(defun pg-pgip-process-pgip 56,1794
(defun pg-pgip-process-msg 75,2725
(defvar pg-pgip-post-process-functions89,3295
(defun pg-pgip-post-process 99,3783
(defun pg-pgip-process-askpgip 115,4394
(defun pg-pgip-process-usespgip 121,4599
(defun pg-pgip-process-usespgml 125,4763
(defun pg-pgip-process-pgmlconfig 129,4927
(defun pg-pgip-process-proverinfo 145,5544
(defun pg-pgip-process-hasprefs 162,6209
(defun pg-pgip-haspref 176,6841
(defun pg-pgip-process-prefval 195,7617
(defun pg-pgip-process-guiconfig 222,8326
(defvar proof-assistant-idtables 229,8443
(defun pg-pgip-process-ids 232,8560
(defun pg-complete-idtable-symbol 258,9636
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
263,9728
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
264,9784
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
265,9840
(defun pg-pgip-process-idvalue 268,9898
(defun pg-pgip-process-menuadd 280,10234
(defun pg-pgip-process-menudel 283,10277
(defun pg-pgip-process-ready 292,10510
(defun pg-pgip-process-cleardisplay 295,10551
(defun pg-pgip-process-proofstate 309,11008
(defun pg-pgip-process-normalresponse 313,11085
(defun pg-pgip-process-errorresponse 317,11209
(defun pg-pgip-process-scriptinsert 321,11332
(defun pg-pgip-process-metainforesponse 326,11466
(defun pg-pgip-process-informfileloaded 335,11707
(defun pg-pgip-process-informfileretracted 341,11973
(defun pg-pgip-process-brokerstatus 354,12450
(defun pg-pgip-process-proveravailmsg 357,12498
(defun pg-pgip-process-newprovermsg 360,12548
(defun pg-pgip-process-proverstatusmsg 363,12596
(defvar pg-pgip-srcids 372,12843
(defun pg-pgip-process-newfile 376,12950
(defun pg-pgip-process-filestatus 392,13538
(defun pg-pgip-process-newobj 412,14193
(defun pg-pgip-process-delobj 415,14235
(defun pg-pgip-process-objectstatus 418,14277
(defun pg-pgip-process-parsescript 432,14632
(defun pg-pgip-get-pgiptype 455,15507
(defun pg-pgip-default-for 475,16300
(defun pg-pgip-subst-for 488,16695
(defun pg-pgip-interpret-value 500,17038
(defun pg-pgip-interpret-choice 518,17723
(defun pg-pgip-string-of-command 549,18740
(defconst pg-pgip-id566,19501
(defvar pg-pgip-refseq 572,19781
(defvar pg-pgip-refid 574,19878
(defvar pg-pgip-seq 577,19970
(defun pg-pgip-assemble-packet 579,20034
(defun pg-pgip-issue 597,20846
(defun pg-pgip-maybe-askpgip 614,21458
(defun pg-pgip-askprefs 620,21649
(defun pg-pgip-askids 624,21763
(defun pg-pgip-reset 637,22051
(defconst pg-pgip-start-element-regexp 668,22749
(defconst pg-pgip-end-element-regexp 669,22801

generic/pg-response.el,1078
(deflocal pg-response-eagerly-raise 31,731
(define-derived-mode proof-response-mode 41,956
(defun proof-response-config-done 65,1966
(defvar pg-response-special-display-regexp 76,2313
(defconst proof-multiframe-parameters80,2480
(defun proof-multiple-frames-enable 89,2779
(defun proof-three-window-enable 99,3108
(defun proof-select-three-b 102,3171
(defun proof-display-three-b 117,3640
(defvar pg-frame-configuration 129,4049
(defun pg-cache-frame-configuration 133,4196
(defun proof-layout-windows 137,4367
(defun proof-delete-other-frames 177,6132
(defvar pg-response-erase-flag 208,7222
(defun pg-response-maybe-erase212,7351
(defun pg-response-display 243,8536
(defun pg-response-display-with-face 275,9661
(defun pg-response-clear-displays 301,10455
(defun proof-next-error 320,11042
(defun pg-response-has-error-location 401,13958
(defvar proof-trace-last-fontify-pos 424,14791
(defun proof-trace-fontify-pos 426,14834
(defun proof-trace-buffer-display 434,15147
(defun proof-trace-buffer-finish 459,16093
(defun pg-thms-buffer-clear 481,16664

generic/pg-thymodes.el,152
(defmacro pg-defthymode 23,500
(defmacro pg-do-unless-null 71,2311
(defun pg-symval 76,2398
(defun pg-modesym 82,2553
(defun pg-modesymval 86,2667

generic/pg-user.el,3075
(defmacro proof-maybe-save-point 31,807
(defun proof-maybe-follow-locked-end 41,1104
(defun proof-assert-next-command-interactive 55,1469
(defun proof-process-buffer 65,1840
(defun proof-undo-last-successful-command 79,2157
(defun proof-undo-and-delete-last-successful-command 84,2319
(defun proof-undo-last-successful-command-1 98,2882
(defun proof-retract-buffer 114,3447
(defun proof-retract-current-goal 123,3727
(defun proof-interrupt-process 142,4233
(defun proof-goto-command-start 169,5222
(defun proof-goto-command-end 192,6162
(defun proof-mouse-goto-point 213,6797
(defvar proof-minibuffer-history 229,7040
(defun proof-minibuffer-cmd 232,7135
(defun proof-frob-locked-end 276,8750
(defmacro proof-if-setting-configured 337,10678
(defmacro proof-define-assistant-command 345,10947
(defmacro proof-define-assistant-command-witharg 358,11402
(defun proof-issue-new-command 378,12225
(defun proof-cd-sync 422,13668
(defun proof-electric-terminator-enable 481,15433
(defun proof-electric-term-incomment-fn 489,15735
(defun proof-process-electric-terminator 509,16488
(defun proof-electric-terminator 536,17636
(defun proof-add-completions 558,18282
(defun proof-script-complete 578,19036
(defun pg-insert-last-output-as-comment 606,19627
(defun pg-copy-span-contents 625,20233
(defun pg-numth-span-higher-or-lower 642,20791
(defun pg-control-span-of 668,21537
(defun pg-move-span-contents 674,21741
(defun pg-fixup-children-spans 726,23921
(defun pg-move-region-down 736,24184
(defun pg-move-region-up 745,24477
(defun proof-forward-command 775,25315
(defun proof-backward-command 796,26036
(defun pg-pos-for-event 818,26387
(defun pg-span-for-event 824,26608
(defun pg-span-context-menu 828,26752
(defun pg-toggle-visibility 843,27207
(defun pg-create-in-span-context-menu 853,27529
(defun pg-span-undo 886,28873
(defun pg-goals-buffers-hint 932,30283
(defun pg-slow-fontify-tracing-hint 936,30465
(defun pg-response-buffers-hint 940,30636
(defun pg-jump-to-end-hint 950,30998
(defun pg-processing-complete-hint 954,31129
(defun pg-next-error-hint 971,31828
(defun pg-hint 976,31980
(defun pg-identifier-under-mouse-query 991,32514
(defun proof-imenu-enable 1032,33998
(defvar pg-input-ring 1063,35044
(defvar pg-input-ring-index 1066,35101
(defvar pg-stored-incomplete-input 1069,35173
(defun pg-previous-input 1072,35276
(defun pg-next-input 1086,35733
(defun pg-delete-input 1091,35855
(defun pg-get-old-input 1104,36193
(defun pg-restore-input 1118,36584
(defun pg-search-start 1129,36874
(defun pg-regexp-arg 1141,37366
(defun pg-search-arg 1153,37814
(defun pg-previous-matching-input-string-position 1167,38231
(defun pg-previous-matching-input 1194,39396
(defun pg-next-matching-input 1213,40246
(defvar pg-matching-input-from-input-string 1221,40629
(defun pg-previous-matching-input-from-input 1225,40743
(defun pg-next-matching-input-from-input 1243,41508
(defun pg-add-to-input-history 1254,41887
(defun pg-remove-from-input-history 1266,42340
(defun  pg-clear-input-ring 1277,42722

generic/pg-vars.el,1106
(defvar proof-assistant-cusgrp 20,380
(defvar proof-assistant-internals-cusgrp 26,642
(defvar proof-assistant 32,913
(defvar proof-assistant-symbol 37,1135
(defvar proof-mode-for-shell 50,1679
(defvar proof-mode-for-response 55,1871
(defvar proof-mode-for-goals 60,2098
(defvar proof-mode-for-script 65,2288
(defvar proof-ready-for-assistant-hook 70,2466
(defvar proof-shell-busy 80,2753
(defvar proof-included-files-list 85,2909
(defvar proof-script-buffer 107,3922
(defvar proof-previous-script-buffer 110,4014
(defvar proof-shell-buffer 114,4185
(defvar proof-goals-buffer 117,4271
(defvar proof-response-buffer 120,4326
(defvar proof-trace-buffer 123,4387
(defvar proof-thms-buffer 127,4541
(defvar proof-shell-error-or-interrupt-seen 131,4696
(defvar pg-response-next-error 136,4920
(defvar proof-shell-proof-completed 139,5027
(defvar proof-terminal-string 151,5571
(defvar proof-shell-last-output 161,5761
(defvar proof-assistant-settings 165,5902
(defvar pg-tracing-slow-mode 172,6265
(defvar proof-nesting-depth 175,6354
(defvar proof-last-theorem-dependencies 182,6589

generic/pg-xml.el,1140
(defalias 'pg-xml-error pg-xml-error
16,366
(defun pg-xml-parse-string 39,1008
(defun pg-xml-parse-buffer 50,1334
(defun pg-xml-get-attr 72,2067
(defun pg-xml-child-elts 80,2369
(defun pg-xml-child-elt 85,2574
(defun pg-xml-get-child 93,2856
(defun pg-xml-get-text-content 103,3228
(defmacro pg-xml-attr 114,3578
(defmacro pg-xml-node 116,3640
(defconst pg-xml-header119,3732
(defun pg-xml-string-of 123,3808
(defun pg-xml-output-internal 134,4175
(defun pg-xml-cdata 168,5325
(defun pg-pgip-get-icon 176,5518
(defsubst pg-pgip-get-name 180,5666
(defsubst pg-pgip-get-version 183,5783
(defsubst pg-pgip-get-descr 186,5906
(defsubst pg-pgip-get-thmname 189,6025
(defsubst pg-pgip-get-thyname 192,6148
(defsubst pg-pgip-get-url 195,6271
(defsubst pg-pgip-get-srcid 198,6386
(defsubst pg-pgip-get-proverid 201,6505
(defsubst pg-pgip-get-symname 204,6630
(defsubst pg-pgip-get-prefcat 207,6750
(defsubst pg-pgip-get-default 210,6878
(defsubst pg-pgip-get-objtype 213,7001
(defsubst pg-pgip-get-value 216,7124
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
219,7194
(defun pg-pgip-get-pgmltext 221,7253

generic/proof-auxmodes.el,149
(defun proof-mmm-support-available 21,550
(defun proof-maths-menu-support-available 45,1168
(defun proof-unicode-tokens-support-available 59,1586

generic/proof-config.el,10807
(defgroup proof-user-options 84,2964
(defun proof-set-value 92,3143
(defcustom proof-electric-terminator-enable 125,4266
(defcustom proof-toolbar-enable 137,4798
(defcustom proof-imenu-enable 143,4971
(defcustom pg-show-hints 149,5142
(defcustom proof-trace-output-slow-catchup 155,5337
(defcustom proof-strict-state-preserving 165,5834
(defcustom proof-strict-read-only 178,6443
(defcustom proof-allow-undo-in-read-only 187,6836
(defcustom proof-three-window-enable 195,7169
(defcustom proof-multiple-frames-enable 214,7919
(defcustom proof-delete-empty-windows 223,8252
(defcustom proof-shrink-windows-tofit 234,8783
(defcustom proof-query-file-save-when-activating-scripting241,9055
(defcustom proof-one-command-per-line257,9775
(defcustom proof-prog-name-ask264,10002
(defcustom proof-prog-name-guess270,10162
(defcustom proof-tidy-response278,10427
(defcustom proof-keep-response-history292,10890
(defcustom pg-input-ring-size 302,11278
(defcustom proof-general-debug 307,11430
(defcustom proof-experimental-features 317,11802
(defcustom proof-follow-mode 331,12337
(defcustom proof-auto-action-when-deactivating-scripting 355,13514
(defcustom proof-script-command-separator 378,14463
(defcustom proof-rsh-command 386,14755
(defcustom proof-disappearing-proofs 402,15305
(defgroup proof-faces 429,15951
(defconst pg-defface-window-systems436,16133
(defmacro proof-face-specs 449,16686
(defface proof-queue-face464,17138
(defface proof-locked-face472,17416
(defface proof-declaration-name-face482,17737
(defface proof-tacticals-name-face491,18023
(defface proof-tactics-name-face500,18285
(defface proof-error-face509,18550
(defface proof-warning-face517,18740
(defface proof-eager-annotation-face526,18997
(defface proof-debug-message-face534,19215
(defface proof-boring-face542,19414
(defface proof-mouse-highlight-face550,19606
(defface proof-highlight-dependent-face558,19802
(defface proof-highlight-dependency-face566,20011
(defface proof-active-area-face574,20208
(defconst proof-face-compat-doc 583,20598
(defconst proof-queue-face 584,20678
(defconst proof-locked-face 585,20746
(defconst proof-declaration-name-face 586,20816
(defconst proof-tacticals-name-face 587,20906
(defconst proof-tactics-name-face 588,20992
(defconst proof-error-face 589,21074
(defconst proof-warning-face 590,21142
(defconst proof-eager-annotation-face 591,21214
(defconst proof-debug-message-face 592,21304
(defconst proof-boring-face 593,21388
(defconst proof-mouse-highlight-face 594,21458
(defconst proof-highlight-dependent-face 595,21546
(defconst proof-highlight-dependency-face 596,21642
(defconst proof-active-area-face 597,21740
(defgroup prover-config 610,21884
(defcustom proof-guess-command-line 652,23213
(defcustom proof-assistant-home-page 667,23708
(defcustom proof-context-command 673,23878
(defcustom proof-info-command 678,24012
(defcustom proof-showproof-command 685,24283
(defcustom proof-goal-command 690,24419
(defcustom proof-save-command 698,24716
(defcustom proof-find-theorems-command 706,25025
(defcustom proof-assistant-true-value 713,25335
(defcustom proof-assistant-false-value 719,25525
(defcustom proof-assistant-format-int-fn 725,25719
(defcustom proof-assistant-format-string-fn 732,25968
(defcustom proof-assistant-setting-format 739,26235
(defgroup proof-script 761,26930
(defcustom proof-terminal-char 766,27060
(defcustom proof-script-sexp-commands 776,27447
(defcustom proof-script-command-end-regexp 787,27904
(defcustom proof-script-command-start-regexp 805,28723
(defcustom proof-script-use-old-parser 816,29184
(defcustom proof-script-integral-proofs 828,29670
(defcustom proof-script-fly-past-comments 843,30326
(defcustom proof-script-parse-function 848,30497
(defcustom proof-script-comment-start 866,31140
(defcustom proof-script-comment-start-regexp 877,31577
(defcustom proof-script-comment-end 885,31896
(defcustom proof-script-comment-end-regexp 897,32318
(defcustom pg-insert-output-as-comment-fn 905,32629
(defcustom proof-string-start-regexp 911,32881
(defcustom proof-string-end-regexp 916,33046
(defcustom proof-case-fold-search 921,33207
(defcustom proof-save-command-regexp 930,33619
(defcustom proof-save-with-hole-regexp 935,33729
(defcustom proof-save-with-hole-result 947,34183
(defcustom proof-goal-command-regexp 957,34631
(defcustom proof-goal-with-hole-regexp 966,35019
(defcustom proof-goal-with-hole-result 978,35462
(defcustom proof-non-undoables-regexp 987,35846
(defcustom proof-nested-undo-regexp 998,36301
(defcustom proof-ignore-for-undo-count 1014,37013
(defcustom proof-script-next-entity-regexps 1022,37316
(defcustom proof-script-find-next-entity-fn1066,39057
(defcustom proof-script-imenu-generic-expression 1086,39897
(defcustom proof-goal-command-p 1094,40236
(defcustom proof-really-save-command-p 1105,40727
(defcustom proof-completed-proof-behaviour 1114,41034
(defcustom proof-count-undos-fn 1142,42390
(defconst proof-no-command 1154,42939
(defcustom proof-find-and-forget-fn 1159,43146
(defcustom proof-forget-id-command 1176,43860
(defcustom pg-topterm-goalhyplit-fn 1186,44218
(defcustom proof-kill-goal-command 1198,44753
(defcustom proof-undo-n-times-cmd 1212,45256
(defcustom proof-nested-goals-history-p 1226,45804
(defcustom proof-state-preserving-p 1235,46141
(defcustom proof-activate-scripting-hook 1245,46613
(defcustom proof-deactivate-scripting-hook 1264,47394
(defcustom proof-indent 1277,47759
(defcustom proof-indent-hang 1282,47866
(defcustom proof-indent-enclose-offset 1287,47992
(defcustom proof-indent-open-offset 1292,48134
(defcustom proof-indent-close-offset 1297,48271
(defcustom proof-indent-any-regexp 1302,48409
(defcustom proof-indent-inner-regexp 1307,48569
(defcustom proof-indent-enclose-regexp 1312,48723
(defcustom proof-indent-open-regexp 1317,48877
(defcustom proof-indent-close-regexp 1322,49029
(defcustom proof-script-font-lock-keywords 1328,49183
(defcustom proof-script-syntax-table-entries 1336,49500
(defcustom proof-script-span-context-menu-extensions 1354,49897
(defgroup proof-shell 1380,50657
(defcustom proof-prog-name 1390,50828
(defcustom proof-shell-auto-terminate-commands 1401,51248
(defcustom proof-shell-pre-sync-init-cmd 1410,51649
(defcustom proof-shell-init-cmd 1424,52207
(defcustom proof-shell-init-hook 1436,52736
(defcustom proof-shell-restart-cmd 1441,52875
(defcustom proof-shell-quit-cmd 1446,53030
(defcustom proof-shell-quit-timeout 1451,53197
(defcustom proof-shell-cd-cmd 1461,53647
(defcustom proof-shell-start-silent-cmd 1478,54318
(defcustom proof-shell-stop-silent-cmd 1487,54694
(defcustom proof-shell-silent-threshold 1496,55029
(defcustom  proof-shell-inform-file-processed-cmd 1504,55363
(defcustom  proof-shell-inform-file-retracted-cmd 1525,56291
(defcustom proof-auto-multiple-files 1553,57563
(defcustom proof-cannot-reopen-processed-files 1568,58284
(defcustom proof-shell-require-command-regexp 1582,58950
(defcustom proof-done-advancing-require-function 1593,59412
(defcustom proof-shell-quiet-errors 1599,59647
(defcustom proof-shell-prompt-pattern 1612,59981
(defcustom proof-shell-wakeup-char 1622,60402
(defcustom proof-shell-annotated-prompt-regexp 1628,60633
(defcustom proof-shell-abort-goal-regexp 1644,61269
(defcustom proof-shell-error-regexp 1649,61404
(defcustom proof-shell-truncate-before-error 1669,62204
(defcustom pg-next-error-regexp 1683,62743
(defcustom pg-next-error-filename-regexp 1698,63352
(defcustom pg-next-error-extract-filename 1722,64385
(defcustom proof-shell-interrupt-regexp 1729,64628
(defcustom proof-shell-proof-completed-regexp 1743,65223
(defcustom proof-shell-clear-response-regexp 1756,65731
(defcustom proof-shell-clear-goals-regexp 1763,66030
(defcustom proof-shell-start-goals-regexp 1770,66323
(defcustom proof-shell-end-goals-regexp 1778,66690
(defcustom proof-shell-eager-annotation-start 1784,66934
(defcustom proof-shell-eager-annotation-start-length 1807,67953
(defcustom proof-shell-eager-annotation-end 1818,68379
(defcustom proof-shell-assumption-regexp 1834,69054
(defcustom proof-shell-process-file 1844,69457
(defcustom proof-shell-retract-files-regexp 1866,70413
(defcustom proof-shell-compute-new-files-list 1875,70749
(defcustom pg-use-specials-for-fontify 1887,71297
(defcustom pg-special-char-regexp 1895,71645
(defcustom proof-shell-set-elisp-variable-regexp 1901,71790
(defcustom proof-shell-match-pgip-cmd 1934,73303
(defcustom proof-shell-issue-pgip-cmd 1943,73632
(defcustom proof-shell-query-dependencies-cmd 1952,73988
(defcustom proof-shell-theorem-dependency-list-regexp 1959,74248
(defcustom proof-shell-theorem-dependency-list-split 1975,74908
(defcustom proof-shell-show-dependency-cmd 1984,75331
(defcustom proof-shell-identifier-under-mouse-cmd 1991,75600
(defcustom proof-shell-trace-output-regexp 2014,76681
(defcustom proof-shell-thms-output-regexp 2028,77139
(defcustom proof-tokens-activate-command 2041,77522
(defcustom proof-tokens-deactivate-command 2048,77763
(defcustom proof-tokens-extra-modes 2055,78010
(defcustom proof-shell-unicode 2070,78517
(defcustom proof-shell-filename-escapes 2078,78837
(defcustom proof-shell-process-connection-type2095,79517
(defcustom proof-shell-strip-crs-from-input 2118,80563
(defcustom proof-shell-strip-crs-from-output 2130,81048
(defcustom proof-shell-insert-hook 2138,81416
(defcustom proof-shell-handle-delayed-output-hook2176,83276
(defcustom proof-shell-handle-error-or-interrupt-hook2182,83491
(defcustom proof-shell-pre-interrupt-hook2200,84244
(defcustom proof-shell-process-output-system-specific 2208,84515
(defcustom proof-state-change-hook 2227,85379
(defcustom proof-shell-syntax-table-entries 2237,85760
(defgroup proof-goals 2255,86132
(defcustom pg-subterm-first-special-char 2260,86253
(defcustom pg-subterm-anns-use-stack 2268,86565
(defcustom pg-goals-change-goal 2277,86864
(defcustom pbp-goal-command 2282,86980
(defcustom pbp-hyp-command 2287,87136
(defcustom pg-subterm-help-cmd 2292,87298
(defcustom pg-goals-error-regexp 2299,87534
(defcustom proof-shell-result-start 2304,87694
(defcustom proof-shell-result-end 2310,87928
(defcustom pg-subterm-start-char 2316,88141
(defcustom pg-subterm-sep-char 2330,88727
(defcustom pg-subterm-end-char 2336,88906
(defcustom pg-topterm-regexp 2342,89063
(defcustom proof-goals-font-lock-keywords 2357,89663
(defcustom proof-resp-font-lock-keywords 2365,89990
(defcustom pg-before-fontify-output-hook 2373,90319
(defcustom pg-after-fontify-output-hook 2381,90680
(defcustom proof-general-name 2393,90929
(defcustom proof-general-home-page2398,91086
(defcustom proof-unnamed-theorem-name2404,91246
(defcustom proof-universal-keys2410,91430

generic/proof-depends.el,824
(defvar proof-thm-names-of-files 23,625
(defvar proof-def-names-of-files 29,909
(defun proof-depends-module-name-for-buffer 38,1213
(defun proof-depends-module-of 48,1655
(defun proof-depends-names-in-same-file 56,1949
(defun proof-depends-process-dependencies 75,2569
(defun proof-dependency-in-span-context-menu 128,4318
(defun proof-dep-alldeps-menu 151,5221
(defun proof-dep-make-alldeps-menu 157,5448
(defun proof-dep-split-deps 175,5944
(defun proof-dep-make-submenu 196,6643
(defun proof-make-highlight-depts-menu 206,6996
(defun proof-goto-dependency 216,7300
(defun proof-show-dependency 222,7523
(defconst pg-dep-span-priority 229,7813
(defconst pg-ordinary-span-priority 230,7849
(defun proof-highlight-depcs 232,7891
(defun proof-highlight-depts 242,8321
(defun proof-dep-unhighlight 253,8795

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table16,544
(defun proof-easy-config-define-derived-modes 23,950
(defun proof-easy-config-check-setup 52,2133
(defmacro proof-easy-config 84,3468

generic/proof-indent.el,219
(defun proof-indent-indent 14,412
(defun proof-indent-offset 23,678
(defun proof-indent-inner-p 40,1278
(defun proof-indent-goto-prev 49,1585
(defun proof-indent-calculate 56,1918
(defun proof-indent-line 76,2640

generic/proof-maths-menu.el,83
(defun proof-maths-menu-set-global 30,959
(defun proof-maths-menu-enable 44,1415

generic/proof-menu.el,2100
(defvar proof-display-some-buffers-count 17,437
(defun proof-display-some-buffers 19,482
(defun proof-menu-define-keys 78,2684
(defun proof-menu-define-main 137,5513
(defvar proof-menu-favourites 146,5701
(defun proof-menu-define-specific 150,5823
(defun proof-assistant-menu-update 188,6841
(defvar proof-help-menu202,7274
(defvar proof-show-hide-menu210,7552
(defvar proof-buffer-menu219,7865
(defun proof-keep-response-history 278,9951
(defconst proof-quick-opts-menu286,10261
(defun proof-quick-opts-vars 437,16483
(defun proof-quick-opts-changed-from-defaults-p 462,17240
(defun proof-quick-opts-changed-from-saved-p 466,17345
(defun proof-quick-opts-save 477,17697
(defun proof-quick-opts-reset 482,17865
(defconst proof-config-menu494,18133
(defconst proof-advanced-menu501,18312
(defvar proof-menu 514,18747
(defun proof-main-menu 523,19031
(defun proof-aux-menu 534,19297
(defun proof-menu-define-favourites-menu 550,19644
(defun proof-def-favourite 570,20300
(defvar proof-make-favourite-cmd-history 593,21275
(defvar proof-make-favourite-menu-history 596,21360
(defun proof-save-favourites 599,21446
(defun proof-del-favourite 604,21594
(defun proof-read-favourite 621,22155
(defun proof-add-favourite 646,22958
(defvar proof-menu-settings 673,24009
(defun proof-menu-define-settings-menu 676,24083
(defun proof-menu-entry-name 696,24827
(defun proof-menu-entry-for-setting 708,25299
(defun proof-settings-vars 726,25789
(defun proof-settings-changed-from-defaults-p 731,25966
(defun proof-settings-changed-from-saved-p 735,26072
(defun proof-settings-save 739,26175
(defun proof-settings-reset 744,26342
(defun proof-defpacustom-fn 751,26587
(defmacro defpacustom 827,29478
(defun proof-assistant-invisible-command-ifposs 842,30305
(defun proof-maybe-askprefs 864,31280
(defun proof-assistant-settings-cmd 871,31484
(defvar proof-assistant-format-table 888,32144
(defun proof-assistant-format-bool 896,32513
(defun proof-assistant-format-int 899,32626
(defun proof-assistant-format-string 902,32718
(defun proof-assistant-format 905,32816

generic/proof-mmm.el,70
(defun proof-mmm-set-global 41,1517
(defun proof-mmm-enable 56,2058

generic/proof-script.el,5199
(defvar proof-element-counters 28,714
(deflocal proof-active-buffer-fake-minor-mode 34,854
(deflocal proof-script-buffer-file-name 37,980
(deflocal pg-script-portions 44,1390
(defun proof-next-element-count 54,1626
(defun proof-element-id 63,1961
(defun proof-next-element-id 67,2130
(deflocal proof-script-last-entity 81,2447
(defun proof-script-find-next-entity 88,2727
(deflocal proof-locked-span 164,5469
(deflocal proof-queue-span 171,5735
(defun proof-span-give-warning 183,6249
(defun proof-span-read-only 187,6363
(defun proof-strict-read-only 196,6795
(defsubst proof-set-locked-endpoints 234,8526
(defsubst proof-detach-queue 238,8670
(defsubst proof-detach-locked 242,8802
(defsubst proof-set-queue-start 246,8938
(defsubst proof-set-locked-end 250,9064
(defsubst proof-set-queue-end 263,9549
(defun proof-init-segmentation 274,9846
(defun proof-restart-buffers 307,11241
(defun proof-script-buffers-with-spans 329,12173
(defun proof-script-remove-all-spans-and-deactivate 339,12529
(defun proof-script-clear-queue-spans 343,12717
(defun proof-unprocessed-begin 362,13278
(defun proof-script-end 370,13532
(defun proof-queue-or-locked-end 379,13833
(defun proof-locked-end 394,14511
(defun proof-locked-region-full-p 411,14896
(defun proof-locked-region-empty-p 420,15168
(defun proof-only-whitespace-to-locked-region-p 424,15318
(defun proof-in-locked-region-p 437,15954
(defun proof-goto-end-of-locked 449,16217
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 466,16976
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 477,17457
(defun proof-end-of-locked-visible-p 491,18110
(defun proof-goto-end-of-queue-or-locked-if-not-visible 500,18561
(defvar pg-idioms 519,19211
(defvar pg-visibility-specs 522,19307
(defconst pg-default-invisibility-spec 527,19514
(defun pg-clear-script-portions 531,19654
(defun pg-add-script-element 538,19902
(defun pg-remove-script-element 541,19978
(defsubst pg-visname 549,20272
(defun pg-add-element 553,20417
(defun pg-open-invisible-span 587,22046
(defun pg-remove-element 598,22409
(defun pg-make-element-invisible 605,22679
(defun pg-make-element-visible 611,22923
(defun pg-toggle-element-visibility 615,23066
(defun pg-redisplay-for-gnuemacs 622,23353
(defun pg-show-all-portions 626,23499
(defun pg-show-all-proofs 644,24170
(defun pg-hide-all-proofs 649,24298
(defun pg-add-proof-element 654,24429
(defun pg-span-name 668,25049
(defvar pg-span-context-menu-keymap689,25756
(defun pg-set-span-helphighlights 698,26010
(defun proof-complete-buffer-atomic 724,26877
(defun proof-register-possibly-new-processed-file 765,28792
(defun proof-inform-prover-file-retracted 816,30920
(defun proof-auto-retract-dependencies 835,31706
(defun proof-unregister-buffer-file-name 889,34246
(defun proof-protected-process-or-retract 935,36069
(defun proof-deactivate-scripting-auto 962,37239
(defun proof-deactivate-scripting 971,37597
(defun proof-activate-scripting 1104,42870
(defun proof-toggle-active-scripting 1224,48248
(defun proof-done-advancing 1265,49609
(defun proof-done-advancing-comment 1360,53257
(defun proof-done-advancing-save 1379,53999
(defun proof-make-goalsave 1472,57614
(defun proof-get-name-from-goal 1487,58357
(defun proof-done-advancing-autosave 1506,59383
(defun proof-done-advancing-other 1571,61929
(defun proof-segment-up-to-parser 1599,62888
(defun proof-script-generic-parse-find-comment-end 1663,64958
(defun proof-script-generic-parse-cmdend 1672,65374
(defun proof-script-generic-parse-cmdstart 1697,66269
(defun proof-script-generic-parse-sexp 1760,68977
(defun proof-cmdstart-add-segment-for-cmd 1784,69913
(defun proof-segment-up-to-cmdstart 1836,72112
(defun proof-segment-up-to-cmdend 1897,74472
(defun proof-semis-to-vanillas 1969,77137
(defun proof-script-new-command-advance 2008,78463
(defun proof-script-next-command-advance 2050,80204
(defun proof-assert-until-point-interactive 2062,80645
(defun proof-assert-until-point 2088,81767
(defun proof-assert-next-command2141,84199
(defun proof-retract-before-change 2189,86437
(defun proof-goto-point 2196,86656
(defun proof-insert-pbp-command 2214,87197
(defun proof-insert-sendback-command 2228,87666
(defun proof-done-retracting 2254,88556
(defun proof-setup-retract-action 2290,90042
(defun proof-last-goal-or-goalsave 2300,90525
(defun proof-retract-target 2323,91365
(defun proof-retract-until-point-interactive 2408,95006
(defun proof-retract-until-point 2416,95391
(define-derived-mode proof-mode 2459,97140
(defun proof-script-set-visited-file-name 2492,98365
(defun proof-script-set-buffer-hooks 2516,99367
(defun proof-script-kill-buffer-fn 2524,99785
(defun proof-config-done-related 2556,101099
(defun proof-generic-goal-command-p 2624,103627
(defun proof-generic-state-preserving-p 2629,103839
(defun proof-generic-count-undos 2638,104356
(defun proof-generic-find-and-forget 2667,105386
(defconst proof-script-important-settings2718,107211
(defun proof-config-done 2733,107764
(defun proof-setup-parsing-mechanism 2802,110070
(defun proof-setup-imenu 2846,111923
(defun proof-setup-func-menu 2863,112528

generic/proof-shell.el,3159
(defvar proof-marker 28,656
(defvar proof-action-list 31,753
(defvar proof-shell-silent 39,929
(defvar proof-shell-last-prompt 46,1220
(defvar proof-shell-last-output-kind 50,1391
(defvar proof-shell-delayed-output 71,2213
(defvar proof-shell-delayed-output-kind 74,2334
(defcustom proof-shell-active-scripting-indicator83,2537
(defun proof-shell-ready-prover 133,3928
(defun proof-shell-live-buffer 147,4468
(defun proof-shell-available-p 154,4703
(defun proof-grab-lock 160,4926
(defun proof-release-lock 172,5485
(defcustom proof-shell-fiddle-frames 187,5884
(defun proof-shell-set-text-representation 193,6107
(defun proof-shell-start 204,6569
(defvar proof-shell-kill-function-hooks 405,13773
(defun proof-shell-kill-function 408,13871
(defun proof-shell-clear-state 497,17674
(defun proof-shell-exit 512,18117
(defun proof-shell-bail-out 524,18562
(defun proof-shell-restart 533,19039
(defvar proof-shell-no-response-display 575,20423
(defvar proof-shell-urgent-message-marker 578,20527
(defvar proof-shell-urgent-message-scanner 581,20648
(defun proof-shell-handle-output 585,20775
(defun proof-shell-handle-delayed-output 620,22094
(defvar proof-shell-no-error-display 648,23137
(defun proof-shell-handle-error 654,23341
(defun proof-shell-handle-interrupt 670,24074
(defun proof-shell-error-or-interrupt-action 684,24687
(defun proof-goals-pos 709,25832
(defun proof-pbp-focus-on-first-goal 714,26037
(defsubst proof-shell-string-match-safe 726,26464
(defun proof-shell-process-output 731,26632
(defun proof-shell-insert 844,31349
(defun proof-shell-command-queue-item 897,33450
(defun proof-shell-set-silent 902,33607
(defun proof-shell-start-silent-item 908,33826
(defun proof-shell-clear-silent 914,34018
(defun proof-shell-stop-silent-item 920,34240
(defun proof-shell-should-be-silent 927,34512
(defun proof-append-alist 940,35068
(defun proof-start-queue 999,37305
(defun proof-extend-queue 1010,37654
(defun proof-shell-exec-loop 1019,38033
(defun proof-shell-insert-loopback-cmd 1084,40621
(defun proof-shell-message 1112,41947
(defun proof-shell-process-urgent-message 1118,42163
(defun proof-shell-strip-eager-annotations 1248,47300
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1259,47636
(defun proof-shell-minibuffer-urgent-interactive-input 1261,47706
(defun proof-shell-process-urgent-messages 1271,48065
(defun proof-shell-filter 1345,51169
(defun proof-shell-filter-process-output 1501,57533
(defvar pg-last-tracing-output-time 1554,59587
(defconst pg-slow-mode-duration 1557,59693
(defconst pg-fast-tracing-mode-threshold 1560,59775
(defvar pg-tracing-cleanup-timer 1563,59903
(defun pg-tracing-tight-loop 1565,59942
(defun pg-finish-tracing-display 1608,61660
(defun proof-shell-wait 1630,62030
(defun proof-done-invisible 1649,62939
(defun proof-shell-invisible-command 1655,63111
(defun proof-shell-invisible-cmd-get-result 1689,64376
(defun proof-shell-invisible-command-invisible-result 1707,65072
(define-derived-mode proof-shell-mode 1726,65502
(defconst proof-shell-important-settings1781,67673
(defun proof-shell-config-done 1787,67788

generic/proof-site.el,504
(defconst proof-assistant-table-default22,727
(defconst proof-general-short-version 60,2143
(defconst proof-general-version-year 66,2331
(defgroup proof-general 73,2484
(defgroup proof-general-internals 78,2592
(defun proof-home-directory-fn 91,2980
(defcustom proof-home-directory102,3351
(defcustom proof-images-directory111,3718
(defcustom proof-info-directory117,3920
(defcustom proof-assistant-table145,5107
(defcustom proof-assistants 180,6223
(defun proof-ready-for-assistant 208,7368

generic/proof-splash.el,764
(defcustom proof-splash-enable 17,320
(defcustom proof-splash-time 22,472
(defcustom proof-splash-contents30,757
(defconst proof-splash-startup-msg 70,2102
(defconst proof-splash-welcome 79,2481
(defsubst proof-emacs-imagep 86,2656
(defun proof-get-image 91,2781
(defvar proof-splash-timeout-conf 116,3741
(defun proof-splash-centre-spaces 119,3854
(defun proof-splash-remove-screen 144,4940
(defun proof-splash-remove-buffer 161,5596
(defvar proof-splash-seen 177,6260
(defun proof-splash-display-screen 181,6377
(defun proof-splash-message 263,9713
(defun proof-splash-timeout-waiter 276,10157
(defvar proof-splash-old-frame-title-format 289,10715
(defun proof-splash-set-frame-titles 291,10765
(defun proof-splash-unset-frame-titles 300,11081

generic/proof-syntax.el,981
(defun proof-ids-to-regexp 15,436
(defun proof-anchor-regexp 19,605
(defconst proof-no-regexp23,707
(defun proof-regexp-alt 28,800
(defun proof-regexp-region 37,1086
(defun proof-re-search-forward-region 46,1509
(defun proof-search-forward 59,2004
(defun proof-replace-regexp-in-string 65,2256
(defun proof-re-search-forward 71,2510
(defun proof-re-search-backward 77,2771
(defun proof-string-match 83,3035
(defun proof-string-match-safe 89,3267
(defun proof-stringfn-match 93,3472
(defun proof-looking-at 100,3732
(defun proof-looking-at-safe 106,3922
(defun proof-looking-at-syntactic-context 110,4062
(defsubst proof-replace-string 122,4425
(defsubst proof-replace-regexp 127,4629
(defsubst proof-replace-regexp-nocasefold 132,4838
(defvar proof-id 140,5120
(defun proof-ids 146,5340
(defun proof-zap-commas 159,5896
(defun proof-format 175,6392
(defun proof-format-filename 194,7031
(defun proof-insert 241,8431
(defun proof-splice-separator 278,9447

generic/proof-toolbar.el,2290
(defun proof-toolbar-function 35,839
(defun proof-toolbar-icon 38,936
(defun proof-toolbar-enabler 41,1037
(defun proof-toolbar-make-icon 48,1190
(defun proof-toolbar-make-toolbar-items 57,1498
(defvar proof-toolbar-map 82,2304
(defun proof-toolbar-available-p 85,2403
(defun proof-toolbar-setup 94,2679
(defalias 'proof-toolbar-enable proof-toolbar-enable
112,3470
(defalias 'proof-toolbar-undo proof-toolbar-undo
142,4450
(defun proof-toolbar-undo-enable-p 144,4518
(defalias 'proof-toolbar-delete proof-toolbar-delete
151,4676
(defun proof-toolbar-delete-enable-p 153,4757
(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
161,4944
(defalias 'proof-toolbar-next proof-toolbar-next
165,5016
(defun proof-toolbar-next-enable-p 167,5087
(defalias 'proof-toolbar-goto proof-toolbar-goto
173,5203
(defun proof-toolbar-goto-enable-p 175,5253
(defalias 'proof-toolbar-retract proof-toolbar-retract
180,5338
(defun proof-toolbar-retract-enable-p 182,5395
(defalias 'proof-toolbar-use proof-toolbar-use
188,5514
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
189,5566
(defalias 'proof-toolbar-restart proof-toolbar-restart
193,5647
(defalias 'proof-toolbar-goal proof-toolbar-goal
197,5712
(defalias 'proof-toolbar-qed proof-toolbar-qed
201,5770
(defun proof-toolbar-qed-enable-p 203,5819
(defalias 'proof-toolbar-state proof-toolbar-state
211,5981
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
212,6024
(defalias 'proof-toolbar-context proof-toolbar-context
216,6103
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
217,6149
(defalias 'proof-toolbar-info proof-toolbar-info
221,6227
(defalias 'proof-toolbar-command proof-toolbar-command
225,6283
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
226,6339
(defun proof-toolbar-help 230,6418
(defalias 'proof-toolbar-find proof-toolbar-find
236,6499
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
237,6551
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
241,6649
(defun proof-toolbar-visibility-enable-p 243,6709
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
248,6823
(defun proof-toolbar-interrupt-enable-p 249,6884
(defun proof-toolbar-scripting-menu 257,7037

generic/proof-unicode-tokens.el,496
(defvar proof-unicode-tokens-initialised 28,761
(defun proof-unicode-tokens-init 31,868
(defun proof-unicode-tokens-configure 45,1370
(defun proof-unicode-tokens-enable 58,1834
(defun proof-unicode-tokens-mode-if-enabled 72,2521
(defun proof-unicode-tokens-set-global 78,2720
(defun proof-unicode-tokens-reconfigure 96,3360
(defun proof-unicode-tokens-configure-prover 122,4248
(defun proof-unicode-tokens-activate-prover 127,4429
(defun proof-unicode-tokens-deactivate-prover 134,4675

generic/proof-utils.el,1873
(defmacro deflocal 62,1812
(defmacro proof-with-current-buffer-if-exists 69,2050
(deflocal proof-buffer-type 75,2260
(defmacro proof-with-script-buffer 81,2540
(defmacro proof-map-buffers 92,2927
(defmacro proof-sym 97,3112
(defsubst proof-try-require 102,3273
(defun proof-save-some-buffers 115,3604
(defmacro proof-ass-sym 164,5205
(defmacro proof-ass-symv 170,5464
(defmacro proof-ass 176,5722
(defun proof-defpgcustom-fn 182,5974
(defun undefpgcustom 203,6845
(defmacro defpgcustom 209,7069
(defun proof-defpgdefault-fn 220,7487
(defmacro defpgdefault 234,7945
(defmacro defpgfun 245,8307
(defmacro proof-eval-when-ready-for-assistant 255,8572
(defun proof-file-truename 268,8967
(defun proof-file-to-buffer 272,9150
(defun proof-files-to-buffers 283,9479
(defun proof-buffers-in-mode 290,9762
(defun pg-save-from-death 304,10212
(defun proof-define-keys 323,10829
(defun pg-remove-specials 334,11121
(defun pg-remove-specials-in-string 344,11459
(defun proof-warn-if-unset 355,11687
(defun proof-get-window-for-buffer 360,11905
(defun proof-display-and-keep-buffer 411,14213
(defun proof-clean-buffer 452,16053
(defun proof-message 467,16674
(defun proof-warning 472,16887
(defun pg-internal-warning 478,17169
(defun proof-debug 486,17488
(defun proof-switch-to-buffer 495,17838
(defun proof-resize-window-tofit 517,18964
(defun proof-submit-bug-report 611,23139
(defun proof-deftoggle-fn 646,24496
(defmacro proof-deftoggle 661,25149
(defun proof-defintset-fn 668,25523
(defmacro proof-defintset 684,26227
(defun proof-defstringset-fn 691,26604
(defmacro proof-defstringset 704,27230
(defun proof-escape-keymap-doc 717,27686
(defmacro proof-defshortcut 721,27819
(defmacro proof-definvisible 736,28417
(defun pg-custom-save-vars 764,29394
(defun pg-custom-reset-vars 782,30117
(defun proof-locate-executable 795,30454

lib/bufhist.el,1099
(defun bufhist-ring-update 32,1227
(defgroup bufhist 41,1549
(defcustom bufhist-ring-size 45,1630
(defvar bufhist-ring 50,1741
(defvar bufhist-ring-pos 53,1815
(defvar bufhist-lastswitch-modified-tick 56,1894
(defvar bufhist-read-only-history 59,2000
(defvar bufhist-saved-mode-line-format 62,2071
(defun bufhist-mode-line-format-entry 65,2172
(defun bufhist-get-buffer-contents 97,3448
(defun bufhist-restore-buffer-contents 109,3932
(defun bufhist-checkpoint 117,4219
(defun bufhist-erase-buffer 125,4588
(defun bufhist-checkpoint-and-erase 135,4933
(defun bufhist-switch-to-index 141,5119
(defun bufhist-first 180,6723
(defun bufhist-last 185,6882
(defun bufhist-prev 190,7028
(defun bufhist-next 198,7251
(defun bufhist-delete 203,7391
(defun bufhist-clear 215,7934
(defun bufhist-init 230,8330
(defun bufhist-exit 255,9267
(defun bufhist-set-readwrite 265,9531
(defun bufhist-before-change-function 280,10151
(defun bufhist-make-buttons 292,10567
(defconst bufhist-minor-mode-map310,11006
(define-minor-mode bufhist-mode322,11468
(defun bufhist-toggle-fn 342,12253

lib/holes.el,2447
(defvar holes-doc 38,1074
(defvar holes-default-hole 133,4672
(defvar holes-active-hole 137,4841
(defcustom holes-empty-hole-string 144,5050
(defcustom holes-empty-hole-regexp 147,5161
(defcustom holes-search-limit 154,5452
(defface active-hole-face166,5828
(defface inactive-hole-face175,6228
(defun holes-region-beginning-or-nil 187,6655
(defun holes-region-end-or-nil 191,6750
(defun holes-copy-active-region 195,6833
(defun holes-is-hole-p 201,7017
(defun holes-hole-start-position 206,7121
(defun holes-hole-end-position 212,7307
(defun holes-hole-buffer 219,7491
(defun holes-hole-at 226,7666
(defun holes-active-hole-exist-p 233,7841
(defun holes-active-hole-start-position 243,8099
(defun holes-active-hole-end-position 253,8471
(defun holes-active-hole-buffer 264,8840
(defun holes-goto-active-hole 275,9146
(defun holes-highlight-hole-as-active 287,9414
(defun holes-highlight-hole 297,9726
(defun holes-disable-active-hole 308,10018
(defun holes-set-active-hole 326,10561
(defun holes-is-in-hole-p 339,10907
(defun holes-make-hole 346,11050
(defun holes-make-hole-at 372,11796
(defun holes-clear-hole 392,12272
(defun holes-clear-hole-at 404,12561
(defun holes-map-holes 413,12820
(defun holes-mapcar-holes 421,13003
(defun holes-clear-all-buffer-holes 427,13175
(defun holes-next 438,13475
(defun holes-next-after-active-hole 445,13726
(defun holes-set-active-hole-next 453,13945
(defun holes-replace-segment 475,14498
(defun holes-replace 485,14852
(defun holes-replace-active-hole 516,16047
(defun holes-replace-update-active-hole 525,16343
(defun holes-delete-update-active-hole 546,17016
(defun holes-set-make-active-hole 555,17246
(defun holes-mouse-replace-active-hole 602,18971
(defun holes-destroy-hole 622,19481
(defun holes-hole-at-event 639,19892
(defun holes-mouse-destroy-hole 644,20005
(defun holes-mouse-forget-hole 654,20245
(defun holes-mouse-set-make-active-hole 670,20555
(defun holes-mouse-set-active-hole 692,21092
(defun holes-set-point-next-hole-destroy 704,21356
(defvar hole-map720,21806
(defvar holes-mode-map730,22189
(defun holes-replace-string-by-holes-backward 767,23664
(defun holes-skeleton-end-hook 785,24365
(defconst holes-jump-doc 794,24803
(defun holes-replace-string-by-holes-backward-jump 801,25010
(defun holes-abbrev-complete 818,25692
(defun holes-insert-and-expand 827,26013
(defvar holes-mode 838,26445
(defun holes-mode 844,26641

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,828
(defun local-vars-list-insert-empty-zone 44,1391
(defun local-vars-list-find 82,2099
(defun local-vars-list-goto-var 101,2874
(defun local-vars-list-get-current 127,3924
(defun local-vars-list-set-current 148,4774
(defun local-vars-list-get 171,5491
(defun local-vars-list-get-safe 188,6023
(defun local-vars-list-set 193,6217

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 53,2237
(defvar maths-menu-tokenise-insert 56,2346
(defun maths-menu-build-menu 59,2485
(defvar maths-menu-menu76,3095
(defvar maths-menu-mode-map336,12653
(define-minor-mode maths-menu-mode344,12872

lib/pg-dev.el,75
(defconst pg-dev-lisp-font-lock-keywords36,1103
(defun unload-pg 70,2040

lib/pg-fontsets.el,176
(defcustom pg-fontsets-default-fontset 28,782
(defun pg-fontsets-make-fontsetsizes 33,928
(defconst pg-fontsets-base-fonts 52,1692
(defun pg-fontsets-make-fontsets 57,1797

lib/proof-compat.el,445
(defvar proof-running-on-win32 31,978
(defun pg-custom-undeclare-variable 51,1756
(defmacro save-selected-frame 97,2922
(defun proof-buffer-syntactic-context-emulate 123,3883
(defvar read-shell-command-map151,5093
(defun read-shell-command 169,5781
(defun frames-of-buffer 179,6209
(defmacro with-selected-window 223,7622
(defun process-live-p 255,8641
(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
266,8913

lib/span.el,1353
(defalias 'span-start span-start
22,612
(defalias 'span-end span-end
23,650
(defalias 'span-set-property span-set-property
24,684
(defalias 'span-property span-property
25,727
(defalias 'span-make span-make
26,766
(defalias 'span-detach span-detach
27,802
(defalias 'span-set-endpoints span-set-endpoints
28,842
(defalias 'span-buffer span-buffer
29,887
(defun span-read-only-hook 31,928
(defun span-read-only 36,1118
(defun span-read-write 43,1425
(defun span-give-warning 48,1592
(defun span-write-warning 53,1735
(defun span-lt 65,2319
(defun spans-at-point-prop 70,2460
(defun spans-at-region-prop 76,2625
(defun span-at 85,2937
(defsubst span-delete 91,3153
(defsubst span-mapcar-spans 98,3375
(defun span-at-before 103,3634
(defun prev-span 120,4360
(defun next-span 126,4511
(defsubst span-live-p 133,4723
(defun span-raise 139,4889
(defalias 'span-object span-object
143,5019
(defun span-string 145,5060
(defun set-span-properties 150,5198
(defun span-find-span 160,5445
(defsubst span-at-event 167,5751
(defun make-detached-span 171,5872
(defun fold-spans 176,5968
(defsubst span-detached-p 190,6501
(defsubst set-span-face 194,6617
(defun set-span-keymap 198,6715
(defsubst span-delete-spans 207,6918
(defsubst span-property-safe 211,7082
(defsubst span-set-start 215,7221
(defsubst span-set-end 219,7353

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3035
(defun texi-docstring-magic-splice-sep 93,3200
(defconst texi-docstring-magic-munge-table103,3505
(defun texi-docstring-magic-untabify 193,7272
(defun texi-docstring-magic-munge-docstring 203,7587
(defun texi-docstring-magic-texi 242,8874
(defun texi-docstring-magic-format-default 255,9314
(defun texi-docstring-magic-texi-for 271,9949
(defconst texi-docstring-magic-comment329,11909
(defun texi-docstring-magic 335,12063
(defun texi-docstring-magic-face-at-point 369,13143
(defun texi-docstring-magic-insert-magic 384,13666

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,349
(defun unicode-chars-list-chars 5050,245961

lib/unicode-tokens.el,3219
(defvar unicode-tokens-token-symbol-map 46,1554
(defvar unicode-tokens-token-format 59,1983
(defvar unicode-tokens-token-variant-format-regexp 65,2232
(defvar unicode-tokens-fontsymb-properties 78,2709
(defvar unicode-tokens-shortcut-alist 83,2943
(defvar unicode-tokens-control-region-format-regexp 94,3209
(defvar unicode-tokens-control-char-format-regexp 95,3266
(defvar unicode-tokens-control-regions 96,3321
(defvar unicode-tokens-control-characters 97,3365
(defvar unicode-tokens-control-char-format 98,3412
(defconst unicode-tokens-configuration-variables104,3501
(defvar unicode-tokens-token-list 120,3834
(defvar unicode-tokens-hash-table 123,3954
(defvar unicode-tokens-token-match-regexp 126,4070
(defvar unicode-tokens-uchar-hash-table 129,4182
(defvar unicode-tokens-uchar-regexp 133,4369
(defgroup unicode-tokens-faces 143,4560
(defface unicode-tokens-script-font-face147,4656
(defface unicode-tokens-fraktur-font-face158,4954
(defface unicode-tokens-serif-font-face169,5279
(defface unicode-tokens-highlight-face180,5572
(defconst unicode-tokens-font-lock-extra-managed-props 189,5934
(defun unicode-tokens-font-lock-keywords 197,6106
(defun unicode-tokens-usable-composition 237,7766
(defun unicode-tokens-help-echo 248,8042
(defvar unicode-tokens-show-symbols 252,8205
(defun unicode-tokens-font-lock-compose-symbol 255,8319
(defun unicode-tokens-show-symbols 272,9035
(defun unicode-tokens-symbs-to-props 280,9336
(defvar unicode-tokens-show-controls 298,9857
(defun unicode-tokens-show-controls 301,9948
(defun unicode-tokens-control-char 314,10524
(defun unicode-tokens-control-region 319,10766
(defun unicode-tokens-control-font-lock-keywords 325,11095
(defvar unicode-tokens-use-shortcuts 336,11425
(defun unicode-tokens-use-shortcuts 339,11528
(defun unicode-tokens-map-ordering 357,12125
(defun unicode-tokens-quail-define-rules 361,12275
(defun unicode-tokens-insert-token 384,12954
(defun unicode-tokens-annotate-region 393,13259
(defun unicode-tokens-insert-control 416,14027
(defun unicode-tokens-insert-uchar-as-token 425,14389
(defun unicode-tokens-delete-token-at-point 432,14619
(defun unicode-tokens-prev-token 439,14914
(defun unicode-tokens-rotate-token-forward 447,15179
(defun unicode-tokens-rotate-token-backward 474,16071
(defun unicode-tokens-copy-token 479,16273
(define-button-type 'unicode-tokens-listunicode-tokens-list
485,16448
(defun unicode-tokens-list-tokens 491,16653
(defun unicode-tokens-copy 514,17385
(defun unicode-tokens-paste 541,18536
(defvar unicode-tokens-highlight-unicode 556,19003
(defconst unicode-tokens-unicode-highlight-patterns559,19095
(defun unicode-tokens-highlight-unicode 563,19264
(defun unicode-tokens-initialise 579,19709
(defvar unicode-tokens-mode-map 587,19959
(define-minor-mode unicode-tokens-mode590,20056
(define-key unicode-tokens-mode-map 661,22479
(define-key unicode-tokens-mode-map 663,22571
(define-key unicode-tokens-mode-map 665,22662
(define-key unicode-tokens-mode-map 667,22769
(define-key unicode-tokens-mode-map 669,22879
(define-key unicode-tokens-mode-map 671,22988
(define-key unicode-tokens-mode-map 673,23095
(defun unicode-tokens-define-menu 681,23224

mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2676
(defun mmm-autoload-class 89,3439
(defvar mmm-changed-buffers-list 129,5006
(defun mmm-major-mode-change 132,5113
(defun mmm-check-changed-buffers 145,5634
(defun mmm-mode-on-maybe 155,6007
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6425
(defun mmm-add-find-file-hook 168,6485

mmm/mmm-class.el,416
(defun mmm-get-class-spec 42,1296
(defun mmm-get-class-parameter 59,2009
(defun mmm-set-class-parameter 63,2175
(defun* mmm-apply-class75,2539
(defun* mmm-apply-classes90,3177
(defun* mmm-apply-all 110,3943
(defun* mmm-ify124,4390
(defun* mmm-match-region206,7473
(defun mmm-match->point 267,10162
(defun mmm-match-and-verify 281,10684
(defun mmm-get-form 307,11742
(defun mmm-default-get-form 318,12238

mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1210
(defun mmm-ify-region 63,1934
(defun mmm-ify-by-regexp75,2362
(defun mmm-parse-buffer 97,3038
(defun mmm-parse-region 106,3374
(defun mmm-parse-block 115,3753
(defun mmm-get-block 132,4504
(defun mmm-reparse-current-region 146,4835
(defun mmm-clear-current-region 167,5509
(defun mmm-clear-regions 172,5673
(defun mmm-clear-all-regions 177,5819
(defun* mmm-end-current-region 185,5979
(defun mmm-narrow-to-submode-region 220,7402
(defun mmm-insert-region 239,8016
(defun mmm-insert-by-key 258,8878
(defun mmm-get-insertion-spec 342,12438
(defun mmm-insertion-help 369,13517
(defun mmm-display-insertion-key 379,13887
(defun mmm-get-all-insertion-keys 401,14709

mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1313
(defvar mmm-keywords-used49,1616
(defmacro mmm-regexp-opt 91,2662
(defvar mmm-evaporate-property110,3311
(defmacro mmm-set-keymap-default 128,4077
(defmacro mmm-event-key 137,4519
(defvar skeleton-positions 146,4738
(defun mmm-fixup-skeleton 147,4769
(defmacro mmm-make-temp-buffer 159,5206
(defvar mmm-font-lock-available-p 172,5602
(defmacro mmm-set-font-lock-defaults 179,5816

mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1117
(defvar mmm-cweb-section-regexp41,1164
(defvar mmm-cweb-c-part-tags44,1254
(defvar mmm-cweb-c-part-regexp47,1313
(defun mmm-cweb-in-limbo 50,1397
(defun mmm-cweb-verify-brief-c 57,1622

mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1236
(defvar mmm-mason-pseudo-perl-tags45,1377
(defvar mmm-mason-non-perl-tags48,1453
(defvar mmm-mason-perl-tags-regexp51,1554
(defvar mmm-mason-pseudo-perl-tags-regexp56,1749
(defvar mmm-mason-tag-names-regexp61,1966
(defun mmm-mason-verify-inline 66,2186
(defun mmm-mason-start-line 156,5090
(defun mmm-mason-end-line 161,5155
(defun mmm-mason-set-mode-line 168,5249

mmm/mmm-mode.el,1024
(defun mmm-mode 101,3867
(defun mmm-mode-on 140,5372
(defun mmm-mode-off 181,7132
(defvar mmm-mode-map 206,7865
(defvar mmm-mode-prefix-map 209,7940
(defvar mmm-mode-menu-map 212,8050
(defun mmm-define-key 215,8141
(define-key mmm-mode-prefix-map 239,8896
(define-key mmm-mode-prefix-map 246,9154
(define-key mmm-mode-map 249,9265
(define-key mmm-mode-menu-map 252,9367
(define-key mmm-mode-menu-map 254,9439
(define-key mmm-mode-menu-map 256,9498
(define-key mmm-mode-menu-map 258,9579
(define-key mmm-mode-menu-map 260,9660
(define-key mmm-mode-menu-map 262,9747
(define-key mmm-mode-menu-map 265,9841
(define-key mmm-mode-menu-map 267,9901
(define-key mmm-mode-menu-map 270,9992
(define-key mmm-mode-menu-map 272,10052
(define-key mmm-mode-menu-map 274,10159
(define-key mmm-mode-menu-map 276,10244
(define-key mmm-mode-menu-map 279,10330
(define-key mmm-mode-menu-map 281,10390
(define-key mmm-mode-menu-map 283,10503
(define-key mmm-mode-menu-map 285,10588
(define-key mmm-mode-map 288,10671

mmm/mmm-noweb.el,1291
(defvar mmm-noweb-code-mode 44,1352
(defvar mmm-noweb-quote-mode 50,1649
(defvar mmm-noweb-quote-string 54,1806
(defvar mmm-noweb-quote-number 58,1929
(defvar mmm-noweb-narrowing 62,2045
(defun mmm-noweb-chunk 68,2176
(defun mmm-noweb-quote 84,2876
(defun mmm-noweb-quote-name 89,3042
(defun mmm-noweb-chunk-name 95,3302
(defun mmm-noweb-regions 140,4748
(defun mmm-noweb-narrow-to-doc-chunk 166,5616
(defun mmm-noweb-fill-chunk 189,6386
(defun mmm-noweb-fill-paragraph-chunk 208,7070
(defun mmm-noweb-fill-named-chunk 222,7487
(defun mmm-noweb-auto-fill-doc-chunk 238,8064
(defun mmm-noweb-auto-fill-doc-mode 246,8283
(defun mmm-noweb-auto-fill-code-mode 251,8473
(defun mmm-noweb-complete-chunk 259,8685
(defvar mmm-noweb-chunk-history 292,9689
(defun mmm-noweb-goto-chunk 295,9767
(defun mmm-noweb-goto-next 307,10091
(defun mmm-noweb-goto-previous 319,10448
(defvar mmm-noweb-map 336,10852
(defvar mmm-noweb-prefix-map 337,10896
(define-key mmm-noweb-map 338,10947
(define-key mmm-noweb-prefix-map 347,11390
(defun mmm-noweb-bind-keys 352,11656
(defun mmm-syntax-region-list 368,12070
(defun mmm-syntax-other-regions 377,12426
(defun mmm-word-other-regions 389,12897
(defun mmm-space-other-regions 395,13066
(defun mmm-undo-syntax-other-regions 401,13237

mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1749
(defun mmm-overlays-at 59,1934
(defun mmm-included-p 72,2387
(defun mmm-overlays-containing 112,3876
(defun mmm-overlays-contained-in 125,4314
(defun mmm-overlays-overlapping 138,4754
(defun mmm-sort-overlays 149,5117
(defvar mmm-current-overlay 158,5387
(defvar mmm-previous-overlay 163,5602
(defvar mmm-current-submode 168,5790
(defvar mmm-previous-submode 173,5990
(defun mmm-update-current-submode 178,6163
(defun mmm-set-current-submode 199,6979
(defun mmm-submode-at 210,7471
(defun mmm-match-front 219,7746
(defun mmm-match-back 238,8507
(defun mmm-front-start 257,9252
(defun mmm-back-end 265,9556
(defun mmm-valid-submode-region 278,9903
(defun* mmm-make-region305,11059
(defun mmm-make-overlay 431,16430
(defun mmm-get-face 459,17563
(defun mmm-clear-overlays 470,17855
(defun mmm-update-mode-info 486,18322
(defun mmm-update-submode-region 571,22607
(defun mmm-add-hooks 588,23365
(defun mmm-remove-hooks 592,23500
(defun mmm-get-local-variables-list 598,23627
(defun mmm-get-locals 618,24547
(defun mmm-get-saved-local 631,25128
(defun mmm-set-local-variables 635,25293
(defun mmm-get-saved-local-variables 646,25734
(defun mmm-save-changed-local-variables 654,26051
(defun mmm-clear-local-variables 673,26909
(defun mmm-enable-font-lock 684,27188
(defun mmm-update-font-lock-buffer 692,27448
(defun mmm-refontify-maybe 705,27880
(defun mmm-submode-changes-in 720,28402
(defun mmm-regions-in 731,28850
(defun mmm-regions-alist 745,29420
(defun mmm-fontify-region 762,30066
(defun mmm-fontify-region-list 782,31097
(defun mmm-beginning-of-syntax 804,32013

mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1618
(defvar mmm-rpm-sh-end-tags53,1842
(defvar mmm-rpm-sh-start-regexp57,2016
(defvar mmm-rpm-sh-end-regexp61,2194

mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2615
(defun mmm-here-doc-get-mode 93,3100
(defun mmm-file-variables-verify 208,6818
(defun mmm-file-variables-find-back 232,7854

mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 41,1310
(defmacro mmm-save-all 60,1954
(defun mmm-format-string 73,2243
(defun mmm-format-matches 84,2695
(defmacro mmm-save-keyword 107,3488
(defmacro mmm-save-keywords 115,3815
(defun mmm-looking-back-at 128,4348
(defun mmm-make-marker 145,4916

mmm/mmm-vars.el,2667
(defgroup mmm 99,3073
(defvar mmm-c-derived-modes106,3183
(defvar mmm-save-local-variables 110,3302
(defvar mmm-buffer-saved-locals 336,10162
(defvar mmm-region-saved-locals-defaults 341,10362
(defvar mmm-region-saved-locals-for-dominant 347,10622
(defgroup mmm-faces 357,10999
(defcustom mmm-submode-decoration-level 363,11170
(defface mmm-init-submode-face 381,12042
(defface mmm-cleanup-submode-face 385,12182
(defface mmm-declaration-submode-face 389,12319
(defface mmm-comment-submode-face 393,12465
(defface mmm-output-submode-face 397,12618
(defface mmm-special-submode-face 401,12767
(defface mmm-code-submode-face 405,12931
(defface mmm-default-submode-face 409,13070
(defface mmm-delimiter-face 414,13278
(defcustom mmm-mode-string 421,13404
(defcustom mmm-submode-mode-line-format 426,13535
(defvar mmm-primary-mode-display-name 443,14190
(defvar mmm-buffer-mode-display-name 448,14404
(defun mmm-set-mode-line 454,14703
(defvar mmm-classes 478,15511
(defvar mmm-global-classes 484,15756
(defcustom mmm-mode-ext-classes-alist 491,15938
(defun mmm-add-mode-ext-class 510,16756
(defcustom mmm-major-mode-preferences519,17081
(defun mmm-add-to-major-mode-preferences 537,17879
(defun mmm-ensure-modename 553,18665
(defun mmm-modename->function 562,18975
(defcustom mmm-delimiter-mode 576,19438
(defcustom mmm-mode-prefix-key 586,19707
(defcustom mmm-command-modifiers 591,19834
(defcustom mmm-insert-modifiers 605,20467
(defcustom mmm-use-old-command-keys 620,21145
(defun mmm-use-old-command-keys 630,21609
(defcustom mmm-mode-hook 638,21808
(defun mmm-run-constructed-hook 658,22615
(defun mmm-run-major-hook 666,23001
(defun mmm-run-submode-hook 669,23078
(defvar mmm-class-hooks-run 672,23165
(defun mmm-run-class-hook 677,23337
(defvar mmm-primary-mode-entry-hook 682,23509
(defcustom mmm-major-mode-hook 697,24156
(defun mmm-run-major-mode-hook 711,24787
(defcustom mmm-global-mode 724,25328
(defcustom mmm-never-modes740,26023
(defvar mmm-set-file-name-for-modes 758,26323
(defvar mmm-mode 769,26682
(defvar mmm-primary-mode 777,26890
(defvar mmm-classes-alist 788,27256
(defun mmm-add-classes 943,35463
(defun mmm-add-group 948,35628
(defun mmm-add-to-group 958,36078
(defconst mmm-version 972,36575
(defun mmm-version 975,36640
(defvar mmm-temp-buffer-name 982,36783
(defvar mmm-interactive-history 988,36913
(defun mmm-add-to-history 994,37182
(defun mmm-clear-history 997,37265
(defvar mmm-mode-ext-classes 1005,37450
(defun mmm-get-mode-ext-classes 1010,37661
(defun mmm-clear-mode-ext-classes 1019,38037
(defun mmm-mode-ext-applies 1023,38162
(defun mmm-get-all-classes 1037,38646

doc/ProofGeneral.texi,5684
@node Top164,4911
@node Preface201,6018
@node News for Version 4.0News for Version 4.0
224,6607
@node Future248,7368
@node Credits279,8667
@node Introducing Proof GeneralIntroducing Proof General
385,12436
@node Installing Proof GeneralInstalling Proof General
440,14414
@node Quick start guideQuick start guide
454,14863
@node Features of Proof GeneralFeatures of Proof General
498,16984
@node Supported proof assistantsSupported proof assistants
587,20921
@node Prerequisites for this manualPrerequisites for this manual
636,22841
@node Organization of this manualOrganization of this manual
680,24460
@node Basic Script ManagementBasic Script Management
706,25288
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
725,25888
@node Proof scriptsProof scripts
979,35666
@node Script buffersScript buffers
1022,37786
@node Locked queue and editing regionsLocked queue and editing regions
1044,38363
@node Goal-save sequencesGoal-save sequences
1100,40510
@node Active scripting bufferActive scripting buffer
1137,41996
@node Summary of Proof General buffersSummary of Proof General buffers
1206,45416
@node Script editing commandsScript editing commands
1268,48090
@node Script processing commandsScript processing commands
1346,50949
@node Proof assistant commandsProof assistant commands
1474,56249
@node Toolbar commandsToolbar commands
1640,62028
@node Interrupting during trace outputInterrupting during trace output
1664,62957
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1703,64881
@node Goals buffer commandsGoals buffer commands
1717,65381
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1806,68945
@node Visibility of completed proofsVisibility of completed proofs
1838,70157
@node Switching between proof scriptsSwitching between proof scripts
1893,72080
@node View of processed files View of processed files 
1930,74052
@node Retracting across filesRetracting across files
1990,77103
@node Asserting across filesAsserting across files
2003,77734
@node Automatic multiple file handlingAutomatic multiple file handling
2016,78300
@node Escaping script managementEscaping script management
2041,79334
@node Editing featuresEditing features
2099,81537
@node Experimental featuresExperimental features
2163,84209
@node Support for other PackagesSupport for other Packages
2197,85473
@node Syntax highlightingSyntax highlighting
2229,86347
@node Unicode supportUnicode support
2258,87351
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2344,90462
@node Support for outline modeSupport for outline mode
2399,92506
@node Support for completionSupport for completion
2424,93635
@node Support for tagsSupport for tags
2481,95796
@node Customizing Proof GeneralCustomizing Proof General
2533,98124
@node Basic optionsBasic options
2573,99794
@node How to customizeHow to customize
2597,100552
@node Display customizationDisplay customization
2644,102519
@node User optionsUser options
2769,107757
@node Changing facesChanging faces
3011,116348
@node Tweaking configuration settingsTweaking configuration settings
3086,119017
@node Hints and TipsHints and Tips
3143,121543
@node Adding your own keybindingsAdding your own keybindings
3162,122144
@node Using file variablesUsing file variables
3219,124715
@node Using abbreviationsUsing abbreviations
3278,126901
@node LEGO Proof GeneralLEGO Proof General
3317,128316
@node LEGO specific commandsLEGO specific commands
3358,129685
@node LEGO tagsLEGO tags
3378,130140
@node LEGO customizationsLEGO customizations
3388,130387
@node Coq Proof GeneralCoq Proof General
3420,131306
@node Coq-specific commandsCoq-specific commands
3436,131715
@node Coq-specific variablesCoq-specific variables
3458,132222
@node Editing multiple proofsEditing multiple proofs
3480,132880
@node User-loaded tacticsUser-loaded tactics
3504,133988
@node Holes featureHoles feature
3568,136462
@node Isabelle Proof GeneralIsabelle Proof General
3595,137749
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3626,138918
@node Isabelle commandsIsabelle commands
3701,141967
@node Isabelle settingsIsabelle settings
3844,146120
@node Isabelle customizationsIsabelle customizations
3858,146702
@node HOL Proof GeneralHOL Proof General
3881,147189
@node Shell Proof GeneralShell Proof General
3923,149011
@node Obtaining and InstallingObtaining and Installing
3959,150470
@node Obtaining Proof GeneralObtaining Proof General
3975,150883
@node Installing Proof General from tarballInstalling Proof General from tarball
4006,152122
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4031,152954
@node Setting the names of binariesSetting the names of binaries
4046,153362
@node Notes for syssiesNotes for syssies
4074,154302
@node Bugs and EnhancementsBugs and Enhancements
4149,157338
@node References4170,158153
@node History of Proof GeneralHistory of Proof General
4210,159176
@node Old News for 3.0Old News for 3.0
4304,163341
@node Old News for 3.1Old News for 3.1
4374,167035
@node Old News for 3.2Old News for 3.2
4400,168207
@node Old News for 3.3Old News for 3.3
4461,171210
@node Old News for 3.4Old News for 3.4
4480,172107
@node Old News for 3.5Old News for 3.5
4502,173162
@node Old News for 3.6Old News for 3.6
4506,173219
@node Old News for 3.7Old News for 3.7
4511,173319
@node Function IndexFunction Index
4555,175217
@node Variable IndexVariable Index
4559,175293
@node Keystroke IndexKeystroke Index
4563,175373
@node Concept IndexConcept Index
4567,175439

doc/PG-adapting.texi,3772
@node Top155,4691
@node Introduction192,5800
@node Future233,7453
@node Credits269,9049
@node Beginning with a New ProverBeginning with a New Prover
279,9341
@node Overview of adding a new proverOverview of adding a new prover
320,11290
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
398,14598
@node Major modes used by Proof GeneralMajor modes used by Proof General
467,17989
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
500,19340
@node Settings for generic user-level commandsSettings for generic user-level commands
515,19886
@node Menu configurationMenu configuration
560,21620
@node Toolbar configurationToolbar configuration
584,22537
@node Proof Script SettingsProof Script Settings
642,24786
@node Recognizing commands and commentsRecognizing commands and comments
664,25366
@node Recognizing proofsRecognizing proofs
785,30887
@node Recognizing other elementsRecognizing other elements
894,35568
@node Configuring undo behaviourConfiguring undo behaviour
1020,41107
@node Nested proofsNested proofs
1157,46515
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1197,48141
@node Activate scripting hookActivate scripting hook
1220,49094
@node Automatic multiple filesAutomatic multiple files
1244,49964
@node Completions1266,50811
@node Proof Shell SettingsProof Shell Settings
1307,52300
@node Proof shell commandsProof shell commands
1338,53582
@node Script input to the shellScript input to the shell
1502,60626
@node Settings for matching various output from proof processSettings for matching various output from proof process
1567,63584
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1698,69368
@node Hooks and other settingsHooks and other settings
1913,79245
@node Goals Buffer SettingsGoals Buffer Settings
1994,82627
@node Splash Screen SettingsSplash Screen Settings
2071,85734
@node Global ConstantsGlobal Constants
2097,86492
@node Handling Multiple FilesHandling Multiple Files
2123,87333
@node Configuring Editing SyntaxConfiguring Editing Syntax
2275,95116
@node Configuring Font LockConfiguring Font Lock
2334,97237
@node Configuring TokensConfiguring Tokens
2406,100592
@node Writing More Lisp CodeWriting More Lisp Code
2444,102093
@node Default values for generic settingsDefault values for generic settings
2461,102738
@node Adding prover-specific configurationsAdding prover-specific configurations
2491,103821
@node Useful variablesUseful variables
2534,105103
@node Useful functions and macrosUseful functions and macros
2549,105602
@node Internals of Proof GeneralInternals of Proof General
2652,109557
@node Spans2680,110465
@node Proof General site configurationProof General site configuration
2692,110787
@node Configuration variable mechanismsConfiguration variable mechanisms
2772,113833
@node Global variablesGlobal variables
2893,119277
@node Proof script modeProof script mode
2963,121825
@node Proof shell modeProof shell mode
3222,133480
@node Debugging3629,149562
@node Plans and IdeasPlans and Ideas
3672,150438
@node Proof by pointing and similar featuresProof by pointing and similar features
3693,151160
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3731,152818
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3776,155043
@node Demonstration InstantiationsDemonstration Instantiations
3806,156074
@node demoisa-easy.el3822,156505
@node demoisa.el3885,158744
@node Function IndexFunction Index
4040,163729
@node Variable IndexVariable Index
4044,163805
@node Concept IndexConcept Index
4053,163984

generic/proof.el,0

generic/proof-autoloads.el,0

pgshell/pgshell.el,0

isar/isar-autotest.el,0

isar/interface-setup.el,0

hol98/hol98.el,0

demoisa/demoisa-easy.el,0

coq/coq-mmm.el,0

coq/coq-autotest.el,0

ccc/ccc.el,0

acl2/acl2.el,0