src/Pure/Thy/thy_output.ML
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-12-02 wenzelm 2010-12-02 configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-11-29 wenzelm 2010-11-29 added document antiquotation @{file};
2010-11-28 wenzelm 2010-11-28 Parse.liberal_name for document antiquotations and attributes;
2010-09-24 wenzelm 2010-09-24 clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees; tuned;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-09-13 haftmann 2010-09-13 type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
2010-09-13 haftmann 2010-09-13 merged
2010-09-13 haftmann 2010-09-13 'class' and 'type' are now antiquoations by default
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-04 wenzelm 2010-09-04 recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);
2010-09-03 wenzelm 2010-09-03 turned eta_contract into proper configuration option;
2010-09-03 wenzelm 2010-09-03 turned show_structs into proper configuration option;
2010-09-03 wenzelm 2010-09-03 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;
2010-09-02 wenzelm 2010-09-02 turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;
2010-08-27 wenzelm 2010-08-27 eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
2010-08-27 wenzelm 2010-08-27 proper context for various Thy_Output options, via official configuration options in ML and Isar;
2010-08-27 wenzelm 2010-08-27 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-30 wenzelm 2010-05-30 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-04-28 haftmann 2010-04-28 term_typ: print styled term
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-04-16 wenzelm 2010-04-16 proper checking of ML functors (in Poly/ML 5.2 or later); eliminated pathetic comments;
2010-02-27 wenzelm 2010-02-27 clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Syntax;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-09 haftmann 2009-10-09 term styles also cover antiquotations term_type and typeof
2009-10-07 haftmann 2009-10-07 generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-03-24 wenzelm 2009-03-24 datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
2009-03-22 wenzelm 2009-03-22 simplified Antiquote.read (again);
2009-03-22 wenzelm 2009-03-22 replaced Antiquote.is_antiq by Antiquote.is_text;
2009-03-20 wenzelm 2009-03-20 Antiquote.read: argument for reporting text;
2009-03-19 wenzelm 2009-03-19 parameterized datatype antiquote and read operation;
2009-03-19 wenzelm 2009-03-19 Antiquote.Text: keep full position information;
2009-03-19 wenzelm 2009-03-19 OuterLex.read_antiq;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-09 wenzelm 2009-03-09 simplified presentation_context_of;
2009-03-09 wenzelm 2009-03-09 moved @{ML_functor} and @{ML_text} to Pure; adapted to simplified ThyOutput.antiquotation interface; misc tuning;
2009-03-09 wenzelm 2009-03-09 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output; removed incomprehensible args parser setup; removed obsolete locale flag -- text is already localized; misc tuning and cleanup of concrete antiquotations; goal state antiquotations: ignore source flag;
2009-03-09 wenzelm 2009-03-09 refined antiquotation interface: formally pass result context and (potential) result source; removed redundant raw_antiquotation;
2009-03-08 wenzelm 2009-03-08 added (raw_)antiquotation -- simplified wrapper for defining output commands;
2009-03-08 wenzelm 2009-03-08 simplified presentation: pass state directly;
2009-03-06 wenzelm 2009-03-06 improved error handling for document antiquotations;
2009-03-03 wenzelm 2009-03-03 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;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-15 Christian Urban 2009-01-15 exported break reference
2008-10-21 wenzelm 2008-10-21 ThyOutput: export some auxiliary operations;