src/Pure/PIDE/document.ML
changeset 47340 9bbf7fd96bcd
parent 47339 79bd24497ffd
child 47341 00f6279bb67a
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Apr 04 21:03:30 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Apr 05 10:45:53 2012 +0200
     1.3 @@ -62,14 +62,14 @@
     1.4  type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
     1.5  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
     1.6  
     1.7 -type exec = exec_id * (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
     1.8 +type exec = (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
     1.9  val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ()));
    1.10  
    1.11  abstype node = Node of
    1.12   {touched: bool,
    1.13    header: node_header,
    1.14    perspective: perspective,
    1.15 -  entries: exec option Entries.T,  (*command entries with excecutions*)
    1.16 +  entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    1.17    last_exec: command_id option,  (*last command with exec state assignment*)
    1.18    result: Toplevel.state lazy}
    1.19  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.20 @@ -356,11 +356,16 @@
    1.21              NONE => true
    1.22            | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
    1.23        in (visible', initial') end;
    1.24 -    fun get_common ((prev, id), exec) (found, (_, flags)) =
    1.25 +    fun get_common ((prev, id), opt_exec) (found, (_, flags)) =
    1.26        if found then NONE
    1.27        else
    1.28          let val found' =
    1.29 -          is_none exec orelse op <> (pairself (Option.map #1) (exec, lookup_entry node0 id));
    1.30 +          (case opt_exec of
    1.31 +            NONE => true
    1.32 +          | SOME (exec_id, exec) =>
    1.33 +              (case lookup_entry node0 id of
    1.34 +                NONE => true
    1.35 +              | SOME (exec_id0, _) => exec_id <> exec_id0));
    1.36          in SOME (found', (prev, update_flags prev flags)) end;
    1.37      val (found, (common, flags)) =
    1.38        iterate_entries get_common node (false, (NONE, (true, true)));
    1.39 @@ -409,9 +414,7 @@
    1.40      val updated =
    1.41        nodes |> Graph.schedule
    1.42          (fn deps => fn (name, node) =>
    1.43 -          if not (is_touched node orelse is_required name)
    1.44 -          then Future.value (([], [], []), node)
    1.45 -          else
    1.46 +          if is_touched node orelse is_required name then
    1.47              let
    1.48                val node0 = node_of old_version name;
    1.49                fun init () = init_theory deps node;
    1.50 @@ -455,7 +458,8 @@
    1.51                        |> set_result result
    1.52                        |> set_touched false;
    1.53                    in ((no_execs, execs, [(name, node')]), node') end)
    1.54 -            end)
    1.55 +            end
    1.56 +          else Future.value (([], [], []), node))
    1.57        |> Future.joins |> map #1;
    1.58  
    1.59      val command_execs =