--- a/src/Pure/Isar/toplevel.ML Sun Mar 08 17:37:18 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Sun Mar 08 20:31:01 2009 +0100
@@ -13,7 +13,6 @@
val proof_node: node -> ProofNode.T option
val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
val context_node: node -> Proof.context
- val presentation_context: node option -> xstring option -> Proof.context
type state
val toplevel: state
val is_toplevel: state -> bool
@@ -23,6 +22,7 @@
val previous_node_of: state -> node option
val node_of: state -> node
val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
+ val presentation_context_of: state -> xstring option -> Proof.context
val context_of: state -> Proof.context
val generic_theory_of: state -> generic_theory
val theory_of: state -> theory
@@ -68,7 +68,7 @@
val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
transition -> transition
val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
- val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
+ val present_local_theory: xstring option -> (state -> unit) -> transition -> transition
val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
transition -> transition
val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
@@ -76,7 +76,7 @@
val theory_to_proof: (theory -> Proof.state) -> transition -> transition
val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
val forget_proof: transition -> transition
- val present_proof: (node -> unit) -> transition -> transition
+ val present_proof: (state -> unit) -> transition -> transition
val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
@@ -145,15 +145,6 @@
val context_node = cases_node Context.proof_of Proof.context_of;
-fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
- | presentation_context (SOME node) NONE = context_node node
- | presentation_context (SOME node) (SOME loc) =
- loc_init loc (cases_node Context.theory_of Proof.theory_of node)
- | presentation_context NONE _ = raise UNDEF;
-
-fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
- | reset_presentation node = node;
-
(* datatype state *)
@@ -189,6 +180,13 @@
fun node_case f g state = cases_node f g (node_of state);
+fun presentation_context_of state opt_loc =
+ (case (try node_of state, opt_loc) of
+ (SOME (Theory (_, SOME ctxt)), NONE) => ctxt
+ | (SOME node, NONE) => context_node node
+ | (SOME node, SOME loc) => loc_init loc (cases_node Context.theory_of Proof.theory_of node)
+ | (NONE, _) => raise UNDEF);
+
val context_of = node_case Context.proof_of Proof.context_of;
val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
val theory_of = node_case Context.theory_of Proof.theory_of;
@@ -324,6 +322,9 @@
local
+fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
+ | reset_presentation node = node;
+
fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy)
| is_draft_theory _ = false;
@@ -338,7 +339,7 @@
in
-fun apply_transaction pos f (node, exit) =
+fun apply_transaction pos f g (node, exit) =
let
val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
val cont_node = reset_presentation node;
@@ -357,7 +358,7 @@
else (result, err);
in
(case err' of
- NONE => result'
+ NONE => tap g result'
| SOME exn => raise FAILURE (result', exn))
end;
@@ -371,7 +372,7 @@
Exit | (*formal exit of theory -- without committing*)
CommitExit | (*exit and commit final theory*)
Keep of bool -> state -> unit | (*peek at state*)
- Transaction of bool -> node -> node; (*node transaction*)
+ Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*)
local
@@ -383,8 +384,8 @@
(controlled_execution exit thy; toplevel)
| apply_tr int _ (Keep f) state =
controlled_execution (fn x => tap (f int) x) state
- | apply_tr int pos (Transaction f) (State (SOME state, _)) =
- apply_transaction pos (fn x => f int x) state
+ | apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) =
+ apply_transaction pos (fn x => f int x) g state
| apply_tr _ _ _ _ = raise UNDEF;
fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
@@ -470,7 +471,9 @@
fun init_theory name f exit = add_trans (Init (name, f, exit));
val exit = add_trans Exit;
val keep' = add_trans o Keep;
-fun transaction f = add_trans (Transaction f);
+
+fun present_transaction f g = add_trans (Transaction (f, g));
+fun transaction f = present_transaction f (K ());
fun keep f = add_trans (Keep (fn _ => f));
fun imperative f = keep (fn _ => f ());
@@ -510,19 +513,19 @@
local
-fun local_theory_presentation loc f g = transaction (fn int =>
+fun local_theory_presentation loc f = present_transaction (fn int =>
(fn Theory (gthy, _) =>
let
val finish = loc_finish loc gthy;
val lthy' = f int (loc_begin loc gthy);
in Theory (finish lthy', SOME lthy') end
- | _ => raise UNDEF) #> tap g);
+ | _ => raise UNDEF));
in
-fun local_theory' loc f = local_theory_presentation loc f (K I);
+fun local_theory' loc f = local_theory_presentation loc f (K ());
fun local_theory loc f = local_theory' loc (K f);
-fun present_local_theory loc g = local_theory_presentation loc (K I) g;
+fun present_local_theory loc = local_theory_presentation loc (K I);
end;
@@ -579,10 +582,10 @@
| SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
| _ => raise UNDEF));
-fun present_proof f = transaction (fn _ =>
+val present_proof = present_transaction (fn _ =>
(fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
| skip as SkipProof _ => skip
- | _ => raise UNDEF) #> tap f);
+ | _ => raise UNDEF));
fun proofs' f = transaction (fn int =>
(fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)
@@ -734,18 +737,18 @@
val future_proof = Proof.global_future_proof
(fn prf =>
Future.fork_pri ~1 (fn () =>
- let val (states, State (result_node, _)) =
+ let val (states, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
=> State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
|> fold_map command_result body_trs
||> command (end_tr |> set_print false);
- in (states, presentation_context (Option.map #1 result_node) NONE) end))
+ in (states, presentation_context_of result_state NONE) end))
#> (fn (states, ctxt) => States.put (SOME states) ctxt);
val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
val states =
- (case States.get (presentation_context (SOME (node_of st'')) NONE) of
+ (case States.get (presentation_context_of st'' NONE) of
NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
| SOME states => states);
val result = Lazy.lazy