2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-04 wenzelm 2013-01-04 prefer old graph browser in Isabelle/jEdit, which still produces better layout; clarified print mode "active_graph": allow to switch "browser" vs. "graphview" uniformly; tuned signature;
2013-01-03 wenzelm 2013-01-03 always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
2012-12-13 wenzelm 2012-12-13 smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-12-13 wenzelm 2012-12-13 enable Isabelle/ML to produce uninterpreted result messages as well;
2012-12-10 wenzelm 2012-12-10 more generous tracing limit -- rescaled in MB;
2012-11-29 wenzelm 2012-11-29 more uniform ML statistics;
2012-11-28 wenzelm 2012-11-28 some support for ML runtime statistics;
2012-11-28 wenzelm 2012-11-28 prefer tight Markup.print_int/parse_int for property values;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-18 wenzelm 2012-11-18 more generous tracing_limit, with explicit system option;
2012-11-18 wenzelm 2012-11-18 update options via protocol; jEdit dialog for "Parallel Checking" options;
2012-10-01 wenzelm 2012-10-01 more direct message header: eliminated historic encoding via single letter;
2012-09-29 wenzelm 2012-09-29 enable show_markup by default (approx. double output size);
2012-09-28 wenzelm 2012-09-28 smarter handling of tracing messages;
2012-09-25 wenzelm 2012-09-25 basic integration of graphview into document model; added Graph_Dockable; updated Isabelle/jEdit authors and dependencies etc.;
2012-09-04 wenzelm 2012-09-04 enable parallel terminal proofs in interaction;
2012-08-07 wenzelm 2012-08-07 simplified process startup phases: INIT suffices for is_ready;
2012-08-07 wenzelm 2012-08-07 prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
2012-08-07 wenzelm 2012-08-07 prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol; just one cumulative Keyword.status at end of batch session;
2012-06-01 wenzelm 2012-06-01 tuned message;
2012-04-09 wenzelm 2012-04-09 disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;
2012-04-07 wenzelm 2012-04-07 enable parallel proofs (cf. e8552cba702d), only affects packages so far; disable quick_and_dirty to make packages produce proofs -- NB: 'sorry' works via "int" mode of proof commands;
2012-03-03 wenzelm 2012-03-03 clarified terminology of raw protocol messages;
2012-02-20 wenzelm 2012-02-20 clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
2012-01-05 wenzelm 2012-01-05 prefer raw_message for protocol implementation;
2012-01-05 wenzelm 2012-01-05 tuned signature -- emphasize special nature of protocol commands;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-10-17 wenzelm 2011-10-17 always use sockets on Windows/Cygwin; discontinued special raw_dump facility;
2011-09-23 wenzelm 2011-09-23 default print mode for Isabelle/Scala, not just Isabelle/jEdit;
2011-09-22 wenzelm 2011-09-22 abstract System_Channel in ML (cf. Scala version); back to TextIO for fifo, which is more stable in Poly/ML 5.4.x; explicit block buffering -- BinIO might be subject to old Poly/ML defaults;
2011-09-21 wenzelm 2011-09-21 alternative Socket_Channel; use BinIO for fifos uniformly;
2011-09-19 wenzelm 2011-09-19 at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;
2011-09-06 wenzelm 2011-09-06 flush after Output.raw_message (and init message) for reduced latency of important protocol events;
2011-08-23 wenzelm 2011-08-23 tuned signature -- contrast physical output primitives versus Output.raw_message;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;
2011-07-12 wenzelm 2011-07-12 clarified YXML.embed_controls -- this is idempotent and cannot be nested;
2011-07-12 wenzelm 2011-07-12 allow empty body for raw_message -- important for Invoke_Scala;
2011-07-11 wenzelm 2011-07-11 some support for raw messages, which bypass standard Symbol/YXML decoding; tuned signature;
2011-07-06 wenzelm 2011-07-06 prefer Synchronized.var;
2011-07-05 wenzelm 2011-07-05 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
2011-07-05 wenzelm 2011-07-05 hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
2011-05-20 wenzelm 2011-05-20 added Isabelle_Process.is_active; tuned signature;
2010-11-13 wenzelm 2010-11-13 back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
2010-11-12 wenzelm 2010-11-12 defensive defaults for more robust experience for new users;
2010-11-02 wenzelm 2010-11-02 simplified some time constants;
2010-10-25 wenzelm 2010-10-25 explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt; eliminated auto_flush threads -- use plain line buffering for stdout/stderr; tuned;
2010-10-25 wenzelm 2010-10-25 more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-27 wenzelm 2010-09-27 renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
2010-09-23 wenzelm 2010-09-23 manage persistent syslog via Session, not Isabelle_Process; tuned;
2010-09-22 wenzelm 2010-09-22 more content for Session_Dockable;
2010-09-22 wenzelm 2010-09-22 main Isabelle_Process via Isabelle_System.Managed_Process; simplified init message: no pid; misc tuning and simplification;
2010-09-20 wenzelm 2010-09-20 Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
2010-09-19 wenzelm 2010-09-19 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop; tuned;
2010-09-17 wenzelm 2010-09-17 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
2010-09-17 wenzelm 2010-09-17 Isabelle_Process: status/report do not require serial numbers;
2010-09-09 wenzelm 2010-09-09 main command loops are supposed to be uninterruptible -- no special treatment here;
2010-08-30 wenzelm 2010-08-30 message serial number indicates physical order;
2010-08-16 wenzelm 2010-08-16 simplified internal message format: dropped special Symbol.STX header;