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.
more robust (amending add9a9f6a290): proper syntax error instead of exception for grammar with unreachable nonterminals, e.g. nonterminal f1 syntax "_F" :: "f1 ⇒ 'b" ("F _" 10);
authorwenzelm
Mon, 24 Feb 2020 22:14:52 +0100
changeset 71468 53fcbede7bf7
parent 71467 708d301205fe
child 71470 b94053ca8d77
more robust (amending add9a9f6a290): proper syntax error instead of exception for grammar with unreachable nonterminals, e.g. nonterminal f1 syntax "_F" :: "f1 ⇒ 'b" ("F _" 10);
src/Pure/Syntax/parser.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/parser.ML	Mon Feb 24 21:43:52 2020 +0100
+++ b/src/Pure/Syntax/parser.ML	Mon Feb 24 22:14:52 2020 +0100
@@ -128,7 +128,12 @@
           if chains_member chains (from, lhs)
           then (SOME from, false, chains)
           else (SOME from, true, chains_insert (from, lhs) chains)
-      | _ => (NONE, false, chains_declare lhs chains));
+      | _ =>
+        let
+          val chains' = chains
+            |> chains_declare lhs
+            |> fold (fn Nonterminal (nt, _) => chains_declare nt | _ => I) rhs;
+        in (NONE, false, chains') end);
 
     (*propagate new chain in lookahead and lambdas;
       added_starts is used later to associate existing
isabelle