src/Pure/General/comment.ML
changeset 67426 6311cf9dc943
parent 67425 7d4a088dbc0e
child 67429 95877cc6630e
equal deleted inserted replaced
67425:7d4a088dbc0e 67426:6311cf9dc943
     5 *)
     5 *)
     6 
     6 
     7 signature COMMENT =
     7 signature COMMENT =
     8 sig
     8 sig
     9   datatype kind = Comment | Cancel
     9   datatype kind = Comment | Cancel
    10   val scan_comment: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    10   val scan_comment: (kind * Symbol_Pos.T list) scanner
    11   val scan_cancel: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    11   val scan_cancel: (kind * Symbol_Pos.T list) scanner
    12   val scan: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    12   val scan: (kind * Symbol_Pos.T list) scanner
    13   val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
    13   val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
    14 end;
    14 end;
    15 
    15 
    16 structure Comment: COMMENT =
    16 structure Comment: COMMENT =
    17 struct
    17 struct