2014-03-29 ago wenzelm propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
2014-03-29 ago wenzelm tuned signature;
2014-03-29 ago wenzelm tuned signature;
2014-03-29 ago wenzelm tuned -- see Text.Range.overlaps(Range);
2014-03-29 ago nipkow tuned
2014-03-28 ago wenzelm tuned;
2014-03-27 ago wenzelm merged
2014-03-27 ago wenzelm tuned -- avoid code duplication;
2014-03-27 ago wenzelm tuned;
2014-03-27 ago wenzelm more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
2014-03-27 ago wenzelm back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
2014-03-27 ago wenzelm tuned;
2014-03-27 ago wenzelm redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
2014-03-27 ago wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-27 ago wenzelm more frugal merge of markup trees: non-overlapping tree counts as empty;
2014-03-27 ago wenzelm more frugal merge of markup trees: filter wrt. subsequent query;
2014-03-27 ago wenzelm tuned signature;
2014-03-27 ago wenzelm more careful treatment of multiple command states (eval + prints): merge content that is actually required;
2014-03-26 ago wenzelm tuned signature -- expose less intermediate information;
2014-03-26 ago wenzelm support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
2014-03-26 ago wenzelm less markup by default -- this is stored persistently in Isabelle/Scala;
2014-03-26 ago wenzelm clarified valid_id: always standardize towards static command.id;
2014-03-26 ago wenzelm prefer Context_Position where a context is available;
2014-03-26 ago wenzelm unused;
2014-03-26 ago wenzelm more uniform Execution.fork vs. Execution.print;
2014-03-26 ago wenzelm added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
2014-03-26 ago huffman tuned proofs
2014-03-26 ago paulson Some useful lemmas
2014-03-26 ago wenzelm tuned comments;
2014-03-26 ago wenzelm tuned load order;
2014-03-26 ago wenzelm superseded by (provide_)parse_files;
2014-03-26 ago wenzelm tuned;
2014-03-25 ago wenzelm merged
2014-03-25 ago wenzelm more warnings for recent versions of Poly/ML (see also fe1f6a1707f7);
2014-03-25 ago wenzelm eliminated dead code;
2014-03-25 ago wenzelm proper configuration option "ML_print_depth";
2014-03-25 ago wenzelm removed junk;
2014-03-25 ago wenzelm clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
2014-03-25 ago wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-25 ago wenzelm separate "sml" mode, suppress old "ml" mode altogether;
2014-03-25 ago wenzelm some SML examples;
2014-03-25 ago wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-25 ago wenzelm updated to scala-2.10.4;
2014-03-25 ago hoelzl cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
2014-03-25 ago traytel prove theorems with fixed variables (export afterwards)
2014-03-24 ago huffman generalized theorems about derivatives of limits of sequences of funtions
2014-03-24 ago wenzelm removed unused 'ax_specification', to give 'specification' a chance to become localized;
2014-03-24 ago wenzelm merged;
2014-03-24 ago wenzelm merged
2014-03-24 ago wenzelm proper Sign.full_name to get internal name (like Sign.add_consts);
2014-03-24 ago wenzelm formal check of user input, avoiding direct references of interal names;
2014-03-24 ago wenzelm discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-20 ago huffman tuned proofs
2014-03-24 ago traytel made tactic more robust
2014-03-24 ago traytel inline helper function
2014-03-24 ago paulson rearranging some deriv theorems
2014-03-23 ago wenzelm modernized approximation, avoiding bad name binding;
2014-03-23 ago wenzelm more sensible treatment of quasi-local variables (NB: Variable.add_fixes is only for term variables, while Variable.declare takes care of types within given terms);
2014-03-22 ago wenzelm merged
2014-03-22 ago wenzelm more antiquotations;