--- a/src/Pure/PIDE/document.ML Mon Aug 05 15:03:52 2013 +0200
+++ b/src/Pure/PIDE/document.ML Mon Aug 05 15:29:10 2013 +0200
@@ -9,7 +9,7 @@
sig
val timing: bool Unsynchronized.ref
type node_header = string * Thy_Header.header * string list
- type overlay = Document_ID.command * string * string list
+ type overlay = Document_ID.command * (string * string list)
datatype node_edit =
Clear | (* FIXME unused !? *)
Edits of (Document_ID.command option * Document_ID.command option) list |
@@ -68,7 +68,7 @@
{required = required,
visible = Inttab.make_set command_ids,
visible_last = try List.last command_ids,
- overlays = Inttab.make_list (map (fn (x, y, z) => (x, (y, z))) overlays)};
+ overlays = Inttab.make_list overlays};
val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
val no_perspective = make_perspective (false, [], []);
@@ -135,7 +135,7 @@
(* node edits and associated executions *)
-type overlay = Document_ID.command * string * string list;
+type overlay = Document_ID.command * (string * string list);
datatype node_edit =
Clear |