src/Pure/Thy/latex.ML
2017-06-06 wenzelm 2017-06-06 tuned signature;
2017-06-06 wenzelm 2017-06-06 discontinued obsolete print mode;
2016-11-27 wenzelm 2016-11-27 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
2016-09-22 wenzelm 2016-09-22 discontinued raw symbols; discontinued Symbol.source; use initial Symbol.explode;
2016-09-22 wenzelm 2016-09-22 raw control symbols are superseded by Latex.embed_raw;
2016-08-02 wenzelm 2016-08-02 proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
2015-11-06 wenzelm 2015-11-06 more formal treatment of control symbols;
2015-11-04 wenzelm 2015-11-04 avoid ligatures;
2015-10-26 wenzelm 2015-10-26 clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
2015-10-22 wenzelm 2015-10-22 more robust ASCII output: avoid ligatures of quotes;
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-10-18 wenzelm 2015-10-18 clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned;
2015-10-18 wenzelm 2015-10-18 support control symbol antiquotations;
2015-10-17 wenzelm 2015-10-17 clarified Latex.environment;
2015-10-15 wenzelm 2015-10-15 clarified modules;
2015-10-13 wenzelm 2015-10-13 tuned signature (cf. XML.trim_blanks);
2015-10-12 wenzelm 2015-10-12 allow control symbols within markup body;
2015-03-25 wenzelm 2015-03-25 tuned signature;
2014-12-09 wenzelm 2014-12-09 imitate command markup and rendering of Isabelle/jEdit in HTML output;
2014-12-03 wenzelm 2014-12-03 clarified token kind;
2014-11-30 wenzelm 2014-11-30 tuned signature -- prefer Input.source;
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-02 wenzelm 2014-11-02 more flexibile \setisabellecontext, independently of header;
2014-11-01 wenzelm 2014-11-01 command-line terminator ";" is no longer accepted;
2014-10-20 wenzelm 2014-10-20 avoid odd ligatures;
2014-10-20 wenzelm 2014-10-20 official support for "tt" style variants, avoid fragile \verb in LaTeX; official document antiquotation @{verbatim};
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 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 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind; tuned message;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-08-23 wenzelm 2013-08-23 discontinued unused antiquotation blocks;
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-09-24 wenzelm 2012-09-24 more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
2012-09-12 wenzelm 2012-09-12 discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
2012-07-31 wenzelm 2012-07-31 more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;
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-07-08 wenzelm 2011-07-08 discontinued special treatment of hard tabulators;
2011-06-20 wenzelm 2011-06-20 more tolerant Symbol.decode;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
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-11-07 wenzelm 2010-11-07 basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
2010-09-23 haftmann 2010-09-23 removed superfluous output_typewriter from cs 65064e8f269
2010-09-16 haftmann 2010-09-16 added output_typewriter from doc-src/more_antiquote.ML
2010-06-24 wenzelm 2010-06-24 explicit treatment of UTF8 character sequences as Isabelle symbols;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2009-03-22 wenzelm 2009-03-22 simplified Antiquote.read (again);
2009-03-20 wenzelm 2009-03-20 Antiquote.read: argument for reporting text;
2009-03-19 wenzelm 2009-03-19 parameterized datatype antiquote and read operation;
2009-03-19 wenzelm 2009-03-19 Antiquote.Text: keep full position information;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-02 wenzelm 2009-01-02 Markup.no_output;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-08-15 wenzelm 2008-08-15 renamed T.source_of' to T.source_position_of;
2008-08-14 wenzelm 2008-08-14 antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-08-07 wenzelm 2008-08-07 simplified Antiquote signature;