src/Pure/Isar/outer_syntax.ML
2014-05-20 wenzelm 2014-05-20 afford strict check (see also AFP/a8e08d947f0a);
2014-05-12 wenzelm 2014-05-12 tuned message;
2014-05-07 wenzelm 2014-05-07 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2014-03-18 wenzelm 2014-03-18 clarified bootstrap process: switch to ML with context and antiquotations earlier;
2014-02-24 wenzelm 2014-02-24 tuned signature;
2014-02-14 wenzelm 2014-02-14 tuned message;
2014-02-13 wenzelm 2014-02-13 explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
2013-12-13 wenzelm 2013-12-13 clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-04-05 wenzelm 2013-04-05 tuned signature -- agree with markup terminology;
2013-02-25 wenzelm 2013-02-25 tuned comment;
2013-02-24 wenzelm 2013-02-24 simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored; eliminated separate Outer_Syntax.read_element;
2013-02-20 wenzelm 2013-02-20 support nested Thy_Syntax.element; more explicit Keyword.is_proof_body; tuned;
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;
2012-11-26 wenzelm 2012-11-26 more general sendback properties; support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
2012-11-26 wenzelm 2012-11-26 refined outer syntax 'help' command;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-25 wenzelm 2012-09-25 tuned;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-24 wenzelm 2012-08-24 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-20 wenzelm 2012-08-20 added keyword kind "thy_load" (with optional list of file extensions);
2012-08-11 wenzelm 2012-08-11 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
2012-08-11 wenzelm 2012-08-11 clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
2012-08-09 wenzelm 2012-08-09 some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
2012-08-02 wenzelm 2012-08-02 report commands as formal entities, with def/ref positions;
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure.thy;
2012-07-05 wenzelm 2012-07-05 internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
2012-04-10 wenzelm 2012-04-10 static relevance of proof via syntax keywords;
2012-03-19 wenzelm 2012-03-19 allow keyword tags to be redefined, but not the command category;
2012-03-16 wenzelm 2012-03-16 check declared vs. defined commands at end of session;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16 wenzelm 2012-03-16 define keywords early when processing the theory header, before running the body commands;
2012-03-16 wenzelm 2012-03-16 clarified Keyword.is_keyword: union of minor and major; misc tuning and simplification;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-12 wenzelm 2012-03-12 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 wenzelm 2011-09-06 bulk reports for improved message throughput;
2011-09-02 wenzelm 2011-09-02 tuned;
2011-09-02 wenzelm 2011-09-02 more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
2011-08-25 wenzelm 2011-08-25 tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
2011-08-21 wenzelm 2011-08-21 tuned Parse.group: delayed failure message;
2011-08-13 wenzelm 2011-08-13 simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13 wenzelm 2011-08-13 simplified Toplevel.init_theory: discontinued special master argument;
2011-07-08 wenzelm 2011-07-08 moved Outer_Syntax.load_thy to Thy_Load.load_thy; tuned signatures; tuned module dependencies;
2011-07-08 wenzelm 2011-07-08 less stateful outer_syntax;
2011-07-01 wenzelm 2011-07-01 clarified Thy_Syntax.element;
2011-03-26 wenzelm 2011-03-26 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
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;
2011-02-05 wenzelm 2011-02-05 more tracing information via Par_List.map_name;
2011-01-13 wenzelm 2011-01-13 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2011-01-09 wenzelm 2011-01-09 more direct treatment of Position.end_offset; tuned;
2010-11-13 wenzelm 2010-11-13 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);
2010-08-15 wenzelm 2010-08-15 rename "unit" to "atom", to avoid confusion with the unit type;
2010-08-09 wenzelm 2010-08-09 Isabelle_Process: separate input fifo for commands (still using the old tty protocol); some partial workarounds for Cygwin;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-07-27 wenzelm 2010-07-27 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; explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database; Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command; added Thy_Load.begin_theory for clarity; structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader; moved some basic commands from isar_cmd.ML to isar_syn.ML; misc tuning and simplification;
2010-07-25 wenzelm 2010-07-25 simplified handling of theory begin/end wrt. toplevel and theory loader;