| Fri, 02 May 2014 20:01:45 +0200 |
wenzelm |
prefer scala.Console with its support for thread-local redirection;
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 21:29:36 +0200 |
wenzelm |
clarified exit sequence: prover is reset afterwards, no more output messages;
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 14:50:40 +0200 |
wenzelm |
clarified;
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 12:27:18 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2014 16:47:47 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2014 15:02:13 +0200 |
wenzelm |
clarified command_input: Consumer_Thread;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2014 13:54:45 +0200 |
wenzelm |
eliminated pointless output actors;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2014 14:52:23 +0200 |
wenzelm |
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 19:26:39 +0200 |
wenzelm |
recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 14:54:17 +0200 |
wenzelm |
more general prover operations;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 13:46:18 +0200 |
wenzelm |
more general prover operations;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 14:36:17 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Sat, 16 Nov 2013 12:29:10 +0100 |
wenzelm |
more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;
|
file |
diff |
annotate
|
| Fri, 15 Nov 2013 19:31:10 +0100 |
wenzelm |
more specific Protocol_Output: empty message.body, main content via bytes/text;
|
file |
diff |
annotate
|
| Thu, 14 Nov 2013 17:17:57 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 12:53:24 +0200 |
wenzelm |
tuned signature -- facilitate experimentation with other processes;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 19:53:06 +0200 |
wenzelm |
tuned -- more uniform ML vs. Scala;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 22:04:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 21:54:43 +0200 |
wenzelm |
no need for raw stdin;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 20:34:15 +0200 |
wenzelm |
public Isabelle_Process.xml_cache (thread-safe);
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 20:27:27 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 20:17:04 +0100 |
wenzelm |
explicit module UTF8;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 15:28:58 +0100 |
wenzelm |
update options via protocol;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 20:17:30 +0200 |
wenzelm |
more direct message header: eliminated historic encoding via single letter;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2012 17:07:25 +0200 |
wenzelm |
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 12:35:24 +0200 |
wenzelm |
tuned signature -- slightly more abstract text representation of prover process;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2012 20:49:17 +0200 |
wenzelm |
support for detached Bash_Job with some control operations;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2012 20:02:44 +0200 |
wenzelm |
support external processes with explicit environment;
|
file |
diff |
annotate
|
| Tue, 29 May 2012 21:48:05 +0200 |
wenzelm |
clarified prover startup: no timeout, read stderr more carefully;
|
file |
diff |
annotate
|
| Tue, 29 May 2012 21:03:11 +0200 |
wenzelm |
need to close_input before expecting threads to terminate/join;
|
file |
diff |
annotate
|
| Tue, 29 May 2012 18:00:54 +0200 |
wenzelm |
more explicit treatment of return code vs. session phase;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 18:18:39 +0100 |
wenzelm |
clarified terminology of raw protocol messages;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 17:46:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 17:30:14 +0100 |
wenzelm |
tuned signature -- emphasize Isabelle_Process Input vs. Output;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 11:31:12 +0100 |
wenzelm |
clarified scope of exception handlers;
|
file |
diff |
annotate
|
| Fri, 02 Mar 2012 22:34:42 +0100 |
wenzelm |
terminate after first exception -- avoid syslog flooding;
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 15:36:48 +0100 |
wenzelm |
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 14:15:37 +0100 |
wenzelm |
prefer raw_message for protocol implementation;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 14:29:14 +0100 |
wenzelm |
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
|
file |
diff |
annotate
|
| Tue, 29 Nov 2011 20:18:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| 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.;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2011 11:24:22 +0200 |
wenzelm |
always use sockets on Windows/Cygwin;
|
file |
diff |
annotate
|
| Sun, 25 Sep 2011 13:48:59 +0200 |
wenzelm |
more uniform defaults;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2011 13:44:31 +0200 |
wenzelm |
explicit option for socket vs. fifo communication;
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 20:35:50 +0200 |
wenzelm |
more abstract wrapping of fifos as System_Channel;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 11:00:39 +0200 |
wenzelm |
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 10:27:04 +0200 |
wenzelm |
more abstract receiver interface;
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 19:12:06 +0200 |
wenzelm |
simplified signatures;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 12 Jul 2011 19:36:46 +0200 |
wenzelm |
more uniform Properties in ML and Scala;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 16:48:02 +0200 |
wenzelm |
JVM method invocation service via Scala layer;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 15:56:30 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 11:13:33 +0200 |
wenzelm |
some support for raw messages, which bypass standard Symbol/YXML decoding;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 10:27:50 +0200 |
wenzelm |
tuned XML.Cache parameters;
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 21:53:27 +0200 |
wenzelm |
echo prover input via raw_messages, for improved protocol tracing;
|
file |
diff |
annotate
|
| Thu, 07 Jul 2011 13:48:30 +0200 |
wenzelm |
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 22:11:32 +0200 |
wenzelm |
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 14:52:32 +0200 |
wenzelm |
explicit import java.lang.System to prevent odd scope problems;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2011 21:35:48 +0200 |
wenzelm |
lazy Isabelle_System.default supports implicit boot;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 17:49:01 +0200 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 20:34:40 +0100 |
wenzelm |
more abstract/uniform handling of time, preferring seconds as Double;
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 18:11:33 +0200 |
wenzelm |
bulk read: observe EOF protocol more carefully -- 0 counts as successful read;
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 22:00:36 +0200 |
wenzelm |
tuned messages -- cf. Admin/MacOS/App1;
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 18:44:26 +0200 |
wenzelm |
explicit Session.Phase indication with associated event bus;
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 15:21:04 +0200 |
wenzelm |
manage persistent syslog via Session, not Isabelle_Process;
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 14:39:29 +0200 |
wenzelm |
tuned prover message categorization;
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 13:28:19 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 21:21:04 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 16:04:20 +0200 |
wenzelm |
more content for Session_Dockable;
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 14:29:13 +0200 |
wenzelm |
more reactive handling of Isabelle_Process startup errors;
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 13:47:48 +0200 |
wenzelm |
main Isabelle_Process via Isabelle_System.Managed_Process;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 23:28:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 21:26:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 21:20:06 +0200 |
wenzelm |
added Isabelle_Process.syslog;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 11:38:14 +0200 |
wenzelm |
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 19 Sep 2010 20:11:51 +0200 |
wenzelm |
message_actor: more robust treatment of EOF;
|
file |
diff |
annotate
|
| Sun, 19 Sep 2010 17:12:34 +0200 |
wenzelm |
simplified Isabelle_Process message kinds;
|
file |
diff |
annotate
|
| Sat, 18 Sep 2010 21:33:56 +0200 |
wenzelm |
recovered basic session stop/restart;
|
file |
diff |
annotate
|
| Sat, 18 Sep 2010 21:10:07 +0200 |
wenzelm |
simplified fifo handling -- rm_fifo always succeeds without ever blocking;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 16:07:18 +0200 |
wenzelm |
module for simplified thread operations (Scala version);
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 13:52:24 +0200 |
wenzelm |
tuned signatures;
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 18:20:36 +0200 |
wenzelm |
XML.Cache: pipe-lined (thread-safe) version using actor;
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 17:04:22 +0200 |
wenzelm |
simplified internal message format: dropped special Symbol.STX header;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 00:44:48 +0200 |
wenzelm |
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
|
file |
diff |
annotate
|
| Tue, 10 Aug 2010 15:12:45 +0200 |
wenzelm |
removed obsolete methods for (ML) commands;
|
file |
diff |
annotate
|
| Tue, 10 Aug 2010 12:29:11 +0200 |
wenzelm |
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 18:18:32 +0200 |
wenzelm |
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
|
file |
diff |
annotate
|
| Sun, 08 Aug 2010 19:36:31 +0200 |
wenzelm |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file |
diff |
annotate
|
| Sat, 07 Aug 2010 22:43:57 +0200 |
wenzelm |
simplified some Markup;
|
file |
diff |
annotate
|
| Sat, 07 Aug 2010 22:09:52 +0200 |
wenzelm |
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 22:26:20 +0200 |
wenzelm |
specific ML_val vs. ML_command;
|
file |
diff |
annotate
|
| Sun, 04 Jul 2010 00:05:32 +0200 |
wenzelm |
simplified Isabelle_Process.Result: use markup directly;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 12:35:40 +0200 |
wenzelm |
indicate prospective properties;
|
file |
diff |
annotate
|
| Tue, 25 May 2010 23:03:13 +0200 |
wenzelm |
eliminated obsolete priority message from Isabelle_Process protocol;
|
file |
diff |
annotate
|
| Fri, 21 May 2010 20:10:45 +0200 |
wenzelm |
simplified message markup, using plain XML.Elem directly;
|
file |
diff |
annotate
|
| Fri, 21 May 2010 14:53:19 +0200 |
wenzelm |
more abstract view on prover output messages;
|
file |
diff |
annotate
|
| Fri, 07 May 2010 22:00:23 +0200 |
wenzelm |
output symbolic pretty printing markup and format in the front end;
|
file |
diff |
annotate
|
| Thu, 31 Dec 2009 00:35:54 +0100 |
wenzelm |
added is_ready;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 22:56:46 +0100 |
wenzelm |
simplified init message -- removed redundant session property;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 22:29:37 +0100 |
wenzelm |
removed obsolete version check -- sanity delegated to Isabelle_System;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2009 22:03:14 +0100 |
wenzelm |
separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
|
file |
diff |
annotate
|
| Fri, 18 Dec 2009 11:44:25 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 23:44:15 +0100 |
wenzelm |
Result.cache;
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 20:14:00 +0100 |
wenzelm |
fifo: raw byte stream;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 21:03:04 +0200 |
wenzelm |
Isabelle_Process: receiver as Actor, not EventBus;
|
file |
diff |
annotate
|
| Sat, 29 Aug 2009 10:50:04 +0200 |
wenzelm |
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2009 13:25:35 +0200 |
wenzelm |
renamed IsabelleProcess to Isabelle_Process;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2009 20:15:29 +0200 |
wenzelm |
static IsabelleSystem.charset;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 18:00:20 +0100 |
wenzelm |
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
|
file |
diff |
annotate
| base
|