| Fri, 16 Oct 2015 10:11:20 +0200 |
wenzelm |
clarified Antiquote.antiq_reports;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 21:16:00 +0200 |
wenzelm |
more direct HTML presentation, without print mode;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 16:41:20 +0200 |
wenzelm |
option editor_output_state;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 14:56:55 +0200 |
wenzelm |
separate panel for proof state output;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 20:55:46 +0200 |
wenzelm |
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 15:00:03 +0200 |
wenzelm |
more explicit bootstrap_thy;
|
file |
diff |
annotate
|
| Wed, 15 Apr 2015 14:54:25 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:23:36 +0200 |
wenzelm |
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 11:25:54 +0200 |
wenzelm |
recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 11:39:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2015 12:58:49 +0100 |
wenzelm |
simplified Command.resolve_files in ML, using blobs_index from Scala;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2015 22:00:51 +0100 |
wenzelm |
clarified markup for embedded files, early before execution;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 17:07:49 +0100 |
wenzelm |
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 13:50:53 +0100 |
wenzelm |
ensure that running into older execution is interruptible (see also b91dc7ab3464);
|
file |
diff |
annotate
|
| Sun, 11 Jan 2015 13:12:47 +0100 |
wenzelm |
do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
|
file |
diff |
annotate
|