2011-03-26 ago present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
2011-03-20 ago structure Timing: covers former start_timing/end_timing and Output.timeit etc;
2011-02-05 ago more tracing information via Par_List.map_name;
2011-01-13 ago Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2011-01-09 ago more direct treatment of Position.end_offset;
2010-11-13 ago simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
2010-08-15 ago rename "unit" to "atom", to avoid confusion with the unit type;
2010-08-09 ago Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
2010-08-08 ago explicitly distinguish Output.status (essential feedback) vs. (useful markup);
2010-07-27 ago simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
2010-07-25 ago simplified handling of theory begin/end wrt. toplevel and theory loader;
2010-07-22 ago load_thy: parallel parsing of units, which consist of statement/proof each;
2010-07-21 ago deps_thy/load_thy: store compact text to reduce space by factor 12;
2010-07-21 ago eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
2010-07-20 ago eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
2010-07-05 ago Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-17 ago renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-17 ago centralized legacy aliases;
2010-05-15 ago renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2009-10-27 ago non-critical atomic accesses;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-03-18 ago de-camelized Symbol_Pos;
2009-03-13 ago eliminated type Args.T;
2009-01-10 ago load_thy: explicit after_load phase for presentation;
2009-01-07 ago added local_theory';
2009-01-02 ago renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
2009-01-02 ago added type 'a parser, simplified signature;
2008-09-30 ago load_thy: more precise treatment of improper cmd or proof (notably 'oops');
2008-09-30 ago load_thy: Toplevel.excursion based on units of command/proof pairs;
2008-09-30 ago simplified process_file, eliminated Toplevel.excursion;
2008-08-14 ago P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-13 ago load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
2008-08-12 ago Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-11 ago Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
2008-08-07 ago updated type of nested sources;
2008-08-04 ago simplified prepare_command;
2008-07-15 ago renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
2008-07-14 ago adapted IsarCmd.init_theory;
2008-07-02 ago Toplevel.init_theory: pass name explicitly;
2008-06-25 ago moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-05-24 ago added local_theory command wrappers;
2008-05-14 ago renamed Position.path to Path.position;
2008-04-17 ago Pretty.mark;
2008-04-10 ago eliminated unused trace, read;
2008-04-10 ago export load_thy -- no backpatching;
2008-04-10 ago moved structure Isar to isar.ML;
2008-03-27 ago added process_file;
2008-03-26 ago adapted to Context.thread_data interface;
2008-03-18 ago theory loader: discontinued *attached* ML scripts;
2008-03-15 ago tuned messages;
2008-01-05 ago secure_main: removed separate welcome;
2008-01-01 ago try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;
2007-12-17 ago cond_timeit: added message argument;
2007-12-08 ago secure_main: enforces terminator, to gain robustness;
2007-12-07 ago added off-line parse;
2007-12-04 ago added Isar.secure_main;
2007-10-06 ago report on keyword/command declarations;
2007-10-06 ago simplified interfaces for outer syntax;