src/Pure/PIDE/document.ML
changeset 44385 e7fdb008aa7d
parent 44384 8f6054a63f96
child 44386 4048ca2658b7
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 22 21:42:02 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 23 12:20:12 2011 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4      Clear |
     1.5      Edits of (command_id option * command_id option) list |
     1.6      Header of node_header |
     1.7 -    Perspective of id list
     1.8 +    Perspective of command_id list
     1.9    type edit = string * node_edit
    1.10    type state
    1.11    val init_state: state
    1.12 @@ -61,30 +61,38 @@
    1.13  
    1.14  abstype node = Node of
    1.15   {header: node_header,
    1.16 +  perspective: command_id list,
    1.17    entries: exec_id option Entries.T,  (*command entries with excecutions*)
    1.18    result: Toplevel.state lazy}
    1.19  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.20  with
    1.21  
    1.22 -fun make_node (header, entries, result) =
    1.23 -  Node {header = header, entries = entries, result = result};
    1.24 +fun make_node (header, perspective, entries, result) =
    1.25 +  Node {header = header, perspective = perspective, entries = entries, result = result};
    1.26  
    1.27 -fun map_node f (Node {header, entries, result}) =
    1.28 -  make_node (f (header, entries, result));
    1.29 +fun map_node f (Node {header, perspective, entries, result}) =
    1.30 +  make_node (f (header, perspective, entries, result));
    1.31  
    1.32  fun get_header (Node {header, ...}) = header;
    1.33 -fun set_header header = map_node (fn (_, entries, result) => (header, entries, result));
    1.34 +fun set_header header =
    1.35 +  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    1.36  
    1.37 -fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result);
    1.38 +fun get_perspective (Node {perspective, ...}) = perspective;
    1.39 +fun set_perspective perspective =
    1.40 +  map_node (fn (header, _, entries, result) => (header, perspective, entries, result));
    1.41 +
    1.42 +fun map_entries f (Node {header, perspective, entries, result}) =
    1.43 +  make_node (header, perspective, f entries, result);
    1.44  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    1.45  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    1.46  
    1.47  fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
    1.48 -fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
    1.49 +fun set_result result =
    1.50 +  map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
    1.51  
    1.52  val empty_exec = Lazy.value Toplevel.toplevel;
    1.53 -val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec);
    1.54 -val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
    1.55 +val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), [], Entries.empty, empty_exec);
    1.56 +val clear_node = map_node (fn (header, _, _, _) => (header, [], Entries.empty, empty_exec));
    1.57  
    1.58  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    1.59  fun default_node name = Graph.default_node (name, empty_node);
    1.60 @@ -97,7 +105,7 @@
    1.61    Clear |
    1.62    Edits of (command_id option * command_id option) list |
    1.63    Header of node_header |
    1.64 -  Perspective of id list;
    1.65 +  Perspective of command_id list;
    1.66  
    1.67  type edit = string * node_edit;
    1.68  
    1.69 @@ -153,7 +161,8 @@
    1.70                (header, Graph.add_deps_acyclic (name, parents) nodes2)
    1.71                  handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    1.72            in Graph.map_node name (set_header header') nodes3 end
    1.73 -      | Perspective _ => nodes));  (* FIXME *)
    1.74 +      | Perspective perspective =>
    1.75 +          update_node name (set_perspective perspective) nodes));
    1.76  
    1.77  fun put_node (name, node) (Version nodes) =
    1.78    Version (update_node name (K node) nodes);
    1.79 @@ -354,9 +363,10 @@
    1.80                          | NONE =>
    1.81                              get_theory (Position.file_only import)
    1.82                                (#2 (Future.join (the (AList.lookup (op =) deps import))))));
    1.83 -                  in Thy_Load.begin_theory dir thy_name imports files parents end
    1.84 +                  in Thy_Load.begin_theory dir thy_name imports files parents end;
    1.85                  fun get_command id =
    1.86                    (id, the_command state id |> Future.map (Toplevel.modify_init init));
    1.87 +                val perspective = get_perspective node;  (* FIXME *)
    1.88                in
    1.89                  (singleton o Future.forks)
    1.90                    {name = "Document.edit", group = NONE,