| Fri, 02 Aug 2013 14:26:09 +0200 |
wenzelm |
maintain overlays within node perspective;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 12:39:45 +0200 |
wenzelm |
full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 22:58:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 22:09:16 +0200 |
wenzelm |
tuned signature -- eliminated pointless type synonym;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 16:01:45 +0200 |
wenzelm |
tuned signature;
|
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
|
| Thu, 04 Jul 2013 12:02:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 16:19:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 15:11:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 19:39:31 +0100 |
wenzelm |
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 16:10:46 +0100 |
wenzelm |
structural equality for Command.Results;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2013 13:09:34 +0100 |
wenzelm |
clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 23:04:35 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:16:08 +0100 |
wenzelm |
tuned implementation according to Library.insert/merge in ML;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:09:08 +0100 |
wenzelm |
more formal class Command.Results;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 13:52:18 +0100 |
wenzelm |
identify dialogs via official serial and maintain as result message;
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 23:36:07 +0100 |
wenzelm |
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 13:21:02 +0100 |
wenzelm |
more abstract Sendback operations, with explicit id/exec_id properties;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 20:36:52 +0100 |
wenzelm |
always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 15:25:49 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 19:34:31 +0200 |
wenzelm |
operations to turn markup into XML;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 19:23:04 +0200 |
wenzelm |
accumulate under exec_id as well;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 19:16:48 +0200 |
wenzelm |
more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 16:50:44 +0200 |
wenzelm |
more realistic sendback: pick exec_id from message position and text from buffer;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 11:09:53 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2012 17:07:25 +0200 |
wenzelm |
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 17:20:40 +0200 |
wenzelm |
more explicit message markup and rendering;
|
file |
diff |
annotate
|