# HG changeset patch # User wenzelm # Date 1346354584 -7200 # Node ID 8686c36fa27dd08248f1f170132ab4c726de6c39 # Parent 9c68e43502ce41e67220bc0ba106c372f4e47872 refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs; diff -r 9c68e43502ce -r 8686c36fa27d src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Aug 30 19:18:49 2012 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Aug 30 21:23:04 2012 +0200 @@ -265,7 +265,7 @@ (* global endings *) fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true))); -val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof; +val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof; val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof); val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof); val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; diff -r 9c68e43502ce -r 8686c36fa27d src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Aug 30 19:18:49 2012 +0200 +++ b/src/Pure/Isar/proof.ML Thu Aug 30 21:23:04 2012 +0200 @@ -1137,19 +1137,21 @@ local -fun future_terminal_proof proof1 proof2 meths int state = - if int orelse is_relevant state orelse not (Goal.local_future_enabled ()) - then proof1 meths state - else snd (proof2 (fn state' => - Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state); +fun future_terminal_proof n proof1 proof2 meths int state = + if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int) + andalso not (is_relevant state) + then + snd (proof2 (fn state' => + Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state) + else proof1 meths state; in fun local_future_terminal_proof x = - future_terminal_proof local_terminal_proof local_future_proof x; + future_terminal_proof 2 local_terminal_proof local_future_proof x; fun global_future_terminal_proof x = - future_terminal_proof global_terminal_proof global_future_proof x; + future_terminal_proof 3 global_terminal_proof global_future_proof x; end; diff -r 9c68e43502ce -r 8686c36fa27d src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Aug 30 19:18:49 2012 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Aug 30 21:23:04 2012 +0200 @@ -53,9 +53,10 @@ val ignored: Position.T -> transition val malformed: Position.T -> string -> transition val is_malformed: transition -> bool - val theory: (theory -> theory) -> transition -> transition + val join_recent_proofs: state -> unit val generic_theory: (generic_theory -> generic_theory) -> transition -> transition val theory': (bool -> theory -> theory) -> transition -> transition + val theory: (theory -> theory) -> transition -> transition val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition val end_local_theory: transition -> transition val open_target: (generic_theory -> local_theory) -> transition -> transition @@ -422,15 +423,21 @@ val unknown_context = imperative (fn () => warning "Unknown context"); -(* theory transitions *) +(* forked proofs *) + +val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint; +val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy); -val global_theory_group = - Sign.new_group #> - Context.theory_map Thm.begin_proofs #> Theory.checkpoint; +fun join_recent_proofs st = + (case try proof_of st of + SOME prf => Proof.join_recent_proofs prf + | NONE => + (case try theory_of st of + SOME thy => Thm.join_recent_proofs thy + | NONE => ())); -val local_theory_group = - Local_Theory.new_group #> - Local_Theory.raw_theory (Context.theory_map Thm.begin_proofs #> Theory.checkpoint); + +(* theory transitions *) fun generic_theory f = transaction (fn _ => (fn Theory (gthy, _) => Theory (f gthy, NONE) @@ -439,7 +446,8 @@ fun theory' f = transaction (fn int => (fn Theory (Context.Theory thy, _) => let val thy' = thy - |> global_theory_group + |> Sign.new_group + |> Theory.checkpoint |> f int |> Sign.reset_group; in Theory (Context.Theory thy', NONE) end @@ -478,9 +486,11 @@ fun local_theory_presentation loc f = present_transaction (fn int => (fn Theory (gthy, _) => let - val (finish, lthy) = loc_begin loc gthy; + val (finish, lthy) = gthy + |> begin_proofs + |> loc_begin loc; val lthy' = lthy - |> local_theory_group + |> Local_Theory.new_group |> f int |> Local_Theory.reset_group; in Theory (finish lthy', SOME lthy') end @@ -534,15 +544,19 @@ fun local_theory_to_proof' loc f = begin_proof (fn int => fn gthy => - let val (finish, lthy) = loc_begin loc gthy - in (finish o Local_Theory.reset_group, f int (local_theory_group lthy)) end); + let val (finish, lthy) = gthy + |> begin_proofs + |> loc_begin loc; + in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end); fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); fun theory_to_proof f = begin_proof (fn _ => fn gthy => (Context.Theory o Sign.reset_group o Proof_Context.theory_of, - (case gthy of Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))); + (case begin_proofs gthy of + Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) + | _ => raise UNDEF))); end; @@ -552,12 +566,12 @@ | _ => raise UNDEF)); val present_proof = present_transaction (fn _ => - (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) + (fn Proof (prf, x) => Proof (Proof_Node.apply Proof.begin_proofs prf, x) | skip as SkipProof _ => skip | _ => raise UNDEF)); fun proofs' f = transaction (fn int => - (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) + (fn Proof (prf, x) => Proof (Proof_Node.applys (f int o Proof.begin_proofs) prf, x) | skip as SkipProof _ => skip | _ => raise UNDEF)); diff -r 9c68e43502ce -r 8686c36fa27d src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Aug 30 19:18:49 2012 +0200 +++ b/src/Pure/PIDE/document.ML Thu Aug 30 21:23:04 2012 +0200 @@ -362,10 +362,7 @@ fun stable_command exec = (case Exn.capture Command.memo_result exec of Exn.Exn exn => not (Exn.is_interrupt exn) - | Exn.Res ((st, _), _) => - (case try Toplevel.theory_of st of - NONE => true - | SOME thy => is_some (Exn.get_res (Exn.capture Thm.join_recent_proofs thy)))); + | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st))); fun make_required nodes = let diff -r 9c68e43502ce -r 8686c36fa27d src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Aug 30 19:18:49 2012 +0200 +++ b/src/Pure/goal.ML Thu Aug 30 21:23:04 2012 +0200 @@ -26,8 +26,9 @@ val norm_result: thm -> thm val fork_name: string -> (unit -> 'a) -> 'a future val fork: (unit -> 'a) -> 'a future + val future_enabled_level: int -> bool val future_enabled: unit -> bool - val local_future_enabled: unit -> bool + val future_enabled_nested: int -> bool val future_result: Proof.context -> thm future -> term -> thm val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm val prove_multi: Proof.context -> string list -> term list -> term list -> @@ -155,12 +156,14 @@ val parallel_proofs = Unsynchronized.ref 1; val parallel_proofs_threshold = Unsynchronized.ref 50; -fun future_enabled () = - Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso +fun future_enabled_level n = + Multithreading.enabled () andalso ! parallel_proofs >= n andalso is_some (Future.worker_task ()); -fun local_future_enabled () = - future_enabled () andalso ! parallel_proofs >= 2 andalso +fun future_enabled () = future_enabled_level 1; + +fun future_enabled_nested n = + future_enabled_level n andalso Synchronized.value forked_proofs < ! parallel_proofs_threshold * Multithreading.max_threads_value ();