src/Pure/Thy/thy_load.ML
2013-03-04 ago refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
2013-03-04 ago join all proofs before scheduling present phase (ordered according to weight);
2013-03-03 ago prefer more systematic Future.flat;
2013-03-03 ago clarified Toplevel.element_result wrt. Toplevel.is_ignored;
2013-02-27 ago discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 ago discontinued obsolete 'uses' within theory header;
2013-02-25 ago clarified Toplevel.element_result: scheduling policies happen here;
2013-02-24 ago simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
2013-02-20 ago more tight representation of command timing;
2013-02-19 ago support for prescient timing information within command transactions;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-10 ago formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
2012-08-29 ago renamed Position.str_of to Position.here;
2012-08-26 ago more accurate defining position of theory;
2012-08-26 ago theory def/ref position reports, which enable hyperlinks etc.;
2012-08-24 ago report source path and let front-end resolve implicit master location (e.g. URL);
2012-08-24 ago some markup for inlined files;
2012-08-23 ago tuned signature;
2012-08-23 ago clarified type Token.file;
2012-08-23 ago simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
2012-08-23 ago tuned signature;
2012-08-23 ago simplified Thy_Load.provide: do not store full path;
2012-08-22 ago tuned;
2012-08-22 ago tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
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;