src/Pure/System/isabelle_process.ML
2013-07-08 ago more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
2013-05-22 ago explicit management of Session.Protocol_Handlers, with protocol state and functions;
2013-05-21 ago proper options;
2013-05-21 ago proper options;
2013-05-17 ago retain quick_and_dirty as-is -- no censorship;
2013-05-12 ago full default options for Isabelle_Process and Build;
2013-03-27 ago separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
2013-03-27 ago more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-13 ago clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
2013-03-04 ago refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
2013-01-22 ago more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
2013-01-16 ago more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-04 ago prefer old graph browser in Isabelle/jEdit, which still produces better layout;
2013-01-03 ago always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
2012-12-13 ago smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-12-13 ago enable Isabelle/ML to produce uninterpreted result messages as well;
2012-12-10 ago more generous tracing limit -- rescaled in MB;
2012-11-29 ago more uniform ML statistics;
2012-11-28 ago some support for ML runtime statistics;
2012-11-28 ago prefer tight Markup.print_int/parse_int for property values;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-18 ago more generous tracing_limit, with explicit system option;
2012-11-18 ago update options via protocol;
2012-10-01 ago more direct message header: eliminated historic encoding via single letter;
2012-09-29 ago enable show_markup by default (approx. double output size);
2012-09-28 ago smarter handling of tracing messages;
2012-09-25 ago basic integration of graphview into document model;
2012-09-04 ago enable parallel terminal proofs in interaction;
2012-08-07 ago simplified process startup phases: INIT suffices for is_ready;
2012-08-07 ago prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
2012-08-07 ago prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
2012-06-01 ago tuned message;
2012-04-09 ago disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;
2012-04-07 ago enable parallel proofs (cf. e8552cba702d), only affects packages so far;
2012-03-03 ago clarified terminology of raw protocol messages;
2012-02-20 ago clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
2012-01-05 ago prefer raw_message for protocol implementation;
2012-01-05 ago tuned signature -- emphasize special nature of protocol commands;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-10-17 ago always use sockets on Windows/Cygwin;
2011-09-23 ago default print mode for Isabelle/Scala, not just Isabelle/jEdit;
2011-09-22 ago abstract System_Channel in ML (cf. Scala version);
2011-09-21 ago alternative Socket_Channel;
2011-09-19 ago at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;
2011-09-06 ago flush after Output.raw_message (and init message) for reduced latency of important protocol events;
2011-08-23 ago tuned signature -- contrast physical output primitives versus Output.raw_message;
2011-08-18 ago more careful treatment of exception serial numbers, with propagation to message channel;
2011-07-12 ago clarified YXML.embed_controls -- this is idempotent and cannot be nested;
2011-07-12 ago allow empty body for raw_message -- important for Invoke_Scala;
2011-07-11 ago some support for raw messages, which bypass standard Symbol/YXML decoding;
2011-07-06 ago prefer Synchronized.var;
2011-07-05 ago Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
2011-07-05 ago hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
2011-05-20 ago added Isabelle_Process.is_active;
2010-11-13 ago back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
2010-11-12 ago defensive defaults for more robust experience for new users;
2010-11-02 ago simplified some time constants;
2010-10-25 ago explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
2010-10-25 ago more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
2010-10-25 ago renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;