1.1 --- a/src/Pure/PIDE/command.ML	Thu Apr 05 11:58:46 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Apr 05 13:01:54 2012 +0200
     1.3 @@ -10,7 +10,8 @@
     1.4    type 'a memo
     1.5    val memo: (unit -> 'a) -> 'a memo
     1.6    val memo_value: 'a -> 'a memo
     1.7 -  val memo_result: 'a memo -> 'a Exn.result
     1.8 +  val memo_eval: 'a memo -> 'a
     1.9 +  val memo_result: 'a memo -> 'a
    1.10    val memo_stable: 'a memo -> bool
    1.11    val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
    1.12  end;
    1.13 @@ -41,7 +42,7 @@
    1.14  fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    1.15  fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    1.16  
    1.17 -fun memo_result (Memo v) =
    1.18 +fun memo_eval (Memo v) =
    1.19    (case Synchronized.value v of
    1.20      Result res => res
    1.21    | _ =>
    1.22 @@ -49,7 +50,13 @@
    1.23          (fn Result res => SOME (res, Result res)
    1.24            | Expr e =>
    1.25                let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
    1.26 -              in SOME (res, Result res) end));
    1.27 +              in SOME (res, Result res) end))
    1.28 +  |> Exn.release;
    1.29 +
    1.30 +fun memo_result (Memo v) =
    1.31 +  (case Synchronized.value v of
    1.32 +    Result res => Exn.release res
    1.33 +  | _ => raise Fail "Unfinished memo result");
    1.34  
    1.35  fun memo_stable (Memo v) =
    1.36    (case Synchronized.value v of

     2.1 --- a/src/Pure/PIDE/document.ML	Thu Apr 05 11:58:46 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Apr 05 13:01:54 2012 +0200
     2.3 @@ -226,7 +226,7 @@
     2.4          in Graph.map_node name (set_header header'') nodes3 end
     2.5          |> touch_node name
     2.6      | Perspective perspective =>
     2.7 -        update_node name (set_perspective perspective) nodes);
     2.8 +        update_node name (set_perspective perspective #> set_touched true) nodes);
     2.9  
    2.10  end;
    2.11  
    2.12 @@ -337,8 +337,8 @@
    2.13            SOME thy => thy
    2.14          | NONE =>
    2.15              Toplevel.end_theory (Position.file_only import)
    2.16 -              (fst (Exn.release (Command.memo_result
    2.17 -                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))))));
    2.18 +              (fst (Command.memo_eval  (* FIXME memo_result !?! *)
    2.19 +                (get_result (snd (Future.join (the (AList.lookup (op =) deps import)))))))));
    2.20    in Thy_Load.begin_theory master_dir header parents end;
    2.21  
    2.22  fun check_theory nodes name =
    2.23 @@ -396,7 +396,7 @@
    2.24              |> modify_init
    2.25              |> Toplevel.put_id exec_id'_string);
    2.26        val exec' = Command.memo (fn () =>
    2.27 -        let val (st, _) = Exn.release (Command.memo_result (snd (snd command_exec)));
    2.28 +        let val (st, _) = Command.memo_result (snd (snd command_exec));
    2.29          in Command.run_command (tr ()) st end);
    2.30        val command_exec' = (command_id', (exec_id', exec'));
    2.31      in SOME (command_exec' :: execs, command_exec', init') end;
    2.32 @@ -486,7 +486,7 @@
    2.33        fun force_exec _ _ NONE = ()
    2.34          | force_exec node command_id (SOME (_, exec)) =
    2.35              let
    2.36 -              val (_, print) = Exn.release (Command.memo_result exec);
    2.37 +              val (_, print) = Command.memo_eval exec;
    2.38                val _ =
    2.39                  if #1 (get_perspective node) command_id
    2.40                  then ignore (Lazy.future Future.default_params print)