src/Pure/Isar/locale.ML
changeset 36652 aace7a969410
parent 36651 97c3bbe63389
child 36653 8629ac3efb19
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Apr 27 22:27:22 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue May 04 19:57:55 2010 +0200
     1.3 @@ -409,9 +409,8 @@
     1.4  
     1.5  (* Diagnostic *)
     1.6  
     1.7 -fun print_registrations thy raw_name =
     1.8 +fun pretty_reg thy (name, morph) =
     1.9    let
    1.10 -    val name = intern thy raw_name;
    1.11      val name' = extern thy name;
    1.12      val ctxt = ProofContext.init thy;
    1.13      fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
    1.14 @@ -423,23 +422,22 @@
    1.15        else prt_term t;
    1.16      fun prt_inst ts =
    1.17        Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
    1.18 -    fun prt_reg (name, morph) =
    1.19 -      let
    1.20 -        val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
    1.21 -        val ts = instance_of thy name morph;
    1.22 -      in
    1.23 -        case qs of
    1.24 -           [] => prt_inst ts
    1.25 -         | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
    1.26 -             Pretty.brk 1, prt_inst ts]
    1.27 -      end;
    1.28 +
    1.29 +    val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
    1.30 +    val ts = instance_of thy name morph;
    1.31    in
    1.32 -    (case these_registrations thy name of
    1.33 -        [] => Pretty.str ("no interpretations")
    1.34 -      | regs => Pretty.big_list "interpretations:" (map prt_reg (rev regs)))
    1.35 -    |> Pretty.writeln
    1.36 +    case qs of
    1.37 +       [] => prt_inst ts
    1.38 +     | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
    1.39 +         Pretty.brk 1, prt_inst ts]
    1.40    end;
    1.41  
    1.42 +fun print_registrations thy raw_name =
    1.43 +  (case these_registrations thy (intern thy raw_name) of
    1.44 +      [] => Pretty.str ("no interpretations")
    1.45 +    | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
    1.46 +  |> Pretty.writeln;
    1.47 +
    1.48  
    1.49  (* Add and extend registrations *)
    1.50