# HG changeset patch
# User wenzelm
# Date 1346347129 -7200
# Node ID 9c68e43502ce41e67220bc0ba106c372f4e47872
# Parent  72808e95687998470054404ef017c53bf69502d2
some support for registering forked proofs within Proof.state, using its bottom context;
tuned signature;

diff -r 72808e956879 -r 9c68e43502ce src/Pure/General/stack.ML
--- a/src/Pure/General/stack.ML	Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/General/stack.ML	Thu Aug 30 19:18:49 2012 +0200
@@ -10,7 +10,9 @@
   val level: 'a T -> int
   val init: 'a -> 'a T
   val top: 'a T -> 'a
+  val bottom: 'a T -> 'a
   val map_top: ('a -> 'a) -> 'a T -> 'a T
+  val map_bottom: ('a -> 'a) -> 'a T -> 'a T
   val map_all: ('a -> 'a) -> 'a T -> 'a T
   val push: 'a T -> 'a T
   val pop: 'a T -> 'a T      (*exception List.Empty*)
@@ -27,8 +29,16 @@
 
 fun top (x, _) = x;
 
+fun bottom (x, []) = x
+  | bottom (_, xs) = List.last xs;
+
 fun map_top f (x, xs) = (f x, xs);
 
+fun map_bottom f (x, []) = (f x, [])
+  | map_bottom f (x, rest) =
+      let val (ys, z) = split_last rest
+      in (x, ys @ [f z]) end;
+
 fun map_all f (x, xs) = (f x, map f xs);
 
 fun push (x, xs) = (x, x :: xs);
