| Thu, 18 Jul 2013 22:32:00 +0200 |
wenzelm |
tuned messages -- avoid text folds stemming from Pretty.chunks;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 10:26:27 +0200 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 12:36:54 +0200 |
wenzelm |
more official command specifications, including source position;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 11:23:14 +0100 |
wenzelm |
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 19:54:50 +0100 |
wenzelm |
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 17:39:34 +0100 |
wenzelm |
prefer uniform Timing.message -- avoid assumption about sequential execution;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 18:10:39 +0200 |
wenzelm |
standardized pretty printing of consts (e.g. see find_theorems, print_theory);
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 18:03:02 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 17:50:29 +0200 |
wenzelm |
simplified/unified command setup;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:56:02 +0100 |
wenzelm |
less hermetic ML;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 13:18:35 +0100 |
wenzelm |
conceal consts via name space, not tags;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:31:16 +0200 |
wenzelm |
handle Type.TYPE_MATCH, not arbitrary exceptions;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 17:07:26 +0200 |
wenzelm |
more detailed start_timing/end_timing;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 15:14:48 +0200 |
wenzelm |
minor tuning according to Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 12:14:52 +1100 |
Timothy Bourke |
Implement Makarius's suggestion for improved type pattern parsing.
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 18:11:39 +1100 |
Timothy Bourke |
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 16:22:37 +0100 |
wenzelm |
avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 16:05:40 +0100 |
wenzelm |
observe basic Isabelle/ML coding conventions;
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 15:46:22 +0100 |
wenzelm |
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
|
file |
diff |
annotate
| base
|