src/Pure/Thy/thy_load.ML
2012-08-22 ago discontinued separate list of required files -- maintain only provided files as they occur at runtime;
2012-08-22 ago clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-22 ago tuned;
2012-08-22 ago tuned errors;
2012-08-21 ago prefer File.full_path in accordance to check_file;
2012-08-21 ago more standard Thy_Load.check_thy for Pure.thy, relying on its header;
2012-08-21 ago refined Thy_Load.check_thy: find more uses in body text, based on keywords;
2012-08-21 ago tuned;
2012-08-20 ago more robust cleaning of "% tag" and "-- cmt";
2012-08-20 ago some support for inlining file content into outer syntax token language;
2012-03-16 ago defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
2012-03-16 ago define keywords early when processing the theory header, before running the body commands;
2012-03-15 ago some support for outer syntax keyword declarations within theory header;
2012-03-04 ago clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
2012-02-29 ago clarified module Thy_Load;
2011-08-25 ago tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
2011-08-21 ago discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
2011-08-21 ago discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;
2011-08-13 ago simplified Toplevel.init_theory: discontinued special master argument;
2011-08-10 ago future_job: explicit indication of interrupts;
2011-07-08 ago moved Outer_Syntax.load_thy to Thy_Load.load_thy;
2011-07-08 ago more abstract Thy_Load.load_file/use_file for external theory resources;
2011-07-08 ago clarified Thy_Load.digest_file -- read ML files only once;
2011-03-20 ago replaced File.check by specific File.check_file, File.check_dir;
2011-03-20 ago tuned;
2011-03-13 ago files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
2011-03-13 ago 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-03-03 ago discontinued legacy load path;
2011-01-14 ago Thy_Load.begin_theory: maintain source specification of imports;
2010-12-29 ago theory loader: implicit load path is considered legacy;
2010-12-29 ago check_file: secondary load path is legacy feature;
2010-11-27 ago prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
2010-11-27 ago moved file identification to thy_load.ML (where it is actually used);
2010-11-19 ago do not export Thy_Load.required, to avoid confusion about the interface;
2010-08-26 ago renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-03 ago simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
2010-07-27 ago simplified Thy_Header.read -- include Source.of_string_limited here;
2010-07-27 ago 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;
2010-07-25 ago Thy_Load.check_loaded via Theory.at_end;
2010-07-24 ago moved basic thy file name operations from Thy_Load to Thy_Header;
2010-07-24 ago moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
2010-07-22 ago tuned message;
2010-07-22 ago discontinued special treatment of ML files -- no longer complete extensions on demand;
2010-07-22 ago eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
2010-07-22 ago tuned signature;
2010-07-21 ago replaced Source.of_list_limited by slightly more economic Source.of_string_limited;
2010-07-21 ago deps_thy/load_thy: store compact text to reduce space by factor 12;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2009-10-27 ago tuned;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-10-01 ago eliminated redundant parameters;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-09-01 ago modernized Thy_Header;
2009-01-16 ago export check_name;
2009-01-09 ago added split_thy_path;
2008-05-14 ago renamed Position.path to Path.position;
2008-04-10 ago eliminated backpatching of load_thy;
2008-03-28 ago reorganized signature of ML_Context;
2007-08-08 ago simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
2007-07-29 ago load_thy: avoid reloading of text;