equal
deleted
inserted
replaced
165 val opt_attribs = Scan.optional attribs []; |
165 val opt_attribs = Scan.optional attribs []; |
166 |
166 |
167 |
167 |
168 (* pretty printing *) |
168 (* pretty printing *) |
169 |
169 |
170 fun markup_extern ctxt = |
|
171 Name_Space.markup_extern ctxt (Name_Space.space_of_table (get_attributes ctxt)); |
|
172 |
|
173 fun pretty_attribs _ [] = [] |
170 fun pretty_attribs _ [] = [] |
174 | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)]; |
171 | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)]; |
175 |
172 |
176 fun pretty_binding ctxt (b, atts) sep = |
173 fun pretty_binding ctxt (b, atts) sep = |
177 (case (Binding.is_empty b, null atts) of |
174 (case (Binding.is_empty b, null atts) of |