src/Pure/General/binding.ML
changeset 45666 d83797ef0d2d
parent 43839 93f6f24010c2
child 46897 ec793befc232
equal deleted inserted replaced
45665:129db1416717 45666:d83797ef0d2d
   120 
   120 
   121 
   121 
   122 (* print *)
   122 (* print *)
   123 
   123 
   124 fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
   124 fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
   125   Pretty.markup (Position.markup pos Markup.binding)
   125   Pretty.markup (Position.markup pos Isabelle_Markup.binding)
   126     [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
   126     [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
   127   |> Pretty.quote;
   127   |> Pretty.quote;
   128 
   128 
   129 val print = Pretty.str_of o pretty;
   129 val print = Pretty.str_of o pretty;
   130 
   130