src/Pure/System/isabelle_process.scala
Thu, 01 Dec 2011 14:29:14 +0100 wenzelm clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
Tue, 29 Nov 2011 20:18:02 +0100 wenzelm clarified modules;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Fri, 25 Nov 2011 18:37:14 +0100 wenzelm retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
Mon, 17 Oct 2011 11:24:22 +0200 wenzelm always use sockets on Windows/Cygwin;
Sun, 25 Sep 2011 13:48:59 +0200 wenzelm more uniform defaults;
Fri, 23 Sep 2011 13:44:31 +0200 wenzelm explicit option for socket vs. fifo communication;
Wed, 21 Sep 2011 20:35:50 +0200 wenzelm more abstract wrapping of fifos as System_Channel;
Wed, 07 Sep 2011 11:00:39 +0200 wenzelm added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
Tue, 06 Sep 2011 11:18:19 +0200 wenzelm buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
Tue, 06 Sep 2011 10:27:04 +0200 wenzelm more abstract receiver interface;
Sun, 04 Sep 2011 19:12:06 +0200 wenzelm simplified signatures;
Sun, 04 Sep 2011 14:29:15 +0200 wenzelm pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
Tue, 12 Jul 2011 19:36:46 +0200 wenzelm more uniform Properties in ML and Scala;
Mon, 11 Jul 2011 16:48:02 +0200 wenzelm JVM method invocation service via Scala layer;
Mon, 11 Jul 2011 15:56:30 +0200 wenzelm tuned signature;
Mon, 11 Jul 2011 11:13:33 +0200 wenzelm some support for raw messages, which bypass standard Symbol/YXML decoding;
Mon, 11 Jul 2011 10:27:50 +0200 wenzelm tuned XML.Cache parameters;
Sat, 09 Jul 2011 21:53:27 +0200 wenzelm echo prover input via raw_messages, for improved protocol tracing;
Thu, 07 Jul 2011 13:48:30 +0200 wenzelm simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
Mon, 04 Jul 2011 22:11:32 +0200 wenzelm quasi-static Isabelle_System -- reduced tendency towards "functorial style";
Thu, 23 Jun 2011 14:52:32 +0200 wenzelm explicit import java.lang.System to prevent odd scope problems;
Wed, 22 Jun 2011 21:35:48 +0200 wenzelm lazy Isabelle_System.default supports implicit boot;
Wed, 08 Jun 2011 17:49:01 +0200 wenzelm updated headers;
Wed, 01 Dec 2010 20:34:40 +0100 wenzelm more abstract/uniform handling of time, preferring seconds as Double;
Mon, 27 Sep 2010 18:11:33 +0200 wenzelm bulk read: observe EOF protocol more carefully -- 0 counts as successful read;
Thu, 23 Sep 2010 22:00:36 +0200 wenzelm tuned messages -- cf. Admin/MacOS/App1;
Thu, 23 Sep 2010 18:44:26 +0200 wenzelm explicit Session.Phase indication with associated event bus;
Thu, 23 Sep 2010 15:21:04 +0200 wenzelm manage persistent syslog via Session, not Isabelle_Process;
Thu, 23 Sep 2010 14:39:29 +0200 wenzelm tuned prover message categorization;
Thu, 23 Sep 2010 13:28:19 +0200 wenzelm tuned message;
Wed, 22 Sep 2010 21:21:04 +0200 wenzelm tuned message;
Wed, 22 Sep 2010 16:04:20 +0200 wenzelm more content for Session_Dockable;
Wed, 22 Sep 2010 14:29:13 +0200 wenzelm more reactive handling of Isabelle_Process startup errors;
Wed, 22 Sep 2010 13:47:48 +0200 wenzelm main Isabelle_Process via Isabelle_System.Managed_Process;
Mon, 20 Sep 2010 23:28:35 +0200 wenzelm tuned;
Mon, 20 Sep 2010 21:26:58 +0200 wenzelm tuned;
Mon, 20 Sep 2010 21:20:06 +0200 wenzelm added Isabelle_Process.syslog;
Mon, 20 Sep 2010 11:38:14 +0200 wenzelm Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
Sun, 19 Sep 2010 22:40:22 +0200 wenzelm refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
Sun, 19 Sep 2010 20:11:51 +0200 wenzelm message_actor: more robust treatment of EOF;
Sun, 19 Sep 2010 17:12:34 +0200 wenzelm simplified Isabelle_Process message kinds;
Sat, 18 Sep 2010 21:33:56 +0200 wenzelm recovered basic session stop/restart;
Sat, 18 Sep 2010 21:10:07 +0200 wenzelm simplified fifo handling -- rm_fifo always succeeds without ever blocking;
Sat, 18 Sep 2010 17:14:47 +0200 wenzelm slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;
Fri, 17 Sep 2010 22:17:57 +0200 wenzelm 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);
Fri, 17 Sep 2010 15:51:11 +0200 wenzelm eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
Mon, 23 Aug 2010 16:07:18 +0200 wenzelm module for simplified thread operations (Scala version);
Sun, 22 Aug 2010 13:52:24 +0200 wenzelm tuned signatures;
Mon, 16 Aug 2010 18:20:36 +0200 wenzelm XML.Cache: pipe-lined (thread-safe) version using actor;
Mon, 16 Aug 2010 17:04:22 +0200 wenzelm simplified internal message format: dropped special Symbol.STX header;
Fri, 13 Aug 2010 21:33:13 +0200 wenzelm 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);
Wed, 11 Aug 2010 00:44:48 +0200 wenzelm native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
Tue, 10 Aug 2010 15:12:45 +0200 wenzelm removed obsolete methods for (ML) commands;
Tue, 10 Aug 2010 12:29:11 +0200 wenzelm distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
Mon, 09 Aug 2010 18:18:32 +0200 wenzelm Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
Sun, 08 Aug 2010 19:36:31 +0200 wenzelm explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
Sat, 07 Aug 2010 22:43:57 +0200 wenzelm simplified some Markup;
Sat, 07 Aug 2010 22:09:52 +0200 wenzelm simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
Mon, 05 Jul 2010 22:26:20 +0200 wenzelm specific ML_val vs. ML_command;
less more (0) -60 tip