# HG changeset patch
# User wenzelm
# Date 1333623714 -7200
# Node ID 7828c7b3c1432ba14d0a79df9fbb88f5ec8c5eb3
# Parent  00f6279bb67ad2c94b74c909c477b6991187d334
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
edit of perspective touches node superficially, to ensure revisit after update;

diff -r 00f6279bb67a -r 7828c7b3c143 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Apr 05 11:58:46 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Apr 05 13:01:54 2012 +0200
@@ -10,7 +10,8 @@
   type 'a memo
   val memo: (unit -> 'a) -> 'a memo
   val memo_value: 'a -> 'a memo
-  val memo_result: 'a memo -> 'a Exn.result
+  val memo_eval: 'a memo -> 'a
+  val memo_result: 'a memo -> 'a
   val memo_stable: 'a memo -> bool
   val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
 end;
@@ -41,7 +42,7 @@
 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
 
-fun memo_result (Memo v) =
+fun memo_eval (Memo v) =
   (case Synchronized.value v of
     Result res => res
   | _ =>
@@ -49,7 +50,13 @@
         (fn Result res => SOME (res, Result res)
           | Expr e =>
               let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
-              in SOME (res, Result res) end));
+              in SOME (res, Result res) end))
+  |> Exn.release;
+
+fun memo_result (Memo v) =
+  (case Synchronized.value v of
+    Result res => Exn.release res
+  | _ => raise Fail "Unfinished memo result");
 
 fun memo_stable (Memo v) =
   (case Synchronized.value v of
diff -r 00f6279bb67a -r 7828c7b3c143 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Apr 05 11:58:46 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Apr 05 13:01:54 2012 +0200
@@ -226,7 +226,7 @@
         in Graph.map_node name (set_header header'') nodes3 end
         |> touch_node name
     | Perspective perspective =>
-        update_node name (set_perspective perspective) nodes);
+        update_node name (set_perspective perspective #> set_touched true) nodes);
 
 end;
 
@@ -337,8 +337,8 @@
           SOME thy => thy
         | NONE =>
             Toplevel.end_theory (Position.file_only import)
-              (fst (Exn.release (Command.memo_result
-                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))))));
+              (fst (Command.memo_eval  (* FIXME memo_result !?! *)
+                (get_result (snd (Future.join (the (AList.lookup (op =) deps import)))))))));
   in Thy_Load.begin_theory master_dir header parents end;
 
 fun check_theory nodes name =
@@ -396,7 +396,7 @@
             |> modify_init
             |> Toplevel.put_id exec_id'_string);
       val exec' = Command.memo (fn () =>
-        let val (st, _) = Exn.release (Command.memo_result (snd (snd command_exec)));
+        let val (st, _) = Command.memo_result (snd (snd command_exec));
         in Command.run_command (tr ()) st end);
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;
@@ -486,7 +486,7 @@
       fun force_exec _ _ NONE = ()
         | force_exec node command_id (SOME (_, exec)) =
             let
-              val (_, print) = Exn.release (Command.memo_result exec);
+              val (_, print) = Command.memo_eval exec;
               val _ =
                 if #1 (get_perspective node) command_id
                 then ignore (Lazy.future Future.default_params print)