equal
deleted
inserted
replaced
170 (* print *) |
170 (* print *) |
171 |
171 |
172 fun pretty (Binding {prefix, qualifier, name, pos, ...}) = |
172 fun pretty (Binding {prefix, qualifier, name, pos, ...}) = |
173 if name = "" then Pretty.str "\"\"" |
173 if name = "" then Pretty.str "\"\"" |
174 else |
174 else |
175 Pretty.markup (Position.markup pos Markup.binding) |
175 Pretty.markup (Position.markup_properties pos Markup.binding) |
176 [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))] |
176 [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))] |
177 |> Pretty.quote; |
177 |> Pretty.quote; |
178 |
178 |
179 val print = Pretty.unformatted_string_of o pretty; |
179 val print = Pretty.unformatted_string_of o pretty; |
180 |
180 |