# HG changeset patch # User wenzelm # Date 1236540661 -3600 # Node ID e3d788b9dffb7c388fb081954ba01928ac16cf43 # Parent 790129514c2d1e3d8297ca8a0898eb8aaf800089 simplified presentation: built into transaction, pass state directly; diff -r 790129514c2d -r e3d788b9dffb src/Pure/Isar/toplevel.ML --- 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