src/Pure/System/isabelle_process.ML
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;
2010-09-27 ago renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
2010-09-23 ago manage persistent syslog via Session, not Isabelle_Process;
2010-09-22 ago more content for Session_Dockable;
2010-09-22 ago main Isabelle_Process via Isabelle_System.Managed_Process;
2010-09-20 ago Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
2010-09-19 ago refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
2010-09-17 ago 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 ago Isabelle_Process: status/report do not require serial numbers;
2010-09-09 ago main command loops are supposed to be uninterruptible -- no special treatment here;
2010-08-30 ago message serial number indicates physical order;
2010-08-16 ago simplified internal message format: dropped special Symbol.STX header;
2010-08-11 ago native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
2010-08-10 ago renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;
2010-08-10 ago distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
2010-08-09 ago auto_flush: higher frequency;
2010-08-09 ago more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
2010-08-09 ago Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
2010-08-08 ago explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-08-07 ago simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-07-03 ago Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-30 ago Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;
2010-05-29 ago explicit markup for forked goals, as indicated by Goal.fork;
2010-05-25 ago eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-05-07 ago output symbolic pretty printing markup and format in the front end;
2010-01-04 ago report keywords as singleton messages, control message kind via print mode;
2009-12-30 ago simplified init message -- removed redundant session property;
2009-12-29 ago removed slightly odd Isar_Document.init;
2009-12-17 ago simplified message format: chunks with explicit size in bytes;
2009-10-27 ago non-critical output -- ship message in one piece;
2009-09-30 ago actually perform Isar_Document.init on startup;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-06-25 ago renamed IsabelleProcess to Isabelle_Process;