From d8dc892dc4e50462163053124c9bafcd312433a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Oct 2019 22:07:00 +0200
Subject: Notations: Avoiding computing parsing rule when in onlyprinting mode.

In particular, this fixes #9741.
---
 parsing/notation_gram.ml | 5 +----
 parsing/notgram_ops.ml   | 6 +++---
 parsing/notgram_ops.mli  | 4 ++--
 parsing/ppextend.ml      | 3 ++-
 4 files changed, 8 insertions(+), 10 deletions(-)

(limited to 'parsing')

diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 9f133ca9d4..ffc92fa53a 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -37,7 +37,4 @@ type one_notation_grammar = {
   notgram_prods : grammar_constr_prod_item list list;
 }
 
-type notation_grammar = {
-  notgram_onlyprinting : bool;
-  notgram_rules : one_notation_grammar list
-}
+type notation_grammar = one_notation_grammar list
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 661f9c5cad..a84d2a4cb0 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -15,16 +15,16 @@ open Notation
 open Notation_gram
 
 (* Register the level of notation for parsing and printing
-   (we also register a precomputed parsing rule) *)
+   (also register the parsing rule if not onlyprinting) *)
 
 let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
 
-let declare_notation_level ntn ~onlyprint parsing_rule level =
+let declare_notation_level ntn parsing_rule level =
   try
     let _ = NotationMap.find ntn !notation_level_map in
     anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
   with Not_found ->
-  notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map
+  notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map
 
 let level_of_notation ntn =
   NotationMap.find ntn !notation_level_map
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index d5711569f0..7c676fbb10 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -16,8 +16,8 @@ val level_eq : level -> level -> bool
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
-val declare_notation_level : notation -> onlyprint:bool -> notation_grammar -> level -> unit
-val level_of_notation : notation -> bool (* = onlyprint *) * notation_grammar * level
+val declare_notation_level : notation -> notation_grammar option -> level -> unit
+val level_of_notation : notation -> notation_grammar option * level
   (** raise [Not_found] if not declared *)
 
 (** Returns notations with defined parsing/printing rules *)
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 92f44faec8..0277e79adb 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -59,7 +59,8 @@ let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
   | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ |
      UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false
 
-(* Concrete syntax for symbolic-extension table *)
+(* Register generic and specific printing rules *)
+
 let generic_notation_printing_rules =
   Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t)
 
-- 
cgit v1.2.3