| Mon, 24 Oct 2016 12:16:12 +0200 |
wenzelm |
discontinued unused / untested distinction of separate PIDE modules;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:29:06 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:46:20 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 13:32:13 +0200 |
wenzelm |
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:07:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2014 09:24:39 +0100 |
wenzelm |
tuned -- see Text.Range.overlaps(Range);
|
file |
diff |
annotate
|
| Fri, 28 Mar 2014 21:17:47 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 20:28:19 +0100 |
wenzelm |
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 13:00:40 +0100 |
wenzelm |
more frugal merge of markup trees: non-overlapping tree counts as empty;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 12:11:32 +0100 |
wenzelm |
more frugal merge of markup trees: filter wrt. subsequent query;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 11:19:31 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 10:43:43 +0100 |
wenzelm |
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 12:07:26 +0100 |
wenzelm |
tuned signature -- more explicit Document.Elements;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 16:14:35 +0100 |
wenzelm |
eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
|
file |
diff |
annotate
|