1.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 16:22:28 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 17:09:28 2013 +0200
     1.3 @@ -108,6 +108,11 @@
     1.4  fun set_result result =
     1.5    map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
     1.6  
     1.7 +fun finished_theory node =
     1.8 +  (case Exn.capture (Command.eval_result o the) (get_result node) of
     1.9 +    Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
    1.10 +  | _ => false);
    1.11 +
    1.12  fun get_node nodes name = String_Graph.get_node nodes name
    1.13    handle String_Graph.UNDEF _ => empty_node;
    1.14  fun default_node name = String_Graph.default_node (name, empty_node);
    1.15 @@ -275,12 +280,6 @@
    1.16    in (versions', commands', execution) end);
    1.17  
    1.18  
    1.19 -fun finished_theory node =
    1.20 -  (case Exn.capture (Command.memo_result o the) (get_result node) of
    1.21 -    Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
    1.22 -  | _ => false);
    1.23 -
    1.24 -
    1.25  
    1.26  (** document execution **)
    1.27  
    1.28 @@ -349,7 +348,7 @@
    1.29          | NONE =>
    1.30              Toplevel.end_theory (Position.file_only import)
    1.31                (#state
    1.32 -                (Command.memo_result
    1.33 +                (Command.eval_result
    1.34                    (the_default Command.no_eval
    1.35                      (get_result (snd (the (AList.lookup (op =) deps import)))))))));
    1.36      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
    1.37 @@ -376,11 +375,11 @@
    1.38            val same' =
    1.39              (case opt_exec of
    1.40                NONE => false
    1.41 -            | SOME (exec_id, exec) =>
    1.42 +            | SOME (eval, _) =>
    1.43                  (case lookup_entry node0 id of
    1.44                    NONE => false
    1.45 -                | SOME (exec_id0, _) =>
    1.46 -                    exec_id = exec_id0 andalso Command.stable_eval (exec_id, exec)));
    1.47 +                | SOME (eval0, _) =>
    1.48 +                    #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
    1.49          in SOME (same', (prev, flags')) end
    1.50        else NONE;
    1.51      val (same, (common, flags)) =
    1.52 @@ -405,7 +404,7 @@
    1.53          else (I, init);
    1.54  
    1.55        val exec_id' = Document_ID.make ();
    1.56 -      val eval' =
    1.57 +      val eval_body' =
    1.58          Command.memo (fn () =>
    1.59            let
    1.60              val eval_state = Command.exec_result (snd command_exec);
    1.61 @@ -416,13 +415,14 @@
    1.62                    |> modify_init
    1.63                    |> Toplevel.put_id exec_id') ();
    1.64            in Command.eval span tr eval_state end);
    1.65 +      val eval' = {exec_id = exec_id', eval = eval_body'};
    1.66        val prints' = if command_visible then Command.print command_name eval' else [];
    1.67 -      val command_exec' = (command_id', (exec_id', (eval', prints')));
    1.68 +      val command_exec' = (command_id', (eval', prints'));
    1.69      in SOME (command_exec' :: execs, command_exec', init') end;
    1.70  
    1.71  fun update_prints state node command_id =
    1.72    (case the_entry node command_id of
    1.73 -    SOME (exec_id, (eval, prints)) =>
    1.74 +    SOME (eval, prints) =>
    1.75        let
    1.76          val (command_name, _) = the_command state command_id;
    1.77          val new_prints = Command.print command_name eval;
    1.78 @@ -433,7 +433,7 @@
    1.79              | NONE => new_print));
    1.80        in
    1.81          if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
    1.82 -        else SOME (command_id, (exec_id, (eval, prints')))
    1.83 +        else SOME (command_id, (eval, prints'))
    1.84        end
    1.85    | NONE => NONE);
    1.86  
    1.87 @@ -479,7 +479,7 @@
    1.88                        else last_common state last_visible node0 node;
    1.89                      val common_command_exec = the_default_entry node common;
    1.90  
    1.91 -                    val (new_execs, (command_id', (_, (eval', _))), _) =
    1.92 +                    val (new_execs, (command_id', (eval', _)), _) =
    1.93                        ([], common_command_exec, if initial then SOME init else NONE) |>
    1.94                        (still_visible orelse node_required) ?
    1.95                          iterate_entries_after common
    1.96 @@ -489,14 +489,14 @@
    1.97  
    1.98                      val updated_execs =
    1.99                        (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
   1.100 -                        if exists (fn (_, (id', _)) => id = id') new_execs then I
   1.101 +                        if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
   1.102                          else append (the_list (update_prints state node id)));
   1.103  
   1.104                      val no_execs =
   1.105                        iterate_entries_after common
   1.106                          (fn ((_, id0), exec0) => fn res =>
   1.107                            if is_none exec0 then NONE
   1.108 -                          else if exists (fn (_, (id, _)) => id0 = id) updated_execs
   1.109 +                          else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
   1.110                            then SOME res
   1.111                            else SOME (id0 :: res)) node0 [];
   1.112