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-19 ago message_actor: more robust treatment of EOF;
2010-09-19 ago simplified Isabelle_Process message kinds;
2010-09-18 ago recovered basic session stop/restart;
2010-09-18 ago simplified fifo handling -- rm_fifo always succeeds without ever blocking;
2010-09-18 ago slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;
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 eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
2010-08-23 ago module for simplified thread operations (Scala version);
2010-08-22 ago tuned signatures;
2010-08-16 ago XML.Cache: pipe-lined (thread-safe) version using actor;
2010-08-16 ago simplified internal message format: dropped special Symbol.STX header;
2010-08-13 ago added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
2010-08-11 ago native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
2010-08-10 ago removed obsolete methods for (ML) commands;
2010-08-10 ago distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
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. (useful markup);
2010-08-07 ago simplified some Markup;
2010-08-07 ago simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
2010-07-05 ago specific ML_val vs. ML_command;
2010-07-04 ago simplified Isabelle_Process.Result: use markup directly;
2010-05-27 ago indicate prospective properties;
2010-05-25 ago eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-21 ago simplified message markup, using plain XML.Elem directly;
2010-05-21 ago more abstract view on prover output messages;
2010-05-07 ago output symbolic pretty printing markup and format in the front end;
2009-12-31 ago added is_ready;
2009-12-30 ago simplified init message -- removed redundant session property;
2009-12-30 ago removed obsolete version check -- sanity delegated to Isabelle_System;
2009-12-28 ago separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
2009-12-18 ago tuned signature;
2009-12-17 ago Result.cache;
2009-12-17 ago fifo: raw byte stream;
2009-09-01 ago Isabelle_Process: receiver as Actor, not EventBus;
2009-08-29 ago moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
2009-06-25 ago renamed IsabelleProcess to Isabelle_Process;
2009-06-07 ago static IsabelleSystem.charset;
2009-02-28 ago moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);