Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sat, 27 Jan 2018 17:27:06 +0100
changeset 67516 656720e8f443
parent 67515 fb87a0e9af21
child 67517 add9a9f6a290
tuned;
src/Pure/Syntax/parser.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/parser.ML	Sat Jan 27 17:23:21 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Sat Jan 27 17:27:06 2018 +0100
@@ -61,6 +61,9 @@
   known yet are associated with this token*)
 val unknown_start = Lexicon.eof;
 
+fun get_start (tok :: _) = tok
+  | get_start [] = unknown_start;
+
 (*get all NTs that are connected with a list of NTs*)
 fun connected_with _ ([]: nt_tag list) relatives = relatives
   | connected_with chains (root :: roots) relatives =
@@ -199,9 +202,7 @@
 
                             (*existing productions whose lookahead may depend on l*)
                             val tk_prods =
-                              these
-                                (AList.lookup (op =) nt_prods
-                                  (SOME (hd l_starts handle List.Empty => unknown_start)));
+                              these (AList.lookup (op =) nt_prods (SOME (get_start l_starts)));
 
                             (*add_lambda is true if an existing production of the nt
                               produces lambda due to the new lambda NT l*)
isabelle