src/Pure/Thy/thy_output.ML
Fri, 24 Aug 2012 12:35:39 +0200 wenzelm check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Fri, 16 Mar 2012 13:05:30 +0100 wenzelm define keywords early when processing the theory header, before running the body commands;
Fri, 16 Mar 2012 11:26:55 +0100 wenzelm clarified Keyword.is_keyword: union of minor and major;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header;
Wed, 14 Mar 2012 19:27:15 +0100 wenzelm tuned;
Wed, 14 Mar 2012 17:52:38 +0100 wenzelm source positions for locale and class expressions;
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);
Wed, 25 Jan 2012 21:10:54 +0100 wenzelm document antiquotations for ML infix operators;
Thu, 12 Jan 2012 20:57:37 +0100 wenzelm tuned;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
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 ||);
Mon, 27 Jun 2011 22:20:49 +0200 wenzelm document antiquotations are managed as theory data, with proper name space and entity markup;
Tue, 03 May 2011 22:27:32 +0200 wenzelm more conventional naming scheme: names_long, names_short, names_unique;
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Sat, 30 Apr 2011 23:20:50 +0200 wenzelm allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
Mon, 18 Apr 2011 23:41:15 +0200 wenzelm pretty_abbrev: read abbreviation more directly;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
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;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Thu, 02 Dec 2010 16:52:52 +0100 wenzelm configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
Mon, 29 Nov 2010 11:22:40 +0100 wenzelm added document antiquotation @{file};
Sun, 28 Nov 2010 21:07:28 +0100 wenzelm Parse.liberal_name for document antiquotations and attributes;
Fri, 24 Sep 2010 16:17:59 +0200 wenzelm clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
Mon, 13 Sep 2010 15:22:40 +0200 haftmann type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
Mon, 13 Sep 2010 14:55:21 +0200 haftmann merged
Mon, 13 Sep 2010 14:53:56 +0200 haftmann 'class' and 'type' are now antiquoations by default
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
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);
Fri, 03 Sep 2010 23:54:48 +0200 wenzelm turned eta_contract into proper configuration option;
Fri, 03 Sep 2010 22:57:21 +0200 wenzelm turned show_structs into proper configuration option;
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;
Thu, 02 Sep 2010 00:48:07 +0200 wenzelm turned show_question_marks into proper configuration option;
Fri, 27 Aug 2010 20:09:36 +0200 wenzelm eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
Fri, 27 Aug 2010 12:40:20 +0200 wenzelm proper context for various Thy_Output options, via official configuration options in ML and Isar;
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.);
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
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;
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;
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;
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;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Sat, 08 May 2010 19:14:13 +0200 wenzelm unified/simplified Pretty.margin_default;
Wed, 28 Apr 2010 08:25:02 +0200 haftmann term_typ: print styled term
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Fri, 16 Apr 2010 11:39:08 +0200 wenzelm proper checking of ML functors (in Poly/ML 5.2 or later);
Sat, 27 Feb 2010 20:51:51 +0100 wenzelm clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Mon, 02 Nov 2009 20:50:48 +0100 wenzelm modernized structure Proof_Syntax;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Fri, 09 Oct 2009 10:00:47 +0200 haftmann term styles also cover antiquotations term_type and typeof
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
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Tue, 24 Mar 2009 11:57:41 +0100 wenzelm datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
less more (0) -100 -60 tip