src/Pure/Thy/thy_output.ML
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;