src/Pure/pure_setup.ML
2010-08-17 wenzelm 2010-08-17 discontinued support for Poly/ML 5.0 and 5.1 versions;
2010-08-11 wenzelm 2010-08-11 more precise and more maintainable dependencies;
2010-07-25 wenzelm 2010-07-25 simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; eliminated obsolete touch_child_thys, register_theory;
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 discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
2010-07-20 wenzelm 2010-07-20 SML/NJ: refrain from modifying toplevel pp for type string -- unclear if it could work here;
2010-07-20 wenzelm 2010-07-20 toplevel pp for Proof.state and Toplevel.state;
2010-06-24 wenzelm 2010-06-24 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
2010-06-24 wenzelm 2010-06-24 treat Pretty.T as strictly abstract type;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2009-11-28 wenzelm 2009-11-28 workaround for strange compiler crash of Poly/ML 5.0 and 5.1 at this point http://isabelle.in.tum.de/repos/isabelle/file/a2fc533175ff/src/HOL/Tools/Nitpick/nitpick_nut.ML#l997
2009-11-09 wenzelm 2009-11-09 setup for official Poly/ML 5.3.0, which is now the default;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-10-20 wenzelm 2009-10-20 fixed SML/NJ toplevel pp; tuned;
2009-06-15 wenzelm 2009-06-15 override toplevel "use" functions last;
2009-06-04 wenzelm 2009-06-04 less experimental polyml-5.3;
2009-03-21 wenzelm 2009-03-21 replaced install_pp/make_pp by more general toplevel_pp based on use_text;
2009-03-21 wenzelm 2009-03-21 Pretty.position; try use ml_system specific install_pp;
2009-03-20 wenzelm 2009-03-20 uniform ml_prompts for RAW and Pure;
2009-03-10 wenzelm 2009-03-10 quote binding for ML toplevel pp;
2009-03-03 wenzelm 2009-03-03 Binding.str_of;
2009-01-23 haftmann 2009-01-23 making SMLNJ happy
2008-12-29 haftmann 2008-12-29 pretty printer for bindings
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue;
2008-10-09 wenzelm 2008-10-09 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
2008-09-29 wenzelm 2008-09-29 install_pp Future.T (polyml only);
2008-09-09 wenzelm 2008-09-09 human-readable printing of TaskQueue.task/group;
2008-08-07 wenzelm 2008-08-07 install_pp Position.T;
2008-06-24 wenzelm 2008-06-24 added pprint_thy_ref;
2008-05-18 wenzelm 2008-05-18 eliminated theory CPure;
2008-04-10 wenzelm 2008-04-10 val theory = ThyInfo.get_theory;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-27 wenzelm 2008-03-27 implicit setup of emerging theory Pure;
2007-10-29 wenzelm 2007-10-29 qualified Proofterm.proofs;
2007-10-11 wenzelm 2007-10-11 renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-08-13 wenzelm 2007-08-13 moved appl syntax to PureThy;
2007-08-07 wenzelm 2007-08-07 theory loader: removed obsolete update_thy (coincides with use_thy);
2007-07-29 wenzelm 2007-07-29 added ML toplevel use commands: Toplevel.program; added install_pp stuff;
2007-07-17 wenzelm 2007-07-17 Pure theory setup.