| Mon, 10 Sep 2012 13:19:56 +0200 |
wenzelm |
formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 12:35:39 +0200 |
wenzelm |
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 13:05:30 +0100 |
wenzelm |
define keywords early when processing the theory header, before running the body commands;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 11:26:55 +0100 |
wenzelm |
clarified Keyword.is_keyword: union of minor and major;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 19:02:34 +0100 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 19:27:15 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 17:52:38 +0100 |
wenzelm |
source positions for locale and class expressions;
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 16:02:14 +0100 |
wenzelm |
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
|
file |
diff |
annotate
|
| Wed, 25 Jan 2012 21:10:54 +0100 |
wenzelm |
document antiquotations for ML infix operators;
|
file |
diff |
annotate
|
| Thu, 12 Jan 2012 20:57:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Tue, 03 May 2011 22:27:32 +0200 |
wenzelm |
more conventional naming scheme: names_long, names_short, names_unique;
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Sat, 30 Apr 2011 23:20:50 +0200 |
wenzelm |
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 23:41:15 +0200 |
wenzelm |
pretty_abbrev: read abbreviation more directly;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 16:52:52 +0100 |
wenzelm |
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 11:22:40 +0100 |
wenzelm |
added document antiquotation @{file};
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 21:07:28 +0100 |
wenzelm |
Parse.liberal_name for document antiquotations and attributes;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 16:17:59 +0200 |
wenzelm |
clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
| 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
|
| Wed, 06 Aug 2008 00:12:21 +0200 |
wenzelm |
adapted Antiq;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 21:24:17 +0200 |
wenzelm |
abstract type Scan.stopper;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 11:19:43 +0200 |
wenzelm |
ProofNode.current
|
file |
diff |
annotate
|
| Thu, 10 Jul 2008 13:37:35 +0200 |
wenzelm |
@{lemma}: allow terminal method;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 21:21:13 +0200 |
wenzelm |
@{lemma}: 'by' keyword;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:20 +0200 |
wenzelm |
Antiquote.Open/Close;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:06 +0200 |
wenzelm |
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
|
file |
diff |
annotate
|
| Mon, 26 May 2008 17:55:37 +0200 |
haftmann |
proper lemma [source] antiquotation
|
file |
diff |
annotate
|
| Wed, 14 May 2008 20:30:53 +0200 |
wenzelm |
added defined_command, defined_option;
|
file |
diff |
annotate
|
| Tue, 29 Apr 2008 19:55:02 +0200 |
haftmann |
added lemma antiquotation
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:19 +0200 |
wenzelm |
pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 00:02:54 +0100 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2008 23:34:24 +0100 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 20:29:07 +0100 |
wenzelm |
abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 14:31:23 +0100 |
wenzelm |
@{const}: improved ProofContext.read_const does the job;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2007 14:39:37 +0100 |
haftmann |
const antiquotation clarified
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 17:06:20 +0200 |
wenzelm |
tuned Const.the_abbreviation;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 22:23:27 +0200 |
wenzelm |
TypeInfer.constrain: canonical argument order;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 19:45:49 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 16:45:03 +0200 |
wenzelm |
PrintMode.with_modes;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 23:18:48 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 23:29:52 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 22:46:59 +0200 |
wenzelm |
print_antiquotations: sort_strings;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:10:35 +0100 |
wenzelm |
renamed Isar/isar_output.ML to Thy/thy_output.ML;
|
file |
diff |
annotate
|