--- 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
--- 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;
--- 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;
--- 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;
--- 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
--- 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));