# HG changeset patch # User wenzelm # Date 1236630373 -3600 # Node ID d7ac4b7aa5902e44633373e0d1d86aa62f095e2d # Parent b6212ae2165650e83e70bf1b84f02b888536390f simplified presentation_context_of; diff -r b6212ae21656 -r d7ac4b7aa590 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Mon Mar 09 21:25:33 2009 +0100 +++ b/src/Pure/Isar/toplevel.ML Mon Mar 09 21:26:13 2009 +0100 @@ -22,7 +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 presentation_context_of: state -> Proof.context val context_of: state -> Proof.context val generic_theory_of: state -> generic_theory val theory_of: state -> theory @@ -180,12 +180,11 @@ 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); +fun presentation_context_of state = + (case try node_of state of + SOME (Theory (_, SOME ctxt)) => ctxt + | SOME node => context_node 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); @@ -742,13 +741,13 @@ => 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_of result_state NONE) end)) + in (states, presentation_context_of result_state) 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_of st'' NONE) of + (case States.get (presentation_context_of st'') of NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr)) | SOME states => states); val result = Lazy.lazy diff -r b6212ae21656 -r d7ac4b7aa590 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon Mar 09 21:25:33 2009 +0100 +++ b/src/Pure/Thy/thy_output.ML Mon Mar 09 21:26:13 2009 +0100 @@ -105,7 +105,7 @@ fun antiquotation name scan out = add_commands [(name, fn src => fn state => let val (x, ctxt) = Args.context_syntax "document antiquotation" - scan src (Toplevel.presentation_context_of state NONE) + scan src (Toplevel.presentation_context_of state) in out {source = src, state = state, context = ctxt} x end)];