src/Pure/Isar/toplevel.ML

 *)
 
 signature TOPLEVEL =
 sig
   exception UNDEF
+  type generic_theory
   type node
-  val theory_node: node -> theory option
+  val theory_node: node -> generic_theory option
   val proof_node: node -> ProofHistory.T option
-  val cases_node: (theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
-  val body_context_node: node option -> xstring option -> Proof.context
+  val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
+  val presentation_context: node option -> xstring option -> Proof.context
   type state
   val toplevel: state
   val is_toplevel: state -> bool
   val is_theory: state -> bool
   val is_proof: state -> bool
   val level: state -> int
   val assert: bool -> unit
   val node_history_of: state -> node History.T
   val node_of: state -> node
-  val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
+  val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
   val context_of: state -> Context.generic
   val theory_of: state -> theory
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
   val enter_forward_proof: state -> Proof.state

   exception TERMINATE
   exception RESTART
   val exn_message: exn -> string
   val program: (unit -> 'a) -> 'a
   val checkpoint: state -> state
-  val copy: state -> state
   type transition
   val undo_limit: bool -> int option
   val empty: transition
   val name_of: transition -> string
   val source_of: transition -> OuterLex.token list option

   val imperative: (unit -> unit) -> transition -> transition
   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
     -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
-  val theory_context: (theory -> Proof.context * theory) -> transition -> transition
-  val local_theory: xstring option -> (local_theory -> local_theory) ->
-    transition -> transition
+  val exit_local_theory: transition -> transition
+  val begin_local_theory: bool -> (theory -> string * local_theory) -> transition -> transition
+  val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
+  val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val proof: (Proof.state -> Proof.state) -> transition -> transition
   val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
   val actual_proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val skip_proof: (int History.T -> int History.T) -> transition -> transition
-  val proof_to_theory: (Proof.state -> theory) -> transition -> transition
-  val proof_to_theory': (bool -> Proof.state -> theory) -> transition -> transition
-  val proof_to_theory_context: (bool -> Proof.state -> Proof.context * theory)
-    -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
   val forget_proof: transition -> transition
-  val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
+  val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
   val present_proof: (bool -> node -> unit) -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
   val apply: bool -> transition -> state -> (state * (exn * string) option) option

 end;
 
 structure Toplevel: TOPLEVEL =
 struct
 
-
 (** toplevel state **)
 
 exception UNDEF;
 
 
 (* datatype state *)
 
+type generic_theory = Context.generic;    (*theory or local_theory*)
+
 datatype node =
-  Theory of theory * Proof.context option |        (*theory with optional body context*)
-  Proof of ProofHistory.T * theory |               (*history of proof states, original theory*)
-  SkipProof of (int History.T * theory) * theory;
+  Theory of generic_theory * Proof.context option | (*theory with presentation context*)
+  Proof of ProofHistory.T * generic_theory |        (*history of proof states, original theory*)
+  SkipProof of (int History.T * generic_theory) * generic_theory;
     (*history of proof depths, resulting theory, original theory*)
 
-val theory_node = fn Theory (thy, _) => SOME thy | _ => NONE;
+val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
 val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
 
-fun cases_node f _ (Theory (thy, _)) = f thy
+fun cases_node f _ (Theory (gthy, _)) = f gthy
   | cases_node _ g (Proof (prf, _)) = g (ProofHistory.current prf)
-  | cases_node f _ (SkipProof ((_, thy), _)) = f thy;
-
-fun body_context_node (SOME (Theory (_, SOME ctxt))) NONE = ctxt
-  | body_context_node (SOME node) loc =
-      node |> cases_node (TheoryTarget.init loc)
-       (if is_some loc then TheoryTarget.init loc o Proof.theory_of
-        else Proof.context_of)
-  | body_context_node NONE _ = raise UNDEF;
+  | cases_node f _ (SkipProof ((_, gthy), _)) = f gthy;
+
+fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
+  | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node
+  | presentation_context (SOME node) (SOME loc) =
+      TheoryTarget.init (SOME loc) (cases_node Context.theory_of Proof.theory_of node)
+  | presentation_context NONE _ = raise UNDEF;
 
 datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
 
 val toplevel = State NONE;
 

   | is_toplevel _ = false;
 
 fun level (State NONE) = 0
   | level (State (SOME (node, _))) =
       (case History.current node of
-        Theory _ => 0
-      | Proof (prf, _) => Proof.level (ProofHistory.current prf)
-      | SkipProof ((h, _), _) => History.current h + 1);    (*different notion of proof depth!*)
+        Theory (Context.Theory _, _) => 0
+      | Theory (Context.Proof _, _) => 1
+      | Proof (prf, _) => Proof.level (ProofHistory.current prf) + 1
+      | SkipProof ((h, _), _) => History.current h + 2);   (*different notion of proof depth!*)
 
 fun str_of_state (State NONE) = "at top level"
   | str_of_state (State (SOME (node, _))) =
       (case History.current node of
-        Theory _ => "in theory mode"
+        Theory (Context.Theory _, _) => "in theory mode"
+      | Theory (Context.Proof _, _) => "in local theory mode"
       | Proof _ => "in proof mode"
       | SkipProof _ => "in skipped proof mode");
 
 
 (* top node *)

 fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
 fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
 
 fun node_case f g state = cases_node f g (node_of state);
 
-val context_of = node_case Context.Theory (Context.Proof o Proof.context_of);
-val theory_of = node_case I Proof.theory_of;
+val context_of = node_case I (Context.Proof o Proof.context_of);
+val theory_of = node_case Context.theory_of Proof.theory_of;
 val proof_of = node_case (fn _ => raise UNDEF) I;
 
 fun proof_position_of state =
   (case node_of state of
     Proof (prf, _) => ProofHistory.position prf
   | _ => raise UNDEF);
 
-val enter_forward_proof = node_case (Proof.init o ProofContext.init) Proof.enter_forward;
+val enter_forward_proof = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
 
 
 (* prompt state *)
 
 fun prompt_state_default (State _) = Source.default_prompt;

 fun prompt_state state = ! prompt_state_fn state;
 
 
 (* print state *)
 
-fun pretty_context thy = [Pretty.block
-  [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
-    Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
+val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I;
 
 fun pretty_state_context state =
-  (case try theory_of state of NONE => []
-  | SOME thy => pretty_context thy);
-
-fun pretty_node prf_only (Theory (thy, _)) = if prf_only then [] else pretty_context thy
+  (case try context_of state of NONE => []
+  | SOME gthy => pretty_context gthy);
+
+fun pretty_node prf_only (Theory (gthy, _)) = if prf_only then [] else pretty_context gthy
   | pretty_node _ (Proof (prf, _)) =
       Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
   | pretty_node _ (SkipProof ((h, _), _)) =
       [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))];
 

 
 fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
 
 val stale_theory = ERROR "Stale theory encountered after succesful execution!";
 
-fun checkpoint_node (Theory (thy, _)) = Theory (Theory.checkpoint thy, NONE)
+fun checkpoint_node (Theory (gthy, _)) = Theory
+      (Context.mapping Theory.checkpoint (LocalTheory.raw_theory Theory.checkpoint) gthy, NONE)
   | checkpoint_node node = node;
-
-fun copy_node (Theory (thy, _)) = Theory (Theory.copy thy, NONE)
-  | copy_node node = node;
 
 fun return (result, NONE) = result
   | return (result, SOME exn) = raise FAILURE (result, exn);
 
 in
 
 fun transaction hist f (node, term) =
   let
     val cont_node = History.map checkpoint_node node;
-    val back_node = History.map copy_node cont_node;
+    val back_node = History.map checkpoint_node cont_node;
     fun state nd = State (SOME (nd, term));
     fun normal_state nd = (state nd, NONE);
     fun error_state nd exn = (state nd, SOME exn);
 
     val (result, err) =
       cont_node
       |> (f
-          |> (if hist then History.apply_copy copy_node else History.map)
+          |> (if hist then History.apply_copy checkpoint_node else History.map)
           |> controlled_execution)
       |> normal_state
       handle exn => error_state cont_node exn;
   in
     if is_stale result

 
 fun mapping f (State (SOME (node, term))) = State (SOME (History.map f node, term))
   | mapping _ state = state;
 
 val checkpoint = mapping checkpoint_node;
-val copy = mapping copy_node;
 
 end;
 
 
 (* primitive transitions *)

 
 fun keep f = add_trans (Keep (fn _ => f));
 fun imperative f = keep (fn _ => f ());
 
 fun init_theory f exit kill =
-  init (fn int => Theory (f int, NONE))
-    (fn Theory (thy, _) => exit thy | _ => raise UNDEF)
-    (fn Theory (thy, _) => kill thy | _ => raise UNDEF);
+  init (fn int => Theory (Context.Theory (f int), NONE))
+    (fn Theory (Context.Theory thy, _) => exit thy | _ => raise UNDEF)
+    (fn Theory (Context.Theory thy, _) => kill thy | _ => raise UNDEF);
 
 
 (* typed transitions *)
 
-fun theory f = app_current
-  (K (fn Theory (thy, _) => Theory (f thy, NONE) | _ => raise UNDEF));
-
 fun theory' f = app_current (fn int =>
-  (fn Theory (thy, _) => Theory (f int thy, NONE) | _ => raise UNDEF));
-
-fun theory_context f = app_current
-  (K (fn Theory (thy, _) => Theory (swap (apfst SOME (f thy))) | _ => raise UNDEF));
-
-fun local_theory loc f = theory_context (TheoryTarget.mapping loc f);
+  (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
+    | _ => raise UNDEF));
+
+fun theory f = theory' (K f);
+
+val exit_local_theory = app_current (fn _ =>
+  (fn Theory (Context.Proof lthy, _) =>
+      let val (ctxt', thy') = TheoryTarget.exit lthy
+      in Theory (Context.Theory thy', SOME ctxt') end
+    | _ => raise UNDEF));
+
+fun begin_local_theory begin f = app_current (fn _ =>
+  (fn Theory (Context.Theory thy, _) =>
+        let
+          val lthy = thy |> f |-> TheoryTarget.begin;
+          val (ctxt, gthy) =
+            if begin then (lthy, Context.Proof lthy)
+            else lthy |> TheoryTarget.exit ||> Context.Theory;
+        in Theory (gthy, SOME ctxt) end
+    | _ => raise UNDEF));
+
+fun local_theory_presentation loc f g = app_current (fn int =>
+  (fn Theory (Context.Theory thy, _) =>
+        let val (ctxt', thy') = TheoryTarget.mapping loc f thy
+        in Theory (Context.Theory thy', SOME ctxt') end
+    | Theory (Context.Proof lthy, _) =>
+        let val (ctxt', lthy') =
+          if is_none loc then f lthy |> (fn lthy' => (lthy', LocalTheory.reinit lthy'))
+          else lthy |> LocalTheory.raw_theory_result (TheoryTarget.mapping loc f)
+        in Theory (Context.Proof lthy', SOME ctxt') end
+    | _ => raise UNDEF) #> tap (g int));
+
+fun local_theory loc f = local_theory_presentation loc f (K I);
+fun present_local_theory loc g = local_theory_presentation loc I g;
 
 fun theory_to_proof f = app_current (fn int =>
-  (fn Theory (thy, _) =>
+  (fn Theory (gthy as Context.Theory thy, _) =>
     let
       val prf = f thy;
       val schematic = Proof.schematic_goal prf;
     in
       if ! skip_proofs andalso schematic then
         warning "Cannot skip proof of schematic goal statement"
       else ();
       if ! skip_proofs andalso not schematic then
         SkipProof ((History.init (undo_limit int) 0,
-          ProofContext.theory_of (Proof.global_skip_proof int prf)), thy)
-      else Proof (ProofHistory.init (undo_limit int) prf, thy)
+          Context.Theory (ProofContext.theory_of (Proof.global_skip_proof int prf))), gthy)
+      else Proof (ProofHistory.init (undo_limit int) prf, gthy)
     end
   | _ => raise UNDEF));
 
 fun proofs' f = map_current (fn int =>
-  (fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy)
-    | SkipProof ((h, thy), orig_thy) => SkipProof ((History.apply I h, thy), orig_thy)
+  (fn Proof (prf, orig_gthy) => Proof (ProofHistory.applys (f int) prf, orig_gthy)
+    | SkipProof ((h, gthy), orig_gthy) => SkipProof ((History.apply I h, gthy), orig_gthy)
     | _ => raise UNDEF));
 
 fun proof' f = proofs' (Seq.single oo f);
 val proofs = proofs' o K;
 val proof = proof' o K;
 
 fun actual_proof f = map_current (fn _ =>
-  (fn Proof (prf, orig_thy) => Proof (f prf, orig_thy) | _ => raise UNDEF));
+  (fn Proof (prf, orig_gthy) => Proof (f prf, orig_gthy)
+    | _ => raise UNDEF));
 
 fun skip_proof f = map_current (fn _ =>
-  (fn SkipProof ((h, thy), orig_thy) => SkipProof ((f h, thy), orig_thy) | _ => raise UNDEF));
-
-fun end_proof f = map_current (fn int =>
-  (fn Proof (prf, _) => Theory (f int (ProofHistory.current prf))
-    | SkipProof ((h, thy), _) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF
+  (fn SkipProof ((h, gthy), orig_gthy) => SkipProof ((f h, gthy), orig_gthy)
     | _ => raise UNDEF));
-
-val forget_proof = map_current (fn _ =>
-  (fn Proof (_, orig_thy) => Theory (orig_thy, NONE)
-    | SkipProof (_, orig_thy) => Theory (orig_thy, NONE)
-    | _ => raise UNDEF));
-
-fun proof_to_theory' f = end_proof (rpair NONE oo f);
-fun proof_to_theory f = proof_to_theory' (K f);
-fun proof_to_theory_context f = end_proof ((swap o apfst SOME) oo f);
 
 fun skip_proof_to_theory p = map_current (fn _ =>
   (fn SkipProof ((h, thy), _) =>
     if p (History.current h) then Theory (thy, NONE)
     else raise UNDEF
   | _ => raise UNDEF));
 
-fun present_local_theory loc f = app_current (fn int =>
-  (fn Theory (thy, _) => Theory (swap (apfst SOME (TheoryTarget.mapping loc I thy)))
-    | _ => raise UNDEF) #> tap (f int));
+val forget_proof = map_current (fn _ =>
+  (fn Proof (_, orig_gthy) => Theory (orig_gthy, NONE)
+    | SkipProof (_, orig_gthy) => Theory (orig_gthy, NONE)
+    | _ => raise UNDEF));
+
+fun end_proof f = map_current (fn int =>
+  (fn Proof (prf, orig_gthy) =>
+        let val state = ProofHistory.current prf in
+          if can (Proof.assert_bottom true) state then
+            let
+              val ctxt' = f int state;
+              val gthy' =
+                if can Context.the_theory orig_gthy
+                then Context.Theory (ProofContext.theory_of ctxt')
+                else Context.Proof (LocalTheory.reinit ctxt');
+            in Theory (gthy', SOME ctxt') end
+          else raise UNDEF
+        end
+    | SkipProof ((h, gthy), _) =>
+        if History.current h = 0 then Theory (gthy, NONE) else raise UNDEF
+    | _ => raise UNDEF));
 
 fun present_proof f = map_current (fn int =>
   (fn node as Proof _ => node | _ => raise UNDEF) #> tap (f int));
 
 val unknown_theory = imperative (fn () => warning "Unknown theory context");