coq/coq-abbrev.el,468
(defun holes-show-doc 10,310
(defun coq-local-vars-list-show-doc 14,387
(defconst coq-tactics-menu 19,487
(defconst coq-tactics-abbrev-table 24,636
(defconst coq-tacticals-menu 27,724
(defconst coq-tacticals-abbrev-table 32,879
(defconst coq-commands-menu 36,972
(defconst coq-commands-abbrev-table 42,1189
(defconst coq-terms-menu 45,1279
(defconst coq-terms-abbrev-table 50,1419
(defpgdefault menu-entries 72,2197
(defpgdefault help-menu-entries153,5618

coq/coq-db.el,559
(defconst coq-syntax-db 22,519
(defvar coq-user-tactics-db58,1892
(defun coq-insert-from-db 68,2241
(defun coq-build-regexp-list-from-db 86,3022
(defun max-length-db 108,4075
(defun coq-build-menu-from-db-internal 120,4350
(defun coq-build-title-menu 155,5974
(defun coq-sort-menu-entries 164,6342
(defun coq-build-menu-from-db 167,6462
(defun coq-build-abbrev-table-from-db 187,7233
(defun filter-state-preserving 203,7787
(defun filter-state-changing 208,7941
(defface coq-solve-tactics-face 215,8162
(defconst coq-solve-tactics-face 223,8424

coq/coq.el,6050
(defcustom coq-translate-to-v8 34,982
(defcustom coq-compile-file-command 49,1471
(defcustom coq-default-undo-limit 59,1840
(defconst coq-shell-init-cmd 64,1968
(defvar coq-utf-safe 73,2184
(defcustom coq-prog-env 82,2600
(defconst coq-shell-restart-cmd 90,2852
(defvar coq-shell-prompt-pattern 97,3112
(defvar coq-shell-cd 105,3441
(defvar coq-shell-abort-goal-regexp 109,3596
(defvar coq-shell-proof-completed-regexp 112,3722
(defvar coq-goal-regexp115,3853
(defun coq-library-directory 124,4042
(defcustom coq-tags 131,4222
(defconst coq-interrupt-regexp 136,4372
(defcustom coq-www-home-page 141,4493
(defvar coq-outline-regexp151,4664
(defvar coq-outline-heading-end-regexp 158,4878
(defvar coq-shell-outline-regexp 160,4932
(defvar coq-shell-outline-heading-end-regexp 161,4982
(defconst coq-kill-goal-command 166,5092
(defconst coq-forget-id-command 167,5135
(defconst coq-back-n-command 168,5182
(defconst coq-state-preserving-tactics-regexp 172,5326
(defconst coq-state-changing-commands-regexp174,5427
(defconst coq-state-preserving-commands-regexp 176,5534
(defconst coq-commands-regexp 178,5646
(defvar coq-retractable-instruct-regexp 180,5724
(defvar coq-non-retractable-instruct-regexp 182,5815
(defvar coq-keywords-section186,5955
(defvar coq-section-regexp 189,6049
(defun coq-set-undo-limit 223,7149
(defconst coq-keywords-decl-defn-regexp234,7588
(defun coq-proof-mode-p 238,7738
(defun coq-is-comment-or-proverprocp 249,8148
(defun coq-is-goalsave-p 251,8252
(defun coq-is-module-equal-p 252,8327
(defun coq-is-def-p 255,8523
(defun coq-is-decl-defn-p 257,8631
(defun coq-state-preserving-command-p 262,8798
(defun coq-command-p 265,8932
(defun coq-state-preserving-tactic-p 268,9032
(defun coq-state-changing-tactic-p 273,9180
(defun coq-state-changing-command-p 280,9414
(defun coq-section-or-module-start-p 287,9760
(defun build-list-id-from-string 296,10001
(defun coq-last-prompt-info 309,10531
(defun coq-last-prompt-info-safe 321,11072
(defvar coq-last-but-one-statenum 331,11587
(defvar coq-last-but-one-proofnum 333,11654
(defvar coq-last-but-one-proofstack 335,11717
(defun coq-get-span-statenum 337,11759
(defun coq-get-span-proofnum 342,11874
(defun coq-get-span-proofstack 347,11989
(defun coq-set-span-statenum 352,12133
(defun coq-get-span-goalcmd 357,12264
(defun coq-set-span-goalcmd 362,12378
(defun coq-set-span-proofnum 367,12508
(defun coq-set-span-proofstack 372,12639
(defun proof-last-locked-span 377,12799
(defun coq-set-state-infos 392,13403
(defun count-not-intersection 432,15482
(defun  coq-find-and-forget-v81 463,16736
(defun coq-find-and-forget-v80 491,17868
(defun coq-find-and-forget 586,22567
(defvar coq-current-goal 599,23107
(defun coq-goal-hyp 602,23172
(defun coq-state-preserving-p 615,23605
(defconst notation-print-kinds-table 630,24111
(defun coq-PrintScope 634,24279
(defun coq-guess-or-ask-for-string 653,24835
(defun coq-ask-do 664,25220
(defun coq-SearchIsos 673,25608
(defun coq-SearchConstant 679,25841
(defun coq-SearchRewrite 683,25934
(defun coq-SearchAbout 687,26032
(defun coq-Print 691,26124
(defun coq-About 695,26246
(defun coq-LocateConstant 699,26363
(defun coq-LocateLibrary 705,26498
(defun coq-addquotes 711,26648
(defun coq-LocateNotation 713,26696
(defun coq-Pwd 720,26895
(defun coq-Inspect 726,27027
(defun coq-PrintSection(730,27127
(defun coq-Print-implicit 734,27221
(defun coq-Check 739,27373
(defun coq-Show 744,27483
(defun coq-Compile 758,27928
(defun coq-guess-command-line 772,28248
(defun coq-pre-shell-start 794,29096
(defun coq-mode-config 804,29545
(defun coq-hybrid-ouput-goals-response-p 920,33755
(defun coq-hybrid-ouput-goals-response 926,34013
(defun coq-shell-mode-config 948,34925
(defun coq-goals-mode-config 992,36996
(defun coq-response-config 999,37228
(defun coq-maybe-compile-buffer 1019,37934
(defun coq-ancestors-of 1056,39468
(defun coq-all-ancestors-of 1079,40435
(defconst coq-require-command-regexp 1091,40828
(defun coq-process-require-command 1096,41037
(defun coq-included-children 1101,41164
(defun coq-process-file 1122,42003
(defpacustom print-fully-explicit 1147,42918
(defpacustom print-implicit 1152,43067
(defpacustom print-coercions 1157,43234
(defpacustom print-match-wildcards 1162,43379
(defpacustom print-elim-types 1167,43560
(defpacustom printing-depth 1172,43727
(defpacustom time-commands 1177,43889
(defpacustom auto-compile-vos 1181,44000
(defun coq-preprocessing 1201,44670
(defun coq-fake-constant-markup 1216,45089
(defun coq-create-span-menu 1238,45896
(defconst module-kinds-table 1265,46698
(defconst modtype-kinds-table1269,46848
(defun coq-insert-section-or-module 1273,46977
(defconst reqkinds-kinds-table1296,47837
(defun coq-insert-requires 1301,47982
(defun coq-end-Section 1317,48488
(defun coq-insert-intros 1335,49072
(defun coq-insert-match 1347,49596
(defun coq-insert-tactic 1379,50774
(defun coq-insert-tactical 1385,51013
(defun coq-insert-command 1391,51262
(defun coq-insert-term 1397,51506
(define-key coq-keymap 1404,51704
(define-key coq-keymap 1405,51762
(define-key coq-keymap 1406,51819
(define-key coq-keymap 1407,51888
(define-key coq-keymap 1408,51944
(define-key coq-keymap 1409,51993
(define-key coq-keymap 1410,52051
(define-key coq-keymap 1412,52112
(define-key coq-keymap 1413,52171
(define-key coq-keymap 1415,52235
(define-key coq-keymap 1416,52295
(define-key coq-keymap 1418,52351
(define-key coq-keymap 1419,52401
(define-key coq-keymap 1420,52451
(define-key coq-keymap 1421,52501
(define-key coq-keymap 1422,52555
(define-key coq-keymap 1423,52614
(defvar last-coq-error-location 1433,52797
(defun coq-get-last-error-location 1442,53196
(defun coq-highlight-error 1475,54593
(defun coq-decide-highlight-error 1544,57278
(defun coq-highlight-error-hook 1549,57440
(defun first-word-of-buffer 1560,57833
(defun coq-show-first-goal 1569,58064
(defun is-not-split-vertic 1594,58953
(defun optim-resp-windows 1603,59392

coq/coq-indent.el,2241
(defconst coq-any-command-regexp11,262
(defconst coq-indent-inner-regexp14,353
(defconst coq-comment-start-regexp 24,814
(defconst coq-comment-end-regexp 25,857
(defconst coq-comment-start-or-end-regexp 26,898
(defconst coq-indent-open-regexp28,1007
(defconst coq-indent-close-regexp33,1181
(defconst coq-indent-closepar-regexp 38,1364
(defconst coq-indent-closematch-regexp 39,1409
(defconst coq-indent-openpar-regexp 40,1480
(defconst coq-indent-openmatch-regexp 41,1524
(defconst coq-indent-any-regexp42,1604
(defconst coq-indent-kw 47,1882
(defconst coq-indent-pattern-regexp 57,2337
(defun coq-indent-goal-command-p 61,2440
(defconst coq-end-command-regexp 82,3498
(defun coq-search-comment-delimiter-forward 87,3651
(defun coq-search-comment-delimiter-backward 96,3983
(defun coq-skip-until-one-comment-backward 103,4257
(defun coq-skip-until-one-comment-forward 115,4873
(defun coq-looking-at-comment 126,5391
(defun coq-find-comment-start 130,5532
(defun coq-find-comment-end 140,5965
(defun coq-looking-at-syntactic-context 152,6511
(defconst coq-end-command-or-comment-regexp158,6733
(defconst coq-end-command-or-comment-start-regexp161,6842
(defun coq-find-not-in-comment-backward 165,6960
(defun coq-find-not-in-comment-forward 184,7863
(defun coq-find-command-end-backward 203,8782
(defun coq-find-command-end-forward 211,9180
(defun coq-find-command-end 219,9559
(defun coq-parse-function 227,9944
(defun coq-find-current-start 236,10147
(defun coq-find-real-start 245,10438
(defun coq-command-at-point 252,10657
(defun only-spaces-on-line 259,10934
(defun find-reg 268,11208
(defun coq-find-no-syntactic-on-line 283,11757
(defun coq-back-to-indentation-prevline 296,12230
(defun coq-find-unclosed 338,14126
(defun coq-find-at-same-level-zero 368,15310
(defun coq-find-unopened 396,16394
(defun coq-find-last-unopened 443,17748
(defun coq-end-offset 456,18152
(defun coq-indent-command-offset 484,18971
(defun coq-indent-expr-offset 531,20797
(defun coq-indent-comment-offset 650,25143
(defun coq-indent-offset 682,26591
(defun coq-indent-calculate 699,27398
(defun proof-indent-line 703,27488
(defun coq-indent-line-not-comments 713,27864
(defun coq-indent-region 723,28263

coq/coq-local-vars.el,279
(defconst coq-local-vars-doc 17,306
(defun coq-insert-coq-prog-name 75,2832
(defun coq-read-directory 83,3185
(defun coq-extract-directories-from-args 98,3874
(defun coq-ask-prog-args 113,4384
(defun coq-ask-prog-name 133,5426
(defun coq-ask-insert-coq-prog-name 148,6067

coq/coq-syntax.el,33
(defcustom coq-prog-name 12,355

coq/x-symbol-coq.el,1746
(defvar x-symbol-coq-required-fonts 16,384
(defvar x-symbol-coq-name 24,785
(defvar x-symbol-coq-modeline-name 25,825
(defcustom x-symbol-coq-header-groups-alist 27,868
(defcustom x-symbol-coq-electric-ignore 34,1086
(defvar x-symbol-coq-required-fonts 41,1331
(defvar x-symbol-coq-extra-menu-items 44,1430
(defvar x-symbol-coq-token-grammar48,1518
(defun x-symbol-coq-default-token-list 64,2184
(defvar x-symbol-coq-user-table 76,2472
(defvar x-symbol-coq-generated-data 79,2578
(defvar x-symbol-coq-master-directory 87,2816
(defvar x-symbol-coq-image-searchpath 88,2864
(defvar x-symbol-coq-image-cached-dirs 89,2911
(defvar x-symbol-coq-image-file-truename-alist 90,2976
(defvar x-symbol-coq-image-keywords 91,3028
(defcustom x-symbol-coq-subscript-matcher 98,3256
(defcustom x-symbol-coq-font-lock-regexp 104,3488
(defcustom x-symbol-coq-font-lock-limit-regexp 109,3660
(defcustom x-symbol-coq-font-lock-contents-regexp 115,3848
(defcustom x-symbol-coq-single-char-regexp 122,4102
(defun x-symbol-coq-subscript-matcher 127,4250
(defun coq-match-subscript 162,5939
(defvar x-symbol-coq-font-lock-allowed-faces 169,6113
(defcustom x-symbol-coq-class-alist174,6338
(defcustom x-symbol-coq-class-face-alist 185,6716
(defvar x-symbol-coq-font-lock-keywords 195,7026
(defvar x-symbol-coq-font-lock-allowed-faces 197,7072
(defvar x-symbol-coq-case-insensitive 203,7296
(defvar x-symbol-coq-token-shape 204,7339
(defvar x-symbol-coq-input-token-ignore 205,7377
(defvar x-symbol-coq-token-list 206,7422
(defvar x-symbol-coq-symbol-table 208,7466
(defvar x-symbol-coq-xsymbol-table 312,9888
(defun x-symbol-coq-prepare-table 459,13756
(defvar x-symbol-coq-table468,14023
(defcustom x-symbol-coq-auto-style475,14184

demoisa/demoisa.el,390
(defcustom isabelledemo-prog-name 54,1809
(defcustom isabelledemo-web-page59,1931
(defun demoisa-config 70,2161
(defun demoisa-shell-config 90,2910
(define-derived-mode demoisa-mode 119,3994
(define-derived-mode demoisa-shell-mode 124,4117
(define-derived-mode demoisa-response-mode 129,4260
(define-derived-mode demoisa-goals-mode 133,4387
(defun demoisa-pre-shell-start 152,5169

isar/isabelle-system.el,1446
(defgroup isabelle 19,596
(defcustom isabelle-web-page23,724
(defcustom isa-isatool-command34,1019
(defvar isatool-not-found 61,1964
(defun isa-set-isatool-command 64,2077
(defun isa-shell-command-to-string 84,2938
(defun isa-getenv 90,3162
(defcustom isabelle-program-name 109,3819
(defvar isabelle-prog-name 135,4767
(defun isabelle-command-line 138,4894
(defun isabelle-choose-logic 162,5851
(defun isa-tool-list-logics 184,6823
(defun isa-view-doc 191,7061
(defun isa-tool-list-docs 199,7286
(defconst isabelle-verbatim-regexp 226,8319
(defun isabelle-verbatim 229,8460
(defcustom isabelle-refresh-logics 236,8616
(defcustom isabelle-logics-available 244,8943
(defcustom isabelle-chosen-logic 252,9243
(defconst isabelle-docs-menu 265,9711
(defun isabelle-logics-menu-calculate 275,10104
(defvar isabelle-time-to-refresh-logics 291,10613
(defun isabelle-logics-menu-refresh 294,10706
(defun isabelle-logics-menu-filter 311,11405
(defun isabelle-menu-bar-update-logics 317,11615
(defvar isabelle-logics-menu-entries 328,11971
(defvar isabelle-logics-menu 330,12043
(defun isabelle-load-isar-keywords 343,12661
(defpgdefault menu-entries364,13402
(defpgdefault help-menu-entries 367,13454
(defpgdefault x-symbol-language 375,13648
(defun isabelle-convert-idmarkup-to-subterm 398,14263
(defun isabelle-create-span-menu 422,15275
(defun isabelle-xml-sml-escapes 438,15720
(defun isabelle-process-pgip 441,15821

isar/isar.el,1243
(defcustom isar-keywords-name 28,580
(defpgdefault completion-table 45,1104
(defcustom isar-web-page47,1157
(defun isar-strip-terminators 61,1494
(defun isar-markup-ml 74,1871
(defun isar-mode-config-set-variables 79,2006
(defun isar-shell-mode-config-set-variables 144,5021
(defun isar-remove-file 242,9190
(defun isar-shell-compute-new-files-list 252,9553
(defun isar-activate-scripting 263,10019
(define-derived-mode isar-shell-mode 272,10189
(define-derived-mode isar-response-mode 277,10312
(define-derived-mode isar-goals-mode 282,10494
(define-derived-mode isar-mode 287,10669
(defpgdefault menu-entries341,12646
(defun isar-count-undos 371,13885
(defun isar-find-and-forget 398,15010
(defun isar-goal-command-p 439,16593
(defun isar-global-save-command-p 444,16765
(defvar isar-current-goal 465,17610
(defun isar-state-preserving-p 468,17676
(defvar isar-shell-current-line-width 493,18835
(defun isar-shell-adjust-line-width 499,19053
(defun isar-pre-shell-start 519,19938
(defun isar-preprocessing 531,20281
(defun isar-mode-config 554,21547
(defun isar-shell-mode-config 566,22117
(defun isar-response-mode-config 577,22487
(defun isar-goals-mode-config 586,22744
(defun isar-goalhyplit-test 597,23090

isar/isar-find-theorems.el,778
(defun isar-find-theorems-minibuffer 18,715
(defun isar-find-theorems-form 32,1334
(defvar isar-find-theorems-data 74,3134
(defvar isar-find-theorems-widget-number 88,3469
(defvar isar-find-theorems-widget-pattern 91,3567
(defvar isar-find-theorems-widget-intro 94,3659
(defvar isar-find-theorems-widget-elim 97,3745
(defvar isar-find-theorems-widget-dest 100,3829
(defvar isar-find-theorems-widget-name 103,3913
(defvar isar-find-theorems-widget-simp 106,4000
(defun isar-find-theorems-create-searchform111,4146
(defun isar-find-theorems-create-help 251,8761
(defun isar-find-theorems-submit-searchform294,10933
(defun isar-find-theorems-parse-criteria 372,13310
(defun isar-find-theorems-parse-number 465,16410
(defun isar-find-theorems-filter-empty 475,16687

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,487
(defconst isar-keywords-minor206,3647
(defconst isar-keywords-control262,4401
(defconst isar-keywords-diag282,4878
(defconst isar-keywords-theory-begin338,5837
(defconst isar-keywords-theory-switch341,5890
(defconst isar-keywords-theory-end344,5945
(defconst isar-keywords-theory-heading347,5993
(defconst isar-keywords-theory-decl353,6100
(defconst isar-keywords-theory-script412,7081
(defconst isar-keywords-theory-goal416,7158
(defconst isar-keywords-qed429,7375
(defconst isar-keywords-qed-block436,7461
(defconst isar-keywords-qed-global439,7508
(defconst isar-keywords-proof-heading442,7557
(defconst isar-keywords-proof-goal447,7640
(defconst isar-keywords-proof-block454,7739
(defconst isar-keywords-proof-open458,7801
(defconst isar-keywords-proof-close461,7847
(defconst isar-keywords-proof-chain464,7894
(defconst isar-keywords-proof-decl471,7997
(defconst isar-keywords-proof-asm480,8118
(defconst isar-keywords-proof-asm-goal487,8213
(defconst isar-keywords-proof-script490,8268

isar/isar-mmm.el,83
(defconst isar-start-latex-regexp 23,697
(defconst isar-start-sml-regexp 35,1130

isar/isar-syntax.el,3471
(defconst isar-script-syntax-table-entries18,433
(defconst isar-script-syntax-table-alist59,1469
(defun isar-init-syntax-table 68,1759
(defun isar-init-output-syntax-table 76,2006
(defconst isar-keyword-begin 92,2453
(defconst isar-keyword-end 93,2491
(defconst isar-keywords-theory-enclose95,2526
(defconst isar-keywords-theory100,2671
(defconst isar-keywords-save105,2816
(defconst isar-keywords-proof-enclose110,2945
(defconst isar-keywords-proof116,3127
(defconst isar-keywords-proof-context123,3332
(defconst isar-keywords-local-goal127,3446
(defconst isar-keywords-proper131,3558
(defconst isar-keywords-improper136,3691
(defconst isar-keywords-outline141,3837
(defconst isar-keywords-fume144,3902
(defconst isar-keywords-indent-open151,4120
(defconst isar-keywords-indent-close157,4304
(defconst isar-keywords-indent-enclose161,4409
(defun isar-regexp-simple-alt 170,4624
(defun isar-ids-to-regexp 190,5384
(defconst isar-ext-first 224,6790
(defconst isar-ext-rest 225,6857
(defconst isar-long-id-stuff 227,6929
(defconst isar-id 228,7003
(defconst isar-idx 229,7073
(defconst isar-string 231,7132
(defconst isar-any-command-regexp233,7192
(defconst isar-name-regexp237,7326
(defconst isar-improper-regexp243,7621
(defconst isar-save-command-regexp247,7769
(defconst isar-global-save-command-regexp250,7870
(defconst isar-goal-command-regexp253,7984
(defconst isar-local-goal-command-regexp256,8092
(defconst isar-comment-start 259,8205
(defconst isar-comment-end 260,8240
(defconst isar-comment-start-regexp 261,8273
(defconst isar-comment-end-regexp 262,8344
(defconst isar-string-start-regexp 264,8412
(defconst isar-string-end-regexp 265,8464
(defconst isar-antiq-regexp274,8717
(defconst isar-nesting-regexp281,8878
(defun isar-nesting 284,8976
(defun isar-match-nesting 296,9397
(defface isabelle-class-name-face308,9728
(defface isabelle-tfree-name-face318,10003
(defface isabelle-tvar-name-face328,10284
(defface isabelle-free-name-face338,10564
(defface isabelle-bound-name-face348,10840
(defface isabelle-var-name-face358,11119
(defconst isabelle-class-name-face 368,11398
(defconst isabelle-tfree-name-face 369,11460
(defconst isabelle-tvar-name-face 370,11522
(defconst isabelle-free-name-face 371,11583
(defconst isabelle-bound-name-face 372,11644
(defconst isabelle-var-name-face 373,11706
(defconst isar-font-lock-local376,11768
(defvar isar-font-lock-keywords-1381,11934
(defvar isar-output-font-lock-keywords-1395,12800
(defvar isar-goals-font-lock-keywords422,14424
(defconst isar-undo 456,15103
(defun isar-remove 458,15165
(defun isar-undos 461,15240
(defun isar-cannot-undo 465,15346
(defconst isar-theory-start-regexp468,15416
(defconst isar-end-regexp474,15581
(defconst isar-undo-fail-regexp478,15682
(defconst isar-undo-skip-regexp482,15786
(defconst isar-undo-ignore-regexp485,15907
(defconst isar-undo-remove-regexp488,15972
(defconst isar-any-entity-regexp496,16147
(defconst isar-named-entity-regexp501,16334
(defconst isar-unnamed-entity-regexp506,16511
(defconst isar-next-entity-regexps509,16613
(defconst isar-generic-expression517,16924
(defconst isar-indent-any-regexp528,17241
(defconst isar-indent-inner-regexp530,17334
(defconst isar-indent-enclose-regexp532,17400
(defconst isar-indent-open-regexp534,17516
(defconst isar-indent-close-regexp536,17626
(defconst isar-outline-regexp542,17763
(defconst isar-outline-heading-end-regexp 546,17916

isar/x-symbol-isabelle.el,1922
(defvar x-symbol-isabelle-required-fonts 20,624
(defvar x-symbol-isabelle-name 28,1028
(defvar x-symbol-isabelle-modeline-name 29,1078
(defcustom x-symbol-isabelle-header-groups-alist 31,1126
(defcustom x-symbol-isabelle-electric-ignore 38,1354
(defvar x-symbol-isabelle-required-fonts 46,1610
(defvar x-symbol-isabelle-extra-menu-items 49,1719
(defvar x-symbol-isabelle-token-grammar53,1817
(defun x-symbol-isabelle-token-list 60,2023
(defvar x-symbol-isabelle-user-table 63,2112
(defvar x-symbol-isabelle-generated-data 66,2233
(defvar x-symbol-isabelle-master-directory 74,2476
(defvar x-symbol-isabelle-image-searchpath 75,2529
(defvar x-symbol-isabelle-image-cached-dirs 76,2581
(defvar x-symbol-isabelle-image-file-truename-alist 77,2651
(defvar x-symbol-isabelle-image-keywords 78,2708
(defcustom x-symbol-isabelle-subscript-matcher 88,3052
(defcustom x-symbol-isabelle-font-lock-regexp 94,3299
(defcustom x-symbol-isabelle-font-lock-limit-regexp 99,3483
(defcustom x-symbol-isabelle-font-lock-contents-regexp 105,3715
(defcustom x-symbol-isabelle-single-char-regexp 115,4107
(defun x-symbol-isabelle-subscript-matcher 121,4385
(defun isabelle-match-subscript 163,6057
(defvar x-symbol-isabelle-font-lock-keywords172,6452
(defvar x-symbol-isabelle-font-lock-allowed-faces 179,6720
(defcustom x-symbol-isabelle-class-alist186,6952
(defcustom x-symbol-isabelle-class-face-alist 197,7377
(defvar x-symbol-isabelle-case-insensitive 212,7905
(defvar x-symbol-isabelle-token-shape 213,7953
(defvar x-symbol-isabelle-input-token-ignore 214,7996
(defvar x-symbol-isabelle-token-list 215,8046
(defvar x-symbol-isabelle-symbol-table 217,8095
(defvar x-symbol-isabelle-xsymbol-table 317,10831
(defun x-symbol-isabelle-prepare-table 463,15265
(defvar x-symbol-isabelle-table471,15465
(defcustom x-symbol-isabelle-auto-style485,15818
(defcustom x-symbol-isabelle-auto-coding-alist 499,16328

lclam/lclam.el,563
(defcustom lclam-prog-name 15,385
(defcustom lclam-web-page21,533
(defun lclam-config 32,763
(defun lclam-shell-config 52,1477
(define-derived-mode lclam-proofscript-mode 72,2136
(define-derived-mode lclam-shell-mode 77,2259
(define-derived-mode lclam-response-mode 82,2393
(define-derived-mode lclam-goals-mode 86,2516
(defun lclam-mode 94,2744
(defun lclam-pre-shell-start 107,3027
(define-derived-mode thy-mode 141,3970
(defvar thy-mode-map 144,4068
(defun thy-add-menus 146,4095
(defun process-thy-file 186,6009
(defun update-thy-only 192,6210

lego/lego.el,1766
(defcustom lego-tags 19,493
(defcustom lego-test-all-name 24,629
(defpgdefault help-menu-entries30,787
(defpgdefault menu-entries34,947
(defvar lego-shell-process-output45,1249
(defconst lego-process-config53,1572
(defconst lego-pretty-set-width 64,2003
(defconst lego-interrupt-regexp 68,2146
(defcustom lego-www-home-page 73,2263
(defcustom lego-www-latest-release78,2387
(defcustom lego-www-refcard84,2565
(defcustom lego-library-www-page90,2714
(defvar lego-prog-name 99,2930
(defvar lego-shell-prompt-pattern 102,2999
(defvar lego-shell-cd 105,3120
(defvar lego-shell-abort-goal-regexp 108,3220
(defvar lego-shell-proof-completed-regexp 113,3412
(defvar lego-save-command-regexp116,3552
(defvar lego-goal-command-regexp118,3642
(defvar lego-kill-goal-command 121,3733
(defvar lego-forget-id-command 122,3776
(defvar lego-undoable-commands-regexp124,3822
(defvar lego-goal-regexp 133,4196
(defvar lego-outline-regexp135,4241
(defvar lego-outline-heading-end-regexp 141,4417
(defvar lego-shell-outline-regexp 143,4470
(defvar lego-shell-outline-heading-end-regexp 144,4522
(define-derived-mode lego-shell-mode 150,4801
(define-derived-mode lego-mode 156,4974
(define-derived-mode lego-goals-mode 167,5271
(defun lego-count-undos 178,5697
(defun lego-goal-command-p 198,6516
(defun lego-find-and-forget 203,6686
(defun lego-goal-hyp 245,8522
(defun lego-state-preserving-p 254,8720
(defvar lego-shell-current-line-width 270,9423
(defun lego-shell-adjust-line-width 278,9730
(defun lego-pre-shell-start 297,10469
(defun lego-mode-config 304,10666
(defun lego-equal-module-filename 373,12764
(defun lego-shell-compute-new-files-list 379,13039
(defun lego-shell-mode-config 393,13565
(defun lego-goals-mode-config 442,15501

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,358
(defconst lego-keywords-save 17,401
(defconst lego-commands19,472
(defconst lego-keywords31,1032
(defconst lego-tacticals 36,1209
(defconst lego-error-regexp 39,1317
(defvar lego-id 42,1476
(defvar lego-ids 44,1503
(defconst lego-arg-list-regexp 48,1699
(defun lego-decl-defn-regexp 51,1815
(defconst lego-definiendum-alternative-regexp59,2187
(defvar lego-font-lock-terms63,2371
(defconst lego-goal-with-hole-regexp89,3227
(defconst lego-save-with-hole-regexp94,3450
(defvar lego-font-lock-keywords-199,3667
(defun lego-init-syntax-table 110,4134

phox/phox.el,682
(defcustom phox-prog-name 31,931
(defcustom phox-sym-lock-enabled 36,1033
(defcustom phox-web-page42,1140
(defcustom phox-doc-dir 48,1290
(defcustom phox-lib-dir 54,1438
(defcustom phox-tags-program 60,1582
(defcustom phox-tags-doc 66,1762
(defcustom phox-etags 72,1900
(defpgdefault menu-entries93,2352
(defun phox-config 107,2545
(defun phox-shell-config 153,4582
(define-derived-mode phox-mode 178,5511
(define-derived-mode phox-shell-mode 198,6123
(define-derived-mode phox-response-mode 203,6251
(define-derived-mode phox-goals-mode 215,6678
(defun phox-pre-shell-start 243,7750
(defpgdefault completion-table257,8264
(defpgdefault x-symbol-language 265,8369

phox/phox-extraction.el,382
(defvar phox-prog-orig 11,480
(defun phox-prog-flags-modify(13,548
(defun phox-prog-flags-extract(42,1352
(defun phox-prog-flags-erase(53,1643
(defun phox-toggle-extraction(61,1839
(defun phox-compile-theorem(73,2241
(defun phox-compile-theorem-on-cursor(79,2467
(defun phox-output 95,2946
(defun phox-output-theorem 105,3160
(defun phox-output-theorem-on-cursor(112,3460

phox/phox-font.el,123
(defconst phox-font-lock-keywords6,282
(defconst phox-sym-lock-keywords-table65,2406
(defun phox-sym-lock-start 88,2980

phox/phox-fun.el,679
(defun phox-init-syntax-table 67,2392
(defvar phox-top-keywords83,2865
(defvar phox-proof-keywords131,3320
(defun phox-find-and-forget 172,3670
(defun phox-assert-next-command-interactive 251,6095
(defun phox-depend-theorem(270,6926
(defun phox-eshow-extlist(279,7216
(defun phox-flag-name(293,7815
(defun phox-path(304,8118
(defun phox-print-expression(315,8355
(defun phox-print-sort-expression(328,8813
(defun phox-priority-symbols-list(339,9126
(defun phox-search-string(351,9499
(defun phox-constraints(366,10027
(defun phox-goals(377,10284
(defvar phox-state-menu389,10494
(defun phox-delete-symbol(414,11484
(defun phox-delete-symbol-on-cursor(420,11693

phox/phox-lang.el,283
(defvar phox-lang8,278
(defun phox-lang-absurd 17,495
(defun phox-lang-suppress 22,590
(defun phox-lang-opendef 27,789
(defun phox-lang-instance 32,908
(defun phox-lang-lock 37,1037
(defun phox-lang-unlock 42,1174
(defun phox-lang-prove 47,1317
(defun phox-lang-let 52,1454

phox/phox-outline.el,70
(defun phox-outline-level(32,1113
(defun phox-setup-outline 46,1587

phox/phox-pbrpm.el,512
(defun phox-pbrpm-left-paren-p 25,1167
(defun phox-pbrpm-right-paren-p 32,1370
(defun phox-pbrpm-menu-from-string 40,1574
(defun phox-pbrpm-rename-in-cmd 49,1908
(defun phox-pbrpm-get-region-name 82,3162
(defun  phox-pbrpm-escape-string 85,3289
(defun phox-pbrpm-generate-menu 89,3424
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
287,10613
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
288,10677
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
289,10739

phox/phox-sym-lock.el,1353
(defvar phox-sym-lock-sym-count 35,1696
(defvar phox-sym-lock-ext-start 38,1766
(defvar phox-sym-lock-ext-end 40,1888
(defvar phox-sym-lock-font-size 43,2007
(defvar phox-sym-lock-keywords 48,2197
(defvar phox-sym-lock-enabled 53,2373
(defvar phox-sym-lock-color 58,2535
(defvar phox-sym-lock-mouse-face 63,2753
(defvar phox-sym-lock-mouse-face-enabled 68,2943
(defconst phox-sym-lock-with-mule 73,3133
(defun phox-sym-lock-gen-symbol 76,3217
(defun phox-sym-lock-make-symbols-atomic 84,3520
(defun phox-sym-lock-compute-font-size 111,4462
(defvar phox-sym-lock-font-name149,5882
(defun phox-sym-lock-set-foreground 187,7167
(defun phox-sym-lock-translate-char 201,7776
(defun phox-sym-lock-translate-char-or-string 209,8044
(defun phox-sym-lock-remap-face 216,8271
(defvar phox-sym-lock-clear-face236,9261
(defun phox-sym-lock 248,9683
(defun phox-sym-lock-rec 257,10087
(defun phox-sym-lock-atom-face 263,10240
(defun phox-sym-lock-pre-idle-hook-first 268,10536
(defun phox-sym-lock-pre-idle-hook-last 276,10894
(defun phox-sym-lock-enable 285,11269
(defun phox-sym-lock-disable 298,11682
(defun phox-sym-lock-mouse-face-enable 311,12100
(defun phox-sym-lock-mouse-face-disable 318,12315
(defun phox-sym-lock-font-lock-hook 325,12534
(defun font-lock-set-defaults 340,13227
(defun phox-sym-lock-patch-keywords 351,13605

phox/phox-tags.el,305
(defun phox-tags-add-table(21,766
(defun phox-tags-reset-table(38,1359
(defun phox-tags-add-doc-table(48,1629
(defun phox-tags-add-lib-table(54,1778
(defun phox-tags-add-local-table(60,1914
(defun phox-tags-create-local-table(66,2097
(defun phox-complete-tag(77,2349
(defvar phox-tags-menu96,2904

phox/x-symbol-phox.el,1609
(defvar x-symbol-phox-required-fonts 14,449
(defcustom x-symbol-phox-header-groups-alist 29,1056
(defcustom x-symbol-phox-electric-ignore 36,1276
(defvar x-symbol-phox-required-fonts 43,1492
(defvar x-symbol-phox-extra-menu-items 46,1593
(defvar x-symbol-phox-token-grammar49,1682
(defvar x-symbol-phox-input-token-grammar63,2473
(defun x-symbol-phox-default-token-list 69,2728
(defvar x-symbol-phox-user-table 81,3046
(defvar x-symbol-phox-generated-data 84,3155
(defvar x-symbol-phox-master-directory 92,3394
(defvar x-symbol-phox-image-searchpath 93,3443
(defvar x-symbol-phox-image-cached-dirs 94,3491
(defvar x-symbol-phox-image-file-truename-alist 95,3557
(defvar x-symbol-phox-image-keywords 96,3610
(defcustom x-symbol-phox-class-alist103,3831
(defcustom x-symbol-phox-class-face-alist 114,4213
(defvar x-symbol-phox-font-lock-keywords 124,4526
(defvar x-symbol-phox-font-lock-allowed-faces 126,4573
(defvar x-symbol-phox-case-insensitive 132,4798
(defvar x-symbol-phox-token-shape 133,4842
(defvar x-symbol-phox-input-token-ignore 134,4881
(defvar x-symbol-phox-token-list 141,5120
(defvar x-symbol-phox-xsymb0-table 143,5165
(defun x-symbol-phox-prepare-table 164,5624
(defvar x-symbol-phox-table172,5800
(defcustom x-symbol-phox-auto-style183,6118
(defvar x-symbol-phox-menu-alist 209,7068
(defvar x-symbol-phox-grid-alist 211,7158
(defvar x-symbol-phox-decode-atree 214,7249
(defvar x-symbol-phox-decode-alist 216,7342
(defvar x-symbol-phox-encode-alist 218,7439
(defvar x-symbol-phox-nomule-decode-exec 222,7596
(defvar x-symbol-phox-nomule-encode-exec 224,7696

plastic/plastic.el,2907
(defcustom plastic-tags 28,805
(defcustom plastic-test-all-name 33,937
(defvar plastic-lit-string 39,1110
(defcustom plastic-help-menu-list43,1223
(defvar plastic-shell-process-output57,1717
(defconst plastic-process-config 65,2043
(defconst plastic-pretty-set-width 72,2293
(defconst plastic-interrupt-regexp 76,2442
(defcustom plastic-www-home-page 82,2563
(defcustom plastic-www-latest-release87,2700
(defcustom plastic-www-refcard93,2873
(defcustom plastic-library-www-page99,3004
(defcustom plastic-base 109,3219
(defvar plastic-prog-name 117,3391
(defun plastic-set-default-env-vars 121,3499
(defvar plastic-shell-prompt-pattern 129,3737
(defvar plastic-shell-cd 132,3862
(defvar plastic-shell-abort-goal-regexp 136,4004
(defvar plastic-shell-proof-completed-regexp 140,4172
(defvar plastic-save-command-regexp143,4315
(defvar plastic-goal-command-regexp145,4411
(defvar plastic-kill-goal-command 148,4508
(defvar plastic-forget-id-command 150,4609
(defvar plastic-undoable-commands-regexp153,4690
(defvar plastic-goal-regexp 165,5137
(defvar plastic-outline-regexp167,5185
(defvar plastic-outline-heading-end-regexp 173,5364
(defvar plastic-shell-outline-regexp 175,5420
(defvar plastic-shell-outline-heading-end-regexp 176,5478
(defvar plastic-error-occurred 178,5549
(define-derived-mode plastic-shell-mode 187,5881
(define-derived-mode plastic-mode 193,6063
(define-derived-mode plastic-goals-mode 207,6516
(defun plastic-count-undos 216,6861
(defun plastic-goal-command-p 236,7737
(defun plastic-find-and-forget 241,7930
(defun plastic-goal-hyp 276,9278
(defun plastic-state-preserving-p 287,9528
(defvar plastic-shell-current-line-width 309,10456
(defun plastic-shell-adjust-line-width 317,10772
(defun plastic-pre-shell-start 338,11653
(defun plastic-mode-config 353,12219
(defun plastic-show-shell-buffer 450,15864
(defun plastic-equal-module-filename 456,15967
(defun plastic-shell-compute-new-files-list 462,16245
(defun plastic-shell-mode-config 478,16782
(defun plastic-goals-mode-config 529,18975
(defun plastic-small-bar 541,19257
(defun plastic-large-bar 543,19346
(defun plastic-preprocessing 545,19484
(defun plastic-all-ctxt 596,21312
(defun plastic-send-one-undo 603,21490
(defun plastic-minibuf-cmd 613,21818
(defun plastic-minibuf 625,22297
(defun plastic-synchro 632,22503
(defun plastic-send-minibuf 637,22644
(defun plastic-had-error 645,22973
(defun plastic-reset-error 649,23148
(defun plastic-call-if-no-error 652,23287
(defun plastic-show-shell 657,23491
(define-key plastic-keymap 666,23753
(define-key plastic-keymap 667,23814
(define-key plastic-keymap 668,23875
(define-key plastic-keymap 669,23935
(define-key plastic-keymap 670,23994
(define-key plastic-keymap 671,24053
(defalias 'proof-toolbar-command proof-toolbar-command
681,24303
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
682,24354

plastic/plastic-syntax.el,648
(defconst plastic-keywords-goal 18,537
(defconst plastic-keywords-save 20,583
(defconst plastic-commands22,657
(defconst plastic-keywords35,1267
(defconst plastic-tacticals 40,1450
(defconst plastic-error-regexp 43,1561
(defvar plastic-id 46,1695
(defvar plastic-ids 48,1725
(defconst plastic-arg-list-regexp 52,1933
(defun plastic-decl-defn-regexp 55,2052
(defconst plastic-definiendum-alternative-regexp63,2433
(defvar plastic-font-lock-terms67,2626
(defconst plastic-goal-with-hole-regexp89,3339
(defconst plastic-save-with-hole-regexp94,3566
(defvar plastic-font-lock-keywords-199,3792
(defun plastic-init-syntax-table 108,4184

twelf/twelf.el,463
(defcustom twelf-root-dir25,591
(defcustom twelf-info-dir31,749
(defun twelf-add-read-declaration 100,3259
(defun twelf-set-syntax 113,3594
(defun twelf-set-word 115,3691
(defun twelf-set-symbol 116,3753
(defun twelf-map-string 118,3817
(defun twelf-mode-extra-config 165,5879
(defconst twelf-syntax-menu171,6085
(defpacustom chatter 185,6452
(defpacustom double-check 190,6545
(defpacustom print-implicit 194,6682
(defpgdefault menu-entries206,6826

twelf/twelf-font.el,917
(defun twelf-font-create-face 31,836
(defvar twelf-font-dark-background 38,1094
(defvar twelf-font-patterns64,2452
(defun twelf-font-fontify-decl 105,4302
(defun twelf-font-fontify-buffer 115,4599
(defun twelf-font-unfontify 122,4858
(defvar font-lock-message-threshold 127,5032
(defun twelf-font-fontify-region 129,5110
(defun twelf-font-highlight 195,7610
(defun twelf-font-find-delimited-comment 204,8067
(defun twelf-font-find-decl 223,8747
(defun twelf-font-find-binder 239,9237
(defun twelf-font-find-parm 301,11094
(defun twelf-font-find-evar 308,11417
(defun twelf-current-decl 330,12159
(defun twelf-next-decl 357,13315
(defconst *whitespace* 382,14337
(defconst *twelf-comment-start* 385,14435
(defconst *twelf-id-chars* 388,14564
(defun skip-twelf-comments-and-whitespace 391,14682
(defun twelf-end-of-par 403,15156
(defun skip-ahead 426,15930
(defun current-line-absolute 438,16352

twelf/twelf-old.el,6958
(defvar twelf-indent 212,8771
(defvar twelf-infix-regexp 215,8831
(defvar twelf-server-program 219,9026
(defvar twelf-info-file 222,9107
(defvar twelf-server-display-commands 225,9180
(defvar twelf-highlight-range-function 230,9428
(defvar twelf-focus-function 235,9711
(defvar twelf-server-echo-commands 241,9991
(defvar twelf-save-silently 244,10112
(defvar twelf-server-timeout 248,10284
(defvar twelf-sml-program 252,10431
(defvar twelf-sml-args 255,10503
(defvar twelf-sml-display-queries 258,10569
(defvar twelf-mode-hook 261,10677
(defvar twelf-server-mode-hook 264,10771
(defvar twelf-config-mode-hook 267,10879
(defvar twelf-sml-mode-hook 270,10993
(defvar twelf-to-twelf-sml-mode 273,11074
(defvar twelf-config-mode 276,11166
(defvar *twelf-server-buffer-name* 283,11430
(defvar *twelf-server-buffer* 286,11534
(defvar *twelf-server-process-name* 289,11622
(defvar *twelf-config-buffer* 292,11713
(defvar *twelf-config-time* 295,11807
(defvar *twelf-config-list* 298,11920
(defvar *twelf-server-last-process-mark* 301,12032
(defvar *twelf-last-region-sent* 304,12150
(defvar *twelf-last-input-buffer* 311,12474
(defvar *twelf-error-pos* 315,12597
(defconst *twelf-read-functions*318,12673
(defconst *twelf-parm-table*325,12911
(defvar twelf-chatter 338,13287
(defvar twelf-double-check 346,13504
(defvar twelf-print-implicit 349,13591
(defconst *twelf-track-parms*352,13683
(defun install-basic-twelf-keybindings 363,14107
(defun install-twelf-keybindings 388,15076
(defvar twelf-mode-map 404,15841
(defvar twelf-mode-syntax-table 416,16277
(defun set-twelf-syntax 419,16356
(defun set-word 421,16453
(defun set-symbol 422,16508
(defun map-string 424,16566
(defconst *whitespace* 456,18043
(defconst *twelf-comment-start* 459,18141
(defconst *twelf-id-chars* 462,18270
(defun skip-twelf-comments-and-whitespace 465,18388
(defun twelf-end-of-par 477,18862
(defun twelf-current-decl 500,19636
(defun twelf-mark-decl 527,20792
(defun twelf-indent-decl 536,21058
(defun twelf-indent-region 545,21344
(defun twelf-indent-lines 556,21668
(defun twelf-comment-indent 564,21841
(defun looked-at 575,22197
(defun twelf-indent-line 580,22369
(defun twelf-indent-line-to 613,24112
(defun twelf-calculate-indent 626,24567
(defun twelf-dsb 641,25191
(defun twelf-mode-variables 667,26603
(defun twelf-mode 689,27416
(defun twelf-info 904,35798
(defconst twelf-error-regexp918,36338
(defconst twelf-error-fields-regexp922,36449
(defconst twelf-error-decl-regexp928,36662
(defun looked-at-nth 932,36811
(defun looked-at-nth-int 938,36993
(defun twelf-error-parser 943,37111
(defun twelf-error-decl 957,37714
(defun twelf-mark-relative 963,37893
(defun twelf-mark-absolute 979,38563
(defun twelf-find-decl 1004,39449
(defun twelf-next-error 1019,40005
(defun twelf-goto-error 1087,42815
(defun twelf-convert-standard-filename 1101,43353
(defun string-member 1113,43848
(defun twelf-config-proceed-p 1125,44340
(defun twelf-save-if-config 1132,44602
(defun twelf-config-save-some-buffers 1145,45074
(defun twelf-save-check-config 1149,45239
(defun twelf-check-config 1164,45795
(defun twelf-save-check-file 1176,46235
(defun twelf-buffer-substring 1192,46958
(defun twelf-buffer-substring-dot 1198,47220
(defun twelf-check-declaration 1204,47486
(defun twelf-highlight-range-zmacs 1227,48546
(defun twelf-focus 1233,48796
(defun twelf-focus-noop 1239,49062
(defun twelf-type-const 1322,52684
(defvar twelf-server-mode-map 1439,57826
(defconst twelf-server-cd-regexp 1451,58378
(defun looked-at-string 1454,58518
(defun twelf-server-directory-tracker 1458,58659
(defun twelf-input-filter 1480,59839
(defun twelf-server-mode 1486,60094
(defun twelf-parse-config 1519,61311
(defun twelf-server-read-config 1537,62203
(defun twelf-server-sync-config 1546,62540
(defun twelf-get-server-buffer 1576,64046
(defun twelf-init-variables 1593,64720
(defun twelf-server 1600,64933
(defun twelf-server-process 1642,66847
(defun twelf-server-display 1651,67253
(defun display-server-buffer 1658,67527
(defun twelf-server-send-command 1673,68259
(defun twelf-accept-process-output 1694,69219
(defun twelf-server-wait 1703,69658
(defun twelf-server-quit 1745,71796
(defun twelf-server-interrupt 1750,71917
(defun twelf-reset 1755,72053
(defun twelf-config-directory 1760,72197
(defun twelf-server-configure 1771,72611
(defun natp 1844,75903
(defun twelf-read-nat 1848,76004
(defun twelf-read-bool 1857,76271
(defun twelf-read-limit 1863,76419
(defun twelf-read-strategy 1873,76722
(defun twelf-read-value 1879,76874
(defun twelf-set 1883,77037
(defun twelf-set-parm 1896,77514
(defun track-parm 1905,77811
(defun twelf-toggle-double-check 1910,77985
(defun twelf-toggle-print-implicit 1916,78188
(defun twelf-get 1922,78401
(defun twelf-timers-reset 1936,79027
(defun twelf-timers-show 1941,79147
(defun twelf-timers-check 1947,79298
(defun twelf-server-restart 1953,79463
(defun twelf-config-mode 1969,80140
(defun twelf-config-mode-check 1985,80739
(defun twelf-tag 1994,81189
(defun twelf-tag-files 2022,82453
(default: *tags-errors*)2026,82756
(defun twelf-tag-file 2047,83507
(defun twelf-next-decl 2082,84729
(defun skip-ahead 2107,85751
(defun current-line-absolute 2119,86173
(defun new-temp-buffer 2124,86383
(defun rev-relativize 2135,86767
(defvar twelf-sml-mode-map 2149,87227
(defconst twelf-sml-prompt-regexp 2159,87605
(defun expand-dir 2161,87660
(defun twelf-sml-cd 2168,87921
(defconst twelf-sml-cd-regexp 2180,88410
(defun twelf-sml-directory-tracker 2183,88544
(defun twelf-sml-mode 2199,89389
(defun twelf-sml 2250,91323
(defun switch-to-twelf-sml 2270,92283
(defun display-twelf-sml-buffer 2281,92632
(defun twelf-sml-send-string 2297,93348
(defun twelf-sml-send-region 2302,93552
(defun twelf-sml-send-query 2326,94758
(defun twelf-sml-send-newline 2336,95155
(defun twelf-sml-send-semicolon 2344,95483
(defun twelf-sml-status 2352,95817
(defvar twelf-sml-init 2374,96764
(defun twelf-sml-set-mode 2377,96941
(defun twelf-sml-quit 2403,98118
(defun twelf-sml-process-buffer 2408,98230
(defun twelf-sml-process 2412,98346
(defvar twelf-to-twelf-sml-mode 2424,98862
(defun install-twelf-to-twelf-sml-keybindings 2427,98947
(defvar twelf-to-twelf-sml-mode-map 2437,99332
(defun twelf-to-twelf-sml-mode 2448,99845
(defconst twelf-at-point-menu2498,101712
(defconst twelf-server-state-menu2508,102084
(defconst twelf-error-menu2518,102401
(defconst twelf-tags-menu2524,102545
(defun twelf-toggle-server-display-commands 2534,102830
(defconst twelf-options-menu2537,102954
(defconst twelf-timers-menu2572,104692
(defconst twelf-syntax-menu2585,105186
(defun twelf-add-menu 2612,106052
(defun twelf-remove-menu 2616,106154
(defun twelf-reset-menu 2620,106252
(defun twelf-server-add-menu 2647,107151
(defun twelf-server-remove-menu 2651,107274
(defun twelf-server-reset-menu 2655,107386

generic/pg-assoc.el,329
(define-derived-mode proof-universal-keys-only-mode 20,563
(defun proof-associated-buffers 32,987
(defun proof-associated-windows 41,1184
(defun pg-assoc-strip-subterm-markup 58,1665
(defvar pg-assoc-ann-regexp 84,2598
(defun pg-assoc-strip-subterm-markup-buf 87,2693
(defun pg-assoc-strip-subterm-markup-buf-old 110,3412

generic/pg-autotest.el,442
(defvar pg-autotest-success 21,538
(defun pg-autotest-find-file 25,622
(defun pg-autotest-find-file-restart 32,893
(defmacro pg-autotest 45,1341
(defun pg-autotest-script-wholefile 59,1689
(defun pg-autotest-retract-file 76,2302
(defun pg-autotest-assert-processed 82,2438
(defun pg-autotest-assert-unprocessed 89,2684
(defun pg-autotest-message 96,2931
(defun pg-autotest-quit-prover 103,3124
(defun pg-autotest-finished 109,3306

generic/pg-goals.el,704
(define-derived-mode proof-goals-mode 29,669
(define-key proof-goals-mode-map 50,1432
(define-key proof-goals-mode-map 53,1515
(define-key proof-goals-mode-map 54,1585
(define-key proof-goals-mode-map 62,2175
(define-key proof-goals-mode-map 64,2248
(define-key proof-goals-mode-map 65,2316
(define-key proof-goals-mode-map 71,2750
(defun proof-goals-config-done 86,3014
(defun pg-goals-display 96,3302
(defun pg-goals-analyse-structure 152,5455
(defun pg-goals-make-top-span 279,10502
(defun pg-goals-yank-subterm 319,12006
(defun pg-goals-button-action 346,12906
(defun proof-expand-path 367,13879
(defun pg-goals-construct-command 376,14123
(defun pg-goals-get-subterm-help 405,15148

generic/pg-metadata.el,128
(defcustom pg-metadata-default-directory 23,628
(defface proof-preparsed-span 28,802
(defun pg-metadata-filename-for 39,1065

generic/pg-pbrpm.el,1781
(defvar pg-pbrpm-use-buffer-menu 13,309
(defvar pg-pbrpm-buffer-menu 15,428
(defvar pg-pbrpm-spans 16,462
(defvar pg-pbrpm-goal-description 17,490
(defvar pg-pbrpm-windows-dialog-bug 18,529
(defun pg-pbrpm-erase-buffer-menu 20,571
(defun pg-pbrpm-menu-change-hook 27,755
(defun pg-pbrpm-create-reset-buffer-menu 45,1332
(defun pg-pbrpm-analyse-goal-buffer 59,1946
(defun pg-pbrpm-button-action 120,4366
(defun pg-pbrpm-exists 127,4592
(defun pg-pbrpm-eliminate-id 131,4704
(defun pg-pbrpm-build-menu 139,4952
(defun pg-pbrpm-setup-span 199,7269
(defun pg-pbrpm-run-command 259,9600
(defun pg-pbrpm-get-pos-info 288,10911
(defun pg-pbrpm-get-region-info 324,12053
(defun auto-select-arround-pos 334,12378
(defun pg-pbrpm-translate-position 346,12822
(defun pg-pbrpm-process-click 352,13046
(defvar pg-pbrpm-remember-region-selected-region 372,14053
(defvar pg-pbrpm-regions-list 373,14107
(defun pg-pbrpm-erase-regions-list 375,14143
(defun pg-pbrpm-filter-regions-list 384,14452
(defface pg-pbrpm-multiple-selection-face391,14715
(defface pg-pbrpm-menu-input-face399,14920
(defun pg-pbrpm-do-remember-region 407,15113
(defun pg-pbrpm-remember-region-drag-up-hook 428,15964
(defun pg-pbrpm-remember-region-click-hook 432,16135
(defun pg-pbrpm-remember-region 437,16320
(defun pg-pbrpm-process-region 451,17035
(defun pg-pbrpm-process-regions-list 468,17761
(defun pg-pbrpm-region-expression 472,17944
(define-key proof-goals-mode-map 497,18906
(define-key proof-goals-mode-map 498,18976
(define-key proof-goals-mode-map 499,19053
(define-key pg-span-context-menu-keymap 500,19133
(define-key pg-span-context-menu-keymap 501,19210
(define-key proof-mode-map 502,19293
(define-key proof-mode-map 503,19357
(define-key proof-mode-map 504,19428

generic/pg-pgip.el,2889
(defalias 'pg-pgip-debug pg-pgip-debug
29,883
(defalias 'pg-pgip-error pg-pgip-error
30,924
(defalias 'pg-pgip-warning pg-pgip-warning
31,959
(defconst pg-pgip-version-supported 33,1009
(defun pg-pgip-process-packet 37,1115
(defvar pg-pgip-last-seen-id 47,1688
(defvar pg-pgip-last-seen-seq 48,1722
(defun pg-pgip-process-pgip 50,1758
(defun pg-pgip-process-msg 69,2689
(defvar pg-pgip-post-process-functions83,3259
(defun pg-pgip-post-process 93,3746
(defun pg-pgip-process-askpgip 109,4357
(defun pg-pgip-process-usespgip 114,4516
(defun pg-pgip-process-usespgml 118,4680
(defun pg-pgip-process-pgmlconfig 122,4844
(defun pg-pgip-process-proverinfo 138,5463
(defun pg-pgip-process-hasprefs 155,6128
(defun pg-pgip-haspref 169,6760
(defun pg-pgip-process-prefval 188,7539
(defun pg-pgip-process-guiconfig 215,8248
(defvar proof-assistant-idtables 222,8365
(defun pg-pgip-process-ids 225,8482
(defun pg-complete-idtable-symbol 251,9561
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
256,9653
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
257,9709
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
258,9765
(defun pg-pgip-process-idvalue 261,9823
(defun pg-pgip-process-menuadd 273,10160
(defun pg-pgip-process-menudel 276,10203
(defun pg-pgip-process-ready 285,10436
(defun pg-pgip-process-cleardisplay 288,10477
(defun pg-pgip-process-proofstate 302,10954
(defun pg-pgip-process-normalresponse 306,11031
(defun pg-pgip-process-errorresponse 310,11155
(defun pg-pgip-process-scriptinsert 314,11278
(defun pg-pgip-process-metainforesponse 319,11412
(defun pg-pgip-process-informfileloaded 328,11653
(defun pg-pgip-process-informfileretracted 334,11920
(defun pg-pgip-process-brokerstatus 347,12397
(defun pg-pgip-process-proveravailmsg 350,12445
(defun pg-pgip-process-newprovermsg 353,12495
(defun pg-pgip-process-proverstatusmsg 356,12543
(defvar pg-pgip-srcids 365,12790
(defun pg-pgip-process-newfile 369,12897
(defun pg-pgip-process-filestatus 385,13485
(defun pg-pgip-process-newobj 405,14140
(defun pg-pgip-process-delobj 408,14182
(defun pg-pgip-process-objectstatus 411,14224
(defun pg-pgip-process-parsescript 425,14580
(defun pg-pgip-get-pgiptype 448,15455
(defun pg-pgip-default-for 468,16252
(defun pg-pgip-subst-for 481,16647
(defun pg-pgip-interpret-value 493,16990
(defun pg-pgip-interpret-choice 511,17676
(defun pg-pgip-string-of-command 542,18696
(defconst pg-pgip-id559,19457
(defvar pg-pgip-refseq 565,19737
(defvar pg-pgip-refid 567,19835
(defvar pg-pgip-seq 570,19929
(defun pg-pgip-assemble-packet 572,19993
(defun pg-pgip-issue 590,20808
(defun pg-pgip-maybe-askpgip 607,21421
(defun pg-pgip-askprefs 613,21612
(defun pg-pgip-askids 617,21726
(defun pg-pgip-reset 630,22017
(defconst pg-pgip-start-element-regexp 661,22715
(defconst pg-pgip-end-element-regexp 662,22767

generic/pg-pgip-old.el,456
(defun pg-pgip-process-oldhaspref 18,633
(defun pg-pgip-process-haspref 21,730
(defun pg-pgip-old-interpret-bool 57,2158
(defun pg-pgip-old-interpret-int 66,2442
(defun pg-pgip-old-interpret-string 71,2615
(defun pg-pgip-old-interpret-choice 74,2669
(defun pg-pgip-old-interpret-value 94,3388
(defun pg-pgip-old-default-for 113,3934
(defun pg-pgip-old-subst-for 124,4258
(defun pg-pgip-old-get-type 131,4423
(defun pg-pgip-old-pgiptype 138,4639

generic/pg-response.el,1188
(define-derived-mode proof-response-mode 25,617
(defun proof-response-config-done 50,1658
(defvar proof-shell-special-display-regexp 71,2433
(defconst proof-multiframe-specifiers 79,2838
(defun proof-map-multiple-frame-specifiers 88,3202
(defconst proof-multiframe-parameters98,3664
(defun proof-multiple-frames-enable 107,3963
(defun proof-three-window-enable 129,4683
(defun proof-select-three-b 133,4747
(defun proof-display-three-b 148,5216
(defvar pg-frame-configuration 162,5710
(defun pg-cache-frame-configuration 166,5857
(defun proof-layout-windows 170,6028
(defun proof-delete-other-frames 211,7841
(defvar pg-response-erase-flag 242,8936
(defun proof-shell-maybe-erase-response245,9051
(defun pg-response-display 276,10253
(defun pg-response-display-with-face 294,11107
(defun pg-response-clear-displays 332,12464
(defvar pg-response-next-error 350,13043
(defun proof-next-error 354,13165
(defun pg-response-has-error-location 434,16105
(defvar proof-trace-last-fontify-pos 457,16938
(defun proof-trace-fontify-pos 459,16981
(defun proof-trace-buffer-display 467,17295
(defun proof-trace-buffer-finish 491,18268
(defun pg-thms-buffer-clear 512,18847

generic/pg-thymodes.el,152
(defmacro pg-defthymode 19,466
(defmacro pg-do-unless-null 67,2277
(defun pg-symval 72,2364
(defun pg-modesym 78,2520
(defun pg-modesymval 82,2634

generic/pg-user.el,2335
(defmacro proof-maybe-save-point 21,410
(defun proof-maybe-follow-locked-end 29,612
(defun proof-assert-next-command-interactive 43,977
(defun proof-process-buffer 53,1348
(defun proof-undo-last-successful-command 67,1665
(defun proof-undo-and-delete-last-successful-command 72,1827
(defun proof-undo-last-successful-command-1 94,2799
(defun proof-retract-buffer 110,3364
(defun proof-retract-current-goal 119,3644
(defun proof-interrupt-process 137,4135
(defun proof-goto-command-start 164,5120
(defun proof-goto-command-end 187,6062
(defun proof-mouse-goto-point 212,6842
(defun proof-mouse-track-insert 227,7416
(defvar proof-minibuffer-history 262,8526
(defun proof-minibuffer-cmd 265,8620
(defun proof-frob-locked-end 313,10426
(defmacro proof-if-setting-configured 406,13340
(defmacro proof-define-assistant-command 414,13610
(defmacro proof-define-assistant-command-witharg 427,14076
(defun proof-issue-new-command 447,14901
(defun proof-cd-sync 492,16400
(deflocal proof-electric-terminator 543,17869
(defun proof-electric-terminator-enable 553,18216
(defun proof-electric-term-incomment-fn 564,18703
(defun proof-process-electric-terminator 584,19459
(defun proof-electric-terminator 611,20610
(defun proof-add-completions 633,21248
(defun proof-script-complete 653,22005
(defun pg-insert-last-output-as-comment 681,22596
(defun pg-copy-span-contents 712,23824
(defun pg-numth-span-higher-or-lower 729,24384
(defun pg-control-span-of 755,25131
(defun pg-move-span-contents 761,25335
(defun pg-fixup-children-span 815,27559
(defun pg-move-region-down 822,27762
(defun pg-move-region-up 831,28056
(defun proof-forward-command 861,28896
(defun proof-backward-command 882,29618
(defvar pg-span-context-menu-keymap898,29862
(defun pg-span-for-event 914,30289
(defun pg-span-context-menu 925,30673
(defun pg-toggle-visibility 940,31133
(defun pg-create-in-span-context-menu 950,31455
(defun pg-span-undo 983,32807
(defun pg-goals-buffers-hint 1029,34217
(defun pg-slow-fontify-tracing-hint 1032,34384
(defun pg-response-buffers-hint 1035,34540
(defun pg-jump-to-end-hint 1044,34889
(defun pg-processing-complete-hint 1047,35005
(defun pg-next-error-hint 1063,35691
(defun pg-hint 1067,35828
(defun pg-identifier-under-mouse-query 1086,36504
(defun proof-imenu-enable 1131,38131

generic/pg-xhtml.el,392
(defvar pg-xhtml-dir 17,423
(defun pg-xhtml-dir 20,489
(defvar pg-xhtml-file-count 32,856
(defun pg-xhtml-next-file 35,928
(defvar pg-xhtml-header 47,1159
(defmacro pg-xhtml-write-tempfile 53,1400
(defun pg-xhtml-cleanup-tempdir 71,1996
(defvar pg-mozilla-prog-name 75,2127
(defun pg-xhtml-display-file-mozilla 79,2235
(defalias 'pg-xhtml-display-file pg-xhtml-display-file
84,2408

generic/pg-xml.el,1096
(defun pg-xml-parse-string 40,1169
(defun pg-xml-parse-buffer 51,1503
(defun pg-xml-get-attr 73,2236
(defun pg-xml-child-elts 81,2540
(defun pg-xml-child-elt 86,2745
(defun pg-xml-get-child 94,3028
(defun pg-xml-get-text-content 104,3400
(defmacro pg-xml-attr 115,3750
(defmacro pg-xml-node 117,3812
(defconst pg-xml-header 120,3905
(defun pg-xml-string-of 124,3982
(defun pg-xml-output-internal 135,4354
(defun pg-xml-cdata 169,5504
(defun pg-pgip-get-icon 177,5697
(defsubst pg-pgip-get-name 181,5845
(defsubst pg-pgip-get-version 184,5962
(defsubst pg-pgip-get-descr 187,6085
(defsubst pg-pgip-get-thmname 190,6204
(defsubst pg-pgip-get-thyname 193,6327
(defsubst pg-pgip-get-url 196,6450
(defsubst pg-pgip-get-srcid 199,6565
(defsubst pg-pgip-get-proverid 202,6684
(defsubst pg-pgip-get-symname 205,6809
(defsubst pg-pgip-get-prefcat 208,6929
(defsubst pg-pgip-get-default 211,7057
(defsubst pg-pgip-get-objtype 214,7180
(defsubst pg-pgip-get-value 217,7303
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7373
(defun pg-pgip-get-pgmltext 222,7432

generic/proof-autoloads.el,57
(defalias (quote proof-x-symbol-decode-region)421,14247

generic/proof-config.el,11099
(defgroup proof-user-options 84,3173
(defcustom proof-electric-terminator-enable 89,3287
(defcustom proof-toolbar-enable 101,3821
(defcustom proof-imenu-enable 107,3994
(defpgcustom x-symbol-enable 113,4165
(defpgcustom maths-menu-enable 122,4515
(defpgcustom mmm-enable 128,4695
(defcustom pg-show-hints 137,5049
(defcustom proof-output-fontify-enable 142,5184
(defcustom proof-trace-output-slow-catchup 152,5566
(defcustom proof-strict-state-preserving 162,6064
(defcustom proof-strict-read-only 175,6673
(defcustom proof-three-window-enable 185,7023
(defcustom proof-multiple-frames-enable 204,7778
(defcustom proof-delete-empty-windows 213,8114
(defcustom proof-shrink-windows-tofit 224,8645
(defcustom proof-toolbar-use-button-enablers 231,8917
(defcustom proof-query-file-save-when-activating-scripting 254,9789
(defpgcustom script-indent 270,10512
(defcustom proof-one-command-per-line 276,10700
(defcustom proof-prog-name-ask 284,10920
(defcustom proof-prog-name-guess 290,11081
(defcustom proof-tidy-response298,11341
(defcustom proof-keep-response-history312,11808
(defcustom proof-general-debug 322,12195
(defcustom proof-experimental-features 331,12568
(defcustom proof-follow-mode 349,13330
(defcustom proof-auto-action-when-deactivating-scripting 375,14525
(defcustom proof-script-command-separator 398,15476
(defcustom proof-rsh-command 406,15769
(defcustom proof-disappearing-proofs 422,16320
(defgroup proof-faces 449,16970
(defface proof-queue-face 454,17076
(defface proof-locked-face462,17356
(defface proof-declaration-name-face475,17859
(defconst proof-declaration-name-face 487,18252
(defface proof-tacticals-name-face492,18488
(defconst proof-tacticals-name-face 501,18750
(defface proof-tactics-name-face506,18980
(defconst proof-tactics-name-face 515,19245
(defface proof-error-face 520,19469
(defface proof-warning-face528,19676
(defconst proof-warning-face 537,19933
(defface proof-eager-annotation-face539,19984
(defface proof-debug-message-face547,20202
(defface proof-boring-face555,20401
(defface proof-mouse-highlight-face563,20593
(defface proof-highlight-dependent-face571,20789
(defface proof-highlight-dependency-face579,20998
(defface proof-active-area-face 587,21195
(defgroup prover-config 604,21471
(defcustom proof-mode-for-shell 638,22590
(defcustom proof-mode-for-response 645,22837
(defcustom proof-mode-for-goals 652,23120
(defcustom proof-mode-for-script 659,23375
(defcustom proof-guess-command-line 670,23809
(defcustom proof-assistant-home-page 685,24306
(defcustom proof-context-command 691,24476
(defcustom proof-info-command 696,24610
(defcustom proof-showproof-command 703,24882
(defcustom proof-goal-command 708,25018
(defcustom proof-save-command 716,25316
(defcustom proof-find-theorems-command 724,25626
(defconst proof-toolbar-entries-default731,25935
(defpgcustom toolbar-entries 765,27853
(defcustom proof-assistant-true-value 783,28574
(defcustom proof-assistant-false-value 789,28764
(defcustom proof-assistant-format-int-fn 795,28958
(defcustom proof-assistant-format-string-fn 802,29207
(defcustom proof-assistant-setting-format 809,29474
(defgroup proof-script 831,30169
(defcustom proof-terminal-char 836,30299
(defcustom proof-script-sexp-commands 846,30703
(defcustom proof-script-command-end-regexp 857,31173
(defcustom proof-script-command-start-regexp 875,31992
(defcustom proof-script-use-old-parser 886,32454
(defcustom proof-script-integral-proofs 898,32943
(defcustom proof-script-fly-past-comments 913,33599
(defcustom proof-script-parse-function 920,33916
(defcustom proof-script-comment-start 938,34562
(defcustom proof-script-comment-start-regexp 949,34997
(defcustom proof-script-comment-end 957,35314
(defcustom proof-script-comment-end-regexp 969,35732
(defcustom pg-insert-output-as-comment-fn 977,36043
(defcustom proof-string-start-regexp 983,36295
(defcustom proof-string-end-regexp 988,36460
(defcustom proof-case-fold-search 993,36621
(defcustom proof-save-command-regexp 1002,37037
(defcustom proof-save-with-hole-regexp 1007,37148
(defcustom proof-save-with-hole-result 1019,37600
(defcustom proof-goal-command-regexp 1030,38064
(defcustom proof-goal-with-hole-regexp 1039,38456
(defcustom proof-goal-with-hole-result 1051,38900
(defcustom proof-non-undoables-regexp 1061,39299
(defcustom proof-nested-undo-regexp 1072,39755
(defcustom proof-ignore-for-undo-count 1088,40467
(defcustom proof-script-next-entity-regexps 1096,40770
(defcustom proof-script-find-next-entity-fn1140,42504
(defcustom proof-script-imenu-generic-expression 1160,43334
(defcustom proof-goal-command-p 1178,44189
(defcustom proof-really-save-command-p 1205,45630
(defcustom proof-completed-proof-behaviour 1217,46091
(defcustom proof-count-undos-fn 1245,47451
(defconst proof-no-command 1280,49052
(defcustom proof-find-and-forget-fn 1285,49256
(defcustom proof-forget-id-command 1302,49967
(defcustom pg-topterm-goalhyplit-fn 1312,50325
(defcustom proof-kill-goal-command 1324,50881
(defcustom proof-undo-n-times-cmd 1338,51391
(defcustom proof-nested-goals-history-p 1352,51940
(defcustom proof-state-preserving-p 1361,52278
(defcustom proof-activate-scripting-hook 1371,52748
(defcustom proof-deactivate-scripting-hook 1390,53526
(defcustom proof-indent 1403,53891
(defcustom proof-indent-hang 1408,53998
(defcustom proof-indent-enclose-offset 1413,54124
(defcustom proof-indent-open-offset 1418,54266
(defcustom proof-indent-close-offset 1423,54403
(defcustom proof-indent-any-regexp 1428,54541
(defcustom proof-indent-inner-regexp 1433,54701
(defcustom proof-indent-enclose-regexp 1438,54855
(defcustom proof-indent-open-regexp 1443,55009
(defcustom proof-indent-close-regexp 1448,55161
(defcustom proof-script-font-lock-keywords 1454,55315
(defcustom proof-script-syntax-table-entries 1462,55638
(defcustom proof-script-span-context-menu-extensions 1480,56035
(defgroup proof-shell 1506,56824
(defcustom proof-prog-name 1516,56995
(defpgcustom prog-args 1529,57630
(defpgcustom prog-env 1542,58205
(defcustom proof-shell-auto-terminate-commands 1551,58631
(defcustom proof-shell-pre-sync-init-cmd 1560,59028
(defcustom proof-shell-init-cmd 1574,59587
(defcustom proof-shell-restart-cmd 1585,60057
(defcustom proof-shell-quit-cmd 1590,60212
(defcustom proof-shell-quit-timeout 1595,60379
(defcustom proof-shell-cd-cmd 1605,60827
(defcustom proof-shell-start-silent-cmd 1622,61494
(defcustom proof-shell-stop-silent-cmd 1631,61870
(defcustom proof-shell-silent-threshold 1640,62207
(defcustom  proof-shell-inform-file-processed-cmd 1648,62541
(defcustom  proof-shell-inform-file-retracted-cmd 1669,63464
(defcustom proof-auto-multiple-files 1697,64735
(defcustom proof-cannot-reopen-processed-files 1712,65456
(defcustom proof-shell-require-command-regexp 1726,66123
(defcustom proof-done-advancing-require-function 1737,66585
(defcustom proof-shell-quiet-errors 1743,66825
(defcustom proof-shell-prompt-pattern 1756,67159
(defcustom proof-shell-wakeup-char 1766,67581
(defcustom proof-shell-annotated-prompt-regexp 1772,67812
(defcustom proof-shell-abort-goal-regexp 1788,68452
(defcustom proof-shell-error-regexp 1793,68587
(defcustom proof-shell-truncate-before-error 1813,69381
(defcustom pg-next-error-regexp 1827,69924
(defcustom pg-next-error-filename-regexp 1842,70534
(defcustom pg-next-error-extract-filename 1866,71572
(defcustom proof-shell-interrupt-regexp 1873,71815
(defcustom proof-shell-proof-completed-regexp 1887,72407
(defcustom proof-shell-clear-response-regexp 1900,72915
(defcustom proof-shell-clear-goals-regexp 1907,73214
(defcustom proof-shell-start-goals-regexp 1914,73507
(defcustom proof-shell-end-goals-regexp 1922,73874
(defcustom proof-shell-eager-annotation-start 1928,74116
(defcustom proof-shell-eager-annotation-start-length 1946,74854
(defcustom proof-shell-eager-annotation-end 1957,75281
(defcustom proof-shell-assumption-regexp 1973,75957
(defcustom proof-shell-process-file 1983,76372
(defcustom proof-shell-retract-files-regexp 2005,77324
(defcustom proof-shell-compute-new-files-list 2014,77660
(defcustom pg-use-specials-for-fontify 2026,78205
(defcustom pg-special-char-regexp 2034,78553
(defcustom proof-shell-set-elisp-variable-regexp 2040,78698
(defcustom proof-shell-match-pgip-cmd 2073,80212
(defcustom proof-shell-issue-pgip-cmd 2082,80542
(defcustom proof-shell-query-dependencies-cmd 2091,80898
(defcustom proof-shell-theorem-dependency-list-regexp 2098,81158
(defcustom proof-shell-theorem-dependency-list-split 2114,81818
(defcustom proof-shell-show-dependency-cmd 2123,82243
(defcustom proof-shell-identifier-under-mouse-cmd 2130,82512
(defcustom proof-shell-trace-output-regexp 2153,83593
(defcustom proof-shell-thms-output-regexp 2169,84137
(defcustom proof-shell-unicode 2182,84523
(defcustom proof-shell-filename-escapes 2190,84851
(defcustom proof-shell-process-connection-type 2207,85531
(defcustom proof-shell-strip-crs-from-input 2230,86578
(defcustom proof-shell-strip-crs-from-output 2242,87067
(defcustom proof-shell-insert-hook 2250,87435
(defcustom proof-pre-shell-start-hook 2290,89399
(defcustom proof-shell-handle-delayed-output-hook2306,89871
(defcustom proof-shell-handle-error-or-interrupt-hook2312,90086
(defcustom proof-shell-pre-interrupt-hook2330,90835
(defcustom proof-shell-process-output-system-specific 2338,91107
(defcustom proof-state-change-hook 2357,91972
(defcustom proof-shell-font-lock-keywords 2368,92354
(defcustom proof-shell-syntax-table-entries 2376,92682
(defgroup proof-goals 2394,93054
(defcustom pg-subterm-first-special-char 2399,93175
(defcustom pg-subterm-anns-use-stack 2407,93487
(defcustom pg-goals-change-goal 2416,93791
(defcustom pbp-goal-command 2421,93906
(defcustom pbp-hyp-command 2426,94062
(defcustom pg-subterm-help-cmd 2431,94224
(defcustom pg-goals-error-regexp 2438,94460
(defcustom proof-shell-result-start 2443,94620
(defcustom proof-shell-result-end 2449,94854
(defcustom pg-subterm-start-char 2455,95067
(defcustom pg-subterm-sep-char 2469,95649
(defcustom pg-subterm-end-char 2475,95828
(defcustom pg-topterm-regexp 2481,95985
(defcustom proof-goals-font-lock-keywords 2498,96588
(defcustom proof-resp-font-lock-keywords 2512,97267
(defcustom pg-before-fontify-output-hook 2524,97845
(defcustom pg-after-fontify-output-hook 2532,98205
(defgroup proof-x-symbol 2544,98459
(defcustom proof-xsym-extra-modes 2549,98587
(defcustom proof-xsym-font-lock-keywords 2562,99216
(defcustom proof-xsym-activate-command 2570,99593
(defcustom proof-xsym-deactivate-command 2577,99829
(defpgcustom favourites 2594,100296
(defpgcustom menu-entries 2599,100486
(defpgcustom help-menu-entries 2606,100723
(defpgcustom keymap 2613,100986
(defpgcustom completion-table 2618,101157
(defpgcustom tags-program 2628,101522
(defcustom proof-general-name 2640,101695
(defcustom proof-general-home-page2645,101852
(defcustom proof-unnamed-theorem-name2651,102011
(defcustom proof-universal-keys2657,102195

generic/proof-depends.el,824
(defvar proof-thm-names-of-files 19,540
(defvar proof-def-names-of-files 25,824
(defun proof-depends-module-name-for-buffer 34,1128
(defun proof-depends-module-of 44,1570
(defun proof-depends-names-in-same-file 52,1864
(defun proof-depends-process-dependencies 71,2484
(defun proof-dependency-in-span-context-menu 124,4226
(defun proof-dep-alldeps-menu 147,5129
(defun proof-dep-make-alldeps-menu 153,5356
(defun proof-dep-split-deps 171,5852
(defun proof-dep-make-submenu 192,6551
(defun proof-make-highlight-depts-menu 202,6904
(defun proof-goto-dependency 212,7208
(defun proof-show-dependency 218,7431
(defconst pg-dep-span-priority 225,7721
(defconst pg-ordinary-span-priority 226,7757
(defun proof-highlight-depcs 228,7799
(defun proof-highlight-depts 238,8229
(defun proof-dep-unhighlight 249,8703

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table15,492
(defun proof-easy-config-define-derived-modes 22,898
(defun proof-easy-config-check-setup 59,2510
(defmacro proof-easy-config 91,3835

generic/proof.el,543
(deflocal proof-buffer-type 35,900
(defvar proof-shell-busy 38,1013
(defvar proof-included-files-list 43,1169
(defvar proof-script-buffer 66,2185
(defvar proof-previous-script-buffer 70,2325
(defvar proof-shell-buffer 75,2579
(defvar proof-goals-buffer 78,2665
(defvar proof-response-buffer 81,2720
(defvar proof-trace-buffer 84,2781
(defvar proof-thms-buffer 88,2935
(defvar proof-shell-error-or-interrupt-seen 92,3090
(defvar proof-shell-proof-completed 97,3315
(defvar proof-terminal-string 109,3860
(defun unload-pg 123,4064

generic/proof-indent.el,219
(defun proof-indent-indent 13,353
(defun proof-indent-offset 22,619
(defun proof-indent-inner-p 39,1219
(defun proof-indent-goto-prev 48,1526
(defun proof-indent-calculate 55,1859
(defun proof-indent-line 74,2575

generic/proof-maths-menu.el,134
(defun proof-maths-menu-support-available 24,782
(defun proof-maths-menu-set-global 37,1275
(defun proof-maths-menu-enable 51,1731

generic/proof-menu.el,2787
(defvar proof-display-some-buffers-count 21,543
(defun proof-display-some-buffers 23,588
(defun proof-menu-define-keys 82,2790
(define-key map 85,2938
(define-key map 86,2990
(define-key map 87,3041
(define-key map 88,3094
(define-key map 89,3148
(define-key map 90,3210
(define-key map 91,3270
(define-key map 92,3332
(define-key map 95,3505
(define-key map 99,3742
(define-key map 100,3796
(define-key map 101,3861
(define-key map 102,3935
(define-key map 105,4116
(define-key map 106,4182
(define-key map 109,4388
(define-key map 110,4454
(define-key map 112,4569
(define-key map 113,4632
(define-key map 115,4717
(define-key map 122,5043
(define-key map 123,5102
(defun proof-menu-define-main 143,5692
(defun proof-menu-define-specific 153,5893
(defun proof-assistant-menu-update 188,6911
(defvar proof-help-menu205,7519
(defvar proof-show-hide-menu213,7797
(defvar proof-buffer-menu222,8110
(defun proof-keep-response-history 277,10207
(defconst proof-quick-opts-menu285,10517
(defun proof-quick-opts-vars 412,15579
(defun proof-quick-opts-changed-from-defaults-p 437,16330
(defun proof-quick-opts-changed-from-saved-p 441,16435
(defun proof-quick-opts-save 452,16787
(defun proof-quick-opts-reset 457,16955
(defconst proof-config-menu469,17223
(defconst proof-advanced-menu476,17402
(defvar proof-menu 489,17837
(defvar proof-main-menu498,18121
(defvar proof-aux-menu508,18347
(defvar proof-menu-favourites 524,18669
(defun proof-menu-define-favourites-menu 527,18776
(defmacro proof-defshortcut 548,19447
(defmacro proof-definvisible 564,20102
(defun proof-def-favourite 585,20927
(defvar proof-make-favourite-cmd-history 608,21902
(defvar proof-make-favourite-menu-history 611,21987
(defun proof-save-favourites 614,22073
(defun proof-del-favourite 619,22221
(defun proof-read-favourite 636,22782
(defun proof-add-favourite 661,23585
(defvar proof-assistant-settings 688,24636
(defvar proof-menu-settings 695,24999
(defun proof-menu-define-settings-menu 698,25073
(defun proof-menu-entry-name 718,25817
(defun proof-menu-entry-for-setting 730,26289
(defun proof-settings-vars 748,26779
(defun proof-settings-changed-from-defaults-p 753,26956
(defun proof-settings-changed-from-saved-p 757,27062
(defun proof-settings-save 761,27165
(defun proof-settings-reset 766,27332
(defun proof-defpacustom-fn 774,27578
(defmacro defpacustom 850,30462
(defun proof-assistant-invisible-command-ifposs 861,31103
(defun proof-maybe-askprefs 883,32078
(defun proof-assistant-settings-cmd 890,32282
(defun proof-assistant-format 907,32942
(defvar proof-assistant-format-table 931,34001
(defun proof-assistant-format-bool 939,34370
(defun proof-assistant-format-int 942,34483
(defun proof-assistant-format-string 945,34575

generic/proof-mmm.el,113
(defun proof-mmm-support-available 27,933
(defun proof-mmm-set-global 53,1833
(defun proof-mmm-enable 68,2374

generic/proof-script.el,5105
(defvar proof-last-theorem-dependencies 41,1047
(defvar proof-nesting-depth 45,1209
(defvar proof-element-counters 52,1440
(deflocal proof-active-buffer-fake-minor-mode 58,1580
(deflocal proof-script-buffer-file-name 61,1706
(defun proof-next-element-count 75,2230
(defun proof-element-id 84,2557
(defun proof-next-element-id 88,2726
(deflocal proof-script-last-entity 102,3042
(defun proof-script-find-next-entity 109,3322
(deflocal proof-locked-span 185,6064
(deflocal proof-queue-span 192,6330
(defun proof-span-read-only 204,6844
(defun proof-strict-read-only 211,7101
(defsubst proof-set-queue-endpoints 226,7771
(defsubst proof-set-locked-endpoints 230,7912
(defsubst proof-detach-queue 234,8056
(defsubst proof-detach-locked 238,8188
(defsubst proof-set-queue-start 242,8324
(defsubst proof-set-locked-end 246,8450
(defsubst proof-set-queue-end 261,9029
(defun proof-init-segmentation 271,9285
(defun proof-restart-buffers 303,10656
(defun proof-script-buffers-with-spans 325,11578
(defun proof-script-remove-all-spans-and-deactivate 335,11934
(defun proof-script-clear-queue-spans 339,12122
(defun proof-unprocessed-begin 357,12663
(defun proof-script-end 365,12917
(defun proof-queue-or-locked-end 374,13218
(defun proof-locked-end 388,13881
(defun proof-locked-region-full-p 404,14251
(defun proof-locked-region-empty-p 412,14508
(defun proof-only-whitespace-to-locked-region-p 416,14658
(defun proof-in-locked-region-p 429,15294
(defun proof-goto-end-of-locked 441,15557
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 458,16316
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 469,16797
(defun proof-end-of-locked-visible-p 483,17450
(defun proof-goto-end-of-queue-or-locked-if-not-visible 492,17901
(defvar pg-idioms 511,18551
(defvar pg-visibility-specs 514,18647
(deflocal pg-script-portions 519,18854
(defun pg-clear-script-portions 522,18976
(defun pg-add-script-element 536,19505
(defun pg-remove-script-element 539,19581
(defsubst pg-visname 547,19859
(defun pg-add-element 551,20004
(defun pg-open-invisible-span 585,21633
(defun pg-remove-element 596,21996
(defun pg-make-element-invisible 603,22266
(defun pg-make-element-visible 609,22523
(defun pg-toggle-element-visibility 614,22702
(defun pg-redisplay-for-gnuemacs 622,23032
(defun pg-show-all-portions 629,23303
(defun pg-show-all-proofs 647,23974
(defun pg-hide-all-proofs 652,24102
(defun pg-add-proof-element 657,24233
(defun pg-span-name 671,24853
(defun pg-set-span-helphighlights 692,25560
(defun proof-complete-buffer-atomic 717,26384
(defun proof-register-possibly-new-processed-file 758,28299
(defun proof-inform-prover-file-retracted 809,30427
(defun proof-auto-retract-dependencies 828,31213
(defun proof-unregister-buffer-file-name 882,33753
(defun proof-protected-process-or-retract 928,35576
(defun proof-deactivate-scripting-auto 955,36746
(defun proof-deactivate-scripting 964,37104
(defun proof-activate-scripting 1101,42509
(defun proof-toggle-active-scripting 1229,48263
(defun proof-done-advancing 1270,49624
(defun proof-done-advancing-comment 1356,52991
(defun proof-done-advancing-save 1375,53733
(defun proof-make-goalsave 1468,57348
(defun proof-get-name-from-goal 1483,58091
(defun proof-done-advancing-autosave 1502,59117
(defun proof-done-advancing-other 1567,61663
(defun proof-segment-up-to-parser 1595,62622
(defun proof-script-generic-parse-find-comment-end 1658,64698
(defun proof-script-generic-parse-cmdend 1667,65114
(defun proof-script-generic-parse-cmdstart 1692,66009
(defun proof-script-generic-parse-sexp 1755,68717
(defun proof-cmdstart-add-segment-for-cmd 1779,69653
(defun proof-segment-up-to-cmdstart 1831,71852
(defun proof-segment-up-to-cmdend 1892,74212
(defun proof-semis-to-vanillas 1963,76859
(defun proof-script-new-command-advance 2002,78185
(defun proof-script-next-command-advance 2044,79926
(defun proof-assert-until-point-interactive 2056,80367
(defun proof-assert-until-point 2082,81489
(defun proof-assert-next-command2135,83921
(defun proof-goto-point 2183,86184
(defun proof-insert-pbp-command 2200,86710
(defun proof-done-retracting 2233,87823
(defun proof-setup-retract-action 2260,88934
(defun proof-last-goal-or-goalsave 2270,89417
(defun proof-retract-target 2293,90257
(defun proof-retract-until-point-interactive 2378,93898
(defun proof-retract-until-point 2386,94283
(define-derived-mode proof-mode 2431,96144
(defun proof-script-set-visited-file-name 2480,98111
(defun proof-script-set-buffer-hooks 2504,99113
(defun proof-script-kill-buffer-fn 2514,99609
(defun proof-config-done-related 2558,101431
(defun proof-generic-goal-command-p 2630,103999
(defun proof-generic-state-preserving-p 2635,104211
(defun proof-generic-count-undos 2644,104728
(defun proof-generic-find-and-forget 2673,105758
(defconst proof-script-important-settings2724,107583
(defun proof-config-done 2737,108120
(defun proof-setup-parsing-mechanism 2834,111668
(defun proof-setup-imenu 2878,113521
(defun proof-setup-func-menu 2895,114126

generic/proof-shell.el,3390
(defvar proof-shell-last-output 19,457
(defvar proof-marker 63,1713
(defvar proof-action-list 66,1810
(defvar proof-shell-silent 74,1986
(defvar proof-shell-last-prompt 88,2469
(defvar proof-shell-last-output-kind 93,2699
(defvar proof-shell-delayed-output 114,3521
(defvar proof-shell-delayed-output-kind 117,3642
(defcustom proof-shell-active-scripting-indicator126,3845
(defun proof-shell-ready-prover 179,5321
(defun proof-shell-live-buffer 193,5861
(defun proof-shell-available-p 200,6096
(defun proof-grab-lock 206,6319
(defun proof-release-lock 223,7036
(defcustom proof-shell-fiddle-frames 243,7592
(deflocal proof-eagerly-raise 250,7833
(defun proof-shell-set-text-representation 253,7939
(defun proof-shell-start 266,8494
(defvar proof-shell-kill-function-hooks 485,16486
(defun proof-shell-kill-function 488,16584
(defun proof-shell-clear-state 577,20387
(defun proof-shell-exit 592,20830
(defun proof-shell-bail-out 604,21275
(defun proof-shell-restart 613,21752
(defvar proof-shell-no-response-display 655,23136
(defvar proof-shell-urgent-message-marker 658,23240
(defvar proof-shell-urgent-message-scanner 661,23361
(defun proof-shell-handle-output 665,23488
(defun proof-shell-handle-delayed-output 730,26341
(defvar proof-shell-no-error-display 765,27763
(defun proof-shell-handle-error 771,27969
(defun proof-shell-handle-interrupt 789,28805
(defun proof-shell-error-or-interrupt-action 803,29427
(defun proof-goals-pos 830,30632
(defun proof-pbp-focus-on-first-goal 835,30837
(defsubst proof-shell-string-match-safe 847,31372
(defun proof-shell-process-output 852,31540
(defvar proof-shell-insert-space-fudge 963,36180
(defun proof-shell-insert 972,36489
(defun proof-shell-command-queue-item 1046,39401
(defun proof-shell-set-silent 1051,39558
(defun proof-shell-start-silent-item 1057,39777
(defun proof-shell-clear-silent 1063,39969
(defun proof-shell-stop-silent-item 1069,40191
(defun proof-shell-should-be-silent 1076,40463
(defun proof-append-alist 1089,41019
(defun proof-start-queue 1148,43256
(defun proof-extend-queue 1159,43605
(defun proof-shell-exec-loop 1170,43986
(defun proof-shell-insert-loopback-cmd 1235,46574
(defun proof-shell-message 1263,47900
(defun proof-shell-process-urgent-message 1269,48116
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1481,57074
(defun proof-shell-minibuffer-urgent-interactive-input 1483,57144
(defun proof-shell-process-urgent-messages 1495,57514
(defun proof-shell-filter 1568,60685
(defun proof-shell-filter-process-output 1727,67274
(defvar pg-last-tracing-output-time 1780,69328
(defvar pg-tracing-slow-mode 1783,69434
(defconst pg-slow-mode-duration 1786,69523
(defconst pg-fast-tracing-mode-threshold 1789,69605
(defvar pg-tracing-cleanup-timer 1792,69733
(defun pg-tracing-tight-loop 1794,69772
(defun pg-finish-tracing-display 1837,71490
(defun proof-shell-dont-show-annotations 1850,71796
(defun proof-shell-show-annotations 1866,72331
(defun proof-shell-wait 1887,72828
(defun proof-done-invisible 1907,73738
(defun proof-shell-invisible-command 1950,75461
(defun proof-shell-invisible-cmd-get-result 1983,76711
(defun proof-shell-invisible-command-invisible-result 2000,77392
(define-derived-mode proof-shell-mode 2020,77896
(defconst proof-shell-important-settings2091,80567
(defun proof-shell-config-done 2096,80667

generic/proof-site.el,719
(defgroup proof-general 20,594
(defgroup proof-general-internals 32,994
(defun proof-home-directory-fn 43,1234
(defcustom proof-home-directory54,1604
(defcustom proof-images-directory63,1970
(defcustom proof-info-directory69,2171
(defcustom proof-assistant-table98,3420
(defun proof-string-to-list 160,5417
(defcustom proof-assistants 176,5908
(defun proof-ready-for-assistant 212,7321
(defconst proof-general-version 325,11540
(defconst proof-general-short-version 328,11681
(defconst proof-general-version-year 333,11841
(defcustom proof-assistant-cusgrp 347,12309
(defcustom proof-assistant-internals-cusgrp 355,12612
(defcustom proof-assistant 363,12924
(defcustom proof-assistant-symbol 371,13193

generic/proof-splash.el,727
(defcustom proof-splash-enable 16,433
(defcustom proof-splash-time 21,585
(defcustom proof-splash-contents29,870
(defconst proof-splash-startup-msg 58,1985
(defconst proof-splash-welcome 67,2364
(defun proof-get-image 85,2900
(defvar proof-splash-timeout-conf 125,4263
(defun proof-splash-centre-spaces 128,4376
(defun proof-splash-remove-screen 156,5545
(defun proof-splash-remove-buffer 176,6271
(defvar proof-splash-seen 192,6935
(defun proof-splash-display-screen 196,7052
(defun proof-splash-message 271,10211
(defun proof-splash-timeout-waiter 281,10574
(defvar proof-splash-old-frame-title-format 298,11313
(defun proof-splash-set-frame-titles 300,11363
(defun proof-splash-unset-frame-titles 309,11679

generic/proof-syntax.el,972
(defun proof-ids-to-regexp 16,445
(defun proof-anchor-regexp 22,701
(defconst proof-no-regexp26,803
(defun proof-regexp-alt 31,898
(defun proof-regexp-region 40,1184
(defun proof-re-search-forward-region 49,1607
(defun proof-search-forward 62,2102
(defun proof-replace-regexp-in-string 68,2354
(defun proof-re-search-forward 74,2608
(defun proof-re-search-backward 80,2869
(defun proof-string-match 86,3133
(defun proof-string-match-safe 92,3365
(defun proof-stringfn-match 96,3570
(defun proof-looking-at 103,3830
(defun proof-looking-at-safe 109,4020
(defun proof-looking-at-syntactic-context 113,4160
(defun proof-replace-string 125,4523
(defun proof-replace-regexp 130,4724
(defun proof-replace-regexp-nocasefold 135,4930
(defvar proof-id 143,5209
(defun proof-ids 149,5429
(defun proof-zap-commas 162,5990
(defun proof-format 180,6559
(defun proof-format-filename 199,7198
(defun proof-insert 248,8676
(defun proof-splice-separator 284,9685

generic/proof-toolbar.el,2877
(defun proof-toolbar-function 49,1595
(defun proof-toolbar-icon 52,1692
(defun proof-toolbar-enabler 55,1793
(defun proof-toolbar-function-with-enabler 58,1901
(defun proof-toolbar-make-icon 65,2074
(defun proof-toolbar-make-toolbar-item 83,2674
(defvar proof-toolbar 122,4055
(deflocal proof-toolbar-itimer 126,4184
(defun proof-toolbar-setup 130,4294
(defun proof-toolbar-build 174,5861
(defalias 'proof-toolbar-enable proof-toolbar-enable
239,8074
(defun proof-toolbar-setup-refresh 248,8313
(defun proof-toolbar-disable-refresh 269,9083
(deflocal proof-toolbar-refresh-flag 276,9405
(defun proof-toolbar-refresh 282,9676
(defvar proof-toolbar-enablers286,9821
(defvar proof-toolbar-enablers-last-state292,9997
(defun proof-toolbar-really-refresh 296,10088
(defun proof-toolbar-undo-enable-p 349,11918
(defalias 'proof-toolbar-undo proof-toolbar-undo
354,12066
(defun proof-toolbar-delete-enable-p 360,12185
(defalias 'proof-toolbar-delete proof-toolbar-delete
366,12359
(defun proof-toolbar-lockedend-enable-p 373,12495
(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
376,12545
(defun proof-toolbar-next-enable-p 385,12633
(defalias 'proof-toolbar-next proof-toolbar-next
389,12740
(defun proof-toolbar-goto-enable-p 396,12834
(defalias 'proof-toolbar-goto proof-toolbar-goto
399,12907
(defun proof-toolbar-retract-enable-p 406,12983
(defalias 'proof-toolbar-retract proof-toolbar-retract
410,13094
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
417,13173
(defalias 'proof-toolbar-use proof-toolbar-use
418,13241
(defun proof-toolbar-restart-enable-p 424,13319
(defalias 'proof-toolbar-restart proof-toolbar-restart
429,13480
(defun proof-toolbar-goal-enable-p 435,13558
(defalias 'proof-toolbar-goal proof-toolbar-goal
442,13791
(defun proof-toolbar-qed-enable-p 449,13863
(defalias 'proof-toolbar-qed proof-toolbar-qed
455,14015
(defun proof-toolbar-state-enable-p 461,14087
(defalias 'proof-toolbar-state proof-toolbar-state
464,14158
(defun proof-toolbar-context-enable-p 470,14227
(defalias 'proof-toolbar-context proof-toolbar-context
473,14300
(defun proof-toolbar-info-enable-p 481,14460
(defalias 'proof-toolbar-info proof-toolbar-info
484,14504
(defun proof-toolbar-command-enable-p 490,14573
(defalias 'proof-toolbar-command proof-toolbar-command
493,14644
(defun proof-toolbar-help-enable-p 499,14724
(defun proof-toolbar-help 502,14769
(defun proof-toolbar-find-enable-p 510,14863
(defalias 'proof-toolbar-find proof-toolbar-find
513,14932
(defun proof-toolbar-visibility-enable-p 519,15030
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
522,15130
(defun proof-toolbar-interrupt-enable-p 528,15218
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
531,15282
(defun proof-toolbar-make-menu-item 540,15471
(defconst proof-toolbar-scripting-menu562,16159

generic/proof-utils.el,2102
(defmacro deflocal 19,531
(defmacro proof-with-current-buffer-if-exists 26,769
(defmacro proof-with-script-buffer 35,1146
(defmacro proof-map-buffers 46,1533
(defmacro proof-sym 51,1718
(defun proof-try-require 56,1879
(defmacro proof-face-specs 63,2073
(defun proof-save-some-buffers 85,2728
(defun proof-set-value 109,3419
(defun proof-ass-symv 169,5596
(defmacro proof-ass-sym 174,5783
(defun proof-defpgcustom-fn 178,5922
(defun undefpgcustom 203,7006
(defmacro defpgcustom 209,7230
(defmacro proof-ass 218,7647
(defun proof-defpgdefault-fn 223,7823
(defmacro defpgdefault 237,8282
(defmacro defpgfun 248,8644
(defun proof-file-truename 263,8938
(defun proof-file-to-buffer 267,9121
(defun proof-files-to-buffers 278,9450
(defun proof-buffers-in-mode 285,9733
(defun pg-save-from-death 299,10184
(defun proof-define-keys 318,10802
(deflocal proof-font-lock-keywords 347,11803
(deflocal proof-font-lock-keywords-case-fold-search 353,12068
(defun proof-font-lock-configure-defaults 356,12191
(defun proof-font-lock-clear-font-lock-vars 404,14504
(defun proof-font-lock-set-font-lock-vars 415,14877
(defun proof-fontify-region 422,15090
(defun pg-remove-specials 480,17318
(defun pg-remove-specials-in-string 490,17657
(defun proof-fontify-buffer 497,17844
(defun proof-warn-if-unset 510,18085
(defun proof-get-window-for-buffer 515,18303
(defun proof-display-and-keep-buffer 566,20617
(defun proof-clean-buffer 598,21926
(defun proof-message 613,22547
(defun proof-warning 618,22760
(defun pg-internal-warning 624,23042
(defun proof-debug 632,23361
(defun proof-switch-to-buffer 647,24032
(defun proof-resize-window-tofit 680,25724
(defun proof-submit-bug-report 780,29736
(defun proof-deftoggle-fn 816,31124
(defmacro proof-deftoggle 831,31779
(defun proof-defintset-fn 838,32153
(defmacro proof-defintset 854,32861
(defun proof-defstringset-fn 861,33238
(defmacro proof-defstringset 874,33865
(defun pg-custom-save-vars 888,34330
(defun pg-custom-reset-vars 906,35056
(defun proof-locate-executable 919,35393
(defconst proof-extra-fls948,36574

generic/proof-x-symbol.el,653
(defpgcustom x-symbol-language 52,2063
(defvar proof-x-symbol-initialized 57,2285
(defun proof-x-symbol-tokenlang-file 60,2380
(defun proof-x-symbol-support-maybe-available 66,2562
(defun proof-x-symbol-initialize 86,3312
(defun proof-x-symbol-enable 177,6973
(defun proof-x-symbol-refresh-output-buffers 207,8290
(defun proof-x-symbol-mode-associated-buffers 222,9044
(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
244,9748
(defun proof-x-symbol-encode-shell-input 246,9814
(defun proof-x-symbol-set-language 263,10405
(defun proof-x-symbol-shell-config 268,10576
(defun proof-x-symbol-config-output-buffer 316,12743

lib/bufhist.el,1099
(defun bufhist-ring-update 32,1226
(defgroup bufhist 41,1548
(defcustom bufhist-ring-size 45,1629
(defvar bufhist-ring 50,1740
(defvar bufhist-ring-pos 53,1814
(defvar bufhist-lastswitch-modified-tick 56,1893
(defvar bufhist-read-only-history 59,1999
(defvar bufhist-saved-mode-line-format 62,2070
(defun bufhist-mode-line-format-entry 65,2171
(defun bufhist-get-buffer-contents 97,3443
(defun bufhist-restore-buffer-contents 109,3927
(defun bufhist-checkpoint 117,4214
(defun bufhist-erase-buffer 125,4583
(defun bufhist-checkpoint-and-erase 135,4928
(defun bufhist-switch-to-index 141,5114
(defun bufhist-first 180,6718
(defun bufhist-last 185,6877
(defun bufhist-prev 190,7023
(defun bufhist-next 198,7246
(defun bufhist-delete 203,7386
(defun bufhist-clear 215,7929
(defun bufhist-init 230,8325
(defun bufhist-exit 255,9262
(defun bufhist-set-readwrite 265,9526
(defun bufhist-before-change-function 280,10146
(defun bufhist-make-buttons 292,10562
(defconst bufhist-minor-mode-map310,11001
(define-minor-mode bufhist-mode322,11463
(defun bufhist-toggle-fn 342,12248

lib/holes.el,2447
(defvar holes-doc 35,993
(defvar holes-default-hole 143,4976
(defvar holes-active-hole 147,5145
(defcustom holes-empty-hole-string 154,5354
(defcustom holes-empty-hole-regexp 157,5465
(defcustom holes-search-limit 164,5756
(defface active-hole-face176,6132
(defface inactive-hole-face188,6580
(defun holes-region-beginning-or-nil 203,7056
(defun holes-region-end-or-nil 208,7166
(defun holes-copy-active-region 213,7264
(defun holes-is-hole-p 220,7463
(defun holes-hole-start-position 226,7570
(defun holes-hole-end-position 233,7759
(defun holes-hole-buffer 240,7943
(defun holes-hole-at 247,8118
(defun holes-active-hole-exist-p 254,8293
(defun holes-active-hole-start-position 264,8551
(defun holes-active-hole-end-position 274,8923
(defun holes-active-hole-buffer 285,9292
(defun holes-goto-active-hole 296,9598
(defun holes-highlight-hole-as-active 308,9866
(defun holes-highlight-hole 318,10178
(defun holes-disable-active-hole 329,10470
(defun holes-set-active-hole 347,11013
(defun holes-is-in-hole-p 360,11359
(defun holes-make-hole 367,11502
(defun holes-make-hole-at 393,12248
(defun holes-clear-hole 413,12724
(defun holes-clear-hole-at 425,13013
(defun holes-map-holes 434,13272
(defun holes-mapcar-holes 442,13455
(defun holes-clear-all-buffer-holes 448,13622
(defun holes-next 459,13922
(defun holes-next-after-active-hole 466,14173
(defun holes-set-active-hole-next 474,14392
(defun holes-replace-segment 496,14945
(defun holes-replace 506,15299
(defun holes-replace-active-hole 537,16494
(defun holes-replace-update-active-hole 546,16795
(defun holes-delete-update-active-hole 567,17485
(defun holes-set-make-active-hole 574,17699
(defun holes-mouse-replace-active-hole 621,19327
(defun holes-destroy-hole 641,19866
(defun holes-hole-at-event 658,20277
(defun holes-mouse-destroy-hole 663,20390
(defun holes-mouse-forget-hole 673,20630
(defun holes-mouse-set-make-active-hole 689,20940
(defun holes-mouse-set-active-hole 711,21501
(defun holes-set-point-next-hole-destroy 723,21765
(defvar hole-map739,22215
(defvar holes-mode-map755,22835
(defun holes-replace-string-by-holes-backward 792,24300
(defun holes-skeleton-end-hook 810,25001
(defconst holes-jump-doc 819,25410
(defun holes-replace-string-by-holes-backward-jump 826,25617
(defun holes-abbrev-complete 843,26248
(defun holes-insert-and-expand 852,26555
(defvar holes-mode 863,26987
(defun holes-mode 869,27183

lib/local-vars-list.el,372
(defconst local-vars-list-doc 25,759
(defun local-vars-list-insert-empty-zone 41,1323
(defun local-vars-list-find 79,2031
(defun local-vars-list-goto-var 98,2806
(defun local-vars-list-get-current 124,3856
(defun local-vars-list-set-current 145,4706
(defun local-vars-list-get 168,5423
(defun local-vars-list-get-safe 185,5955
(defun local-vars-list-set 190,6149

lib/maths-menu.el,153
(defun maths-menu-build-menu 48,2022
(defvar maths-menu-menu67,2690
(defvar maths-menu-mode-map312,11648
(define-minor-mode maths-menu-mode337,12521

lib/proof-compat.el,1003
(defvar proof-running-on-XEmacs 25,818
(defvar proof-running-on-Emacs21 27,940
(defvar proof-running-on-win32 31,1187
(defun pg-custom-undeclare-variable 43,1621
(defun pg-window-system 118,4103
(defconst pg-defface-window-systems 127,4474
(defun subst-char-in-string 151,5191
(defun replace-regexp-in-string 165,5745
(defconst menuvisiblep 227,8458
(defun set-window-text-height 244,9077
(defmacro save-selected-frame 270,10027
(defun warn 309,11329
(defun redraw-modeline 316,11584
(defun replace-in-string 331,12151
(defun proof-buffer-syntactic-context-emulate 380,13669
(defvar read-shell-command-map413,14976
(defun read-shell-command 431,15678
(defun remassq 443,16159
(defun remassoc 455,16548
(defun frames-of-buffer 468,16993
(defmacro with-selected-window 507,18255
(defun pg-pop-to-buffer 550,19644
(defun process-live-p 601,21496
(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
618,21999
(defun select-buffers-tab-buffers-by-mode 662,23347

lib/span.el,132
(defsubst delete-spans 24,499
(defsubst span-property-safe 28,653
(defsubst set-span-start 32,792
(defsubst set-span-end 36,924

lib/span-extent.el,968
(defsubst make-span 12,367
(defsubst detach-span 16,489
(defsubst set-span-endpoints 20,576
(defsubst set-span-property 24,709
(defsubst span-read-only 28,836
(defsubst span-read-write 32,940
(defun span-give-warning 36,1047
(defun span-write-warning 40,1155
(defsubst span-property 45,1355
(defsubst delete-span 49,1470
(defsubst mapcar-spans 55,1641
(defsubst span-at 59,1847
(defsubst span-at-before 63,1964
(defsubst span-start 68,2161
(defsubst span-end 72,2290
(defsubst prev-span 76,2413
(defsubst next-span 80,2559
(defsubst span-live-p 84,2701
(defun span-raise 92,2973
(defalias 'span-object span-object
96,3072
(defalias 'span-string span-string
97,3111
(defsubst make-detached-span 100,3197
(defsubst span-buffer 105,3259
(defsubst span-detached-p 110,3351
(defsubst set-span-face 115,3463
(defsubst fold-spans 119,3558
(defsubst set-span-properties 123,3755
(defsubst set-span-keymap 127,3863
(defsubst span-at-event 132,4007

lib/span-overlay.el,1201
(defalias 'span-start span-start
12,370
(defalias 'span-end span-end
13,408
(defalias 'set-span-property set-span-property
14,442
(defalias 'span-property span-property
15,485
(defalias 'make-span make-span
16,524
(defalias 'detach-span detach-span
17,560
(defalias 'set-span-endpoints set-span-endpoints
18,600
(defalias 'span-buffer span-buffer
19,645
(defun span-read-only-hook 21,686
(defun span-read-only 25,818
(defun span-read-write 40,1594
(defun span-give-warning 46,1813
(defun span-write-warning 50,1921
(defun span-lt 57,2247
(defun spans-at-point-prop 62,2388
(defun spans-at-region-prop 68,2553
(defun span-at 76,2797
(defsubst delete-span 82,3011
(defsubst mapcar-spans 89,3233
(defun span-at-before 93,3437
(defun prev-span 110,4163
(defun next-span 116,4314
(defsubst span-live-p 145,5539
(defun span-raise 151,5705
(defalias 'span-object span-object
157,5948
(defun span-string 159,5989
(defun set-span-properties 165,6171
(defun span-find-span 177,6426
(defsubst span-at-event 184,6733
(defun make-detached-span 189,6857
(defun fold-spans 194,6953
(defsubst span-detached-p 209,7487
(defsubst set-span-face 213,7602
(defun set-span-keymap 217,7699

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 85,2997
(defun texi-docstring-magic-splice-sep 90,3162
(defconst texi-docstring-magic-munge-table100,3467
(defun texi-docstring-magic-untabify 190,7187
(defun texi-docstring-magic-munge-docstring 200,7502
(defun texi-docstring-magic-texi 239,8789
(defun texi-docstring-magic-format-default 252,9229
(defun texi-docstring-magic-texi-for 268,9864
(defconst texi-docstring-magic-comment326,11824
(defun texi-docstring-magic 332,11978
(defun texi-docstring-magic-face-at-point 366,13058
(defun texi-docstring-magic-insert-magic 381,13581

lib/unichars.el,35
(defvar unicode-character-list1,0

lib/xml-fixed.el,528
(defsubst xml-node-name 82,2904
(defsubst xml-node-attributes 87,3023
(defsubst xml-node-children 92,3141
(defun xml-get-children 97,3277
(defun xml-get-attribute 107,3600
(defun xml-parse-file 123,4064
(defun xml-parse-region 144,4648
(defun xml-parse-tag 179,5693
(defun xml-parse-attlist 284,9162
(defun xml-skip-dtd 321,10552
(defun xml-parse-dtd 338,11188
(defun xml-parse-elem-type 408,13266
(defun xml-substitute-special 449,14421
(defun xml-debug-print 470,15228
(defun xml-debug-print-internal 474,15320

lib/xmlunicode.el,1499
(defvar unicode-ldquo 128,5364
(defvar unicode-rdquo 129,5416
(defvar unicode-lsquo 130,5468
(defvar unicode-rsquo 131,5520
(defvar unicode-quot 132,5572
(defvar unicode-apos 133,5624
(defvar unicode-capos 134,5676
(defvar unicode-ndash 135,5728
(defvar unicode-mdash 136,5780
(defvar unicode-hellip 137,5832
(defvar unicode-charref-format 139,5885
(defvar xml-tag-search-limit 142,5975
(defvar unicode-character-list-file 145,6078
(defvar unicode-character-alist 151,6364
(defvar iso8879-character-alist 163,6744
(defun iso8879-to-codepoints 178,7237
(defun unicode-to-codepoints 188,7652
(defvar unicode-glyph-list198,8069
(defun unicode-character-insert 269,12058
(defun iso8879-character-insert 287,12974
(defun xml-unicode-insert 302,13825
(defvar unicode-character-menu-alist324,14474
(defun  unicode-character-menu-insert 362,15486
(defvar unicode-character-menu-map 370,15785
(defun make-unicode-character-menu-bar 373,15902
(defun in-start-tag 389,16503
(defun after-start-tag 406,16930
(defun in-comment 423,17409
(defun unicode-looking-backward-at 441,17905
(defun unicode-smart-double-quote 454,18377
(defun unicode-smart-single-quote 498,19687
(defun unicode-smart-hyphen 536,20905
(defun unicode-smart-period 559,21477
(defun unicode-smart-semicolon 582,22084
(defvar xml-quail-define-rules 631,23451
(defvar unicode-character-shortcut-alist669,24777
(defun unicode-character-shortcut-insert 758,30273
(defun show-unicode-character-list 770,30690

mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2675
(defun mmm-autoload-class 89,3438
(defvar mmm-changed-buffers-list 129,5005
(defun mmm-major-mode-change 132,5112
(defun mmm-check-changed-buffers 145,5633
(defun mmm-mode-on-maybe 155,6006
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6424
(defun mmm-add-find-file-hook 168,6484

mmm/mmm-class.el,416
(defun mmm-get-class-spec 42,1295
(defun mmm-get-class-parameter 59,2008
(defun mmm-set-class-parameter 63,2174
(defun* mmm-apply-class75,2538
(defun* mmm-apply-classes90,3176
(defun* mmm-apply-all 110,3942
(defun* mmm-ify124,4389
(defun* mmm-match-region206,7472
(defun mmm-match->point 267,10161
(defun mmm-match-and-verify 281,10683
(defun mmm-get-form 307,11741
(defun mmm-default-get-form 318,12237

mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1209
(defun mmm-ify-region 63,1933
(defun mmm-ify-by-regexp75,2361
(defun mmm-parse-buffer 97,3037
(defun mmm-parse-region 106,3373
(defun mmm-parse-block 115,3752
(defun mmm-get-block 132,4503
(defun mmm-reparse-current-region 146,4834
(defun mmm-clear-current-region 167,5508
(defun mmm-clear-regions 172,5672
(defun mmm-clear-all-regions 177,5818
(defun* mmm-end-current-region 185,5978
(defun mmm-narrow-to-submode-region 220,7401
(defun mmm-insert-region 239,8015
(defun mmm-insert-by-key 258,8877
(defun mmm-get-insertion-spec 342,12437
(defun mmm-insertion-help 369,13516
(defun mmm-display-insertion-key 379,13886
(defun mmm-get-all-insertion-keys 401,14708

mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1312
(defvar mmm-keywords-used49,1615
(defmacro mmm-regexp-opt 90,2612
(defvar mmm-evaporate-property109,3261
(defmacro mmm-set-keymap-default 127,4027
(defmacro mmm-event-key 136,4469
(defvar skeleton-positions 145,4688
(defun mmm-fixup-skeleton 146,4719
(defmacro mmm-make-temp-buffer 158,5156
(defvar mmm-font-lock-available-p 171,5552
(defmacro mmm-set-font-lock-defaults 178,5766

mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1116
(defvar mmm-cweb-section-regexp41,1163
(defvar mmm-cweb-c-part-tags44,1253
(defvar mmm-cweb-c-part-regexp47,1312
(defun mmm-cweb-in-limbo 50,1396
(defun mmm-cweb-verify-brief-c 57,1621

mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1235
(defvar mmm-mason-pseudo-perl-tags45,1376
(defvar mmm-mason-non-perl-tags48,1452
(defvar mmm-mason-perl-tags-regexp51,1553
(defvar mmm-mason-pseudo-perl-tags-regexp56,1748
(defvar mmm-mason-tag-names-regexp61,1965
(defun mmm-mason-verify-inline 66,2185
(defun mmm-mason-start-line 156,5089
(defun mmm-mason-end-line 161,5154
(defun mmm-mason-set-mode-line 168,5248

mmm/mmm-mode.el,1024
(defun mmm-mode 101,3866
(defun mmm-mode-on 140,5371
(defun mmm-mode-off 181,7131
(defvar mmm-mode-map 206,7864
(defvar mmm-mode-prefix-map 209,7939
(defvar mmm-mode-menu-map 212,8049
(defun mmm-define-key 215,8140
(define-key mmm-mode-prefix-map 239,8895
(define-key mmm-mode-prefix-map 246,9153
(define-key mmm-mode-map 249,9264
(define-key mmm-mode-menu-map 252,9366
(define-key mmm-mode-menu-map 254,9438
(define-key mmm-mode-menu-map 256,9497
(define-key mmm-mode-menu-map 258,9578
(define-key mmm-mode-menu-map 260,9659
(define-key mmm-mode-menu-map 262,9746
(define-key mmm-mode-menu-map 265,9840
(define-key mmm-mode-menu-map 267,9900
(define-key mmm-mode-menu-map 270,9991
(define-key mmm-mode-menu-map 272,10051
(define-key mmm-mode-menu-map 274,10158
(define-key mmm-mode-menu-map 276,10243
(define-key mmm-mode-menu-map 279,10329
(define-key mmm-mode-menu-map 281,10389
(define-key mmm-mode-menu-map 283,10502
(define-key mmm-mode-menu-map 285,10587
(define-key mmm-mode-map 288,10670

mmm/mmm-noweb.el,1291
(defvar mmm-noweb-code-mode 44,1352
(defvar mmm-noweb-quote-mode 50,1649
(defvar mmm-noweb-quote-string 54,1806
(defvar mmm-noweb-quote-number 58,1929
(defvar mmm-noweb-narrowing 62,2045
(defun mmm-noweb-chunk 68,2176
(defun mmm-noweb-quote 84,2876
(defun mmm-noweb-quote-name 89,3042
(defun mmm-noweb-chunk-name 95,3302
(defun mmm-noweb-regions 140,4748
(defun mmm-noweb-narrow-to-doc-chunk 166,5616
(defun mmm-noweb-fill-chunk 189,6386
(defun mmm-noweb-fill-paragraph-chunk 208,7070
(defun mmm-noweb-fill-named-chunk 222,7487
(defun mmm-noweb-auto-fill-doc-chunk 238,8064
(defun mmm-noweb-auto-fill-doc-mode 246,8283
(defun mmm-noweb-auto-fill-code-mode 251,8473
(defun mmm-noweb-complete-chunk 259,8685
(defvar mmm-noweb-chunk-history 292,9689
(defun mmm-noweb-goto-chunk 295,9767
(defun mmm-noweb-goto-next 307,10091
(defun mmm-noweb-goto-previous 319,10448
(defvar mmm-noweb-map 336,10852
(defvar mmm-noweb-prefix-map 337,10896
(define-key mmm-noweb-map 338,10947
(define-key mmm-noweb-prefix-map 347,11390
(defun mmm-noweb-bind-keys 352,11656
(defun mmm-syntax-region-list 368,12070
(defun mmm-syntax-other-regions 377,12426
(defun mmm-word-other-regions 389,12897
(defun mmm-space-other-regions 395,13066
(defun mmm-undo-syntax-other-regions 401,13237

mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1748
(defun mmm-overlays-at 59,1933
(defun mmm-included-p 72,2386
(defun mmm-overlays-containing 112,3875
(defun mmm-overlays-contained-in 125,4313
(defun mmm-overlays-overlapping 138,4753
(defun mmm-sort-overlays 149,5116
(defvar mmm-current-overlay 158,5386
(defvar mmm-previous-overlay 163,5601
(defvar mmm-current-submode 168,5789
(defvar mmm-previous-submode 173,5989
(defun mmm-update-current-submode 178,6162
(defun mmm-set-current-submode 199,6978
(defun mmm-submode-at 210,7470
(defun mmm-match-front 219,7745
(defun mmm-match-back 238,8506
(defun mmm-front-start 257,9251
(defun mmm-back-end 265,9555
(defun mmm-valid-submode-region 278,9902
(defun* mmm-make-region305,11058
(defun mmm-make-overlay 431,16429
(defun mmm-get-face 459,17562
(defun mmm-clear-overlays 470,17854
(defun mmm-update-mode-info 486,18321
(defun mmm-update-submode-region 571,22606
(defun mmm-add-hooks 588,23364
(defun mmm-remove-hooks 592,23499
(defun mmm-get-local-variables-list 598,23626
(defun mmm-get-locals 618,24546
(defun mmm-get-saved-local 631,25127
(defun mmm-set-local-variables 635,25292
(defun mmm-get-saved-local-variables 646,25733
(defun mmm-save-changed-local-variables 654,26050
(defun mmm-clear-local-variables 673,26908
(defun mmm-enable-font-lock 684,27187
(defun mmm-update-font-lock-buffer 692,27447
(defun mmm-refontify-maybe 705,27879
(defun mmm-submode-changes-in 720,28401
(defun mmm-regions-in 731,28849
(defun mmm-regions-alist 745,29419
(defun mmm-fontify-region 762,30065
(defun mmm-fontify-region-list 782,31096
(defun mmm-beginning-of-syntax 804,32012

mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1617
(defvar mmm-rpm-sh-end-tags53,1841
(defvar mmm-rpm-sh-start-regexp57,2015
(defvar mmm-rpm-sh-end-regexp61,2193

mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2614
(defun mmm-here-doc-get-mode 93,3099
(defun mmm-file-variables-verify 208,6817
(defun mmm-file-variables-find-back 232,7853

mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 41,1309
(defmacro mmm-save-all 60,1953
(defun mmm-format-string 73,2242
(defun mmm-format-matches 84,2694
(defmacro mmm-save-keyword 107,3487
(defmacro mmm-save-keywords 115,3814
(defun mmm-looking-back-at 128,4347
(defun mmm-make-marker 145,4915

mmm/mmm-vars.el,2667
(defgroup mmm 99,3072
(defvar mmm-c-derived-modes106,3182
(defvar mmm-save-local-variables 110,3301
(defvar mmm-buffer-saved-locals 336,10161
(defvar mmm-region-saved-locals-defaults 341,10361
(defvar mmm-region-saved-locals-for-dominant 347,10621
(defgroup mmm-faces 357,10998
(defcustom mmm-submode-decoration-level 363,11169
(defface mmm-init-submode-face 381,12041
(defface mmm-cleanup-submode-face 385,12181
(defface mmm-declaration-submode-face 389,12318
(defface mmm-comment-submode-face 393,12464
(defface mmm-output-submode-face 397,12617
(defface mmm-special-submode-face 401,12766
(defface mmm-code-submode-face 405,12930
(defface mmm-default-submode-face 409,13069
(defface mmm-delimiter-face 414,13277
(defcustom mmm-mode-string 421,13403
(defcustom mmm-submode-mode-line-format 426,13534
(defvar mmm-primary-mode-display-name 443,14189
(defvar mmm-buffer-mode-display-name 448,14403
(defun mmm-set-mode-line 454,14702
(defvar mmm-classes 478,15510
(defvar mmm-global-classes 484,15755
(defcustom mmm-mode-ext-classes-alist 491,15937
(defun mmm-add-mode-ext-class 510,16755
(defcustom mmm-major-mode-preferences519,17080
(defun mmm-add-to-major-mode-preferences 537,17878
(defun mmm-ensure-modename 553,18664
(defun mmm-modename->function 562,18974
(defcustom mmm-delimiter-mode 576,19437
(defcustom mmm-mode-prefix-key 586,19706
(defcustom mmm-command-modifiers 591,19833
(defcustom mmm-insert-modifiers 605,20466
(defcustom mmm-use-old-command-keys 620,21144
(defun mmm-use-old-command-keys 630,21608
(defcustom mmm-mode-hook 638,21807
(defun mmm-run-constructed-hook 658,22614
(defun mmm-run-major-hook 666,23000
(defun mmm-run-submode-hook 669,23077
(defvar mmm-class-hooks-run 672,23164
(defun mmm-run-class-hook 677,23336
(defvar mmm-primary-mode-entry-hook 682,23508
(defcustom mmm-major-mode-hook 697,24155
(defun mmm-run-major-mode-hook 711,24786
(defcustom mmm-global-mode 724,25327
(defcustom mmm-never-modes740,26022
(defvar mmm-set-file-name-for-modes 758,26322
(defvar mmm-mode 769,26681
(defvar mmm-primary-mode 777,26889
(defvar mmm-classes-alist 788,27255
(defun mmm-add-classes 943,35462
(defun mmm-add-group 948,35627
(defun mmm-add-to-group 958,36077
(defconst mmm-version 972,36574
(defun mmm-version 975,36639
(defvar mmm-temp-buffer-name 982,36782
(defvar mmm-interactive-history 988,36912
(defun mmm-add-to-history 994,37181
(defun mmm-clear-history 997,37264
(defvar mmm-mode-ext-classes 1005,37449
(defun mmm-get-mode-ext-classes 1010,37660
(defun mmm-clear-mode-ext-classes 1019,38036
(defun mmm-mode-ext-applies 1023,38161
(defun mmm-get-all-classes 1037,38645

x-symbol/lisp/auto-autoloads.el,63
(defalias 'x-symbol-map-autoload x-symbol-map-autoload
23,974

x-symbol/lisp/x-symbol-bib.el,549
(defcustom x-symbol-bib-auto-style 42,1544
(defcustom x-symbol-bib-modeline-name 49,1800
(defcustom x-symbol-bib-header-groups-alist 55,1979
(defcustom x-symbol-bib-electric-ignore 62,2268
(defcustom x-symbol-bib-class-alist 69,2558
(defcustom x-symbol-bib-class-face-alist 76,2824
(defvar x-symbol-bib-token-grammar89,3308
(defvar x-symbol-bib-required-fonts 99,3784
(defvar x-symbol-bib-user-table 103,3960
(defvar x-symbol-bib-table106,4064
(defvar x-symbol-bib-generated-data 113,4390
(defun x-symbol-bib-default-token-list 117,4529

x-symbol/lisp/x-symbol.el,9173
(defvar x-symbol-trace-invisible 51,1979
(defconst x-symbol-language-access-alist66,2494
(defstruct (x-symbol-generated178,8375
(defstruct (x-symbol-grammar189,8587
(defvar x-symbol-map 212,9415
(defvar x-symbol-unalias-alist 216,9542
(defvar x-symbol-latin-decode-alists 220,9659
(defvar x-symbol-context-atree 224,9844
(defvar x-symbol-electric-atree 228,9959
(defvar x-symbol-grid-alist 231,10053
(defvar x-symbol-menu-alist 234,10136
(defvar x-symbol-all-charsyms 237,10243
(defvar x-symbol-fancy-value-cache 242,10451
(defvar x-symbol-fchar-tables 246,10614
(defvar x-symbol-bchar-tables 249,10743
(defvar x-symbol-cstring-table 251,10779
(defvar x-symbol-fontified-cstring-table 253,10816
(defvar x-symbol-charsym-decode-obarray 255,10863
(defun x-symbol-set-variable 262,11092
(defun x-symbol-ensure-hashtable 276,11727
(defun x-symbol-puthash 283,12029
(defun x-symbol-call-function-or-regexp 291,12358
(defun x-symbol-match-in-alist 300,12758
(defun x-symbol-fancy-string 329,13982
(defun x-symbol-fancy-value 351,14899
(defun x-symbol-fancy-associations 370,15666
(defun x-symbol-language-value 399,16818
(defun x-symbol-charsym-face 413,17476
(defun x-symbol-image-available-p 426,18103
(defun x-symbol-default-context-info-ignore 431,18315
(defun x-symbol-default-info-keys-keymaps 445,19082
(defun x-symbol-alias-charsym 457,19557
(defun x-symbol-default-valid-charsym 466,19926
(defun x-symbol-next-valid-charsym 488,20963
(defun x-symbol-valid-context-charsym 515,21970
(defun x-symbol-next-valid-charsym-before 526,22569
(defun x-symbol-prefix-arg-texts 550,23626
(defun x-symbol-region-text 559,23921
(defun x-symbol-language-text 568,24217
(defun x-symbol-coding-text 576,24617
(defun x-symbol-language-modeline-text 594,25312
(defun x-symbol-coding-modeline-text 600,25548
(defun x-symbol-translate-to-ascii 646,27453
(defun x-symbol-package-web 680,28718
(defun x-symbol-package-info 687,28939
(defun x-symbol-package-bug 693,29100
(defun x-symbol-package-reply-to-report 744,31073
(defvar x-symbol-encode-rchars 764,31801
(defun x-symbol-even-escapes-before-p 772,32083
(defun x-symbol-decode-region 780,32262
(defun x-symbol-decode-all 793,32735
(defun x-symbol-decode-single-token 856,35803
(defun x-symbol-decode-lisp 865,36110
(defun x-symbol-encode-string 897,37577
(defun x-symbol-encode-all 908,37896
(defun x-symbol-encode-lisp 970,40852
(defun x-symbol-decode-recode 1006,42257
(defun x-symbol-decode 1036,43633
(defun x-symbol-encode-recode 1049,44224
(defun x-symbol-encode 1077,45500
(defun x-symbol-unalias 1093,46259
(defun x-symbol-copy-region-encoded 1158,49178
(defun x-symbol-yank-decoded 1186,50428
(defun x-symbol-update-modeline 1213,51528
(defun x-symbol-auto-coding-alist 1237,52383
(defun x-symbol-auto-8bit-search 1273,53544
(defvar x-symbol-font-family-postfixes1298,54334
(defvar x-symbol-font-lock-property-alist1301,54450
(defvar x-symbol-font-lock-keywords1305,54631
(defvar x-symbol-subscript-matcher 1332,55626
(defvar x-symbol-subscript-type 1336,55729
(defun x-symbol-subscripts-available-p 1339,55780
(defun x-symbol-font-lock-start 1345,56021
(defun x-symbol-match-subscript 1354,56407
(defun x-symbol-init-font-lock 1360,56620
(defun x-symbol-set-image 1392,58208
(defun x-symbol-mode-internal 1410,58954
(defun nuke-x-symbol 1484,62057
(defun x-symbol-options-filter 1497,62510
(defun x-symbol-extra-filter 1533,63666
(defun x-symbol-menu-filter 1541,63914
(defvar x-symbol-list-mode-map1568,64751
(defvar x-symbol-list-buffer 1594,65901
(defvar x-symbol-list-win-config 1596,65977
(defvar x-symbol-invisible-spec 1598,66088
(defvar x-symbol-itimer 1602,66238
(defvar x-symbol-invisible-display-table1605,66321
(defvar x-symbol-invisible-font 1614,66557
(defvar x-symbol-charsym-info-cache 1639,67744
(defvar x-symbol-language-info-caches 1641,67835
(defvar x-symbol-coding-info-cache 1643,67929
(defvar x-symbol-keys-info-cache 1645,68018
(defun x-symbol-list-bury 1653,68323
(defun x-symbol-list-restore 1659,68519
(defun x-symbol-list-store 1689,69737
(defun x-symbol-list-mode 1698,70154
(defun x-symbol-list-scroll 1719,70956
(defun x-symbol-init-language-interactive 1742,71598
(defun x-symbol-list-menu 1759,72312
(defun x-symbol-list-selected 1814,74220
(defun x-symbol-list-menu-selected 1840,75429
(defun x-symbol-list-mouse-selected 1851,75882
(defun x-symbol-charsym-info 1868,76604
(defun x-symbol-language-info 1882,77205
(defun x-symbol-coding-info 1914,78405
(defun x-symbol-keys-info 1934,79177
(defun x-symbol-info 1958,80100
(defun x-symbol-list-info 1971,80638
(defun x-symbol-highlight-echo 1985,81181
(defun x-symbol-point-info 1996,81730
(defun x-symbol-hide-revealed-at-point 2042,83652
(defun x-symbol-reveal-invisible 2079,85319
(defun x-symbol-show-info-and-invisible 2127,87511
(defun x-symbol-start-itimer-once 2163,89053
(defun x-symbol-setup-minibuffer 2179,89679
(defvar x-symbol-language-history 2197,90250
(defvar x-symbol-token-history 2200,90374
(defvar x-symbol-last-abbrev 2203,90450
(defvar x-symbol-electric-pos 2205,90546
(defvar x-symbol-command-keys 2208,90628
(defvar x-symbol-help-keys 2212,90759
(defvar x-symbol-help-language 2214,90854
(defvar x-symbol-help-completions 2216,90953
(defvar x-symbol-help-completions1 2218,91045
(defun x-symbol-map-default-binding 2226,91321
(defun x-symbol-read-charsym-token 2257,92399
(defun x-symbol-insert-command 2283,93322
(defun x-symbol-read-language 2334,95329
(defun x-symbol-read-token 2349,96007
(defun x-symbol-read-token-direct 2388,97516
(defun x-symbol-grid 2400,97916
(defun x-symbol-replace-from 2488,101532
(defvar x-symbol-token-search-prelude-size 2524,103033
(defun x-symbol-replace-token 2526,103081
(defun x-symbol-match-token-before 2551,104172
(defun x-symbol-token-input 2595,105975
(defun x-symbol-modify-key 2616,106805
(defun x-symbol-rotate-key 2649,108134
(defun x-symbol-electric-input 2703,110344
(defun x-symbol-help-mapper 2745,112045
(defun x-symbol-help-output 2768,112884
(defun x-symbol-help 2811,114480
(defvar x-symbol-face-docstrings2864,116549
(defvar x-symbol-all-key-prefixes 2870,116737
(defvar x-symbol-all-key-chain-alist 2872,116848
(defvar x-symbol-all-horizontal-chain-alist 2874,116947
(defvar x-symbol-all-chain-subchains-alist 2876,117060
(defvar x-symbol-all-exclusive-context-alist 2878,117174
(defalias 'x-symbol-table-grouping x-symbol-table-grouping
2886,117470
(defalias 'x-symbol-table-aspects x-symbol-table-aspects
2887,117511
(defalias 'x-symbol-table-score x-symbol-table-score
2888,117552
(defalias 'x-symbol-table-input x-symbol-table-input
2889,117592
(defsubst x-symbol-table-prefixes 2890,117633
(defsubst x-symbol-table-junk 2891,117684
(defsubst x-symbol-charsym-defined-p 2893,117735
(defun x-symbol-try-font-name-0 2901,118036
(defun x-symbol-try-font-name 2919,118592
(defun x-symbol-set-cstrings 2936,119108
(defun x-symbol-init-charsym-command 2981,121086
(defun x-symbol-init-charsym-input 2989,121452
(defun x-symbol-init-charsym-aspects 3058,124170
(defun x-symbol-init-cset 3088,125450
(defun x-symbol-make-atree 3238,132273
(defun x-symbol-atree-push 3242,132353
(defun x-symbol-component-root-p 3262,133042
(defun x-symbol-component-elements 3266,133181
(defun x-symbol-component-merge 3273,133429
(defun x-symbol-component-space 3287,133977
(defun x-symbol-modify-less-than 3301,134561
(defun x-symbol-inherit-aspects 3306,134784
(defun x-symbol-compute-aspects 3315,135223
(defun x-symbol-init-aspects 3331,135941
(defun x-symbol-sort-modify-chain 3376,137990
(defun x-symbol-init-horizontal/key-alist 3391,138562
(defun x-symbol-init-exclusive-alist 3407,139308
(defun x-symbol-init-horizontal-chain 3445,140912
(defun x-symbol-init-exclusive-chain 3453,141244
(defun x-symbol-init-rotate-chain 3460,141571
(defun x-symbol-init-context-atree 3481,142445
(defun x-symbol-init-key-bindings 3526,144728
(defun x-symbol-rotate-modify-less-than 3549,145651
(defun x-symbol-subgroup-less-than 3557,146046
(defun x-symbol-header-charsyms 3562,146303
(defun x-symbol-init-grid/menu 3588,147353
(defun x-symbol-init-input 3659,149953
(defun x-symbol-init-latin-decoding 3789,156429
(defun x-symbol-get-prime-for 3830,158300
(defun x-symbol-alist-to-obarray 3839,158624
(defun x-symbol-alist-to-hash-table 3845,158832
(defun x-symbol-init-language 3855,159165
(defvar x-symbol-latin1-cset3979,164630
(defvar x-symbol-latin2-cset3985,164803
(defvar x-symbol-latin3-cset3991,164976
(defvar x-symbol-latin5-cset3997,165149
(defvar x-symbol-latin9-cset4003,165321
(defvar x-symbol-xsymb0-cset4009,165527
(defvar x-symbol-xsymb1-cset4015,165782
(defvar x-symbol-latin1-table4021,166024
(defvar x-symbol-latin2-table4122,170494
(defvar x-symbol-latin3-table4221,173695
(defvar x-symbol-latin5-table4320,176576
(defvar x-symbol-latin9-table4419,178886
(defvar x-symbol-xsymb0-table4518,181276
(defvar x-symbol-xsymb1-table4668,188672
(defvar x-symbol-no-of-charsyms 4876,199307
(defun x-symbol-mac-setup1 4884,199673
(defun x-symbol-mac-setup2 4910,200582

x-symbol/lisp/x-symbol-emacs.el,1126
(defun emacs-version>=34,1341
(defvar x-symbol-emacs-has-font-lock-with-props68,3005
(defvar x-symbol-emacs-has-correct-find-safe-coding86,3670
(defvar x-symbol-emacs-after-create-image-function101,4184
(defvar image-types 127,5041
(defvar init-file-loaded 163,6428
(defvar message-stack 166,6501
(defun region-active-p 249,9811
(defvar x-symbol-data-directory 286,11176
(defun x-symbol-directory-files 356,13453
(defun x-symbol-event-in-current-buffer 370,13841
(defun x-symbol-create-image 373,13890
(defun x-symbol-make-glyph 376,13975
(defun x-symbol-set-glyph-image 379,14046
(defvar x-symbol-heading-strut-glyph 394,14543
(defvar x-symbol-invisible-face 397,14630
(defvar x-symbol-face 398,14688
(defvar x-symbol-sub-face 399,14726
(defvar x-symbol-sup-face 400,14772
(defvar x-symbol-emacs-w32-font-directories402,14819
(defvar x-symbol-invisible-display-table 415,15297
(defalias 'x-symbol-window-width x-symbol-window-width
417,15344
(defun x-symbol-set-face-font 428,15796
(defun x-symbol-event-matches-key-specifier-p 439,16269
(defun start-itimer 449,16541
(defun itimer-live-p 451,16638

x-symbol/lisp/x-symbol-hooks.el,3109
(defvar x-symbol-warn-of-old-emacs 66,2522
(defvar x-symbol-data-directory81,3030
(defvar x-symbol-font-directory87,3246
(defun x-symbol-define-user-options 98,3661
(defun x-symbol-auto-mode-suffixes 126,5060
(defcustom x-symbol-initialize 143,5652
(defvar x-symbol-orig-comint-input-sender 177,7219
(defun x-symbol-coding-system-from-locale 185,7531
(defun x-symbol-buffer-coding 223,9137
(defvar x-symbol-default-coding279,11196
(defcustom x-symbol-compose-key 325,13040
(defcustom x-symbol-auto-key-autoload 332,13308
(defvar x-symbol-auto-conversion-method 340,13623
(defvar x-symbol-language-alist 361,14586
(defcustom x-symbol-charsym-name 370,14923
(defcustom x-symbol-tex-name 378,15273
(defcustom x-symbol-tex-modes384,15440
(defcustom x-symbol-sgml-name 392,15708
(defcustom x-symbol-sgml-modes398,15880
(defcustom x-symbol-bib-name 407,16207
(defcustom x-symbol-bib-modes 413,16377
(defcustom x-symbol-texi-name 420,16603
(defcustom x-symbol-texi-modes 426,16779
(defvar x-symbol-mode 438,17188
(defvar x-symbol-language 445,17415
(defvar x-symbol-coding 460,18103
(defvar x-symbol-8bits 487,19379
(defvar x-symbol-unique 502,19965
(defvar x-symbol-subscripts 517,20547
(defvar x-symbol-image 530,21112
(defcustom x-symbol-auto-mode-suffixes 547,21754
(defcustom x-symbol-auto-8bit-search-limit 556,22179
(defcustom x-symbol-auto-style-alist 563,22461
(defvar x-symbol-mode-disable-alist 609,24419
(defun x-symbol-image-set-colormap 617,24694
(defcustom x-symbol-image-colormap-allocation 635,25402
(defcustom x-symbol-image-convert-colormap646,25858
(defalias 'x-symbol-cset-registry x-symbol-cset-registry
665,26545
(defalias 'x-symbol-cset-coding x-symbol-cset-coding
666,26587
(defalias 'x-symbol-cset-leading x-symbol-cset-leading
667,26627
(defalias 'x-symbol-cset-score x-symbol-cset-score
668,26668
(defalias 'x-symbol-cset-left x-symbol-cset-left
669,26708
(defalias 'x-symbol-cset-right x-symbol-cset-right
670,26745
(defvar x-symbol-input-initialized 672,26784
(defun x-symbol-key-autoload 681,27080
(defalias 'x-symbol-map-autoload x-symbol-map-autoload
703,28055
(defun x-symbol-buffer-file-name 710,28304
(defun x-symbol-auto-set-variable 723,28776
(defun x-symbol-mode 729,28994
(defun turn-on-x-symbol-conditionally 860,34373
(defun x-symbol-fontify 868,34663
(defun x-symbol-comint-output-filter 896,35787
(defun x-symbol-comint-send 905,36149
(defun x-symbol-format-decode 921,36806
(defun x-symbol-format-encode 943,37724
(defun x-symbol-after-insert-file 958,38250
(defun x-symbol-write-region-annotate-function 995,40092
(defun x-symbol-write-file-hook 1015,41096
(defvar x-symbol-modeline-string 1076,43560
(defvar x-symbol-mode-map1081,43775
(defconst x-symbol-early-language-access-alist1090,44065
(defun x-symbol-init-language-accesses 1095,44274
(defun x-symbol-register-language 1126,45445
(defun x-symbol-initialize 1146,46317
(defun x-symbol-after-init 1248,51435
(defun x-symbol-inherit-from-buffer 1306,54270
(defun x-symbol-auctex-math-insert 1339,55750
(defun x-symbol-turn-on-bib-cite 1348,56068

x-symbol/lisp/x-symbol-image.el,1980
(defvar x-symbol-image-process-buffer 48,1782
(defvar x-symbol-image-process-name 51,1893
(defvar x-symbol-image-highlight-map54,1992
(defun x-symbol-image-try-special 73,2736
(defvar x-symbol-image-broken-image82,3092
(defvar x-symbol-image-create-image87,3298
(defvar x-symbol-image-design-glyph92,3528
(defvar x-symbol-image-locked-glyph98,3773
(defvar x-symbol-image-remote-glyph104,4005
(defvar x-symbol-image-junk-glyph110,4240
(defvar x-symbol-image-buffer-extents 116,4471
(defvar x-symbol-image-memory-cache 121,4705
(defvar x-symbol-image-all-recursive-dirs 131,5181
(defvar x-symbol-image-all-dirs 133,5289
(defun x-symbol-image-parse-buffer 142,5583
(defun x-symbol-image-after-change-function 184,7740
(defun x-symbol-image-delete-extents 201,8322
(defun x-symbol-image-parse-region 230,9501
(defun x-symbol-image-default-file-name 313,12935
(defun x-symbol-image-init-memory-cache 329,13656
(defun x-symbol-image-init-memory-cache-1 359,14931
(defun x-symbol-image-searchpath 371,15428
(defun x-symbol-image-searchpath-1 399,16532
(defun x-symbol-image-mouse-editor 425,17580
(defun x-symbol-image-editor 433,17814
(defun x-symbol-image-highlight-menu 462,18897
(defun x-symbol-image-help-echo 471,19252
(defun x-symbol-image-file-name 486,19870
(defun x-symbol-image-event-file 502,20552
(defun x-symbol-image-active-file 513,20947
(defvar x-symbol-image-process-stack 569,22856
(defvar x-symbol-image-process-elem 573,23024
(defun x-symbol-image-create-glyph 587,23677
(defun x-symbol-image-cache-name 645,25868
(defun x-symbol-image-process-stack 670,26998
(defun x-symbol-image-convert-file 683,27562
(defun x-symbol-image-start-convert-mono 691,27895
(defun x-symbol-image-start-convert-color 702,28375
(defun x-symbol-image-start-convert-truecolor 713,28866
(defun x-symbol-image-start-convert-mswindows 723,29317
(defun x-symbol-image-start-convert-colormap 738,29917
(defun x-symbol-image-process-sentinel 755,30778

x-symbol/lisp/x-symbol-macs.el,569
(defmacro x-symbol-ignore-property-changes 43,1617
(defun x-symbol-set/push-assq/assoc 62,2278
(defmacro x-symbol-set-assq 76,2819
(defmacro x-symbol-set-assoc 82,3057
(defmacro x-symbol-push-assq 88,3300
(defmacro x-symbol-push-assoc 95,3618
(defmacro x-symbol-dolist-delaying 107,4113
(defmacro x-symbol-do-plist 148,5816
(defmacro x-symbol-while-charsym 168,6560
(defmacro x-symbol-encode-for-charsym 190,7309
(defmacro x-symbol-decode-for-charsym 220,8473
(defmacro x-symbol-decode-unique-test 245,9292
(defmacro x-symbol-set-buffer-multibyte 251,9467

x-symbol/lisp/x-symbol-mule.el,1507
(defvar x-symbol-mule-default-charset48,2000
(defalias 'x-symbol-make-cset x-symbol-make-cset
71,2912
(defalias 'x-symbol-make-char x-symbol-make-char
72,2968
(defalias 'x-symbol-init-charsym-syntax x-symbol-init-charsym-syntax
73,3024
(defalias 'x-symbol-charsym-after x-symbol-charsym-after
74,3100
(defalias 'x-symbol-string-to-charsyms x-symbol-string-to-charsyms
75,3164
(defalias 'x-symbol-match-before x-symbol-match-before
76,3238
(defalias 'x-symbol-encode-lisp x-symbol-encode-lisp
77,3300
(defalias 'x-symbol-pre-command-hook x-symbol-pre-command-hook
78,3360
(defalias 'x-symbol-post-command-hook x-symbol-post-command-hook
79,3430
(defalias 'x-symbol-encode-charsym-after x-symbol-encode-charsym-after
80,3502
(defalias 'x-symbol-init-quail-bindings x-symbol-init-quail-bindings
81,3580
(defvar x-symbol-mule-char-table 83,3657
(defvar x-symbol-mule-pre-command 85,3738
(defun x-symbol-mule-make-charset 93,4009
(defvar x-symbol-mule-default-font 107,4558
(defun x-symbol-mule-default-font 109,4599
(defun x-symbol-mule-make-cset 128,5509
(defun x-symbol-mule-make-char 190,7903
(defun x-symbol-mule-init-charsym-syntax 220,9039
(defun x-symbol-mule-init-quail-bindings 236,9669
(defun x-symbol-mule-encode-charsym-after 255,10393
(defun x-symbol-mule-charsym-after 259,10498
(defun x-symbol-mule-string-to-charsyms 268,10909
(defun x-symbol-mule-match-before 281,11395
(defun x-symbol-mule-pre-command-hook 305,12385
(defun x-symbol-mule-post-command-hook 314,12788

x-symbol/lisp/x-symbol-nomule.el,1954
(defalias 'x-symbol-make-cset x-symbol-make-cset
46,1779
(defalias 'x-symbol-make-char x-symbol-make-char
47,1837
(defalias 'x-symbol-init-charsym-syntax x-symbol-init-charsym-syntax
48,1895
(defalias 'x-symbol-charsym-after x-symbol-charsym-after
49,1944
(defalias 'x-symbol-string-to-charsyms x-symbol-string-to-charsyms
50,2010
(defalias 'x-symbol-match-before x-symbol-match-before
51,2086
(defalias 'x-symbol-encode-lisp x-symbol-encode-lisp
52,2150
(defalias 'x-symbol-pre-command-hook x-symbol-pre-command-hook
53,2212
(defalias 'x-symbol-post-command-hook x-symbol-post-command-hook
54,2284
(defalias 'x-symbol-encode-charsym-after x-symbol-encode-charsym-after
55,2358
(defalias 'x-symbol-init-quail-bindings x-symbol-init-quail-bindings
56,2438
(defvar x-symbol-nomule-mouse-yank-function 58,2488
(defvar x-symbol-nomule-mouse-track-function61,2629
(defvar x-symbol-nomule-cstring-regexp 66,2867
(defvar x-symbol-nomule-char-table 71,3128
(defvar x-symbol-nomule-pre-command 73,3211
(defvar x-symbol-nomule-leading-faces-alist 76,3309
(defvar x-symbol-nomule-font-lock-face 79,3482
(defvar x-symbol-nomule-display-table82,3583
(defvar x-symbol-nomule-character-quote-syntax 93,3945
(defun x-symbol-nomule-init-faces 101,4248
(defun x-symbol-nomule-make-cset 124,5108
(defun x-symbol-nomule-make-char 150,6186
(defun x-symbol-nomule-multibyte-char-p 180,7511
(defun x-symbol-nomule-encode-charsym-after 185,7749
(defun x-symbol-nomule-charsym-after 197,8147
(defun x-symbol-nomule-string-to-charsyms 220,9090
(defun x-symbol-nomule-match-before 236,9730
(defun x-symbol-nomule-goto-leading-char 269,11142
(defun x-symbol-nomule-mouse-yank-function 275,11371
(defun x-symbol-nomule-mouse-track-function 282,11690
(defun x-symbol-nomule-pre-command-hook 299,12476
(defun x-symbol-nomule-post-command-hook 313,13109
(defun x-symbol-nomule-match-cstring 351,14756
(defun x-symbol-nomule-fontify-cstrings 369,15504

x-symbol/lisp/x-symbol-sgml.el,1521
(defcustom x-symbol-sgml-auto-style41,1525
(defcustom x-symbol-sgml-auto-coding-alist52,1947
(defface x-symbol-sgml-symbol-face71,2757
(defface x-symbol-sgml-noname-face79,3038
(defcustom x-symbol-sgml-modeline-name 87,3301
(defcustom x-symbol-sgml-header-groups-alist93,3484
(defcustom x-symbol-sgml-class-alist113,4257
(defcustom x-symbol-sgml-class-face-alist124,4674
(defcustom x-symbol-sgml-electric-ignore 134,5097
(defvar x-symbol-sgml-token-list 141,5365
(defvar x-symbol-sgml-token-grammar156,6077
(defvar x-symbol-sgml-user-table 163,6317
(defvar x-symbol-sgml-generated-data 166,6426
(defcustom x-symbol-sgml-master-directory 175,6746
(defcustom x-symbol-sgml-image-searchpath 182,6973
(defcustom x-symbol-sgml-image-cached-dirs 189,7223
(defcustom x-symbol-sgml-image-file-truename-alist196,7489
(defcustom x-symbol-sgml-image-keywords226,8698
(defun x-symbol-sgml-image-file-truename 236,9078
(defcustom x-symbol-sgml-subscript-matcher 250,9639
(defcustom x-symbol-sgml-font-lock-regexp 256,9875
(defcustom x-symbol-sgml-font-lock-limit-regexp 262,10079
(defcustom x-symbol-sgml-font-lock-contents-regexp 269,10350
(defcustom x-symbol-sgml-font-lock-alist276,10605
(defun x-symbol-sgml-default-token-list 292,11264
(defvar x-symbol-sgml-latin1-table310,12052
(defvar x-symbol-sgml-latinN-table409,15286
(defvar x-symbol-sgml-xsymb0-table495,17715
(defvar x-symbol-sgml-xsymb1-table601,21570
(defvar x-symbol-sgml-table640,23549
(defun x-symbol-sgml-subscript-matcher 657,24155

x-symbol/lisp/x-symbol-tex.el,2359
(defcustom x-symbol-tex-auto-style55,1896
(defcustom x-symbol-tex-auto-coding-alist70,2510
(defcustom x-symbol-tex-coding-master 87,3158
(defcustom x-symbol-tex-modeline-name 99,3626
(defcustom x-symbol-tex-header-groups-alist 105,3805
(defcustom x-symbol-tex-electric-ignore 112,4065
(defcustom x-symbol-tex-electric-ignore-regexp 119,4364
(defcustom x-symbol-tex-token-suppress-space 126,4653
(defvar x-symbol-tex-extra-menu-items135,5045
(defvar x-symbol-tex-token-grammar145,5474
(defvar x-symbol-tex-verb-delimiter-regexp 160,6263
(defvar x-symbol-tex-env-verbatim-regexp 164,6456
(defvar x-symbol-tex-env-tabbing-regexp 168,6637
(defvar x-symbol-tex-user-table 172,6812
(defvar x-symbol-tex-generated-data 175,6916
(defcustom x-symbol-tex-master-directory 184,7234
(defcustom x-symbol-tex-image-searchpath191,7518
(defcustom x-symbol-tex-image-cached-dirs 209,8205
(defcustom x-symbol-tex-image-keywords216,8458
(defcustom x-symbol-tex-subscript-matcher 234,9311
(defcustom x-symbol-tex-invisible-braces 240,9543
(defcustom x-symbol-tex-font-lock-allowed-faces245,9639
(defvar x-symbol-tex-font-lock-regexp256,10183
(defvar x-symbol-tex-font-lock-limit-regexp 261,10425
(defface x-symbol-tex-math-face270,10764
(defface x-symbol-tex-text-face278,11034
(defcustom x-symbol-tex-class-alist286,11306
(defcustom x-symbol-tex-class-face-alist320,12867
(defun x-symbol-tex-auto-coding-alist 336,13456
(defun x-symbol-tex-default-master-directory 360,14702
(defun x-symbol-tex-default-electric-ignore 368,15088
(defun x-symbol-tex-default-token-list 390,16097
(defun x-symbol-tex-after-init-language 400,16459
(defvar x-symbol-tex-required-fonts 419,17293
(defvar x-symbol-tex-latin1-table423,17445
(defvar x-symbol-tex-latinN-table522,21630
(defvar x-symbol-tex-xsymb0-table611,25318
(defvar x-symbol-tex-xsymb1-table726,29931
(defvar x-symbol-tex-table886,37347
(defun x-symbol-tex-subscript-matcher 903,37904
(defun x-symbol-tex-encode 951,39573
(defun x-symbol-tex-decode 972,40387
(defun x-symbol-tex-token-input 1047,43403
(defun x-symbol-tex-translate-locations 1063,43971
(defun x-symbol-tex-error-location 1119,45896
(defun x-symbol-tex-preview-locations 1149,46926
(defun x-symbol-tex-xdecode-old 1203,48666
(defvar x-symbol-tex-xdecode-obarray 1245,50315
(defun x-symbol-tex-xdecode-latex 1247,50358

x-symbol/lisp/x-symbol-texi.el,597
(defcustom x-symbol-texi-auto-style 41,1573
(defcustom x-symbol-texi-modeline-name 48,1832
(defcustom x-symbol-texi-header-groups-alist54,2015
(defcustom x-symbol-texi-electric-ignore 69,2682
(defcustom x-symbol-texi-class-alist76,2950
(defcustom x-symbol-texi-class-face-alist 89,3508
(defvar x-symbol-texi-token-grammar98,3801
(defvar x-symbol-texi-user-table 107,4094
(defvar x-symbol-texi-generated-data 110,4206
(defvar x-symbol-texi-latin1-table119,4523
(defvar x-symbol-texi-latinN-table218,7766
(defvar x-symbol-texi-xsymbX-table303,10629
(defvar x-symbol-texi-table327,11362

x-symbol/lisp/x-symbol-unichars.el,99
(defvar x-symbol-unicode-character-list5,115
(defun x-symbol-list-unicode-characters 5044,235676

x-symbol/lisp/x-symbol-unicode.el,170
(defconst x-symbol-xsym-unicode-map	12,383
(defconst x-symbol-old-tables 260,9819
(defconst x-symbol-unicode-table 276,10252
(defconst x-symbol-unicode-cset292,10757

x-symbol/lisp/x-symbol-unicode-extras.el,38
(defconst x-symol-unicode-extras 2,1

x-symbol/lisp/x-symbol-vars.el,8058
(defconst x-symbol-version 40,1516
(defgroup x-symbol 49,1858
(defgroup x-symbol-mode 56,2069
(defgroup x-symbol-input-init 61,2198
(defgroup x-symbol-input-control 66,2334
(defgroup x-symbol-info-general 71,2466
(defgroup x-symbol-info-strings 76,2602
(defgroup x-symbol-miscellaneous 81,2738
(defgroup x-symbol-image-general 86,2864
(defgroup x-symbol-image-language 91,3029
(defgroup x-symbol-tex 101,3458
(defgroup x-symbol-sgml 107,3589
(defgroup x-symbol-bib 113,3725
(defgroup x-symbol-texi 119,3859
(define-widget 'x-symbol-key x-symbol-key
132,4246
(define-widget 'x-symbol-auto-style x-symbol-auto-style
136,4336
(define-widget 'x-symbol-command x-symbol-command
156,5203
(define-widget 'x-symbol-charsym x-symbol-charsym
161,5311
(define-widget 'x-symbol-group x-symbol-group
165,5402
(define-widget 'x-symbol-coding x-symbol-coding
169,5494
(define-widget 'x-symbol-function-or-regexp x-symbol-function-or-regexp
178,5712
(define-widget 'x-symbol-fancy-spec x-symbol-fancy-spec
182,5881
(define-widget 'x-symbol-fancy x-symbol-fancy
191,6229
(define-widget 'x-symbol-auto-coding x-symbol-auto-coding
200,6582
(define-widget 'x-symbol-headers x-symbol-headers
211,6889
(define-widget 'x-symbol-class-info x-symbol-class-info
217,7045
(define-widget 'x-symbol-class-faces x-symbol-class-faces
224,7288
(define-widget 'x-symbol-image-keywords x-symbol-image-keywords
232,7568
(defconst x-symbol-cache-variables 249,8155
(defun x-symbol-set-cache-variable 258,8514
(defconst x-symbol-LANG-name 270,8931
(defconst x-symbol-LANG-modes 276,9186
(defconst x-symbol-LANG-auto-style 282,9519
(defcustom x-symbol-LANG-modeline-name 336,11613
(defconst x-symbol-LANG-required-fonts 343,11898
(defconst x-symbol-LANG-token-grammar348,12134
(defconst x-symbol-LANG-generated-data 416,15400
(defconst x-symbol-LANG-table 422,15652
(defconst x-symbol-LANG-header-groups-alist 435,16207
(defconst x-symbol-LANG-class-alist441,16510
(defconst x-symbol-LANG-class-face-alist 455,17122
(defconst x-symbol-LANG-electric-ignore 466,17574
(defconst x-symbol-LANG-extra-menu-items 477,18088
(defconst x-symbol-LANG-subscript-matcher 485,18533
(defconst x-symbol-LANG-image-keywords 494,19001
(defconst x-symbol-LANG-master-directory 509,19696
(defconst x-symbol-LANG-image-searchpath 515,19987
(defconst x-symbol-LANG-image-cached-dirs 523,20414
(defvar x-symbol-package-url 534,20885
(defconst x-symbol-maintainer-address 539,21129
(defvar x-symbol-installer-address 542,21268
(defcustom x-symbol-token-input 552,21708
(defcustom x-symbol-electric-input 567,22362
(defcustom x-symbol-local-menu 598,24006
(defcustom x-symbol-local-grid 608,24350
(defcustom x-symbol-temp-grid 620,24893
(defcustom x-symbol-temp-help 630,25272
(defvar x-symbol-use-refbuffer-once 640,25670
(defcustom x-symbol-reveal-invisible 657,26459
(defcustom x-symbol-character-info 676,27270
(defcustom x-symbol-context-info 695,28145
(defcustom x-symbol-charsym-modeline-name 710,28745
(defcustom x-symbol-coding-name-alist716,28955
(defcustom x-symbol-coding-modeline-alist742,29899
(defcustom x-symbol-modeline-state-list757,30432
(defcustom x-symbol-set-coding-system-if-undecided 794,31811
(defcustom x-symbol-auto-coding-search-limit 807,32387
(defcustom x-symbol-charsym-ascii-alist 819,32858
(defcustom x-symbol-charsym-ascii-groups832,33446
(defcustom x-symbol-valid-charsym-function 843,33930
(defvar x-symbol-user-table 849,34181
(defvar x-symbol-mule-change-default-face 861,34742
(defcustom x-symbol-map-default-keys-alist872,35242
(defcustom x-symbol-map-default-bindings902,36271
(defvar x-symbol-after-init-input-hook 915,36725
(defvar x-symbol-menu929,37366
(defcustom x-symbol-menu-max-items 1005,40730
(defcustom x-symbol-header-groups-alist1013,41090
(defcustom x-symbol-completions-buffer 1042,42228
(defcustom x-symbol-grid-buffer-format 1049,42470
(defcustom x-symbol-grid-reuse 1058,42862
(defcustom x-symbol-grid-header-echo1065,43142
(defcustom x-symbol-grid-ignore-charsyms 1076,43585
(defcustom x-symbol-grid-tab-width 1082,43812
(defface x-symbol-heading-face1089,44115
(defvar x-symbol-heading-strut-glyph1101,44565
(defvar x-symbol-key-init-ignore 1115,45116
(defvar x-symbol-quail-init-ignore 1119,45254
(defvar x-symbol-context-init-ignore 1123,45394
(defcustom x-symbol-context-ignore 1130,45685
(defcustom x-symbol-electric-ignore 1138,46014
(defcustom x-symbol-rotate-suffix-char 1149,46535
(defcustom x-symbol-rotate-prefix-alist1158,46977
(defvar x-symbol-list-mode-hook 1181,47657
(defvar x-symbol-key-min-length 1186,47824
(defvar x-symbol-quail-suffix-string 1191,48048
(defvar x-symbol-define-input-method-quail 1194,48100
(defcustom x-symbol-idle-delay 1201,48355
(defface x-symbol-revealed-face1209,48703
(defcustom x-symbol-context-info-ignore 1217,48995
(defcustom x-symbol-context-info-threshold 1225,49388
(defcustom x-symbol-context-info-ignore-regexp 1231,49594
(defcustom x-symbol-context-info-ignore-groups1237,49821
(defface x-symbol-info-face1251,50343
(defface x-symbol-emph-info-face1262,50788
(defcustom x-symbol-info-intro-after1270,51073
(defcustom x-symbol-info-intro-before1279,51379
(defcustom x-symbol-info-intro-highlight1288,51684
(defcustom x-symbol-info-intro-list1297,52025
(defcustom x-symbol-info-intro-yank1306,52413
(defcustom x-symbol-info-alias-after1315,52795
(defcustom x-symbol-info-alias-before1325,53227
(defcustom x-symbol-info-context-pre1335,53644
(defcustom x-symbol-info-context-post1344,54033
(defcustom x-symbol-info-token-pre 1353,54349
(defcustom x-symbol-info-token-charsym1360,54609
(defcustom x-symbol-info-classes-pre 1369,54957
(defcustom x-symbol-info-classes-sep 1376,55213
(defcustom x-symbol-info-classes-post 1383,55468
(defcustom x-symbol-info-classes-charsym 1390,55728
(defcustom x-symbol-info-coding-pre 1397,56006
(defcustom x-symbol-info-coding-sep 1404,56252
(defcustom x-symbol-info-coding-post 1411,56499
(defcustom x-symbol-info-coding-alist1418,56723
(defcustom x-symbol-info-keys-keymaps 1434,57353
(defcustom x-symbol-info-keys-pre1442,57729
(defcustom x-symbol-info-keys-sep 1451,58097
(defcustom x-symbol-info-keys-post 1458,58354
(defconst x-symbol-fancy-cache-size 1465,58581
(defvar x-symbol-cache-size 1468,58688
(defvar x-symbol-modify-aspects-alist1477,59011
(defvar x-symbol-rotate-aspects-alist1491,59696
(defvar x-symbol-group-input-alist1507,60510
(defvar x-symbol-group-syntax-alist1557,62097
(defvar x-symbol-subgroup-string-alist1600,63344
(defvar x-symbol-latin-force-use 1614,63859
(defvar x-symbol-font-sizes1623,64369
(defvar x-symbol-font-lock-with-extra-props1633,64777
(defvar x-symbol-latin1-fonts1637,64928
(defvar x-symbol-latin2-fonts1642,65128
(defvar x-symbol-latin3-fonts1648,65391
(defvar x-symbol-latin5-fonts1654,65654
(defvar x-symbol-latin9-fonts1661,65961
(defvar x-symbol-xsymb0-fonts1666,66159
(defvar x-symbol-xsymb1-fonts1672,66450
(defcustom x-symbol-image-max-width 1683,66913
(defcustom x-symbol-image-max-height 1688,67035
(defcustom x-symbol-image-update-cache 1693,67158
(defcustom x-symbol-image-use-remote 1709,67929
(defcustom x-symbol-image-current-marker 1734,69128
(defcustom x-symbol-image-scale-method 1742,69475
(defcustom x-symbol-image-explicitly-relative-regexp 1756,70205
(defcustom x-symbol-image-searchpath-follow-symlink 1761,70387
(defcustom x-symbol-image-cache-directories1776,71082
(defvar x-symbol-image-temp-name1825,73064
(defcustom x-symbol-image-convert-mono-regexp1834,73481
(defcustom x-symbol-image-help-echo1848,74169
(defcustom x-symbol-image-editor-alist1860,74673
(defvar x-symbol-image-menu1893,76029
(defvar x-symbol-image-data-directory 1914,77032
(defvar x-symbol-image-special-glyphs1918,77199
(defcustom x-symbol-image-convert-file-alist1951,78897
(defcustom x-symbol-image-convert-program1961,79365
(defcustom x-symbol-image-converter1967,79592
(defun x-symbol-variable-interactive 2074,84086
(defcustom x-symbol-use-unicode 2093,84916

x-symbol/lisp/x-symbol-xmacs.el,522
(defun x-symbol-paren-reset-mode 102,4657
(defvar x-symbol-xmacs-default-face-fonts 136,6073
(defalias 'x-symbol-directory-files x-symbol-directory-files
138,6121
(defun x-symbol-event-in-current-buffer 140,6176
(defun x-symbol-create-image 144,6318
(defalias 'x-symbol-make-glyph x-symbol-make-glyph
149,6483
(defalias 'x-symbol-set-glyph-image x-symbol-set-glyph-image
151,6528
(defun x-symbol-set-face-font 153,6583
(defun x-symbol-event-matches-key-specifier-p 163,7016
(defun x-symbol-window-width 173,7418

doc/ProofGeneral.texi,5379
@node Top166,5052
@node Preface203,6168
@node Latest news for version 3.7Latest news for version 3.7
226,6764
@node Future264,8432
@node Credits295,9731
@node Introducing Proof GeneralIntroducing Proof General
394,13165
@node Installing Proof GeneralInstalling Proof General
450,15197
@node Quick start guideQuick start guide
464,15645
@node Features of Proof GeneralFeatures of Proof General
508,17753
@node Supported proof assistantsSupported proof assistants
597,21678
@node Prerequisites for this manualPrerequisites for this manual
646,23584
@node Organization of this manualOrganization of this manual
690,25210
@node Basic Script ManagementBasic Script Management
716,26038
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
735,26638
@node Proof scriptsProof scripts
986,36291
@node Script buffersScript buffers
1029,38411
@node Locked queue and editing regionsLocked queue and editing regions
1051,38988
@node Goal-save sequencesGoal-save sequences
1107,41135
@node Active scripting bufferActive scripting buffer
1144,42621
@node Summary of Proof General buffersSummary of Proof General buffers
1213,46041
@node Script editing commandsScript editing commands
1275,48715
@node Script processing commandsScript processing commands
1353,51573
@node Proof assistant commandsProof assistant commands
1481,56874
@node Toolbar commandsToolbar commands
1631,61878
@node Interrupting during trace outputInterrupting during trace output
1655,62807
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1694,64731
@node Goals buffer commandsGoals buffer commands
1708,65231
@node Advanced Script ManagementAdvanced Script Management
1797,68764
@node Visibility of completed proofsVisibility of completed proofs
1828,69918
@node Switching between proof scriptsSwitching between proof scripts
1883,71841
@node View of processed files View of processed files 
1920,73813
@node Retracting across filesRetracting across files
1980,76864
@node Asserting across filesAsserting across files
1993,77495
@node Automatic multiple file handlingAutomatic multiple file handling
2006,78061
@node Escaping script managementEscaping script management
2031,79095
@node Experimental featuresExperimental features
2089,81298
@node Support for other PackagesSupport for other Packages
2123,82561
@node Syntax highlightingSyntax highlighting
2155,83436
@node X-Symbol supportX-Symbol support
2194,85057
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2253,87603
@node Support for outline modeSupport for outline mode
2312,89733
@node Support for completionSupport for completion
2338,90863
@node Support for tagsSupport for tags
2395,93031
@node Customizing Proof GeneralCustomizing Proof General
2447,95360
@node Basic optionsBasic options
2487,97030
@node How to customizeHow to customize
2511,97788
@node Display customizationDisplay customization
2562,99890
@node User optionsUser options
2687,105124
@node Changing facesChanging faces
2951,114523
@node Tweaking configuration settingsTweaking configuration settings
3026,117192
@node Hints and TipsHints and Tips
3083,119718
@node Adding your own keybindingsAdding your own keybindings
3102,120319
@node Using file variablesUsing file variables
3158,122852
@node Using abbreviationsUsing abbreviations
3217,125038
@node LEGO Proof GeneralLEGO Proof General
3256,126454
@node LEGO specific commandsLEGO specific commands
3297,127823
@node LEGO tagsLEGO tags
3317,128278
@node LEGO customizationsLEGO customizations
3327,128525
@node Coq Proof GeneralCoq Proof General
3359,129444
@node Coq-specific commandsCoq-specific commands
3375,129853
@node Coq-specific variablesCoq-specific variables
3397,130360
@node Editing multiple proofsEditing multiple proofs
3419,131018
@node User-loaded tacticsUser-loaded tactics
3443,132126
@node Holes featureHoles feature
3507,134600
@node Isabelle Proof GeneralIsabelle Proof General
3534,135887
@node Isabelle commandsIsabelle commands
3564,137017
@node Logics and SettingsLogics and Settings
3671,140065
@node Isabelle customizationsIsabelle customizations
3705,141605
@node HOL Proof GeneralHOL Proof General
3729,142087
@node Shell Proof GeneralShell Proof General
3771,143909
@node Obtaining and InstallingObtaining and Installing
3807,145368
@node Obtaining Proof GeneralObtaining Proof General
3823,145781
@node Installing Proof General from tarballInstalling Proof General from tarball
3854,147020
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
3879,147852
@node Setting the names of binariesSetting the names of binaries
3894,148260
@node Notes for syssiesNotes for syssies
3922,149200
@node Bugs and EnhancementsBugs and Enhancements
3995,152138
@node References4016,152953
@node History of Proof GeneralHistory of Proof General
4056,153977
@node Old News for 3.0Old News for 3.0
4147,158079
@node Old News for 3.1Old News for 3.1
4217,161773
@node Old News for 3.2Old News for 3.2
4243,162945
@node Old News for 3.3Old News for 3.3
4304,165948
@node Old News for 3.4Old News for 3.4
4323,166845
@node Function IndexFunction Index
4346,167901
@node Variable IndexVariable Index
4350,167977
@node Keystroke IndexKeystroke Index
4354,168057
@node Concept IndexConcept Index
4358,168123

doc/PG-adapting.texi,3776
@node Top157,4775
@node Introduction195,5920
@node Future236,7573
@node Credits272,9169
@node Beginning with a New ProverBeginning with a New Prover
282,9461
@node Overview of adding a new proverOverview of adding a new prover
323,11410
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
397,14831
@node Major modes used by Proof GeneralMajor modes used by Proof General
466,18222
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
539,21305
@node Settings for generic user-level commandsSettings for generic user-level commands
554,21851
@node Menu configurationMenu configuration
599,23587
@node Toolbar configurationToolbar configuration
623,24505
@node Proof Script SettingsProof Script Settings
681,26750
@node Recognizing commands and commentsRecognizing commands and comments
703,27330
@node Recognizing proofsRecognizing proofs
824,32857
@node Recognizing other elementsRecognizing other elements
936,37676
@node Configuring undo behaviourConfiguring undo behaviour
1062,43154
@node Nested proofsNested proofs
1200,48501
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1240,50128
@node Activate scripting hookActivate scripting hook
1263,51074
@node Automatic multiple filesAutomatic multiple files
1287,51938
@node Completions1309,52785
@node Proof Shell SettingsProof Shell Settings
1349,54263
@node Proof shell commandsProof shell commands
1380,55545
@node Script input to the shellScript input to the shell
1547,62724
@node Settings for matching various output from proof processSettings for matching various output from proof process
1614,65767
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1745,71534
@node Hooks and other settingsHooks and other settings
1955,81081
@node Goals Buffer SettingsGoals Buffer Settings
2054,85078
@node Splash Screen SettingsSplash Screen Settings
2131,88192
@node Global ConstantsGlobal Constants
2157,88950
@node Handling Multiple FilesHandling Multiple Files
2183,89799
@node Configuring Editing SyntaxConfiguring Editing Syntax
2335,97583
@node Configuring Font LockConfiguring Font Lock
2392,99700
@node Configuring X-SymbolConfiguring X-Symbol
2479,103943
@node Writing More Lisp CodeWriting More Lisp Code
2539,106466
@node Default values for generic settingsDefault values for generic settings
2556,107111
@node Adding prover-specific configurationsAdding prover-specific configurations
2586,108194
@node Useful variablesUseful variables
2629,109476
@node Useful functions and macrosUseful functions and macros
2655,110270
@node Internals of Proof GeneralInternals of Proof General
2758,114233
@node Spans2786,115141
@node Proof General site configurationProof General site configuration
2799,115515
@node Configuration variable mechanismsConfiguration variable mechanisms
2879,118603
@node Global variablesGlobal variables
2997,123839
@node Proof script modeProof script mode
3067,126389
@node Proof shell modeProof shell mode
3326,138044
@node Debugging3732,154091
@node Plans and IdeasPlans and Ideas
3775,154968
@node Proof by pointing and similar featuresProof by pointing and similar features
3796,155690
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3834,157348
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3879,159573
@node Demonstration InstantiationsDemonstration Instantiations
3909,160604
@node demoisa-easy.el3925,161035
@node demoisa.el3988,163274
@node Function IndexFunction Index
4156,168803
@node Variable IndexVariable Index
4160,168879
@node Concept IndexConcept Index
4169,169058

x-symbol/lisp/_pkg.el,0

x-symbol/lisp/custom-load.el,0

lib/holes-load.el,0

generic/proof-system.el,0

generic/_pkg.el,0

twelf/x-symbol-twelf.el,0

pgshell/pgshell.el,0

lego/x-symbol-lego.el,0

isar/x-symbol-isar.el,0

isar/isar-templates.el,0

isar/isar-autotest.el,0

isar/interface-setup.el,0

hol98/x-symbol-hol98.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/x-symbol-acl2.el,0

acl2/acl2.el,0