simplified presentation_context_of;
authorwenzelm
Mon Mar 09 21:26:13 2009 +0100 (2009-03-09)
changeset 30398d7ac4b7aa590
parent 30397 b6212ae21656
child 30399 a4772a650b4e
simplified presentation_context_of;
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Mar 09 21:25:33 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 09 21:26:13 2009 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    val previous_node_of: state -> node option
     1.5    val node_of: state -> node
     1.6    val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
     1.7 -  val presentation_context_of: state -> xstring option -> Proof.context
     1.8 +  val presentation_context_of: state -> Proof.context
     1.9    val context_of: state -> Proof.context
    1.10    val generic_theory_of: state -> generic_theory
    1.11    val theory_of: state -> theory
    1.12 @@ -180,12 +180,11 @@
    1.13  
    1.14  fun node_case f g state = cases_node f g (node_of state);
    1.15  
    1.16 -fun presentation_context_of state opt_loc =
    1.17 -  (case (try node_of state, opt_loc) of
    1.18 -    (SOME (Theory (_, SOME ctxt)), NONE) => ctxt
    1.19 -  | (SOME node, NONE) => context_node node
    1.20 -  | (SOME node, SOME loc) => loc_init loc (cases_node Context.theory_of Proof.theory_of node)
    1.21 -  | (NONE, _) => raise UNDEF);
    1.22 +fun presentation_context_of state =
    1.23 +  (case try node_of state of
    1.24 +    SOME (Theory (_, SOME ctxt)) => ctxt
    1.25 +  | SOME node => context_node node
    1.26 +  | NONE => raise UNDEF);
    1.27  
    1.28  val context_of = node_case Context.proof_of Proof.context_of;
    1.29  val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
    1.30 @@ -742,13 +741,13 @@
    1.31                    => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
    1.32                  |> fold_map command_result body_trs
    1.33                  ||> command (end_tr |> set_print false);
    1.34 -              in (states, presentation_context_of result_state NONE) end))
    1.35 +              in (states, presentation_context_of result_state) end))
    1.36            #> (fn (states, ctxt) => States.put (SOME states) ctxt);
    1.37  
    1.38          val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
    1.39  
    1.40          val states =
    1.41 -          (case States.get (presentation_context_of st'' NONE) of
    1.42 +          (case States.get (presentation_context_of st'') of
    1.43              NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
    1.44            | SOME states => states);
    1.45          val result = Lazy.lazy
     2.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 21:25:33 2009 +0100
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 21:26:13 2009 +0100
     2.3 @@ -105,7 +105,7 @@
     2.4  
     2.5  fun antiquotation name scan out = add_commands [(name, fn src => fn state =>
     2.6    let val (x, ctxt) = Args.context_syntax "document antiquotation"
     2.7 -    scan src (Toplevel.presentation_context_of state NONE)
     2.8 +    scan src (Toplevel.presentation_context_of state)
     2.9    in out {source = src, state = state, context = ctxt} x end)];
    2.10  
    2.11