src/Pure/ML/ml_lex.ML
changeset 31474 0ae32184bde0
parent 31426 5c9dbd511510
child 31543 5bef6c7cc819
equal deleted inserted replaced
31473:fd341ca4b8de 31474:0ae32184bde0
    13   val stopper: token Scan.stopper
    13   val stopper: token Scan.stopper
    14   val is_regular: token -> bool
    14   val is_regular: token -> bool
    15   val is_improper: token -> bool
    15   val is_improper: token -> bool
    16   val set_range: Position.range -> token -> token
    16   val set_range: Position.range -> token -> token
    17   val pos_of: token -> Position.T
    17   val pos_of: token -> Position.T
       
    18   val end_pos_of: token -> Position.T
    18   val kind_of: token -> token_kind
    19   val kind_of: token -> token_kind
    19   val content_of: token -> string
    20   val content_of: token -> string
    20   val check_content_of: token -> string
    21   val check_content_of: token -> string
    21   val flatten: token list -> string
    22   val flatten: token list -> string
    22   val report_token: token -> unit
    23   val report_token: token -> unit