src/Pure/PIDE/command.scala
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;
Thu, 12 Aug 2010 15:19:11 +0200 wenzelm clarified "state" (accumulated data) vs. "exec" (execution that produces data);
Thu, 12 Aug 2010 14:22:23 +0200 wenzelm misc tuning and simplification;
Thu, 12 Aug 2010 13:59:18 +0200 wenzelm specific command state;
Thu, 12 Aug 2010 13:49:08 +0200 wenzelm specific Session.Commands_Changed;
Wed, 11 Aug 2010 22:41:26 +0200 wenzelm represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
Fri, 06 Aug 2010 21:52:49 +0200 wenzelm avoid null in Scala;
Thu, 05 Aug 2010 14:35:35 +0200 wenzelm simplified/refined document model: collection of named nodes, without proper dependencies yet;
Sun, 13 Jun 2010 22:33:18 +0200 wenzelm tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
Sun, 30 May 2010 18:23:50 +0200 wenzelm more detailed token markup, including command kind as sub_kind;
Sat, 29 May 2010 20:49:04 +0200 wenzelm tuned messages;
Fri, 28 May 2010 22:21:08 +0200 wenzelm accumulate only local results -- no proper history support yet;
Thu, 27 May 2010 00:47:15 +0200 wenzelm Command.toString: include id for debugging;
Thu, 20 May 2010 10:43:46 +0200 wenzelm explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
Wed, 05 May 2010 22:23:45 +0200 wenzelm some rearrangement of Scala sources;
less more (0) tip