merged

--- a/src/HOL/Library/Polynomial.thy	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/HOL/Library/Polynomial.thy	Fri Apr 06 13:50:07 2012 +0200
@@ -492,7 +492,7 @@
 
 subsection {* Multiplication of polynomials *}
 
-text {* TODO: move to Set_Interval.thy *}
+(* TODO: move to Set_Interval.thy *)
 lemma setsum_atMost_Suc_shift:
   fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
   shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"

--- a/src/Pure/Concurrent/par_exn.ML	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Fri Apr 06 13:50:07 2012 +0200
@@ -14,7 +14,7 @@
   val release_first: 'a Exn.result list -> 'a list
 end;
 
-structure Par_Exn =
+structure Par_Exn: PAR_EXN =
 struct
 
 (* identification via serial numbers *)

--- a/src/Pure/IsaMakefile	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/IsaMakefile	Fri Apr 06 13:50:07 2012 +0200
@@ -155,6 +155,7 @@
   ML/ml_parse.ML					\
   ML/ml_syntax.ML					\
   ML/ml_thms.ML						\
+  PIDE/command.ML					\
   PIDE/document.ML					\
   PIDE/isabelle_markup.ML				\
   PIDE/markup.ML					\

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/command.ML	Fri Apr 06 13:50:07 2012 +0200
@@ -0,0 +1,127 @@
+(*  Title:      Pure/PIDE/command.ML
+    Author:     Makarius
+
+Prover command execution.
+*)
+
+signature COMMAND =
+sig
+  val parse_command: string -> string -> Token.T list
+  type 'a memo
+  val memo: (unit -> 'a) -> 'a memo
+  val memo_value: 'a -> 'a memo
+  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;
+
+structure Command: COMMAND =
+struct
+
+(* parse command *)
+
+fun parse_command id text =
+  Position.setmp_thread_data (Position.id_only id)
+    (fn () =>
+      let
+        val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
+        val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
+      in toks end) ();
+
+
+(* memo results *)
+
+datatype 'a expr =
+  Expr of unit -> 'a |
+  Result of 'a Exn.result;
+
+abstype 'a memo = Memo of 'a expr Synchronized.var
+with
+
+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_eval (Memo v) =
+  (case Synchronized.value v of
+    Result res => res
+  | _ =>
+      Synchronized.guarded_access v
+        (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))
+  |> 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
+    Result (Exn.Exn exn) => not (Exn.is_interrupt exn)
+  | _ => true);
+
+end;
+
+
+(* run command *)
+
+local
+
+fun run int tr st =
+  (case Toplevel.transition int tr st of
+    SOME (st', NONE) => ([], SOME st')
+  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
+  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
+
+fun timing tr t =
+  if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
+
+fun proof_status tr st =
+  (case try Toplevel.proof_of st of
+    SOME prf => Toplevel.status tr (Proof.status_markup prf)
+  | NONE => ());
+
+val no_print = Lazy.value ();
+
+fun print_state tr st =
+  (Lazy.lazy o Toplevel.setmp_thread_position tr)
+    (fn () => Toplevel.print_state false st);
+
+in
+
+fun run_command tr st =
+  let
+    val is_init = Toplevel.is_init tr;
+    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
+
+    val _ = Multithreading.interrupted ();
+    val _ = Toplevel.status tr Isabelle_Markup.forked;
+    val start = Timing.start ();
+    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+    val _ = timing tr (Timing.result start);
+    val _ = Toplevel.status tr Isabelle_Markup.joined;
+    val _ = List.app (Toplevel.error_msg tr) errs;
+  in
+    (case result of
+      NONE =>
+        let
+          val _ = if null errs then Exn.interrupt () else ();
+          val _ = Toplevel.status tr Isabelle_Markup.failed;
+        in (st, no_print) end
+    | SOME st' =>
+        let
+          val _ = Toplevel.status tr Isabelle_Markup.finished;
+          val _ = proof_status tr st';
+          val do_print =
+            not is_init andalso
+              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+        in (st', if do_print then print_state tr st' else no_print) end)
+  end;
+
+end;
+
+end;
+

--- a/src/Pure/PIDE/document.ML	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Apr 06 13:50:07 2012 +0200
@@ -25,11 +25,11 @@
   type state
   val init_state: state
   val define_command: command_id -> string -> string -> state -> state
+  val discontinue_execution: state -> unit
   val cancel_execution: state -> Future.task list
-  val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
+  val execute: version_id -> state -> state
   val update: version_id -> version_id -> edit list -> state ->
     ((command_id * exec_id option) list * (string * command_id option) list) * state
-  val execute: version_id -> state -> state
   val remove_versions: version_id list -> state -> state
   val state: unit -> state
   val change_state: (state -> state) -> unit
@@ -62,17 +62,16 @@
 type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
-type exec = exec_id * (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
-val no_print = Lazy.value ();
-val no_exec = (no_id, Lazy.value (Toplevel.toplevel, no_print));
+type exec = (Toplevel.state * unit lazy) Command.memo;  (*eval/print process*)
+val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
 
 abstype node = Node of
  {touched: bool,
   header: node_header,
   perspective: perspective,
-  entries: exec option Entries.T,  (*command entries with excecutions*)
+  entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
   last_exec: command_id option,  (*last command with exec state assignment*)
-  result: Toplevel.state lazy}
+  result: exec}
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
@@ -88,11 +87,10 @@
 
 val no_header = Exn.Exn (ERROR "Bad theory header");
 val no_perspective = make_perspective [];
-val no_result = Lazy.value Toplevel.toplevel;
 
-val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
+val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec);
 val clear_node = map_node (fn (_, header, _, _, _, _) =>
-  (false, header, no_perspective, Entries.empty, NONE, no_result));
+  (false, header, no_perspective, Entries.empty, NONE, no_exec));
 
 
 (* basic components *)
