src/Pure/ML/ml_lex.ML
changeset 40319 daaa0b236a3f
parent 39507 839873937ddd
child 40337 d25bbb5f1c9e
equal deleted inserted replaced
40318:035b2afbeb2e 40319:daaa0b236a3f
    71 fun token_leq (tok, tok') = content_of tok <= content_of tok';
    71 fun token_leq (tok, tok') = content_of tok <= content_of tok';
    72 
    72 
    73 fun check_content_of tok =
    73 fun check_content_of tok =
    74   (case kind_of tok of
    74   (case kind_of tok of
    75     Error msg => error msg
    75     Error msg => error msg
    76   | _ => content_of tok);
    76   | _ =>
       
    77       (case tok of
       
    78         Token (_, (Keyword, ":>")) =>
       
    79           warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
       
    80             \prefer non-opaque matching (:) possibly with abstype" ^
       
    81             Position.str_of (pos_of tok))
       
    82       | _ => ();
       
    83       content_of tok));
    77 
    84 
    78 val flatten = implode o map (Symbol.escape o check_content_of);
    85 val flatten = implode o map (Symbol.escape o check_content_of);
    79 
    86 
    80 fun is_regular (Token (_, (Error _, _))) = false
    87 fun is_regular (Token (_, (Error _, _))) = false
    81   | is_regular (Token (_, (EOF, _))) = false
    88   | is_regular (Token (_, (EOF, _))) = false