| Mon, 13 Sep 2010 15:22:40 +0200 |
haftmann |
type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 14:55:21 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 14:53:56 +0200 |
haftmann |
'class' and 'type' are now antiquoations by default
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 00:31:21 +0200 |
wenzelm |
recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 23:54:48 +0200 |
wenzelm |
turned eta_contract into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 22:57:21 +0200 |
wenzelm |
turned show_structs into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 21:13:53 +0200 |
wenzelm |
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 00:48:07 +0200 |
wenzelm |
turned show_question_marks into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 20:09:36 +0200 |
wenzelm |
eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 12:40:20 +0200 |
wenzelm |
proper context for various Thy_Output options, via official configuration options in ML and Isar;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 00:09:56 +0200 |
wenzelm |
Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 21:34:19 +0200 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 19:14:13 +0200 |
wenzelm |
unified/simplified Pretty.margin_default;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 08:25:02 +0200 |
haftmann |
term_typ: print styled term
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 11:39:08 +0200 |
wenzelm |
proper checking of ML functors (in Poly/ML 5.2 or later);
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 20:51:51 +0100 |
wenzelm |
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:50:48 +0100 |
wenzelm |
modernized structure Proof_Syntax;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2009 10:00:47 +0200 |
haftmann |
term styles also cover antiquotations term_type and typeof
|
file |
diff |
annotate
|
| Wed, 07 Oct 2009 16:57:56 +0200 |
haftmann |
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 11:57:41 +0100 |
wenzelm |
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:49:47 +0100 |
wenzelm |
simplified Antiquote.read (again);
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 19:10:58 +0100 |
wenzelm |
replaced Antiquote.is_antiq by Antiquote.is_text;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 20:21:38 +0100 |
wenzelm |
Antiquote.read: argument for reporting text;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 16:56:51 +0100 |
wenzelm |
parameterized datatype antiquote and read operation;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 15:44:14 +0100 |
wenzelm |
Antiquote.Text: keep full position information;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 15:22:53 +0100 |
wenzelm |
OuterLex.read_antiq;
|
file |
diff |
annotate
|
| Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 21:26:13 +0100 |
wenzelm |
simplified presentation_context_of;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 20:34:11 +0100 |
wenzelm |
moved @{ML_functor} and @{ML_text} to Pure;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 17:53:53 +0100 |
wenzelm |
simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 11:56:34 +0100 |
wenzelm |
refined antiquotation interface: formally pass result context and (potential) result source;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 21:12:37 +0100 |
wenzelm |
added (raw_)antiquotation -- simplified wrapper for defining output commands;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 20:31:54 +0100 |
wenzelm |
simplified presentation: pass state directly;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 21:49:58 +0100 |
wenzelm |
improved error handling for document antiquotations;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 12:55:38 +0000 |
Christian Urban |
exported break reference
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 15:01:16 +0200 |
wenzelm |
ThyOutput: export some auxiliary operations;
|
file |
diff |
annotate
|
| Tue, 30 Sep 2008 14:19:28 +0200 |
wenzelm |
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:38 +0200 |
wenzelm |
simplified ML_Context.eval_in -- expect immutable Proof.context value;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2008 17:03:58 +0200 |
wenzelm |
report antiquotation names;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2008 15:50:44 +0200 |
wenzelm |
Args.name_source(_position) for proper position information;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 19:52:40 +0200 |
wenzelm |
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 19:21:43 +0200 |
wenzelm |
simplified Antiquote signature;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 13:45:09 +0200 |
wenzelm |
Antiquote.read/read_arguments;
|
file |
diff |
annotate
|