@@ -112,6 +110,10 @@
   map_node (fn (touched, header, _, entries, last_exec, result) =>
     (touched, header, make_perspective ids, entries, last_exec, result));
 
+val visible_command = #1 o get_perspective;
+val visible_last = #2 o get_perspective;
+val visible_node = is_some o visible_last
+
 fun map_entries f =
   map_node (fn (touched, header, perspective, entries, last_exec, result) =>
     (touched, header, perspective, f entries, last_exec, result));
@@ -128,7 +130,7 @@
   map_node (fn (touched, header, perspective, entries, _, result) =>
     (touched, header, perspective, entries, last_exec, result));
 
-fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
+fun get_result (Node {result, ...}) = result;
 fun set_result result =
   map_node (fn (touched, header, perspective, entries, last_exec, _) =>
     (touched, header, perspective, entries, last_exec, result));
@@ -160,8 +162,8 @@
     NONE => err_undef "command entry" id
   | SOME (exec, _) => exec);
 
-fun the_default_entry node (SOME id) = (id, (the_default no_exec (the_entry node id)))
-  | the_default_entry _ NONE = (no_id, no_exec);
+fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id)))
+  | the_default_entry _ NONE = (no_id, (no_id, no_exec));
 
 fun update_entry id exec =
   map_entries (Entries.update (id, exec));
@@ -194,7 +196,7 @@
   fold (fn desc =>
       update_node desc
         (set_touched true #>
-          desc <> name ? (map_entries (reset_after NONE) #> set_result no_result)))
+          desc <> name ? (map_entries (reset_after NONE) #> set_result no_exec)))
     (Graph.all_succs nodes [name]) nodes;
 
 in
@@ -228,7 +230,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;
 
@@ -239,12 +241,12 @@
 
 
 
-(** global state -- document structure and execution process **)
+(** document state -- content structure and execution process **)
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
-  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> name * span*)
-  execution: version_id * Future.group}  (*current execution process*)
+  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
+  execution: version_id * Future.group * bool Unsynchronized.ref}  (*current execution process*)
 with
 
 fun make_state (versions, commands, execution) =
@@ -254,7 +256,8 @@
   make_state (f (versions, commands, execution));
 
 val init_state =
-  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE));
+  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
+    (no_id, Future.new_group NONE, Unsynchronized.ref false));
 
 
 (* document versions *)
