2012-03-19 wenzelm 2012-03-19 clarified command span classification: strict Command.is_command, permissive;
2012-03-13 wenzelm 2012-03-13 clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-04 wenzelm 2012-03-04 added Command.proper_range (still unused);
2012-02-27 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2012-01-09 wenzelm 2012-01-09 tuned;
2012-01-07 wenzelm 2012-01-07 accumulate status as regular markup for command range; tuned signature;
2011-12-01 wenzelm 2011-12-01 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
2011-11-29 wenzelm 2011-11-29 clarified modules;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-26 wenzelm 2011-11-26 sharing of token source with span source;
2011-11-11 wenzelm 2011-11-11 prefer statically typed Text.Markup;
2011-09-17 wenzelm 2011-09-17 Document.Node.Name convenience;
2011-09-01 wenzelm 2011-09-01 more abstract Document.Node.Name; tuned signature;
2011-08-31 wenzelm 2011-08-31 maintain name of *the* enclosing node as part of command -- avoid full document traversal;
2011-08-25 wenzelm 2011-08-25 slightly more abstract Command.Perspective;
2011-08-23 wenzelm 2011-08-23 propagate editor perspective through document model;
2011-08-22 wenzelm 2011-08-22 some support for editor perspective;
2011-07-09 wenzelm 2011-07-09 tuned signature;
2011-07-04 wenzelm 2011-07-04 Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-06-23 wenzelm 2011-06-23 explicit import java.lang.System to prevent odd scope problems;
2010-11-16 wenzelm 2010-11-16 avoid spam;
2010-11-10 wenzelm 2010-11-10 some support for nested source structure, based on section headings;
2010-09-22 wenzelm 2010-09-22 Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
2010-09-17 wenzelm 2010-09-17 allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
2010-09-07 wenzelm 2010-09-07 Command.State.accumulate: check actual source range;
2010-09-07 wenzelm 2010-09-07 Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
2010-08-31 wenzelm 2010-08-31 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body; Position.Id_Range convenience;
2010-08-30 wenzelm 2010-08-30 Command.newlines: account for physical newlines;
2010-08-30 wenzelm 2010-08-30 Command.results: ordered by serial number;
2010-08-25 wenzelm 2010-08-25 tuned;
2010-08-25 wenzelm 2010-08-25 organized markup properties via apply/unapply patterns;
2010-08-25 wenzelm 2010-08-25 more precise Command.State accumulation;
2010-08-24 wenzelm 2010-08-24 tuned root markup;
2010-08-23 wenzelm 2010-08-23 tuned;
2010-08-22 wenzelm 2010-08-22 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
2010-08-22 wenzelm 2010-08-22 tuned signature;
2010-08-22 wenzelm 2010-08-22 renamed Markup_Tree.Node to Text.Info; body may depend on full Text.Info, including range; tuned;
2010-08-22 wenzelm 2010-08-22 Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
2010-08-22 wenzelm 2010-08-22 Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;
2010-08-22 wenzelm 2010-08-22 Command.State: accumulate markup reports uniformly; Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo; tuned;
2010-08-19 wenzelm 2010-08-19 parameterized type Markup_Tree.Node; allow arbitrary interpretations, not just filtering; renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps;
2010-08-19 wenzelm 2010-08-19 Command.status: full XML.Tree, i.e. Markup with potential "arguments";
2010-08-18 wenzelm 2010-08-18 more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned;
2010-08-18 wenzelm 2010-08-18 decode Isabelle symbol positions in one spot;
2010-08-16 wenzelm 2010-08-16 simplified command status: interpret stacked markup on demand;
2010-08-15 wenzelm 2010-08-15 some derived operations on Text.Range;
2010-08-15 wenzelm 2010-08-15 specific types Text.Offset and Text.Range; minor tuning;
2010-08-14 wenzelm 2010-08-14 Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
2010-08-14 wenzelm 2010-08-14 tuned;
2010-08-13 wenzelm 2010-08-13 explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;
2010-08-12 wenzelm 2010-08-12 more basic notion of unparsed input;
2010-08-12 wenzelm 2010-08-12 clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type (ML) / Document.ID;
2010-08-12 wenzelm 2010-08-12 misc tuning and simplification;
2010-08-12 wenzelm 2010-08-12 specific command state;
2010-08-12 wenzelm 2010-08-12 specific Session.Commands_Changed;
2010-08-11 wenzelm 2010-08-11 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 wenzelm 2010-08-06 avoid null in Scala; tuned comments;
2010-08-05 wenzelm 2010-08-05 simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;
2010-06-13 wenzelm 2010-06-13 tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
2010-05-30 wenzelm 2010-05-30 more detailed token markup, including command kind as sub_kind; type-safe access to Command.HighlightInfo;