src/Pure/Isar/outer_syntax.scala
2016-07-10 wenzelm 2016-07-10 tuned signature: more uniform Keyword.spec;
2016-07-07 wenzelm 2016-07-07 clarified signature;
2016-02-28 wenzelm 2016-02-28 discontinued old 'header';
2016-01-24 wenzelm 2016-01-24 proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;
2015-10-17 wenzelm 2015-10-17 added 'paragraph', 'subparagraph';
2015-07-08 wenzelm 2015-07-08 clarified text folds: proof ... qed counts as extra block;
2015-07-08 wenzelm 2015-07-08 tuned;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 wenzelm 2015-04-04 more general notion of command span: command keyword not necessarily at start; support for special 'private' prefix for local_theory commands; clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;
2015-03-17 wenzelm 2015-03-17 misc tuning and simplification;
2015-03-15 wenzelm 2015-03-15 hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;
2015-03-15 wenzelm 2015-03-15 more command categories, as in ML;
2015-03-12 wenzelm 2015-03-12 clarified command content;
2015-01-08 wenzelm 2015-01-08 tuned;
2014-12-09 wenzelm 2014-12-09 tuned signature;
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-12-02 wenzelm 2014-12-02 node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;
2014-12-01 wenzelm 2014-12-01 more merge operations;
2014-11-07 wenzelm 2014-11-07 tuned outline;
2014-11-05 wenzelm 2014-11-05 more uniform header_keywords in ML/Scala; tuned signature;
2014-11-05 wenzelm 2014-11-05 clarified representation of type Keywords; tuned signature;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.Keywords;
2014-11-05 wenzelm 2014-11-05 clarified minor/major lexicon (like ML version);
2014-11-02 wenzelm 2014-11-02 uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete control command category;
2014-10-21 wenzelm 2014-10-21 tuned;
2014-10-21 wenzelm 2014-10-21 support for structure matching; misc tuning;
2014-10-21 wenzelm 2014-10-21 tuned rendering;
2014-10-21 wenzelm 2014-10-21 clarified tree root;
2014-10-19 wenzelm 2014-10-19 tuned signature and modules;
2014-10-18 wenzelm 2014-10-18 more folds;
2014-10-18 wenzelm 2014-10-18 clarified Line_Structure wrt. command span;
2014-10-18 wenzelm 2014-10-18 tuned signature;
2014-10-16 wenzelm 2014-10-16 more explicit Line_Nesting;
2014-10-16 wenzelm 2014-10-16 tuned comments;
2014-10-16 wenzelm 2014-10-16 support line context with depth; basic setup for "isabelle" fold handling; misc tuning;
2014-09-30 wenzelm 2014-09-30 tuned;
2014-08-12 wenzelm 2014-08-12 clarified Position.Identified: do not require range from prover, default to command position;
2014-08-12 wenzelm 2014-08-12 maintain Command_Range position as in ML;
2014-08-12 wenzelm 2014-08-12 tuned signature;
2014-08-12 wenzelm 2014-08-12 tuned signature;
2014-08-12 wenzelm 2014-08-12 separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
2014-08-11 wenzelm 2014-08-11 more explicit type Span in Scala, according to ML version;
2014-04-03 wenzelm 2014-04-03 more abstract Prover.Syntax, as proposed by Carst Tankink;
2014-03-29 wenzelm 2014-03-29 tuned signature;
2014-02-25 wenzelm 2014-02-25 tuned signature;
2014-02-22 wenzelm 2014-02-22 refined language context: antiquotes; support default completions, with move of caret position; tuned signature;
2014-02-20 wenzelm 2014-02-20 default completion context via outer syntax; no symbol completion for ML files; tuned;
2014-02-16 wenzelm 2014-02-16 tuned signature -- emphasize line-oriented aspect;
2014-02-14 wenzelm 2014-02-14 tuned signature (in accordance to ML version);
2014-02-14 wenzelm 2014-02-14 tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
2013-11-18 wenzelm 2013-11-18 inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;
2013-11-17 wenzelm 2013-11-17 explicit indication of thy_load commands;
2013-08-29 wenzelm 2013-08-29 explicit indication of outer syntax with no tokens; uniform Isabelle.markers, based on syntax specification -- no tokens for NEWS;
2013-06-24 wenzelm 2013-06-24 improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first; tuned signature;
2013-05-18 wenzelm 2013-05-18 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
2012-12-07 wenzelm 2012-12-07 adhoc recovery from spurious NPEs, similar quantum-effect behind 7c8ce63a3c00;
2012-11-19 wenzelm 2012-11-19 alternative completion for outer syntax keywords;
2012-08-22 wenzelm 2012-08-22 find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;