src/Pure/Thy/latex.ML
Tue, 24 Jun 2008 19:43:20 +0200 wenzelm Antiquote.Open/Close;
Tue, 10 Jul 2007 16:45:06 +0200 wenzelm Markup.add_mode;
Sat, 07 Jul 2007 00:15:02 +0200 wenzelm simplified pretty token metric: type int;
Thu, 12 Apr 2007 15:01:13 +0200 wenzelm output_basic: added isaantiq markup (only inside verbatim tokens);
Tue, 14 Mar 2006 22:06:33 +0100 wenzelm Output.add_mode: keyword component;
Thu, 01 Sep 2005 15:58:10 +0200 wenzelm removed obsolete 'symbols' mode;
Mon, 29 Aug 2005 16:18:07 +0200 wenzelm delimiter markup for verbatim tokens;
Sun, 28 Aug 2005 16:04:53 +0200 wenzelm output_basic: handle AltString token;
Tue, 16 Aug 2005 13:42:52 +0200 wenzelm eliminated datatype token;
Thu, 21 Apr 2005 22:02:06 +0200 wenzelm superceded by Pure.thy and CPure.thy;
Tue, 22 Jun 2004 09:51:23 +0200 wenzelm tuned output;
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sun, 20 Jun 2004 09:26:48 +0200 wenzelm Symbol.encode_raw;
Sat, 12 Jun 2004 22:45:46 +0200 wenzelm added output_known_symbols; tuned;
Sun, 06 Jun 2004 18:35:11 +0200 wenzelm no token translation / setup for Latex;
Sat, 05 Jun 2004 13:07:31 +0200 wenzelm Symbol.decode;
Sat, 29 May 2004 15:08:21 +0200 wenzelm handle raw symbols; Output.add_mode;
Mon, 26 Apr 2004 15:01:05 +0200 wenzelm use Syntax.is_ascii_identifier;
Fri, 16 Apr 2004 18:45:56 +0200 berghofe Replaced quote by Library.quote, since quote now refers to Symbol.quote
Wed, 14 Apr 2004 12:19:16 +0200 schirmer * raw control symbols are of the form \<^raw:...> now.
Tue, 27 Jan 2004 09:44:14 +0100 schirmer \<^raw...> does no longer print an additional space.
Mon, 26 Jan 2004 10:34:02 +0100 schirmer * Support for raw latex output in control symbols: \<^raw...>
Sun, 21 Oct 2001 19:40:39 +0200 wenzelm flag_markup;
Wed, 10 Oct 2001 18:41:13 +0200 berghofe Exported output_symbols.
Wed, 31 Jan 2001 22:16:22 +0100 wenzelm strip_blanks moved to General/symbol.ML;
Sun, 21 Jan 2001 19:55:25 +0100 wenzelm setuo indent: \isaindent;
Sat, 04 Nov 2000 18:42:29 +0100 wenzelm isamarkup: handle % in input;
Wed, 18 Oct 2000 23:27:16 +0200 wenzelm \isabellecontext: output_syms;
Tue, 10 Oct 2000 23:44:44 +0200 wenzelm fully enclose "\isadigit{...}";
Mon, 11 Sep 2000 17:37:09 +0200 wenzelm define \isabellecontext;
Wed, 30 Aug 2000 17:54:05 +0200 wenzelm token trans: removed \mbox to achieve proper italic correction;
Mon, 28 Aug 2000 20:32:55 +0200 wenzelm added tex_trailer;
Mon, 21 Aug 2000 18:38:27 +0200 wenzelm more \isachars;
Sat, 19 Aug 2000 12:49:19 +0200 wenzelm output \isachar;
Tue, 08 Aug 2000 16:57:44 +0200 wenzelm token translation: enclose "\\mbox{" "}";
Thu, 03 Aug 2000 00:44:08 +0200 wenzelm improved output of space symbol;
Mon, 26 Jun 2000 00:23:17 +0200 wenzelm tuned;
Sun, 25 Jun 2000 23:55:22 +0200 wenzelm adapted to improved presentation;
Tue, 06 Jun 2000 20:31:22 +0200 wenzelm session.tex: nsert blank lines in order to guarantee new paragraphs
Wed, 24 May 2000 19:09:36 +0200 wenzelm proper token_translation for latex mode;
Sun, 21 May 2000 14:33:46 +0200 wenzelm replaced {{ }} by { };
Fri, 05 May 2000 22:18:40 +0200 wenzelm GPLed;
Mon, 03 Apr 2000 14:00:16 +0200 wenzelm support markup environments;
Fri, 17 Mar 2000 16:30:45 +0100 wenzelm old_symbol_source: include header;
Wed, 15 Mar 2000 18:24:27 +0100 wenzelm tuned comments;
Fri, 04 Feb 2000 21:44:38 +0100 wenzelm added old_symbol_source;
Mon, 10 Jan 2000 17:08:41 +0100 wenzelm isabellesimple: avoid paragraph;
Fri, 29 Oct 1999 12:49:50 +0200 wenzelm \isasymbol renamed to \isasym;
Thu, 21 Oct 1999 18:43:06 +0200 wenzelm output \isasymbols;
Wed, 13 Oct 1999 19:41:18 +0200 wenzelm markup / varbatim: comment out (%) newline char;
Fri, 08 Oct 1999 15:09:14 +0200 wenzelm improved presentation;
Thu, 07 Oct 1999 17:20:58 +0200 wenzelm verbatim markup tokens;
Wed, 06 Oct 1999 18:12:35 +0200 wenzelm improved presentation;
Wed, 06 Oct 1999 00:35:05 +0200 wenzelm accomodate markup commands;
Tue, 05 Oct 1999 21:18:13 +0200 wenzelm strip_blanks;
Tue, 05 Oct 1999 15:33:35 +0200 wenzelm Simple LaTeX presentation primitives (based on outer lexical syntax).
less more (0) tip