diff -r 72808e956879 -r 9c68e43502ce src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Aug 30 19:18:49 2012 +0200
@@ -111,6 +111,9 @@
     (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
+  val begin_proofs: state -> state
+  val register_proofs: thm list -> state -> state
+  val join_recent_proofs: state -> unit
   val schematic_goal: state -> bool
   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
@@ -168,8 +171,11 @@
 fun init ctxt =
   State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
 
-fun current (State st) = Stack.top st |> (fn Node node => node);
-fun map_current f (State st) = State (Stack.map_top (map_node f) st);
+fun top (State st) = Stack.top st |> (fn Node node => node);
+fun bottom (State st) = Stack.bottom st |> (fn Node node => node);
+
+fun map_top f (State st) = State (Stack.map_top (map_node f) st);
+fun map_bottom f (State st) = State (Stack.map_bottom (map_node f) st);
 fun map_all f (State st) = State (Stack.map_all (map_node f) st);
 
 
@@ -195,18 +201,21 @@
 
 (* context *)
 
-val context_of = #context o current;
+val context_of = #context o top;
 val theory_of = Proof_Context.theory_of o context_of;
 
 fun map_node_context f =
   map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun map_context f =
-  map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
+  map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun map_context_result f state =
   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
 
+fun map_context_bottom f =
+  map_bottom (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
+
 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun propagate_ml_env state = map_contexts
@@ -218,7 +227,7 @@
 
 (* facts *)
 
-val get_facts = #facts o current;
+val get_facts = #facts o top;
 
 fun the_facts state =
   (case get_facts state of SOME facts => facts
@@ -229,7 +238,7 @@
   | _ => error "Single theorem expected");
 
 fun put_facts facts =
-  map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
+  map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
   put_thms true (Auto_Bind.thisN, facts);
 
 val set_facts = put_facts o SOME;
@@ -249,8 +258,8 @@
 
 (* mode *)
 
-val get_mode = #mode o current;
-fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
+val get_mode = #mode o top;
+fun put_mode mode = map_top (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
 
 val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
 
@@ -274,7 +283,7 @@
 (* current goal *)
 
 fun current_goal state =
-  (case current state of
+  (case top state of
     {context, goal = SOME (Goal goal), ...} => (context, goal)
   | _ => error "No current goal");
 
@@ -285,7 +294,7 @@
     else state
   end;
 
-fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
+fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
 
 val set_goal = put_goal o SOME;
 val reset_goal = put_goal NONE;
@@ -338,7 +347,7 @@
 
 fun pretty_state nr state =
   let
-    val {context = ctxt, facts, mode, goal = _} = current state;
+    val {context = ctxt, facts, mode, goal = _} = top state;
     val verbose = Config.get ctxt Proof_Context.verbose;
 
     fun levels_up 0 = ""
@@ -1051,6 +1060,14 @@
 
 (** future proofs **)
 
+(* forked proofs *)
+
+val begin_proofs = map_context_bottom (Context.proof_map Thm.begin_proofs);
+val register_proofs = map_context_bottom o Context.proof_map o Thm.register_proofs;
+
+val join_recent_proofs = Thm.join_local_proofs o #context o bottom;
+
+
 (* relevant proof states *)
 
 fun is_schematic t =
diff -r 72808e956879 -r 9c68e43502ce src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 19:18:49 2012 +0200
@@ -426,11 +426,11 @@
 
 val global_theory_group =
   Sign.new_group #>
-  Thm.begin_recent_proofs #> Theory.checkpoint;
+  Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
 
 val local_theory_group =
   Local_Theory.new_group #>
-  Local_Theory.raw_theory (Thm.begin_recent_proofs #> Theory.checkpoint);
+  Local_Theory.raw_theory (Context.theory_map Thm.begin_proofs #> Theory.checkpoint);
 
 fun generic_theory f = transaction (fn _ =>
   (fn Theory (gthy, _) => Theory (f gthy, NONE)
diff -r 72808e956879 -r 9c68e43502ce src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 30 19:18:49 2012 +0200
@@ -357,7 +357,7 @@
   is_some (Exn.get_res (Exn.capture (fn () =>
     fst (fst (Command.memo_result (the (get_result node))))
     |> Toplevel.end_theory Position.none
-    |> Thm.join_all_proofs) ()));
+    |> Thm.join_theory_proofs) ()));
 
 fun stable_command exec =
   (case Exn.capture Command.memo_result exec of
diff -r 72808e956879 -r 9c68e43502ce src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Aug 30 19:18:49 2012 +0200
@@ -176,7 +176,7 @@
 local
 
 fun finish_thy ((thy, present, commit): result) =
-  (Thm.join_all_proofs thy; Future.join present; commit (); thy);
+  (Thm.join_theory_proofs thy; Future.join present; commit (); thy);
 
 val schedule_seq =
   Graph.schedule (fn deps => fn (_, task) =>
diff -r 72808e956879 -r 9c68e43502ce src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/global_theory.ML	Thu Aug 30 19:18:49 2012 +0200
@@ -124,7 +124,7 @@
 
 (* enter_thms *)
 
-fun register_proofs thms thy = (thms, Thm.register_proofs thms thy);
+fun register_proofs thms thy = (thms, Context.theory_map (Thm.register_proofs thms) thy);
 
 fun enter_thms pre_name post_name app_att (b, thms) thy =
   if Binding.is_empty b
diff -r 72808e956879 -r 9c68e43502ce src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/more_thm.ML	Thu Aug 30 19:18:49 2012 +0200
@@ -95,10 +95,11 @@
   val legacy_get_kind: thm -> string
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
-  val register_proofs: thm list -> theory -> theory
-  val begin_recent_proofs: theory -> theory
+  val register_proofs: thm list -> Context.generic -> Context.generic
+  val begin_proofs: Context.generic -> Context.generic
+  val join_local_proofs: Proof.context -> unit
   val join_recent_proofs: theory -> unit
-  val join_all_proofs: theory -> unit
+  val join_theory_proofs: theory -> unit
 end;
 
 structure Thm: THM =
@@ -470,7 +471,7 @@
 fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
 
 
-(* forked proofs within the context *)
+(* forked proofs *)
 
 type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
 
@@ -482,19 +483,20 @@
 
 fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
 
-structure Proofs = Theory_Data
+structure Proofs = Generic_Data
 (
-  type T = proofs * proofs;  (*recent proofs, all proofs of theory node*)
+  type T = proofs * proofs;  (*recent proofs since last begin, all proofs of theory node*)
   val empty = (empty_proofs, empty_proofs);
   fun extend _ = empty;
   fun merge _ = empty;
 );
 
+val begin_proofs = Proofs.map (apfst (K empty_proofs));
 val register_proofs = Proofs.map o pairself o add_proofs;
-val begin_recent_proofs = Proofs.map (apfst (K empty_proofs));
 
-val join_recent_proofs = force_proofs o #1 o Proofs.get;
-val join_all_proofs = force_proofs o #2 o Proofs.get;
+val join_local_proofs = force_proofs o #1 o Proofs.get o Context.Proof;
+val join_recent_proofs = force_proofs o #1 o Proofs.get o Context.Theory;
+val join_theory_proofs = force_proofs o #2 o Proofs.get o Context.Theory;
 
 
 open Thm;