src/Pure/Thy/latex.ML
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;
2008-08-07 wenzelm 2008-08-07 Antiquote.read/read_arguments;
2008-08-06 wenzelm 2008-08-06 adapted Antiq;
2008-06-24 wenzelm 2008-06-24 Antiquote.Open/Close;
2007-07-10 wenzelm 2007-07-10 Markup.add_mode;
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int; separate print_mode setup for Output/Pretty;
2007-04-12 wenzelm 2007-04-12 output_basic: added isaantiq markup (only inside verbatim tokens);
2006-03-14 wenzelm 2006-03-14 Output.add_mode: keyword component;
2005-09-01 wenzelm 2005-09-01 removed obsolete 'symbols' mode;
2005-08-29 wenzelm 2005-08-29 delimiter markup for verbatim tokens;
2005-08-28 wenzelm 2005-08-28 output_basic: handle AltString token;
2005-08-16 wenzelm 2005-08-16 eliminated datatype token; replaced output_tokens by separate output_XXX; replaced flag_markup by markup_true/false; added begin/end_delim, begin/end_tag;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2004-06-22 wenzelm 2004-06-22 tuned output;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-20 wenzelm 2004-06-20 Symbol.encode_raw;
2004-06-12 wenzelm 2004-06-12 added output_known_symbols; tuned;
2004-06-06 wenzelm 2004-06-06 no token translation / setup for Latex;
2004-06-05 wenzelm 2004-06-05 Symbol.decode;
2004-05-29 wenzelm 2004-05-29 handle raw symbols; Output.add_mode;
2004-04-26 wenzelm 2004-04-26 use Syntax.is_ascii_identifier;
2004-04-16 berghofe 2004-04-16 Replaced quote by Library.quote, since quote now refers to Symbol.quote
2004-04-14 schirmer 2004-04-14 * raw control symbols are of the form \<^raw:...> now. * again allowing symbols to begin with "\\" instead of "\" for compatibility with ML-strings of old style theory and ML-files and isa-ProofGeneral.
2004-01-27 schirmer 2004-01-27 \<^raw...> does no longer print an additional space.
2004-01-26 schirmer 2004-01-26 * Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy
2001-10-21 wenzelm 2001-10-21 flag_markup;
2001-10-10 berghofe 2001-10-10 Exported output_symbols.
2001-01-31 wenzelm 2001-01-31 strip_blanks moved to General/symbol.ML;
2001-01-21 wenzelm 2001-01-21 setuo indent: \isaindent;
2000-11-04 wenzelm 2000-11-04 isamarkup: handle % in input;
2000-10-18 wenzelm 2000-10-18 \isabellecontext: output_syms;