src/Pure/Isar/isar_cmd.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-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 renamed Standard_Syntax to Syntax_Phases;
2011-04-05 wenzelm 2011-04-05 moved decode/parse operations to standard_syntax.ML; tuned;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
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-01-06 ballarin 2011-01-06 Diagnostic command to show locale dependencies.
2010-11-28 wenzelm 2010-11-28 added 'syntax_declaration' command;
2010-11-27 wenzelm 2010-11-27 more explicit Isabelle_System operations;
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-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-09-06 wenzelm 2010-09-06 discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.;
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-08-30 wenzelm 2010-08-30 tuned;
2010-08-11 wenzelm 2010-08-11 prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
2010-08-03 wenzelm 2010-08-03 eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;
2010-07-31 ballarin 2010-07-31 print_interps shows interpretations in proofs.
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-25 wenzelm 2010-07-25 simplified handling of theory begin/end wrt. toplevel and theory loader;
2010-07-25 wenzelm 2010-07-25 Thy_Load.check_loaded via Theory.at_end;
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 thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
2010-07-21 wenzelm 2010-07-21 thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;
2010-06-03 wenzelm 2010-06-03 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
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-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-25 wenzelm 2010-04-25 replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
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-03-22 wenzelm 2010-03-22 added Specification.axiom convenience;
2010-03-21 wenzelm 2010-03-21 minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-02-16 wenzelm 2010-02-16 simplified meaning of ProofContext.verbose; eliminated strange ProofContext.setmp_verbose_CRITICAL; less confusing printing of (cumulative) unnamed facts;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-08 wenzelm 2009-11-08 print_theorems: suppress concealed (global) facts, unless "!" option is given;
2009-11-05 wenzelm 2009-11-05 allow "pervasive" local theory declarations, which are applied the background theory;
2009-11-02 wenzelm 2009-11-02 structure Thm_Deps;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Syntax;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-10-28 wenzelm 2009-10-28 renamed Proof.flat_goal to Proof.simple_goal;
2009-10-27 wenzelm 2009-10-27 ProofContext.setmp_verbose_CRITICAL;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-02 wenzelm 2009-10-02 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-09-29 ballarin 2009-09-29 Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-19 wenzelm 2009-07-19 parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-06-27 wenzelm 2009-06-27 tune File.isabelle_tool signature;
2009-03-30 wenzelm 2009-03-30 tuned;
2009-03-30 wenzelm 2009-03-30 added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);
2009-03-18 wenzelm 2009-03-18 more precise type Symbol_Pos.text;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-15 wenzelm 2009-03-15 ML_Syntax.make_binding;