src/Pure/PIDE/command.scala
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);
Thu, 23 Jun 2011 14:52:32 +0200 wenzelm explicit import java.lang.System to prevent odd scope problems;
Tue, 16 Nov 2010 22:40:45 +0100 wenzelm avoid spam;
Wed, 10 Nov 2010 15:00:40 +0100 wenzelm some support for nested source structure, based on section headings;
Wed, 22 Sep 2010 22:39:17 +0200 wenzelm Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
Fri, 17 Sep 2010 17:10:44 +0200 wenzelm allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
Tue, 07 Sep 2010 16:51:28 +0200 wenzelm Command.State.accumulate: check actual source range;
Tue, 07 Sep 2010 16:40:30 +0200 wenzelm Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
Tue, 31 Aug 2010 23:28:21 +0200 wenzelm Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
Mon, 30 Aug 2010 20:11:21 +0200 wenzelm Command.newlines: account for physical newlines;
Mon, 30 Aug 2010 13:01:32 +0200 wenzelm Command.results: ordered by serial number;
Wed, 25 Aug 2010 22:45:24 +0200 wenzelm tuned;
Wed, 25 Aug 2010 22:37:53 +0200 wenzelm organized markup properties via apply/unapply patterns;
Wed, 25 Aug 2010 18:19:04 +0200 wenzelm more precise Command.State accumulation;
Tue, 24 Aug 2010 20:36:48 +0200 wenzelm tuned root markup;
Mon, 23 Aug 2010 16:13:13 +0200 wenzelm tuned;
Sun, 22 Aug 2010 20:11:17 +0200 wenzelm simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
Sun, 22 Aug 2010 19:53:20 +0200 wenzelm tuned signature;
Sun, 22 Aug 2010 18:46:16 +0200 wenzelm renamed Markup_Tree.Node to Text.Info;
Sun, 22 Aug 2010 16:37:15 +0200 wenzelm Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
Sun, 22 Aug 2010 13:59:47 +0200 wenzelm Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;
Sun, 22 Aug 2010 12:54:12 +0200 wenzelm Command.State: accumulate markup reports uniformly;
Thu, 19 Aug 2010 22:52:00 +0200 wenzelm parameterized type Markup_Tree.Node;
Thu, 19 Aug 2010 11:26:07 +0200 wenzelm Command.status: full XML.Tree, i.e. Markup with potential "arguments";
Wed, 18 Aug 2010 23:44:50 +0200 wenzelm more efficient Markup_Tree, based on branches sorted by quasi-order;
Wed, 18 Aug 2010 11:25:09 +0200 wenzelm decode Isabelle symbol positions in one spot;
Mon, 16 Aug 2010 00:07:28 +0200 wenzelm simplified command status: interpret stacked markup on demand;
Sun, 15 Aug 2010 23:07:22 +0200 wenzelm some derived operations on Text.Range;
Sun, 15 Aug 2010 22:48:56 +0200 wenzelm specific types Text.Offset and Text.Range;
Sat, 14 Aug 2010 23:01:53 +0200 wenzelm Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
Sat, 14 Aug 2010 11:52:24 +0200 wenzelm tuned;
Fri, 13 Aug 2010 18:21:19 +0200 wenzelm explicit Document.State value, instead of individual state variables in Session, Command, Document;
Thu, 12 Aug 2010 17:55:23 +0200 wenzelm more basic notion of unparsed input;
less more (0) -60 tip