src/Pure/Tools/build.ML
2 months ago wenzelm 2020-05-24 asynchronous build_session: notably for Scala.fulfill protocol commands during run;
2 months ago wenzelm 2020-05-24 clarified build_session protocol;
2 months ago wenzelm 2020-05-24 clarified signature;
2 months ago wenzelm 2020-05-24 more robust: explicit check for PIDE session;
2 months ago wenzelm 2020-05-24 tuned signature;
4 months ago wenzelm 2020-04-03 tuned signature;
4 months ago wenzelm 2020-04-02 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
4 months ago wenzelm 2020-04-02 clarified signature: more direct Isabelle_Process.EXIT;
4 months ago wenzelm 2020-03-30 more accurate treatment of errors;
4 months ago wenzelm 2020-03-29 tuned signature -- follow Scala;
4 months ago wenzelm 2020-03-29 clarified protocol messages: explicitly use physical_writeln, always encode_lines;
4 months ago wenzelm 2020-03-29 tuned;
4 months ago wenzelm 2020-03-28 tuned;
4 months ago wenzelm 2020-03-28 eliminated pointless flag (see also 6533ceee4cd7);
9 months ago wenzelm 2019-11-02 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
9 months ago wenzelm 2019-10-19 proper protocol_message for bootstrap proofs;
11 months ago wenzelm 2019-09-16 find theories via session directories only -- ignore known_theories;
11 months ago wenzelm 2019-09-12 find theory files via session structure: much faster Prover IDE startup;
18 months ago wenzelm 2019-01-30 discontinued obsolete option "checkpoint";
2018-06-26 wenzelm 2018-06-26 tuned signature;
2018-05-20 wenzelm 2018-05-20 tuned;
2018-05-16 wenzelm 2018-05-16 avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);
2018-05-14 wenzelm 2018-05-14 clarified signature: more explicit type "context" with full options;
2018-05-11 wenzelm 2018-05-11 more scalable -- avoid huge lines within stdout;
2018-05-05 wenzelm 2018-05-05 protocol message for export of theory resources;
2018-01-23 wenzelm 2018-01-23 treat sessions as entities with defining position; tuned signature;
2018-01-19 wenzelm 2018-01-19 formal treatment of documentation names;
2017-12-29 wenzelm 2017-12-29 formal check of @{cite} bibtex entries -- only in batch-mode session builds;
2017-12-16 wenzelm 2017-12-16 added document antiquotation @{session name}; renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
2017-10-16 wenzelm 2017-10-16 provide theory timing information, similar to command timing but always considered relevant;
2017-09-28 wenzelm 2017-09-28 session-qualified theory names are mandatory;
2017-06-09 wenzelm 2017-06-09 avoid markup, for the sake of Build_Log.Log_File.parse_props;
2017-05-27 wenzelm 2017-05-27 clarified build errors; tuned signature;
2017-05-26 wenzelm 2017-05-26 tuned;
2017-05-26 wenzelm 2017-05-26 store errors in build db;
2017-04-21 wenzelm 2017-04-21 eliminated default_qualifier: just a constant;
2017-04-19 wenzelm 2017-04-19 more position information;
2017-04-13 wenzelm 2017-04-13 clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
2017-04-10 wenzelm 2017-04-10 proper import qualifier for global theories; clarified uniqueness;
2017-04-08 wenzelm 2017-04-08 more qualifier treatment, but in the end it is still ignored;
2017-04-08 wenzelm 2017-04-08 provide Resources.import_name in ML, similar to Scala version; reset default_qualifier for now; tuned;
2017-04-08 wenzelm 2017-04-08 more session_base information in ML; tuned signature;
2017-04-07 wenzelm 2017-04-07 provide session base for "isabelle build" and "isabelle console" ML process;
2017-03-19 wenzelm 2017-03-19 eliminated somewhat redundant inlined name (despite a7aa17a1f721);
2017-03-18 wenzelm 2017-03-18 more realistic PIDE build session;
2017-03-18 wenzelm 2017-03-18 more explicit build_session args; support both command-line and PIDE version;
2017-03-18 wenzelm 2017-03-18 avoid compiler warning;
2017-02-27 wenzelm 2017-02-27 absent timing information means zero, according to 0070053570c4, f235646b1b73;
2016-12-18 wenzelm 2016-12-18 dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);
2016-10-19 wenzelm 2016-10-19 added system option "profiling";
2016-09-08 wenzelm 2016-09-08 option "checkpoint" helps to fine-tune global heap space management;
2016-04-09 wenzelm 2016-04-09 shared output primitives of physical/virtual Pure;
2016-04-09 wenzelm 2016-04-09 tuned signature;
2016-04-06 wenzelm 2016-04-06 clarified bootstrap;
2016-04-02 wenzelm 2016-04-02 prefer infix operations;
2016-04-01 wenzelm 2016-04-01 less bulky timing information, e.g. HOL 56913 ~> 672;
2016-03-26 wenzelm 2016-03-26 obsolete -- done in Isabelle_Process.init_options;
2016-03-26 wenzelm 2016-03-26 clarified use of options;
2016-03-26 wenzelm 2016-03-26 tuned signature;
2016-03-18 wenzelm 2016-03-18 clarified modules;