src/Pure/Thy/thy_output.ML
Fri, 03 Apr 2015 19:56:51 +0200 wenzelm more uniform "verbose" option to print name space;
Wed, 25 Mar 2015 11:39:52 +0100 wenzelm tuned signature;
Mon, 22 Dec 2014 16:44:24 +0100 wenzelm system option "pretty_margin" is superseded by "thy_output_margin";
Sun, 30 Nov 2014 14:02:48 +0100 wenzelm tuned signature;
Sun, 30 Nov 2014 13:15:04 +0100 wenzelm tuned signature;
Sun, 30 Nov 2014 12:46:16 +0100 wenzelm tuned signature -- prefer Input.source;
Sun, 30 Nov 2014 12:24:56 +0100 wenzelm more abstract type Input.source;
Thu, 13 Nov 2014 23:45:15 +0100 wenzelm uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
Wed, 12 Nov 2014 11:39:27 +0100 wenzelm make SML/NJ happy;
Tue, 11 Nov 2014 18:16:25 +0100 wenzelm more position information, e.g. relevant for errors in generated ML source;
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Thu, 06 Nov 2014 15:47:04 +0100 wenzelm more explicit Keyword.keywords;
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Sat, 01 Nov 2014 20:19:07 +0100 wenzelm clarified syntax -- avoid overlap with command category;
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Sat, 01 Nov 2014 15:01:41 +0100 wenzelm command-line terminator ";" is no longer accepted;
Tue, 21 Oct 2014 09:50:22 +0200 wenzelm clarified verbatim line breaks, e.g. relevant for Implementation mldecls;
Mon, 20 Oct 2014 16:52:36 +0200 wenzelm official support for "tt" style variants, avoid fragile \verb in LaTeX;
Thu, 28 Aug 2014 15:47:26 +0200 wenzelm more liberal embedded "text", which includes cartouches;
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Sat, 24 May 2014 12:55:09 +0200 wenzelm strip trailing white space, to avoid notorious problems of jEdit with last line;
Sat, 12 Apr 2014 17:46:54 +0200 wenzelm markup for prose words within formal comments;
Sun, 06 Apr 2014 16:36:28 +0200 wenzelm more source positions;
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Thu, 27 Mar 2014 17:56:13 +0100 wenzelm redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
Tue, 18 Mar 2014 15:29:58 +0100 wenzelm more antiquotations;
Tue, 18 Mar 2014 11:27:09 +0100 wenzelm tuned signature;
Wed, 12 Mar 2014 21:58:48 +0100 wenzelm simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
Tue, 11 Mar 2014 14:28:39 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 21:15:29 +0100 wenzelm some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
Mon, 10 Mar 2014 18:06:23 +0100 wenzelm clarified Args.check_src: retain name space information for error output;
Mon, 10 Mar 2014 16:30:07 +0100 wenzelm clarified Args.src: more abstract type, position refers to name only;
Mon, 10 Mar 2014 15:30:29 +0100 wenzelm tuned signature;
Sun, 09 Mar 2014 16:37:56 +0100 wenzelm tuned signature;
Thu, 06 Mar 2014 13:44:01 +0100 wenzelm more uniform check_const/read_const;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
Sun, 02 Mar 2014 19:00:45 +0100 wenzelm clarified names of antiquotations and markup;
Sat, 01 Mar 2014 23:17:37 +0100 wenzelm tuned signature;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Fri, 28 Feb 2014 10:50:54 +0100 wenzelm tuned errors -- in accordance to ML antiquotations;
Fri, 28 Feb 2014 10:40:04 +0100 wenzelm more explicit method reports;
Wed, 26 Feb 2014 10:40:13 +0100 wenzelm method language markup, e.g. relevant to prevent outer keyword completion;
Tue, 25 Feb 2014 14:56:58 +0100 wenzelm proper context for global data;
Tue, 25 Feb 2014 10:50:12 +0100 wenzelm more markup;
Wed, 19 Feb 2014 21:38:44 +0100 wenzelm prefer guarded Context_Position.report where feasible;
Tue, 18 Feb 2014 20:50:07 +0100 wenzelm more markup;
Tue, 18 Feb 2014 16:34:02 +0100 wenzelm generic markup for embedded languages;
Mon, 17 Feb 2014 11:14:26 +0100 wenzelm more markup;
Wed, 22 Jan 2014 16:03:11 +0100 wenzelm tuned signature;
Mon, 09 Dec 2013 12:16:52 +0100 wenzelm added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience;
Fri, 23 Aug 2013 15:36:54 +0200 wenzelm discontinued unused antiquotation blocks;
Fri, 16 Aug 2013 22:39:31 +0200 wenzelm more markup via Name_Space.check;
Thu, 16 May 2013 21:09:58 +0200 wenzelm Thy_Output.modes as proper option;
Thu, 16 May 2013 20:50:01 +0200 wenzelm some system options as context-sensitive config options;
Mon, 13 May 2013 12:40:17 +0200 wenzelm retain goal display options when printing error messages, to avoid breakdown for huge goals;
Fri, 05 Apr 2013 20:54:55 +0200 wenzelm tuned signature -- agree with markup terminology;
Fri, 05 Apr 2013 20:43:43 +0200 wenzelm unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
less more (0) -100 -60 tip