| Wed, 11 Dec 2013 18:02:22 +0100 |
wenzelm |
support for polml-5.5.2;
|
file |
diff |
annotate
|
| Fri, 22 Nov 2013 21:13:44 +0100 |
wenzelm |
clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 11:55:52 +0100 |
wenzelm |
load files that are not provided by PIDE blobs;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 19:33:27 +0100 |
wenzelm |
maintain blobs within document state: digest + text in ML, digest-only in Scala;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 20:32:26 +0200 |
wenzelm |
maintain goal forks as part of global execution;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 11:18:36 +0200 |
wenzelm |
cancel_query via direct access to the exec_id of the running query process;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 15:29:10 +0200 |
wenzelm |
tuned signature -- more uniform treatment of overlays as command mapping;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 14:26:09 +0200 |
wenzelm |
maintain overlays within node perspective;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 12:14:13 +0200 |
wenzelm |
allow explicit indication of required node: full eval, no prints;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 11:54:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 18:59:58 +0200 |
wenzelm |
keep memo_exec execution running, which is important to cancel goal forks eventually;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 16:52:04 +0200 |
wenzelm |
maintain explicit execution frontier: avoid conflict with former task via static dependency;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 14:18:57 +0200 |
wenzelm |
actually purge removed goal futures -- avoid memory leak;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 13:00:36 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Mon, 15 Jul 2013 10:25:35 +0200 |
wenzelm |
more careful termination of removed execs, leaving running execs undisturbed;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 12:04:16 +0200 |
wenzelm |
clarified execution: maintain running execs only, check "stable" separately via memo (again);
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 11:28:03 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 11:07:02 +0200 |
wenzelm |
clarified module name;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 23:24:40 +0200 |
wenzelm |
more explicit type Exec.context;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 18:41:05 +0200 |
wenzelm |
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 16:35:37 +0200 |
wenzelm |
tuned -- cleanup before publishing assignment;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 14:42:11 +0200 |
wenzelm |
global management of command execution fragments;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 23:30:10 +0200 |
wenzelm |
added "echo" command for demonstration purposes;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 21:13:32 +0200 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 12:33:28 +0200 |
wenzelm |
tuned start_execution: avoid sleep on worker thread;
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 13:17:22 +0200 |
wenzelm |
tuned protocol terminology;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 15:38:03 +0200 |
wenzelm |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2013 23:51:47 +0200 |
wenzelm |
separate exec_id assignment for Command.print states, without affecting result of eval;
|
file |
diff |
annotate
|
| Wed, 22 May 2013 14:10:45 +0200 |
wenzelm |
explicit management of Session.Protocol_Handlers, with protocol state and functions;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 16:27:44 +0100 |
wenzelm |
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
|
file |
diff |
annotate
|