coq/coq-abbrev.el,504
(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,666
(defconst coq-tacticals-menu 27,784
(defconst coq-tacticals-abbrev-table 31,894
(defconst coq-commands-menu 34,986
(defconst coq-commands-abbrev-table 40,1203
(defconst coq-terms-menu 43,1293
(defconst coq-terms-abbrev-table 48,1433
(defun coq-install-abbrevs 55,1628
(defpgdefault menu-entries 74,2307
(defpgdefault help-menu-entries155,5728

coq/coq-db.el,559
(defconst coq-syntax-db 22,534
(defvar coq-user-tactics-db58,1907
(defun coq-insert-from-db 68,2256
(defun coq-build-regexp-list-from-db 86,3037
(defun max-length-db 108,4090
(defun coq-build-menu-from-db-internal 120,4365
(defun coq-build-title-menu 155,5988
(defun coq-sort-menu-entries 164,6356
(defun coq-build-menu-from-db 170,6486
(defun coq-build-abbrev-table-from-db 192,7323
(defun filter-state-preserving 209,7881
(defun filter-state-changing 214,8035
(defface coq-solve-tactics-face 221,8256
(defconst coq-solve-tactics-face 229,8518

coq/coq.el,6283
(defcustom coq-translate-to-v8 41,1202
(defun coq-build-prog-args 47,1382
(defcustom coq-compile-file-command 60,1762
(defcustom coq-default-undo-limit 70,2131
(defconst coq-shell-init-cmd 75,2259
(defcustom coq-prog-env 93,2860
(defconst coq-shell-restart-cmd 101,3112
(defvar coq-shell-prompt-pattern 108,3372
(defvar coq-shell-cd 116,3701
(defvar coq-shell-abort-goal-regexp 120,3856
(defvar coq-shell-proof-completed-regexp 123,3982
(defvar coq-goal-regexp126,4134
(defun coq-library-directory 135,4323
(defcustom coq-tags 142,4503
(defconst coq-interrupt-regexp 147,4653
(defcustom coq-www-home-page 152,4774
(defvar coq-outline-regexp162,4945
(defvar coq-outline-heading-end-regexp 169,5159
(defvar coq-shell-outline-regexp 171,5213
(defvar coq-shell-outline-heading-end-regexp 172,5263
(defconst coq-kill-goal-command 177,5373
(defconst coq-forget-id-command 178,5416
(defconst coq-back-n-command 179,5463
(defconst coq-state-preserving-tactics-regexp 183,5607
(defconst coq-state-changing-commands-regexp185,5708
(defconst coq-state-preserving-commands-regexp 187,5815
(defconst coq-commands-regexp 189,5927
(defvar coq-retractable-instruct-regexp 191,6005
(defvar coq-non-retractable-instruct-regexp 193,6096
(defvar coq-keywords-section197,6236
(defvar coq-section-regexp 200,6330
(defun coq-set-undo-limit 234,7430
(defconst coq-keywords-decl-defn-regexp245,7869
(defun coq-proof-mode-p 249,8019
(defun coq-is-comment-or-proverprocp 260,8427
(defun coq-is-goalsave-p 262,8531
(defun coq-is-module-equal-p 263,8606
(defun coq-is-def-p 266,8802
(defun coq-is-decl-defn-p 268,8910
(defun coq-state-preserving-command-p 273,9077
(defun coq-command-p 276,9211
(defun coq-state-preserving-tactic-p 279,9311
(defun coq-state-changing-tactic-p 284,9459
(defun coq-state-changing-command-p 291,9693
(defun coq-section-or-module-start-p 298,10039
(defun build-list-id-from-string 307,10280
(defun coq-last-prompt-info 320,10810
(defun coq-last-prompt-info-safe 332,11351
(defvar coq-last-but-one-statenum 338,11608
(defvar coq-last-but-one-proofnum 344,11906
(defvar coq-last-but-one-proofstack 347,12004
(defun coq-get-span-statenum 350,12114
(defun coq-get-span-proofnum 355,12229
(defun coq-get-span-proofstack 360,12344
(defun coq-set-span-statenum 365,12488
(defun coq-get-span-goalcmd 370,12619
(defun coq-set-span-goalcmd 375,12733
(defun coq-set-span-proofnum 380,12863
(defun coq-set-span-proofstack 385,12994
(defun proof-last-locked-span 390,13154
(defun coq-set-state-infos 405,13758
(defun count-not-intersection 445,15837
(defun  coq-find-and-forget-v81 476,17091
(defun coq-find-and-forget-v80 504,18223
(defun coq-find-and-forget 599,22922
(defvar coq-current-goal 612,23462
(defun coq-goal-hyp 615,23527
(defun coq-state-preserving-p 628,23960
(defconst notation-print-kinds-table 643,24466
(defun coq-PrintScope 647,24634
(defun coq-guess-or-ask-for-string 666,25190
(defun coq-ask-do 677,25575
(defun coq-SearchIsos 686,25963
(defun coq-SearchConstant 692,26196
(defun coq-SearchRewrite 696,26289
(defun coq-SearchAbout 700,26387
(defun coq-Print 704,26479
(defun coq-About 708,26601
(defun coq-LocateConstant 712,26718
(defun coq-LocateLibrary 718,26853
(defun coq-addquotes 724,27003
(defun coq-LocateNotation 726,27051
(defun coq-Pwd 733,27250
(defun coq-Inspect 739,27382
(defun coq-PrintSection(743,27482
(defun coq-Print-implicit 747,27575
(defun coq-Check 752,27726
(defun coq-Show 757,27834
(defun coq-Compile 771,28277
(defun coq-guess-command-line 785,28597
(defun coq-mode-config 806,29450
(defun coq-hybrid-ouput-goals-response-p 920,33646
(defun coq-hybrid-ouput-goals-response 926,33904
(defun coq-shell-mode-config 946,34814
(defun coq-goals-mode-config 990,36885
(defun coq-response-config 997,37117
(defpacustom print-fully-explicit 1020,37826
(defpacustom print-implicit 1025,37975
(defpacustom print-coercions 1030,38142
(defpacustom print-match-wildcards 1035,38287
(defpacustom print-elim-types 1040,38468
(defpacustom printing-depth 1045,38635
(defpacustom time-commands 1050,38797
(defpacustom auto-compile-vos 1054,38908
(defun coq-maybe-compile-buffer 1083,40024
(defun coq-ancestors-of 1120,41558
(defun coq-all-ancestors-of 1143,42525
(defconst coq-require-command-regexp 1155,42918
(defun coq-process-require-command 1160,43127
(defun coq-included-children 1165,43254
(defun coq-process-file 1186,44093
(defun coq-preprocessing 1201,44632
(defun coq-fake-constant-markup 1216,45051
(defun coq-create-span-menu 1238,45858
(defconst module-kinds-table 1258,46435
(defconst modtype-kinds-table1262,46585
(defun coq-insert-section-or-module 1266,46714
(defconst reqkinds-kinds-table1289,47574
(defun coq-insert-requires 1294,47719
(defun coq-end-Section 1310,48225
(defun coq-insert-intros 1328,48809
(defun coq-insert-match 1340,49333
(defun coq-insert-tactic 1372,50511
(defun coq-insert-tactical 1378,50750
(defun coq-insert-command 1384,50999
(defun coq-insert-term 1390,51243
(define-key coq-keymap 1396,51440
(define-key coq-keymap 1397,51498
(define-key coq-keymap 1398,51555
(define-key coq-keymap 1399,51624
(define-key coq-keymap 1400,51680
(define-key coq-keymap 1401,51729
(define-key coq-keymap 1402,51787
(define-key coq-keymap 1404,51848
(define-key coq-keymap 1405,51907
(define-key coq-keymap 1407,51971
(define-key coq-keymap 1408,52031
(define-key coq-keymap 1410,52087
(define-key coq-keymap 1411,52137
(define-key coq-keymap 1412,52187
(define-key coq-keymap 1413,52237
(define-key coq-keymap 1414,52291
(define-key coq-keymap 1415,52350
(defvar last-coq-error-location 1425,52533
(defun coq-get-last-error-location 1434,52932
(defun coq-highlight-error 1467,54329
(defvar coq-allow-highlight-error 1532,56884
(defun coq-decide-highlight-error 1538,57150
(defun coq-highlight-error-hook 1543,57312
(defun first-word-of-buffer 1554,57705
(defun coq-show-first-goal 1564,57937
(defvar coq-modeline-string2 1580,58606
(defvar coq-modeline-string1 1581,58650
(defvar coq-modeline-string0 1582,58693
(defun coq-build-subgoals-string 1583,58738
(defun coq-update-minor-mode-alist 1588,58906
(defun is-not-split-vertic 1614,59974
(defun optim-resp-windows 1623,60413

coq/coq-indent.el,2259
(defconst coq-any-command-regexp17,315
(defconst coq-indent-inner-regexp20,406
(defconst coq-comment-start-regexp 31,794
(defconst coq-comment-end-regexp 32,837
(defconst coq-comment-start-or-end-regexp33,878
(defconst coq-indent-open-regexp35,986
(defconst coq-indent-close-regexp40,1160
(defconst coq-indent-closepar-regexp 45,1341
(defconst coq-indent-closematch-regexp 46,1386
(defconst coq-indent-openpar-regexp 47,1457
(defconst coq-indent-openmatch-regexp 48,1501
(defconst coq-indent-any-regexp49,1581
(defconst coq-indent-kw54,1859
(defconst coq-indent-pattern-regexp 64,2313
(defun coq-indent-goal-command-p 68,2416
(defconst coq-end-command-regexp90,3471
(defun coq-search-comment-delimiter-forward 95,3623
(defun coq-search-comment-delimiter-backward 104,3953
(defun coq-skip-until-one-comment-backward 111,4227
(defun coq-skip-until-one-comment-forward 126,4934
(defun coq-looking-at-comment 137,5452
(defun coq-find-comment-start 141,5593
(defun coq-find-comment-end 152,6026
(defun coq-looking-at-syntactic-context 165,6572
(defconst coq-end-command-or-comment-regexp171,6794
(defconst coq-end-command-or-comment-start-regexp174,6903
(defun coq-find-not-in-comment-backward 178,7021
(defun coq-find-not-in-comment-forward 198,7922
(defun coq-find-command-end-backward 222,9064
(defun coq-find-command-end-forward 231,9455
(defun coq-find-command-end 240,9832
(defun coq-parse-function 249,10215
(defun coq-find-current-start 258,10417
(defun coq-find-real-start 267,10708
(defun coq-command-at-point 274,10927
(defun coq-indent-only-spaces-on-line 281,11204
(defun coq-indent-find-reg 287,11481
(defun coq-find-no-syntactic-on-line 301,12017
(defun coq-back-to-indentation-prevline 314,12490
(defun coq-find-unclosed 358,14404
(defun coq-find-at-same-level-zero 388,15705
(defun coq-find-unopened 416,16870
(defun coq-find-last-unopened 459,18320
(defun coq-end-offset 470,18717
(defun coq-indent-command-offset 495,19508
(defun coq-indent-expr-offset 542,21332
(defun coq-indent-comment-offset 658,26035
(defun coq-indent-offset 690,27493
(defun coq-indent-calculate 708,28356
(defun coq-indent-line 711,28444
(defun coq-indent-line-not-comments 721,28810
(defun coq-indent-region 731,29199

coq/coq-local-vars.el,279
(defconst coq-local-vars-doc 17,304
(defun coq-insert-coq-prog-name 75,2830
(defun coq-read-directory 83,3183
(defun coq-extract-directories-from-args 98,3872
(defun coq-ask-prog-args 113,4382
(defun coq-ask-prog-name 133,5424
(defun coq-ask-insert-coq-prog-name 148,6065

coq/coq-syntax.el,2614
(defcustom coq-prog-name 12,354
(defvar coq-version-is-V8 33,1300
(defvar coq-version-is-V8-0 35,1379
(defvar coq-version-is-V8-1 42,1757
(defun coq-determine-version 51,2190
(defcustom coq-user-tactics-db 96,4048
(defcustom coq-user-commands-db 113,4561
(defcustom coq-user-tacticals-db 129,5080
(defcustom coq-user-solve-tactics-db 145,5601
(defcustom coq-user-reserved-db 163,6122
(defvar coq-tactics-db181,6653
(defvar coq-solve-tactics-db336,14721
(defvar coq-tacticals-db360,15568
(defvar coq-decl-db384,16455
(defvar coq-defn-db406,17673
(defvar coq-goal-starters-db459,21659
(defvar coq-other-commands-db486,23214
(defvar coq-commands-db610,32411
(defvar coq-terms-db617,32637
(defun coq-count-match 681,35289
(defun coq-goal-command-str-v80-p 700,36152
(defun coq-module-opening-p 723,37025
(defun coq-section-command-p 734,37441
(defun coq-goal-command-str-v81-p 738,37538
(defun coq-goal-command-p-v81 753,38207
(defun coq-goal-command-str-p 763,38547
(defun coq-goal-command-p 773,38913
(defvar coq-keywords-save-strict781,39225
(defvar coq-keywords-save790,39338
(defun coq-save-command-p 794,39416
(defvar coq-keywords-kill-goal 803,39710
(defvar coq-keywords-state-changing-misc-commands807,39801
(defvar coq-keywords-goal810,39926
(defvar coq-keywords-decl813,40009
(defvar coq-keywords-defn816,40083
(defvar coq-keywords-state-changing-commands820,40158
(defvar coq-keywords-state-preserving-commands829,40419
(defvar coq-keywords-commands834,40635
(defvar coq-solve-tactics839,40784
(defvar coq-tacticals843,40905
(defvar coq-reserved849,41044
(defvar coq-state-changing-tactics860,41373
(defvar coq-state-preserving-tactics863,41482
(defvar coq-tactics867,41596
(defvar coq-retractable-instruct870,41685
(defvar coq-non-retractable-instruct873,41795
(defvar coq-keywords877,41923
(defvar coq-symbols884,42091
(defvar coq-error-regexp 903,42304
(defvar coq-id 906,42532
(defvar coq-id-shy 907,42557
(defvar coq-ids 909,42611
(defun coq-first-abstr-regexp 911,42652
(defvar coq-font-lock-terms914,42748
(defconst coq-save-command-regexp-strict934,43711
(defconst coq-save-command-regexp938,43878
(defconst coq-save-with-hole-regexp942,44031
(defconst coq-goal-command-regexp946,44190
(defconst coq-goal-with-hole-regexp949,44290
(defconst coq-decl-with-hole-regexp953,44423
(defconst coq-defn-with-hole-regexp960,44672
(defconst coq-with-with-hole-regexp970,44961
(defvar coq-font-lock-keywords-1976,45254
(defvar coq-font-lock-keywords 1001,46519
(defun coq-init-syntax-table 1003,46577
(defconst coq-generic-expression1032,47476

coq/coq-unicode-tokens.el,290
(defconst coq-token-format 18,631
(defconst coq-charref-format 19,664
(defconst coq-token-prefix 20,698
(defconst coq-token-suffix 21,730
(defconst coq-token-match 22,762
(defconst coq-hexcode-match 23,793
(defcustom coq-token-name-alist 25,827
(defcustom coq-shortcut-alist44,1557

coq/x-symbol-coq.el,1748
(defvar x-symbol-coq-required-fonts 19,510
(defvar x-symbol-coq-name 27,911
(defvar x-symbol-coq-modeline-name 28,951
(defcustom x-symbol-coq-header-groups-alist 30,994
(defcustom x-symbol-coq-electric-ignore 37,1212
(defvar x-symbol-coq-required-fonts 44,1457
(defvar x-symbol-coq-extra-menu-items 47,1556
(defvar x-symbol-coq-token-grammar51,1644
(defun x-symbol-coq-default-token-list 67,2310
(defvar x-symbol-coq-user-table 79,2598
(defvar x-symbol-coq-generated-data 82,2704
(defvar x-symbol-coq-master-directory 90,2942
(defvar x-symbol-coq-image-searchpath 91,2990
(defvar x-symbol-coq-image-cached-dirs 92,3037
(defvar x-symbol-coq-image-file-truename-alist 93,3102
(defvar x-symbol-coq-image-keywords 94,3154
(defcustom x-symbol-coq-subscript-matcher 101,3382
(defcustom x-symbol-coq-font-lock-regexp 107,3614
(defcustom x-symbol-coq-font-lock-limit-regexp 112,3786
(defcustom x-symbol-coq-font-lock-contents-regexp 118,3974
(defcustom x-symbol-coq-single-char-regexp 125,4228
(defun x-symbol-coq-subscript-matcher 130,4376
(defun coq-match-subscript 165,6065
(defvar x-symbol-coq-font-lock-allowed-faces 172,6231
(defcustom x-symbol-coq-class-alist177,6456
(defcustom x-symbol-coq-class-face-alist 188,6834
(defvar x-symbol-coq-font-lock-keywords 198,7144
(defvar x-symbol-coq-font-lock-allowed-faces 200,7190
(defvar x-symbol-coq-case-insensitive 206,7414
(defvar x-symbol-coq-token-shape 207,7457
(defvar x-symbol-coq-input-token-ignore 208,7495
(defvar x-symbol-coq-token-list 209,7540
(defvar x-symbol-coq-symbol-table 211,7584
(defvar x-symbol-coq-xsymbol-table 315,10006
(defun x-symbol-coq-prepare-table 462,13874
(defvar x-symbol-coq-table471,14141
(defcustom x-symbol-coq-auto-style478,14302

demoisa/demoisa.el,349
(defcustom isabelledemo-prog-name 54,1809
(defcustom isabelledemo-web-page59,1931
(defun demoisa-config 70,2161
(defun demoisa-shell-config 91,2953
(define-derived-mode demoisa-mode 117,3930
(define-derived-mode demoisa-shell-mode 122,4053
(define-derived-mode demoisa-response-mode 127,4196
(define-derived-mode demoisa-goals-mode 131,4323

isar/isabelle-system.el,1401
(defgroup isabelle 26,775
(defcustom isabelle-web-page30,903
(defcustom isa-isatool-command41,1198
(defvar isatool-not-found 71,2260
(defun isa-set-isatool-command 74,2373
(defun isa-shell-command-to-string 97,3317
(defun isa-getenv 103,3541
(defcustom isabelle-program-name123,4228
(defvar isabelle-prog-name 149,5158
(defun isa-tool-list-logics 152,5285
(defcustom isabelle-logics-available 159,5522
(defcustom isabelle-chosen-logic 170,5886
(defun isabelle-command-line 183,6354
(defun isabelle-choose-logic 206,7311
(defun isa-view-doc 228,8277
(defun isa-tool-list-docs 237,8541
(defconst isabelle-verbatim-regexp 264,9573
(defun isabelle-verbatim 267,9715
(defcustom isabelle-refresh-logics 274,9876
(defvar isabelle-docs-menu 282,10203
(defvar isabelle-logics-menu-entries 290,10490
(defun isabelle-logics-menu-calculate 293,10563
(defvar isabelle-time-to-refresh-logics 312,11126
(defun isabelle-logics-menu-refresh 316,11221
(defun isabelle-logics-menu-filter 333,11918
(defun isabelle-menu-bar-update-logics 339,12128
(defvar isabelle-logics-menu350,12467
(defun isabelle-load-isar-keywords 363,13079
(defpgdefault menu-entries384,13820
(defpgdefault help-menu-entries 387,13872
(defun isabelle-convert-idmarkup-to-subterm 415,14630
(defun isabelle-create-span-menu 439,15641
(defun isabelle-xml-sml-escapes 455,16083
(defun isabelle-process-pgip 458,16184

isar/isar.el,1204
(defcustom isar-keywords-name 31,720
(defpgdefault completion-table 48,1243
(defcustom isar-web-page50,1296
(defun isar-strip-terminators 64,1632
(defun isar-markup-ml 77,2009
(defun isar-mode-config-set-variables 82,2144
(defun isar-shell-mode-config-set-variables 150,5325
(defun isar-remove-file 247,9384
(defun isar-shell-compute-new-files-list 257,9747
(defun isar-activate-scripting 268,10213
(define-derived-mode isar-shell-mode 277,10383
(define-derived-mode isar-response-mode 282,10506
(define-derived-mode isar-goals-mode 287,10688
(define-derived-mode isar-mode 292,10863
(defpgdefault menu-entries346,12835
(defun isar-count-undos 376,14074
(defun isar-find-and-forget 403,15188
(defun isar-goal-command-p 442,16768
(defun isar-global-save-command-p 447,16945
(defvar isar-current-goal 468,17806
(defun isar-state-preserving-p 471,17872
(defvar isar-shell-current-line-width 496,19069
(defun isar-shell-adjust-line-width 501,19261
(defun isar-preprocessing 524,20152
(defun isar-mode-config 547,21419
(defun isar-shell-mode-config 558,21920
(defun isar-response-mode-config 569,22279
(defun isar-goals-mode-config 578,22522
(defun isar-goalhyplit-test 589,22854

isar/isar-find-theorems.el,778
(defun isar-find-theorems-minibuffer 18,712
(defun isar-find-theorems-form 32,1331
(defvar isar-find-theorems-data 74,3131
(defvar isar-find-theorems-widget-number 88,3466
(defvar isar-find-theorems-widget-pattern 91,3564
(defvar isar-find-theorems-widget-intro 94,3656
(defvar isar-find-theorems-widget-elim 97,3742
(defvar isar-find-theorems-widget-dest 100,3826
(defvar isar-find-theorems-widget-name 103,3910
(defvar isar-find-theorems-widget-simp 106,3997
(defun isar-find-theorems-create-searchform111,4143
(defun isar-find-theorems-create-help 251,8758
(defun isar-find-theorems-submit-searchform294,10930
(defun isar-find-theorems-parse-criteria 372,13307
(defun isar-find-theorems-parse-number 465,16407
(defun isar-find-theorems-filter-empty 475,16684

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,481
(defconst isar-keywords-minor206,3641
(defconst isar-keywords-control262,4395
(defconst isar-keywords-diag282,4872
(defconst isar-keywords-theory-begin338,5831
(defconst isar-keywords-theory-switch341,5884
(defconst isar-keywords-theory-end344,5939
(defconst isar-keywords-theory-heading347,5987
(defconst isar-keywords-theory-decl353,6094
(defconst isar-keywords-theory-script412,7075
(defconst isar-keywords-theory-goal416,7152
(defconst isar-keywords-qed429,7369
(defconst isar-keywords-qed-block436,7455
(defconst isar-keywords-qed-global439,7502
(defconst isar-keywords-proof-heading442,7551
(defconst isar-keywords-proof-goal447,7634
(defconst isar-keywords-proof-block454,7733
(defconst isar-keywords-proof-open458,7795
(defconst isar-keywords-proof-close461,7841
(defconst isar-keywords-proof-chain464,7888
(defconst isar-keywords-proof-decl471,7991
(defconst isar-keywords-proof-asm480,8112
(defconst isar-keywords-proof-asm-goal487,8207
(defconst isar-keywords-proof-script490,8262

isar/isar-mmm.el,83
(defconst isar-start-latex-regexp 23,697
(defconst isar-start-sml-regexp 35,1130

isar/isar-syntax.el,3471
(defconst isar-script-syntax-table-entries20,471
(defconst isar-script-syntax-table-alist61,1502
(defun isar-init-syntax-table 70,1792
(defun isar-init-output-syntax-table 78,2039
(defconst isar-keyword-begin 94,2486
(defconst isar-keyword-end 95,2524
(defconst isar-keywords-theory-enclose97,2559
(defconst isar-keywords-theory102,2704
(defconst isar-keywords-save107,2849
(defconst isar-keywords-proof-enclose112,2978
(defconst isar-keywords-proof118,3160
(defconst isar-keywords-proof-context125,3365
(defconst isar-keywords-local-goal129,3479
(defconst isar-keywords-proper133,3591
(defconst isar-keywords-improper138,3724
(defconst isar-keywords-outline143,3870
(defconst isar-keywords-fume146,3935
(defconst isar-keywords-indent-open153,4153
(defconst isar-keywords-indent-close159,4337
(defconst isar-keywords-indent-enclose163,4442
(defun isar-regexp-simple-alt 172,4657
(defun isar-ids-to-regexp 192,5417
(defconst isar-ext-first 226,6823
(defconst isar-ext-rest 227,6890
(defconst isar-long-id-stuff 229,6962
(defconst isar-id 230,7036
(defconst isar-idx 231,7106
(defconst isar-string 233,7165
(defconst isar-any-command-regexp235,7225
(defconst isar-name-regexp239,7359
(defconst isar-improper-regexp245,7654
(defconst isar-save-command-regexp249,7802
(defconst isar-global-save-command-regexp252,7903
(defconst isar-goal-command-regexp255,8017
(defconst isar-local-goal-command-regexp258,8125
(defconst isar-comment-start 261,8238
(defconst isar-comment-end 262,8273
(defconst isar-comment-start-regexp 263,8306
(defconst isar-comment-end-regexp 264,8377
(defconst isar-string-start-regexp 266,8445
(defconst isar-string-end-regexp 267,8497
(defconst isar-antiq-regexp276,8750
(defconst isar-nesting-regexp283,8911
(defun isar-nesting 286,9009
(defun isar-match-nesting 298,9430
(defface isabelle-class-name-face310,9761
(defface isabelle-tfree-name-face320,10036
(defface isabelle-tvar-name-face330,10317
(defface isabelle-free-name-face340,10597
(defface isabelle-bound-name-face350,10873
(defface isabelle-var-name-face360,11152
(defconst isabelle-class-name-face 370,11431
(defconst isabelle-tfree-name-face 371,11493
(defconst isabelle-tvar-name-face 372,11555
(defconst isabelle-free-name-face 373,11616
(defconst isabelle-bound-name-face 374,11677
(defconst isabelle-var-name-face 375,11739
(defconst isar-font-lock-local378,11801
(defvar isar-font-lock-keywords-1383,11967
(defvar isar-output-font-lock-keywords-1397,12833
(defvar isar-goals-font-lock-keywords424,14457
(defconst isar-undo 458,15136
(defun isar-remove 460,15198
(defun isar-undos 463,15273
(defun isar-cannot-undo 467,15379
(defconst isar-theory-start-regexp470,15449
(defconst isar-end-regexp476,15614
(defconst isar-undo-fail-regexp480,15715
(defconst isar-undo-skip-regexp484,15819
(defconst isar-undo-ignore-regexp487,15940
(defconst isar-undo-remove-regexp490,16005
(defconst isar-any-entity-regexp498,16180
(defconst isar-named-entity-regexp503,16367
(defconst isar-unnamed-entity-regexp508,16544
(defconst isar-next-entity-regexps511,16646
(defconst isar-generic-expression519,16957
(defconst isar-indent-any-regexp530,17274
(defconst isar-indent-inner-regexp532,17367
(defconst isar-indent-enclose-regexp534,17433
(defconst isar-indent-open-regexp536,17549
(defconst isar-indent-close-regexp538,17659
(defconst isar-outline-regexp544,17796
(defconst isar-outline-heading-end-regexp 548,17949

isar/isar-unicode-tokens.el,298
(defconst isar-token-format 14,433
(defconst isar-charref-format 15,471
(defconst isar-token-prefix 16,513
(defconst isar-token-suffix 17,548
(defconst isar-token-match 18,581
(defconst isar-hexcode-match 19,635
(defcustom isar-token-name-alist21,697
(defcustom isar-shortcut-alist354,8635

isar/x-symbol-isar.el,1775
(defvar x-symbol-isar-required-fonts 15,498
(defvar x-symbol-isar-name 23,898
(defvar x-symbol-isar-modeline-name 24,944
(defcustom x-symbol-isar-header-groups-alist 26,988
(defcustom x-symbol-isar-electric-ignore 33,1208
(defvar x-symbol-isar-required-fonts 41,1456
(defvar x-symbol-isar-extra-menu-items 44,1561
(defvar x-symbol-isar-token-grammar48,1655
(defun x-symbol-isar-token-list 55,1853
(defvar x-symbol-isar-user-table 58,1938
(defvar x-symbol-isar-generated-data 61,2051
(defvar x-symbol-isar-master-directory 69,2290
(defvar x-symbol-isar-image-searchpath 70,2339
(defvar x-symbol-isar-image-cached-dirs 71,2387
(defvar x-symbol-isar-image-file-truename-alist 72,2453
(defvar x-symbol-isar-image-keywords 73,2506
(defcustom x-symbol-isar-subscript-matcher 83,2846
(defcustom x-symbol-isar-font-lock-regexp 89,3081
(defcustom x-symbol-isar-font-lock-limit-regexp 94,3257
(defcustom x-symbol-isar-font-lock-contents-regexp 100,3481
(defcustom x-symbol-isar-single-char-regexp 110,3865
(defun x-symbol-isar-subscript-matcher 116,4135
(defun isabelle-match-subscript 158,5787
(defvar x-symbol-isar-font-lock-keywords167,6163
(defvar x-symbol-isar-font-lock-allowed-faces 174,6423
(defcustom x-symbol-isar-class-alist181,6651
(defcustom x-symbol-isar-class-face-alist 192,7072
(defvar x-symbol-isar-case-insensitive 207,7592
(defvar x-symbol-isar-token-shape 208,7636
(defvar x-symbol-isar-input-token-ignore 209,7675
(defvar x-symbol-isar-token-list 210,7721
(defvar x-symbol-isar-symbol-table 212,7766
(defvar x-symbol-isar-xsymbol-table 312,10498
(defun x-symbol-isar-prepare-table 458,14928
(defvar x-symbol-isar-table466,15124
(defcustom x-symbol-isar-auto-style480,15457
(defcustom x-symbol-isar-auto-coding-alist 494,15954

lclam/lclam.el,524
(defcustom lclam-prog-name 15,385
(defcustom lclam-web-page21,533
(defun lclam-config 32,763
(defun lclam-shell-config 54,1557
(define-derived-mode lclam-proofscript-mode 74,2216
(define-derived-mode lclam-shell-mode 79,2339
(define-derived-mode lclam-response-mode 84,2473
(define-derived-mode lclam-goals-mode 88,2596
(defun lclam-mode 96,2824
(define-derived-mode thy-mode 133,3635
(defvar thy-mode-map 136,3733
(defun thy-add-menus 138,3760
(defun process-thy-file 178,5674
(defun update-thy-only 184,5875

lego/lego.el,1727
(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,6687
(defun lego-goal-hyp 245,8523
(defun lego-state-preserving-p 254,8721
(defvar lego-shell-current-line-width 270,9424
(defun lego-shell-adjust-line-width 278,9731
(defun lego-mode-config 297,10470
(defun lego-equal-module-filename 365,12497
(defun lego-shell-compute-new-files-list 371,12772
(defun lego-shell-mode-config 385,13298
(defun lego-goals-mode-config 434,15234

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,644
(defcustom phox-prog-name 31,909
(defcustom phox-sym-lock-enabled 36,1011
(defcustom phox-web-page42,1118
(defcustom phox-doc-dir 48,1268
(defcustom phox-lib-dir 54,1416
(defcustom phox-tags-program 60,1560
(defcustom phox-tags-doc 66,1740
(defcustom phox-etags 72,1878
(defpgdefault menu-entries93,2330
(defun phox-config 107,2523
(defun phox-shell-config 153,4560
(define-derived-mode phox-mode 178,5489
(define-derived-mode phox-shell-mode 198,6101
(define-derived-mode phox-response-mode 203,6229
(define-derived-mode phox-goals-mode 215,6656
(defpgdefault completion-table240,7524
(defpgdefault x-symbol-language 248,7629

phox/phox-extraction.el,382
(defvar phox-prog-orig 11,480
(defun phox-prog-flags-modify(13,548
(defun phox-prog-flags-extract(42,1352
(defun phox-prog-flags-erase(53,1643
(defun phox-toggle-extraction(61,1839
(defun phox-compile-theorem(73,2241
(defun phox-compile-theorem-on-cursor(79,2467
(defun phox-output 95,2946
(defun phox-output-theorem 105,3160
(defun phox-output-theorem-on-cursor(112,3460

phox/phox-font.el,123
(defconst phox-font-lock-keywords6,282
(defconst phox-sym-lock-keywords-table65,2401
(defun phox-sym-lock-start 88,2975

phox/phox-fun.el,679
(defun phox-init-syntax-table 67,2392
(defvar phox-top-keywords83,2865
(defvar phox-proof-keywords131,3320
(defun phox-find-and-forget 172,3670
(defun phox-assert-next-command-interactive 251,6095
(defun phox-depend-theorem(270,6926
(defun phox-eshow-extlist(279,7216
(defun phox-flag-name(293,7815
(defun phox-path(304,8118
(defun phox-print-expression(315,8355
(defun phox-print-sort-expression(328,8813
(defun phox-priority-symbols-list(339,9126
(defun phox-search-string(351,9499
(defun phox-constraints(366,10027
(defun phox-goals(377,10284
(defvar phox-state-menu389,10494
(defun phox-delete-symbol(414,11484
(defun phox-delete-symbol-on-cursor(420,11693

phox/phox-lang.el,283
(defvar phox-lang8,278
(defun phox-lang-absurd 17,495
(defun phox-lang-suppress 22,590
(defun phox-lang-opendef 27,789
(defun phox-lang-instance 32,908
(defun phox-lang-lock 37,1037
(defun phox-lang-unlock 42,1174
(defun phox-lang-prove 47,1317
(defun phox-lang-let 52,1454

phox/phox-outline.el,70
(defun phox-outline-level(32,1113
(defun phox-setup-outline 46,1587

phox/phox-pbrpm.el,512
(defun phox-pbrpm-left-paren-p 27,1188
(defun phox-pbrpm-right-paren-p 34,1391
(defun phox-pbrpm-menu-from-string 42,1595
(defun phox-pbrpm-rename-in-cmd 51,1929
(defun phox-pbrpm-get-region-name 84,3183
(defun  phox-pbrpm-escape-string 87,3310
(defun phox-pbrpm-generate-menu 91,3445
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
289,10634
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
290,10698
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
291,10760

phox/phox-sym-lock.el,1353
(defvar phox-sym-lock-sym-count 34,1598
(defvar phox-sym-lock-ext-start 37,1668
(defvar phox-sym-lock-ext-end 39,1790
(defvar phox-sym-lock-font-size 42,1909
(defvar phox-sym-lock-keywords 47,2099
(defvar phox-sym-lock-enabled 52,2275
(defvar phox-sym-lock-color 57,2437
(defvar phox-sym-lock-mouse-face 62,2655
(defvar phox-sym-lock-mouse-face-enabled 67,2845
(defconst phox-sym-lock-with-mule 72,3035
(defun phox-sym-lock-gen-symbol 75,3119
(defun phox-sym-lock-make-symbols-atomic 83,3422
(defun phox-sym-lock-compute-font-size 110,4364
(defvar phox-sym-lock-font-name148,5784
(defun phox-sym-lock-set-foreground 190,7270
(defun phox-sym-lock-translate-char 204,7879
(defun phox-sym-lock-translate-char-or-string 212,8147
(defun phox-sym-lock-remap-face 219,8374
(defvar phox-sym-lock-clear-face239,9364
(defun phox-sym-lock 251,9786
(defun phox-sym-lock-rec 260,10190
(defun phox-sym-lock-atom-face 266,10343
(defun phox-sym-lock-pre-idle-hook-first 271,10639
(defun phox-sym-lock-pre-idle-hook-last 279,10997
(defun phox-sym-lock-enable 288,11372
(defun phox-sym-lock-disable 301,11785
(defun phox-sym-lock-mouse-face-enable 314,12203
(defun phox-sym-lock-mouse-face-disable 321,12418
(defun phox-sym-lock-font-lock-hook 328,12637
(defun font-lock-set-defaults 343,13330
(defun phox-sym-lock-patch-keywords 354,13708

phox/phox-tags.el,305
(defun phox-tags-add-table(21,766
(defun phox-tags-reset-table(38,1354
(defun phox-tags-add-doc-table(48,1619
(defun phox-tags-add-lib-table(54,1768
(defun phox-tags-add-local-table(60,1904
(defun phox-tags-create-local-table(66,2087
(defun phox-complete-tag(77,2339
(defvar phox-tags-menu96,2889

phox/x-symbol-phox.el,1609
(defvar x-symbol-phox-required-fonts 16,472
(defcustom x-symbol-phox-header-groups-alist 31,1079
(defcustom x-symbol-phox-electric-ignore 38,1299
(defvar x-symbol-phox-required-fonts 45,1515
(defvar x-symbol-phox-extra-menu-items 48,1616
(defvar x-symbol-phox-token-grammar51,1705
(defvar x-symbol-phox-input-token-grammar65,2496
(defun x-symbol-phox-default-token-list 71,2751
(defvar x-symbol-phox-user-table 83,3069
(defvar x-symbol-phox-generated-data 86,3178
(defvar x-symbol-phox-master-directory 94,3417
(defvar x-symbol-phox-image-searchpath 95,3466
(defvar x-symbol-phox-image-cached-dirs 96,3514
(defvar x-symbol-phox-image-file-truename-alist 97,3580
(defvar x-symbol-phox-image-keywords 98,3633
(defcustom x-symbol-phox-class-alist105,3854
(defcustom x-symbol-phox-class-face-alist 116,4236
(defvar x-symbol-phox-font-lock-keywords 126,4549
(defvar x-symbol-phox-font-lock-allowed-faces 128,4596
(defvar x-symbol-phox-case-insensitive 134,4821
(defvar x-symbol-phox-token-shape 135,4865
(defvar x-symbol-phox-input-token-ignore 136,4904
(defvar x-symbol-phox-token-list 143,5143
(defvar x-symbol-phox-xsymb0-table 145,5188
(defun x-symbol-phox-prepare-table 166,5647
(defvar x-symbol-phox-table174,5823
(defcustom x-symbol-phox-auto-style185,6141
(defvar x-symbol-phox-menu-alist 211,7084
(defvar x-symbol-phox-grid-alist 213,7174
(defvar x-symbol-phox-decode-atree 216,7265
(defvar x-symbol-phox-decode-alist 218,7358
(defvar x-symbol-phox-encode-alist 220,7455
(defvar x-symbol-phox-nomule-decode-exec 224,7612
(defvar x-symbol-phox-nomule-encode-exec 226,7712

plastic/plastic.el,2866
(defcustom plastic-tags 29,821
(defcustom plastic-test-all-name 34,953
(defvar plastic-lit-string 41,1144
(defcustom plastic-help-menu-list45,1258
(defvar plastic-shell-process-output59,1752
(defconst plastic-process-config 67,2078
(defconst plastic-pretty-set-width 74,2328
(defconst plastic-interrupt-regexp 78,2477
(defcustom plastic-www-home-page 84,2598
(defcustom plastic-www-latest-release89,2735
(defcustom plastic-www-refcard95,2908
(defcustom plastic-library-www-page101,3039
(defcustom plastic-base 111,3254
(defvar plastic-prog-name 119,3426
(defun plastic-set-default-env-vars 123,3534
(defvar plastic-shell-prompt-pattern 131,3772
(defvar plastic-shell-cd 134,3897
(defvar plastic-shell-abort-goal-regexp 138,4039
(defvar plastic-shell-proof-completed-regexp 142,4207
(defvar plastic-save-command-regexp145,4350
(defvar plastic-goal-command-regexp147,4446
(defvar plastic-kill-goal-command 150,4543
(defvar plastic-forget-id-command 152,4644
(defvar plastic-undoable-commands-regexp155,4725
(defvar plastic-goal-regexp 167,5172
(defvar plastic-outline-regexp169,5220
(defvar plastic-outline-heading-end-regexp 175,5399
(defvar plastic-shell-outline-regexp 177,5455
(defvar plastic-shell-outline-heading-end-regexp 178,5513
(defvar plastic-error-occurred 180,5584
(define-derived-mode plastic-shell-mode 189,5916
(define-derived-mode plastic-mode 195,6098
(define-derived-mode plastic-goals-mode 209,6551
(defun plastic-count-undos 218,6896
(defun plastic-goal-command-p 238,7772
(defun plastic-find-and-forget 243,7965
(defun plastic-goal-hyp 278,9313
(defun plastic-state-preserving-p 289,9563
(defvar plastic-shell-current-line-width 312,10539
(defun plastic-shell-adjust-line-width 320,10855
(defun plastic-mode-config 347,11950
(defun plastic-show-shell-buffer 436,15191
(defun plastic-equal-module-filename 442,15294
(defun plastic-shell-compute-new-files-list 448,15572
(defun plastic-shell-mode-config 464,16109
(defun plastic-goals-mode-config 515,18302
(defun plastic-small-bar 527,18584
(defun plastic-large-bar 529,18673
(defun plastic-preprocessing 531,18811
(defun plastic-all-ctxt 582,20639
(defun plastic-send-one-undo 589,20817
(defun plastic-minibuf-cmd 599,21145
(defun plastic-minibuf 611,21624
(defun plastic-synchro 618,21830
(defun plastic-send-minibuf 623,21971
(defun plastic-had-error 631,22300
(defun plastic-reset-error 635,22475
(defun plastic-call-if-no-error 638,22614
(defun plastic-show-shell 643,22818
(define-key plastic-keymap 652,23080
(define-key plastic-keymap 653,23141
(define-key plastic-keymap 654,23202
(define-key plastic-keymap 655,23262
(define-key plastic-keymap 656,23321
(define-key plastic-keymap 657,23380
(defalias 'proof-toolbar-command proof-toolbar-command
667,23630
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
668,23681

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,402
(defun proof-associated-buffers 38,1096
(defun proof-associated-windows 48,1308
(defun pg-assoc-strip-subterm-markup 65,1789
(defvar pg-assoc-ann-regexp 91,2722
(defun pg-assoc-strip-subterm-markup-buf 94,2817
(defun pg-assoc-strip-subterm-markup-buf-old 117,3536
(defconst pg-assoc-active-area-keymap 146,4391
(defun pg-assoc-make-top-span 153,4616
(defun pg-assoc-analyse-structure 190,6081

generic/pg-autotest.el,442
(defvar pg-autotest-success 24,543
(defun pg-autotest-find-file 28,627
(defun pg-autotest-find-file-restart 35,907
(defmacro pg-autotest 48,1355
(defun pg-autotest-script-wholefile 62,1702
(defun pg-autotest-retract-file 79,2315
(defun pg-autotest-assert-processed 85,2451
(defun pg-autotest-assert-unprocessed 92,2705
(defun pg-autotest-message 99,2965
(defun pg-autotest-quit-prover 106,3158
(defun pg-autotest-finished 112,3339

generic/pg-custom.el,600
(defpgcustom x-symbol-enable 32,1065
(defpgcustom x-symbol-language 42,1491
(defpgcustom maths-menu-enable 47,1713
(defpgcustom unicode-tokens-enable 53,1893
(defpgcustom mmm-enable 59,2070
(defpgcustom script-indent 68,2424
(defconst proof-toolbar-entries-default73,2561
(defpgcustom toolbar-entries 107,4474
(defpgcustom prog-args 125,5194
(defpgcustom prog-env 138,5769
(defpgcustom favourites 147,6195
(defpgcustom menu-entries 152,6384
(defpgcustom help-menu-entries 159,6620
(defpgcustom keymap 166,6883
(defpgcustom completion-table 171,7055
(defpgcustom tags-program 182,7429

generic/pg-goals.el,363
(define-derived-mode proof-goals-mode 30,632
(define-key proof-goals-mode-map 61,1622
(defun proof-goals-config-done 91,3090
(defun pg-goals-display 101,3378
(defun pg-goals-yank-subterm 167,5815
(defun pg-goals-button-action 194,6715
(defun proof-expand-path 215,7687
(defun pg-goals-construct-command 224,7929
(defun pg-goals-get-subterm-help 256,9117

generic/pg-pbrpm.el,1803
(defvar pg-pbrpm-use-buffer-menu 22,547
(defvar pg-pbrpm-start-goal-regexp 25,669
(defvar pg-pbrpm-start-goal-regexp-par-num 29,826
(defvar pg-pbrpm-end-goal-regexp 32,949
(defvar pg-pbrpm-start-hyp-regexp 36,1101
(defvar pg-pbrpm-start-hyp-regexp-par-num 40,1262
(defvar pg-pbrpm-start-concl-regexp 44,1469
(defvar pg-pbrpm-auto-select-regexp 48,1633
(defvar pg-pbrpm-buffer-menu 55,1794
(defvar pg-pbrpm-spans 56,1828
(defvar pg-pbrpm-goal-description 57,1856
(defvar pg-pbrpm-windows-dialog-bug 58,1895
(defvar pbrpm-menu-desc 59,1936
(defun pg-pbrpm-erase-buffer-menu 61,1966
(defun pg-pbrpm-menu-change-hook 68,2150
(defun pg-pbrpm-create-reset-buffer-menu 86,2726
(defun pg-pbrpm-analyse-goal-buffer 101,3355
(defun pg-pbrpm-button-action 161,5765
(defun pg-pbrpm-exists 168,5991
(defun pg-pbrpm-eliminate-id 172,6103
(defun pg-pbrpm-build-menu 180,6349
(defun pg-pbrpm-setup-span 253,8976
(defun pg-pbrpm-run-command 313,11294
(defun pg-pbrpm-get-pos-info 342,12604
(defun pg-pbrpm-get-region-info 384,13911
(defun pg-pbrpm-auto-select-around-point 395,14325
(defun pg-pbrpm-translate-position 410,14855
(defun pg-pbrpm-process-click 418,15113
(defvar pg-pbrpm-remember-region-selected-region 438,16138
(defvar pg-pbrpm-regions-list 439,16192
(defun pg-pbrpm-erase-regions-list 441,16228
(defun pg-pbrpm-filter-regions-list 450,16536
(defface pg-pbrpm-multiple-selection-face457,16799
(defface pg-pbrpm-menu-input-face465,17001
(defun pg-pbrpm-do-remember-region 473,17191
(defun pg-pbrpm-remember-region-drag-up-hook 494,18039
(defun pg-pbrpm-remember-region-click-hook 498,18210
(defun pg-pbrpm-remember-region 503,18395
(defun pg-pbrpm-process-region 517,19110
(defun pg-pbrpm-process-regions-list 535,19839
(defun pg-pbrpm-region-expression 539,20022

generic/pg-pgip.el,2889
(defalias 'pg-pgip-debug pg-pgip-debug
35,919
(defalias 'pg-pgip-error pg-pgip-error
36,960
(defalias 'pg-pgip-warning pg-pgip-warning
37,995
(defconst pg-pgip-version-supported 39,1045
(defun pg-pgip-process-packet 43,1151
(defvar pg-pgip-last-seen-id 53,1723
(defvar pg-pgip-last-seen-seq 54,1757
(defun pg-pgip-process-pgip 56,1793
(defun pg-pgip-process-msg 75,2724
(defvar pg-pgip-post-process-functions89,3294
(defun pg-pgip-post-process 99,3782
(defun pg-pgip-process-askpgip 115,4393
(defun pg-pgip-process-usespgip 121,4598
(defun pg-pgip-process-usespgml 125,4762
(defun pg-pgip-process-pgmlconfig 129,4926
(defun pg-pgip-process-proverinfo 145,5543
(defun pg-pgip-process-hasprefs 162,6208
(defun pg-pgip-haspref 176,6840
(defun pg-pgip-process-prefval 195,7616
(defun pg-pgip-process-guiconfig 222,8325
(defvar proof-assistant-idtables 229,8442
(defun pg-pgip-process-ids 232,8559
(defun pg-complete-idtable-symbol 258,9635
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
263,9727
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
264,9783
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
265,9839
(defun pg-pgip-process-idvalue 268,9897
(defun pg-pgip-process-menuadd 280,10233
(defun pg-pgip-process-menudel 283,10276
(defun pg-pgip-process-ready 292,10509
(defun pg-pgip-process-cleardisplay 295,10550
(defun pg-pgip-process-proofstate 309,11007
(defun pg-pgip-process-normalresponse 313,11084
(defun pg-pgip-process-errorresponse 317,11208
(defun pg-pgip-process-scriptinsert 321,11331
(defun pg-pgip-process-metainforesponse 326,11465
(defun pg-pgip-process-informfileloaded 335,11706
(defun pg-pgip-process-informfileretracted 341,11972
(defun pg-pgip-process-brokerstatus 354,12449
(defun pg-pgip-process-proveravailmsg 357,12497
(defun pg-pgip-process-newprovermsg 360,12547
(defun pg-pgip-process-proverstatusmsg 363,12595
(defvar pg-pgip-srcids 372,12842
(defun pg-pgip-process-newfile 376,12949
(defun pg-pgip-process-filestatus 392,13537
(defun pg-pgip-process-newobj 412,14192
(defun pg-pgip-process-delobj 415,14234
(defun pg-pgip-process-objectstatus 418,14276
(defun pg-pgip-process-parsescript 432,14631
(defun pg-pgip-get-pgiptype 455,15506
(defun pg-pgip-default-for 475,16299
(defun pg-pgip-subst-for 488,16694
(defun pg-pgip-interpret-value 500,17037
(defun pg-pgip-interpret-choice 518,17722
(defun pg-pgip-string-of-command 549,18739
(defconst pg-pgip-id566,19500
(defvar pg-pgip-refseq 572,19780
(defvar pg-pgip-refid 574,19877
(defvar pg-pgip-seq 577,19969
(defun pg-pgip-assemble-packet 579,20033
(defun pg-pgip-issue 597,20845
(defun pg-pgip-maybe-askpgip 614,21457
(defun pg-pgip-askprefs 620,21648
(defun pg-pgip-askids 624,21762
(defun pg-pgip-reset 637,22050
(defconst pg-pgip-start-element-regexp 668,22748
(defconst pg-pgip-end-element-regexp 669,22800

generic/pg-response.el,1182
(deflocal pg-response-eagerly-raise 31,730
(define-derived-mode proof-response-mode 41,955
(defun proof-response-config-done 67,2079
(defvar pg-response-special-display-regexp 88,2854
(defconst proof-multiframe-specifiers96,3260
(defun proof-map-multiple-frame-specifiers 105,3617
(defconst proof-multiframe-parameters116,4139
(defun proof-multiple-frames-enable 125,4438
(defun proof-three-window-enable 143,5082
(defun proof-select-three-b 147,5146
(defun proof-display-three-b 162,5615
(defvar pg-frame-configuration 176,6107
(defun pg-cache-frame-configuration 180,6254
(defun proof-layout-windows 184,6425
(defun proof-delete-other-frames 225,8248
(defvar pg-response-erase-flag 256,9338
(defun pg-response-maybe-erase260,9467
(defun pg-response-display 291,10652
(defun pg-response-display-with-face 310,11500
(defun pg-response-clear-displays 346,12730
(defun proof-next-error 365,13317
(defun pg-response-has-error-location 446,16233
(defvar proof-trace-last-fontify-pos 469,17066
(defun proof-trace-fontify-pos 471,17109
(defun proof-trace-buffer-display 479,17422
(defun proof-trace-buffer-finish 503,18394
(defun pg-thms-buffer-clear 524,18974

generic/pg-thymodes.el,152
(defmacro pg-defthymode 23,499
(defmacro pg-do-unless-null 71,2307
(defun pg-symval 76,2394
(defun pg-modesym 82,2549
(defun pg-modesymval 86,2663

generic/pg-user.el,3127
(defmacro proof-maybe-save-point 31,805
(defun proof-maybe-follow-locked-end 39,1007
(defun proof-assert-next-command-interactive 53,1372
(defun proof-process-buffer 63,1743
(defun proof-undo-last-successful-command 77,2060
(defun proof-undo-and-delete-last-successful-command 82,2222
(defun proof-undo-last-successful-command-1 104,3193
(defun proof-retract-buffer 120,3758
(defun proof-retract-current-goal 129,4038
(defun proof-interrupt-process 148,4544
(defun proof-goto-command-start 175,5533
(defun proof-goto-command-end 198,6473
(defun proof-mouse-goto-point 223,7251
(defun proof-mouse-track-insert 239,7883
(defvar proof-minibuffer-history 275,9020
(defun proof-minibuffer-cmd 278,9115
(defun proof-frob-locked-end 326,10909
(defmacro proof-if-setting-configured 387,12839
(defmacro proof-define-assistant-command 395,13108
(defmacro proof-define-assistant-command-witharg 408,13563
(defun proof-issue-new-command 428,14386
(defun proof-cd-sync 473,15881
(defun proof-electric-terminator-enable 532,17640
(defun proof-electric-term-incomment-fn 540,17935
(defun proof-process-electric-terminator 560,18686
(defun proof-electric-terminator 587,19834
(defun proof-add-completions 609,20471
(defun proof-script-complete 629,21225
(defun pg-insert-last-output-as-comment 657,21816
(defun pg-copy-span-contents 688,23050
(defun pg-numth-span-higher-or-lower 705,23608
(defun pg-control-span-of 731,24354
(defun pg-move-span-contents 737,24558
(defun pg-fixup-children-spans 789,26738
(defun pg-move-region-down 799,27001
(defun pg-move-region-up 808,27294
(defun proof-forward-command 838,28132
(defun proof-backward-command 859,28853
(defun pg-pos-for-event 881,29204
(defun pg-span-for-event 893,29565
(defun pg-span-context-menu 897,29709
(defun pg-toggle-visibility 912,30164
(defun pg-create-in-span-context-menu 922,30486
(defun pg-span-undo 955,31830
(defun pg-goals-buffers-hint 1001,33240
(defun pg-slow-fontify-tracing-hint 1005,33422
(defun pg-response-buffers-hint 1009,33593
(defun pg-jump-to-end-hint 1019,33955
(defun pg-processing-complete-hint 1023,34086
(defun pg-next-error-hint 1040,34785
(defun pg-hint 1045,34937
(defun pg-identifier-under-mouse-query 1064,35606
(defun proof-imenu-enable 1110,37261
(defvar pg-input-ring 1143,38401
(defvar pg-input-ring-index 1146,38457
(defvar pg-stored-incomplete-input 1149,38528
(defun pg-previous-input 1152,38630
(defun pg-next-input 1166,39087
(defun pg-delete-input 1171,39209
(defun pg-get-old-input 1184,39547
(defun pg-restore-input 1198,39938
(defun pg-search-start 1209,40228
(defun pg-regexp-arg 1221,40720
(defun pg-search-arg 1233,41168
(defun pg-previous-matching-input-string-position 1247,41585
(defun pg-previous-matching-input 1274,42750
(defun pg-next-matching-input 1293,43586
(defvar pg-matching-input-from-input-string 1301,43969
(defun pg-previous-matching-input-from-input 1305,44083
(defun pg-next-matching-input-from-input 1323,44848
(defun pg-add-to-input-history 1334,45227
(defun pg-remove-from-input-history 1346,45680
(defun  pg-clear-input-ring 1357,46063

generic/pg-vars.el,1106
(defvar proof-assistant-cusgrp 20,379
(defvar proof-assistant-internals-cusgrp 26,641
(defvar proof-assistant 32,912
(defvar proof-assistant-symbol 37,1134
(defvar proof-mode-for-shell 50,1678
(defvar proof-mode-for-response 55,1870
(defvar proof-mode-for-goals 60,2097
(defvar proof-mode-for-script 65,2287
(defvar proof-ready-for-assistant-hook 70,2465
(defvar proof-shell-busy 80,2752
(defvar proof-included-files-list 85,2908
(defvar proof-script-buffer 107,3921
(defvar proof-previous-script-buffer 110,4013
(defvar proof-shell-buffer 114,4184
(defvar proof-goals-buffer 117,4270
(defvar proof-response-buffer 120,4325
(defvar proof-trace-buffer 123,4386
(defvar proof-thms-buffer 127,4540
(defvar proof-shell-error-or-interrupt-seen 131,4695
(defvar pg-response-next-error 136,4919
(defvar proof-shell-proof-completed 139,5026
(defvar proof-terminal-string 151,5570
(defvar proof-shell-last-output 161,5760
(defvar proof-assistant-settings 165,5901
(defvar pg-tracing-slow-mode 172,6264
(defvar proof-nesting-depth 175,6353
(defvar proof-last-theorem-dependencies 182,6588

generic/pg-xml.el,1141
(defalias 'pg-xml-error pg-xml-error
24,625
(defun pg-xml-parse-string 47,1267
(defun pg-xml-parse-buffer 58,1593
(defun pg-xml-get-attr 80,2326
(defun pg-xml-child-elts 88,2628
(defun pg-xml-child-elt 93,2833
(defun pg-xml-get-child 101,3115
(defun pg-xml-get-text-content 111,3487
(defmacro pg-xml-attr 122,3837
(defmacro pg-xml-node 124,3899
(defconst pg-xml-header127,3991
(defun pg-xml-string-of 131,4067
(defun pg-xml-output-internal 142,4434
(defun pg-xml-cdata 176,5584
(defun pg-pgip-get-icon 184,5777
(defsubst pg-pgip-get-name 188,5925
(defsubst pg-pgip-get-version 191,6042
(defsubst pg-pgip-get-descr 194,6165
(defsubst pg-pgip-get-thmname 197,6284
(defsubst pg-pgip-get-thyname 200,6407
(defsubst pg-pgip-get-url 203,6530
(defsubst pg-pgip-get-srcid 206,6645
(defsubst pg-pgip-get-proverid 209,6764
(defsubst pg-pgip-get-symname 212,6889
(defsubst pg-pgip-get-prefcat 215,7009
(defsubst pg-pgip-get-default 218,7137
(defsubst pg-pgip-get-objtype 221,7260
(defsubst pg-pgip-get-value 224,7383
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
227,7453
(defun pg-pgip-get-pgmltext 229,7512

generic/proof-config.el,11008
(defgroup proof-user-options 85,3024
(defun proof-set-value 94,3221
(defcustom proof-electric-terminator-enable 127,4340
(defcustom proof-toolbar-enable 139,4872
(defcustom proof-imenu-enable 145,5045
(defcustom pg-show-hints 151,5216
(defcustom proof-output-fontify-enable 156,5351
(defcustom proof-trace-output-slow-catchup 166,5734
(defcustom proof-strict-state-preserving 176,6231
(defcustom proof-strict-read-only 189,6840
(defcustom proof-allow-undo-in-read-only 198,7189
(defcustom proof-three-window-enable 206,7570
(defcustom proof-multiple-frames-enable 225,8320
(defcustom proof-delete-empty-windows 234,8653
(defcustom proof-shrink-windows-tofit 245,9184
(defcustom proof-toolbar-use-button-enablers 252,9456
(defcustom proof-query-file-save-when-activating-scripting260,9791
(defcustom proof-one-command-per-line276,10511
(defcustom proof-prog-name-ask283,10738
(defcustom proof-prog-name-guess289,10898
(defcustom proof-tidy-response297,11157
(defcustom proof-keep-response-history311,11620
(defcustom pg-input-ring-size 321,12008
(defcustom proof-general-debug 326,12160
(defcustom proof-experimental-features 336,12532
(defcustom proof-follow-mode 350,13067
(defcustom proof-auto-action-when-deactivating-scripting 374,14247
(defcustom proof-script-command-separator 397,15196
(defcustom proof-rsh-command 405,15488
(defcustom proof-disappearing-proofs 421,16038
(defgroup proof-faces 448,16684
(defconst pg-defface-window-systems 453,16790
(defmacro proof-face-specs 465,17307
(defface proof-queue-face481,17827
(defface proof-locked-face489,18105
(defface proof-declaration-name-face502,18608
(defface proof-tacticals-name-face511,18894
(defface proof-tactics-name-face520,19156
(defface proof-error-face529,19421
(defface proof-warning-face537,19627
(defface proof-eager-annotation-face546,19884
(defface proof-debug-message-face554,20102
(defface proof-boring-face562,20301
(defface proof-mouse-highlight-face570,20493
(defface proof-highlight-dependent-face578,20689
(defface proof-highlight-dependency-face586,20898
(defface proof-active-area-face594,21095
(defconst proof-face-compat-doc 604,21486
(defconst proof-queue-face 605,21566
(defconst proof-locked-face 606,21634
(defconst proof-declaration-name-face 607,21704
(defconst proof-tacticals-name-face 608,21794
(defconst proof-tactics-name-face 609,21880
(defconst proof-error-face 610,21962
(defconst proof-warning-face 611,22030
(defconst proof-eager-annotation-face 612,22102
(defconst proof-debug-message-face 613,22192
(defconst proof-boring-face 614,22276
(defconst proof-mouse-highlight-face 615,22346
(defconst proof-highlight-dependent-face 616,22434
(defconst proof-highlight-dependency-face 617,22530
(defconst proof-active-area-face 618,22628
(defgroup prover-config 628,22769
(defcustom proof-guess-command-line 670,24080
(defcustom proof-assistant-home-page 685,24575
(defcustom proof-context-command 691,24745
(defcustom proof-info-command 696,24879
(defcustom proof-showproof-command 703,25150
(defcustom proof-goal-command 708,25286
(defcustom proof-save-command 716,25583
(defcustom proof-find-theorems-command 724,25892
(defcustom proof-assistant-true-value 731,26202
(defcustom proof-assistant-false-value 737,26392
(defcustom proof-assistant-format-int-fn 743,26586
(defcustom proof-assistant-format-string-fn 750,26835
(defcustom proof-assistant-setting-format 757,27102
(defgroup proof-script 779,27797
(defcustom proof-terminal-char 784,27927
(defcustom proof-script-sexp-commands 794,28314
(defcustom proof-script-command-end-regexp 805,28771
(defcustom proof-script-command-start-regexp 823,29590
(defcustom proof-script-use-old-parser 834,30051
(defcustom proof-script-integral-proofs 846,30537
(defcustom proof-script-fly-past-comments 861,31193
(defcustom proof-script-parse-function 866,31364
(defcustom proof-script-comment-start 884,32007
(defcustom proof-script-comment-start-regexp 895,32444
(defcustom proof-script-comment-end 903,32761
(defcustom proof-script-comment-end-regexp 915,33183
(defcustom pg-insert-output-as-comment-fn 923,33494
(defcustom proof-string-start-regexp 929,33746
(defcustom proof-string-end-regexp 934,33911
(defcustom proof-case-fold-search 939,34072
(defcustom proof-save-command-regexp 948,34482
(defcustom proof-save-with-hole-regexp 953,34592
(defcustom proof-save-with-hole-result 965,35046
(defcustom proof-goal-command-regexp 975,35497
(defcustom proof-goal-with-hole-regexp 984,35885
(defcustom proof-goal-with-hole-result 996,36326
(defcustom proof-non-undoables-regexp 1005,36713
(defcustom proof-nested-undo-regexp 1016,37168
(defcustom proof-ignore-for-undo-count 1032,37880
(defcustom proof-script-next-entity-regexps 1040,38183
(defcustom proof-script-find-next-entity-fn1084,39918
(defcustom proof-script-imenu-generic-expression 1104,40756
(defcustom proof-goal-command-p 1122,41609
(defcustom proof-really-save-command-p 1149,43046
(defcustom proof-completed-proof-behaviour 1161,43508
(defcustom proof-count-undos-fn 1189,44864
(defconst proof-no-command 1201,45413
(defcustom proof-find-and-forget-fn 1206,45618
(defcustom proof-forget-id-command 1223,46330
(defcustom pg-topterm-goalhyplit-fn 1233,46688
(defcustom proof-kill-goal-command 1245,47223
(defcustom proof-undo-n-times-cmd 1259,47724
(defcustom proof-nested-goals-history-p 1273,48272
(defcustom proof-state-preserving-p 1282,48609
(defcustom proof-activate-scripting-hook 1292,49079
(defcustom proof-deactivate-scripting-hook 1311,49858
(defcustom proof-indent 1324,50223
(defcustom proof-indent-hang 1329,50330
(defcustom proof-indent-enclose-offset 1334,50456
(defcustom proof-indent-open-offset 1339,50598
(defcustom proof-indent-close-offset 1344,50735
(defcustom proof-indent-any-regexp 1349,50873
(defcustom proof-indent-inner-regexp 1354,51033
(defcustom proof-indent-enclose-regexp 1359,51187
(defcustom proof-indent-open-regexp 1364,51341
(defcustom proof-indent-close-regexp 1369,51493
(defcustom proof-script-font-lock-keywords 1375,51647
(defcustom proof-script-syntax-table-entries 1383,51976
(defcustom proof-script-span-context-menu-extensions 1401,52373
(defgroup proof-shell 1427,53133
(defcustom proof-prog-name 1437,53304
(defcustom proof-shell-auto-terminate-commands 1448,53722
(defcustom proof-shell-pre-sync-init-cmd 1457,54119
(defcustom proof-shell-init-cmd 1471,54677
(defcustom proof-shell-restart-cmd 1482,55146
(defcustom proof-shell-quit-cmd 1487,55301
(defcustom proof-shell-quit-timeout 1492,55468
(defcustom proof-shell-cd-cmd 1502,55916
(defcustom proof-shell-start-silent-cmd 1519,56581
(defcustom proof-shell-stop-silent-cmd 1528,56955
(defcustom proof-shell-silent-threshold 1537,57288
(defcustom  proof-shell-inform-file-processed-cmd 1545,57622
(defcustom  proof-shell-inform-file-retracted-cmd 1566,58544
(defcustom proof-auto-multiple-files 1594,59810
(defcustom proof-cannot-reopen-processed-files 1609,60531
(defcustom proof-shell-require-command-regexp 1623,61197
(defcustom proof-done-advancing-require-function 1634,61659
(defcustom proof-shell-quiet-errors 1640,61894
(defcustom proof-shell-prompt-pattern 1653,62228
(defcustom proof-shell-wakeup-char 1663,62649
(defcustom proof-shell-annotated-prompt-regexp 1669,62880
(defcustom proof-shell-abort-goal-regexp 1685,63514
(defcustom proof-shell-error-regexp 1690,63649
(defcustom proof-shell-truncate-before-error 1710,64443
(defcustom pg-next-error-regexp 1724,64986
(defcustom pg-next-error-filename-regexp 1739,65595
(defcustom pg-next-error-extract-filename 1763,66628
(defcustom proof-shell-interrupt-regexp 1770,66871
(defcustom proof-shell-proof-completed-regexp 1784,67462
(defcustom proof-shell-clear-response-regexp 1797,67970
(defcustom proof-shell-clear-goals-regexp 1804,68269
(defcustom proof-shell-start-goals-regexp 1811,68562
(defcustom proof-shell-end-goals-regexp 1819,68929
(defcustom proof-shell-eager-annotation-start 1825,69171
(defcustom proof-shell-eager-annotation-start-length 1848,70191
(defcustom proof-shell-eager-annotation-end 1859,70617
(defcustom proof-shell-assumption-regexp 1875,71292
(defcustom proof-shell-process-file 1885,71695
(defcustom proof-shell-retract-files-regexp 1907,72651
(defcustom proof-shell-compute-new-files-list 1916,72987
(defcustom pg-use-specials-for-fontify 1928,73535
(defcustom pg-special-char-regexp 1936,73883
(defcustom proof-shell-set-elisp-variable-regexp 1942,74028
(defcustom proof-shell-match-pgip-cmd 1975,75539
(defcustom proof-shell-issue-pgip-cmd 1984,75868
(defcustom proof-shell-query-dependencies-cmd 1993,76224
(defcustom proof-shell-theorem-dependency-list-regexp 2000,76484
(defcustom proof-shell-theorem-dependency-list-split 2016,77144
(defcustom proof-shell-show-dependency-cmd 2025,77567
(defcustom proof-shell-identifier-under-mouse-cmd 2032,77836
(defcustom proof-shell-trace-output-regexp 2055,78917
(defcustom proof-shell-thms-output-regexp 2069,79375
(defcustom proof-shell-unicode 2082,79761
(defcustom proof-shell-filename-escapes 2090,80081
(defcustom proof-shell-process-connection-type2107,80761
(defcustom proof-shell-strip-crs-from-input 2130,81807
(defcustom proof-shell-strip-crs-from-output 2142,82292
(defcustom proof-shell-insert-hook 2150,82660
(defcustom proof-shell-handle-delayed-output-hook2190,84617
(defcustom proof-shell-handle-error-or-interrupt-hook2196,84832
(defcustom proof-shell-pre-interrupt-hook2214,85581
(defcustom proof-shell-process-output-system-specific 2222,85853
(defcustom proof-state-change-hook 2241,86717
(defcustom proof-shell-font-lock-keywords 2252,87099
(defcustom proof-shell-syntax-table-entries 2260,87431
(defgroup proof-goals 2278,87803
(defcustom pg-subterm-first-special-char 2283,87924
(defcustom pg-subterm-anns-use-stack 2291,88236
(defcustom pg-goals-change-goal 2300,88535
(defcustom pbp-goal-command 2305,88651
(defcustom pbp-hyp-command 2310,88807
(defcustom pg-subterm-help-cmd 2315,88969
(defcustom pg-goals-error-regexp 2322,89205
(defcustom proof-shell-result-start 2327,89365
(defcustom proof-shell-result-end 2333,89599
(defcustom pg-subterm-start-char 2339,89812
(defcustom pg-subterm-sep-char 2353,90392
(defcustom pg-subterm-end-char 2359,90571
(defcustom pg-topterm-regexp 2365,90728
(defcustom proof-goals-font-lock-keywords 2382,91330
(defcustom proof-resp-font-lock-keywords 2396,92015
(defcustom pg-before-fontify-output-hook 2408,92595
(defcustom pg-after-fontify-output-hook 2416,92955
(defgroup proof-x-symbol 2428,93235
(defcustom proof-xsym-extra-modes 2433,93363
(defcustom proof-xsym-font-lock-keywords 2446,93991
(defcustom proof-xsym-activate-command 2454,94368
(defcustom proof-xsym-deactivate-command 2461,94603
(defcustom proof-general-name 2478,94888
(defcustom proof-general-home-page2483,95045
(defcustom proof-unnamed-theorem-name2489,95205
(defcustom proof-universal-keys2495,95389

generic/proof-depends.el,824
(defvar proof-thm-names-of-files 23,624
(defvar proof-def-names-of-files 29,908
(defun proof-depends-module-name-for-buffer 38,1212
(defun proof-depends-module-of 48,1654
(defun proof-depends-names-in-same-file 56,1948
(defun proof-depends-process-dependencies 75,2568
(defun proof-dependency-in-span-context-menu 128,4317
(defun proof-dep-alldeps-menu 151,5220
(defun proof-dep-make-alldeps-menu 157,5447
(defun proof-dep-split-deps 175,5943
(defun proof-dep-make-submenu 196,6642
(defun proof-make-highlight-depts-menu 206,6995
(defun proof-goto-dependency 216,7299
(defun proof-show-dependency 222,7522
(defconst pg-dep-span-priority 229,7812
(defconst pg-ordinary-span-priority 230,7848
(defun proof-highlight-depcs 232,7890
(defun proof-highlight-depts 242,8320
(defun proof-dep-unhighlight 253,8794

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table16,543
(defun proof-easy-config-define-derived-modes 23,949
(defun proof-easy-config-check-setup 56,2359
(defmacro proof-easy-config 88,3694

generic/proof-indent.el,219
(defun proof-indent-indent 14,411
(defun proof-indent-offset 23,677
(defun proof-indent-inner-p 40,1277
(defun proof-indent-goto-prev 49,1584
(defun proof-indent-calculate 56,1917
(defun proof-indent-line 76,2639

generic/proof-maths-menu.el,134
(defun proof-maths-menu-support-available 31,994
(defun proof-maths-menu-set-global 42,1423
(defun proof-maths-menu-enable 56,1879

generic/proof-menu.el,2101
(defvar proof-display-some-buffers-count 17,437
(defun proof-display-some-buffers 19,482
(defun proof-menu-define-keys 78,2684
(defun proof-menu-define-main 141,5720
(defvar proof-menu-favourites 150,5908
(defun proof-menu-define-specific 154,6030
(defun proof-assistant-menu-update 192,7056
(defvar proof-help-menu208,7639
(defvar proof-show-hide-menu216,7917
(defvar proof-buffer-menu225,8230
(defun proof-keep-response-history 286,10398
(defconst proof-quick-opts-menu294,10708
(defun proof-quick-opts-vars 437,16385
(defun proof-quick-opts-changed-from-defaults-p 462,17136
(defun proof-quick-opts-changed-from-saved-p 466,17241
(defun proof-quick-opts-save 477,17593
(defun proof-quick-opts-reset 482,17761
(defconst proof-config-menu494,18029
(defconst proof-advanced-menu501,18208
(defvar proof-menu 514,18643
(defun proof-main-menu 523,18927
(defun proof-aux-menu 534,19193
(defun proof-menu-define-favourites-menu 550,19540
(defun proof-def-favourite 570,20196
(defvar proof-make-favourite-cmd-history 593,21171
(defvar proof-make-favourite-menu-history 596,21256
(defun proof-save-favourites 599,21342
(defun proof-del-favourite 604,21490
(defun proof-read-favourite 621,22051
(defun proof-add-favourite 646,22854
(defvar proof-menu-settings 673,23905
(defun proof-menu-define-settings-menu 676,23979
(defun proof-menu-entry-name 696,24723
(defun proof-menu-entry-for-setting 708,25195
(defun proof-settings-vars 726,25685
(defun proof-settings-changed-from-defaults-p 731,25862
(defun proof-settings-changed-from-saved-p 735,25968
(defun proof-settings-save 739,26071
(defun proof-settings-reset 744,26238
(defun proof-defpacustom-fn 751,26483
(defmacro defpacustom 827,29367
(defun proof-assistant-invisible-command-ifposs 842,30194
(defun proof-maybe-askprefs 864,31169
(defun proof-assistant-settings-cmd 871,31373
(defvar proof-assistant-format-table 888,32033
(defun proof-assistant-format-bool 896,32402
(defun proof-assistant-format-int 899,32515
(defun proof-assistant-format-string 902,32607
(defun proof-assistant-format 905,32705

generic/proof-mmm.el,114
(defun proof-mmm-support-available 34,1131
(defun proof-mmm-set-global 58,1979
(defun proof-mmm-enable 73,2520

generic/proof-script.el,5112
(defvar proof-element-counters 28,718
(deflocal proof-active-buffer-fake-minor-mode 34,858
(deflocal proof-script-buffer-file-name 37,984
(deflocal pg-script-portions 44,1394
(defun proof-next-element-count 54,1630
(defun proof-element-id 63,1957
(defun proof-next-element-id 67,2126
(deflocal proof-script-last-entity 81,2443
(defun proof-script-find-next-entity 88,2723
(deflocal proof-locked-span 164,5465
(deflocal proof-queue-span 171,5731
(defun proof-span-read-only 183,6245
(defun proof-strict-read-only 190,6502
(defsubst proof-set-locked-endpoints 219,7693
(defsubst proof-detach-queue 223,7837
(defsubst proof-detach-locked 227,7969
(defsubst proof-set-queue-start 231,8105
(defsubst proof-set-locked-end 235,8231
(defsubst proof-set-queue-end 248,8716
(defun proof-init-segmentation 259,9013
(defun proof-restart-buffers 292,10408
(defun proof-script-buffers-with-spans 314,11340
(defun proof-script-remove-all-spans-and-deactivate 324,11696
(defun proof-script-clear-queue-spans 328,11884
(defun proof-unprocessed-begin 347,12445
(defun proof-script-end 355,12699
(defun proof-queue-or-locked-end 364,13000
(defun proof-locked-end 379,13678
(defun proof-locked-region-full-p 396,14063
(defun proof-locked-region-empty-p 405,14335
(defun proof-only-whitespace-to-locked-region-p 409,14485
(defun proof-in-locked-region-p 422,15121
(defun proof-goto-end-of-locked 434,15384
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 451,16143
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 462,16624
(defun proof-end-of-locked-visible-p 476,17277
(defun proof-goto-end-of-queue-or-locked-if-not-visible 485,17728
(defvar pg-idioms 504,18378
(defvar pg-visibility-specs 507,18474
(defconst pg-default-invisibility-spec 512,18681
(defun pg-clear-script-portions 516,18821
(defun pg-add-script-element 530,19298
(defun pg-remove-script-element 533,19374
(defsubst pg-visname 541,19652
(defun pg-add-element 545,19797
(defun pg-open-invisible-span 579,21426
(defun pg-remove-element 590,21789
(defun pg-make-element-invisible 597,22059
(defun pg-make-element-visible 603,22316
(defun pg-toggle-element-visibility 608,22495
(defun pg-redisplay-for-gnuemacs 616,22825
(defun pg-show-all-portions 623,23096
(defun pg-show-all-proofs 641,23767
(defun pg-hide-all-proofs 646,23895
(defun pg-add-proof-element 651,24026
(defun pg-span-name 665,24646
(defvar pg-span-context-menu-keymap686,25353
(defun pg-set-span-helphighlights 699,25724
(defun proof-complete-buffer-atomic 727,26653
(defun proof-register-possibly-new-processed-file 768,28568
(defun proof-inform-prover-file-retracted 819,30696
(defun proof-auto-retract-dependencies 838,31482
(defun proof-unregister-buffer-file-name 892,34022
(defun proof-protected-process-or-retract 938,35845
(defun proof-deactivate-scripting-auto 965,37015
(defun proof-deactivate-scripting 974,37373
(defun proof-activate-scripting 1111,42778
(defun proof-toggle-active-scripting 1233,48210
(defun proof-done-advancing 1274,49571
(defun proof-done-advancing-comment 1369,53219
(defun proof-done-advancing-save 1388,53961
(defun proof-make-goalsave 1481,57576
(defun proof-get-name-from-goal 1496,58319
(defun proof-done-advancing-autosave 1515,59345
(defun proof-done-advancing-other 1580,61891
(defun proof-segment-up-to-parser 1608,62850
(defun proof-script-generic-parse-find-comment-end 1671,64940
(defun proof-script-generic-parse-cmdend 1680,65356
(defun proof-script-generic-parse-cmdstart 1705,66251
(defun proof-script-generic-parse-sexp 1768,68959
(defun proof-cmdstart-add-segment-for-cmd 1792,69895
(defun proof-segment-up-to-cmdstart 1844,72108
(defun proof-segment-up-to-cmdend 1905,74468
(defun proof-semis-to-vanillas 1977,77147
(defun proof-script-new-command-advance 2016,78473
(defun proof-script-next-command-advance 2058,80214
(defun proof-assert-until-point-interactive 2070,80655
(defun proof-assert-until-point 2096,81777
(defun proof-assert-next-command2149,84209
(defun proof-goto-point 2197,86472
(defun proof-insert-pbp-command 2215,87013
(defun proof-insert-sendback-command 2229,87482
(defun proof-done-retracting 2255,88372
(defun proof-setup-retract-action 2291,89858
(defun proof-last-goal-or-goalsave 2301,90341
(defun proof-retract-target 2324,91181
(defun proof-retract-until-point-interactive 2409,94822
(defun proof-retract-until-point 2417,95207
(define-derived-mode proof-mode 2460,96956
(defun proof-script-set-visited-file-name 2510,98883
(defun proof-script-set-buffer-hooks 2534,99885
(defun proof-script-kill-buffer-fn 2542,100303
(defun proof-config-done-related 2586,102125
(defun proof-generic-goal-command-p 2656,104603
(defun proof-generic-state-preserving-p 2661,104815
(defun proof-generic-count-undos 2670,105332
(defun proof-generic-find-and-forget 2699,106362
(defconst proof-script-important-settings2750,108187
(defun proof-config-done 2765,108740
(defun proof-setup-parsing-mechanism 2853,111858
(defun proof-setup-imenu 2897,113711
(defun proof-setup-func-menu 2914,114316

generic/proof-shell.el,3311
(defvar proof-marker 28,649
(defvar proof-action-list 31,746
(defvar proof-shell-silent 39,922
(defvar proof-shell-last-prompt 46,1213
(defvar proof-shell-last-output-kind 50,1384
(defvar proof-shell-delayed-output 71,2206
(defvar proof-shell-delayed-output-kind 74,2327
(defcustom proof-shell-active-scripting-indicator83,2530
(defun proof-shell-ready-prover 135,3998
(defun proof-shell-live-buffer 149,4538
(defun proof-shell-available-p 156,4773
(defun proof-grab-lock 162,4996
(defun proof-release-lock 179,5708
(defcustom proof-shell-fiddle-frames 199,6259
(defun proof-shell-set-text-representation 205,6482
(defun proof-shell-start 216,6944
(defvar proof-shell-kill-function-hooks 426,14491
(defun proof-shell-kill-function 429,14589
(defun proof-shell-clear-state 518,18392
(defun proof-shell-exit 533,18835
(defun proof-shell-bail-out 545,19280
(defun proof-shell-restart 554,19757
(defvar proof-shell-no-response-display 596,21141
(defvar proof-shell-urgent-message-marker 599,21245
(defvar proof-shell-urgent-message-scanner 602,21366
(defun proof-shell-handle-output 606,21493
(defun proof-shell-handle-delayed-output 649,23186
(defvar proof-shell-no-error-display 677,24229
(defun proof-shell-handle-error 683,24433
(defun proof-shell-handle-interrupt 701,25269
(defun proof-shell-error-or-interrupt-action 715,25882
(defun proof-goals-pos 740,27027
(defun proof-pbp-focus-on-first-goal 745,27232
(defsubst proof-shell-string-match-safe 757,27762
(defun proof-shell-process-output 762,27930
(defvar proof-shell-insert-space-fudge 873,32570
(defun proof-shell-insert 883,32889
(defun proof-shell-command-queue-item 956,35841
(defun proof-shell-set-silent 961,35998
(defun proof-shell-start-silent-item 967,36217
(defun proof-shell-clear-silent 973,36409
(defun proof-shell-stop-silent-item 979,36631
(defun proof-shell-should-be-silent 986,36903
(defun proof-append-alist 999,37459
(defun proof-start-queue 1058,39696
(defun proof-extend-queue 1069,40045
(defun proof-shell-exec-loop 1078,40424
(defun proof-shell-insert-loopback-cmd 1143,43012
(defun proof-shell-message 1171,44338
(defun proof-shell-process-urgent-message 1177,44554
(defun proof-shell-strip-eager-annotations 1309,49819
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1320,50155
(defun proof-shell-minibuffer-urgent-interactive-input 1322,50225
(defun proof-shell-process-urgent-messages 1332,50584
(defun proof-shell-filter 1406,53683
(defun proof-shell-filter-process-output 1567,60316
(defvar pg-last-tracing-output-time 1620,62370
(defconst pg-slow-mode-duration 1623,62476
(defconst pg-fast-tracing-mode-threshold 1626,62558
(defvar pg-tracing-cleanup-timer 1629,62686
(defun pg-tracing-tight-loop 1631,62725
(defun pg-finish-tracing-display 1674,64443
(defun proof-shell-dont-show-annotations 1687,64749
(defun proof-shell-show-annotations 1703,65270
(defun proof-shell-wait 1725,65797
(defun proof-done-invisible 1744,66706
(defun proof-shell-invisible-command 1750,66878
(defun proof-shell-invisible-cmd-get-result 1784,68143
(defun proof-shell-invisible-command-invisible-result 1802,68839
(define-derived-mode proof-shell-mode 1821,69269
(defconst proof-shell-important-settings1891,71935
(defun proof-shell-config-done 1897,72050

generic/proof-site.el,504
(defconst proof-assistant-table-default23,727
(defconst proof-general-short-version 61,2143
(defconst proof-general-version-year 67,2331
(defgroup proof-general 74,2484
(defgroup proof-general-internals 79,2592
(defun proof-home-directory-fn 92,2980
(defcustom proof-home-directory103,3351
(defcustom proof-images-directory112,3718
(defcustom proof-info-directory118,3920
(defcustom proof-assistant-table145,5066
(defcustom proof-assistants 180,6182
(defun proof-ready-for-assistant 208,7327

generic/proof-splash.el,726
(defcustom proof-splash-enable 17,319
(defcustom proof-splash-time 22,471
(defcustom proof-splash-contents30,756
(defconst proof-splash-startup-msg 58,1775
(defconst proof-splash-welcome 67,2154
(defun proof-get-image 86,2701
(defvar proof-splash-timeout-conf 125,4052
(defun proof-splash-centre-spaces 128,4165
(defun proof-splash-remove-screen 156,5335
(defun proof-splash-remove-buffer 176,6056
(defvar proof-splash-seen 192,6720
(defun proof-splash-display-screen 196,6837
(defun proof-splash-message 271,9991
(defun proof-splash-timeout-waiter 284,10435
(defvar proof-splash-old-frame-title-format 300,11131
(defun proof-splash-set-frame-titles 302,11181
(defun proof-splash-unset-frame-titles 311,11497

generic/proof-syntax.el,981
(defun proof-ids-to-regexp 17,530
(defun proof-anchor-regexp 23,786
(defconst proof-no-regexp27,888
(defun proof-regexp-alt 32,983
(defun proof-regexp-region 41,1269
(defun proof-re-search-forward-region 50,1692
(defun proof-search-forward 63,2187
(defun proof-replace-regexp-in-string 69,2439
(defun proof-re-search-forward 75,2693
(defun proof-re-search-backward 81,2954
(defun proof-string-match 87,3218
(defun proof-string-match-safe 93,3450
(defun proof-stringfn-match 97,3655
(defun proof-looking-at 104,3915
(defun proof-looking-at-safe 110,4105
(defun proof-looking-at-syntactic-context 114,4245
(defsubst proof-replace-string 126,4608
(defsubst proof-replace-regexp 131,4812
(defsubst proof-replace-regexp-nocasefold 136,5021
(defvar proof-id 144,5303
(defun proof-ids 150,5523
(defun proof-zap-commas 163,6084
(defun proof-format 181,6653
(defun proof-format-filename 200,7292
(defun proof-insert 249,8770
(defun proof-splice-separator 286,9794

generic/proof-toolbar.el,2874
(defun proof-toolbar-function 42,1325
(defun proof-toolbar-icon 45,1422
(defun proof-toolbar-enabler 48,1523
(defun proof-toolbar-function-with-enabler 51,1631
(defun proof-toolbar-make-icon 58,1804
(defun proof-toolbar-make-toolbar-item 76,2404
(defvar proof-toolbar 115,3780
(deflocal proof-toolbar-itimer 119,3909
(defun proof-toolbar-setup 123,4019
(defun proof-toolbar-build 166,5562
(defalias 'proof-toolbar-enable proof-toolbar-enable
231,7760
(defun proof-toolbar-setup-refresh 242,8064
(defun proof-toolbar-disable-refresh 263,8885
(deflocal proof-toolbar-refresh-flag 271,9275
(defun proof-toolbar-refresh 277,9546
(defvar proof-toolbar-enablers281,9691
(defvar proof-toolbar-enablers-last-state287,9867
(defun proof-toolbar-really-refresh 291,9958
(defun proof-toolbar-undo-enable-p 346,11852
(defalias 'proof-toolbar-undo proof-toolbar-undo
351,12000
(defun proof-toolbar-delete-enable-p 357,12119
(defalias 'proof-toolbar-delete proof-toolbar-delete
363,12293
(defun proof-toolbar-lockedend-enable-p 370,12429
(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
373,12479
(defun proof-toolbar-next-enable-p 382,12567
(defalias 'proof-toolbar-next proof-toolbar-next
386,12674
(defun proof-toolbar-goto-enable-p 393,12768
(defalias 'proof-toolbar-goto proof-toolbar-goto
396,12841
(defun proof-toolbar-retract-enable-p 403,12917
(defalias 'proof-toolbar-retract proof-toolbar-retract
407,13028
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
414,13107
(defalias 'proof-toolbar-use proof-toolbar-use
415,13175
(defun proof-toolbar-restart-enable-p 421,13253
(defalias 'proof-toolbar-restart proof-toolbar-restart
426,13414
(defun proof-toolbar-goal-enable-p 432,13492
(defalias 'proof-toolbar-goal proof-toolbar-goal
439,13725
(defun proof-toolbar-qed-enable-p 446,13797
(defalias 'proof-toolbar-qed proof-toolbar-qed
452,13949
(defun proof-toolbar-state-enable-p 458,14021
(defalias 'proof-toolbar-state proof-toolbar-state
461,14092
(defun proof-toolbar-context-enable-p 467,14161
(defalias 'proof-toolbar-context proof-toolbar-context
470,14234
(defun proof-toolbar-info-enable-p 478,14394
(defalias 'proof-toolbar-info proof-toolbar-info
481,14438
(defun proof-toolbar-command-enable-p 487,14507
(defalias 'proof-toolbar-command proof-toolbar-command
490,14578
(defun proof-toolbar-help-enable-p 496,14658
(defun proof-toolbar-help 499,14703
(defun proof-toolbar-find-enable-p 507,14797
(defalias 'proof-toolbar-find proof-toolbar-find
510,14866
(defun proof-toolbar-visibility-enable-p 516,14964
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
519,15064
(defun proof-toolbar-interrupt-enable-p 525,15152
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
528,15216
(defun proof-toolbar-make-menu-item 537,15405
(defun proof-toolbar-scripting-menu 560,16105

generic/proof-unicode-tokens.el,531
(defun proof-unicode-tokens-support-available 20,548
(defvar proof-unicode-tokens-initialised 29,921
(defun proof-unicode-tokens-init 32,1028
(defun proof-unicode-tokens-set-global 51,1563
(defun proof-unicode-tokens-enable 66,2079
(defun proof-token-name-alist 83,2768
(defun proof-shortcut-alist 98,3420
(defun proof-unicode-tokens-activate-prover 109,3756
(defun proof-unicode-tokens-deactivate-prover 116,3999
(defun proof-unicode-tokens-shell-config 125,4322
(defun proof-unicode-tokens-encode-shell-input 135,4719

generic/proof-utils.el,2116
(defmacro deflocal 63,1903
(defmacro proof-with-current-buffer-if-exists 70,2141
(deflocal proof-buffer-type 76,2351
(defmacro proof-with-script-buffer 82,2631
(defmacro proof-map-buffers 93,3018
(defmacro proof-sym 98,3203
(defsubst proof-try-require 103,3364
(defun proof-save-some-buffers 116,3695
(defmacro proof-ass-sym 165,5296
(defmacro proof-ass-symv 171,5555
(defmacro proof-ass 177,5813
(defun proof-defpgcustom-fn 183,6065
(defun undefpgcustom 204,6936
(defmacro defpgcustom 210,7160
(defun proof-defpgdefault-fn 221,7578
(defmacro defpgdefault 235,8036
(defmacro defpgfun 246,8398
(defmacro proof-eval-when-ready-for-assistant 256,8663
(defun proof-file-truename 269,9058
(defun proof-file-to-buffer 273,9241
(defun proof-files-to-buffers 284,9570
(defun proof-buffers-in-mode 291,9853
(defun pg-save-from-death 305,10303
(defun proof-define-keys 324,10920
(deflocal proof-font-lock-keywords 353,11919
(defun proof-font-lock-configure-defaults 359,12176
(defun proof-font-lock-clear-font-lock-vars 405,14327
(defun proof-font-lock-set-font-lock-vars 411,14539
(defun proof-fontify-region 415,14695
(defun pg-remove-specials 477,17097
(defun pg-remove-specials-in-string 487,17435
(defun proof-fontify-buffer 494,17622
(defun proof-warn-if-unset 507,17863
(defun proof-get-window-for-buffer 512,18081
(defun proof-display-and-keep-buffer 563,20389
(defun proof-clean-buffer 595,21696
(defun proof-message 610,22317
(defun proof-warning 615,22530
(defun pg-internal-warning 621,22812
(defun proof-debug 629,23131
(defun proof-switch-to-buffer 644,23802
(defun proof-resize-window-tofit 677,25491
(defun proof-submit-bug-report 777,29503
(defun proof-deftoggle-fn 813,30882
(defmacro proof-deftoggle 828,31535
(defun proof-defintset-fn 835,31909
(defmacro proof-defintset 851,32613
(defun proof-defstringset-fn 858,32990
(defmacro proof-defstringset 871,33616
(defmacro proof-defshortcut 885,34073
(defmacro proof-definvisible 900,34712
(defun pg-custom-save-vars 928,35689
(defun pg-custom-reset-vars 946,36412
(defun proof-locate-executable 959,36749

generic/proof-x-symbol.el,580
(defvar proof-x-symbol-initialized 52,2005
(defun proof-x-symbol-tokenlang-file 55,2100
(defun proof-x-symbol-support-maybe-available 61,2282
(defun proof-x-symbol-initialize 81,3011
(defun proof-x-symbol-enable 164,6277
(defun proof-x-symbol-refresh-output-buffers 186,7158
(defun proof-x-symbol-mode-associated-buffers 201,7900
(defun proof-x-symbol-decode-region 219,8438
(defun proof-x-symbol-encode-shell-input 240,9435
(defun proof-x-symbol-set-language 257,10026
(defun proof-x-symbol-shell-config 262,10197
(defun proof-x-symbol-config-output-buffer 309,12338

lib/bufhist.el,1100
(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 101,3514
(defun bufhist-restore-buffer-contents 113,3998
(defun bufhist-checkpoint 121,4285
(defun bufhist-erase-buffer 129,4654
(defun bufhist-checkpoint-and-erase 139,4999
(defun bufhist-switch-to-index 145,5185
(defun bufhist-first 184,6789
(defun bufhist-last 189,6948
(defun bufhist-prev 194,7094
(defun bufhist-next 202,7317
(defun bufhist-delete 207,7457
(defun bufhist-clear 219,8000
(defun bufhist-init 234,8396
(defun bufhist-exit 259,9333
(defun bufhist-set-readwrite 269,9597
(defun bufhist-before-change-function 284,10217
(defun bufhist-make-buttons 296,10633
(defconst bufhist-minor-mode-map314,11072
(define-minor-mode bufhist-mode326,11534
(defun bufhist-toggle-fn 346,12319

lib/holes.el,2448
(defvar holes-doc 37,1048
(defvar holes-default-hole 145,5031
(defvar holes-active-hole 149,5200
(defcustom holes-empty-hole-string 156,5409
(defcustom holes-empty-hole-regexp 159,5520
(defcustom holes-search-limit 166,5811
(defface active-hole-face178,6187
(defface inactive-hole-face190,6635
(defun holes-region-beginning-or-nil 205,7111
(defun holes-region-end-or-nil 210,7221
(defun holes-copy-active-region 215,7319
(defun holes-is-hole-p 222,7518
(defun holes-hole-start-position 228,7625
(defun holes-hole-end-position 235,7814
(defun holes-hole-buffer 242,7998
(defun holes-hole-at 249,8173
(defun holes-active-hole-exist-p 256,8348
(defun holes-active-hole-start-position 266,8606
(defun holes-active-hole-end-position 276,8978
(defun holes-active-hole-buffer 287,9347
(defun holes-goto-active-hole 298,9653
(defun holes-highlight-hole-as-active 310,9921
(defun holes-highlight-hole 320,10233
(defun holes-disable-active-hole 331,10525
(defun holes-set-active-hole 349,11068
(defun holes-is-in-hole-p 362,11414
(defun holes-make-hole 369,11557
(defun holes-make-hole-at 395,12303
(defun holes-clear-hole 415,12779
(defun holes-clear-hole-at 427,13068
(defun holes-map-holes 436,13327
(defun holes-mapcar-holes 444,13510
(defun holes-clear-all-buffer-holes 450,13682
(defun holes-next 461,13982
(defun holes-next-after-active-hole 468,14233
(defun holes-set-active-hole-next 476,14452
(defun holes-replace-segment 498,15005
(defun holes-replace 508,15359
(defun holes-replace-active-hole 539,16554
(defun holes-replace-update-active-hole 548,16855
(defun holes-delete-update-active-hole 569,17545
(defun holes-set-make-active-hole 576,17759
(defun holes-mouse-replace-active-hole 623,19484
(defun holes-destroy-hole 643,20023
(defun holes-hole-at-event 660,20434
(defun holes-mouse-destroy-hole 665,20547
(defun holes-mouse-forget-hole 675,20787
(defun holes-mouse-set-make-active-hole 691,21097
(defun holes-mouse-set-active-hole 713,21658
(defun holes-set-point-next-hole-destroy 725,21922
(defvar hole-map741,22372
(defvar holes-mode-map757,22992
(defun holes-replace-string-by-holes-backward 794,24457
(defun holes-skeleton-end-hook 812,25158
(defconst holes-jump-doc 821,25596
(defun holes-replace-string-by-holes-backward-jump 828,25803
(defun holes-abbrev-complete 845,26434
(defun holes-insert-and-expand 854,26741
(defvar holes-mode 865,27173
(defun holes-mode 871,27369

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,827
(defun local-vars-list-insert-empty-zone 44,1391
(defun local-vars-list-find 82,2099
(defun local-vars-list-goto-var 101,2874
(defun local-vars-list-get-current 127,3924
(defun local-vars-list-set-current 148,4774
(defun local-vars-list-get 171,5491
(defun local-vars-list-get-safe 188,6023
(defun local-vars-list-set 193,6217

lib/maths-menu.el,153
(defun maths-menu-build-menu 51,2136
(defvar maths-menu-menu70,2804
(defvar maths-menu-mode-map315,11762
(define-minor-mode maths-menu-mode323,11981

lib/pg-dev.el,75
(defconst pg-dev-lisp-font-lock-keywords36,1102
(defun unload-pg 70,2039

lib/proof-compat.el,751
(defvar proof-running-on-win32 29,913
(defun pg-custom-undeclare-variable 49,1708
(defun subst-char-in-string 139,4496
(defun replace-regexp-in-string 154,5085
(defconst menuvisiblep 216,7798
(defun set-window-text-height 233,8411
(defmacro save-selected-frame 259,9361
(defun warn 298,10658
(defun redraw-modeline 305,10913
(defun proof-buffer-syntactic-context-emulate 316,11351
(defvar read-shell-command-map349,12658
(defun read-shell-command 367,13346
(defun remassq 379,13827
(defun remassoc 391,14216
(defun frames-of-buffer 404,14661
(defmacro with-selected-window 443,15923
(defun pg-pop-to-buffer 486,17301
(defun process-live-p 537,19163
(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
556,19778

lib/span.el,137
(defsubst span-delete-spans 22,479
(defsubst span-property-safe 26,643
(defsubst span-set-start 30,782
(defsubst span-set-end 34,914

lib/span-extent.el,1015
(defsubst span-make 12,367
(defsubst span-detach 16,489
(defsubst span-set-endpoints 20,576
(defsubst span-set-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 span-delete 49,1470
(defsubst span-mapcar-spans 55,1641
(defsubst spans-at-region-prop 59,1852
(defsubst span-at 63,2040
(defsubst span-at-before 67,2157
(defsubst span-start 72,2354
(defsubst span-end 76,2483
(defsubst prev-span 80,2606
(defsubst next-span 84,2752
(defsubst span-live-p 88,2894
(defun span-raise 96,3166
(defalias 'span-object span-object
100,3265
(defalias 'span-string span-string
101,3304
(defsubst make-detached-span 104,3390
(defsubst span-buffer 109,3452
(defsubst span-detached-p 114,3544
(defsubst set-span-face 119,3656
(defsubst fold-spans 123,3751
(defsubst set-span-properties 127,3948
(defsubst set-span-keymap 131,4056
(defsubst span-at-event 136,4200

lib/span-overlay.el,1206
(defalias 'span-start span-start
12,370
(defalias 'span-end span-end
13,408
(defalias 'span-set-property span-set-property
14,442
(defalias 'span-property span-property
15,485
(defalias 'span-make span-make
16,524
(defalias 'span-detach span-detach
17,560
(defalias 'span-set-endpoints span-set-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 77,2865
(defsubst span-delete 83,3079
(defsubst span-mapcar-spans 90,3301
(defun span-at-before 94,3510
(defun prev-span 111,4236
(defun next-span 117,4387
(defsubst span-live-p 146,5612
(defun span-raise 152,5778
(defalias 'span-object span-object
158,6021
(defun span-string 160,6062
(defun set-span-properties 166,6244
(defun span-find-span 178,6499
(defsubst span-at-event 185,6806
(defun make-detached-span 189,6927
(defun fold-spans 194,7023
(defsubst span-detached-p 209,7557
(defsubst set-span-face 213,7672
(defun set-span-keymap 217,7769

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3034
(defun texi-docstring-magic-splice-sep 93,3199
(defconst texi-docstring-magic-munge-table103,3504
(defun texi-docstring-magic-untabify 193,7271
(defun texi-docstring-magic-munge-docstring 203,7586
(defun texi-docstring-magic-texi 242,8873
(defun texi-docstring-magic-format-default 255,9313
(defun texi-docstring-magic-texi-for 271,9948
(defconst texi-docstring-magic-comment329,11908
(defun texi-docstring-magic 335,12062
(defun texi-docstring-magic-face-at-point 369,13142
(defun texi-docstring-magic-insert-magic 384,13665

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,348
(defun unicode-chars-list-chars 5050,245960

lib/unicode-tokens.el,1484
(defvar unicode-tokens-charref-format 51,1831
(defvar unicode-tokens-token-format 54,1928
(defvar unicode-tokens-token-name-alist 57,2019
(defvar unicode-tokens-glyph-list 60,2112
(defvar unicode-tokens-token-prefix 64,2256
(defvar unicode-tokens-token-suffix 67,2340
(defvar unicode-tokens-token-match 70,2422
(defvar unicode-tokens-hexcode-match 73,2507
(defvar unicode-tokens-shortcut-alist76,2614
(defvar unicode-tokens-max-token-length 86,2852
(defvar unicode-tokens-codept-charname-alist 89,2951
(defvar unicode-tokens-token-alist 92,3059
(defvar unicode-tokens-ustring-alist 95,3142
(defun unicode-tokens-insert-char 103,3245
(defun unicode-tokens-insert-string 113,3666
(defun unicode-tokens-character-insert 123,4043
(defun unicode-tokens-token-insert 145,4951
(defun unicode-tokens-replace-token-after 166,5848
(defun unicode-tokens-looking-backward-at 188,6597
(defun unicode-tokens-electric-suffix 199,7059
(defvar unicode-tokens-rotate-glyph-last-char 245,8623
(defun unicode-tokens-rotate-glyph-forward 247,8675
(defun unicode-tokens-rotate-glyph-backward 276,9857
(defun unicode-tokens-map-ordering 296,10435
(defun unicode-tokens-quail-define-rules 300,10585
(defvar unicode-tokens-format-entry347,12191
(defun unicode-tokens-tokens-to-unicode 355,12413
(defun unicode-tokens-unicode-to-tokens 366,12787
(defvar unicode-tokens-mode-map 380,13100
(define-minor-mode unicode-tokens-mode383,13197
(defun unicode-tokens-initialise 407,13965

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

mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2675
(defun mmm-autoload-class 89,3438
(defvar mmm-changed-buffers-list 129,5005
(defun mmm-major-mode-change 132,5112
(defun mmm-check-changed-buffers 145,5633
(defun mmm-mode-on-maybe 155,6006
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6424
(defun mmm-add-find-file-hook 168,6484

mmm/mmm-class.el,416
(defun mmm-get-class-spec 42,1295
(defun mmm-get-class-parameter 59,2008
(defun mmm-set-class-parameter 63,2174
(defun* mmm-apply-class75,2538
(defun* mmm-apply-classes90,3176
(defun* mmm-apply-all 110,3942
(defun* mmm-ify124,4389
(defun* mmm-match-region206,7472
(defun mmm-match->point 267,10161
(defun mmm-match-and-verify 281,10683
(defun mmm-get-form 307,11741
(defun mmm-default-get-form 318,12237

mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1209
(defun mmm-ify-region 63,1933
(defun mmm-ify-by-regexp75,2361
(defun mmm-parse-buffer 97,3037
(defun mmm-parse-region 106,3373
(defun mmm-parse-block 115,3752
(defun mmm-get-block 132,4503
(defun mmm-reparse-current-region 146,4834
(defun mmm-clear-current-region 167,5508
(defun mmm-clear-regions 172,5672
(defun mmm-clear-all-regions 177,5818
(defun* mmm-end-current-region 185,5978
(defun mmm-narrow-to-submode-region 220,7401
(defun mmm-insert-region 239,8015
(defun mmm-insert-by-key 258,8877
(defun mmm-get-insertion-spec 342,12437
(defun mmm-insertion-help 369,13516
(defun mmm-display-insertion-key 379,13886
(defun mmm-get-all-insertion-keys 401,14708

mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1312
(defvar mmm-keywords-used49,1615
(defmacro mmm-regexp-opt 91,2661
(defvar mmm-evaporate-property110,3310
(defmacro mmm-set-keymap-default 128,4076
(defmacro mmm-event-key 137,4518
(defvar skeleton-positions 146,4737
(defun mmm-fixup-skeleton 147,4768
(defmacro mmm-make-temp-buffer 159,5205
(defvar mmm-font-lock-available-p 172,5601
(defmacro mmm-set-font-lock-defaults 179,5815

mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1116
(defvar mmm-cweb-section-regexp41,1163
(defvar mmm-cweb-c-part-tags44,1253
(defvar mmm-cweb-c-part-regexp47,1312
(defun mmm-cweb-in-limbo 50,1396
(defun mmm-cweb-verify-brief-c 57,1621

mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1235
(defvar mmm-mason-pseudo-perl-tags45,1376
(defvar mmm-mason-non-perl-tags48,1452
(defvar mmm-mason-perl-tags-regexp51,1553
(defvar mmm-mason-pseudo-perl-tags-regexp56,1748
(defvar mmm-mason-tag-names-regexp61,1965
(defun mmm-mason-verify-inline 66,2185
(defun mmm-mason-start-line 156,5089
(defun mmm-mason-end-line 161,5154
(defun mmm-mason-set-mode-line 168,5248

mmm/mmm-mode.el,1024
(defun mmm-mode 101,3866
(defun mmm-mode-on 140,5371
(defun mmm-mode-off 181,7131
(defvar mmm-mode-map 206,7864
(defvar mmm-mode-prefix-map 209,7939
(defvar mmm-mode-menu-map 212,8049
(defun mmm-define-key 215,8140
(define-key mmm-mode-prefix-map 239,8895
(define-key mmm-mode-prefix-map 246,9153
(define-key mmm-mode-map 249,9264
(define-key mmm-mode-menu-map 252,9366
(define-key mmm-mode-menu-map 254,9438
(define-key mmm-mode-menu-map 256,9497
(define-key mmm-mode-menu-map 258,9578
(define-key mmm-mode-menu-map 260,9659
(define-key mmm-mode-menu-map 262,9746
(define-key mmm-mode-menu-map 265,9840
(define-key mmm-mode-menu-map 267,9900
(define-key mmm-mode-menu-map 270,9991
(define-key mmm-mode-menu-map 272,10051
(define-key mmm-mode-menu-map 274,10158
(define-key mmm-mode-menu-map 276,10243
(define-key mmm-mode-menu-map 279,10329
(define-key mmm-mode-menu-map 281,10389
(define-key mmm-mode-menu-map 283,10502
(define-key mmm-mode-menu-map 285,10587
(define-key mmm-mode-map 288,10670

mmm/mmm-noweb.el,1291
(defvar mmm-noweb-code-mode 44,1352
(defvar mmm-noweb-quote-mode 50,1649
(defvar mmm-noweb-quote-string 54,1806
(defvar mmm-noweb-quote-number 58,1929
(defvar mmm-noweb-narrowing 62,2045
(defun mmm-noweb-chunk 68,2176
(defun mmm-noweb-quote 84,2876
(defun mmm-noweb-quote-name 89,3042
(defun mmm-noweb-chunk-name 95,3302
(defun mmm-noweb-regions 140,4748
(defun mmm-noweb-narrow-to-doc-chunk 166,5616
(defun mmm-noweb-fill-chunk 189,6386
(defun mmm-noweb-fill-paragraph-chunk 208,7070
(defun mmm-noweb-fill-named-chunk 222,7487
(defun mmm-noweb-auto-fill-doc-chunk 238,8064
(defun mmm-noweb-auto-fill-doc-mode 246,8283
(defun mmm-noweb-auto-fill-code-mode 251,8473
(defun mmm-noweb-complete-chunk 259,8685
(defvar mmm-noweb-chunk-history 292,9689
(defun mmm-noweb-goto-chunk 295,9767
(defun mmm-noweb-goto-next 307,10091
(defun mmm-noweb-goto-previous 319,10448
(defvar mmm-noweb-map 336,10852
(defvar mmm-noweb-prefix-map 337,10896
(define-key mmm-noweb-map 338,10947
(define-key mmm-noweb-prefix-map 347,11390
(defun mmm-noweb-bind-keys 352,11656
(defun mmm-syntax-region-list 368,12070
(defun mmm-syntax-other-regions 377,12426
(defun mmm-word-other-regions 389,12897
(defun mmm-space-other-regions 395,13066
(defun mmm-undo-syntax-other-regions 401,13237

mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1748
(defun mmm-overlays-at 59,1933
(defun mmm-included-p 72,2386
(defun mmm-overlays-containing 112,3875
(defun mmm-overlays-contained-in 125,4313
(defun mmm-overlays-overlapping 138,4753
(defun mmm-sort-overlays 149,5116
(defvar mmm-current-overlay 158,5386
(defvar mmm-previous-overlay 163,5601
(defvar mmm-current-submode 168,5789
(defvar mmm-previous-submode 173,5989
(defun mmm-update-current-submode 178,6162
(defun mmm-set-current-submode 199,6978
(defun mmm-submode-at 210,7470
(defun mmm-match-front 219,7745
(defun mmm-match-back 238,8506
(defun mmm-front-start 257,9251
(defun mmm-back-end 265,9555
(defun mmm-valid-submode-region 278,9902
(defun* mmm-make-region305,11058
(defun mmm-make-overlay 431,16429
(defun mmm-get-face 459,17562
(defun mmm-clear-overlays 470,17854
(defun mmm-update-mode-info 486,18321
(defun mmm-update-submode-region 571,22606
(defun mmm-add-hooks 588,23364
(defun mmm-remove-hooks 592,23499
(defun mmm-get-local-variables-list 598,23626
(defun mmm-get-locals 618,24546
(defun mmm-get-saved-local 631,25127
(defun mmm-set-local-variables 635,25292
(defun mmm-get-saved-local-variables 646,25733
(defun mmm-save-changed-local-variables 654,26050
(defun mmm-clear-local-variables 673,26908
(defun mmm-enable-font-lock 684,27187
(defun mmm-update-font-lock-buffer 692,27447
(defun mmm-refontify-maybe 705,27879
(defun mmm-submode-changes-in 720,28401
(defun mmm-regions-in 731,28849
(defun mmm-regions-alist 745,29419
(defun mmm-fontify-region 762,30065
(defun mmm-fontify-region-list 782,31096
(defun mmm-beginning-of-syntax 804,32012

mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1617
(defvar mmm-rpm-sh-end-tags53,1841
(defvar mmm-rpm-sh-start-regexp57,2015
(defvar mmm-rpm-sh-end-regexp61,2193

mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2614
(defun mmm-here-doc-get-mode 93,3099
(defun mmm-file-variables-verify 208,6817
(defun mmm-file-variables-find-back 232,7853

mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 41,1309
(defmacro mmm-save-all 60,1953
(defun mmm-format-string 73,2242
(defun mmm-format-matches 84,2694
(defmacro mmm-save-keyword 107,3487
(defmacro mmm-save-keywords 115,3814
(defun mmm-looking-back-at 128,4347
(defun mmm-make-marker 145,4915

mmm/mmm-vars.el,2667
(defgroup mmm 99,3072
(defvar mmm-c-derived-modes106,3182
(defvar mmm-save-local-variables 110,3301
(defvar mmm-buffer-saved-locals 336,10161
(defvar mmm-region-saved-locals-defaults 341,10361
(defvar mmm-region-saved-locals-for-dominant 347,10621
(defgroup mmm-faces 357,10998
(defcustom mmm-submode-decoration-level 363,11169
(defface mmm-init-submode-face 381,12041
(defface mmm-cleanup-submode-face 385,12181
(defface mmm-declaration-submode-face 389,12318
(defface mmm-comment-submode-face 393,12464
(defface mmm-output-submode-face 397,12617
(defface mmm-special-submode-face 401,12766
(defface mmm-code-submode-face 405,12930
(defface mmm-default-submode-face 409,13069
(defface mmm-delimiter-face 414,13277
(defcustom mmm-mode-string 421,13403
(defcustom mmm-submode-mode-line-format 426,13534
(defvar mmm-primary-mode-display-name 443,14189
(defvar mmm-buffer-mode-display-name 448,14403
(defun mmm-set-mode-line 454,14702
(defvar mmm-classes 478,15510
(defvar mmm-global-classes 484,15755
(defcustom mmm-mode-ext-classes-alist 491,15937
(defun mmm-add-mode-ext-class 510,16755
(defcustom mmm-major-mode-preferences519,17080
(defun mmm-add-to-major-mode-preferences 537,17878
(defun mmm-ensure-modename 553,18664
(defun mmm-modename->function 562,18974
(defcustom mmm-delimiter-mode 576,19437
(defcustom mmm-mode-prefix-key 586,19706
(defcustom mmm-command-modifiers 591,19833
(defcustom mmm-insert-modifiers 605,20466
(defcustom mmm-use-old-command-keys 620,21144
(defun mmm-use-old-command-keys 630,21608
(defcustom mmm-mode-hook 638,21807
(defun mmm-run-constructed-hook 658,22614
(defun mmm-run-major-hook 666,23000
(defun mmm-run-submode-hook 669,23077
(defvar mmm-class-hooks-run 672,23164
(defun mmm-run-class-hook 677,23336
(defvar mmm-primary-mode-entry-hook 682,23508
(defcustom mmm-major-mode-hook 697,24155
(defun mmm-run-major-mode-hook 711,24786
(defcustom mmm-global-mode 724,25327
(defcustom mmm-never-modes740,26022
(defvar mmm-set-file-name-for-modes 758,26322
(defvar mmm-mode 769,26681
(defvar mmm-primary-mode 777,26889
(defvar mmm-classes-alist 788,27255
(defun mmm-add-classes 943,35462
(defun mmm-add-group 948,35627
(defun mmm-add-to-group 958,36077
(defconst mmm-version 972,36574
(defun mmm-version 975,36639
(defvar mmm-temp-buffer-name 982,36782
(defvar mmm-interactive-history 988,36912
(defun mmm-add-to-history 994,37181
(defun mmm-clear-history 997,37264
(defvar mmm-mode-ext-classes 1005,37449
(defun mmm-get-mode-ext-classes 1010,37660
(defun mmm-clear-mode-ext-classes 1019,38036
(defun mmm-mode-ext-applies 1023,38161
(defun mmm-get-all-classes 1037,38645

x-symbol/lisp/auto-autoloads.el,63
(defalias 'x-symbol-map-autoload x-symbol-map-autoload
23,974

x-symbol/lisp/x-symbol-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,9210
(defvar x-symbol-trace-invisible 52,2014
(defconst x-symbol-language-access-alist67,2529
(defstruct (x-symbol-generated179,8410
(defstruct (x-symbol-grammar190,8622
(defvar x-symbol-map 213,9450
(defvar x-symbol-unalias-alist 217,9577
(defvar x-symbol-latin-decode-alists 221,9694
(defvar x-symbol-context-atree 225,9879
(defvar x-symbol-electric-atree 229,9994
(defvar x-symbol-grid-alist 232,10088
(defvar x-symbol-menu-alist 235,10171
(defvar x-symbol-all-charsyms 238,10278
(defvar x-symbol-fancy-value-cache 243,10486
(defvar x-symbol-fchar-tables 247,10649
(defvar x-symbol-bchar-tables 250,10778
(defvar x-symbol-cstring-table 252,10814
(defvar x-symbol-fontified-cstring-table 254,10851
(defvar x-symbol-charsym-decode-obarray 256,10898
(defun x-symbol-set-variable 263,11127
(defun x-symbol-ensure-hashtable 277,11762
(defun x-symbol-puthash 284,12064
(defun x-symbol-call-function-or-regexp 292,12393
(defun x-symbol-match-in-alist 301,12793
(defun x-symbol-fancy-string 330,14017
(defun x-symbol-fancy-value 352,14934
(defun x-symbol-fancy-associations 371,15701
(defun x-symbol-language-value 400,16853
(defun x-symbol-charsym-face 414,17511
(defun x-symbol-image-available-p 427,18138
(defun x-symbol-default-context-info-ignore 432,18350
(defun x-symbol-default-info-keys-keymaps 446,19117
(defun x-symbol-alias-charsym 458,19592
(defun x-symbol-default-valid-charsym 467,19961
(defun x-symbol-next-valid-charsym 489,20998
(defun x-symbol-valid-context-charsym 516,22005
(defun x-symbol-next-valid-charsym-before 527,22604
(defun x-symbol-prefix-arg-texts 551,23661
(defun x-symbol-region-text 560,23956
(defun x-symbol-language-text 569,24252
(defun x-symbol-coding-text 577,24652
(defun x-symbol-language-modeline-text 595,25347
(defun x-symbol-coding-modeline-text 601,25583
(defun x-symbol-translate-to-ascii 647,27488
(defun x-symbol-package-web 681,28753
(defun x-symbol-package-info 688,28974
(defun x-symbol-package-bug 694,29135
(defun x-symbol-package-reply-to-report 745,31108
(defvar x-symbol-encode-rchars 765,31836
(defun x-symbol-even-escapes-before-p 773,32118
(defun x-symbol-decode-region 781,32297
(defun x-symbol-decode-all 794,32770
(defun x-symbol-decode-single-token 857,35838
(defun x-symbol-decode-lisp 866,36145
(defun x-symbol-encode-string 898,37612
(defun x-symbol-encode-all 909,37931
(defun x-symbol-encode-lisp 973,40966
(defun x-symbol-decode-recode 1009,42371
(defun x-symbol-decode 1039,43747
(defun x-symbol-encode-recode 1052,44338
(defun x-symbol-encode 1080,45614
(defun x-symbol-unalias 1096,46373
(defun x-symbol-copy-region-encoded 1161,49292
(defun x-symbol-yank-decoded 1189,50542
(defun x-symbol-update-modeline 1216,51642
(defun x-symbol-auto-coding-alist 1240,52497
(defun x-symbol-auto-8bit-search 1276,53658
(defvar x-symbol-font-family-postfixes1301,54448
(defvar x-symbol-font-lock-property-alist1304,54564
(defvar x-symbol-font-lock-keywords1308,54745
(defvar x-symbol-subscript-matcher 1335,55740
(defvar x-symbol-subscript-type 1339,55843
(defun x-symbol-subscripts-available-p 1342,55894
(defun x-symbol-font-lock-start 1348,56135
(defun x-symbol-match-subscript 1357,56521
(defun x-symbol-init-font-lock 1363,56734
(defun x-symbol-set-image 1395,58322
(defun x-symbol-mode-internal 1413,59068
(defun nuke-x-symbol 1487,62177
(defun x-symbol-options-filter 1500,62630
(defun x-symbol-extra-filter 1536,63786
(defun x-symbol-menu-filter 1544,64034
(defvar x-symbol-list-mode-map1574,65013
(defvar x-symbol-list-buffer 1600,66163
(defvar x-symbol-list-win-config 1602,66239
(defvar x-symbol-invisible-spec 1604,66350
(defvar x-symbol-itimer 1608,66500
(defvar x-symbol-invisible-display-table1611,66583
(defvar x-symbol-invisible-font 1620,66819
(defvar x-symbol-charsym-info-cache 1645,68006
(defvar x-symbol-language-info-caches 1647,68097
(defvar x-symbol-coding-info-cache 1649,68191
(defvar x-symbol-keys-info-cache 1651,68280
(defun x-symbol-list-bury 1659,68585
(defun x-symbol-list-restore 1665,68781
(defun x-symbol-list-store 1695,69999
(defun x-symbol-list-mode 1704,70416
(defun x-symbol-list-scroll 1725,71218
(defun x-symbol-init-language-interactive 1748,71860
(defun x-symbol-list-menu 1765,72574
(defun x-symbol-list-selected 1820,74482
(defun x-symbol-list-menu-selected 1846,75691
(defun x-symbol-list-mouse-selected 1857,76144
(defun x-symbol-charsym-info 1874,76866
(defun x-symbol-language-info 1888,77467
(defun x-symbol-coding-info 1920,78667
(defun x-symbol-keys-info 1940,79439
(defun x-symbol-info 1964,80362
(defun x-symbol-list-info 1977,80900
(defun x-symbol-highlight-echo 1991,81443
(defun x-symbol-point-info 2002,81992
(defun x-symbol-hide-revealed-at-point 2048,83914
(defun x-symbol-reveal-invisible 2085,85581
(defun x-symbol-show-info-and-invisible 2133,87773
(defun x-symbol-start-itimer-once 2169,89315
(defun x-symbol-setup-minibuffer 2185,89941
(defvar x-symbol-language-history 2203,90512
(defvar x-symbol-token-history 2206,90636
(defvar x-symbol-last-abbrev 2209,90712
(defvar x-symbol-electric-pos 2211,90808
(defvar x-symbol-command-keys 2214,90890
(defvar x-symbol-help-keys 2218,91021
(defvar x-symbol-help-language 2220,91116
(defvar x-symbol-help-completions 2222,91215
(defvar x-symbol-help-completions1 2224,91307
(defun x-symbol-map-default-binding 2232,91583
(defun x-symbol-read-charsym-token 2263,92661
(defun x-symbol-insert-command 2289,93584
(defun x-symbol-read-language 2340,95591
(defun x-symbol-read-token 2355,96269
(defun x-symbol-read-token-direct 2394,97778
(defun x-symbol-grid 2406,98178
(defun x-symbol-replace-from 2494,101794
(defvar x-symbol-token-search-prelude-size 2530,103295
(defun x-symbol-replace-token 2532,103343
(defun x-symbol-match-token-before 2557,104434
(defun x-symbol-token-input 2601,106237
(defun x-symbol-modify-key 2622,107067
(defun x-symbol-rotate-key 2655,108396
(defun x-symbol-electric-input 2709,110606
(defun x-symbol-help-mapper 2751,112307
(defun x-symbol-help-output 2774,113146
(defun x-symbol-help 2817,114742
(defvar x-symbol-face-docstrings2870,116811
(defvar x-symbol-all-key-prefixes 2876,116999
(defvar x-symbol-all-key-chain-alist 2878,117110
(defvar x-symbol-all-horizontal-chain-alist 2880,117209
(defvar x-symbol-all-chain-subchains-alist 2882,117322
(defvar x-symbol-all-exclusive-context-alist 2884,117436
(defalias 'x-symbol-table-grouping x-symbol-table-grouping
2892,117732
(defalias 'x-symbol-table-aspects x-symbol-table-aspects
2893,117773
(defalias 'x-symbol-table-score x-symbol-table-score
2894,117814
(defalias 'x-symbol-table-input x-symbol-table-input
2895,117854
(defsubst x-symbol-table-prefixes 2896,117895
(defsubst x-symbol-table-junk 2897,117946
(defsubst x-symbol-charsym-defined-p 2899,117997
(defun x-symbol-try-font-name-0 2907,118298
(defun x-symbol-try-font-name 2925,118854
(defun x-symbol-set-cstrings 2942,119370
(defun x-symbol-init-charsym-command 2987,121348
(defun x-symbol-init-charsym-input 2995,121714
(defun x-symbol-init-charsym-aspects 3064,124432
(defun x-symbol-init-cset 3094,125712
(defun x-symbol-make-atree 3244,132535
(defun x-symbol-atree-push 3248,132615
(defun x-symbol-component-root-p 3268,133304
(defun x-symbol-component-elements 3272,133443
(defun x-symbol-component-merge 3279,133691
(defun x-symbol-component-space 3293,134239
(defun x-symbol-modify-less-than 3307,134823
(defun x-symbol-inherit-aspects 3312,135046
(defun x-symbol-compute-aspects 3321,135485
(defun x-symbol-init-aspects 3337,136203
(defun x-symbol-sort-modify-chain 3382,138252
(defun x-symbol-init-horizontal/key-alist 3397,138824
(defun x-symbol-init-exclusive-alist 3413,139570
(defun x-symbol-init-horizontal-chain 3451,141174
(defun x-symbol-init-exclusive-chain 3459,141506
(defun x-symbol-init-rotate-chain 3466,141833
(defun x-symbol-init-context-atree 3487,142707
(defun x-symbol-init-key-bindings 3532,144990
(defun x-symbol-rotate-modify-less-than 3555,145913
(defun x-symbol-subgroup-less-than 3563,146308
(defun x-symbol-header-charsyms 3568,146565
(defun x-symbol-init-grid/menu 3594,147615
(defun x-symbol-init-input 3666,150271
(defun x-symbol-init-latin-decoding 3796,156747
(defun x-symbol-get-prime-for 3837,158618
(defun x-symbol-alist-to-obarray 3846,158942
(defun x-symbol-alist-to-hash-table 3852,159150
(defun x-symbol-init-language 3862,159483
(defvar x-symbol-latin1-cset3986,164948
(defvar x-symbol-latin2-cset3992,165121
(defvar x-symbol-latin3-cset3998,165294
(defvar x-symbol-latin5-cset4004,165467
(defvar x-symbol-latin9-cset4010,165639
(defvar x-symbol-xsymb0-cset4016,165845
(defvar x-symbol-xsymb1-cset4022,166100
(defvar x-symbol-latin1-table4028,166342
(defvar x-symbol-latin2-table4129,170812
(defvar x-symbol-latin3-table4228,174013
(defvar x-symbol-latin5-table4327,176894
(defvar x-symbol-latin9-table4426,179204
(defvar x-symbol-xsymb0-table4525,181594
(defvar x-symbol-xsymb1-table4675,188990
(defvar x-symbol-no-of-charsyms 4883,199625
(defun x-symbol-mac-setup1 4891,199991
(defun x-symbol-mac-setup2 4909,200636
(defun x-symbol-startup 4935,201502

x-symbol/lisp/x-symbol-emacs.el,1126
(defun emacs-version>=33,1289
(defvar x-symbol-emacs-has-font-lock-with-props67,2953
(defvar x-symbol-emacs-has-correct-find-safe-coding87,3682
(defvar x-symbol-emacs-after-create-image-function102,4196
(defvar image-types 128,5053
(defvar init-file-loaded 164,6440
(defvar message-stack 167,6513
(defun region-active-p 250,9823
(defvar x-symbol-data-directory 287,11188
(defun x-symbol-directory-files 357,13465
(defun x-symbol-event-in-current-buffer 371,13853
(defun x-symbol-create-image 374,13902
(defun x-symbol-make-glyph 377,13987
(defun x-symbol-set-glyph-image 380,14058
(defvar x-symbol-heading-strut-glyph 395,14555
(defvar x-symbol-invisible-face 398,14642
(defvar x-symbol-face 399,14700
(defvar x-symbol-sub-face 400,14738
(defvar x-symbol-sup-face 401,14784
(defvar x-symbol-emacs-w32-font-directories403,14831
(defvar x-symbol-invisible-display-table 416,15309
(defalias 'x-symbol-window-width x-symbol-window-width
418,15356
(defun x-symbol-set-face-font 429,15852
(defun x-symbol-event-matches-key-specifier-p 440,16325
(defun start-itimer 450,16597
(defun itimer-live-p 452,16694

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,169
(defconst x-symbol-xsym-unicode-map	19,604
(defconst x-symbol-old-tables267,10039
(defconst x-symbol-unicode-table283,10470
(defconst x-symbol-unicode-cset299,10973

x-symbol/lisp/x-symbol-unicode-extras.el,40
(defconst x-symol-unicode-extras13,263

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,5509
@node Top167,5089
@node Preface204,6217
@node Latest news for version 3.7Latest news for version 3.7
227,6813
@node Future269,8735
@node Credits300,10034
@node Introducing Proof GeneralIntroducing Proof General
406,13803
@node Installing Proof GeneralInstalling Proof General
462,15845
@node Quick start guideQuick start guide
476,16294
@node Features of Proof GeneralFeatures of Proof General
520,18415
@node Supported proof assistantsSupported proof assistants
609,22352
@node Prerequisites for this manualPrerequisites for this manual
658,24258
@node Organization of this manualOrganization of this manual
702,25884
@node Basic Script ManagementBasic Script Management
728,26712
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
747,27312
@node Proof scriptsProof scripts
998,36965
@node Script buffersScript buffers
1041,39085
@node Locked queue and editing regionsLocked queue and editing regions
1063,39662
@node Goal-save sequencesGoal-save sequences
1119,41809
@node Active scripting bufferActive scripting buffer
1156,43295
@node Summary of Proof General buffersSummary of Proof General buffers
1225,46715
@node Script editing commandsScript editing commands
1287,49389
@node Script processing commandsScript processing commands
1365,52248
@node Proof assistant commandsProof assistant commands
1493,57549
@node Toolbar commandsToolbar commands
1659,63328
@node Interrupting during trace outputInterrupting during trace output
1683,64257
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1722,66181
@node Goals buffer commandsGoals buffer commands
1736,66681
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1825,70220
@node Visibility of completed proofsVisibility of completed proofs
1857,71432
@node Switching between proof scriptsSwitching between proof scripts
1912,73355
@node View of processed files View of processed files 
1949,75327
@node Retracting across filesRetracting across files
2009,78378
@node Asserting across filesAsserting across files
2022,79009
@node Automatic multiple file handlingAutomatic multiple file handling
2035,79575
@node Escaping script managementEscaping script management
2060,80609
@node Editing featuresEditing features
2118,82812
@node Experimental featuresExperimental features
2182,85484
@node Support for other PackagesSupport for other Packages
2216,86748
@node Syntax highlightingSyntax highlighting
2249,87643
@node X-Symbol supportX-Symbol support
2288,89264
@node Unicode supportUnicode support
2346,91804
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2461,96601
@node Support for outline modeSupport for outline mode
2520,98731
@node Support for completionSupport for completion
2546,99861
@node Support for tagsSupport for tags
2604,102037
@node Customizing Proof GeneralCustomizing Proof General
2656,104366
@node Basic optionsBasic options
2696,106036
@node How to customizeHow to customize
2720,106794
@node Display customizationDisplay customization
2771,108896
@node User optionsUser options
2896,114134
@node Changing facesChanging faces
3168,123833
@node Tweaking configuration settingsTweaking configuration settings
3243,126502
@node Hints and TipsHints and Tips
3300,129028
@node Adding your own keybindingsAdding your own keybindings
3319,129629
@node Using file variablesUsing file variables
3375,132162
@node Using abbreviationsUsing abbreviations
3434,134348
@node LEGO Proof GeneralLEGO Proof General
3473,135764
@node LEGO specific commandsLEGO specific commands
3514,137133
@node LEGO tagsLEGO tags
3534,137588
@node LEGO customizationsLEGO customizations
3544,137835
@node Coq Proof GeneralCoq Proof General
3576,138754
@node Coq-specific commandsCoq-specific commands
3592,139163
@node Coq-specific variablesCoq-specific variables
3614,139670
@node Editing multiple proofsEditing multiple proofs
3636,140328
@node User-loaded tacticsUser-loaded tactics
3660,141436
@node Holes featureHoles feature
3724,143910
@node Isabelle Proof GeneralIsabelle Proof General
3751,145197
@node Isabelle commandsIsabelle commands
3781,146327
@node Logics and SettingsLogics and Settings
3926,150484
@node Isabelle customizationsIsabelle customizations
3960,152024
@node HOL Proof GeneralHOL Proof General
3984,152506
@node Shell Proof GeneralShell Proof General
4026,154328
@node Obtaining and InstallingObtaining and Installing
4062,155787
@node Obtaining Proof GeneralObtaining Proof General
4078,156200
@node Installing Proof General from tarballInstalling Proof General from tarball
4109,157439
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4134,158271
@node Setting the names of binariesSetting the names of binaries
4149,158679
@node Notes for syssiesNotes for syssies
4177,159619
@node Bugs and EnhancementsBugs and Enhancements
4252,162655
@node References4273,163470
@node History of Proof GeneralHistory of Proof General
4313,164494
@node Old News for 3.0Old News for 3.0
4404,168596
@node Old News for 3.1Old News for 3.1
4474,172290
@node Old News for 3.2Old News for 3.2
4500,173462
@node Old News for 3.3Old News for 3.3
4561,176465
@node Old News for 3.4Old News for 3.4
4580,177362
@node Function IndexFunction Index
4603,178418
@node Variable IndexVariable Index
4607,178494
@node Keystroke IndexKeystroke Index
4611,178574
@node Concept IndexConcept Index
4615,178640

doc/PG-adapting.texi,3776
@node Top157,4776
@node Introduction195,5921
@node Future236,7574
@node Credits272,9170
@node Beginning with a New ProverBeginning with a New Prover
282,9462
@node Overview of adding a new proverOverview of adding a new prover
323,11411
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
401,14719
@node Major modes used by Proof GeneralMajor modes used by Proof General
470,18110
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
503,19461
@node Settings for generic user-level commandsSettings for generic user-level commands
518,20007
@node Menu configurationMenu configuration
563,21741
@node Toolbar configurationToolbar configuration
587,22658
@node Proof Script SettingsProof Script Settings
645,24900
@node Recognizing commands and commentsRecognizing commands and comments
667,25480
@node Recognizing proofsRecognizing proofs
788,30987
@node Recognizing other elementsRecognizing other elements
900,35800
@node Configuring undo behaviourConfiguring undo behaviour
1026,41311
@node Nested proofsNested proofs
1163,46705
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1203,48331
@node Activate scripting hookActivate scripting hook
1226,49277
@node Automatic multiple filesAutomatic multiple files
1250,50140
@node Completions1272,50987
@node Proof Shell SettingsProof Shell Settings
1313,52476
@node Proof shell commandsProof shell commands
1344,53758
@node Script input to the shellScript input to the shell
1508,60697
@node Settings for matching various output from proof processSettings for matching various output from proof process
1575,63737
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1706,69486
@node Hooks and other settingsHooks and other settings
1921,79357
@node Goals Buffer SettingsGoals Buffer Settings
2002,82726
@node Splash Screen SettingsSplash Screen Settings
2079,85825
@node Global ConstantsGlobal Constants
2105,86583
@node Handling Multiple FilesHandling Multiple Files
2131,87424
@node Configuring Editing SyntaxConfiguring Editing Syntax
2283,95207
@node Configuring Font LockConfiguring Font Lock
2342,97328
@node Configuring X-SymbolConfiguring X-Symbol
2429,101613
@node Writing More Lisp CodeWriting More Lisp Code
2489,104133
@node Default values for generic settingsDefault values for generic settings
2506,104778
@node Adding prover-specific configurationsAdding prover-specific configurations
2536,105861
@node Useful variablesUseful variables
2579,107143
@node Useful functions and macrosUseful functions and macros
2594,107642
@node Internals of Proof GeneralInternals of Proof General
2697,111597
@node Spans2725,112505
@node Proof General site configurationProof General site configuration
2738,112879
@node Configuration variable mechanismsConfiguration variable mechanisms
2818,115925
@node Global variablesGlobal variables
2939,121355
@node Proof script modeProof script mode
3009,123903
@node Proof shell modeProof shell mode
3268,135558
@node Debugging3675,151640
@node Plans and IdeasPlans and Ideas
3718,152516
@node Proof by pointing and similar featuresProof by pointing and similar features
3739,153238
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3777,154896
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3822,157121
@node Demonstration InstantiationsDemonstration Instantiations
3852,158152
@node demoisa-easy.el3868,158583
@node demoisa.el3931,160821
@node Function IndexFunction Index
4086,165805
@node Variable IndexVariable Index
4090,165881
@node Concept IndexConcept Index
4099,166060

x-symbol/lisp/_pkg.el,0

x-symbol/lisp/custom-load.el,0

lib/holes-load.el,0

generic/proof.el,0

generic/proof-autoloads.el,0

twelf/x-symbol-twelf.el,0

pgshell/pgshell.el,0

lego/x-symbol-lego.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