src/Pure/Thy/latex.ML
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;
2000-10-10 wenzelm 2000-10-10 fully enclose "\isadigit{...}"; \<^foo> produces "\isactrlfoo ";
2000-09-11 wenzelm 2000-09-11 define \isabellecontext;
2000-08-30 wenzelm 2000-08-30 token trans: removed \mbox to achieve proper italic correction;
2000-08-28 wenzelm 2000-08-28 added tex_trailer;
2000-08-21 wenzelm 2000-08-21 more \isachars; added \isadigit; simplified command markup;
2000-08-19 wenzelm 2000-08-19 output \isachar;
2000-08-08 wenzelm 2000-08-08 token translation: enclose "\\mbox{" "}";
2000-08-03 wenzelm 2000-08-03 improved output of space symbol;
2000-06-26 wenzelm 2000-06-26 tuned;
2000-06-25 wenzelm 2000-06-25 adapted to improved presentation;
2000-06-06 wenzelm 2000-06-06 session.tex: nsert blank lines in order to guarantee new paragraphs for each file (otherwise TeX would easily choke on large input);
2000-05-24 wenzelm 2000-05-24 proper token_translation for latex mode;
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-03 wenzelm 2000-04-03 support markup environments;
2000-03-17 wenzelm 2000-03-17 old_symbol_source: include header;
2000-03-15 wenzelm 2000-03-15 tuned comments; renamed isabelle env; proper symbol output for "latex" mode;
2000-02-04 wenzelm 2000-02-04 added old_symbol_source; tuned;