src/Pure/System/isabelle_process.ML
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;
Tue, 29 Dec 2009 20:30:40 +0100 wenzelm removed slightly odd Isar_Document.init;
Thu, 17 Dec 2009 15:09:07 +0100 wenzelm simplified message format: chunks with explicit size in bytes;
Tue, 27 Oct 2009 13:34:37 +0100 wenzelm non-critical output -- ship message in one piece;
Wed, 30 Sep 2009 23:16:15 +0200 wenzelm actually perform Isar_Document.init on startup;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 25 Jun 2009 13:25:35 +0200 wenzelm renamed IsabelleProcess to Isabelle_Process;
Tue, 02 Jun 2009 23:30:45 +0200 wenzelm IsabelleProcess: emit status "ready" after initialization and reports;
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);
less more (0) tip