src/Pure/Tools/rail.ML

 
 
 (* datatype token *)
 
 datatype kind =
-  Keyword | Ident | String | Space | Comment | Antiq of Antiquote.antiq | EOF;
+  Keyword | Ident | String | Space | Comment of Comment.kind | Antiq of Antiquote.antiq | EOF;
 
 datatype token = Token of Position.range * (kind * string);
 
 fun pos_of (Token ((pos, _), _)) = pos;
 fun end_pos_of (Token ((_, pos), _)) = pos;

 
 fun kind_of (Token (_, (k, _))) = k;
 fun content_of (Token (_, (_, x))) = x;
 
 fun is_proper (Token (_, (Space, _))) = false
-  | is_proper (Token (_, (Comment, _))) = false
+  | is_proper (Token (_, (Comment _, _))) = false
   | is_proper _ = true;
 
 
 (* diagnostics *)
 
 val print_kind =
  fn Keyword => "rail keyword"
   | Ident => "identifier"
   | String => "single-quoted string"
   | Space => "white space"
-  | Comment => "formal comment"
+  | Comment _ => "formal comment"
   | Antiq _ => "antiquotation"
   | EOF => "end-of-input";
 
 fun print (Token ((pos, _), (k, x))) =
   (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^

 
 val err_prefix = "Rail lexical error: ";
 
 val scan_token =
   scan_space >> token Space ||
-  Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment ||
+  Comment.scan >> (fn (kind, ss) => token (Comment kind) ss)||
   Antiquote.scan_antiq >> antiq_token ||
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||
   Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
     [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]);