| Wed, 06 Jul 2011 20:46:06 +0200 |
prefer Synchronized.var;
|
file | diff | annotate |
| Tue, 05 Jul 2011 22:39:15 +0200 |
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
|
file | diff | annotate |
| Tue, 05 Jul 2011 21:53:59 +0200 |
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
|
file | diff | annotate |
| Fri, 20 May 2011 20:44:03 +0200 |
added Isabelle_Process.is_active;
|
file | diff | annotate |
| Sat, 13 Nov 2010 12:32:21 +0100 |
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
|
file | diff | annotate |
| Fri, 12 Nov 2010 21:37:01 +0100 |
defensive defaults for more robust experience for new users;
|
file | diff | annotate |
| Tue, 02 Nov 2010 20:55:12 +0100 |
simplified some time constants;
|
file | diff | annotate |
| Mon, 25 Oct 2010 22:47:02 +0200 |
explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
|
file | diff | annotate |
| Mon, 25 Oct 2010 21:23:09 +0200 |
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
|
file | diff | annotate |
| Mon, 25 Oct 2010 21:06:56 +0200 |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file | diff | annotate |
| Mon, 27 Sep 2010 20:26:10 +0200 |
renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
|
file | diff | annotate |
| Thu, 23 Sep 2010 15:21:04 +0200 |
manage persistent syslog via Session, not Isabelle_Process;
|
file | diff | annotate |
| Wed, 22 Sep 2010 16:04:20 +0200 |
more content for Session_Dockable;
|
file | diff | annotate |
| Wed, 22 Sep 2010 13:47:48 +0200 |
main Isabelle_Process via Isabelle_System.Managed_Process;
|
file | diff | annotate |
| Mon, 20 Sep 2010 11:38:14 +0200 |
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
|
file | diff | annotate |
| Sun, 19 Sep 2010 22:40:22 +0200 |
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 |
| Fri, 17 Sep 2010 22:17:57 +0200 |
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 20:56:32 +0200 |
Isabelle_Process: status/report do not require serial numbers;
|
file | diff | annotate |
| Thu, 09 Sep 2010 18:00:16 +0200 |
main command loops are supposed to be uninterruptible -- no special treatment here;
|
file | diff | annotate |
| Mon, 30 Aug 2010 11:35:17 +0200 |
message serial number indicates physical order;
|
file | diff | annotate |
| Mon, 16 Aug 2010 17:04:22 +0200 |
simplified internal message format: dropped special Symbol.STX header;
|
file | diff | annotate |
| Wed, 11 Aug 2010 00:44:48 +0200 |
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
|
file | diff | annotate |
| Tue, 10 Aug 2010 20:13:52 +0200 |
renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;
|
file | diff | annotate |
| Tue, 10 Aug 2010 12:29:11 +0200 |
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
|
file | diff | annotate |
| Mon, 09 Aug 2010 22:02:26 +0200 |
auto_flush: higher frequency;
|
file | diff | annotate |
| Mon, 09 Aug 2010 21:23:24 +0200 |
more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
|
file | diff | annotate |
| Mon, 09 Aug 2010 18:18:32 +0200 |
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
|
file | diff | annotate |
| Sun, 08 Aug 2010 19:36:31 +0200 |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file | diff | annotate |
| Sat, 07 Aug 2010 21:03:06 +0200 |
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
|
file | diff | annotate |
| Sat, 03 Jul 2010 22:33:10 +0200 |
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
|
file | diff | annotate |
| Mon, 31 May 2010 21:06:57 +0200 |
modernized some structure names, keeping a few legacy aliases;
|
file | diff | annotate |
| Sun, 30 May 2010 13:47:12 +0200 |
Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;
|
file | diff | annotate |
| Sat, 29 May 2010 19:46:29 +0200 |
explicit markup for forked goals, as indicated by Goal.fork;
|
file | diff | annotate |
| Tue, 25 May 2010 23:03:13 +0200 |
eliminated obsolete priority message from Isabelle_Process protocol;
|
file | diff | annotate |
| Sat, 15 May 2010 23:16:32 +0200 |
refer directly to structure Keyword and Parse;
|
file | diff | annotate |
| Fri, 07 May 2010 22:00:23 +0200 |
output symbolic pretty printing markup and format in the front end;
|
file | diff | annotate |
| Mon, 04 Jan 2010 19:43:59 +0100 |
report keywords as singleton messages, control message kind via print mode;
|
file | diff | annotate |
| Wed, 30 Dec 2009 22:56:46 +0100 |
simplified init message -- removed redundant session property;
|
file | diff | annotate |
| Tue, 29 Dec 2009 20:30:40 +0100 |
removed slightly odd Isar_Document.init;
|
file | diff | annotate |
| Thu, 17 Dec 2009 15:09:07 +0100 |
simplified message format: chunks with explicit size in bytes;
|
file | diff | annotate |
| Tue, 27 Oct 2009 13:34:37 +0100 |
non-critical output -- ship message in one piece;
|
file | diff | annotate |
| Wed, 30 Sep 2009 23:16:15 +0200 |
actually perform Isar_Document.init on startup;
|
file | diff | annotate |
| Tue, 29 Sep 2009 11:49:22 +0200 |
explicit indication of Unsynchronized.ref;
|
file | diff | annotate |
| Thu, 25 Jun 2009 13:25:35 +0200 |
renamed IsabelleProcess to Isabelle_Process;
|
file | diff | annotate |
| Tue, 02 Jun 2009 23:30:45 +0200 |
IsabelleProcess: emit status "ready" after initialization and reports;
|
file | diff | annotate |
| Sat, 28 Feb 2009 18:00:20 +0100 |
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
|
file | diff | annotate | base |