src/Pure/PIDE/document.ML
changeset 47406 8818f54773cc
parent 47405 559b44b5164c
child 47407 8da23ecc70cd
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 09 17:38:39 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 09 19:50:04 2012 +0200
     1.3 @@ -66,20 +66,18 @@
     1.4  val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
     1.5  
     1.6  abstype node = Node of
     1.7 - {touched: bool,
     1.8 -  header: node_header,
     1.9 + {header: node_header,
    1.10    perspective: perspective,
    1.11    entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    1.12    result: exec}
    1.13  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.14  with
    1.15  
    1.16 -fun make_node (touched, header, perspective, entries, result) =
    1.17 -  Node {touched = touched, header = header, perspective = perspective,
    1.18 -    entries = entries, result = result};
    1.19 +fun make_node (header, perspective, entries, result) =
    1.20 +  Node {header = header, perspective = perspective, entries = entries, result = result};
    1.21  
    1.22 -fun map_node f (Node {touched, header, perspective, entries, result}) =
    1.23 -  make_node (f (touched, header, perspective, entries, result));
    1.24 +fun map_node f (Node {header, perspective, entries, result}) =
    1.25 +  make_node (f (header, perspective, entries, result));
    1.26  
    1.27  fun make_perspective command_ids : perspective =
    1.28    (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
    1.29 @@ -87,35 +85,26 @@
    1.30  val no_header = Exn.Exn (ERROR "Bad theory header");
    1.31  val no_perspective = make_perspective [];
    1.32  
    1.33 -val empty_node = make_node (false, no_header, no_perspective, Entries.empty, no_exec);
    1.34 -val clear_node = map_node (fn (_, header, _, _, _) =>
    1.35 -  (false, header, no_perspective, Entries.empty, no_exec));
    1.36 +val empty_node = make_node (no_header, no_perspective, Entries.empty, no_exec);
    1.37 +val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_exec));
    1.38  
    1.39  
    1.40  (* basic components *)
    1.41  
    1.42 -fun is_touched (Node {touched, ...}) = touched;
    1.43 -fun set_touched touched =
    1.44 -  map_node (fn (_, header, perspective, entries, result) =>
    1.45 -    (touched, header, perspective, entries, result));
    1.46 -
    1.47  fun get_header (Node {header, ...}) = header;
    1.48  fun set_header header =
    1.49 -  map_node (fn (touched, _, perspective, entries, result) =>
    1.50 -    (touched, header, perspective, entries, result));
    1.51 +  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    1.52  
    1.53  fun get_perspective (Node {perspective, ...}) = perspective;
    1.54  fun set_perspective ids =
    1.55 -  map_node (fn (touched, header, _, entries, result) =>
    1.56 -    (touched, header, make_perspective ids, entries, result));
    1.57 +  map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
    1.58  
    1.59  val visible_command = #1 o get_perspective;
    1.60  val visible_last = #2 o get_perspective;
    1.61  val visible_node = is_some o visible_last
    1.62  
    1.63  fun map_entries f =
    1.64 -  map_node (fn (touched, header, perspective, entries, result) =>
    1.65 -    (touched, header, perspective, f entries, result));
    1.66 +  map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
    1.67  fun get_entries (Node {entries, ...}) = entries;
    1.68  
    1.69  fun iterate_entries f = Entries.iterate NONE f o get_entries;
    1.70 @@ -126,8 +115,7 @@
    1.71  
    1.72  fun get_result (Node {result, ...}) = result;
    1.73  fun set_result result =
    1.74 -  map_node (fn (touched, header, perspective, entries, _) =>
    1.75 -    (touched, header, perspective, entries, result));
    1.76 +  map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
    1.77  
    1.78  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    1.79  fun default_node name = Graph.default_node (name, empty_node);
    1.80 @@ -182,30 +170,13 @@
    1.81  fun nodes_of (Version nodes) = nodes;
    1.82  val node_of = get_node o nodes_of;
    1.83  
    1.84 -local
    1.85 -
    1.86  fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
    1.87  
    1.88 -fun touch_node name nodes =
    1.89 -  fold (fn desc =>
    1.90 -      update_node desc
    1.91 -        (set_touched true #>
    1.92 -          desc <> name ? (map_entries (reset_after NONE) #> set_result no_exec)))
    1.93 -    (Graph.all_succs nodes [name]) nodes;
    1.94 -
    1.95 -in
    1.96 -
    1.97  fun edit_nodes (name, node_edit) (Version nodes) =
    1.98    Version
    1.99      (case node_edit of
   1.100 -      Clear =>
   1.101 -        nodes
   1.102 -        |> update_node name clear_node
   1.103 -        |> touch_node name
   1.104 -    | Edits edits =>
   1.105 -        nodes
   1.106 -        |> update_node name (edit_node edits)
   1.107 -        |> touch_node name
   1.108 +      Clear => update_node name clear_node nodes
   1.109 +    | Edits edits => update_node name (edit_node edits) nodes
   1.110      | Header header =>
   1.111          let
   1.112            val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
   1.113 @@ -222,11 +193,7 @@
   1.114              (header', Graph.add_deps_acyclic (name, imports) nodes2)
   1.115                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
   1.116          in Graph.map_node name (set_header header'') nodes3 end
   1.117 -        |> touch_node name
   1.118 -    | Perspective perspective =>
   1.119 -        update_node name (set_perspective perspective #> set_touched true) nodes);
   1.120 -
   1.121 -end;
   1.122 +    | Perspective perspective => update_node name (set_perspective perspective) nodes);
   1.123  
   1.124  fun put_node (name, node) (Version nodes) =
   1.125    Version (update_node name (K node) nodes);
   1.126 @@ -388,7 +355,7 @@
   1.127            Symtab.update (a, ())) all_visible Symtab.empty;
   1.128    in Symtab.defined required end;
   1.129  
   1.130 -fun init_theory deps node =
   1.131 +fun init_theory imports node =
   1.132    let
   1.133      (* FIXME provide files via Scala layer, not master_dir *)
   1.134      val (dir, header) = Exn.release (get_header node);
   1.135 @@ -402,8 +369,8 @@
   1.136            SOME thy => thy
   1.137          | NONE =>
   1.138              Toplevel.end_theory (Position.file_only import)
   1.139 -              (fst (Command.memo_eval  (* FIXME memo_result !?! *)
   1.140 -                (get_result (snd (Future.join (the (AList.lookup (op =) deps import)))))))));
   1.141 +              (fst (Command.memo_result
   1.142 +                (get_result (snd (the (AList.lookup (op =) imports import))))))));
   1.143    in Thy_Load.begin_theory master_dir header parents end;
   1.144  
   1.145  fun check_theory nodes name =
   1.146 @@ -460,9 +427,9 @@
   1.147              #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
   1.148              |> modify_init
   1.149              |> Toplevel.put_id exec_id'_string);
   1.150 -      val exec' = Command.memo (fn () =>
   1.151 -        let val (st, _) = Command.memo_eval (snd (snd command_exec));  (* FIXME memo_result !?! *)
   1.152 -        in Command.run_command (tr ()) st end);
   1.153 +      val exec' =
   1.154 +        Command.memo (fn () =>
   1.155 +          Command.run_command (tr ()) (fst (Command.memo_result (snd (snd command_exec)))));
   1.156        val command_exec' = (command_id', (exec_id', exec'));
   1.157      in SOME (command_exec' :: execs, command_exec', init') end;
   1.158  
   1.159 @@ -481,21 +448,28 @@
   1.160      val updated =
   1.161        nodes |> Graph.schedule
   1.162          (fn deps => fn (name, node) =>
   1.163 -          if is_touched node orelse is_required name andalso not (stable_finished_theory node) then
   1.164 -            let
   1.165 -              val node0 = node_of old_version name;
   1.166 -              fun init () = init_theory deps node;
   1.167 -              val bad_init =
   1.168 -                not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
   1.169 -            in
   1.170 -              (singleton o Future.forks)
   1.171 -                {name = "Document.update", group = NONE,
   1.172 -                  deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
   1.173 -                (fn () =>
   1.174 +          (singleton o Future.forks)
   1.175 +            {name = "Document.update", group = NONE,
   1.176 +              deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
   1.177 +            (fn () =>
   1.178 +              let
   1.179 +                val imports = map (apsnd Future.join) deps;
   1.180 +                val updated_imports = exists (is_some o #3 o #1 o #2) imports;
   1.181 +                val required = is_required name;
   1.182 +              in
   1.183 +                if updated_imports orelse AList.defined (op =) edits name orelse
   1.184 +                  required andalso not (stable_finished_theory node)
   1.185 +                then
   1.186                    let
   1.187 -                    val required = is_required name;
   1.188 +                    val node0 = node_of old_version name;
   1.189 +                    fun init () = init_theory imports node;
   1.190 +                    val bad_init =
   1.191 +                      not (check_theory nodes name andalso forall (check_theory nodes o #1) imports);
   1.192 +
   1.193                      val last_visible = visible_last node;
   1.194 -                    val (common, (visible, initial)) = last_common state last_visible node0 node;
   1.195 +                    val (common, (visible, initial)) =
   1.196 +                      if updated_imports then (NONE, (true, true))
   1.197 +                      else last_common state last_visible node0 node;
   1.198                      val common_command_exec = the_default_entry node common;
   1.199  
   1.200                      val (new_execs, (command_id', (_, exec')), _) =
   1.201 @@ -521,17 +495,19 @@
   1.202                      val node' = node
   1.203                        |> fold reset_entry no_execs
   1.204                        |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
   1.205 -                      |> set_result result
   1.206 -                      |> set_touched false;
   1.207 -                  in ((no_execs, new_execs, [(name, node')]), node') end)
   1.208 -            end
   1.209 -          else Future.value (([], [], []), node))
   1.210 +                      |> set_result result;
   1.211 +                    val updated_node =
   1.212 +                      if null no_execs andalso null new_execs then NONE
   1.213 +                      else SOME (name, node');
   1.214 +                  in ((no_execs, new_execs, updated_node), node') end
   1.215 +                else (([], [], NONE), node)
   1.216 +              end))
   1.217        |> Future.joins |> map #1;
   1.218  
   1.219      val command_execs =
   1.220        map (rpair NONE) (maps #1 updated) @
   1.221        map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   1.222 -    val updated_nodes = maps #3 updated;
   1.223 +    val updated_nodes = map_filter #3 updated;
   1.224  
   1.225      val state' = state
   1.226        |> define_version new_id (fold put_node updated_nodes new_version);