292 (* markup reports *) |
292 (* markup reports *) |
293 |
293 |
294 local |
294 local |
295 |
295 |
296 val token_kind_markup = |
296 val token_kind_markup = |
297 fn Command => (Markup.keyword1, "") |
297 fn Var => (Markup.var, "") |
298 | Keyword => (Markup.keyword2, "") |
|
299 | Ident => (Markup.empty, "") |
|
300 | Long_Ident => (Markup.empty, "") |
|
301 | Sym_Ident => (Markup.empty, "") |
|
302 | Var => (Markup.var, "") |
|
303 | Type_Ident => (Markup.tfree, "") |
298 | Type_Ident => (Markup.tfree, "") |
304 | Type_Var => (Markup.tvar, "") |
299 | Type_Var => (Markup.tvar, "") |
305 | Nat => (Markup.empty, "") |
|
306 | Float => (Markup.empty, "") |
|
307 | Space => (Markup.empty, "") |
|
308 | String => (Markup.string, "") |
300 | String => (Markup.string, "") |
309 | Alt_String => (Markup.alt_string, "") |
301 | Alt_String => (Markup.alt_string, "") |
310 | Verbatim => (Markup.verbatim, "") |
302 | Verbatim => (Markup.verbatim, "") |
311 | Cartouche => (Markup.cartouche, "") |
303 | Cartouche => (Markup.cartouche, "") |
312 | Comment => (Markup.comment, "") |
304 | Comment => (Markup.comment, "") |
313 | Error msg => (Markup.bad, msg) |
305 | Error msg => (Markup.bad, msg) |
314 | Internal_Value => (Markup.empty, "") |
306 | _ => (Markup.empty, ""); |
315 | EOF => (Markup.empty, ""); |
|
316 |
307 |
317 fun keyword_report tok markup = ((pos_of tok, markup), ""); |
308 fun keyword_report tok markup = ((pos_of tok, markup), ""); |
318 |
309 |
319 fun command_markup keywords x = |
310 fun command_markup keywords x = |
320 (case Keyword.command_kind keywords x of |
311 (case Keyword.command_kind keywords x of |