target update: invisible context position avoids duplication of reports etc.;
authorwenzelm
Mon Sep 29 14:41:24 2008 +0200 (2008-09-29 ago)
changeset 28406daeb21fec18f
parent 28405 000dee6d5d80
child 28407 f9db1da584ac
target update: invisible context position avoids duplication of reports etc.;
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Mon Sep 29 14:41:23 2008 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Sep 29 14:41:24 2008 +0200
     1.3 @@ -154,7 +154,10 @@
     1.4  
     1.5  fun target_result f lthy =
     1.6    let
     1.7 -    val (res, ctxt') = f (target_of lthy);
     1.8 +    val (res, ctxt') = target_of lthy
     1.9 +      |> ContextPosition.set_visible false
    1.10 +      |> f
    1.11 +      ||> ContextPosition.restore_visible lthy;
    1.12      val thy' = ProofContext.theory_of ctxt';
    1.13      val lthy' = lthy
    1.14        |> map_target (K ctxt')