--- a/src/Pure/PIDE/document.ML Mon Aug 22 21:42:02 2011 +0200
+++ b/src/Pure/PIDE/document.ML Tue Aug 23 12:20:12 2011 +0200
@@ -20,7 +20,7 @@
Clear |
Edits of (command_id option * command_id option) list |
Header of node_header |
- Perspective of id list
+ Perspective of command_id list
type edit = string * node_edit
type state
val init_state: state
@@ -61,30 +61,38 @@
abstype node = Node of
{header: node_header,
+ perspective: command_id list,
entries: exec_id option Entries.T, (*command entries with excecutions*)
result: Toplevel.state lazy}
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-fun make_node (header, entries, result) =
- Node {header = header, entries = entries, result = result};
+fun make_node (header, perspective, entries, result) =
+ Node {header = header, perspective = perspective, entries = entries, result = result};
-fun map_node f (Node {header, entries, result}) =
- make_node (f (header, entries, result));
+fun map_node f (Node {header, perspective, entries, result}) =
+ make_node (f (header, perspective, entries, result));
fun get_header (Node {header, ...}) = header;
-fun set_header header = map_node (fn (_, entries, result) => (header, entries, result));
+fun set_header header =
+ map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
-fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result);
+fun get_perspective (Node {perspective, ...}) = perspective;
+fun set_perspective perspective =
+ map_node (fn (header, _, entries, result) => (header, perspective, entries, result));
+
+fun map_entries f (Node {header, perspective, entries, result}) =
+ make_node (header, perspective, f entries, result);
fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
-fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
+fun set_result result =
+ map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
val empty_exec = Lazy.value Toplevel.toplevel;
-val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec);
-val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
+val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), [], Entries.empty, empty_exec);
+val clear_node = map_node (fn (header, _, _, _) => (header, [], Entries.empty, empty_exec));
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
fun default_node name = Graph.default_node (name, empty_node);
@@ -97,7 +105,7 @@
Clear |
Edits of (command_id option * command_id option) list |
Header of node_header |
- Perspective of id list;
+ Perspective of command_id list;
type edit = string * node_edit;
@@ -153,7 +161,8 @@
(header, Graph.add_deps_acyclic (name, parents) nodes2)
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
in Graph.map_node name (set_header header') nodes3 end
- | Perspective _ => nodes)); (* FIXME *)
+ | Perspective perspective =>
+ update_node name (set_perspective perspective) nodes));
fun put_node (name, node) (Version nodes) =
Version (update_node name (K node) nodes);
@@ -354,9 +363,10 @@
| NONE =>
get_theory (Position.file_only import)
(#2 (Future.join (the (AList.lookup (op =) deps import))))));
- in Thy_Load.begin_theory dir thy_name imports files parents end
+ in Thy_Load.begin_theory dir thy_name imports files parents end;
fun get_command id =
(id, the_command state id |> Future.map (Toplevel.modify_init init));
+ val perspective = get_perspective node; (* FIXME *)
in
(singleton o Future.forks)
{name = "Document.edit", group = NONE,