equal
deleted
inserted
replaced
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 |