src/Pure/Thy/thy_load.ML
2013-12-09 ago provide @{file_unchecked} in Isabelle/Pure;
2013-11-20 ago load files that are not provided by PIDE blobs;
2013-11-20 ago tuned;
2013-11-19 ago more uniform handling of inlined files;
2013-11-19 ago release file errors at runtime: Command.eval instead of Command.read;
2013-11-19 ago maintain blobs within document state: digest + text in ML, digest-only in Scala;
2013-11-16 ago prefer explicit "document" flag -- eliminated stateful Present.no_document;
2013-11-16 ago simplified HTML theory presentation;
2013-11-16 ago removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
2013-11-16 ago tuned;
2013-11-16 ago tuned signature;
2013-11-16 ago tuned signature -- clarified Proof General legacy;
2013-11-16 ago toplevel function "use" refers to raw ML bootstrap environment;
2013-11-16 ago obsolete;
2013-11-16 ago tuned signature;
2013-09-04 ago some explicit indication of Proof General legacy;
2013-08-23 ago added Theory.setup convenience;
2013-07-30 ago type theory is purely value-oriented;
2013-07-28 ago breakable @{file};
2013-07-05 ago tuned signature;
2013-07-03 ago tuned signature;
2013-03-27 ago more liberal handling of skipped proofs;
2013-03-13 ago clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
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;