src/Pure/System/isabelle_process.ML
Tue, 07 Aug 2012 19:16:58 +0200 wenzelm simplified process startup phases: INIT suffices for is_ready;
Tue, 07 Aug 2012 17:08:22 +0200 wenzelm prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
Tue, 07 Aug 2012 16:34:15 +0200 wenzelm prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
Fri, 01 Jun 2012 13:02:09 +0200 wenzelm tuned message;
Mon, 09 Apr 2012 23:06:14 +0200 wenzelm disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;
Sat, 07 Apr 2012 19:59:09 +0200 wenzelm enable parallel proofs (cf. e8552cba702d), only affects packages so far;
Sat, 03 Mar 2012 18:18:39 +0100 wenzelm clarified terminology of raw protocol messages;
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;
Thu, 05 Jan 2012 14:15:37 +0100 wenzelm prefer raw_message for protocol implementation;
Thu, 05 Jan 2012 13:24:29 +0100 wenzelm tuned signature -- emphasize special nature of protocol commands;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Mon, 17 Oct 2011 11:24:22 +0200 wenzelm always use sockets on Windows/Cygwin;
Fri, 23 Sep 2011 14:13:15 +0200 wenzelm default print mode for Isabelle/Scala, not just Isabelle/jEdit;
Thu, 22 Sep 2011 20:33:08 +0200 wenzelm abstract System_Channel in ML (cf. Scala version);
Wed, 21 Sep 2011 22:18:17 +0200 wenzelm alternative Socket_Channel;
Mon, 19 Sep 2011 16:40:17 +0200 wenzelm at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;
Tue, 06 Sep 2011 10:16:12 +0200 wenzelm flush after Output.raw_message (and init message) for reduced latency of important protocol events;
Tue, 23 Aug 2011 16:53:05 +0200 wenzelm tuned signature -- contrast physical output primitives versus Output.raw_message;
Thu, 18 Aug 2011 17:53:32 +0200 wenzelm more careful treatment of exception serial numbers, with propagation to message channel;
Tue, 12 Jul 2011 13:45:05 +0200 wenzelm clarified YXML.embed_controls -- this is idempotent and cannot be nested;
Tue, 12 Jul 2011 13:39:29 +0200 wenzelm allow empty body for raw_message -- important for Invoke_Scala;
Mon, 11 Jul 2011 11:13:33 +0200 wenzelm some support for raw messages, which bypass standard Symbol/YXML decoding;
Wed, 06 Jul 2011 20:46:06 +0200 wenzelm prefer Synchronized.var;
Tue, 05 Jul 2011 22:39:15 +0200 wenzelm Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
Tue, 05 Jul 2011 21:53:59 +0200 wenzelm hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
Fri, 20 May 2011 20:44:03 +0200 wenzelm added Isabelle_Process.is_active;
Sat, 13 Nov 2010 12:32:21 +0100 wenzelm back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
Fri, 12 Nov 2010 21:37:01 +0100 wenzelm defensive defaults for more robust experience for new users;
Tue, 02 Nov 2010 20:55:12 +0100 wenzelm simplified some time constants;
Mon, 25 Oct 2010 22:47:02 +0200 wenzelm explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
Mon, 25 Oct 2010 21:23:09 +0200 wenzelm more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Mon, 27 Sep 2010 20:26:10 +0200 wenzelm renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
Thu, 23 Sep 2010 15:21:04 +0200 wenzelm manage persistent syslog via Session, not Isabelle_Process;
Wed, 22 Sep 2010 16:04:20 +0200 wenzelm more content for Session_Dockable;
Wed, 22 Sep 2010 13:47:48 +0200 wenzelm main Isabelle_Process via Isabelle_System.Managed_Process;
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;
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 20:56:32 +0200 wenzelm Isabelle_Process: status/report do not require serial numbers;
Thu, 09 Sep 2010 18:00:16 +0200 wenzelm main command loops are supposed to be uninterruptible -- no special treatment here;
Mon, 30 Aug 2010 11:35:17 +0200 wenzelm message serial number indicates physical order;
Mon, 16 Aug 2010 17:04:22 +0200 wenzelm simplified internal message format: dropped special Symbol.STX header;
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 20:13:52 +0200 wenzelm renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;
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 22:02:26 +0200 wenzelm auto_flush: higher frequency;
Mon, 09 Aug 2010 21:23:24 +0200 wenzelm more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
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 21:03:06 +0200 wenzelm simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
Sat, 03 Jul 2010 22:33:10 +0200 wenzelm Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Sun, 30 May 2010 13:47:12 +0200 wenzelm Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;
Sat, 29 May 2010 19:46:29 +0200 wenzelm explicit markup for forked goals, as indicated by Goal.fork;
Tue, 25 May 2010 23:03:13 +0200 wenzelm eliminated obsolete priority message from Isabelle_Process protocol;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Fri, 07 May 2010 22:00:23 +0200 wenzelm output symbolic pretty printing markup and format in the front end;
Mon, 04 Jan 2010 19:43:59 +0100 wenzelm report keywords as singleton messages, control message kind via print mode;
Wed, 30 Dec 2009 22:56:46 +0100 wenzelm simplified init message -- removed redundant session property;
less more (0) -60 tip