src/Pure/ML/ml_lex.ML
changeset 59124 60c134fdd290
parent 59112 e670969f34df
child 61457 3e21699bb83b
equal deleted inserted replaced
59123:e68e44836d04 59124:60c134fdd290
   142 (* markup *)
   142 (* markup *)
   143 
   143 
   144 local
   144 local
   145 
   145 
   146 fun token_kind_markup SML =
   146 fun token_kind_markup SML =
   147  fn Keyword => (Markup.empty, "")
   147  fn Type_Var => (Markup.ML_tvar, "")
   148   | Ident => (Markup.empty, "")
       
   149   | Long_Ident => (Markup.empty, "")
       
   150   | Type_Var => (Markup.ML_tvar, "")
       
   151   | Word => (Markup.ML_numeral, "")
   148   | Word => (Markup.ML_numeral, "")
   152   | Int => (Markup.ML_numeral, "")
   149   | Int => (Markup.ML_numeral, "")
   153   | Real => (Markup.ML_numeral, "")
   150   | Real => (Markup.ML_numeral, "")
   154   | Char => (Markup.ML_char, "")
   151   | Char => (Markup.ML_char, "")
   155   | String => (if SML then Markup.SML_string else Markup.ML_string, "")
   152   | String => (if SML then Markup.SML_string else Markup.ML_string, "")
   156   | Space => (Markup.empty, "")
       
   157   | Cartouche => (Markup.ML_cartouche, "")
   153   | Cartouche => (Markup.ML_cartouche, "")
   158   | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
   154   | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
   159   | Error msg => (Markup.bad, msg)
   155   | Error msg => (Markup.bad, msg)
   160   | EOF => (Markup.empty, "");
   156   | _ => (Markup.empty, "");
   161 
   157 
   162 in
   158 in
   163 
   159 
   164 fun report_of_token SML (tok as Token ((pos, _), (kind, x))) =
   160 fun report_of_token SML (tok as Token ((pos, _), (kind, x))) =
   165   let
   161   let