1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 29 15:20:02 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 29 15:59:47 2013 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
     1.5    type eval
     1.6    val eval_eq: eval * eval -> bool
     1.7 +  val eval_finished: eval -> bool
     1.8    val eval_result_state: eval -> Toplevel.state
     1.9    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.10    type print
    1.11 @@ -116,6 +117,8 @@
    1.12  
    1.13  fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.14  
    1.15 +fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
    1.16 +
    1.17  fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
    1.18  val eval_result_state = #state o eval_result;
    1.19  

     2.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 15:20:02 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 29 15:59:47 2013 +0200
     2.3 @@ -105,10 +105,10 @@
     2.4    | (NONE, NONE) => false
     2.5    | _ => true);
     2.6  
     2.7 -fun finished_theory node =
     2.8 -  (case Exn.capture (Command.eval_result_state o the) (get_result node) of
     2.9 -    Exn.Res st => can (Toplevel.end_theory Position.none) st
    2.10 -  | _ => false);
    2.11 +fun pending_result node =
    2.12 +  (case get_result node of
    2.13 +    SOME eval => not (Command.eval_finished eval)
    2.14 +  | NONE => false);
    2.15  
    2.16  fun get_node nodes name = String_Graph.get_node nodes name
    2.17    handle String_Graph.UNDEF _ => empty_node;
    2.18 @@ -295,9 +295,7 @@
    2.19        if Execution.is_running execution_id then
    2.20          nodes_of (the_version state version_id) |> String_Graph.schedule
    2.21            (fn deps => fn (name, node) =>
    2.22 -            if not (visible_node node) andalso finished_theory node then
    2.23 -              Future.value ()
    2.24 -            else
    2.25 +            if visible_node node orelse pending_result node then
    2.26                (singleton o Future.forks)
    2.27                  {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    2.28                    deps = map (Future.task_of o #2) deps, pri = pri, interrupts = false}
    2.29 @@ -308,7 +306,8 @@
    2.30                          if Execution.is_running execution_id
    2.31                          then SOME (Command.exec execution_id exec)
    2.32                          else NONE
    2.33 -                    | NONE => NONE)) node ()))
    2.34 +                    | NONE => NONE)) node ())
    2.35 +            else Future.value ())
    2.36        else [];
    2.37    in () end;
    2.38  
    2.39 @@ -448,6 +447,7 @@
    2.40  
    2.41      val nodes = nodes_of new_version;
    2.42      val is_required = make_required nodes;
    2.43 +    val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty;
    2.44  
    2.45      val updated = timeit "Document.update" (fn () =>
    2.46        nodes |> String_Graph.schedule
    2.47 @@ -458,11 +458,10 @@
    2.48              (fn () =>
    2.49                let
    2.50                  val imports = map (apsnd Future.join) deps;
    2.51 -                val imports_changed = exists (#4 o #1 o #2) imports;
    2.52 +                val imports_result_changed = exists (#4 o #1 o #2) imports;
    2.53                  val node_required = is_required name;
    2.54                in
    2.55 -                if imports_changed orelse AList.defined (op =) edits name orelse
    2.56 -                  not (finished_theory node)
    2.57 +                if Symtab.defined edited name orelse visible_node node orelse imports_result_changed
    2.58                  then
    2.59                    let
    2.60                      val node0 = node_of old_version name;
    2.61 @@ -472,7 +471,7 @@
    2.62                        forall (fn (name, (_, node)) => check_theory true name node) imports;
    2.63  
    2.64                      val (print_execs, common, (still_visible, initial)) =
    2.65 -                      if imports_changed then (assign_update_empty, NONE, (true, true))
    2.66 +                      if imports_result_changed then (assign_update_empty, NONE, (true, true))
    2.67                        else last_common state node0 node;
    2.68                      val common_command_exec = the_default_entry node common;
    2.69