# HG changeset patch
# User wenzelm
# Date 1334086265 -7200
# Node ID df8fc0567a3d472d08ff5e8238da7af905be02c2
# Parent  c486ac962b8999ce3ebe0a3e56a14e25f7db29b5
static relevance of proof via syntax keywords;

diff -r c486ac962b89 -r df8fc0567a3d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 10 21:31:05 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 c486ac962b89 -r df8fc0567a3d src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Apr 10 21:31:05 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 c486ac962b89 -r df8fc0567a3d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 10 21:31:05 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 c486ac962b89 -r df8fc0567a3d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 10 21:31:05 2012 +0200
@@ -672,12 +672,7 @@
 
 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')
+    if immediate orelse null proof_trs orelse not (can 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