changeset 31474 | 0ae32184bde0 |
parent 31426 | 5c9dbd511510 |
child 31543 | 5bef6c7cc819 |
--- a/src/Pure/ML/ml_lex.ML Sat Jun 06 19:58:10 2009 +0200 +++ b/src/Pure/ML/ml_lex.ML Sat Jun 06 19:58:11 2009 +0200 @@ -15,6 +15,7 @@ val is_improper: token -> bool val set_range: Position.range -> token -> token val pos_of: token -> Position.T + val end_pos_of: token -> Position.T val kind_of: token -> token_kind val content_of: token -> string val check_content_of: token -> string