src/Pure/Thy/thy_load.ML
2014-03-10 wenzelm 2014-03-10 some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
2014-03-03 wenzelm 2014-03-03 tuned messages and markup;
2014-02-27 wenzelm 2014-02-27 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;
2014-02-24 wenzelm 2014-02-24 tuned signature;
2014-02-19 wenzelm 2014-02-19 prefer guarded Context_Position.report where feasible;
2013-12-09 wenzelm 2013-12-09 provide @{file_unchecked} in Isabelle/Pure;
2013-11-20 wenzelm 2013-11-20 load files that are not provided by PIDE blobs; uniform resolve_files via Command.read;
2013-11-20 wenzelm 2013-11-20 tuned;
2013-11-19 wenzelm 2013-11-19 more uniform handling of inlined files;
2013-11-19 wenzelm 2013-11-19 release file errors at runtime: Command.eval instead of Command.read;
2013-11-19 wenzelm 2013-11-19 maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;
2013-11-16 wenzelm 2013-11-16 prefer explicit "document" flag -- eliminated stateful Present.no_document;
2013-11-16 wenzelm 2013-11-16 simplified HTML theory presentation;
2013-11-16 wenzelm 2013-11-16 removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
2013-11-16 wenzelm 2013-11-16 tuned;
2013-11-16 wenzelm 2013-11-16 tuned signature;
2013-11-16 wenzelm 2013-11-16 tuned signature -- clarified Proof General legacy;
2013-11-16 wenzelm 2013-11-16 toplevel function "use" refers to raw ML bootstrap environment;
2013-11-16 wenzelm 2013-11-16 obsolete;
2013-11-16 wenzelm 2013-11-16 tuned signature;
2013-09-04 wenzelm 2013-09-04 some explicit indication of Proof General legacy;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-28 wenzelm 2013-07-28 breakable @{file};
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-03-27 wenzelm 2013-03-27 more liberal handling of skipped proofs;
2013-03-13 wenzelm 2013-03-13 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;
2013-03-04 wenzelm 2013-03-04 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones; refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;
2013-03-04 wenzelm 2013-03-04 join all proofs before scheduling present phase (ordered according to weight); tuned;
2013-03-03 wenzelm 2013-03-03 prefer more systematic Future.flat;
2013-03-03 wenzelm 2013-03-03 clarified Toplevel.element_result wrt. Toplevel.is_ignored;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2013-02-25 wenzelm 2013-02-25 clarified Toplevel.element_result: scheduling policies happen here; tuned;
2013-02-24 wenzelm 2013-02-24 simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored; eliminated separate Outer_Syntax.read_element;
2013-02-20 wenzelm 2013-02-20 more tight representation of command timing; tuned signatures; tuned;
2013-02-19 wenzelm 2013-02-19 support for prescient timing information within command transactions;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-10 wenzelm 2012-09-10 formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-26 wenzelm 2012-08-26 more accurate defining position of theory;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-24 wenzelm 2012-08-24 report source path and let front-end resolve implicit master location (e.g. URL);
2012-08-24 wenzelm 2012-08-24 some markup for inlined files;
2012-08-23 wenzelm 2012-08-23 tuned signature;
2012-08-23 wenzelm 2012-08-23 clarified type Token.file;
2012-08-23 wenzelm 2012-08-23 simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
2012-08-23 wenzelm 2012-08-23 tuned signature;
2012-08-23 wenzelm 2012-08-23 simplified Thy_Load.provide: do not store full path;
2012-08-22 wenzelm 2012-08-22 tuned;
2012-08-22 wenzelm 2012-08-22 tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
2012-08-22 wenzelm 2012-08-22 discontinued separate list of required files -- maintain only provided files as they occur at runtime; tuned signature;
2012-08-22 wenzelm 2012-08-22 clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-22 wenzelm 2012-08-22 tuned;
2012-08-22 wenzelm 2012-08-22 tuned errors;
2012-08-21 wenzelm 2012-08-21 prefer File.full_path in accordance to check_file;
2012-08-21 wenzelm 2012-08-21 more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;
2012-08-21 wenzelm 2012-08-21 refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;
2012-08-21 wenzelm 2012-08-21 tuned;