src/Pure/PIDE/command.scala
Fri, 09 Aug 2013 10:41:17 +0200 wenzelm retain original messages properties, e.g. for retrieval via Command.Results;
Fri, 02 Aug 2013 14:26:09 +0200 wenzelm maintain overlays within node perspective;
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);
Fri, 05 Jul 2013 22:58:24 +0200 wenzelm tuned signature;
Fri, 05 Jul 2013 22:09:16 +0200 wenzelm tuned signature -- eliminated pointless type synonym;
Fri, 05 Jul 2013 16:01:45 +0200 wenzelm tuned signature;
Fri, 05 Jul 2013 15:38:03 +0200 wenzelm explicit module Document_ID as source of globally unique identifiers across ML/Scala;
Thu, 04 Jul 2013 23:51:47 +0200 wenzelm separate exec_id assignment for Command.print states, without affecting result of eval;
Thu, 04 Jul 2013 12:02:11 +0200 wenzelm tuned;
Wed, 03 Jul 2013 16:19:57 +0200 wenzelm tuned signature;
Wed, 03 Jul 2013 15:11:15 +0200 wenzelm tuned signature;
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;
Sat, 23 Mar 2013 16:10:46 +0100 wenzelm structural equality for Command.Results;
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;
Fri, 14 Dec 2012 23:04:35 +0100 wenzelm tuned;
Fri, 14 Dec 2012 12:16:08 +0100 wenzelm tuned implementation according to Library.insert/merge in ML;
Fri, 14 Dec 2012 12:09:08 +0100 wenzelm more formal class Command.Results;
Thu, 13 Dec 2012 17:29:23 +0100 wenzelm more careful handling of Dialog_Result, with active area and color feedback;
Thu, 13 Dec 2012 13:52:18 +0100 wenzelm identify dialogs via official serial and maintain as result message;
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.;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Thu, 22 Nov 2012 13:21:02 +0100 wenzelm more abstract Sendback operations, with explicit id/exec_id properties;
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;
Fri, 28 Sep 2012 15:25:49 +0200 wenzelm tuned signature;
Thu, 27 Sep 2012 19:34:31 +0200 wenzelm operations to turn markup into XML;
Sat, 22 Sep 2012 19:23:04 +0200 wenzelm accumulate under exec_id as well;
Sat, 22 Sep 2012 19:16:48 +0200 wenzelm more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
Fri, 21 Sep 2012 16:50:44 +0200 wenzelm more realistic sendback: pick exec_id from message position and text from buffer;
Thu, 20 Sep 2012 11:09:53 +0200 wenzelm tuned signature;
Wed, 19 Sep 2012 17:07:25 +0200 wenzelm earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
Tue, 18 Sep 2012 17:20:40 +0200 wenzelm more explicit message markup and rendering;
Tue, 18 Sep 2012 14:51:12 +0200 wenzelm some actual rich text markup via XML.content_markup;
Tue, 18 Sep 2012 13:18:45 +0200 wenzelm some support for inital command markup;
Fri, 14 Sep 2012 20:49:54 +0200 wenzelm refined output panel: more value-oriented approach to update and caret focus;
Fri, 31 Aug 2012 14:35:04 +0200 wenzelm more markup for failed goal forks, reusing "bad";
Fri, 24 Aug 2012 19:35:44 +0200 wenzelm more precise counting of line/column;
Fri, 10 Aug 2012 13:33:07 +0200 wenzelm clarified undefined, unparsed, unfinished command spans;
Thu, 09 Aug 2012 17:13:46 +0200 wenzelm tuned signature;
Tue, 07 Aug 2012 22:25:17 +0200 wenzelm more structural parsing for minor modes;
Mon, 30 Jul 2012 13:42:45 +0200 wenzelm tuned signature;
Fri, 13 Apr 2012 21:17:59 +0200 wenzelm include trailing comments in proper_command range;
Mon, 19 Mar 2012 14:59:31 +0100 wenzelm clarified command span classification: strict Command.is_command, permissive Command.name;
Tue, 13 Mar 2012 21:17:37 +0100 wenzelm clarified command state -- markup within proper_range, excluding trailing whitespace;
Sun, 04 Mar 2012 19:03:28 +0100 wenzelm added Command.proper_range (still unused);
Mon, 27 Feb 2012 17:13:25 +0100 wenzelm prefer final ADTs -- prevent ooddities;
Mon, 09 Jan 2012 23:08:33 +0100 wenzelm tuned;
Sat, 07 Jan 2012 12:39:46 +0100 wenzelm accumulate status as regular markup for command range;
Thu, 01 Dec 2011 14:29:14 +0100 wenzelm clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
Tue, 29 Nov 2011 20:18:02 +0100 wenzelm clarified modules;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Sat, 26 Nov 2011 17:10:03 +0100 wenzelm sharing of token source with span source;
Fri, 11 Nov 2011 14:24:38 +0100 wenzelm prefer statically typed Text.Markup;
Sat, 17 Sep 2011 23:04:03 +0200 wenzelm Document.Node.Name convenience;
Thu, 01 Sep 2011 13:34:45 +0200 wenzelm more abstract Document.Node.Name;
Wed, 31 Aug 2011 15:41:22 +0200 wenzelm maintain name of *the* enclosing node as part of command -- avoid full document traversal;
Thu, 25 Aug 2011 11:41:48 +0200 wenzelm slightly more abstract Command.Perspective;
Tue, 23 Aug 2011 12:20:12 +0200 wenzelm propagate editor perspective through document model;
Mon, 22 Aug 2011 21:42:02 +0200 wenzelm some support for editor perspective;
Sat, 09 Jul 2011 12:56:51 +0200 wenzelm tuned signature;
Mon, 04 Jul 2011 22:25:33 +0200 wenzelm Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
less more (0) -100 -60 tip