| 2015-07-06 |
wenzelm |
2015-07-06 |
plain string output, without funny control chars;
|
file | diff | annotate |
| 2015-07-06 |
wenzelm |
2015-07-06 |
proper outer syntax category, e.g. relevant for PIDE markup;
|
file | diff | annotate |
| 2015-06-29 |
wenzelm |
2015-06-29 |
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
|
file | diff | annotate |
| 2015-04-06 |
wenzelm |
2015-04-06 |
@{command_spec} is superseded by @{command_keyword};
|
file | diff | annotate |
| 2015-04-06 |
wenzelm |
2015-04-06 |
more position information and PIDE markup for command keywords;
|
file | diff | annotate |
| 2014-12-03 |
wenzelm |
2014-12-03 |
tuned signature;
|
file | diff | annotate |
| 2014-11-26 |
wenzelm |
2014-11-26 |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file | diff | annotate |
| 2014-11-07 |
wenzelm |
2014-11-07 |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
|
file | diff | annotate |
| 2014-11-06 |
wenzelm |
2014-11-06 |
tuned signature;
|
file | diff | annotate |
| 2014-11-05 |
wenzelm |
2014-11-05 |
more frugal keywords;
|
file | diff | annotate |
| 2014-11-05 |
wenzelm |
2014-11-05 |
explicit type Keyword.keywords;
tuned signature;
|
file | diff | annotate |
| 2014-11-03 |
wenzelm |
2014-11-03 |
eliminated unused int_only flag (see also c12484a27367);
just proper commands;
|
file | diff | annotate |
| 2014-08-12 |
wenzelm |
2014-08-12 |
tuned signature according to Scala version -- prefer explicit argument;
|
file | diff | annotate |
| 2014-05-08 |
wenzelm |
2014-05-08 |
some position markup to help locating the query context, e.g. from "Info" dockable;
|
file | diff | annotate |
| 2014-05-08 |
wenzelm |
2014-05-08 |
tuned message: more compact, imitate actual command line;
|
file | diff | annotate |
| 2014-05-07 |
wenzelm |
2014-05-07 |
tuned message -- more context for detached window etc.;
|
file | diff | annotate |
| 2014-04-27 |
wenzelm |
2014-04-27 |
tuned;
|
file | diff | annotate |
| 2014-04-26 |
wenzelm |
2014-04-26 |
tuned message;
|
file | diff | annotate |
| 2014-04-26 |
wenzelm |
2014-04-26 |
PIDE support for find_consts;
|
file | diff | annotate |
| 2014-03-12 |
wenzelm |
2014-03-12 |
tuned signature;
|
file | diff | annotate |
| 2014-03-10 |
wenzelm |
2014-03-10 |
abstract type Name_Space.table;
clarified pretty_locale_deps: sort strings;
clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
|
file | diff | annotate |
| 2013-07-18 |
wenzelm |
2013-07-18 |
tuned messages -- avoid text folds stemming from Pretty.chunks;
|
file | diff | annotate |
| 2013-04-09 |
wenzelm |
2013-04-09 |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;
|
file | diff | annotate |
| 2012-11-26 |
wenzelm |
2012-11-26 |
tuned command descriptions;
|
file | diff | annotate |
| 2012-10-17 |
wenzelm |
2012-10-17 |
more formal markup;
|
file | diff | annotate |
| 2012-08-02 |
wenzelm |
2012-08-02 |
more official command specifications, including source position;
|
file | diff | annotate |
| 2012-03-17 |
wenzelm |
2012-03-17 |
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
tuned;
|
file | diff | annotate |
| 2012-03-16 |
wenzelm |
2012-03-16 |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file | diff | annotate |
| 2012-02-27 |
wenzelm |
2012-02-27 |
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 |
| 2012-02-27 |
wenzelm |
2012-02-27 |
prefer uniform Timing.message -- avoid assumption about sequential execution;
|
file | diff | annotate |
| 2011-04-16 |
wenzelm |
2011-04-16 |
modernized structure Proof_Context;
|
file | diff | annotate |
| 2011-03-20 |
wenzelm |
2011-03-20 |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;
|
file | diff | annotate |
| 2010-08-11 |
wenzelm |
2010-08-11 |
standardized pretty printing of consts (e.g. see find_theorems, print_theory);
|
file | diff | annotate |
| 2010-08-11 |
wenzelm |
2010-08-11 |
misc tuning and simplification;
|
file | diff | annotate |
| 2010-08-11 |
wenzelm |
2010-08-11 |
simplified/unified command setup;
|
file | diff | annotate |
| 2010-05-15 |
wenzelm |
2010-05-15 |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file | diff | annotate |
| 2010-05-15 |
wenzelm |
2010-05-15 |
refer directly to structure Keyword and Parse;
eliminated old-style structure aliases K and P;
|
file | diff | annotate |
| 2010-03-20 |
wenzelm |
2010-03-20 |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file | diff | annotate |
| 2009-10-29 |
wenzelm |
2009-10-29 |
less hermetic ML;
parse_pattern: apply Consts.intern only once (Why is this done anyway?);
modernized structure names;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
conceal consts via name space, not tags;
|
file | diff | annotate |
| 2009-09-30 |
wenzelm |
2009-09-30 |
handle Type.TYPE_MATCH, not arbitrary exceptions;
|
file | diff | annotate |
| 2009-06-17 |
wenzelm |
2009-06-17 |
more detailed start_timing/end_timing;
|
file | diff | annotate |
| 2009-06-17 |
wenzelm |
2009-06-17 |
minor tuning according to Isabelle/ML conventions;
slightly less combinators;
|
file | diff | annotate |
| 2009-03-03 |
Timothy Bourke |
2009-03-03 |
Implement Makarius's suggestion for improved type pattern parsing.
|
file | diff | annotate |
| 2009-03-02 |
Timothy Bourke |
2009-03-02 |
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
|
file | diff | annotate |
| 2009-03-01 |
wenzelm |
2009-03-01 |
use long names for old-style fold combinators;
|
file | diff | annotate |
| 2009-03-01 |
wenzelm |
2009-03-01 |
avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
|
file | diff | annotate |
| 2009-02-27 |
wenzelm |
2009-02-27 |
observe basic Isabelle/ML coding conventions;
|
file | diff | annotate |
| 2009-02-27 |
wenzelm |
2009-02-27 |
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
|
file | diff | annotate | base |