@@ -276,18 +279,10 @@
 
 (* commands *)
 
-fun parse_command id text =
-  Position.setmp_thread_data (Position.id_only id)
-    (fn () =>
-      let
-        val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
-        val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
-      in toks end) ();
-
 fun define_command (id: command_id) name text =
   map_state (fn (versions, commands, execution) =>
     let
-      val span = Lazy.lazy (fn () => parse_command (print_id id) text);
+      val span = Lazy.lazy (fn () => Command.parse_command (print_id id) text);
       val commands' =
         Inttab.update_new (id, (name, span)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
@@ -301,85 +296,99 @@
 
 (* document execution *)
 
-fun cancel_execution (State {execution, ...}) = Future.cancel_group (#2 execution);
-
-end;
-
-
-(* toplevel transactions *)
-
-local
-
-fun timing tr t =
-  if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
-
-fun proof_status tr st =
-  (case try Toplevel.proof_of st of
-    SOME prf => Toplevel.status tr (Proof.status_markup prf)
-  | NONE => ());
-
-fun print_state tr st =
-  (Lazy.lazy o Toplevel.setmp_thread_position tr)
-    (fn () => Toplevel.print_state false st);
-
-fun run int tr st =
-  (case Toplevel.transition int tr st of
-    SOME (st', NONE) => ([], SOME st')
-  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
-  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
-
-in
+fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false;
 
-fun run_command tr st =
-  let
-    val is_init = Toplevel.is_init tr;
-    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
-
-    val _ = Multithreading.interrupted ();
-    val _ = Toplevel.status tr Isabelle_Markup.forked;
-    val start = Timing.start ();
-    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
-    val _ = timing tr (Timing.result start);
-    val _ = Toplevel.status tr Isabelle_Markup.joined;
-    val _ = List.app (Toplevel.error_msg tr) errs;
-  in
-    (case result of
-      NONE =>
-        let
-          val _ = if null errs then Exn.interrupt () else ();
-          val _ = Toplevel.status tr Isabelle_Markup.failed;
-        in (st, no_print) end
-    | SOME st' =>
-        let
-          val _ = Toplevel.status tr Isabelle_Markup.finished;
-          val _ = proof_status tr st';
-          val do_print =
-            not is_init andalso
-              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
-        in (st', if do_print then print_state tr st' else no_print) end)
-  end;
+fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group;
 
 end;
 
 
 
+(** execute **)
 
-(** update **)
+fun finished_theory node =
+  (case Exn.capture Command.memo_result (get_result node) of
+    Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
+  | _ => false);
 
-(* perspective *)
+fun execute version_id state =
+  state |> map_state (fn (versions, commands, _) =>
+    let
+      val version = the_version state version_id;
 
-fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state =
-  let
-    val old_version = the_version state old_id;
-    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *)
-    val new_version = edit_nodes (name, Perspective perspective) old_version;
-  in define_version new_id new_version state end;
+      fun run node command_id exec =
+        let
+          val (_, print) = Command.memo_eval exec;
+          val _ =
+            if visible_command node command_id
+            then ignore (Lazy.future Future.default_params print)
+            else ();
+        in () end;
+
+      val group = Future.new_group NONE;
+      val running = Unsynchronized.ref true;
+
+      val _ =
+        nodes_of version |> Graph.schedule
+          (fn deps => fn (name, node) =>
+            if not (visible_node node) andalso finished_theory node then
+              Future.value ()
+            else
+              (singleton o Future.forks)
+                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
+                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
+                (fn () =>
+                  iterate_entries (fn ((_, id), opt_exec) => fn () =>
+                    (case opt_exec of
+                      SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
+                    | NONE => NONE)) node ()));
+
+    in (versions, commands, (version_id, group, running)) end);
 
 
-(* edits *)
+
+
+(** edits **)
+
+(* update *)
 
 local
 
+fun make_required nodes =
+  let
+    val all_visible =
+      Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
+      |> Graph.all_preds nodes
+      |> map (rpair ()) |> Symtab.make;
+
+    val required =
+      Symtab.fold (fn (a, ()) =>
+        exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ?
+          Symtab.update (a, ())) all_visible Symtab.empty;
+  in Symtab.defined required end;
+
+fun init_theory deps node =
+  let
+    (* FIXME provide files via Scala layer, not master_dir *)
+    val (dir, header) = Exn.release (get_header node);
+    val master_dir =
+      (case Url.explode dir of
+        Url.File path => path
+      | _ => Path.current);
+    val parents =
+      #imports header |> map (fn import =>
+        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
+          SOME thy => thy
+        | NONE =>
+            Toplevel.end_theory (Position.file_only 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 =
+  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
+  is_some (Exn.get_res (get_header (get_node nodes name)));
+
 fun last_common state last_visible node0 node =
   let
     fun update_flags prev (visible, initial) =
@@ -390,11 +399,17 @@
             NONE => true
           | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
       in (visible', initial') end;
-    fun get_common ((prev, id), exec) (found, (_, flags)) =
+    fun get_common ((prev, id), opt_exec) (found, (_, flags)) =
       if found then NONE
       else
         let val found' =
-          is_none exec orelse op <> (pairself (Option.map #1) (exec, lookup_entry node0 id));
+          (case opt_exec of
+            NONE => true
+          | SOME (exec_id, exec) =>
+              not (Command.memo_stable exec) orelse
+              (case lookup_entry node0 id of
+                NONE => true
+              | SOME (exec_id0, _) => exec_id <> exec_id0));
         in SOME (found', (prev, update_flags prev flags)) end;
     val (found, (common, flags)) =
       iterate_entries get_common node (false, (NONE, (true, true)));
@@ -424,41 +439,12 @@
             #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
             |> modify_init
             |> Toplevel.put_id exec_id'_string);
-      val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command (tr ()) st);
+      val exec' = Command.memo (fn () =>
+        let val (st, _) = Command.memo_eval (snd (snd command_exec));  (* FIXME memo_result !?! *)
+        in Command.run_command (tr ()) st end);
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;
 
-fun make_required nodes =
-  let
-    val all_visible =
-      Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
-      |> Graph.all_preds nodes;
-    val required =
-      fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
-        all_visible Symtab.empty;
-  in Symtab.defined required end;
-
-fun check_theory nodes name =
-  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
-  is_some (Exn.get_res (get_header (get_node nodes name)));
-
-fun init_theory deps node =
-  let
-    (* FIXME provide files via Scala layer, not master_dir *)
-    val (dir, header) = Exn.release (get_header node);
-    val master_dir =
-      (case Url.explode dir of
-        Url.File path => path
-      | _ => Path.current);
-    val parents =
-      #imports header |> map (fn import =>
-        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
-          SOME thy => thy
-        | NONE =>
-            get_theory (Position.file_only import)
-              (snd (Future.join (the (AList.lookup (op =) deps import))))));
-  in Thy_Load.begin_theory master_dir header parents end;
-
 in
 
 fun update (old_id: version_id) (new_id: version_id) edits state =
@@ -473,9 +459,7 @@
     val updated =
       nodes |> Graph.schedule
         (fn deps => fn (name, node) =>
-          if not (is_touched node orelse is_required name)
-          then Future.value (([], [], []), node)
-          else
+          if is_touched node orelse is_required name andalso not (finished_theory node) then
             let
               val node0 = node_of old_version name;
               fun init () = init_theory deps node;
@@ -488,7 +472,7 @@
                 (fn () =>
                   let
                     val required = is_required name;
-                    val last_visible = #2 (get_perspective node);
+                    val last_visible = visible_last node;
                     val (common, (visible, initial)) = last_common state last_visible node0 node;
                     val common_command_exec = the_default_entry node common;
 
@@ -509,8 +493,8 @@
 
                     val last_exec = if command_id = no_id then NONE else SOME command_id;
                     val result =
-                      if is_some (after_entry node last_exec) then no_result
-                      else Lazy.map #1 exec;
+                      if is_some (after_entry node last_exec) then no_exec
+                      else exec;
 
                     val node' = node
                       |> fold reset_entry no_execs
@@ -519,7 +503,8 @@
                       |> set_result result
                       |> set_touched false;
                   in ((no_execs, execs, [(name, node')]), node') end)
-            end)
+            end
+          else Future.value (([], [], []), node))
       |> Future.joins |> map #1;
 
     val command_execs =
@@ -535,36 +520,6 @@
 end;
 
 
-(* execute *)
-
-fun execute version_id state =
-  state |> map_state (fn (versions, commands, _) =>
-    let
-      val version = the_version state version_id;
-
-      fun force_exec _ _ NONE = ()
-        | force_exec node command_id (SOME (_, exec)) =
-            let
-              val (_, print) = Lazy.force exec;
-              val _ =
-                if #1 (get_perspective node) command_id
-                then ignore (Lazy.future Future.default_params print)
-                else ();
-            in () end;
-
-      val group = Future.new_group NONE;
-      val _ =
-        nodes_of version |> Graph.schedule
-          (fn deps => fn (name, node) =>
-            (singleton o Future.forks)
-              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
-                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
-              (iterate_entries (fn ((_, id), exec) => fn () =>
-                SOME (force_exec node id exec)) node));
-
-    in (versions, commands, (version_id, group)) end);
-
-
 (* remove versions *)
 
 fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>

--- a/src/Pure/PIDE/protocol.ML	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Apr 06 13:50:07 2012 +0200
@@ -13,24 +13,12 @@
       Document.change_state (Document.define_command (Document.parse_id id) name text));
 
 val _ =
-  Isabelle_Process.protocol_command "Document.cancel_execution"
-    (fn [] => ignore (Document.cancel_execution (Document.state ())));
+  Isabelle_Process.protocol_command "Document.discontinue_execution"
+    (fn [] => Document.discontinue_execution (Document.state ()));
 
 val _ =
-  Isabelle_Process.protocol_command "Document.update_perspective"
-    (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
-      let
-        val old_id = Document.parse_id old_id_string;
-        val new_id = Document.parse_id new_id_string;
-        val ids = YXML.parse_body ids_yxml
-          |> let open XML.Decode in list int end;
-
-        val _ = Future.join_tasks (Document.cancel_execution state);
-      in
-        state
-        |> Document.update_perspective old_id new_id name ids
-        |> Document.execute new_id
-      end));
+  Isabelle_Process.protocol_command "Document.cancel_execution"
+    (fn [] => ignore (Document.cancel_execution (Document.state ())));
 
 val _ =
   Isabelle_Process.protocol_command "Document.update"

--- a/src/Pure/PIDE/protocol.scala	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Apr 06 13:50:07 2012 +0200
@@ -191,21 +191,9 @@
 
   /* document versions */
 
-  def cancel_execution()
-  {
-    input("Document.cancel_execution")
-  }
+  def discontinue_execution() { input("Document.discontinue_execution") }
 
-  def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
-    name: Document.Node.Name, perspective: Command.Perspective)
-  {
-    val ids =
-    { import XML.Encode._
-      list(long)(perspective.commands.map(_.id)) }
-
-    input("Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
-      name.node, YXML.string_of_body(ids))
-  }
+  def cancel_execution() { input("Document.cancel_execution") }
 
   def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
     edits: List[Document.Edit_Command])

--- a/src/Pure/ROOT.ML	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 06 13:50:07 2012 +0200
@@ -251,6 +251,7 @@
 use "Thy/present.ML";
 use "Thy/thy_load.ML";
 use "Thy/thy_info.ML";
+use "PIDE/command.ML";
 use "PIDE/document.ML";
 use "Thy/rail.ML";
 

--- a/src/Pure/System/session.scala	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/System/session.scala	Fri Apr 06 13:50:07 2012 +0200
@@ -267,27 +267,6 @@
     }
 
 
