src/Pure/PIDE/command.scala
2011-12-01 ago clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
2011-11-29 ago clarified modules;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-26 ago sharing of token source with span source;
2011-11-11 ago prefer statically typed Text.Markup;
2011-09-17 ago Document.Node.Name convenience;
2011-09-01 ago more abstract Document.Node.Name;
2011-08-31 ago maintain name of *the* enclosing node as part of command -- avoid full document traversal;
2011-08-25 ago slightly more abstract Command.Perspective;
2011-08-23 ago propagate editor perspective through document model;
2011-08-22 ago some support for editor perspective;
2011-07-09 ago tuned signature;
2011-07-04 ago Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-06-23 ago explicit import java.lang.System to prevent odd scope problems;
2010-11-16 ago avoid spam;
2010-11-10 ago some support for nested source structure, based on section headings;
2010-09-22 ago Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
2010-09-17 ago allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
2010-09-07 ago Command.State.accumulate: check actual source range;
2010-09-07 ago Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
2010-08-31 ago Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
2010-08-30 ago Command.newlines: account for physical newlines;
2010-08-30 ago Command.results: ordered by serial number;
2010-08-25 ago tuned;
2010-08-25 ago organized markup properties via apply/unapply patterns;
2010-08-25 ago more precise Command.State accumulation;
2010-08-24 ago tuned root markup;
2010-08-23 ago tuned;
2010-08-22 ago simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
2010-08-22 ago tuned signature;
2010-08-22 ago renamed Markup_Tree.Node to Text.Info;
2010-08-22 ago Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
2010-08-22 ago Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;
2010-08-22 ago Command.State: accumulate markup reports uniformly;
2010-08-19 ago parameterized type Markup_Tree.Node;
2010-08-19 ago Command.status: full XML.Tree, i.e. Markup with potential "arguments";
2010-08-18 ago more efficient Markup_Tree, based on branches sorted by quasi-order;
2010-08-18 ago decode Isabelle symbol positions in one spot;
2010-08-16 ago simplified command status: interpret stacked markup on demand;
2010-08-15 ago some derived operations on Text.Range;
2010-08-15 ago specific types Text.Offset and Text.Range;
2010-08-14 ago Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
2010-08-14 ago tuned;
2010-08-13 ago explicit Document.State value, instead of individual state variables in Session, Command, Document;
2010-08-12 ago more basic notion of unparsed input;
2010-08-12 ago clarified "state" (accumulated data) vs. "exec" (execution that produces data);
2010-08-12 ago misc tuning and simplification;
2010-08-12 ago specific command state;
2010-08-12 ago specific Session.Commands_Changed;
2010-08-11 ago 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);
2010-08-06 ago avoid null in Scala;
2010-08-05 ago simplified/refined document model: collection of named nodes, without proper dependencies yet;
2010-06-13 ago tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
2010-05-30 ago more detailed token markup, including command kind as sub_kind;
2010-05-29 ago tuned messages;
2010-05-28 ago accumulate only local results -- no proper history support yet;
2010-05-27 ago Command.toString: include id for debugging;
2010-05-20 ago explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
2010-05-05 ago some rearrangement of Scala sources;