From 49c33ad595b0cdcf91e5368e25e26f6743824a73 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 27 Jan 2008 14:52:23 +0000 Subject: Updated. --- COMPATIBILITY | 4 +- TAGS | 1102 +++++++++++++++++++++++++++++---------------------------- 2 files changed, 569 insertions(+), 537 deletions(-) diff --git a/COMPATIBILITY b/COMPATIBILITY index c07a928b..64af7b6c 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -6,9 +6,9 @@ on Linux: Emacs 22.1.1 -- recommended and supported - Emacs 21.4.1 -- tested; works except X-Symbol sub/superscripts - XEmacs 21.4.XX -- tested + Emacs 21.4.1 -- tested; poorer X-Symbol sub/superscript support XEmacs 21.5 (beta28) -- tested; PG has workarounds for several bugs + XEmacs 21.4.XX -- tested and prover versions: diff --git a/TAGS b/TAGS index 66f800da..ce9cce75 100644 --- a/TAGS +++ b/TAGS @@ -185,7 +185,7 @@ coq/coq.el,6066 (defun is-not-split-vertic 1587,58739 (defun optim-resp-windows 1596,59178 -coq/coq-indent.el,2247 +coq/coq-indent.el,2259 (defconst coq-any-command-regexp17,315 (defconst coq-indent-inner-regexp20,406 (defconst coq-comment-start-regexp 31,794 @@ -214,30 +214,30 @@ coq/coq-indent.el,2247 (defconst coq-end-command-or-comment-start-regexp173,6813 (defun coq-find-not-in-comment-backward 177,6931 (defun coq-find-not-in-comment-forward 197,7832 -(defun coq-find-command-end-backward 217,8753 -(defun coq-find-command-end-forward 226,9144 -(defun coq-find-command-end 235,9521 -(defun coq-parse-function 244,9904 -(defun coq-find-current-start 253,10106 -(defun coq-find-real-start 262,10397 -(defun coq-command-at-point 269,10616 -(defun only-spaces-on-line 276,10893 -(defun coq-indent-find-reg 285,11164 -(defun coq-find-no-syntactic-on-line 299,11700 -(defun coq-back-to-indentation-prevline 312,12173 -(defun coq-find-unclosed 356,14087 -(defun coq-find-at-same-level-zero 386,15267 -(defun coq-find-unopened 414,16345 -(defun coq-find-last-unopened 457,17795 -(defun coq-end-offset 468,18192 -(defun coq-indent-command-offset 493,18983 -(defun coq-indent-expr-offset 540,20807 -(defun coq-indent-comment-offset 656,25510 -(defun coq-indent-offset 688,26957 -(defun coq-indent-calculate 706,27820 -(defun coq-indent-line 709,27908 -(defun coq-indent-line-not-comments 719,28274 -(defun coq-indent-region 729,28663 +(defun coq-find-command-end-backward 221,8974 +(defun coq-find-command-end-forward 230,9365 +(defun coq-find-command-end 239,9742 +(defun coq-parse-function 248,10125 +(defun coq-find-current-start 257,10327 +(defun coq-find-real-start 266,10618 +(defun coq-command-at-point 273,10837 +(defun coq-indent-only-spaces-on-line 280,11114 +(defun coq-indent-find-reg 286,11391 +(defun coq-find-no-syntactic-on-line 300,11927 +(defun coq-back-to-indentation-prevline 313,12400 +(defun coq-find-unclosed 357,14314 +(defun coq-find-at-same-level-zero 387,15615 +(defun coq-find-unopened 415,16780 +(defun coq-find-last-unopened 458,18230 +(defun coq-end-offset 469,18627 +(defun coq-indent-command-offset 494,19418 +(defun coq-indent-expr-offset 541,21242 +(defun coq-indent-comment-offset 657,25945 +(defun coq-indent-offset 689,27403 +(defun coq-indent-calculate 707,28266 +(defun coq-indent-line 710,28354 +(defun coq-indent-line-not-comments 720,28720 +(defun coq-indent-region 730,29109 coq/coq-local-vars.el,279 (defconst coq-local-vars-doc 17,306 @@ -364,41 +364,50 @@ demoisa/demoisa.el,349 (define-derived-mode demoisa-response-mode 127,4196 (define-derived-mode demoisa-goals-mode 131,4323 -isar/isabelle-system.el,1399 -(defgroup isabelle 26,775 -(defcustom isabelle-web-page30,903 -(defcustom isa-isatool-command41,1198 -(defvar isatool-not-found 68,2141 -(defun isa-set-isatool-command 71,2254 -(defun isa-shell-command-to-string 91,3115 -(defun isa-getenv 97,3339 -(defcustom isabelle-program-name116,4000 -(defvar isabelle-prog-name 142,4930 -(defun isa-tool-list-logics 145,5057 -(defcustom isabelle-logics-available 152,5294 -(defcustom isabelle-chosen-logic 163,5658 -(defun isabelle-command-line 176,6126 -(defun isabelle-choose-logic 199,7083 -(defun isa-view-doc 221,8049 -(defun isa-tool-list-docs 229,8274 -(defconst isabelle-verbatim-regexp 256,9306 -(defun isabelle-verbatim 259,9448 -(defcustom isabelle-refresh-logics 266,9609 -(defvar isabelle-docs-menu 274,9936 -(defvar isabelle-logics-menu-entries 282,10223 -(defun isabelle-logics-menu-calculate 285,10296 -(defvar isabelle-time-to-refresh-logics 304,10859 -(defun isabelle-logics-menu-refresh 308,10954 -(defun isabelle-logics-menu-filter 325,11651 -(defun isabelle-menu-bar-update-logics 331,11861 -(defvar isabelle-logics-menu342,12200 -(defun isabelle-load-isar-keywords 355,12812 -(defpgdefault menu-entries376,13553 -(defpgdefault help-menu-entries 379,13605 -(defun isabelle-convert-idmarkup-to-subterm 407,14363 -(defun isabelle-create-span-menu 431,15374 -(defun isabelle-xml-sml-escapes 447,15816 -(defun isabelle-process-pgip 450,15917 +isar/isabelle-system.el,1401 +(defgroup isabelle 26,776 +(defcustom isabelle-web-page30,904 +(defcustom isa-isatool-command41,1199 +(defvar isatool-not-found 71,2261 +(defun isa-set-isatool-command 74,2374 +(defun isa-shell-command-to-string 96,3296 +(defun isa-getenv 102,3520 +(defcustom isabelle-program-name122,4207 +(defvar isabelle-prog-name 148,5137 +(defun isa-tool-list-logics 151,5264 +(defcustom isabelle-logics-available 158,5501 +(defcustom isabelle-chosen-logic 169,5865 +(defun isabelle-command-line 182,6333 +(defun isabelle-choose-logic 205,7290 +(defun isa-view-doc 227,8256 +(defun isa-tool-list-docs 236,8520 +(defconst isabelle-verbatim-regexp 263,9552 +(defun isabelle-verbatim 266,9694 +(defcustom isabelle-refresh-logics 273,9855 +(defvar isabelle-docs-menu 281,10182 +(defvar isabelle-logics-menu-entries 289,10469 +(defun isabelle-logics-menu-calculate 292,10542 +(defvar isabelle-time-to-refresh-logics 311,11105 +(defun isabelle-logics-menu-refresh 315,11200 +(defun isabelle-logics-menu-filter 332,11897 +(defun isabelle-menu-bar-update-logics 338,12107 +(defvar isabelle-logics-menu349,12446 +(defun isabelle-load-isar-keywords 362,13058 +(defpgdefault menu-entries383,13799 +(defpgdefault help-menu-entries 386,13851 +(defun isabelle-convert-idmarkup-to-subterm 414,14609 +(defun isabelle-create-span-menu 438,15620 +(defun isabelle-xml-sml-escapes 454,16062 +(defun isabelle-process-pgip 457,16163 + +isar/isabelle-unicode-tokens.el,257 +(defconst isar-token-format 10,368 +(defconst isar-charref-format 11,406 +(defconst isar-token-prefix 12,448 +(defconst isar-token-suffix 13,483 +(defconst isar-token-match 14,516 +(defconst isar-hexcode-match 15,570 +(defconst isar-token-name-alist17,632 isar/isar.el,1204 (defcustom isar-keywords-name 31,721 @@ -1259,87 +1268,74 @@ generic/pg-pbrpm.el,1802 (defun pg-pbrpm-process-regions-list 533,19781 (defun pg-pbrpm-region-expression 537,19964 -generic/pg-pgip.el,2892 -(defalias 'pg-pgip-debug pg-pgip-debug36,985 -(defalias 'pg-pgip-error pg-pgip-error37,1026 -(defalias 'pg-pgip-warning pg-pgip-warning38,1061 -(defconst pg-pgip-version-supported 40,1111 -(defun pg-pgip-process-packet 44,1217 -(defvar pg-pgip-last-seen-id 54,1789 -(defvar pg-pgip-last-seen-seq 55,1823 -(defun pg-pgip-process-pgip 57,1859 -(defun pg-pgip-process-msg 76,2790 -(defvar pg-pgip-post-process-functions90,3360 -(defun pg-pgip-post-process 100,3848 -(defun pg-pgip-process-askpgip 116,4459 -(defun pg-pgip-process-usespgip 122,4664 -(defun pg-pgip-process-usespgml 126,4828 -(defun pg-pgip-process-pgmlconfig 130,4992 -(defun pg-pgip-process-proverinfo 146,5609 -(defun pg-pgip-process-hasprefs 163,6274 -(defun pg-pgip-haspref 177,6906 -(defun pg-pgip-process-prefval 196,7682 -(defun pg-pgip-process-guiconfig 223,8391 -(defvar proof-assistant-idtables 230,8508 -(defun pg-pgip-process-ids 233,8625 -(defun pg-complete-idtable-symbol 259,9701 -(defalias 'pg-pgip-process-setids pg-pgip-process-setids264,9793 -(defalias 'pg-pgip-process-addids pg-pgip-process-addids265,9849 -(defalias 'pg-pgip-process-delids pg-pgip-process-delids266,9905 -(defun pg-pgip-process-idvalue 269,9963 -(defun pg-pgip-process-menuadd 281,10299 -(defun pg-pgip-process-menudel 284,10342 -(defun pg-pgip-process-ready 293,10575 -(defun pg-pgip-process-cleardisplay 296,10616 -(defun pg-pgip-process-proofstate 310,11073 -(defun pg-pgip-process-normalresponse 314,11150 -(defun pg-pgip-process-errorresponse 318,11274 -(defun pg-pgip-process-scriptinsert 322,11397 -(defun pg-pgip-process-metainforesponse 327,11531 -(defun pg-pgip-process-informfileloaded 336,11772 -(defun pg-pgip-process-informfileretracted 342,12038 -(defun pg-pgip-process-brokerstatus 355,12515 -(defun pg-pgip-process-proveravailmsg 358,12563 -(defun pg-pgip-process-newprovermsg 361,12613 -(defun pg-pgip-process-proverstatusmsg 364,12661 -(defvar pg-pgip-srcids 373,12908 -(defun pg-pgip-process-newfile 377,13015 -(defun pg-pgip-process-filestatus 393,13603 -(defun pg-pgip-process-newobj 413,14258 -(defun pg-pgip-process-delobj 416,14300 -(defun pg-pgip-process-objectstatus 419,14342 -(defun pg-pgip-process-parsescript 433,14697 -(defun pg-pgip-get-pgiptype 456,15572 -(defun pg-pgip-default-for 476,16365 -(defun pg-pgip-subst-for 489,16760 -(defun pg-pgip-interpret-value 501,17103 -(defun pg-pgip-interpret-choice 519,17788 -(defun pg-pgip-string-of-command 550,18805 -(defconst pg-pgip-id567,19566 -(defvar pg-pgip-refseq 573,19846 -(defvar pg-pgip-refid 575,19943 -(defvar pg-pgip-seq 578,20035 -(defun pg-pgip-assemble-packet 580,20099 -(defun pg-pgip-issue 598,20911 -(defun pg-pgip-maybe-askpgip 615,21523 -(defun pg-pgip-askprefs 621,21714 -(defun pg-pgip-askids 625,21828 -(defun pg-pgip-reset 638,22116 -(defconst pg-pgip-start-element-regexp 669,22814 -(defconst pg-pgip-end-element-regexp 670,22866 - -generic/pg-pgip-old.el,456 -(defun pg-pgip-process-oldhaspref 19,617 -(defun pg-pgip-process-haspref 22,714 -(defun pg-pgip-old-interpret-bool 58,2142 -(defun pg-pgip-old-interpret-int 67,2426 -(defun pg-pgip-old-interpret-string 72,2599 -(defun pg-pgip-old-interpret-choice 75,2653 -(defun pg-pgip-old-interpret-value 95,3372 -(defun pg-pgip-old-default-for 114,3918 -(defun pg-pgip-old-subst-for 125,4242 -(defun pg-pgip-old-get-type 132,4407 -(defun pg-pgip-old-pgiptype 139,4623 +generic/pg-pgip.el,2889 +(defalias 'pg-pgip-debug pg-pgip-debug35,920 +(defalias 'pg-pgip-error pg-pgip-error36,961 +(defalias 'pg-pgip-warning pg-pgip-warning37,996 +(defconst pg-pgip-version-supported 39,1046 +(defun pg-pgip-process-packet 43,1152 +(defvar pg-pgip-last-seen-id 53,1724 +(defvar pg-pgip-last-seen-seq 54,1758 +(defun pg-pgip-process-pgip 56,1794 +(defun pg-pgip-process-msg 75,2725 +(defvar pg-pgip-post-process-functions89,3295 +(defun pg-pgip-post-process 99,3783 +(defun pg-pgip-process-askpgip 115,4394 +(defun pg-pgip-process-usespgip 121,4599 +(defun pg-pgip-process-usespgml 125,4763 +(defun pg-pgip-process-pgmlconfig 129,4927 +(defun pg-pgip-process-proverinfo 145,5544 +(defun pg-pgip-process-hasprefs 162,6209 +(defun pg-pgip-haspref 176,6841 +(defun pg-pgip-process-prefval 195,7617 +(defun pg-pgip-process-guiconfig 222,8326 +(defvar proof-assistant-idtables 229,8443 +(defun pg-pgip-process-ids 232,8560 +(defun pg-complete-idtable-symbol 258,9636 +(defalias 'pg-pgip-process-setids pg-pgip-process-setids263,9728 +(defalias 'pg-pgip-process-addids pg-pgip-process-addids264,9784 +(defalias 'pg-pgip-process-delids pg-pgip-process-delids265,9840 +(defun pg-pgip-process-idvalue 268,9898 +(defun pg-pgip-process-menuadd 280,10234 +(defun pg-pgip-process-menudel 283,10277 +(defun pg-pgip-process-ready 292,10510 +(defun pg-pgip-process-cleardisplay 295,10551 +(defun pg-pgip-process-proofstate 309,11008 +(defun pg-pgip-process-normalresponse 313,11085 +(defun pg-pgip-process-errorresponse 317,11209 +(defun pg-pgip-process-scriptinsert 321,11332 +(defun pg-pgip-process-metainforesponse 326,11466 +(defun pg-pgip-process-informfileloaded 335,11707 +(defun pg-pgip-process-informfileretracted 341,11973 +(defun pg-pgip-process-brokerstatus 354,12450 +(defun pg-pgip-process-proveravailmsg 357,12498 +(defun pg-pgip-process-newprovermsg 360,12548 +(defun pg-pgip-process-proverstatusmsg 363,12596 +(defvar pg-pgip-srcids 372,12843 +(defun pg-pgip-process-newfile 376,12950 +(defun pg-pgip-process-filestatus 392,13538 +(defun pg-pgip-process-newobj 412,14193 +(defun pg-pgip-process-delobj 415,14235 +(defun pg-pgip-process-objectstatus 418,14277 +(defun pg-pgip-process-parsescript 432,14632 +(defun pg-pgip-get-pgiptype 455,15507 +(defun pg-pgip-default-for 475,16300 +(defun pg-pgip-subst-for 488,16695 +(defun pg-pgip-interpret-value 500,17038 +(defun pg-pgip-interpret-choice 518,17723 +(defun pg-pgip-string-of-command 549,18740 +(defconst pg-pgip-id566,19501 +(defvar pg-pgip-refseq 572,19781 +(defvar pg-pgip-refid 574,19878 +(defvar pg-pgip-seq 577,19970 +(defun pg-pgip-assemble-packet 579,20034 +(defun pg-pgip-issue 597,20846 +(defun pg-pgip-maybe-askpgip 614,21458 +(defun pg-pgip-askprefs 620,21649 +(defun pg-pgip-askids 624,21763 +(defun pg-pgip-reset 637,22051 +(defconst pg-pgip-start-element-regexp 668,22749 +(defconst pg-pgip-end-element-regexp 669,22801 generic/pg-response.el,1182 (deflocal pg-response-eagerly-raise 31,731 @@ -1804,50 +1800,50 @@ generic/proof-menu.el,2101 (defvar proof-buffer-menu225,8231 (defun proof-keep-response-history 287,10476 (defconst proof-quick-opts-menu295,10786 -(defun proof-quick-opts-vars 449,16914 -(defun proof-quick-opts-changed-from-defaults-p 474,17665 -(defun proof-quick-opts-changed-from-saved-p 478,17770 -(defun proof-quick-opts-save 489,18122 -(defun proof-quick-opts-reset 494,18290 -(defconst proof-config-menu506,18558 -(defconst proof-advanced-menu513,18737 -(defvar proof-menu 526,19172 -(defun proof-main-menu 535,19456 -(defun proof-aux-menu 546,19722 -(defun proof-menu-define-favourites-menu 562,20069 -(defun proof-def-favourite 582,20725 -(defvar proof-make-favourite-cmd-history 605,21700 -(defvar proof-make-favourite-menu-history 608,21785 -(defun proof-save-favourites 611,21871 -(defun proof-del-favourite 616,22019 -(defun proof-read-favourite 633,22580 -(defun proof-add-favourite 658,23383 -(defvar proof-menu-settings 685,24434 -(defun proof-menu-define-settings-menu 688,24508 -(defun proof-menu-entry-name 708,25252 -(defun proof-menu-entry-for-setting 720,25724 -(defun proof-settings-vars 738,26214 -(defun proof-settings-changed-from-defaults-p 743,26391 -(defun proof-settings-changed-from-saved-p 747,26497 -(defun proof-settings-save 751,26600 -(defun proof-settings-reset 756,26767 -(defun proof-defpacustom-fn 763,27012 -(defmacro defpacustom 839,29896 -(defun proof-assistant-invisible-command-ifposs 854,30723 -(defun proof-maybe-askprefs 876,31698 -(defun proof-assistant-settings-cmd 883,31902 -(defvar proof-assistant-format-table 900,32562 -(defun proof-assistant-format-bool 908,32931 -(defun proof-assistant-format-int 911,33044 -(defun proof-assistant-format-string 914,33136 -(defun proof-assistant-format 917,33234 +(defun proof-quick-opts-vars 450,16937 +(defun proof-quick-opts-changed-from-defaults-p 475,17688 +(defun proof-quick-opts-changed-from-saved-p 479,17793 +(defun proof-quick-opts-save 490,18145 +(defun proof-quick-opts-reset 495,18313 +(defconst proof-config-menu507,18581 +(defconst proof-advanced-menu514,18760 +(defvar proof-menu 527,19195 +(defun proof-main-menu 536,19479 +(defun proof-aux-menu 547,19745 +(defun proof-menu-define-favourites-menu 563,20092 +(defun proof-def-favourite 583,20748 +(defvar proof-make-favourite-cmd-history 606,21723 +(defvar proof-make-favourite-menu-history 609,21808 +(defun proof-save-favourites 612,21894 +(defun proof-del-favourite 617,22042 +(defun proof-read-favourite 634,22603 +(defun proof-add-favourite 659,23406 +(defvar proof-menu-settings 686,24457 +(defun proof-menu-define-settings-menu 689,24531 +(defun proof-menu-entry-name 709,25275 +(defun proof-menu-entry-for-setting 721,25747 +(defun proof-settings-vars 739,26237 +(defun proof-settings-changed-from-defaults-p 744,26414 +(defun proof-settings-changed-from-saved-p 748,26520 +(defun proof-settings-save 752,26623 +(defun proof-settings-reset 757,26790 +(defun proof-defpacustom-fn 764,27035 +(defmacro defpacustom 840,29919 +(defun proof-assistant-invisible-command-ifposs 855,30746 +(defun proof-maybe-askprefs 877,31721 +(defun proof-assistant-settings-cmd 884,31925 +(defvar proof-assistant-format-table 901,32585 +(defun proof-assistant-format-bool 909,32954 +(defun proof-assistant-format-int 912,33067 +(defun proof-assistant-format-string 915,33159 +(defun proof-assistant-format 918,33257 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,5058 +generic/proof-script.el,5108 (defvar proof-element-counters 28,719 (deflocal proof-active-buffer-fake-minor-mode 34,859 (deflocal proof-script-buffer-file-name 37,985 @@ -1888,77 +1884,78 @@ generic/proof-script.el,5058 (defun proof-goto-end-of-queue-or-locked-if-not-visible 475,17368 (defvar pg-idioms 494,18018 (defvar pg-visibility-specs 497,18114 -(defun pg-clear-script-portions 502,18321 -(defun pg-add-script-element 516,18850 -(defun pg-remove-script-element 519,18926 -(defsubst pg-visname 527,19204 -(defun pg-add-element 531,19349 -(defun pg-open-invisible-span 565,20978 -(defun pg-remove-element 576,21341 -(defun pg-make-element-invisible 583,21611 -(defun pg-make-element-visible 589,21868 -(defun pg-toggle-element-visibility 594,22047 -(defun pg-redisplay-for-gnuemacs 602,22377 -(defun pg-show-all-portions 609,22648 -(defun pg-show-all-proofs 627,23319 -(defun pg-hide-all-proofs 632,23447 -(defun pg-add-proof-element 637,23578 -(defun pg-span-name 651,24198 -(defvar pg-span-context-menu-keymap672,24905 -(defun pg-set-span-helphighlights 685,25276 -(defun proof-complete-buffer-atomic 713,26205 -(defun proof-register-possibly-new-processed-file 754,28120 -(defun proof-inform-prover-file-retracted 805,30248 -(defun proof-auto-retract-dependencies 824,31034 -(defun proof-unregister-buffer-file-name 878,33574 -(defun proof-protected-process-or-retract 924,35397 -(defun proof-deactivate-scripting-auto 951,36567 -(defun proof-deactivate-scripting 960,36925 -(defun proof-activate-scripting 1097,42330 -(defun proof-toggle-active-scripting 1219,47762 -(defun proof-done-advancing 1260,49123 -(defun proof-done-advancing-comment 1355,52771 -(defun proof-done-advancing-save 1374,53513 -(defun proof-make-goalsave 1467,57128 -(defun proof-get-name-from-goal 1482,57871 -(defun proof-done-advancing-autosave 1501,58897 -(defun proof-done-advancing-other 1566,61443 -(defun proof-segment-up-to-parser 1594,62402 -(defun proof-script-generic-parse-find-comment-end 1657,64478 -(defun proof-script-generic-parse-cmdend 1666,64894 -(defun proof-script-generic-parse-cmdstart 1691,65789 -(defun proof-script-generic-parse-sexp 1754,68497 -(defun proof-cmdstart-add-segment-for-cmd 1778,69433 -(defun proof-segment-up-to-cmdstart 1830,71632 -(defun proof-segment-up-to-cmdend 1891,73992 -(defun proof-semis-to-vanillas 1963,76657 -(defun proof-script-new-command-advance 2002,77983 -(defun proof-script-next-command-advance 2044,79724 -(defun proof-assert-until-point-interactive 2056,80165 -(defun proof-assert-until-point 2082,81287 -(defun proof-assert-next-command2135,83719 -(defun proof-goto-point 2183,85982 -(defun proof-insert-pbp-command 2201,86523 -(defun proof-done-retracting 2233,87623 -(defun proof-setup-retract-action 2269,89109 -(defun proof-last-goal-or-goalsave 2279,89592 -(defun proof-retract-target 2302,90432 -(defun proof-retract-until-point-interactive 2387,94073 -(defun proof-retract-until-point 2395,94458 -(define-derived-mode proof-mode 2438,96207 -(defun proof-script-set-visited-file-name 2488,98134 -(defun proof-script-set-buffer-hooks 2512,99136 -(defun proof-script-kill-buffer-fn 2520,99554 -(defun proof-config-done-related 2564,101376 -(defun proof-generic-goal-command-p 2634,103854 -(defun proof-generic-state-preserving-p 2639,104066 -(defun proof-generic-count-undos 2648,104583 -(defun proof-generic-find-and-forget 2677,105613 -(defconst proof-script-important-settings2728,107438 -(defun proof-config-done 2743,107991 -(defun proof-setup-parsing-mechanism 2831,111109 -(defun proof-setup-imenu 2875,112962 -(defun proof-setup-func-menu 2892,113567 +(defconst pg-default-invisibility-spec 502,18321 +(defun pg-clear-script-portions 506,18461 +(defun pg-add-script-element 520,18938 +(defun pg-remove-script-element 523,19014 +(defsubst pg-visname 531,19292 +(defun pg-add-element 535,19437 +(defun pg-open-invisible-span 569,21066 +(defun pg-remove-element 580,21429 +(defun pg-make-element-invisible 587,21699 +(defun pg-make-element-visible 593,21956 +(defun pg-toggle-element-visibility 598,22135 +(defun pg-redisplay-for-gnuemacs 606,22465 +(defun pg-show-all-portions 613,22736 +(defun pg-show-all-proofs 631,23407 +(defun pg-hide-all-proofs 636,23535 +(defun pg-add-proof-element 641,23666 +(defun pg-span-name 655,24286 +(defvar pg-span-context-menu-keymap676,24993 +(defun pg-set-span-helphighlights 689,25364 +(defun proof-complete-buffer-atomic 717,26293 +(defun proof-register-possibly-new-processed-file 758,28208 +(defun proof-inform-prover-file-retracted 809,30336 +(defun proof-auto-retract-dependencies 828,31122 +(defun proof-unregister-buffer-file-name 882,33662 +(defun proof-protected-process-or-retract 928,35485 +(defun proof-deactivate-scripting-auto 955,36655 +(defun proof-deactivate-scripting 964,37013 +(defun proof-activate-scripting 1101,42418 +(defun proof-toggle-active-scripting 1223,47850 +(defun proof-done-advancing 1264,49211 +(defun proof-done-advancing-comment 1359,52859 +(defun proof-done-advancing-save 1378,53601 +(defun proof-make-goalsave 1471,57216 +(defun proof-get-name-from-goal 1486,57959 +(defun proof-done-advancing-autosave 1505,58985 +(defun proof-done-advancing-other 1570,61531 +(defun proof-segment-up-to-parser 1598,62490 +(defun proof-script-generic-parse-find-comment-end 1661,64566 +(defun proof-script-generic-parse-cmdend 1670,64982 +(defun proof-script-generic-parse-cmdstart 1695,65877 +(defun proof-script-generic-parse-sexp 1758,68585 +(defun proof-cmdstart-add-segment-for-cmd 1782,69521 +(defun proof-segment-up-to-cmdstart 1834,71720 +(defun proof-segment-up-to-cmdend 1895,74080 +(defun proof-semis-to-vanillas 1967,76745 +(defun proof-script-new-command-advance 2006,78071 +(defun proof-script-next-command-advance 2048,79812 +(defun proof-assert-until-point-interactive 2060,80253 +(defun proof-assert-until-point 2086,81375 +(defun proof-assert-next-command2139,83807 +(defun proof-goto-point 2187,86070 +(defun proof-insert-pbp-command 2205,86611 +(defun proof-done-retracting 2237,87711 +(defun proof-setup-retract-action 2273,89197 +(defun proof-last-goal-or-goalsave 2283,89680 +(defun proof-retract-target 2306,90520 +(defun proof-retract-until-point-interactive 2391,94161 +(defun proof-retract-until-point 2399,94546 +(define-derived-mode proof-mode 2442,96295 +(defun proof-script-set-visited-file-name 2492,98222 +(defun proof-script-set-buffer-hooks 2516,99224 +(defun proof-script-kill-buffer-fn 2524,99642 +(defun proof-config-done-related 2568,101464 +(defun proof-generic-goal-command-p 2638,103942 +(defun proof-generic-state-preserving-p 2643,104154 +(defun proof-generic-count-undos 2652,104671 +(defun proof-generic-find-and-forget 2681,105701 +(defconst proof-script-important-settings2732,107526 +(defun proof-config-done 2747,108079 +(defun proof-setup-parsing-mechanism 2835,111197 +(defun proof-setup-imenu 2879,113050 +(defun proof-setup-func-menu 2896,113655 generic/proof-shell.el,3315 (defvar proof-marker 28,643 @@ -1977,62 +1974,62 @@ generic/proof-shell.el,3315 (defcustom proof-shell-fiddle-frames 208,6507 (defun proof-shell-set-text-representation 215,6748 (defun proof-shell-start 228,7303 -(defvar proof-shell-kill-function-hooks 437,14828 -(defun proof-shell-kill-function 440,14926 -(defun proof-shell-clear-state 529,18729 -(defun proof-shell-exit 544,19172 -(defun proof-shell-bail-out 556,19617 -(defun proof-shell-restart 565,20094 -(defvar proof-shell-no-response-display 607,21478 -(defvar proof-shell-urgent-message-marker 610,21582 -(defvar proof-shell-urgent-message-scanner 613,21703 -(defun proof-shell-handle-output 617,21830 -(defun proof-shell-handle-delayed-output 677,24471 -(defvar proof-shell-no-error-display 705,25514 -(defun proof-shell-handle-error 711,25718 -(defun proof-shell-handle-interrupt 729,26554 -(defun proof-shell-error-or-interrupt-action 743,27167 -(defun proof-goals-pos 768,28312 -(defun proof-pbp-focus-on-first-goal 773,28517 -(defsubst proof-shell-string-match-safe 785,29047 -(defun proof-shell-process-output 790,29215 -(defvar proof-shell-insert-space-fudge 901,33855 -(defun proof-shell-insert 911,34174 -(defun proof-shell-command-queue-item 985,37085 -(defun proof-shell-set-silent 990,37242 -(defun proof-shell-start-silent-item 996,37461 -(defun proof-shell-clear-silent 1002,37653 -(defun proof-shell-stop-silent-item 1008,37875 -(defun proof-shell-should-be-silent 1015,38147 -(defun proof-append-alist 1028,38703 -(defun proof-start-queue 1087,40940 -(defun proof-extend-queue 1098,41289 -(defun proof-shell-exec-loop 1109,41670 -(defun proof-shell-insert-loopback-cmd 1174,44258 -(defun proof-shell-message 1202,45584 -(defun proof-shell-process-urgent-message 1208,45800 -(defun proof-shell-strip-eager-annotations 1340,51065 -(defvar proof-shell-minibuffer-urgent-interactive-input-history 1351,51401 -(defun proof-shell-minibuffer-urgent-interactive-input 1353,51471 -(defun proof-shell-process-urgent-messages 1363,51830 -(defun proof-shell-filter 1437,54929 -(defun proof-shell-filter-process-output 1596,61518 -(defvar pg-last-tracing-output-time 1649,63572 -(defconst pg-slow-mode-duration 1652,63678 -(defconst pg-fast-tracing-mode-threshold 1655,63760 -(defvar pg-tracing-cleanup-timer 1658,63888 -(defun pg-tracing-tight-loop 1660,63927 -(defun pg-finish-tracing-display 1703,65645 -(defun proof-shell-dont-show-annotations 1716,65951 -(defun proof-shell-show-annotations 1732,66472 -(defun proof-shell-wait 1754,66999 -(defun proof-done-invisible 1774,67909 -(defun proof-shell-invisible-command 1817,69632 -(defun proof-shell-invisible-cmd-get-result 1851,70897 -(defun proof-shell-invisible-command-invisible-result 1869,71593 -(define-derived-mode proof-shell-mode 1888,72023 -(defconst proof-shell-important-settings1958,74689 -(defun proof-shell-config-done 1964,74804 +(defvar proof-shell-kill-function-hooks 438,14850 +(defun proof-shell-kill-function 441,14948 +(defun proof-shell-clear-state 530,18751 +(defun proof-shell-exit 545,19194 +(defun proof-shell-bail-out 557,19639 +(defun proof-shell-restart 566,20116 +(defvar proof-shell-no-response-display 608,21500 +(defvar proof-shell-urgent-message-marker 611,21604 +(defvar proof-shell-urgent-message-scanner 614,21725 +(defun proof-shell-handle-output 618,21852 +(defun proof-shell-handle-delayed-output 678,24493 +(defvar proof-shell-no-error-display 706,25536 +(defun proof-shell-handle-error 712,25740 +(defun proof-shell-handle-interrupt 730,26576 +(defun proof-shell-error-or-interrupt-action 744,27189 +(defun proof-goals-pos 769,28334 +(defun proof-pbp-focus-on-first-goal 774,28539 +(defsubst proof-shell-string-match-safe 786,29069 +(defun proof-shell-process-output 791,29237 +(defvar proof-shell-insert-space-fudge 902,33877 +(defun proof-shell-insert 912,34196 +(defun proof-shell-command-queue-item 986,37107 +(defun proof-shell-set-silent 991,37264 +(defun proof-shell-start-silent-item 997,37483 +(defun proof-shell-clear-silent 1003,37675 +(defun proof-shell-stop-silent-item 1009,37897 +(defun proof-shell-should-be-silent 1016,38169 +(defun proof-append-alist 1029,38725 +(defun proof-start-queue 1088,40962 +(defun proof-extend-queue 1099,41311 +(defun proof-shell-exec-loop 1110,41692 +(defun proof-shell-insert-loopback-cmd 1175,44280 +(defun proof-shell-message 1203,45606 +(defun proof-shell-process-urgent-message 1209,45822 +(defun proof-shell-strip-eager-annotations 1341,51087 +(defvar proof-shell-minibuffer-urgent-interactive-input-history 1352,51423 +(defun proof-shell-minibuffer-urgent-interactive-input 1354,51493 +(defun proof-shell-process-urgent-messages 1364,51852 +(defun proof-shell-filter 1438,54951 +(defun proof-shell-filter-process-output 1597,61540 +(defvar pg-last-tracing-output-time 1650,63594 +(defconst pg-slow-mode-duration 1653,63700 +(defconst pg-fast-tracing-mode-threshold 1656,63782 +(defvar pg-tracing-cleanup-timer 1659,63910 +(defun pg-tracing-tight-loop 1661,63949 +(defun pg-finish-tracing-display 1704,65667 +(defun proof-shell-dont-show-annotations 1717,65973 +(defun proof-shell-show-annotations 1733,66494 +(defun proof-shell-wait 1755,67021 +(defun proof-done-invisible 1775,67931 +(defun proof-shell-invisible-command 1818,69654 +(defun proof-shell-invisible-cmd-get-result 1852,70919 +(defun proof-shell-invisible-command-invisible-result 1870,71615 +(define-derived-mode proof-shell-mode 1889,72045 +(defconst proof-shell-important-settings1959,74711 +(defun proof-shell-config-done 1965,74826 generic/proof-site.el,505 (defconst proof-assistant-table-default23,728 @@ -2189,31 +2186,31 @@ generic/proof-utils.el,2111 (defun proof-font-lock-clear-font-lock-vars 372,13261 (defun proof-font-lock-set-font-lock-vars 378,13473 (defun proof-fontify-region 382,13629 -(defun pg-remove-specials 442,15930 -(defun pg-remove-specials-in-string 452,16268 -(defun proof-fontify-buffer 459,16455 -(defun proof-warn-if-unset 472,16696 -(defun proof-get-window-for-buffer 477,16914 -(defun proof-display-and-keep-buffer 528,19222 -(defun proof-clean-buffer 560,20529 -(defun proof-message 575,21150 -(defun proof-warning 580,21363 -(defun pg-internal-warning 586,21645 -(defun proof-debug 594,21964 -(defun proof-switch-to-buffer 609,22635 -(defun proof-resize-window-tofit 642,24324 -(defun proof-submit-bug-report 742,28336 -(defun proof-deftoggle-fn 778,29715 -(defmacro proof-deftoggle 793,30368 -(defun proof-defintset-fn 800,30742 -(defmacro proof-defintset 816,31446 -(defun proof-defstringset-fn 823,31823 -(defmacro proof-defstringset 836,32449 -(defmacro proof-defshortcut 850,32906 -(defmacro proof-definvisible 865,33545 -(defun pg-custom-save-vars 893,34522 -(defun pg-custom-reset-vars 911,35245 -(defun proof-locate-executable 924,35582 +(defun pg-remove-specials 439,15846 +(defun pg-remove-specials-in-string 449,16184 +(defun proof-fontify-buffer 456,16371 +(defun proof-warn-if-unset 469,16612 +(defun proof-get-window-for-buffer 474,16830 +(defun proof-display-and-keep-buffer 525,19138 +(defun proof-clean-buffer 557,20445 +(defun proof-message 572,21066 +(defun proof-warning 577,21279 +(defun pg-internal-warning 583,21561 +(defun proof-debug 591,21880 +(defun proof-switch-to-buffer 606,22551 +(defun proof-resize-window-tofit 639,24240 +(defun proof-submit-bug-report 739,28252 +(defun proof-deftoggle-fn 775,29631 +(defmacro proof-deftoggle 790,30284 +(defun proof-defintset-fn 797,30658 +(defmacro proof-defintset 813,31362 +(defun proof-defstringset-fn 820,31739 +(defmacro proof-defstringset 833,32365 +(defmacro proof-defshortcut 847,32822 +(defmacro proof-definvisible 862,33461 +(defun pg-custom-save-vars 890,34438 +(defun pg-custom-reset-vars 908,35161 +(defun proof-locate-executable 921,35498 generic/proof-x-symbol.el,580 (defvar proof-x-symbol-initialized 52,2006 @@ -2343,26 +2340,26 @@ lib/pg-dev.el,75 (defconst pg-dev-lisp-font-lock-keywords35,1049 (defun unload-pg 69,1986 -lib/proof-compat.el,748 +lib/proof-compat.el,751 (defvar proof-running-on-win32 29,914 (defun pg-custom-undeclare-variable 41,1371 -(defun subst-char-in-string 103,3016 -(defun replace-regexp-in-string 118,3605 -(defconst menuvisiblep 180,6318 -(defun set-window-text-height 197,6931 -(defmacro save-selected-frame 223,7881 -(defun warn 262,9178 -(defun redraw-modeline 269,9433 -(defun proof-buffer-syntactic-context-emulate 280,9871 -(defvar read-shell-command-map313,11178 -(defun read-shell-command 331,11866 -(defun remassq 343,12347 -(defun remassoc 355,12736 -(defun frames-of-buffer 368,13181 -(defmacro with-selected-window 407,14443 -(defun pg-pop-to-buffer 450,15821 -(defun process-live-p 501,17654 -(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context518,18157 +(defun subst-char-in-string 131,4159 +(defun replace-regexp-in-string 146,4748 +(defconst menuvisiblep 208,7461 +(defun set-window-text-height 225,8074 +(defmacro save-selected-frame 251,9024 +(defun warn 290,10321 +(defun redraw-modeline 297,10576 +(defun proof-buffer-syntactic-context-emulate 308,11014 +(defvar read-shell-command-map341,12321 +(defun read-shell-command 359,13009 +(defun remassq 371,13490 +(defun remassoc 383,13879 +(defun frames-of-buffer 396,14324 +(defmacro with-selected-window 435,15586 +(defun pg-pop-to-buffer 478,16964 +(defun process-live-p 529,18797 +(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context546,19300 lib/span.el,137 (defsubst span-delete-spans 22,479 @@ -2456,6 +2453,28 @@ lib/unicode-chars.el,80 (defvar unicode-chars-alist12,348 (defun unicode-chars-list-chars 5050,245960 +lib/unicode-tokens.el,938 +(defvar unicode-tokens-charref-format 50,1715 +(defvar unicode-tokens-token-format 53,1812 +(defvar unicode-tokens-token-name-alist 56,1903 +(defvar unicode-tokens-glyph-list 59,2004 +(defvar unicode-tokens-token-prefix 63,2148 +(defvar unicode-tokens-token-suffix 66,2232 +(defvar unicode-tokens-token-match 69,2314 +(defvar unicode-tokens-hexcode-match 72,2399 +(defvar unicode-tokens-token-codept-alist 80,2569 +(defvar unicode-tokens-max-token-length 83,2667 +(defun unicode-tokens-insert-char 91,2784 +(defun unicode-tokens-character-insert 101,3205 +(defun unicode-tokens-token-insert 123,4113 +(defun unicode-tokens-replace-token-after 146,5099 +(defun unicode-tokens-looking-backward-at 168,5827 +(defun unicode-tokens-electric-suffix 179,6289 +(defun unicode-tokens-quail-define-rules 261,8641 +(defvar unicode-tokens-mode-map 292,9671 +(define-minor-mode unicode-tokens-mode295,9768 +(defun unicode-tokens-initialise 316,10395 + lib/xml-fixed.el,528 (defsubst xml-node-name 82,2904 (defsubst xml-node-attributes 87,3023 @@ -2771,7 +2790,7 @@ x-symbol/lisp/x-symbol-bib.el,549 (defvar x-symbol-bib-generated-data 113,4390 (defun x-symbol-bib-default-token-list 117,4529 -x-symbol/lisp/x-symbol.el,9173 +x-symbol/lisp/x-symbol.el,9210 (defvar x-symbol-trace-invisible 51,1979 (defconst x-symbol-language-access-alist66,2494 (defstruct (x-symbol-generated178,8375 @@ -2827,186 +2846,187 @@ x-symbol/lisp/x-symbol.el,9173 (defun x-symbol-decode-lisp 865,36110 (defun x-symbol-encode-string 897,37577 (defun x-symbol-encode-all 908,37896 -(defun x-symbol-encode-lisp 970,40852 -(defun x-symbol-decode-recode 1006,42257 -(defun x-symbol-decode 1036,43633 -(defun x-symbol-encode-recode 1049,44224 -(defun x-symbol-encode 1077,45500 -(defun x-symbol-unalias 1093,46259 -(defun x-symbol-copy-region-encoded 1158,49178 -(defun x-symbol-yank-decoded 1186,50428 -(defun x-symbol-update-modeline 1213,51528 -(defun x-symbol-auto-coding-alist 1237,52383 -(defun x-symbol-auto-8bit-search 1273,53544 -(defvar x-symbol-font-family-postfixes1298,54334 -(defvar x-symbol-font-lock-property-alist1301,54450 -(defvar x-symbol-font-lock-keywords1305,54631 -(defvar x-symbol-subscript-matcher 1332,55626 -(defvar x-symbol-subscript-type 1336,55729 -(defun x-symbol-subscripts-available-p 1339,55780 -(defun x-symbol-font-lock-start 1345,56021 -(defun x-symbol-match-subscript 1354,56407 -(defun x-symbol-init-font-lock 1360,56620 -(defun x-symbol-set-image 1392,58208 -(defun x-symbol-mode-internal 1410,58954 -(defun nuke-x-symbol 1484,62057 -(defun x-symbol-options-filter 1497,62510 -(defun x-symbol-extra-filter 1533,63666 -(defun x-symbol-menu-filter 1541,63914 -(defvar x-symbol-list-mode-map1568,64751 -(defvar x-symbol-list-buffer 1594,65901 -(defvar x-symbol-list-win-config 1596,65977 -(defvar x-symbol-invisible-spec 1598,66088 -(defvar x-symbol-itimer 1602,66238 -(defvar x-symbol-invisible-display-table1605,66321 -(defvar x-symbol-invisible-font 1614,66557 -(defvar x-symbol-charsym-info-cache 1639,67744 -(defvar x-symbol-language-info-caches 1641,67835 -(defvar x-symbol-coding-info-cache 1643,67929 -(defvar x-symbol-keys-info-cache 1645,68018 -(defun x-symbol-list-bury 1653,68323 -(defun x-symbol-list-restore 1659,68519 -(defun x-symbol-list-store 1689,69737 -(defun x-symbol-list-mode 1698,70154 -(defun x-symbol-list-scroll 1719,70956 -(defun x-symbol-init-language-interactive 1742,71598 -(defun x-symbol-list-menu 1759,72312 -(defun x-symbol-list-selected 1814,74220 -(defun x-symbol-list-menu-selected 1840,75429 -(defun x-symbol-list-mouse-selected 1851,75882 -(defun x-symbol-charsym-info 1868,76604 -(defun x-symbol-language-info 1882,77205 -(defun x-symbol-coding-info 1914,78405 -(defun x-symbol-keys-info 1934,79177 -(defun x-symbol-info 1958,80100 -(defun x-symbol-list-info 1971,80638 -(defun x-symbol-highlight-echo 1985,81181 -(defun x-symbol-point-info 1996,81730 -(defun x-symbol-hide-revealed-at-point 2042,83652 -(defun x-symbol-reveal-invisible 2079,85319 -(defun x-symbol-show-info-and-invisible 2127,87511 -(defun x-symbol-start-itimer-once 2163,89053 -(defun x-symbol-setup-minibuffer 2179,89679 -(defvar x-symbol-language-history 2197,90250 -(defvar x-symbol-token-history 2200,90374 -(defvar x-symbol-last-abbrev 2203,90450 -(defvar x-symbol-electric-pos 2205,90546 -(defvar x-symbol-command-keys 2208,90628 -(defvar x-symbol-help-keys 2212,90759 -(defvar x-symbol-help-language 2214,90854 -(defvar x-symbol-help-completions 2216,90953 -(defvar x-symbol-help-completions1 2218,91045 -(defun x-symbol-map-default-binding 2226,91321 -(defun x-symbol-read-charsym-token 2257,92399 -(defun x-symbol-insert-command 2283,93322 -(defun x-symbol-read-language 2334,95329 -(defun x-symbol-read-token 2349,96007 -(defun x-symbol-read-token-direct 2388,97516 -(defun x-symbol-grid 2400,97916 -(defun x-symbol-replace-from 2488,101532 -(defvar x-symbol-token-search-prelude-size 2524,103033 -(defun x-symbol-replace-token 2526,103081 -(defun x-symbol-match-token-before 2551,104172 -(defun x-symbol-token-input 2595,105975 -(defun x-symbol-modify-key 2616,106805 -(defun x-symbol-rotate-key 2649,108134 -(defun x-symbol-electric-input 2703,110344 -(defun x-symbol-help-mapper 2745,112045 -(defun x-symbol-help-output 2768,112884 -(defun x-symbol-help 2811,114480 -(defvar x-symbol-face-docstrings2864,116549 -(defvar x-symbol-all-key-prefixes 2870,116737 -(defvar x-symbol-all-key-chain-alist 2872,116848 -(defvar x-symbol-all-horizontal-chain-alist 2874,116947 -(defvar x-symbol-all-chain-subchains-alist 2876,117060 -(defvar x-symbol-all-exclusive-context-alist 2878,117174 -(defalias 'x-symbol-table-grouping x-symbol-table-grouping2886,117470 -(defalias 'x-symbol-table-aspects x-symbol-table-aspects2887,117511 -(defalias 'x-symbol-table-score x-symbol-table-score2888,117552 -(defalias 'x-symbol-table-input x-symbol-table-input2889,117592 -(defsubst x-symbol-table-prefixes 2890,117633 -(defsubst x-symbol-table-junk 2891,117684 -(defsubst x-symbol-charsym-defined-p 2893,117735 -(defun x-symbol-try-font-name-0 2901,118036 -(defun x-symbol-try-font-name 2919,118592 -(defun x-symbol-set-cstrings 2936,119108 -(defun x-symbol-init-charsym-command 2981,121086 -(defun x-symbol-init-charsym-input 2989,121452 -(defun x-symbol-init-charsym-aspects 3058,124170 -(defun x-symbol-init-cset 3088,125450 -(defun x-symbol-make-atree 3238,132273 -(defun x-symbol-atree-push 3242,132353 -(defun x-symbol-component-root-p 3262,133042 -(defun x-symbol-component-elements 3266,133181 -(defun x-symbol-component-merge 3273,133429 -(defun x-symbol-component-space 3287,133977 -(defun x-symbol-modify-less-than 3301,134561 -(defun x-symbol-inherit-aspects 3306,134784 -(defun x-symbol-compute-aspects 3315,135223 -(defun x-symbol-init-aspects 3331,135941 -(defun x-symbol-sort-modify-chain 3376,137990 -(defun x-symbol-init-horizontal/key-alist 3391,138562 -(defun x-symbol-init-exclusive-alist 3407,139308 -(defun x-symbol-init-horizontal-chain 3445,140912 -(defun x-symbol-init-exclusive-chain 3453,141244 -(defun x-symbol-init-rotate-chain 3460,141571 -(defun x-symbol-init-context-atree 3481,142445 -(defun x-symbol-init-key-bindings 3526,144728 -(defun x-symbol-rotate-modify-less-than 3549,145651 -(defun x-symbol-subgroup-less-than 3557,146046 -(defun x-symbol-header-charsyms 3562,146303 -(defun x-symbol-init-grid/menu 3588,147353 -(defun x-symbol-init-input 3659,149953 -(defun x-symbol-init-latin-decoding 3789,156429 -(defun x-symbol-get-prime-for 3830,158300 -(defun x-symbol-alist-to-obarray 3839,158624 -(defun x-symbol-alist-to-hash-table 3845,158832 -(defun x-symbol-init-language 3855,159165 -(defvar x-symbol-latin1-cset3979,164630 -(defvar x-symbol-latin2-cset3985,164803 -(defvar x-symbol-latin3-cset3991,164976 -(defvar x-symbol-latin5-cset3997,165149 -(defvar x-symbol-latin9-cset4003,165321 -(defvar x-symbol-xsymb0-cset4009,165527 -(defvar x-symbol-xsymb1-cset4015,165782 -(defvar x-symbol-latin1-table4021,166024 -(defvar x-symbol-latin2-table4122,170494 -(defvar x-symbol-latin3-table4221,173695 -(defvar x-symbol-latin5-table4320,176576 -(defvar x-symbol-latin9-table4419,178886 -(defvar x-symbol-xsymb0-table4518,181276 -(defvar x-symbol-xsymb1-table4668,188672 -(defvar x-symbol-no-of-charsyms 4876,199307 -(defun x-symbol-mac-setup1 4884,199673 -(defun x-symbol-mac-setup2 4910,200582 +(defun x-symbol-encode-lisp 972,40931 +(defun x-symbol-decode-recode 1008,42336 +(defun x-symbol-decode 1038,43712 +(defun x-symbol-encode-recode 1051,44303 +(defun x-symbol-encode 1079,45579 +(defun x-symbol-unalias 1095,46338 +(defun x-symbol-copy-region-encoded 1160,49257 +(defun x-symbol-yank-decoded 1188,50507 +(defun x-symbol-update-modeline 1215,51607 +(defun x-symbol-auto-coding-alist 1239,52462 +(defun x-symbol-auto-8bit-search 1275,53623 +(defvar x-symbol-font-family-postfixes1300,54413 +(defvar x-symbol-font-lock-property-alist1303,54529 +(defvar x-symbol-font-lock-keywords1307,54710 +(defvar x-symbol-subscript-matcher 1334,55705 +(defvar x-symbol-subscript-type 1338,55808 +(defun x-symbol-subscripts-available-p 1341,55859 +(defun x-symbol-font-lock-start 1347,56100 +(defun x-symbol-match-subscript 1356,56486 +(defun x-symbol-init-font-lock 1362,56699 +(defun x-symbol-set-image 1394,58287 +(defun x-symbol-mode-internal 1412,59033 +(defun nuke-x-symbol 1486,62136 +(defun x-symbol-options-filter 1499,62589 +(defun x-symbol-extra-filter 1535,63745 +(defun x-symbol-menu-filter 1543,63993 +(defvar x-symbol-list-mode-map1573,64972 +(defvar x-symbol-list-buffer 1599,66122 +(defvar x-symbol-list-win-config 1601,66198 +(defvar x-symbol-invisible-spec 1603,66309 +(defvar x-symbol-itimer 1607,66459 +(defvar x-symbol-invisible-display-table1610,66542 +(defvar x-symbol-invisible-font 1619,66778 +(defvar x-symbol-charsym-info-cache 1644,67965 +(defvar x-symbol-language-info-caches 1646,68056 +(defvar x-symbol-coding-info-cache 1648,68150 +(defvar x-symbol-keys-info-cache 1650,68239 +(defun x-symbol-list-bury 1658,68544 +(defun x-symbol-list-restore 1664,68740 +(defun x-symbol-list-store 1694,69958 +(defun x-symbol-list-mode 1703,70375 +(defun x-symbol-list-scroll 1724,71177 +(defun x-symbol-init-language-interactive 1747,71819 +(defun x-symbol-list-menu 1764,72533 +(defun x-symbol-list-selected 1819,74441 +(defun x-symbol-list-menu-selected 1845,75650 +(defun x-symbol-list-mouse-selected 1856,76103 +(defun x-symbol-charsym-info 1873,76825 +(defun x-symbol-language-info 1887,77426 +(defun x-symbol-coding-info 1919,78626 +(defun x-symbol-keys-info 1939,79398 +(defun x-symbol-info 1963,80321 +(defun x-symbol-list-info 1976,80859 +(defun x-symbol-highlight-echo 1990,81402 +(defun x-symbol-point-info 2001,81951 +(defun x-symbol-hide-revealed-at-point 2047,83873 +(defun x-symbol-reveal-invisible 2084,85540 +(defun x-symbol-show-info-and-invisible 2132,87732 +(defun x-symbol-start-itimer-once 2168,89274 +(defun x-symbol-setup-minibuffer 2184,89900 +(defvar x-symbol-language-history 2202,90471 +(defvar x-symbol-token-history 2205,90595 +(defvar x-symbol-last-abbrev 2208,90671 +(defvar x-symbol-electric-pos 2210,90767 +(defvar x-symbol-command-keys 2213,90849 +(defvar x-symbol-help-keys 2217,90980 +(defvar x-symbol-help-language 2219,91075 +(defvar x-symbol-help-completions 2221,91174 +(defvar x-symbol-help-completions1 2223,91266 +(defun x-symbol-map-default-binding 2231,91542 +(defun x-symbol-read-charsym-token 2262,92620 +(defun x-symbol-insert-command 2288,93543 +(defun x-symbol-read-language 2339,95550 +(defun x-symbol-read-token 2354,96228 +(defun x-symbol-read-token-direct 2393,97737 +(defun x-symbol-grid 2405,98137 +(defun x-symbol-replace-from 2493,101753 +(defvar x-symbol-token-search-prelude-size 2529,103254 +(defun x-symbol-replace-token 2531,103302 +(defun x-symbol-match-token-before 2556,104393 +(defun x-symbol-token-input 2600,106196 +(defun x-symbol-modify-key 2621,107026 +(defun x-symbol-rotate-key 2654,108355 +(defun x-symbol-electric-input 2708,110565 +(defun x-symbol-help-mapper 2750,112266 +(defun x-symbol-help-output 2773,113105 +(defun x-symbol-help 2816,114701 +(defvar x-symbol-face-docstrings2869,116770 +(defvar x-symbol-all-key-prefixes 2875,116958 +(defvar x-symbol-all-key-chain-alist 2877,117069 +(defvar x-symbol-all-horizontal-chain-alist 2879,117168 +(defvar x-symbol-all-chain-subchains-alist 2881,117281 +(defvar x-symbol-all-exclusive-context-alist 2883,117395 +(defalias 'x-symbol-table-grouping x-symbol-table-grouping2891,117691 +(defalias 'x-symbol-table-aspects x-symbol-table-aspects2892,117732 +(defalias 'x-symbol-table-score x-symbol-table-score2893,117773 +(defalias 'x-symbol-table-input x-symbol-table-input2894,117813 +(defsubst x-symbol-table-prefixes 2895,117854 +(defsubst x-symbol-table-junk 2896,117905 +(defsubst x-symbol-charsym-defined-p 2898,117956 +(defun x-symbol-try-font-name-0 2906,118257 +(defun x-symbol-try-font-name 2924,118813 +(defun x-symbol-set-cstrings 2941,119329 +(defun x-symbol-init-charsym-command 2986,121307 +(defun x-symbol-init-charsym-input 2994,121673 +(defun x-symbol-init-charsym-aspects 3063,124391 +(defun x-symbol-init-cset 3093,125671 +(defun x-symbol-make-atree 3243,132494 +(defun x-symbol-atree-push 3247,132574 +(defun x-symbol-component-root-p 3267,133263 +(defun x-symbol-component-elements 3271,133402 +(defun x-symbol-component-merge 3278,133650 +(defun x-symbol-component-space 3292,134198 +(defun x-symbol-modify-less-than 3306,134782 +(defun x-symbol-inherit-aspects 3311,135005 +(defun x-symbol-compute-aspects 3320,135444 +(defun x-symbol-init-aspects 3336,136162 +(defun x-symbol-sort-modify-chain 3381,138211 +(defun x-symbol-init-horizontal/key-alist 3396,138783 +(defun x-symbol-init-exclusive-alist 3412,139529 +(defun x-symbol-init-horizontal-chain 3450,141133 +(defun x-symbol-init-exclusive-chain 3458,141465 +(defun x-symbol-init-rotate-chain 3465,141792 +(defun x-symbol-init-context-atree 3486,142666 +(defun x-symbol-init-key-bindings 3531,144949 +(defun x-symbol-rotate-modify-less-than 3554,145872 +(defun x-symbol-subgroup-less-than 3562,146267 +(defun x-symbol-header-charsyms 3567,146524 +(defun x-symbol-init-grid/menu 3593,147574 +(defun x-symbol-init-input 3665,150230 +(defun x-symbol-init-latin-decoding 3795,156706 +(defun x-symbol-get-prime-for 3836,158577 +(defun x-symbol-alist-to-obarray 3845,158901 +(defun x-symbol-alist-to-hash-table 3851,159109 +(defun x-symbol-init-language 3861,159442 +(defvar x-symbol-latin1-cset3985,164907 +(defvar x-symbol-latin2-cset3991,165080 +(defvar x-symbol-latin3-cset3997,165253 +(defvar x-symbol-latin5-cset4003,165426 +(defvar x-symbol-latin9-cset4009,165598 +(defvar x-symbol-xsymb0-cset4015,165804 +(defvar x-symbol-xsymb1-cset4021,166059 +(defvar x-symbol-latin1-table4027,166301 +(defvar x-symbol-latin2-table4128,170771 +(defvar x-symbol-latin3-table4227,173972 +(defvar x-symbol-latin5-table4326,176853 +(defvar x-symbol-latin9-table4425,179163 +(defvar x-symbol-xsymb0-table4524,181553 +(defvar x-symbol-xsymb1-table4674,188949 +(defvar x-symbol-no-of-charsyms 4882,199584 +(defun x-symbol-mac-setup1 4890,199950 +(defun x-symbol-mac-setup2 4916,200859 +(defun x-symbol-startup 4934,201525 x-symbol/lisp/x-symbol-emacs.el,1126 -(defun emacs-version>=34,1341 -(defvar x-symbol-emacs-has-font-lock-with-props68,3005 -(defvar x-symbol-emacs-has-correct-find-safe-coding86,3670 -(defvar x-symbol-emacs-after-create-image-function101,4184 -(defvar image-types 127,5041 -(defvar init-file-loaded 163,6428 -(defvar message-stack 166,6501 -(defun region-active-p 249,9811 -(defvar x-symbol-data-directory 286,11176 -(defun x-symbol-directory-files 356,13453 -(defun x-symbol-event-in-current-buffer 370,13841 -(defun x-symbol-create-image 373,13890 -(defun x-symbol-make-glyph 376,13975 -(defun x-symbol-set-glyph-image 379,14046 -(defvar x-symbol-heading-strut-glyph 394,14543 -(defvar x-symbol-invisible-face 397,14630 -(defvar x-symbol-face 398,14688 -(defvar x-symbol-sub-face 399,14726 -(defvar x-symbol-sup-face 400,14772 -(defvar x-symbol-emacs-w32-font-directories402,14819 -(defvar x-symbol-invisible-display-table 415,15297 -(defalias 'x-symbol-window-width x-symbol-window-width417,15344 -(defun x-symbol-set-face-font 428,15796 -(defun x-symbol-event-matches-key-specifier-p 439,16269 -(defun start-itimer 449,16541 -(defun itimer-live-p 451,16638 +(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-width418,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 @@ -3306,14 +3326,14 @@ x-symbol/lisp/x-symbol-unichars.el,99 (defvar x-symbol-unicode-character-list5,115 (defun x-symbol-list-unicode-characters 5044,235676 -x-symbol/lisp/x-symbol-unicode.el,170 -(defconst x-symbol-xsym-unicode-map 12,383 -(defconst x-symbol-old-tables 260,9819 -(defconst x-symbol-unicode-table 276,10252 -(defconst x-symbol-unicode-cset292,10757 +x-symbol/lisp/x-symbol-unicode.el,168 +(defconst x-symbol-xsym-unicode-map 18,546 +(defconst x-symbol-old-tables266,9981 +(defconst x-symbol-unicode-table282,10412 +(defconst x-symbol-unicode-cset298,10915 -x-symbol/lisp/x-symbol-unicode-extras.el,38 -(defconst x-symol-unicode-extras 2,1 +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 @@ -3652,20 +3672,32 @@ x-symbol/lisp/custom-load.el,0 lib/holes-load.el,0 +generic/test.el,0 + generic/proof.el,0 generic/proof-autoloads.el,0 +generic/pg-cmdhist.el,0 + +generic/comptest.el,0 + twelf/x-symbol-twelf.el,0 pgshell/pgshell.el,0 lego/x-symbol-lego.el,0 +isar/test.el,0 + +isar/isar-templates.el,0 + isar/isar-autotest.el,0 isar/interface-setup.el,0 +isar/comptest.el,0 + hol98/x-symbol-hol98.el,0 hol98/hol98.el,0 -- cgit v1.2.3