src/Pure/PIDE/document.ML
changeset 52808 143f225e50f5
parent 52798 9d3c9862d1dd
child 52810 cd28423ba19f
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 31 10:54:37 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 31 12:14:13 2013 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4      Clear |    (* FIXME unused !? *)
     1.5      Edits of (Document_ID.command option * Document_ID.command option) list |
     1.6      Deps of node_header |
     1.7 -    Perspective of Document_ID.command list
     1.8 +    Perspective of bool * Document_ID.command list
     1.9    type edit = string * node_edit
    1.10    type state
    1.11    val init_state: state
    1.12 @@ -40,12 +40,12 @@
    1.13  fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
    1.14  
    1.15  type node_header = string * Thy_Header.header * string list;
    1.16 -type perspective = Inttab.set * Document_ID.command option;
    1.17 +type perspective = bool * Inttab.set * Document_ID.command option;
    1.18  structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
    1.19  
    1.20  abstype node = Node of
    1.21   {header: node_header,  (*master directory, theory header, errors*)
    1.22 -  perspective: perspective,  (*visible commands, last visible command*)
    1.23 +  perspective: perspective,  (*required node, visible commands, last visible command*)
    1.24    entries: Command.exec option Entries.T,  (*command entries with excecutions*)
    1.25    result: Command.eval option}  (*result of last execution*)
    1.26  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    1.27 @@ -57,11 +57,11 @@
    1.28  fun map_node f (Node {header, perspective, entries, result}) =
    1.29    make_node (f (header, perspective, entries, result));
    1.30  
    1.31 -fun make_perspective command_ids : perspective =
    1.32 -  (Inttab.make_set command_ids, try List.last command_ids);
    1.33 +fun make_perspective (required, command_ids) : perspective =
    1.34 +  (required, Inttab.make_set command_ids, try List.last command_ids);
    1.35  
    1.36  val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
    1.37 -val no_perspective = make_perspective [];
    1.38 +val no_perspective = make_perspective (false, []);
    1.39  
    1.40  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.41  val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
    1.42 @@ -83,11 +83,12 @@
    1.43    in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
    1.44  
    1.45  fun get_perspective (Node {perspective, ...}) = perspective;
    1.46 -fun set_perspective ids =
    1.47 -  map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
    1.48 +fun set_perspective args =
    1.49 +  map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));
    1.50  
    1.51 -val visible_command = Inttab.defined o #1 o get_perspective;
    1.52 -val visible_last = #2 o get_perspective;
    1.53 +val required_node = #1 o get_perspective;
    1.54 +val visible_command = Inttab.defined o #2 o get_perspective;
    1.55 +val visible_last = #3 o get_perspective;
    1.56  val visible_node = is_some o visible_last
    1.57  
    1.58  fun map_entries f =
    1.59 @@ -127,7 +128,7 @@
    1.60    Clear |
    1.61    Edits of (Document_ID.command option * Document_ID.command option) list |
    1.62    Deps of node_header |
    1.63 -  Perspective of Document_ID.command list;
    1.64 +  Perspective of bool * Document_ID.command list;
    1.65  
    1.66  type edit = string * node_edit;
    1.67  
    1.68 @@ -365,16 +366,18 @@
    1.69  
    1.70  fun make_required nodes =
    1.71    let
    1.72 -    val all_visible =
    1.73 -      String_Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
    1.74 +    fun all_preds P =
    1.75 +      String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes []
    1.76        |> String_Graph.all_preds nodes
    1.77 -      |> map (rpair ()) |> Symtab.make;
    1.78 +      |> Symtab.make_set;
    1.79  
    1.80 -    val required =
    1.81 -      Symtab.fold (fn (a, ()) =>
    1.82 -        exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
    1.83 -          Symtab.update (a, ())) all_visible Symtab.empty;
    1.84 -  in required end;
    1.85 +    val all_visible = all_preds visible_node;
    1.86 +    val all_required = all_preds required_node;
    1.87 +  in
    1.88 +    Symtab.fold (fn (a, ()) =>
    1.89 +      exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
    1.90 +        Symtab.update (a, ())) all_visible all_required
    1.91 +  end;
    1.92  
    1.93  fun init_theory deps node span =
    1.94    let