| Tue, 07 Sep 2010 16:51:28 +0200 |
wenzelm |
Command.State.accumulate: check actual source range;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 20:11:21 +0200 |
wenzelm |
Command.newlines: account for physical newlines;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 13:01:32 +0200 |
wenzelm |
Command.results: ordered by serial number;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 22:45:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 22:37:53 +0200 |
wenzelm |
organized markup properties via apply/unapply patterns;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:19:04 +0200 |
wenzelm |
more precise Command.State accumulation;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 20:36:48 +0200 |
wenzelm |
tuned root markup;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 16:13:13 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 19:53:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 18:46:16 +0200 |
wenzelm |
renamed Markup_Tree.Node to Text.Info;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 16:37:15 +0200 |
wenzelm |
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 13:59:47 +0200 |
wenzelm |
Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 12:54:12 +0200 |
wenzelm |
Command.State: accumulate markup reports uniformly;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 22:52:00 +0200 |
wenzelm |
parameterized type Markup_Tree.Node;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:26:07 +0200 |
wenzelm |
Command.status: full XML.Tree, i.e. Markup with potential "arguments";
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 23:44:50 +0200 |
wenzelm |
more efficient Markup_Tree, based on branches sorted by quasi-order;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 11:25:09 +0200 |
wenzelm |
decode Isabelle symbol positions in one spot;
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 00:07:28 +0200 |
wenzelm |
simplified command status: interpret stacked markup on demand;
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 23:07:22 +0200 |
wenzelm |
some derived operations on Text.Range;
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 22:48:56 +0200 |
wenzelm |
specific types Text.Offset and Text.Range;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 14 Aug 2010 11:52:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 13 Aug 2010 18:21:19 +0200 |
wenzelm |
explicit Document.State value, instead of individual state variables in Session, Command, Document;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 17:55:23 +0200 |
wenzelm |
more basic notion of unparsed input;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 15:19:11 +0200 |
wenzelm |
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 14:22:23 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:59:18 +0200 |
wenzelm |
specific command state;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:49:08 +0200 |
wenzelm |
specific Session.Commands_Changed;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Fri, 06 Aug 2010 21:52:49 +0200 |
wenzelm |
avoid null in Scala;
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 14:35:35 +0200 |
wenzelm |
simplified/refined document model: collection of named nodes, without proper dependencies yet;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 18:23:50 +0200 |
wenzelm |
more detailed token markup, including command kind as sub_kind;
|
file |
diff |
annotate
|
| Sat, 29 May 2010 20:49:04 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Fri, 28 May 2010 22:21:08 +0200 |
wenzelm |
accumulate only local results -- no proper history support yet;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 00:47:15 +0200 |
wenzelm |
Command.toString: include id for debugging;
|
file |
diff |
annotate
|
| Thu, 20 May 2010 10:43:46 +0200 |
wenzelm |
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
|
file |
diff |
annotate
|
| Wed, 05 May 2010 22:23:45 +0200 |
wenzelm |
some rearrangement of Scala sources;
|
file |
diff |
annotate
| base
|