1.1 --- a/src/Pure/ML/ml_lex.ML	Sun Mar 22 19:10:58 2009 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Mar 22 19:10:59 2009 +0100
     1.3 @@ -13,9 +13,10 @@
     1.4    val stopper: token Scan.stopper
     1.5    val is_regular: token -> bool
     1.6    val is_improper: token -> bool
     1.7 -  val pos_of: token -> string
     1.8 +  val pos_of: token -> Position.T
     1.9    val kind_of: token -> token_kind
    1.10    val content_of: token -> string
    1.11 +  val text_of: token -> string
    1.12    val markup_of: token -> Markup.T
    1.13    val report_token: token -> unit
    1.14    val keywords: string list
    1.15 @@ -42,10 +43,8 @@
    1.16  
    1.17  (* position *)
    1.18  
    1.19 -fun position_of (Token ((pos, _), _)) = pos;
    1.20 -fun end_position_of (Token ((_, pos), _)) = pos;
    1.21 -
    1.22 -val pos_of = Position.str_of o position_of;
    1.23 +fun pos_of (Token ((pos, _), _)) = pos;
    1.24 +fun end_pos_of (Token ((_, pos), _)) = pos;
    1.25  
    1.26  
    1.27  (* control tokens *)
    1.28 @@ -57,7 +56,7 @@
    1.29    | is_eof _ = false;
    1.30  
    1.31  val stopper =
    1.32 -  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
    1.33 +  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
    1.34  
    1.35  
    1.36  (* token content *)
    1.37 @@ -67,6 +66,11 @@
    1.38  
    1.39  fun kind_of (Token (_, (k, _))) = k;
    1.40  
    1.41 +fun text_of tok =
    1.42 +  (case kind_of tok of
    1.43 +    Error msg => error (msg ^ Position.str_of (pos_of tok))
    1.44 +  | _ => Symbol.escape (content_of tok));
    1.45 +
    1.46  fun is_regular (Token (_, (Error _, _))) = false
    1.47    | is_regular (Token (_, (EOF, _))) = false
    1.48    | is_regular _ = true;
    1.49 @@ -93,7 +97,7 @@
    1.50      | Error _   => Markup.ML_malformed
    1.51      | EOF       => Markup.none);
    1.52  
    1.53 -fun report_token tok = Position.report (markup_of tok) (position_of tok);
    1.54 +fun report_token tok = Position.report (markup_of tok) (pos_of tok);
    1.55  
    1.56  
    1.57