equal
deleted
inserted
replaced
154 else |
154 else |
155 Pretty.markup (Position.markup pos Markup.binding) |
155 Pretty.markup (Position.markup pos Markup.binding) |
156 [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))] |
156 [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))] |
157 |> Pretty.quote; |
157 |> Pretty.quote; |
158 |
158 |
159 val print = Pretty.str_of o pretty; |
159 val print = Pretty.unformatted_string_of o pretty; |
160 |
160 |
161 val pp = pretty o set_pos Position.none; |
161 val pp = pretty o set_pos Position.none; |
162 |
162 |
163 |
163 |
164 (* check *) |
164 (* check *) |