src/Pure/Thy/thy_syntax.ML
2015-10-09 wenzelm 2015-10-09 more direct HTML presentation, without print mode;
2015-03-25 wenzelm 2015-03-25 tuned signature;
2014-12-10 wenzelm 2014-12-10 more explicit markup for improper commands; clarified CSS rendering;
2014-12-09 wenzelm 2014-12-09 imitate command markup and rendering of Isabelle/jEdit in HTML output;
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-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
2014-11-01 wenzelm 2014-11-01 recover via scanner; 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 clarified Command_Span in accordance to Scala (see also c2c1e5944536);
2014-08-11 wenzelm 2014-08-11 more explicit type Span in Scala, according to ML version;
2014-05-28 wenzelm 2014-05-28 tuned signature;
2014-03-05 wenzelm 2014-03-05 suppress short abbreviations more uniformly, for outer and quasi-outer syntax; tuned signature;
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-25 wenzelm 2014-02-25 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind; tuned message;
2014-02-24 wenzelm 2014-02-24 tuned signature;
2014-01-22 wenzelm 2014-01-22 clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-11-19 wenzelm 2013-11-19 release file errors at runtime: Command.eval instead of Command.read;
2013-11-16 wenzelm 2013-11-16 tuned signature;
2013-09-24 wenzelm 2013-09-24 clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer); simplified command padding: always newline, despite lack of indentation;
2013-03-13 wenzelm 2013-03-13 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;
2013-03-03 wenzelm 2013-03-03 more Thy_Syntax.element operations;
2013-02-24 wenzelm 2013-02-24 simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored; eliminated separate Outer_Syntax.read_element;
2013-02-24 wenzelm 2013-02-24 tuned;
2013-02-20 wenzelm 2013-02-20 support nested Thy_Syntax.element; more explicit Keyword.is_proof_body; tuned;
2012-11-26 wenzelm 2012-11-26 more uniform Symbol.is_ascii_identifier in ML/Scala;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-22 wenzelm 2012-08-22 tuned errors;
2012-08-20 wenzelm 2012-08-20 some support for inlining file content into outer syntax token language;
2012-08-20 wenzelm 2012-08-20 tuned;
2012-08-11 wenzelm 2012-08-11 more liberal scanning of potentially malformed symbols;
2012-08-11 wenzelm 2012-08-11 clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
2012-08-10 wenzelm 2012-08-10 sneak message into "bad" markup as property -- to be displayed after YXML parsing;
2012-08-10 wenzelm 2012-08-10 discontinued mostly unused markup for command spans;
2012-08-10 wenzelm 2012-08-10 more visible markup of malformed input as "bad";
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-03-04 wenzelm 2012-03-04 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-09-06 wenzelm 2011-09-06 bulk reports for improved message throughput;
2011-09-04 wenzelm 2011-09-04 eliminated markup for plain identifiers (frequent but insignificant); reduced "black" markup (outer string etc. takes care of it already);
2011-09-02 wenzelm 2011-09-02 more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
2011-08-21 wenzelm 2011-08-21 tuned;
2011-08-21 wenzelm 2011-08-21 discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;
2011-07-01 wenzelm 2011-07-01 clarified Thy_Syntax.element;
2011-06-18 wenzelm 2011-06-18 more uniform treatment of "keyword" vs. "operator";
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-01-09 wenzelm 2011-01-09 more direct treatment of Position.end_offset; tuned;
2010-12-04 wenzelm 2010-12-04 eliminated obsolete Token.Malformed -- subsumed by Token.Error;
2010-11-13 wenzelm 2010-11-13 report malformed symbols;
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-10-30 wenzelm 2010-10-30 support for floating-point tokens in outer syntax (coinciding with inner syntax version);
2010-10-25 wenzelm 2010-10-25 explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-08-18 wenzelm 2010-08-18 uniform Markup.empty/Markup.Empty in ML and Scala;
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-08-15 wenzelm 2010-08-15 rename "unit" to "atom", to avoid confusion with the unit type;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-30 wenzelm 2010-05-30 more detailed token markup, including command kind as sub_kind; type-safe access to Command.HighlightInfo;
2010-05-30 wenzelm 2010-05-30 simplified command/keyword markup;