src/Pure/Tools/build.ML
2017-04-21 ago eliminated default_qualifier: just a constant;
2017-04-19 ago more position information;
2017-04-13 ago clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
2017-04-10 ago proper import qualifier for global theories;
2017-04-08 ago more qualifier treatment, but in the end it is still ignored;
2017-04-08 ago provide Resources.import_name in ML, similar to Scala version;
2017-04-08 ago more session_base information in ML;
2017-04-07 ago provide session base for "isabelle build" and "isabelle console" ML process;
2017-03-19 ago eliminated somewhat redundant inlined name (despite a7aa17a1f721);
2017-03-18 ago more realistic PIDE build session;
2017-03-18 ago more explicit build_session args;
2017-03-18 ago avoid compiler warning;
2017-02-27 ago absent timing information means zero, according to 0070053570c4, f235646b1b73;
2016-12-18 ago dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);
2016-10-19 ago added system option "profiling";
2016-09-08 ago option "checkpoint" helps to fine-tune global heap space management;
2016-04-09 ago shared output primitives of physical/virtual Pure;
2016-04-09 ago tuned signature;
2016-04-06 ago clarified bootstrap;
2016-04-02 ago prefer infix operations;
2016-04-01 ago less bulky timing information, e.g. HOL 56913 ~> 672;
2016-03-26 ago obsolete -- done in Isabelle_Process.init_options;
2016-03-26 ago clarified use of options;
2016-03-26 ago tuned signature;
2016-03-18 ago clarified modules;
2016-03-15 ago ML save_state under control of Isabelle/Scala;
2016-03-12 ago clarified session build options: already provided by ML_Process;
2016-02-29 ago redundant -- already part of Session.finish;
2016-02-29 ago save heap more directly;
2015-10-10 ago more explicit HTML.symbols;
2015-10-09 ago output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-01-25 ago discontinued obsolete option "document_graph";
2015-01-25 ago provide session_graph.pdf via Isabelle/Scala;
2015-01-15 ago more informative build_theories_result: cumulative Runtime.exn_message;
2015-01-15 ago tuned;
2015-01-14 ago clarified build_theories: proper protocol handler;
2015-01-14 ago clarified build_theories;
2015-01-13 ago some support for PIDE batch session;
2014-12-22 ago system option "pretty_margin" is superseded by "thy_output_margin";
2014-12-18 ago suppress irrelevant timing messages (the majority);
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-10-31 ago discontinued pointless option: timing is always on (overall theory only);
2014-04-22 ago tuned;
2014-04-17 ago tuned comments;
2014-04-17 ago tuned;
2014-04-17 ago tuned;
2014-04-11 ago explicit 'document_files' in session ROOT specifications;
2014-04-10 ago removed obsolete doc_dump option (see also 892061142ba6);
2014-02-13 ago explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
2014-02-10 ago seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
2013-12-11 ago support for polml-5.5.2;
2013-11-16 ago prefer explicit "document" flag -- eliminated stateful Present.no_document;
2013-08-26 ago added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
2013-08-02 ago tuned signature;
2013-07-19 ago just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
2013-06-30 ago discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
2013-06-30 ago backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
2013-06-27 ago manage option "proofs" within theory context -- with minor overhead for primitive inferences;
2013-05-21 ago proper options;