-    /* perspective */
-
-    def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
-    {
-      val previous = global_state().tip_version
-      val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
-
-      val text_edits: List[Document.Edit_Text] =
-        List((name, Document.Node.Perspective(text_perspective)))
-      val change =
-        global_state >>>
-          (_.continue_history(Future.value(previous), text_edits, Future.value(version)))
-
-      val assignment = global_state().the_assignment(previous).check_finished
-      global_state >> (_.define_version(version, assignment))
-      global_state >>> (_.assign(version.id))
-
-      prover.get.update_perspective(previous.id, version.id, name, perspective)
-    }
-
-
     /* incoming edits */
 
     def handle_edits(name: Document.Node.Name,
@@ -296,7 +275,7 @@
     {
       val previous = global_state().history.tip.version
 
-      prover.get.cancel_execution()
+      prover.get.discontinue_execution()
 
       val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
       val version = Future.promise[Document.Version]
@@ -465,12 +444,8 @@
           reply(())
 
         case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
-          if (text_edits.isEmpty && global_state().tip_stable &&
-              perspective.range.stop <= global_state().last_exec_offset(name))
-            update_perspective(name, perspective)
-          else
-            handle_edits(name, header,
-              List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
+          handle_edits(name, header,
+            List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
           reply(())
 
         case Messages(msgs) =>

--- a/src/Pure/Thy/thy_syntax.scala	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Apr 06 13:50:07 2012 +0200
@@ -118,28 +118,6 @@
     }
   }
 
-  def update_perspective(nodes: Document.Nodes,
-      name: Document.Node.Name, text_perspective: Text.Perspective)
-    : (Command.Perspective, Option[Document.Nodes]) =
-  {
-    val node = nodes(name)
-    val perspective = command_perspective(node, text_perspective)
-    val new_nodes =
-      if (node.perspective same perspective) None
-      else Some(nodes + (name -> node.update_perspective(perspective)))
-    (perspective, new_nodes)
-  }
-
-  def edit_perspective(previous: Document.Version,
-      name: Document.Node.Name, text_perspective: Text.Perspective)
-    : (Command.Perspective, Document.Version) =
-  {
-    val nodes = previous.nodes
-    val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
-    val version = Document.Version.make(previous.syntax, new_nodes getOrElse nodes)
-    (perspective, version)
-  }
-
 
 
   /** header edits: structure and outer syntax **/
@@ -311,11 +289,11 @@
       case (name, Document.Node.Header(_)) =>
 
       case (name, Document.Node.Perspective(text_perspective)) =>
-        update_perspective(nodes, name, text_perspective) match {
-          case (_, None) =>
-          case (perspective, Some(nodes1)) =>
-            doc_edits += (name -> Document.Node.Perspective(perspective))
-            nodes = nodes1
+        val node = nodes(name)
+        val perspective = command_perspective(node, text_perspective)
+        if (!(node.perspective same perspective)) {
+          doc_edits += (name -> Document.Node.Perspective(perspective))
+          nodes += (name -> node.update_perspective(perspective))
         }
     }
     (doc_edits.toList, Document.Version.make(syntax, nodes))

--- a/src/Pure/global_theory.ML	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Pure/global_theory.ML	Fri Apr 06 13:50:07 2012 +0200
@@ -49,7 +49,7 @@
 
 (** theory data **)
 
-type proofs = thm list * unit lazy;
+type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
 
 val empty_proofs: proofs = ([], Lazy.value ());
 
@@ -61,7 +61,7 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * (proofs * proofs);
+  type T = Facts.T * (proofs * proofs);  (*facts, recent proofs, all proofs of theory node*)
   val empty = (Facts.empty, (empty_proofs, empty_proofs));
   fun extend (facts, _) = (facts, snd empty);
   fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), snd empty);

--- a/src/Tools/quickcheck.ML	Fri Apr 06 10:37:46 2012 +0200
+++ b/src/Tools/quickcheck.ML	Fri Apr 06 13:50:07 2012 +0200
@@ -343,7 +343,7 @@
     val cs = space_explode " " s
   in
     if forall (fn c => c = "expand" orelse c = "interpret") cs then cs
-    else (Output.warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
+    else (warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
       ["interpret", "expand"])
   end