print_state_context: local theory context, not proof context;
authorwenzelm
Mon Oct 01 15:14:57 2007 +0200 (2007-10-01)
changeset 247956f5cb7885fd7
parent 24794 5740b01a1553
child 24796 529e458f84d2
print_state_context: local theory context, not proof context;
context_position: cover Theory case as well (requires additional checkpoint);
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Oct 01 15:14:56 2007 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Oct 01 15:14:57 2007 +0200
     1.3 @@ -210,9 +210,11 @@
     1.4  val pretty_context = LocalTheory.pretty o Context.cases (loc_init NONE) I;
     1.5  
     1.6  fun print_state_context state =
     1.7 -  (case try (node_case I (Context.Proof o Proof.context_of)) state of
     1.8 +  (case try node_of state of
     1.9      NONE => []
    1.10 -  | SOME gthy => pretty_context gthy)
    1.11 +  | SOME (Theory (gthy, _)) => pretty_context gthy
    1.12 +  | SOME (Proof (_, (_, gthy))) => pretty_context gthy
    1.13 +  | SOME (SkipProof (_, (gthy, _))) => pretty_context gthy)
    1.14    |> Pretty.chunks |> Pretty.writeln;
    1.15  
    1.16  fun print_state prf_only state =
    1.17 @@ -340,10 +342,9 @@
    1.18      | node => node);
    1.19  
    1.20  fun context_position pos = History.map_current
    1.21 -  (fn Theory (Context.Proof lthy, ctxt) =>
    1.22 -        Theory (Context.Proof (ContextPosition.put pos lthy), ctxt)
    1.23 +  (fn Theory (gthy, ctxt) => Theory (ContextPosition.put pos gthy, ctxt)
    1.24      | Proof (prf, x) =>
    1.25 -        Proof (ProofHistory.map_current (Proof.map_context (ContextPosition.put pos)) prf, x)
    1.26 +        Proof (ProofHistory.map_current (Proof.map_context (ContextPosition.put_ctxt pos)) prf, x)
    1.27      | node => node);
    1.28  
    1.29  fun return (result, NONE) = result
    1.30 @@ -362,6 +363,7 @@
    1.31      val (result, err) =
    1.32        cont_node
    1.33        |> context_position pos
    1.34 +      |> map_theory Theory.checkpoint
    1.35        |> (f
    1.36            |> (if hist then History.apply' (History.current back_node) else History.map_current)
    1.37            |> controlled_execution)
    1.38 @@ -550,7 +552,7 @@
    1.39          let
    1.40            val pos = ContextPosition.get (Context.proof_of gthy);
    1.41            val finish = loc_finish loc gthy;
    1.42 -          val lthy' = f (ContextPosition.put pos (loc_begin loc gthy));
    1.43 +          val lthy' = f (ContextPosition.put_ctxt pos (loc_begin loc gthy));
    1.44          in Theory (finish lthy', SOME lthy') end
    1.45      | _ => raise UNDEF) #> tap (g int));
    1.46  
    1.47 @@ -565,7 +567,7 @@
    1.48  (* proof transitions *)
    1.49  
    1.50  fun end_proof f = map_current (fn int =>
    1.51 -  (fn Proof (prf, (finish, orig_gthy)) =>
    1.52 +  (fn Proof (prf, (finish, _)) =>
    1.53          let val state = ProofHistory.current prf in
    1.54            if can (Proof.assert_bottom true) state then
    1.55              let
    1.56 @@ -600,7 +602,8 @@
    1.57  
    1.58  fun local_theory_to_proof' loc f = begin_proof
    1.59    (fn int => fn gthy =>
    1.60 -    f int (ContextPosition.put (ContextPosition.get (Context.proof_of gthy)) (loc_begin loc gthy)))
    1.61 +    f int (ContextPosition.put_ctxt (ContextPosition.get (Context.proof_of gthy))
    1.62 +      (loc_begin loc gthy)))
    1.63    (loc_finish loc);
    1.64  
    1.65  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);