Merge PR#429: Don't require printing-only notation to be productive

1 files changed, 8 insertions, 6 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 008d5cf9f5..e90d638d03 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -903,8 +903,8 @@ let find_precedence lev etyps symbols =
   let first_symbol =
     let rec aux = function
       | Break _ :: t -> aux t
-      | h :: t -> h
-      | [] -> assert false (* rule is known to be productive *) in
+      | h :: t -> Some h
+      | [] -> None in
     aux symbols in
   let last_is_terminal () =
     let rec aux b = function
@@ -914,7 +914,8 @@ let find_precedence lev etyps symbols =
       | [] -> b in
     aux false symbols in
   match first_symbol with
-  | NonTerminal x ->
+  | None -> [],0
+  | Some (NonTerminal x) ->
       (try match List.assoc x etyps with
 	| ETConstr _ ->
 	    error "The level of the leftmost non-terminal cannot be changed."
@@ -937,11 +938,11 @@ let find_precedence lev etyps symbols =
 	if Option.is_empty lev then
 	  error "A left-recursive notation must have an explicit level."
 	else [],Option.get lev)
-  | Terminal _ when last_is_terminal () ->
+  | Some (Terminal _) when last_is_terminal () ->
       if Option.is_empty lev then
 	([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
-  | _ ->
+  | Some _ ->
       if Option.is_empty lev then error "Cannot determine the level.";
       [],Option.get lev
 
@@ -983,6 +984,7 @@ let remove_curly_brackets l =
 
 let compute_syntax_data df modifiers =
   let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in
+  if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'.";
   let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
   let toks = split_notation_string df in
   let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
@@ -991,7 +993,7 @@ let compute_syntax_data df modifiers =
   let symbols' = remove_curly_brackets symbols in
   let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in
   let ntn_for_grammar = make_notation_key symbols' in
-  check_rule_productivity symbols';
+  if not onlyprint then check_rule_productivity symbols';
   let msgs,n = find_precedence n etyps symbols' in
   let innerlevel = NumLevel 200 in
   let typs =