src/Pure/System/session.ML
2013-05-22 ago explicit management of Session.Protocol_Handlers, with protocol state and functions;
2013-05-20 ago even later Options.reset_default -- still needed for printing errors of Session.finish (e.g. via Command_Line.tool0);
2013-05-20 ago reset options last -- other parts of the system may still need them;
2013-05-17 ago discontinued obsolete isabelle usedir, mkdir, make;
2013-05-17 ago event timer as separate service thread;
2013-05-12 ago load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
2013-03-13 ago clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
2013-03-12 ago discontinued "isabelle usedir" option -r (reset session path);
2013-03-11 ago discontinued "isabelle usedir" option -P (remote path);
2013-02-25 ago more explicit Goal.shutdown_futures;
2013-01-24 ago more efficient inlined properties, especially relevant for voluminous tasks trace;
2013-01-09 ago standardized treatment of timing properties;
2013-01-08 ago include timing properties in log;
2013-01-03 ago maintain session index on Scala side, for more determistic results;
2012-12-07 ago make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
2012-11-18 ago isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
2012-10-18 ago more basic Goal.reset_futures as snapshot of implicit state;
2012-10-18 ago collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
2012-10-17 ago another Future.shutdown after Future.cancel_groups (cf. 0d4106850eb2);
2012-10-17 ago more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;
2012-09-10 ago more explicit indication of legacy features;
2012-08-28 ago discontinued centralistic changelog;
2012-08-14 ago explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
2012-08-14 ago more direct interpretation of document_variants for build (unchanged for usedir);
2012-08-07 ago prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
2012-08-06 ago pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
2012-08-02 ago more official command specifications, including source position;
2012-07-27 ago prefer explicit datatype Present.dump_mode;
2012-07-27 ago simplified Session.name;
2012-07-26 ago proper arguments for old usedir;
2012-07-26 ago refined "document_dump_mode": "all", "tex+sty", "tex";
2012-07-24 ago more precise propagation of options: build, session, theories;
2012-07-24 ago pass build options to ML;
2012-07-23 ago pass ISABELLE_BROWSER_INFO as explicit argument;
2012-07-21 ago some actual build function on ML side;
2012-03-16 ago check declared vs. defined commands at end of session;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-08-23 ago tuned signature -- contrast physical output primitives versus Output.raw_message;
2011-03-30 ago session timing: show pseudo-speedup factor;
2011-03-20 ago structure Timing: covers former start_timing/end_timing and Output.timeit etc;
2011-03-20 ago tuned terminology for document variants;
2011-02-04 ago parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
2010-09-27 ago renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
2010-09-22 ago renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-15 ago renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-19 ago parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-06-30 ago more detailed timing message;
2009-06-17 ago usedir: internal timing option;
2009-06-06 ago ML_Compiler.exn_message;
2009-02-28 ago moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);