clarified PIDE markup;
authorwenzelm
Wed Jun 22 11:10:18 2016 +0200 (2016-06-22 ago)
changeset 63346c8366fb67538
parent 63345 70b2313f9c52
child 63347 e344dc82f6c2
clarified PIDE markup;
src/Pure/Isar/generic_target.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Wed Jun 22 10:42:53 2016 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Jun 22 11:10:18 2016 +0200
     1.3 @@ -242,7 +242,9 @@
     1.4  
     1.5      (*local definition*)
     1.6      val ([(lhs, (_, local_def))], lthy3) = lthy2
     1.7 -      |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))];
     1.8 +      |> Context_Position.set_visible false
     1.9 +      |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))]
    1.10 +      ||> Context_Position.restore_visible lthy2;
    1.11  
    1.12      (*result*)
    1.13      val def =
    1.14 @@ -329,8 +331,8 @@
    1.15    in
    1.16      lthy
    1.17      |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
    1.18 +    |> Context_Position.set_visible false
    1.19      |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
    1.20 -    |> Context_Position.set_visible false
    1.21      |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
    1.22      ||> Context_Position.restore_visible lthy
    1.23    end;