# HG changeset patch
# User wenzelm
# Date 1334091924 -7200
# Node ID c0e8c98ee50e4ca76a7ac600269eb41ab9d62164
# Parent  d53e422e06f2dff7998918b3676dc02bf24cb47d# Parent  9679bab23f93d2350b289d0cf33b5d55223f3ecc
merged

diff -r d53e422e06f2 -r c0e8c98ee50e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 10 16:10:50 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 10 23:05:24 2012 +0200
@@ -464,7 +464,7 @@
       (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
 val _ =
-  Outer_Syntax.command ("sublocale", Keyword.thy_goal)
+  Outer_Syntax.command ("sublocale", Keyword.thy_schematic_goal)
     "prove sublocale relation between a locale and a locale expression"
     (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
       parse_interpretation_arguments false
@@ -472,7 +472,7 @@
           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
 
 val _ =
-  Outer_Syntax.command ("interpretation", Keyword.thy_goal)
+  Outer_Syntax.command ("interpretation", Keyword.thy_schematic_goal)
     "prove interpretation of locale expression in theory"
     (parse_interpretation_arguments true
       >> (fn (expr, equations) => Toplevel.print o
diff -r d53e422e06f2 -r c0e8c98ee50e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Apr 10 16:10:50 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Apr 10 23:05:24 2012 +0200
@@ -296,7 +296,8 @@
     val (tr, proper_head) = read head |>> Toplevel.modify_init init;
     val proof_trs = map read proof |> filter #2 |> map #1;
   in
-    if proper_head andalso proper_proof then [(tr, proof_trs)]
+    if proper_head andalso proper_proof andalso
+      not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   end;
 
diff -r d53e422e06f2 -r c0e8c98ee50e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 10 16:10:50 2012 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Apr 10 23:05:24 2012 +0200
@@ -112,11 +112,8 @@
   val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
-  val is_relevant: state -> bool
-  val local_future_proof: (state -> ('a * state) Future.future) ->
-    state -> 'a Future.future * state
-  val global_future_proof: (state -> ('a * Proof.context) Future.future) ->
-    state -> 'a Future.future * context
+  val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
+  val global_future_proof: (state -> ('a * Proof.context) future) -> state -> 'a future * context
   val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
   val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
 end;
diff -r d53e422e06f2 -r c0e8c98ee50e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Apr 10 16:10:50 2012 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 10 23:05:24 2012 +0200
@@ -659,55 +659,43 @@
 
 fun command_result tr st =
   let val st' = command tr st
-  in (st', st') end;
+  in ((tr, st'), st') end;
 
 
 (* scheduled proof result *)
 
-structure States = Proof_Data
+structure Result = Proof_Data
 (
-  type T = state list future option;
-  fun init _ = NONE;
+  type T = (transition * state) list future;
+  val empty: T = Future.value [];
+  fun init _ = empty;
 );
 
 fun proof_result immediate (tr, proof_trs) st =
-  let val st' = command tr st in
-    if immediate orelse
-      null proof_trs orelse
-      Keyword.is_schematic_goal (name_of tr) orelse
-      exists (Keyword.is_qed_global o name_of) proof_trs orelse
-      not (can proof_of st') orelse
-      Proof.is_relevant (proof_of st')
-    then
-      let val (states, st'') = fold_map command_result proof_trs st'
-      in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end
-    else
-      let
-        val (body_trs, end_tr) = split_last proof_trs;
-        val finish = Context.Theory o Proof_Context.theory_of;
+  if immediate orelse null proof_trs
+  then fold_map command_result (tr :: proof_trs) st |>> Future.value
+  else
+    let
+      val st' = command tr st;
+      val (body_trs, end_tr) = split_last proof_trs;
+      val finish = Context.Theory o Proof_Context.theory_of;
 
-        val future_proof = Proof.global_future_proof
-          (fn prf =>
-            Goal.fork_name "Toplevel.future_proof"
-              (fn () =>
-                let val (states, result_state) =
-                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
-                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
-                  |> fold_map command_result body_trs
-                  ||> command (end_tr |> set_print false);
-                in (states, presentation_context_of result_state) end))
-          #> (fn (states, ctxt) => States.put (SOME states) ctxt);
+      val future_proof = Proof.global_future_proof
+        (fn prf =>
+          Goal.fork_name "Toplevel.future_proof"
+            (fn () =>
+              let val (result, result_state) =
+                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
+                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
+                |> fold_map command_result body_trs ||> command end_tr;
+              in (result, presentation_context_of result_state) end))
+        #-> Result.put;
 
-        val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
+      val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
+      val result =
+        Result.get (presentation_context_of st'')
+        |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
 
-        val states =
-          (case States.get (presentation_context_of st'') of
-            NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
-          | SOME states => states);
-        val result = states
-          |> Future.map (fn sts => (tr, st') :: (body_trs ~~ sts) @ [(end_tr, st'')]);
-
-      in (result, st'') end
-  end;
+    in (result, st'') end;
 
 end;
diff -r d53e422e06f2 -r c0e8c98ee50e src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Apr 10 16:10:50 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Apr 10 23:05:24 2012 +0200
@@ -312,7 +312,7 @@
             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}
+                  deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
                 (fn () =>
                   iterate_entries (fn ((_, id), opt_exec) => fn () =>
                     (case opt_exec of
diff -r d53e422e06f2 -r c0e8c98ee50e src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Apr 10 16:10:50 2012 +0100
+++ b/src/Pure/goal.ML	Tue Apr 10 23:05:24 2012 +0200
@@ -125,7 +125,7 @@
       val _ = forked 1;
       val future =
         (singleton o Future.forks)
-          {name = name, group = NONE, deps = [], pri = 0, interrupts = false}
+          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
           (fn () =>
             Exn.release
               (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));