# HG changeset patch # User wenzelm # Date 1517395226 -3600 # Node ID 679253fef27751efa334571f1b25a80079094aff # Parent 4a087b9a29c556c1fe6d6d08fbc09f3738676d31 clarified signature; diff -r 4a087b9a29c5 -r 679253fef277 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Wed Jan 31 11:26:50 2018 +0100 +++ b/src/Pure/Syntax/lexicon.ML Wed Jan 31 11:40:26 2018 +0100 @@ -30,6 +30,8 @@ val pos_of_token: token -> Position.T val end_pos_of_token: token -> Position.T val tokens_match_ord: token * token -> order + val literal: string -> token + val is_literal: token -> bool val is_proper: token -> bool val dummy: token val mk_eof: Position.T -> token @@ -154,6 +156,9 @@ (Literal, Literal) => fast_string_ord (apply2 str_of_token toks) | kinds => token_kind_ord kinds); +fun literal s = Token (Literal, s, Position.no_range); +fun is_literal tok = kind_of_token tok = Literal; + val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true); val dummy = Token (Dummy, "", Position.no_range); diff -r 4a087b9a29c5 -r 679253fef277 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Jan 31 11:26:50 2018 +0100 +++ b/src/Pure/Syntax/parser.ML Wed Jan 31 11:40:26 2018 +0100 @@ -401,8 +401,10 @@ val print_nt = tags_name tags; fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ string_of_int p ^ ")"); - fun pretty_symb (Terminal (Lexicon.Token (kind, s, _))) = - if kind = Lexicon.Literal then Pretty.quote (Pretty.keyword1 s) else Pretty.str s + fun pretty_symb (Terminal tok) = + if Lexicon.is_literal tok + then Pretty.quote (Pretty.keyword1 (Lexicon.str_of_token tok)) + else Pretty.str (Lexicon.str_of_token tok) | pretty_symb (Nonterminal (tag, p)) = Pretty.str (print_nt tag ^ print_pri p); fun pretty_const "" = [] @@ -446,8 +448,7 @@ nonterminals are converted to integer tags*) fun symb_of [] nt_count tags result = (nt_count, tags, rev result) | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result = - symb_of ss nt_count tags - (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result) + symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result) | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result = let val (nt_count', tags', new_symb) = @@ -722,11 +723,12 @@ let fun freeze a = map_range (curry Vector.sub a) (Vector.length a); val prods = maps (prods_content o #2) (freeze (#prods gram)); - fun guess (SOME ([Nonterminal (_, k), - Terminal (Lexicon.Token (Lexicon.Literal, s, _)), Nonterminal (_, l)], _, j)) = - if k = j andalso l = j + 1 then SOME (s, true, false, j) - else if k = j + 1 then if l = j then SOME (s, false, true, j) - else if l = j + 1 then SOME (s, false, false, j) + fun guess (SOME ([Nonterminal (_, k), Terminal tok, Nonterminal (_, l)], _, j)) = + if Lexicon.is_literal tok then + if k = j andalso l = j + 1 then SOME (Lexicon.str_of_token tok, true, false, j) + else if k = j + 1 then if l = j then SOME (Lexicon.str_of_token tok, false, true, j) + else if l = j + 1 then SOME (Lexicon.str_of_token tok, false, false, j) + else NONE else NONE else NONE | guess _ = NONE; diff -r 4a087b9a29c5 -r 679253fef277 src/Pure/Syntax/simple_syntax.ML --- a/src/Pure/Syntax/simple_syntax.ML Wed Jan 31 11:26:50 2018 +0100 +++ b/src/Pure/Syntax/simple_syntax.ML Wed Jan 31 11:40:26 2018 +0100 @@ -31,8 +31,9 @@ (* basic scanners *) -fun $$ s = Scan.some (fn Lexicon.Token (Lexicon.Literal, s', _) => - if s = s' then SOME s else NONE | _ => NONE); +fun $$ s = + Scan.some (fn tok => + if Lexicon.is_literal tok andalso s = Lexicon.str_of_token tok then SOME s else NONE); fun enum1 s scan = scan ::: Scan.repeat ($$ s |-- scan); fun enum2 s scan = scan ::: Scan.repeat1 ($$ s |-- scan);