src/Pure/Thy/thy_output.ML
Fri, 20 Mar 2009 20:21:38 +0100 wenzelm Antiquote.read: argument for reporting text;
Thu, 19 Mar 2009 16:56:51 +0100 wenzelm parameterized datatype antiquote and read operation;
Thu, 19 Mar 2009 15:44:14 +0100 wenzelm Antiquote.Text: keep full position information;
Thu, 19 Mar 2009 15:22:53 +0100 wenzelm OuterLex.read_antiq;
Wed, 18 Mar 2009 21:55:38 +0100 wenzelm de-camelized Symbol_Pos;
Fri, 13 Mar 2009 21:25:15 +0100 wenzelm eliminated type Args.T;
Mon, 09 Mar 2009 21:26:13 +0100 wenzelm simplified presentation_context_of;
Mon, 09 Mar 2009 20:34:11 +0100 wenzelm moved @{ML_functor} and @{ML_text} to Pure;
Mon, 09 Mar 2009 17:53:53 +0100 wenzelm simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
Mon, 09 Mar 2009 11:56:34 +0100 wenzelm refined antiquotation interface: formally pass result context and (potential) result source;
Sun, 08 Mar 2009 21:12:37 +0100 wenzelm added (raw_)antiquotation -- simplified wrapper for defining output commands;
Sun, 08 Mar 2009 20:31:54 +0100 wenzelm simplified presentation: pass state directly;
Fri, 06 Mar 2009 21:49:58 +0100 wenzelm improved error handling for document antiquotations;
Tue, 03 Mar 2009 12:12:38 +0100 wenzelm ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Thu, 15 Jan 2009 12:55:38 +0000 Christian Urban exported break reference
Tue, 21 Oct 2008 15:01:16 +0200 wenzelm ThyOutput: export some auxiliary operations;
Tue, 30 Sep 2008 14:19:28 +0200 wenzelm turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
Wed, 17 Sep 2008 21:27:38 +0200 wenzelm simplified ML_Context.eval_in -- expect immutable Proof.context value;
Fri, 15 Aug 2008 17:03:58 +0200 wenzelm report antiquotation names;
Fri, 15 Aug 2008 15:50:44 +0200 wenzelm Args.name_source(_position) for proper position information;
Thu, 14 Aug 2008 19:52:40 +0200 wenzelm antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Thu, 07 Aug 2008 19:21:43 +0200 wenzelm simplified Antiquote signature;
Thu, 07 Aug 2008 13:45:09 +0200 wenzelm Antiquote.read/read_arguments;
Wed, 06 Aug 2008 00:12:21 +0200 wenzelm adapted Antiq;
Mon, 04 Aug 2008 21:24:17 +0200 wenzelm abstract type Scan.stopper;
Mon, 14 Jul 2008 11:19:43 +0200 wenzelm ProofNode.current
Thu, 10 Jul 2008 13:37:35 +0200 wenzelm @{lemma}: allow terminal method;
Sat, 28 Jun 2008 21:21:13 +0200 wenzelm @{lemma}: 'by' keyword;
Tue, 24 Jun 2008 19:43:20 +0200 wenzelm Antiquote.Open/Close;
Wed, 18 Jun 2008 18:55:06 +0200 wenzelm moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
Mon, 26 May 2008 17:55:37 +0200 haftmann proper lemma [source] antiquotation
Wed, 14 May 2008 20:30:53 +0200 wenzelm added defined_command, defined_option;
Tue, 29 Apr 2008 19:55:02 +0200 haftmann added lemma antiquotation
Thu, 17 Apr 2008 22:22:19 +0200 wenzelm pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
Fri, 28 Mar 2008 00:02:54 +0100 wenzelm reorganized signature of ML_Context;
Mon, 24 Mar 2008 23:34:24 +0100 wenzelm ML runtime compilation: pass position, tuned signature;
Sun, 11 Nov 2007 20:29:07 +0100 wenzelm abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
Sat, 10 Nov 2007 14:31:23 +0100 wenzelm @{const}: improved ProofContext.read_const does the job;
Tue, 30 Oct 2007 14:39:37 +0100 haftmann const antiquotation clarified
Tue, 16 Oct 2007 17:06:20 +0200 wenzelm tuned Const.the_abbreviation;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Sun, 23 Sep 2007 22:23:27 +0200 wenzelm TypeInfer.constrain: canonical argument order;
Mon, 23 Jul 2007 19:45:49 +0200 wenzelm marked some CRITICAL sections;
Mon, 23 Jul 2007 16:45:03 +0200 wenzelm PrintMode.with_modes;
Thu, 19 Jul 2007 23:18:48 +0200 wenzelm tuned signature;
Tue, 10 Jul 2007 23:29:52 +0200 wenzelm tuned;
Tue, 05 Jun 2007 22:46:59 +0200 wenzelm print_antiquotations: sort_strings;
Fri, 19 Jan 2007 22:10:35 +0100 wenzelm renamed Isar/isar_output.ML to Thy/thy_output.ML;
less more (0) tip