OuterLex.name_of: include val;
authorwenzelm
Tue Jun 27 20:35:31 2000 +0200 (2000-06-27)
changeset 9155adfa40218e06
parent 9154 e71460b18988
child 9156 b9fe44ad3381
OuterLex.name_of: include val;
src/Pure/Isar/outer_lex.ML
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_lex.ML	Tue Jun 27 00:02:01 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_lex.ML	Tue Jun 27 20:35:31 2000 +0200
     1.3 @@ -106,8 +106,6 @@
     1.4  fun keyword_with pred (Token (_, (Keyword, x))) = pred x
     1.5    | keyword_with _ _ = false;
     1.6  
     1.7 -fun name_of (Token (_, (k, _))) = str_of_kind k;
     1.8 -
     1.9  fun is_proper (Token (_, (Space, _))) = false
    1.10    | is_proper (Token (_, (Comment, _))) = false
    1.11    | is_proper _ = true;
    1.12 @@ -132,7 +130,10 @@
    1.13    | is_indent _ = false;
    1.14  
    1.15  
    1.16 -(* value of token *)
    1.17 +(* name and value of token *)
    1.18 +
    1.19 +fun name_of (tok as Token (_, (k, x))) =
    1.20 +  if is_semicolon tok then "terminator" else str_of_kind k ^ " " ^ quote x;
    1.21  
    1.22  fun val_of (Token (_, (_, x))) = x;
    1.23  
     2.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Jun 27 00:02:01 2000 +0200
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Jun 27 20:35:31 2000 +0200
     2.3 @@ -85,8 +85,7 @@
     2.4  
     2.5  fun fail_with s = Scan.fail_with
     2.6    (fn [] => s ^ " expected (past end-of-file!)"
     2.7 -    | (tok :: _) => s ^ " expected,\nbut " ^ T.name_of tok ^ " " ^
     2.8 -      quote (T.val_of tok) ^ T.pos_of tok ^ " was found");
     2.9 +    | (tok :: _) => s ^ " expected,\nbut " ^ T.name_of tok ^ T.pos_of tok ^ " was found");
    2.10  
    2.11  fun group s scan = scan || fail_with s;
    2.12