src/Pure/Thy/thy_output.ML
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;
2008-09-30 wenzelm 2008-09-30 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
2008-09-17 wenzelm 2008-09-17 simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-08-15 wenzelm 2008-08-15 report antiquotation names; tuned messages;
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-14 wenzelm 2008-08-14 antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-08-07 wenzelm 2008-08-07 simplified Antiquote signature;
2008-08-07 wenzelm 2008-08-07 Antiquote.read/read_arguments;
2008-08-06 wenzelm 2008-08-06 adapted Antiq;
2008-08-04 wenzelm 2008-08-04 abstract type Scan.stopper;
2008-07-14 wenzelm 2008-07-14 ProofNode.current
2008-07-10 wenzelm 2008-07-10 @{lemma}: allow terminal method;
2008-06-28 wenzelm 2008-06-28 @{lemma}: 'by' keyword;
2008-06-24 wenzelm 2008-06-24 Antiquote.Open/Close;
2008-06-18 wenzelm 2008-06-18 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
2008-05-26 haftmann 2008-05-26 proper lemma [source] antiquotation
2008-05-14 wenzelm 2008-05-14 added defined_command, defined_option;
2008-04-29 haftmann 2008-04-29 added lemma antiquotation
2008-04-17 wenzelm 2008-04-17 pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2007-11-11 wenzelm 2007-11-11 abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
2007-11-10 wenzelm 2007-11-10 @{const}: improved ProofContext.read_const does the job;
2007-10-30 haftmann 2007-10-30 const antiquotation clarified