src/Pure/PIDE/command.scala
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;
less more (0) -14 tip