src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Mon Aug 22 21:09:26 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 22 21:42:02 2011 +0200
@@ -19,7 +19,8 @@
   datatype node_edit =
     Clear |
     Edits of (command_id option * command_id option) list |
-    Header of node_header
+    Header of node_header |
+    Perspective of id list
   type edit = string * node_edit
   type state
   val init_state: state
@@ -95,7 +96,8 @@
 datatype node_edit =
   Clear |
   Edits of (command_id option * command_id option) list |
-  Header of node_header;
+  Header of node_header |
+  Perspective of id list;
 
 type edit = string * node_edit;
 
@@ -150,7 +152,8 @@
             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));
+          in Graph.map_node name (set_header header') nodes3 end
+      | Perspective _ => nodes));  (* FIXME *)
 
 fun put_node (name, node) (Version nodes) =
   Version (update_node name (K node) nodes);