diff options
| author | David Aspinall | 2008-07-24 09:51:53 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-07-24 09:51:53 +0000 |
| commit | 76d6b0b2b1f039549d308a0d2c478a6b05869af9 (patch) | |
| tree | 78cc7e13bf290a17e7006a6d4616a8a08e36ce8f /etc | |
| parent | 8f8e9388b582ad6d3ee6e1eea842a8d443d4ce89 (diff) | |
Merge changes from Version4Branch.
Diffstat (limited to 'etc')
28 files changed, 75 insertions, 1048 deletions
diff --git a/etc/README.devel b/etc/README.devel deleted file mode 100644 index b66e857c..00000000 --- a/etc/README.devel +++ /dev/null @@ -1,100 +0,0 @@ --*- outline -*- - -* Developers Notes for Proof General -==================================== - -David Aspinall, March 2000. - -$Id$ - -Notes here about development conventions and compatibility -issues. Please read if you contribute to Proof General! - -Please also join the (very low volume) developers mailing -list, see http://www.proofgeneral.org/mailinglist - - -** Project planning - -We don't use any rigorous planning mechanisms, but please use and -maintain the simple "todo" lists. They can include lists of things to -do as well as notes about outstanding bugs, etc. Each item is -classified with a priority. What usually happens is that either -something is fixed quickly, or its priority gradually decreases, -saving much time not implementing unimportant things! - -Items which are based on bug/problem reports by users are given a -higher priority by default (unless to fix them would be unreasonably -difficult). - -In the top-level directory, todo holds the list of things to do in the -generic Elisp basis and for other generic parts of the project. Each -proof assistant then has its own todo file. - - -** Coding Standards - -When writing your modes, please follow the Emacs Lisp Conventions -See the Emacs Lisp reference manual, node Style Tips. - - -** Testing - -Ideally, we would have an automated test suite for Proof General. -Emacs Lisp is certainly flexible to have such a thing, but it would -take some effort to set it up. Although automated tests could test -functions and states for the right values, a user interface ultimately -needs some human checks that visible appearances and user-input behave -as expected. - -At the moment, we rely on the tiny example files included for each -proof system as simple tests that basic scripting works. Additional -test scripts to test parsing complex scripts and tests against -specific fixed bugs are included in etc/<PA>. Multiple file scripting -test cases should also be provided in etc/<PA>. - - -** Standards for each instance of PG - -We include a README file and low-level todo file for each prover. - - -** Using custom library - -Please use the custom library for all variable declarations, apart -from very low-level variables. Follow the customize group conventions -laid out in generic/proof-config.el - - -** Compatibility with different Emacsen - -One of the greatest problems in developing Proof General is -maintaining compatibility across different versions of Emacs. - -XEmacs is the primary development (and use) platform, but we'd like to -maintain compatibility with FSF Emacs, and the Japanicised versions of -that. The development policy is for the main codebase to be written -for the latest stable version of XEmacs. We follow XEmacs advice on -removing obsolete function calls. - -Hopefully one day we may have a proper test suite and mechanism to -test across different versions of Emacs. For the time being, follow -the following tips. - -*** Compatibility hacks collected in proof-compat.el - - - This file contains implementations/emulations of functions to - provide uniformity between different Emacs versions. If you - use a function specific to XEmacs or newer versions, consider adding - a conditional definition of it here to support other versions - for a while. - -*** Common Lisp macros -- Japan Emacsen have older versions - - - Use (dolist (var list) body), not (dolist (var list result) body). - - - -** CVS tips - - See etc/cvs-tips.txt diff --git a/etc/debugging-tips.txt b/etc/debugging-tips.txt deleted file mode 100644 index b8ac649d..00000000 --- a/etc/debugging-tips.txt +++ /dev/null @@ -1,89 +0,0 @@ -Tips for Debugging Proof General -- David Aspinall -==================================================== - -Emacs debug flags -================= - -If Proof General gives an error, you can set the Emacs debug -flags to find out where in the code it occurs, showing a -stack trace. - -On Emacs, check the boxes in the Options menu: - - Options -> Enter Debugger on Error - Options -> Enter Debugger on Quit - -On XEmacs you can find the check boxes under the menu Options -> -Troubleshooting. - -You can also set these variables directly in lisp: - - (setq debug-on-error t) ; debug on errors - (setq debug-on-quit t) ; debug on CTRL-G for looping code - -You can make settings like this using M-x set-variable, or writing Lisp -code as above in the *scratch* buffer, and typing C-x C-e to evaluate -the expressions, or using M-x eval-expression (ESC-:). - - -Debugging start-up problems -=========================== - -If you get an error when visiting a theorem prover file -(i.e. around the time that the splash screen appears), try -starting XEmacs normally: - - xemacs -q -no-site-file - -setting the debug flag: - - M-x eval-expression RET (setq debug-on-error t) RET - -and then visiting a theory file (e.g. empty Test.thy), *before* -loading Proof General. Load Proof General with the command: - - M-x load-file <PATH-TO-ProofGeneral>/generic/proof-site.el - -And then issue the command to switch the buffer into the mode -which is giving you problems, e.g. - - M-x isar-mode RET - -Hopefully this should produce a stack trace. (The stack trace -may otherwise be hidden, since some versions of Emacs try to -hide errors which occur when a file is visited). - - - - -Quick hints for edebug (source-level debugger) -============================================== - -Source-level debugging is more useful than backtraces, especially if -you are writing your own additions for Proof General. - -Load the source file <foo>.el, and locate the function you -want to debug. Type - - M-x edebug-defun RET - -to instrument it for debugging. - -When the code reaches the function it will enter the source-level -debugger. Keep pressing space to step through and see the result of -evaluating sub-expressions, or hit "c" to continue. - -Pressing ? gives more commands. - - - -Proof General debug messages -============================ - -Proof General includes internal debugging messages. -Make these settings to see them: - - (setq proof-tidy-response nil) ; response buffer never clears - (setq proof-show-debug-messages t) ; debug messages appear in response buffer - - diff --git a/etc/isa/\backslashname/test.ML b/etc/isa/\backslashname/test.ML deleted file mode 100644 index 0691e38e..00000000 --- a/etc/isa/\backslashname/test.ML +++ /dev/null @@ -1,11 +0,0 @@ -(* Scripting here tests quotation mechanism for filenames. *) - -(* At the moment this trips a bug in Isabelle which objects - to filename of this directory. - - Easy way to test for other provers is with a link, - \bizzare \\<rightarrow> ProofGeneral/ then load \bizarre/coq/example.v, etc - -*) - -val a = 1; diff --git a/etc/isa/\backslashname/test.thy b/etc/isa/\backslashname/test.thy deleted file mode 100644 index 2ca5331f..00000000 --- a/etc/isa/\backslashname/test.thy +++ /dev/null @@ -1 +0,0 @@ -test = Pure diff --git a/etc/isa/long-line-backslash.ML b/etc/isa/long-line-backslash.ML deleted file mode 100644 index 66435c1b..00000000 --- a/etc/isa/long-line-backslash.ML +++ /dev/null @@ -1,20 +0,0 @@ -(* - - long-line-backslash.ML - - Test for long lines with backslashes in them. - Cause problem with pty communication where line length - is limited to 256 characters sometimes (e.g. on Solaris). - -*) - -val nasty_string="\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\"; - -(* Test subsequent commands can be processed *) - -val one = 1; -val two = 2; -val three = 3; - -(* Test something with eager annotations *) - diff --git a/etc/isa/message-test.ML b/etc/isa/message-test.ML deleted file mode 100644 index 4afd7120..00000000 --- a/etc/isa/message-test.ML +++ /dev/null @@ -1,16 +0,0 @@ -(* Testing different kinds of markup in Isabelle output *) - -(* ordinary output between prompts *) -print "ordinary"; -print "ordinary\n"; (* final newline no difference *) - -(* eager annotation: displayed as soon as it's seen *) -writeln "eager to be seen!"; - -print "more ordinary\n"; - -Goal "P-->P"; - -(* C-c RET to here should show eager annotation, as well as - updating goals buffer properly. *) -error "something went wrong"; diff --git a/etc/isa/multiple/A.ML b/etc/isa/multiple/A.ML deleted file mode 100644 index 771a5f1a..00000000 --- a/etc/isa/multiple/A.ML +++ /dev/null @@ -1,11 +0,0 @@ -(* Scripting buffer for theory A *) - -1; - -(* A few commands so that we can test partial-retraction. *) - -2; - -3; - - diff --git a/etc/isa/multiple/A.thy b/etc/isa/multiple/A.thy deleted file mode 100644 index fc585327..00000000 --- a/etc/isa/multiple/A.thy +++ /dev/null @@ -1,7 +0,0 @@ -(* - File: /home/da/proofgen/ProofGeneral/etc/isa/multiple/A.thy - Theory Name: A - Logic Image: Pure -*) - -A = Pure diff --git a/etc/isa/multiple/B.ML b/etc/isa/multiple/B.ML deleted file mode 100644 index e0226516..00000000 --- a/etc/isa/multiple/B.ML +++ /dev/null @@ -1,4 +0,0 @@ -(* Scripting buffer for theory B *) - -val b = 0; -val b1 = 1; diff --git a/etc/isa/multiple/B.thy b/etc/isa/multiple/B.thy deleted file mode 100644 index a896bca2..00000000 --- a/etc/isa/multiple/B.thy +++ /dev/null @@ -1,7 +0,0 @@ -(* - File: /home/da/proofgen/ProofGeneral/etc/isa/multiple/B.thy - Theory Name: B - Logic Image: Pure -*) - -B = Pure diff --git a/etc/isa/multiple/C.ML b/etc/isa/multiple/C.ML deleted file mode 100644 index 4ad965a2..00000000 --- a/etc/isa/multiple/C.ML +++ /dev/null @@ -1,4 +0,0 @@ -(* Scripting buffer for theory C *) - -val c1 = 4; -val c = 5; diff --git a/etc/isa/multiple/C.thy b/etc/isa/multiple/C.thy deleted file mode 100644 index 3316eaee..00000000 --- a/etc/isa/multiple/C.thy +++ /dev/null @@ -1,10 +0,0 @@ -(* - File: /home/da/proofgen/ProofGeneral/etc/isa/multiple/C.thy - Theory Name: C - Logic Image: Pure -*) - -theory C = A + B -files "foobar/foo.ML": - -end diff --git a/etc/isa/multiple/D.ML b/etc/isa/multiple/D.ML deleted file mode 100644 index 76dd89c1..00000000 --- a/etc/isa/multiple/D.ML +++ /dev/null @@ -1,3 +0,0 @@ -(* Scripting buffer for theory D *) - -val it = (); diff --git a/etc/isa/multiple/D.thy b/etc/isa/multiple/D.thy deleted file mode 100644 index afacc20e..00000000 --- a/etc/isa/multiple/D.thy +++ /dev/null @@ -1,7 +0,0 @@ -(* - File: /home/da/proofgen/ProofGeneral/etc/isa/multiple/D.thy - Theory Name: D - Logic Image: Pure -*) - -D = Pure diff --git a/etc/isa/multiple/Err.ML b/etc/isa/multiple/Err.ML deleted file mode 100644 index 177da5ce..00000000 --- a/etc/isa/multiple/Err.ML +++ /dev/null @@ -1,5 +0,0 @@ -(* Test to see that scripting is *not* turned on - if an error occurs during activation -*) - -val x = 1; diff --git a/etc/isa/multiple/Err.thy b/etc/isa/multiple/Err.thy deleted file mode 100644 index d36a5af2..00000000 --- a/etc/isa/multiple/Err.thy +++ /dev/null @@ -1,3 +0,0 @@ -(* Dummy file to cause an error in use_thy *) - -Err = blah
\ No newline at end of file diff --git a/etc/isa/multiple/README b/etc/isa/multiple/README deleted file mode 100644 index 8ffa6fba..00000000 --- a/etc/isa/multiple/README +++ /dev/null @@ -1,102 +0,0 @@ -Test files for multiple file handling with Isabelle. - - -Test schedule -============= - -[C depends on A and B, D is independent] - -Notation: A means that buffer A.l is unlocked - A+ means that buffer A.l is partly locked - A* means that buffer A.l is locked - ? means that behaviour might be different for proof systems - with non-linear contexts - -Borrowed from Thomas's lego tests: (v 1.2) - - 1) visit A.ML EFFECTS A - 2) visit C.ML EFFECTS A C - 3) assert C EFFECTS A* C* - 4) visit B.ML,B.thy,C.thy EFFECTS A* B* C* C.thy* B.thy* - 5) visit D.ML,D.thy EFFECTS A* B* C* D D.thy - 6) retract to middle of B EFFECTS A* B C D B.thy* (*thy remains locked*) - 7) assert first command of B EFFECTS A* B+ C D - 8) assert C EFFECTS A* B+ C D [error message, correctly] - 9) assert B EFFECTS A* B* C D -10) assert D EFFECTS A* B* C D* D.thy* -11) retract B EFFECTS A* B C D? [D* D.thy* for Isabelle] -12) assert C EFFECTS A* B* C* D? -13) retract B EFFECTS A* B C D? [B.thy* D*,D.thy* again] -14) assert B EFFECTS A* B* C D? -15) assert C EFFECTS A* B* C* D? [everything locked] - BROKEN 11.12.98: B.ML *may* not be locked? - -16) retract to middle of B EFFECTS A* B+ C D? - BROKEN! Now retracts whole thing. -14) M-x proof-shell-restart EFFECTS A B C D - - -MORE TESTS NEEDED FOR ISABELLE: -=============================== - -Should test assertion of theory files, and watch what happens to ML files. - -Because of theory loader's odd behaviour, must watch what happens -to ML files of autoloaded children. - - -1) visit example.ML, example.thy EFFECT: ML thy -2) assert .ML EFFECT: ML* thy* -3) retract thy EFFECT: ML thy - - -1) visit example.ML, example.thy ML thy -2) assert thy ML* thy* (reads theory too) - - -(* Test case for outdating a child theory *) - -1) assert C.thy A*, B*, C* -2) retract B.thy A* -3) edit B.thy to touch timestamp -4) assert B.thy A*, B*, C Message: "C out of date" -5) assert C.thy A*, B*, C* - - -(* Test case for removing a dependency from a theory: - this automatically unlocks the orphaned theory, - is this right?? -*) - -1) assert C.thy A*, B*, C* -2) retract C.thy A*, B*, C -3) edit C.thy to C=A, remove dependency on B -4) assert C.thy A*, B, C* (B automatically unlocked) - - - - - ------------------------------------------------------------------ - -Question: - -We assert script A. -We assert script B. -Can we retract to middle of A? Yes, we should be able to! - - - ------------------------------------------------------------------ - -Tester: - -Visit A.ML. Assert partly. - -Visit C.thy. Assert it. - -This should lock remainder of A.ML, since it has now been read -completely. - - - diff --git a/etc/isa/multiple/foobar/foo.ML b/etc/isa/multiple/foobar/foo.ML deleted file mode 100644 index 25084a22..00000000 --- a/etc/isa/multiple/foobar/foo.ML +++ /dev/null @@ -1,4 +0,0 @@ - -val foo = "foo"; - -val bar = 1; diff --git a/etc/isa/parsing.ML b/etc/isa/parsing.ML deleted file mode 100644 index 805e69fb..00000000 --- a/etc/isa/parsing.ML +++ /dev/null @@ -1,13 +0,0 @@ -(* Any (* nested comments *) are tricky in XEmacs (21.4.8), - but better syntax handling in Emacs at the moment. -*) - -Goal "A \\<and> B \\<longrightarrow> B \\<and> A"; -by (rtac impI 1); -by (etac conjE 1); -by (rtac conjI 1); -by (assume_tac 1); -by (assume_tac 1); -qed "and_comms"; - -(* Comment at the end?! *)
\ No newline at end of file diff --git a/etc/isa/settings.ML b/etc/isa/settings.ML deleted file mode 100644 index 3250f9ca..00000000 --- a/etc/isa/settings.ML +++ /dev/null @@ -1,21 +0,0 @@ -(* - Simple test for variable setting mechanism ML -> PG. - This kind of protocol is included in PGIP for setting config variables. - Here we can use it for executing arbitrary elisp, in fact (eek!) -*) - -fun pg_setvar var exp = writeln ("Proof General, please set the variable " ^ var ^ " to: #" ^ exp ^ "#."); - -pg_setvar "wag" "(+ 33 44)"; (* C-h v wag RET gives 77 *) - -fun pgset var = pg_setvar var "t"; -fun pgreset var = pg_setvar var "nil"; - -pgset "isa-show-types"; (* sets show-types in menu *) - -(* What might be nice is to override 'set' 'reset' fuctions to mirror - settings in PG automatically, but then we'd need to retrieve the - names of the ML values from the 'set' and 'reset' functions... *) - -(* test failure case: prints a debug message if proof-show-debug-messages<>nil *) -pg_setvar "wig" "blah 12 x12" diff --git a/etc/isa/thy/test.ML b/etc/isa/thy/test.ML deleted file mode 100644 index 6a434570..00000000 --- a/etc/isa/thy/test.ML +++ /dev/null @@ -1,5 +0,0 @@ -(* Test case for wrong file type - bug report by jv@ddre.dk - - This file should be ML, not theory! -*)
\ No newline at end of file diff --git a/etc/isa/xsym.ML b/etc/isa/xsym.ML deleted file mode 100644 index 797bad69..00000000 --- a/etc/isa/xsym.ML +++ /dev/null @@ -1,18 +0,0 @@ -(* a few token characters to exercise X-Symbol *) - -Goal "A \\<and> B \\<longrightarrow> B \\<and> A"; -by (rtac impI 1); -by (etac conjE 1); -by (rtac conjI 1); -by (assume_tac 1); -by (assume_tac 1); -qed "and_comms"; - -3; - -4; - -print "hello"; - -writeln "hello"; -error "hello"; diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy new file mode 100644 index 00000000..a6f80cf7 --- /dev/null +++ b/etc/isar/TokensAcid.thy @@ -0,0 +1,45 @@ +(* Some acid tests for token modes *) + +theory TokensAcid imports Main +begin + +(* Here's a table of all tokens for symbols, + produced by unicode-tokens-list-tokens *) + +(* +\<alpha> \<beta> \<gamma> \<delta> \<epsilon> \<zeta> \<eta> \<theta> \<iota> \<kappa> +\<lambda> \<mu> \<nu> \<xi> \<pi> \<rho> \<sigma> \<tau> \<upsilon> \<phi> +\<chi> \<psi> \<omega> \<Gamma> \<Delta> \<Theta> \<Lambda> \<Xi> \<Pi> \<Sigma> +\<Upsilon> \<Phi> \<Psi> \<Omega> \<leftarrow> \<rightarrow> \<Leftarrow> \<Rightarrow> \<leftrightarrow> \<Leftrightarrow> +\<mapsto> \<longleftarrow> \<Longleftarrow> \<longrightarrow> \<Longrightarrow> \<longleftrightarrow> \<Longleftrightarrow> \<longmapsto> \<midarrow> \<Midarrow> +\<hookleftarrow> \<hookrightarrow> \<leftharpoondown> \<rightharpoondown> \<leftharpoonup> \<rightharpoonup> \<rightleftharpoons> \<leadsto> \<downharpoonleft> \<downharpoonright> +\<upharpoonleft> \<upharpoonright> \<restriction> \<Colon> \<up> \<Up> \<down> \<Down> \<updown> \<Updown> +\<langle> \<rangle> \<lceil> \<rceil> \<lfloor> \<rfloor> \<lparr> \<rparr> \<lbrakk> \<rbrakk> +\<lbrace> \<rbrace> \<guillemotleft> \<guillemotright> \<bottom> \<top> \<and> \<And> \<or> \<Or> +\<forall> \<exists> \<nexists> \<not> \<box> \<diamond> \<turnstile> \<Turnstile> \<tturnstile> \<TTurnstile> +\<stileturn> \<surd> \<le> \<ge> \<lless> \<ggreater> \<in> \<notin> \<subset> \<supset> +\<subseteq> \<supseteq> \<sqsubset> \<sqsupset> \<sqsubseteq> \<sqsupseteq> \<inter> \<Inter> \<union> \<Union> +\<squnion> \<sqinter> \<setminus> \<propto> \<uplus> \<noteq> \<sim> \<doteq> \<simeq> \<approx> +\<asymp> \<cong> \<smile> \<equiv> \<frown> \<bowtie> \<prec> \<succ> \<preceq> \<succeq> +\<parallel> \<bar> \<plusminus> \<minusplus> \<times> \<div> \<cdot> \<star> \<bullet> \<circ> +\<dagger> \<ddagger> \<lhd> \<rhd> \<unlhd> \<unrhd> \<triangleleft> \<triangleright> \<triangle> \<triangleq> +\<oplus> \<otimes> \<odot> \<ominus> \<oslash> \<dots> \<cdots> \<Sum> \<Prod> \<Coprod> +\<infinity> \<integral> \<ointegral> \<clubsuit> \<diamondsuit> \<heartsuit> \<spadesuit> \<aleph> \<emptyset> \<nabla> +\<partial> \<Re> \<Im> \<flat> \<natural> \<sharp> \<angle> \<copyright> \<registered> \<hyphen> +\<inverse> \<onesuperior> \<twosuperior> \<threesuperior> \<onequarter> \<onehalf> \<threequarters> \<ordmasculine> \<ordfeminine> \<section> +\<paragraph> \<exclamdown> \<questiondown> \<euro> \<pounds> \<yen> \<cent> \<currency> \<degree> \<mho> +\<lozenge> \<wp> \<wrong> \<acute> \<index> \<dieresis> \<cedilla> \<hungarumlaut> \<spacespace> \<some> +\<stareq> \<defeq> \<questioneq> \<vartheta> \<varpi> \<varrho> \<varsigma> \<varphi> \<hbar> \<ell> +\<ast> \<bigcirc> \<bigtriangleup> \<bigtriangledown> \<ni> \<mid> \<notlt> \<notle> \<notprec> \<notpreceq> +\<notsubset> \<notsubseteq> \<notsqsubseteq> \<notgt> \<notge> \<notsucc> \<notsucceq> \<notsupset> \<notsupseteq> \<notsqsupseteq> +\<notequiv> \<notsim> \<notsimeq> \<notapprox> \<notcong> \<notasymp> \<nearrow> \<searrow> \<swarrow> \<nwarrow> +\<vdots> \<ddots> \<closequote> \<openquote> \<opendblquote> \<closedblquote> \<emdash> \<prime> \<doubleprime> \<tripleprime> +\<nbspace> \<thinspace> \<notni> \<colonequals> \<foursuperior> \<fivesuperior> \<sixsuperior> \<sevensuperior> \<eightsuperior> \<ninesuperior> +\<zero> \<one> \<two> \<three> \<four> \<five> \<six> \<seven> \<eight> \<nine> +\<A> \<B> \<C> \<D> \<E> \<F> \<G> \<H> \<I> \<J> +\<K> \<L> \<M> \<N> \<O> \<P> \<Q> \<R> \<S> \<T> +\<U> \<V> \<W> \<X> \<Y> \<Z> +*) + + +end diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy index 3689f300..0425fc39 100644 --- a/etc/isar/XSymbolTests.thy +++ b/etc/isar/XSymbolTests.thy @@ -1,4 +1,4 @@ -(* Some checks for X-Symbol behaviour. +(* Some checks for Unicode Tokens behaviour. This file should be displayed sensibly, and also the display back from Isabelle ought to match. @@ -26,14 +26,18 @@ by auto Problem reported by Norbert Schirmer <norbert.schirmer@web.de> Currently, superscript output highlighting seems broken anyway? *) -consts silly:: "'a => 'a => 'a" ("_\<^sup>_" [1000,1000] 1000) +consts "\<alpha1>":: "'a => 'a" ("\<alpha1>\<^sup>_") +consts "\<alpha2>":: "'a => 'a => 'a" ("\<alpha2>\<^sup>_") +consts "\<alpha3>":: "'a => 'a => 'a => 'a" ("_\<^sup>_\<^sup>_") consts k:: 'a +term "\<alpha>" term "a\<^sup>b" (* b should be a blue variable *) term "\<forall>x. a\<^sup>x" (* x should be a green bound variable *) term "a\<^sup>k" (* k should be a black constant *) term "\<alpha>\<^isub>2" (* alpha should be blue variable with subscripted blue 2 *) +term "\<alpha>\<^isup>x" (* identifier *) consts sausage:: "'a => 'a => 'a" ("_\<^bsup>_\<^esup>" [1000,1000] 1000) @@ -58,6 +62,8 @@ constdefs P2 :: bool ("P\<^sup>2") (* superscript *) "P\<^sup>2 == True" + "P\<^loc>x" (* location escape *) + (* Buglet here: if we enable x-sym during scripting, goals/response flks are not updated, so xsyms do not appear in output windows. Stoping/starting @@ -68,6 +74,12 @@ thm P1_def P2_def (* check display from Isabelle *) constdefs (* long sub/sups, new 29/12/03, added by Gerwin Klein *) +\<^bitalic>test italics\<^eitalic> +\<^bserif>serif\<^eserif> +\<^bfrakt>fraktur\<^efrakt> +\<^bbold>test\<^ebold> + +\<^bsub> asda low\<^esub> Plow :: bool ("P\<^bsub>low\<^esub>") (* spanning subscript *) "P\<^bsub>low\<^esub> \<equiv> True" Phigh :: bool ("P\<^bsup>high\<^esup>") (* spanning superscript *) @@ -80,9 +92,10 @@ by (simp add: P1_def P2_def) (* .. and response window *) consts "P\<^sup>\<alpha>" :: bool (* superscript of a token char *) - "\<^bold>X" :: bool (* bold character - [not supported in current X-Symbols] *) + "\<^bold>P" :: bool (* bold character *) + "\<^italic>i" :: int +\<^bitalic>italic?\<^eitalic> (* test: using a symbol as a subscript *) (* 9.3.03: this causes nasty prob with pre-command hook, @@ -91,6 +104,10 @@ consts consts intof :: "nat \<Rightarrow> int" ("_\<^sub>\<int>" 50) mynat :: nat ("\<gamma>") +\<one> \<two> \<C> \<J> \<S> \<h> h \<AA> + +\<^bscript>foo\<^escript> +bar term "intof 3" @@ -118,3 +135,12 @@ primrec end +\<A> +\<AA> \<ABC> \<ss> \<pounds> \<yen> + +SYMBOL Ideas: + + \<0x888> for unicode character + \<alpha:foo> for variants, same display + + \<color:foo> for colour, no sems (dropped in translation)
\ No newline at end of file diff --git a/etc/isar/multiple/C.thy b/etc/isar/multiple/C.thy index 079a1f78..22d86858 100644 --- a/etc/isar/multiple/C.thy +++ b/etc/isar/multiple/C.thy @@ -1,5 +1,3 @@ -(* -*- isar -*- *) - theory C imports A B begin diff --git a/etc/patches/duplicated-short-messages-fix.txt b/etc/patches/duplicated-short-messages-fix.txt deleted file mode 100644 index 45b8727f..00000000 --- a/etc/patches/duplicated-short-messages-fix.txt +++ /dev/null @@ -1,107 +0,0 @@ -This change should have gone into 3.0, but I forgot to make the -setting and so it missed testing. - -Minor bug without it is that Isabelle (others?) will sometimes -display messages less than 10 characters long twice, since -the urgent message scanner gets moved too far back. - -Sould probably also add this fix in proof-shell/proof-shell-insert: - - ;; FIXME: possible improvement. Make for post 3.0 releases - ;; in case of problems. - ;; (set-marker proof-shell-urgent-message-marker (point)) - ;; (set-marker proof-shell-urgent-message-scanner (point)) - - - da. - - - - -? etc/duplicated-short-messages-fix.txt -Index: coq/coq.el -=================================================================== -RCS file: /home/proofgen/src/ProofGeneral/coq/coq.el,v -retrieving revision 3.0 -diff -c -r3.0 coq.el -*** coq.el 1999/11/17 20:39:08 3.0 ---- coq.el 1999/11/29 13:22:14 -*************** -*** 502,507 **** ---- 502,508 ---- - proof-shell-field-char ?\374 ; not done - proof-shell-goal-char ?\375 ; done - proof-shell-eager-annotation-start "\376" ; done -+ proof-shell-eager-annotation-start-length 1 - proof-shell-eager-annotation-end "\377" ; done - proof-shell-annotated-prompt-regexp - (concat proof-shell-prompt-pattern -Index: isa/isa.el -=================================================================== -RCS file: /home/proofgen/src/ProofGeneral/isa/isa.el,v -retrieving revision 3.4 -diff -c -r3.4 isa.el -*** isa.el 1999/11/29 12:14:05 3.4 ---- isa.el 1999/11/29 13:22:15 -*************** -*** 172,177 **** ---- 172,178 ---- - proof-shell-quit-cmd "quit();" - - proof-shell-eager-annotation-start "\360\\|\362" -+ proof-shell-eager-annotation-start-length 1 - proof-shell-eager-annotation-end "\361\\|\363" - - ;; Some messages delimited by eager annotations -Index: isar/isar.el -=================================================================== -RCS file: /home/proofgen/src/ProofGeneral/isar/isar.el,v -retrieving revision 3.1 -diff -c -r3.1 isar.el -*** isar.el 1999/11/18 15:00:57 3.1 ---- isar.el 1999/11/29 13:22:15 -*************** -*** 250,255 **** ---- 250,256 ---- - proof-shell-restart-cmd "ProofGeneral.restart;" - proof-shell-quit-cmd (isar-verbatim "quit();") - -+ proof-shell-eager-annotation-start-length 1 - proof-shell-eager-annotation-start "\360\\|\362" - proof-shell-eager-annotation-end "\361\\|\363" - -Index: lego/lego.el -=================================================================== -RCS file: /home/proofgen/src/ProofGeneral/lego/lego.el,v -retrieving revision 3.1 -diff -c -r3.1 lego.el -*** lego.el 1999/11/24 21:48:24 3.1 ---- lego.el 1999/11/29 13:22:16 -*************** -*** 453,458 **** ---- 453,459 ---- - proof-shell-field-char ?\374 - proof-shell-goal-char ?\375 - proof-shell-eager-annotation-start "\376" -+ proof-shell-eager-annotation-start-length 1 - proof-shell-eager-annotation-end "\377" - proof-shell-annotated-prompt-regexp "Lego> \371" - proof-shell-result-start "\372 Pbp result \373" -Index: plastic/plastic.el -=================================================================== -RCS file: /home/proofgen/src/ProofGeneral/plastic/plastic.el,v -retrieving revision 3.1 -diff -c -r3.1 plastic.el -*** plastic.el 1999/11/22 18:52:47 3.1 ---- plastic.el 1999/11/29 13:22:16 -*************** -*** 538,543 **** ---- 538,546 ---- - proof-shell-field-char ?\374 - proof-shell-goal-char ?\375 - proof-shell-eager-annotation-start "\376" -+ ;; FIXME da: if p-s-e-a-s is implemented, you should set -+ ;; proof-shell-eager-annotation-start-length=1 to -+ ;; avoid possibility of duplicating short messages. - proof-shell-eager-annotation-end "\377" - - proof-shell-annotated-prompt-regexp "LF> \371" diff --git a/etc/patches/fix-attempt-for-eager-cleaning.txt b/etc/patches/fix-attempt-for-eager-cleaning.txt deleted file mode 100644 index 519df708..00000000 --- a/etc/patches/fix-attempt-for-eager-cleaning.txt +++ /dev/null @@ -1,66 +0,0 @@ -Patch below doesn't work because it examines the head of the -proof-action-list which is empty by the time -proof-handle-delayed-output gets called! - -Best thing may be to temporarily extend -proof-handle-delayed-output-hook with a function to clear the erase -flag... BUT can't remove it from proof-shell-done-invisible, -because that's too early!!! Argh. - -Maybe we need a special test in the exec loop for just one element in -the action list, and then call the callback *after* handling delayed -output? - -Um. Not for 3.0, then. - - - - -*** ProofGeneral.prev/generic/proof-shell.el Thu Nov 18 13:07:33 1999 ---- ProofGeneral/generic/proof-shell.el Thu Nov 18 13:03:25 1999 -*************** -*** 676,682 **** - ;; Erase the response buffer if need be, maybe also removing the - ;; window. Indicate that it should be erased before the next - ;; output. -! (proof-shell-maybe-erase-response t t) - - (set-buffer proof-goals-buffer) - ---- 676,684 ---- - ;; Erase the response buffer if need be, maybe also removing the - ;; window. Indicate that it should be erased before the next - ;; output. -! (proof-shell-maybe-erase-response -! (or proof-shell-erase-response-flag t) ; preserve invisible cmd o/p -! t) - - (set-buffer proof-goals-buffer) - -*************** -*** 829,835 **** - (unless proof-shell-leave-annotations-in-output - (setq str (proof-shell-strip-special-annotations str))) - -! (proof-shell-maybe-erase-response t nil) - (proof-response-buffer-display str) - (proof-display-and-keep-buffer proof-response-buffer)) - ;; ---- 831,847 ---- - (unless proof-shell-leave-annotations-in-output - (setq str (proof-shell-strip-special-annotations str))) - -! (proof-shell-maybe-erase-response -! ;; Magical detection of invisible commands, whose output -! ;; gets preserved specially. -! (if (and -! (not (eq proof-shell-erase-response-flag 'invisible)) -! (eq (nth 2 (car-safe proof-action-list)) -! 'proof-shell-done-invisible)) -! 'invisible -! t) ; erase next time, probably -! t) ; clean. -! - (proof-response-buffer-display str) - (proof-display-and-keep-buffer proof-response-buffer)) - ;; diff --git a/etc/profiling.txt b/etc/profiling.txt deleted file mode 100644 index 8348c7ad..00000000 --- a/etc/profiling.txt +++ /dev/null @@ -1,408 +0,0 @@ -Notes on Profiling Proof General in XEmacs [da] ------------------------------------------------- - -Usage of Elisp profiler: - - M-x elp-instrument-package RET proof RET - -< do something now > - - M-x elp-results - -To display results. - - -M-x clear-profiling-info -Eval: (profile (proof-toolbar-next) (proof-shell-wait)) -M-x profile-results - -NB: Must ignore calls to accept-process-output and sit-for, these - are from proof-shell-wait (only). - - -Testing by processing first line of src/HOL/Real/ROOT.ML (i.e. loading -RealDef) - -Best case scenarios: - - * Running Isabelle in ordinary shell buffer in Emacs, PIII: - ~8% Emacs (PIII), ~90% SML if shell hidden - ~15% X, ~25% xemacs, ~60% SML if shell displayed! - - * Running Isabelle in xterm: - ~3% xterm, ~2% X, 95% SML if xterm hidden - ~4% xterm, ~16% X, 90% SML if xterm revealed - - -Before optimization: - - * CPU time split about 70%/30% (Cel 366) or 65%/35% (PIII 500) SML/xemacs - - - - - - - - -Sample Runs. Tue Oct 5 ------------------------ - -[On Cel 366 64M] - - -Function Name Ticks %/Total Call Count -=================================== ===== ======= ========== -(in redisplay) 1183 44.947 -re-search-forward 901 34.233 8061 -sit-for 159 6.041 11919 -comint-output-filter 93 3.533 3596 -accept-process-output 43 1.634 11919 -string-match 34 1.292 7300 -font-lock-pre-idle-hook 30 1.140 25261 -insert-before-markers 28 1.064 3597 -let 14 0.532 10853 -map-extents 13 0.494 539 -(in garbage collection) 10 0.380 -byte-code 9 0.342 25376 -while 8 0.304 3648 -setq 7 0.266 8299 -comint-postoutput-scroll-to-bottom 7 0.266 3597 -next-window 6 0.228 7194 -put-nonduplicable-text-property 5 0.190 1166 -marker-position 5 0.190 14389 -goto-char 5 0.190 14097 -walk-windows 4 0.152 3597 -window-minibuffer-p 4 0.152 3597 -proof-toolbar-refresh 4 0.152 3686 -and 4 0.152 11162 -selected-window 3 0.114 14390 -window-start 3 0.114 3596 -proof-shell-filter 3 0.114 3597 -itimer-time-difference 3 0.114 546 -#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 3 0.114 7194 -#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 3 0.114 1298 -process-buffer 3 0.114 3596 -point 3 0.114 7382 -or 3 0.114 7256 -comint-watch-for-password-prompt 3 0.114 3597 -save-excursion 2 0.076 3655 -proof-shell-process-urgent-messages 2 0.076 3597 -marker-buffer 2 0.076 3596 -font-lock-fontify-keywords-region 2 0.076 45 -process-mark 2 0.076 7208 -redisplay-echo-area 2 0.076 23 -if 2 0.076 18901 -buffer-name 1 0.038 3650 -erase-buffer 1 0.038 26 -pos-visible-in-window-p 1 0.038 1 -window-buffer 1 0.038 7195 -self-insert-command 1 0.038 14 -< 1 0.038 4300 -itimer-timer-driver 1 0.038 182 -font-lock-fontify-glumped-region 1 0.038 31 -get-buffer-process 1 0.038 3633 -char-to-string 1 0.038 3597 -save-current-buffer 1 0.038 17 -insert-string 1 0.038 23 --------------------------------------------------------------------- -Total 2632 100.00 - - -One tick = 1 ms - - -[On PIII 256M] top shows roughly 65% SML / 35% xemacs. - -Function Name Ticks %/Total Call Count -====================================== ===== ======= ========== -(in redisplay) 3529 55.166 -re-search-forward 1520 23.761 31627 -sit-for 356 5.565 33870 -comint-output-filter 265 4.143 12980 -accept-process-output 125 1.954 33870 -font-lock-pre-idle-hook 67 1.047 73094 -insert-before-markers 51 0.797 12981 -(in garbage collection) 46 0.719 -string-match 44 0.688 27686 -byte-code 27 0.422 74822 -let 23 0.360 39724 -#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 21 0.328 25962 -selected-window 20 0.313 51951 -comint-postoutput-scroll-to-bottom 19 0.297 12981 -setq 15 0.234 39971 -if 15 0.234 72709 -walk-windows 13 0.203 12981 -proof-toolbar-refresh 13 0.203 14429 -marker-position 12 0.188 51925 -proof-shell-filter 12 0.188 12981 -goto-char 12 0.188 53685 -run-hook-with-args 12 0.188 13219 -next-window 11 0.172 25962 -and 9 0.141 40761 -save-excursion 8 0.125 13756 -buffer-name 7 0.109 13783 -window-buffer 7 0.109 26077 -log-message 7 0.109 237 -process-mark 7 0.109 26208 -point 7 0.109 27554 -while 7 0.109 13727 -#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 6 0.094 11268 -char-to-string 6 0.094 12981 -force-mode-line-update 6 0.094 12980 -< 5 0.078 19216 -itimer-run-expired-timers 4 0.063 415 -aref 4 0.063 11953 -get-buffer-process 4 0.063 13290 -proof-shell-process-urgent-messages 4 0.063 12981 -redisplay-echo-area 4 0.063 238 -insert-string 4 0.063 238 -font-lock-fontify-keywords-region 4 0.063 740 -window-minibuffer-p 3 0.047 12981 -window-start 3 0.047 12980 -marker-buffer 3 0.047 12980 -process-buffer 3 0.047 12980 -featurep 3 0.047 2120 -comint-watch-for-password-prompt 3 0.047 12981 -set-buffer 2 0.031 259 -or 2 0.031 26285 -font-lock-after-change-function-1 2 0.031 494 -font-lock-default-fontify-region 2 0.031 740 -event-over-toolbar-p 1 0.016 107 -get-buffer 1 0.016 433 -extent-object 1 0.016 988 -itimerp 1 0.016 9136 -itimer-is-idle 1 0.016 3735 -set-extent-property 1 0.016 1024 -make-string 1 0.016 247 -next-single-property-change 1 0.016 246 -expand-file-name 1 0.016 96 -incf 1 0.016 11268 -center-to-window-line 1 0.016 9 -proof-done-advancing 1 0.016 2 -itimer-time-difference 1 0.016 1660 -itimer-timer-driver 1 0.016 415 -1+ 1 0.016 11268 -length 1 0.016 249 -append-message 1 0.016 238 -concat 1 0.016 246 -proof-shell-strip-special-annotations 1 0.016 246 -proof-shell-process-urgent-message 1 0.016 246 -buffer-substring 1 0.016 493 -save-current-buffer 1 0.016 248 -newline 1 0.016 246 -insert 1 0.016 249 -current-time 1 0.016 831 -match-beginning 1 0.016 247 -font-lock-append-text-property 1 0.016 246 -progn 1 0.016 1034 -proof-response-buffer-display 1 0.016 246 -font-lock-fontify-syntactically-region 1 0.016 740 -font-lock-fontify-glumped-region 1 0.016 494 -#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150> 1 0.016 248 -font-lock-after-change-function 1 0.016 494 ------------------------------------------------------------------------ -Total 6397 100.00 - - -One tick = 1 ms - - -*** After some optimization attempt in proof-shell-process-urgent-messages, - to remove re-search-forward hog: - -[Cel 366] - -Function Name Ticks %/Total Call Count -=================================== ===== ======= ========== -accept-process-output 3279 62.374 1047436 -(in redisplay) 919 17.481 -sit-for 547 10.405 1047435 -re-search-forward 134 2.549 8950 -while 110 2.092 3648 -comint-output-filter 65 1.236 3347 -(in garbage collection) 24 0.457 -font-lock-pre-idle-hook 18 0.342 14166 -insert-before-markers 15 0.285 3348 -string-match 10 0.190 7376 -let 9 0.171 7010 -#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 9 0.171 6696 -setq 6 0.114 12598 -byte-code 5 0.095 14879 -#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 5 0.095 4762 -and 5 0.095 10936 -comint-postoutput-scroll-to-bottom 5 0.095 3348 -log-message 4 0.076 98 -save-excursion 3 0.057 3655 -itimerp 3 0.057 14128 -selected-window 3 0.057 13403 -next-window 3 0.057 6696 -point 3 0.057 10722 -proof-toolbar-refresh 3 0.057 3942 -if 3 0.057 23233 -font-lock-default-unfontify-region 3 0.057 295 -walk-windows 2 0.038 3348 -event-window 2 0.038 658 -buffer-name 2 0.038 3670 -erase-buffer 2 0.038 105 -put-nonduplicable-text-property 2 0.038 590 -window-start 2 0.038 3347 -null 2 0.038 3352 -marker-position 2 0.038 13393 -marker-buffer 2 0.038 3347 -itimer-time-difference 2 0.038 2223 -- 2 0.038 3350 -font-lock-fontify-keywords-region 2 0.038 295 -goto-char 2 0.038 14092 -buffer-substring 2 0.038 196 -redisplay-echo-area 2 0.038 104 -run-hook-with-args 2 0.038 3447 -comint-watch-for-password-prompt 2 0.038 3348 -event-over-vertical-divider-p 1 0.019 254 -event-glyph-extent 1 0.019 329 -get-buffer 1 0.019 255 -pointer-image-instance-p 1 0.019 985 -barf-if-buffer-read-only 1 0.019 98 -extent-at 1 0.019 87 -itimer-value 1 0.019 6175 -pos-visible-in-window-p 1 0.019 4 -expand-file-name 1 0.019 192 -file-truename 1 0.019 104 -center-to-window-line 1 0.019 4 -proof-shell-process-urgent-messages 1 0.019 3348 -proof-shell-filter 1 0.019 3348 -set-marker 1 0.019 3429 -itimer-run-expired-timers 1 0.019 247 -< 1 0.019 5950 -min 1 0.019 3428 -1- 1 0.019 3428 -display-message 1 0.019 99 -font-lock-fontify-glumped-region 1 0.019 197 -get-buffer-process 1 0.019 6791 -process-mark 1 0.019 10124 -default-mouse-motion-handler 1 0.019 329 -char-to-string 1 0.019 3348 -save-current-buffer 1 0.019 99 -newline 1 0.019 98 -or 1 0.019 3490 -#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150> 1 0.019 99 -font-lock-unfontify-region 1 0.019 295 -specifier-instance 1 0.019 329 --------------------------------------------------------------------- -Total 5257 100.00 - - -One tick = 1 ms - - -[PIII] split now about 70%/30% - -Function Name Ticks %/Total Call Count -====================================== ===== ======= ========== -(in redisplay) 3638 72.082 -sit-for 358 7.093 34176 -comint-output-filter 247 4.894 12963 -accept-process-output 132 2.615 34176 -font-lock-pre-idle-hook 70 1.387 74389 -insert-before-markers 67 1.328 12964 -string-match 50 0.991 27655 -(in garbage collection) 43 0.852 -#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 29 0.575 25928 -re-search-forward 25 0.495 18630 -comint-postoutput-scroll-to-bottom 24 0.476 12964 -byte-code 22 0.436 76129 -selected-window 20 0.396 51883 -walk-windows 19 0.376 12964 -let 18 0.357 13746 -next-window 16 0.317 25928 -proof-toolbar-refresh 13 0.258 14445 -while 13 0.258 13710 -proof-shell-filter 11 0.218 12964 -process-mark 11 0.218 39137 -save-excursion 10 0.198 13741 -setq 10 0.198 27010 -and 9 0.178 27701 -goto-char 8 0.159 27695 -run-hook-with-args 8 0.159 13211 -if 7 0.139 33491 -font-lock-fontify-keywords-region 6 0.119 740 -#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 6 0.119 11268 -get-buffer-process 6 0.119 26242 -char-to-string 6 0.119 12964 -redisplay-echo-area 6 0.119 253 -specifier-instance 6 0.119 656 -itimerp 5 0.099 5713 -1- 5 0.099 13209 -point 5 0.099 27523 -buffer-name 4 0.079 13766 -current-buffer 4 0.079 13210 -window-start 4 0.079 12963 -< 4 0.079 6236 -itimer-timer-driver 4 0.079 380 -default-mouse-motion-handler 4 0.079 656 -featurep 4 0.079 2693 -force-mode-line-update 4 0.079 12963 -comint-watch-for-password-prompt 4 0.079 12964 -proof-shell-process-urgent-messages 3 0.059 12964 -font-lock-fontify-syntactically-region 3 0.059 740 -incf 3 0.059 11268 -marker-position 3 0.059 12968 -set-marker 3 0.059 13210 -itimer-time-difference 3 0.059 1140 -process-buffer 3 0.059 12963 -event-window 2 0.040 1312 -window-minibuffer-p 2 0.040 12964 -window-buffer 2 0.040 26524 -- 2 0.040 12967 -move-to-left-margin 2 0.040 246 -remove-message 2 0.040 253 -event-buffer 2 0.040 656 -font-lock-default-unfontify-region 2 0.040 740 -font-lock-after-change-function 2 0.040 494 -buffer-substring 2 0.040 493 -insert-string 2 0.040 253 -event-over-modeline-p 1 0.020 537 -event-glyph-extent 1 0.020 656 -set-syntax-table 1 0.020 740 -pointer-image-instance-p 1 0.020 1913 -extent-start-position 1 0.020 494 -make-extent 1 0.020 527 -detach-extent 1 0.020 495 -extent-at 1 0.020 363 -itimer-value 1 0.020 2660 -itimer-is-idle 1 0.020 2280 -set-extent-property 1 0.020 1024 -highlight-extent 1 0.020 656 -pos-visible-in-window-p 1 0.020 9 -glyph-property-instance 1 0.020 656 -get-text-property 1 0.020 492 -put-nonduplicable-text-property 1 0.020 1480 -next-single-property-change 1 0.020 246 -quote 1 0.020 13798 -marker-buffer 1 0.020 12963 -itimer-run-expired-timers 1 0.020 380 -aset 1 0.020 5280 -log-message 1 0.020 246 -min 1 0.020 13209 -current-left-margin 1 0.020 246 -display-message 1 0.020 246 -fw-frame 1 0.020 656 -font-lock-fontify-region 1 0.020 740 -font-lock-append-text-property 1 0.020 246 -substring 1 0.020 247 -proof-response-buffer-display 1 0.020 246 -delq 1 0.020 246 -syntactically-sectionize 1 0.020 740 -format 1 0.020 238 -proof-file-truename 1 0.020 88 -newline 1 0.020 246 -store-match-data 1 0.020 742 -proof-zap-commas-region 1 0.020 494 -specifierp 1 0.020 656 -log-message-filter 1 0.020 246 ------------------------------------------------------------------------ -Total 5047 100.00 - - -One tick = 1 ms - |