clarified type Command.eval;

--- a/src/Pure/PIDE/command.ML	Fri Jul 05 16:22:28 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jul 05 17:09:28 2013 +0200
@@ -19,19 +19,20 @@
   val read: span -> Toplevel.transition
   type eval_state =
     {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
-  type eval = eval_state memo
+  type eval = {exec_id: Document_ID.exec, eval: eval_state memo}
   val no_eval: eval
+  val eval_result: eval -> eval_state
   val eval: span -> Toplevel.transition -> eval_state -> eval_state
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
   val print: string -> eval -> print list
   val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
-  type exec = Document_ID.exec * (eval * print list)
+  type exec = eval * print list
   val no_exec: exec
   val exec_ids: exec -> Document_ID.exec list
   val exec_result: exec -> eval_state
   val exec_run: exec -> unit
-  val stable_eval: exec -> bool
+  val stable_eval: eval -> bool
   val stable_print: print -> bool
 end;
 
@@ -125,8 +126,10 @@
 val no_eval_state: eval_state =
   {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
 
-type eval = eval_state memo;
-val no_eval = memo_value no_eval_state;
+type eval = {exec_id: Document_ID.exec, eval: eval_state memo};
+
+val no_eval: eval = {exec_id = Document_ID.none, eval = memo_value no_eval_state};
+fun eval_result ({eval, ...}: eval) = memo_result eval;
 
 local
 
@@ -210,7 +213,7 @@
           val exec_id = Document_ID.make ();
           fun body () =
             let
-              val {failed, command, state = st', ...} = memo_result eval;
+              val {failed, command, state = st', ...} = eval_result eval;
               val tr = Toplevel.put_id exec_id command;
             in if failed then () else print_error tr (fn () => print_fn tr st') () end;
         in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
@@ -219,7 +222,7 @@
           val exec_id = Document_ID.make ();
           fun body () =
             let
-              val {command, ...} = memo_result eval;
+              val {command, ...} = eval_result eval;
               val tr = Toplevel.put_id exec_id command;
             in output_error tr exn end;
         in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
@@ -244,29 +247,29 @@
 
 
 
-(** managed evaluation with potential interrupts **)
+(** managed evaluation **)
 
 (* execution *)
 
-type exec = Document_ID.exec * (eval * print list);
-val no_exec: exec = (Document_ID.none, (no_eval, []));
+type exec = eval * print list;
+val no_exec: exec = (no_eval, []);
 
-fun exec_ids ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
+fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
 
-fun exec_result ((_, (eval, _)): exec) = memo_result eval;
+fun exec_result (({eval, ...}, _): exec) = memo_result eval;
 
-fun exec_run ((_, (eval, prints)): exec) =
+fun exec_run (({eval, ...}, prints): exec) =
  (memo_eval eval;
   prints |> List.app (fn {name, pri, print, ...} =>
     memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
 
 
-(* stable situations *)
+(* stable situations after cancellation *)
 
 fun stable_goals exec_id =
   not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
 
-fun stable_eval ((exec_id, (eval, _)): exec) =
+fun stable_eval ({exec_id, eval}: eval) =
   stable_goals exec_id andalso memo_stable eval;
 
 fun stable_print ({exec_id, print, ...}: print) =

--- a/src/Pure/PIDE/document.ML	Fri Jul 05 16:22:28 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jul 05 17:09:28 2013 +0200
@@ -108,6 +108,11 @@
 fun set_result result =
   map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
 
+fun finished_theory node =
+  (case Exn.capture (Command.eval_result o the) (get_result node) of
+    Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
+  | _ => false);
+
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
 fun default_node name = String_Graph.default_node (name, empty_node);
@@ -275,12 +280,6 @@
   in (versions', commands', execution) end);
 
 
-fun finished_theory node =
-  (case Exn.capture (Command.memo_result o the) (get_result node) of
-    Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
-  | _ => false);
-
-
 
 (** document execution **)
 
@@ -349,7 +348,7 @@
         | NONE =>
             Toplevel.end_theory (Position.file_only import)
               (#state
-                (Command.memo_result
+                (Command.eval_result
                   (the_default Command.no_eval
                     (get_result (snd (the (AList.lookup (op =) deps import)))))))));
     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
@@ -376,11 +375,11 @@
           val same' =
             (case opt_exec of
               NONE => false
-            | SOME (exec_id, exec) =>
+            | SOME (eval, _) =>
                 (case lookup_entry node0 id of
                   NONE => false
-                | SOME (exec_id0, _) =>
-                    exec_id = exec_id0 andalso Command.stable_eval (exec_id, exec)));
+                | SOME (eval0, _) =>
+                    #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
         in SOME (same', (prev, flags')) end
       else NONE;
     val (same, (common, flags)) =
@@ -405,7 +404,7 @@
         else (I, init);
 
       val exec_id' = Document_ID.make ();
-      val eval' =
+      val eval_body' =
         Command.memo (fn () =>
           let
             val eval_state = Command.exec_result (snd command_exec);
@@ -416,13 +415,14 @@
                   |> modify_init
                   |> Toplevel.put_id exec_id') ();
           in Command.eval span tr eval_state end);
+      val eval' = {exec_id = exec_id', eval = eval_body'};
       val prints' = if command_visible then Command.print command_name eval' else [];
-      val command_exec' = (command_id', (exec_id', (eval', prints')));
+      val command_exec' = (command_id', (eval', prints'));
     in SOME (command_exec' :: execs, command_exec', init') end;
 
 fun update_prints state node command_id =
   (case the_entry node command_id of
-    SOME (exec_id, (eval, prints)) =>
+    SOME (eval, prints) =>
       let
         val (command_name, _) = the_command state command_id;
         val new_prints = Command.print command_name eval;
@@ -433,7 +433,7 @@
             | NONE => new_print));
       in
         if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
-        else SOME (command_id, (exec_id, (eval, prints')))
+        else SOME (command_id, (eval, prints'))
       end
   | NONE => NONE);
 
@@ -479,7 +479,7 @@
                       else last_common state last_visible node0 node;
                     val common_command_exec = the_default_entry node common;
 
-                    val (new_execs, (command_id', (_, (eval', _))), _) =
+                    val (new_execs, (command_id', (eval', _)), _) =
                       ([], common_command_exec, if initial then SOME init else NONE) |>
                       (still_visible orelse node_required) ?
                         iterate_entries_after common
@@ -489,14 +489,14 @@
 
                     val updated_execs =
                       (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
-                        if exists (fn (_, (id', _)) => id = id') new_execs then I
+                        if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
                         else append (the_list (update_prints state node id)));
 
                     val no_execs =
                       iterate_entries_after common
                         (fn ((_, id0), exec0) => fn res =>
                           if is_none exec0 then NONE
-                          else if exists (fn (_, (id, _)) => id0 = id) updated_execs
+                          else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
                           then SOME res
                           else SOME (id0 :: res)) node0 [];