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;
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;
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;
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;
2012-08-20 wenzelm 2012-08-20 more robust cleaning of "% tag" and "-- cmt";
2012-08-20 wenzelm 2012-08-20 some support for inlining file content into outer syntax token language;
2012-03-16 wenzelm 2012-03-16 defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
2012-03-16 wenzelm 2012-03-16 define keywords early when processing the theory header, before running the body commands;
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;