src/Pure/Isar/outer_syntax.scala
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;
2012-08-21 wenzelm 2012-08-21 more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;
2012-08-21 wenzelm 2012-08-21 some support for thy_load_commands; clarified signatures;
2012-08-21 wenzelm 2012-08-21 clarified initialization of Thy_Load, Thy_Info, Session;
2012-08-20 wenzelm 2012-08-20 added keyword kind "thy_load" (with optional list of file extensions);
2012-08-07 wenzelm 2012-08-07 permissive outer syntax wrt. symbol recoding;
2012-08-07 wenzelm 2012-08-07 simplified Document.Node.Header -- internalized errors;
2012-08-07 wenzelm 2012-08-07 tuned signature;
2012-08-04 wenzelm 2012-08-04 refined outer syntax;
2012-08-03 wenzelm 2012-08-03 static outer syntax based on session specifications;
2012-04-14 wenzelm 2012-04-14 keyword ";" is declared via prover (as "minor", not "diag");
2012-03-16 wenzelm 2012-03-16 more abstract heading level;
2012-03-15 wenzelm 2012-03-15 maintain Version.syntax within document state; clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;
2012-03-15 wenzelm 2012-03-15 explicit Outer_Syntax.Decl;
2012-02-27 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2012-02-23 wenzelm 2012-02-23 streamlined abstract datatype;
2012-02-23 wenzelm 2012-02-23 streamlined abstract datatype;
2011-08-08 wenzelm 2011-08-08 avoid pointless completion of illegal control commands;
2011-07-12 wenzelm 2011-07-12 added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
2011-07-07 wenzelm 2011-07-07 simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style"; tuned implicit build/init messages;
2011-06-19 wenzelm 2011-06-19 some unicode chars for special control symbols;
2011-06-18 wenzelm 2011-06-18 hardwired abbreviations for standard control symbols;
2011-06-16 wenzelm 2011-06-16 some support for partial scans with explicit context; clarified junk vs. junk1;
2010-11-13 wenzelm 2010-11-13 somewhat adhoc replacement for 'thus' and 'hence'; complete words as short as 2 characters, e.g. "Un";
2010-11-10 wenzelm 2010-11-10 eliminated obsolete heading category -- superseded by heading_level;
2010-11-10 wenzelm 2010-11-10 treat main theory commands like headings, and nest anything else inside;
2010-11-10 wenzelm 2010-11-10 default Sidekick parser based on section headings;
2010-11-10 wenzelm 2010-11-10 some support for nested source structure, based on section headings;
2010-08-17 wenzelm 2010-08-17 report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
2010-05-17 wenzelm 2010-05-17 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
2010-05-15 wenzelm 2010-05-15 renamed Outer_Keyword to Keyword (in Scala);
2010-01-05 wenzelm 2010-01-05 tuned message;
2009-12-22 wenzelm 2009-12-22 renamed class Outer_Keyword to Outer_Syntax; renamed tokenize to scan (cf. ML version);