src/Pure/PIDE/document.ML

   type node_header = (string * string list * (string * bool) list) Exn.result
   datatype node_edit =
     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
   val join_commands: state -> unit
   val cancel_execution: state -> Future.task list

 type node_header = (string * string list * (string * bool) list) Exn.result;
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 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 map_node f (Node {header, entries, result}) =
-  make_node (f (header, entries, result));
+fun make_node (header, perspective, entries, result) =
+  Node {header = header, perspective = perspective, entries = entries, result = 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 map_entries f (Node {header, entries, result}) = make_node (header, f entries, result);
+fun set_header header =
+  map_node (fn (_, perspective, entries, result) => (header, perspective, 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);
 fun update_node name f = default_node name #> Graph.map_node name f;
 

 
 datatype node_edit =
   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;
 
 fun the_entry (Node {entries, ...}) id =
   (case Entries.lookup entries id of

                   (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
             val (header', nodes3) =
               (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);
 
 end;

                         (case Thy_Info.lookup_theory import of
                           SOME thy => thy
                         | 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,
                     deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
                   (fn () =>