src/Pure/Isar/token.ML
2016-04-01 wenzelm 2016-04-01 tuned signature;
2016-03-31 wenzelm 2016-03-31 clarified modules;
2016-01-07 wenzelm 2016-01-07 prefer non-ASCII output;
2015-12-10 wenzelm 2015-12-10 make SML/NJ happy;
2015-12-09 wenzelm 2015-12-09 tuned;
2015-12-09 wenzelm 2015-12-09 tuned signature;
2015-12-09 wenzelm 2015-12-09 tuned;
2015-12-09 wenzelm 2015-12-09 clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
2015-11-10 wenzelm 2015-11-10 added document antiquotation @{theory_text}; tuned document;
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-10-18 wenzelm 2015-10-18 support control symbol antiquotations;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-02 wenzelm 2015-09-02 trim context more thoroughly;
2015-05-01 wenzelm 2015-05-01 modifier markup for all parsed tokens; report literal token markup, before re-assignment;
2015-04-09 wenzelm 2015-04-09 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
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-04-02 wenzelm 2015-04-02 tuned signature;
2015-04-02 wenzelm 2015-04-02 operation on embedded sources for Eisbach;
2015-04-02 wenzelm 2015-04-02 tuned -- emphasize semantics of already checked src;
2015-03-25 wenzelm 2015-03-25 tuned signature;
2015-03-24 wenzelm 2015-03-24 clarified input source;
2015-03-10 wenzelm 2015-03-10 clarified Token.check_src: intern at most once; Method.parse_internal for Eisbach: intern method names;
2015-03-07 wenzelm 2015-03-07 added declare_maxidx operations for Eisbach;
2014-12-10 wenzelm 2014-12-10 more explicit markup for improper commands; clarified CSS rendering;
2014-12-10 wenzelm 2014-12-10 tuned;
2014-12-09 wenzelm 2014-12-09 imitate command markup and rendering of Isabelle/jEdit in HTML output;
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-12-03 wenzelm 2014-12-03 clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-12-03 wenzelm 2014-12-03 clarified token kind;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-11-05 wenzelm 2014-11-05 eliminated pointless dynamic keywords (TTY legacy);
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-11-01 wenzelm 2014-11-01 tuned signature (see ab2483fad861);
2014-11-01 wenzelm 2014-11-01 recover via scanner; tuned signature;
2014-11-01 wenzelm 2014-11-01 simplified -- scanning is never interactive;
2014-11-01 wenzelm 2014-11-01 command-line terminator ";" is no longer accepted;
2014-10-31 wenzelm 2014-10-31 removed pointless markup; tuned comments;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete \<^sync> marker;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete tty and prompt;
2014-08-25 wenzelm 2014-08-25 tuned signature;
2014-08-21 wenzelm 2014-08-21 tuned;
2014-08-20 wenzelm 2014-08-20 support for declaration within token source;
2014-08-20 wenzelm 2014-08-20 support for nested Token.src within Token.T; tuned signature;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-15 wenzelm 2014-08-15 more informative Token.Name with history of morphisms; tuned signature;
2014-08-14 wenzelm 2014-08-14 more informative Token.Fact: retain name of dynamic fact (without selection);
2014-03-18 wenzelm 2014-03-18 more markup for improper elements;
2014-03-12 wenzelm 2014-03-12 clarified Markup.operator vs. Markup.delimiter; tuned color;
2014-03-12 wenzelm 2014-03-12 more explicit markup for Token.Literal; Markup.quasi_keyword for Parse.$$$ -- it is used within Args.syntax as well; Markup.operator for name of Args.syntax, to override outer keywords like "where"; tuned signature;
2014-03-05 wenzelm 2014-03-05 more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
2014-03-05 wenzelm 2014-03-05 more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;
2014-03-05 wenzelm 2014-03-05 suppress short abbreviations more uniformly, for outer and quasi-outer syntax; tuned signature;
2014-03-05 wenzelm 2014-03-05 clarified init_assignable: make double-sure that initial values are reset; more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-27 wenzelm 2014-02-27 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;
2014-02-25 wenzelm 2014-02-25 back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;
2014-02-25 wenzelm 2014-02-25 tuned message -- more markup;