src/Pure/Isar/outer_syntax.ML
2012-11-26 ago more general sendback properties;
2012-11-26 ago refined outer syntax 'help' command;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-25 ago tuned;
2012-08-29 ago renamed Position.str_of to Position.here;
2012-08-24 ago check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-20 ago added keyword kind "thy_load" (with optional list of file extensions);
2012-08-11 ago clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
2012-08-11 ago clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
2012-08-09 ago some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
2012-08-02 ago report commands as formal entities, with def/ref positions;
2012-08-02 ago more official command specifications, including source position;
2012-08-01 ago more standard bootstrapping of Pure.thy;
2012-07-05 ago internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
2012-04-10 ago static relevance of proof via syntax keywords;
2012-03-19 ago allow keyword tags to be redefined, but not the command category;
2012-03-16 ago check declared vs. defined commands at end of session;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16 ago define keywords early when processing the theory header, before running the body commands;
2012-03-16 ago clarified Keyword.is_keyword: union of minor and major;
2012-03-15 ago declare command keywords via theory header, including strict checking outside Pure;
2012-03-12 ago refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
2011-09-06 ago bulk reports for improved message throughput;
2011-09-02 ago tuned;
2011-09-02 ago more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
2011-08-25 ago tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
2011-08-21 ago tuned Parse.group: delayed failure message;
2011-08-13 ago simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13 ago simplified Toplevel.init_theory: discontinued special master argument;
2011-07-08 ago moved Outer_Syntax.load_thy to Thy_Load.load_thy;
2011-07-08 ago less stateful outer_syntax;
2011-07-01 ago clarified Thy_Syntax.element;
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. Output.report (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);