src/Pure/Isar/isar_syn.ML
2011-04-03 wenzelm 2011-04-03 added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-01-16 wenzelm 2011-01-16 added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2011-01-13 wenzelm 2011-01-13 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2011-01-06 ballarin 2011-01-06 Diagnostic command to show locale dependencies.
2010-12-18 ballarin 2010-12-18 Add mixins to sublocale command.
2010-12-17 wenzelm 2010-12-17 Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-05 wenzelm 2010-12-05 command 'notepad' replaces former 'example_proof';
2010-12-04 wenzelm 2010-12-04 formal notepad without any result;
2010-11-28 wenzelm 2010-11-28 added 'syntax_declaration' command;
2010-11-07 wenzelm 2010-11-07 'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
2010-11-06 wenzelm 2010-11-06 mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
2010-09-08 haftmann 2010-09-08 removed ancient constdefs command
2010-09-06 wenzelm 2010-09-06 discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.;
2010-08-31 wenzelm 2010-08-31 moved Toplevel.run_command to Pure/PIDE/document.ML; eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL; tuned signatures;
2010-08-30 wenzelm 2010-08-30 tuned;
2010-08-25 wenzelm 2010-08-25 discontinued obsolete 'global' and 'local' commands;
2010-08-11 haftmann 2010-08-11 more convenient split of class modules: class and class_declaration
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-08-11 haftmann 2010-08-11 moved instantiation target formally to class_target.ML
2010-08-11 haftmann 2010-08-11 moved overloading target formally to overloading.ML
2010-07-31 ballarin 2010-07-31 Interpretation in proofs supports mixins.
2010-07-28 wenzelm 2010-07-28 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
2010-07-27 wenzelm 2010-07-27 theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
2010-07-27 wenzelm 2010-07-27 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps; explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database; Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command; added Thy_Load.begin_theory for clarity; structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader; moved some basic commands from isar_cmd.ML to isar_syn.ML; misc tuning and simplification;
2010-07-24 wenzelm 2010-07-24 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;
2010-07-21 wenzelm 2010-07-21 eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing; misc tuning and simplification;
2010-07-20 wenzelm 2010-07-20 warning in proper transaction context;
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-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 renamed structure ValueParse to Parse_Value; eliminated old-style structure alias V;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-05-12 wenzelm 2010-05-12 updated/unified some legacy warnings;
2010-04-29 wenzelm 2010-04-29 ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-04-28 wenzelm 2010-04-28 localized default sort;
2010-04-28 wenzelm 2010-04-28 modernized/simplified Sign.set_defsort;
2010-04-26 wenzelm 2010-04-26 command 'example_proof' opens an empty proof body;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-04-23 wenzelm 2010-04-23 explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-16 wenzelm 2010-04-16 keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-16 wenzelm 2010-04-16 modernized old-style type abbreviations;
2010-04-16 wenzelm 2010-04-16 local type abbreviations;
2010-04-11 haftmann 2010-04-11 user interface for abstract datatypes is an attribute, not a command
2010-03-21 wenzelm 2010-03-21 minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-18 wenzelm 2010-03-18 typedecl: no sort constraints;
2010-03-09 wenzelm 2010-03-09 localized typedecl;
2010-03-07 wenzelm 2010-03-07 separate structure Typedecl;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-01 wenzelm 2010-03-01 added type_notation command;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-23 haftmann 2010-02-23 dropped axclass
2010-02-19 haftmann 2010-02-19 added code_abstype keyword
2010-02-18 wenzelm 2010-02-18 removed unused Theory_Target.begin; Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb; renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern; tuned;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;