src/Pure/Tools/build.ML
21 months ago wenzelm 2017-10-16 provide theory timing information, similar to command timing but always considered relevant;
21 months ago 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;
2016-03-15 wenzelm 2016-03-15 ML save_state under control of Isabelle/Scala;
2016-03-12 wenzelm 2016-03-12 clarified session build options: already provided by ML_Process; tuned signature;
2016-02-29 wenzelm 2016-02-29 redundant -- already part of Session.finish;
2016-02-29 wenzelm 2016-02-29 save heap more directly;
2015-10-10 wenzelm 2015-10-10 more explicit HTML.symbols; tuned signature;
2015-10-09 wenzelm 2015-10-09 output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-01-25 wenzelm 2015-01-25 discontinued obsolete option "document_graph";
2015-01-25 wenzelm 2015-01-25 provide session_graph.pdf via Isabelle/Scala;
2015-01-15 wenzelm 2015-01-15 more informative build_theories_result: cumulative Runtime.exn_message;
2015-01-15 wenzelm 2015-01-15 tuned;
2015-01-14 wenzelm 2015-01-14 clarified build_theories: proper protocol handler;
2015-01-14 wenzelm 2015-01-14 clarified build_theories;
2015-01-13 wenzelm 2015-01-13 some support for PIDE batch session; clarified Thy_Info.use_thys_options and corresponding protocol command;
2014-12-22 wenzelm 2014-12-22 system option "pretty_margin" is superseded by "thy_output_margin";
2014-12-18 wenzelm 2014-12-18 suppress irrelevant timing messages (the majority);
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-10-31 wenzelm 2014-10-31 discontinued pointless option: timing is always on (overall theory only);
2014-04-22 wenzelm 2014-04-22 tuned;
2014-04-17 wenzelm 2014-04-17 tuned comments;
2014-04-17 wenzelm 2014-04-17 tuned;
2014-04-17 wenzelm 2014-04-17 tuned;
2014-04-11 wenzelm 2014-04-11 explicit 'document_files' in session ROOT specifications; clarified Isabelle_System.copy_file(_base): preserve file-attributes and local directory hierarchy;
2014-04-10 wenzelm 2014-04-10 removed obsolete doc_dump option (see also 892061142ba6);
2014-02-13 wenzelm 2014-02-13 explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
2014-02-10 wenzelm 2014-02-10 seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
2013-12-11 wenzelm 2013-12-11 support for polml-5.5.2; support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890); clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;
2013-11-16 wenzelm 2013-11-16 prefer explicit "document" flag -- eliminated stateful Present.no_document;
2013-08-26 wenzelm 2013-08-26 added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;