src/Pure/Thy/thy_output.ML
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
2007-10-16 wenzelm 2007-10-16 tuned Const.the_abbreviation;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-09-23 wenzelm 2007-09-23 TypeInfer.constrain: canonical argument order;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections; eliminated transform_failure (to avoid critical section for main transactions);
2007-07-23 wenzelm 2007-07-23 PrintMode.with_modes;
2007-07-19 wenzelm 2007-07-19 tuned signature;
2007-07-10 wenzelm 2007-07-10 tuned;
2007-06-05 wenzelm 2007-06-05 print_antiquotations: sort_strings;
2007-01-19 wenzelm 2007-01-19 renamed Isar/isar_output.ML to Thy/thy_output.ML; tuned messages; Antiquote.scan_arguments (moved from here); moved ML context stuff to from Context to ML_Context;