Merge remote-tracking branch 'github/pr/194' into trunk

10 files changed, 86 insertions, 86 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index d1d6de9ae..f445f2e08 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -188,6 +188,7 @@ match sm with
       | LeftA -> ["associativity", "left"]
       end
   | SetEntryType (s, _) -> ["entrytype", s]
+  | SetOnlyPrinting -> ["onlyprinting", ""]
   | SetOnlyParsing v -> ["compat", Flags.pr_version v]
   | SetFormat (system, (loc, s)) ->
       let start, stop = unlock loc in
diff --git a/interp/notation.ml b/interp/notation.ml
index b19fd9e1f..7ad104d03 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -967,23 +967,27 @@ let pr_visibility prglob = function
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
 (* Concrete syntax for symbolic-extension table *)
-let printing_rules =
-  ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t)
+let notation_rules =
+  ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
 
-let declare_notation_printing_rule ntn ~extra unpl =
-  printing_rules := String.Map.add ntn (unpl,extra) !printing_rules
+let declare_notation_rule ntn ~extra unpl gram =
+  notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
 
 let find_notation_printing_rule ntn =
-  try fst (String.Map.find ntn !printing_rules)
+  try pi1 (String.Map.find ntn !notation_rules)
   with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
 let find_notation_extra_printing_rules ntn =
-  try snd (String.Map.find ntn !printing_rules)
+  try pi2 (String.Map.find ntn !notation_rules)
   with Not_found -> []
+let find_notation_parsing_rules ntn =
+  try pi3 (String.Map.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn)
+
 let add_notation_extra_printing_rule ntn k v =
   try
-    printing_rules := 
-      let p, pp = String.Map.find ntn !printing_rules in
-      String.Map.add ntn (p, (k,v) :: pp) !printing_rules
+    notation_rules :=
+      let p, pp, gr = String.Map.find ntn !notation_rules in
+      String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
   with Not_found ->
     user_err_loc (Loc.ghost,"add_notation_extra_printing_rule",
       str "No such Notation.")
@@ -993,7 +997,7 @@ let add_notation_extra_printing_rule ntn k v =
 
 let freeze _ =
  (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
-  !delimiters_map, !notations_key_table, !printing_rules,
+  !delimiters_map, !notations_key_table, !notation_rules,
   !scope_class_map)
 
 let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
@@ -1003,7 +1007,7 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
   delimiters_map := dlm;
   arguments_scope := asc;
   notations_key_table := fkm;
-  printing_rules := pprules;
+  notation_rules := pprules;
   scope_class_map := clsc
 
 let init () =
@@ -1011,7 +1015,7 @@ let init () =
   notation_level_map := String.Map.empty;
   delimiters_map := String.Map.empty;
   notations_key_table := KeyMap.empty;
-  printing_rules := String.Map.empty;
+  notation_rules := String.Map.empty;
   scope_class_map := initial_scope_class_map
 
 let _ =
diff --git a/interp/notation.mli b/interp/notation.mli
index 480979ccc..a85dc50f2 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -196,10 +196,11 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
-val declare_notation_printing_rule :
-  notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val declare_notation_rule :
+  notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
 val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val find_notation_parsing_rules : notation -> notation_grammar
 val add_notation_extra_printing_rule : notation -> string -> string -> unit
 
 (** Rem: printing rules for primitive token are canonical *)
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 7c5d7657b..883b01772 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -78,3 +78,19 @@ type notation_interp_env = {
   ninterp_rec_vars : Id.t Id.Map.t;
   mutable ninterp_only_parse : bool;
 }
+
+type grammar_constr_prod_item =
+  | GramConstrTerminal of Tok.t
+  | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
+  | GramConstrListMark of int * bool
+    (* tells action rule to make a list of the n previous parsed items;
+       concat with last parsed list if true *)
+
+type notation_grammar = {
+  notgram_level : int;
+  notgram_assoc : Extend.gram_assoc option;
+  notgram_notation : Constrexpr.notation;
+  notgram_prods : grammar_constr_prod_item list list;
+  notgram_typs : notation_var_internalization_type list;
+  notgram_onlyprinting : bool;
+}
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 6ce15a7c5..cfa30a4d5 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -206,6 +206,7 @@ type syntax_modifier =
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing of Flags.compat_version
+  | SetOnlyPrinting
   | SetFormat of string * string located
 
 type proof_end =
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 21a9afa29..ade31c1d3 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -9,9 +9,10 @@
 open Errors
 open Util
 open Pcoq
-open Extend
 open Constrexpr
+open Notation
 open Notation_term
+open Extend
 open Libnames
 open Names
 
@@ -320,13 +321,6 @@ let cases_pattern_expr_of_name (loc,na) = match na with
   | Anonymous -> CPatAtom (loc,None)
   | Name id -> CPatAtom (loc,Some (Ident (loc,id)))
 
-type grammar_constr_prod_item =
-  | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of constr_prod_entry_key * Id.t option
-  | GramConstrListMark of int * bool
-    (* tells action rule to make a list of the n previous parsed items;
-       concat with last parsed list if true *)
-
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
@@ -444,14 +438,6 @@ let make_act : type r. r target -> _ -> r gen_eval = function
   let env = (env.constrs, env.constrlists) in
   CPatNotation (loc, notation, env, [])
 
-type notation_grammar = {
-  notgram_level : int;
-  notgram_assoc : gram_assoc option;
-  notgram_notation : notation;
-  notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
-}
-
 let extend_constr state forpat ng =
   let n = ng.notgram_level in
   let assoc = ng.notgram_assoc in
@@ -491,12 +477,3 @@ let constr_grammar : (Notation.level * notation_grammar) grammar_command =
   create_grammar_command "Notation" extend_constr_notation
 
 let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn)
-
-let recover_constr_grammar ntn prec =
-  let filter (prec', ng) =
-    if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
-    else None
-  in
-  match List.map_filter filter (recover_grammar_command constr_grammar) with
-  | [x] -> x
-  | _ -> assert false
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 1fe06a29d..6dda3817a 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -19,28 +19,7 @@ open Egramml
 (** This is the part specific to Coq-level Notation and Tactic Notation.
     For the ML-level tactic and vernac extensions, see Egramml. *)
 
-(** For constr notations *)
-
-type grammar_constr_prod_item =
-  | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of constr_prod_entry_key * Id.t option
-  | GramConstrListMark of int * bool
-    (* tells action rule to make a list of the n previous parsed items;
-       concat with last parsed list if true *)
-
-type notation_grammar = {
-  notgram_level : int;
-  notgram_assoc : gram_assoc option;
-  notgram_notation : notation;
-  notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
-}
-
 (** {5 Adding notations} *)
 
-val extend_constr_grammar : Notation.level -> notation_grammar -> unit
+val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
-
-val recover_constr_grammar : notation -> Notation.level -> notation_grammar
-(** For a declared grammar, returns the rule + the ordered entry types
-    of variables in the rule (for use in the interpretation) *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0df15babd..9c1f5afb8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1076,6 +1076,7 @@ GEXTEND Gram
       | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc NonA
+      | IDENT "only"; IDENT "printing" -> SetOnlyPrinting
       | IDENT "only"; IDENT "parsing" ->
         SetOnlyParsing Flags.Current
       | IDENT "compat"; s = STRING ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 10b2bda05..cd7434843 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -357,6 +357,7 @@ module Make
     | SetAssoc RightA -> keyword "right associativity"
     | SetAssoc NonA -> keyword "no associativity"
     | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
+    | SetOnlyPrinting -> keyword "only printing"
     | SetOnlyParsing Flags.Current -> keyword "only parsing"
     | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
     | SetFormat("text",s) -> keyword "format " ++ pr_located qs s
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index b22d53f54..7d8c67025 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -680,6 +680,7 @@ type syntax_extension_obj = locality_flag * syntax_extension list
 let cache_one_syntax_extension se =
   let ntn = se.synext_notation in
   let prec = se.synext_level in
+  let onlyprint = se.synext_notgram.notgram_onlyprinting in
   try
     let oldprec = Notation.level_of_notation ntn in
     if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec
@@ -687,10 +688,10 @@ let cache_one_syntax_extension se =
     (* Reserve the notation level *)
     Notation.declare_notation_level ntn prec;
     (* Declare the parsing rule *)
-    Egramcoq.extend_constr_grammar prec se.synext_notgram;
-    (* Declare the printing rule *)
-    Notation.declare_notation_printing_rule ntn
-      ~extra:se.synext_extra (se.synext_unparsing, fst prec)
+    if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram;
+    (* Declare the notation rule *)
+    Notation.declare_notation_rule ntn
+      ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram
 
 let cache_syntax_extension (_, (_, sy)) =
   List.iter cache_one_syntax_extension sy
@@ -723,9 +724,10 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
 
 let interp_modifiers modl =
   let onlyparsing = ref false in
+  let onlyprinting = ref false in
   let rec interp assoc level etyps format extra = function
     | [] ->
-	(assoc,level,etyps,!onlyparsing,format,extra)
+	(assoc,level,etyps,!onlyparsing,!onlyprinting,format,extra)
     | SetEntryType (s,typ) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
@@ -750,6 +752,9 @@ let interp_modifiers modl =
     | SetOnlyParsing _ :: l ->
 	onlyparsing := true;
 	interp assoc level etyps format extra l
+    | SetOnlyPrinting :: l ->
+	onlyprinting := true;
+	interp assoc level etyps format extra l
     | SetFormat ("text",s) :: l ->
 	if not (Option.is_empty format) then error "A format is given more than once.";
 	interp assoc level etyps (Some s) extra l
@@ -758,7 +763,7 @@ let interp_modifiers modl =
   in interp None None [] None [] modl
 
 let check_infix_modifiers modifiers =
-  let (assoc,level,t,b,fmt,extra) = interp_modifiers modifiers in
+  let (_, _, t, _, _, _, _) = interp_modifiers modifiers in
   if not (List.is_empty t) then
     error "Explicit entry level or type unexpected in infix notation."
 
@@ -769,13 +774,20 @@ let check_useless_entry_types recvars mainvars etyps =
                   (pr_id x ++ str " is unbound in the notation.")
   | _ -> ()
 
-let no_syntax_modifiers = function
-  | [] | [SetOnlyParsing _] -> true
-  | _ -> false
+let not_a_syntax_modifier = function
+| SetOnlyParsing _ -> true
+| SetOnlyPrinting -> true
+| _ -> false
 
-let is_only_parsing = function
-  | [SetOnlyParsing _] -> true
-  | _ -> false
+let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods
+
+let is_only_parsing mods =
+  let test = function SetOnlyParsing _ -> true | _ -> false in
+  List.exists test mods
+
+let is_only_printing mods =
+  let test = function SetOnlyPrinting -> true | _ -> false in
+  List.exists test mods
 
 (* Compute precedences from modifiers (or find default ones) *)
 
@@ -942,7 +954,7 @@ let remove_curly_brackets l =
   in aux true l
 
 let compute_syntax_data df modifiers =
-  let (assoc,n,etyps,onlyparse,fmt,extra) = interp_modifiers modifiers in
+  let (assoc,n,etyps,onlyparse,onlyprint,fmt,extra) = interp_modifiers modifiers in
   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
@@ -968,17 +980,22 @@ let compute_syntax_data df modifiers =
   let sy_data = (n,sy_typs,symbols',fmt) in
   let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in
   let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
-  let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in
+  let i_data = (onlyparse,onlyprint,recvars,mainvars,(ntn_for_interp,df')) in
   (* Return relevant data for interpretation and for parsing/printing *)
   (msgs,i_data,i_typs,sy_fulldata,extra)
 
 let compute_pure_syntax_data df mods =
-  let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
+  let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
   let msgs =
     if onlyparse then
       (Feedback.msg_warning,
       strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
+  let msgs =
+    if onlyprint then
+      (Feedback.msg_warning,
+      strbrk "The only printing modifier has no effect in Reserved Notation.")::msgs
+    else msgs in
   msgs, sy_data, extra
 
 (**********************************************************************)
@@ -1063,7 +1080,7 @@ let recover_syntax ntn =
     let prec = Notation.level_of_notation ntn in
     let pp_rule,_ = Notation.find_notation_printing_rule ntn in
     let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
-    let pa_rule = Egramcoq.recover_constr_grammar ntn prec in
+    let pa_rule = Notation.find_notation_parsing_rules ntn in
     { synext_level = prec;
       synext_notation = ntn;
       synext_notgram = pa_rule;
@@ -1086,22 +1103,24 @@ let recover_notation_syntax rawntn =
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
 
-let make_pa_rule i_typs (n,typs,symbols,_) ntn =
+let make_pa_rule i_typs (n,typs,symbols,_) ntn onlyprint =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
   { notgram_level = n;
     notgram_assoc = assoc;
     notgram_notation = ntn;
     notgram_prods = prod;
-    notgram_typs = i_typs; }
+    notgram_typs = i_typs;
+    notgram_onlyprinting = onlyprint;
+  }
 
 let make_pp_rule (n,typs,symbols,fmt) =
   match fmt with
   | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
   | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
 
-let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra =
-  let pa_rule = make_pa_rule i_typs sy_data ntn in
+let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint =
+  let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in
   let pp_rule = make_pp_rule sy_data in
   let sy = {
     synext_level = prec;
@@ -1124,10 +1143,10 @@ let to_map l =
 
 let add_notation_in_scope local df c mods scope =
   let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in
-  (* Prepare the parsing and printing rules *)
-  let sy_rules = make_syntax_rules sy_data extra in
   (* Prepare the interpretation *)
-  let (onlyparse, recvars,mainvars, df') = i_data in
+  let (onlyparse, onlyprint, recvars,mainvars, df') = i_data in
+  (* Prepare the parsing and printing rules *)
+  let sy_rules = make_syntax_rules sy_data extra onlyprint in
   let i_vars = make_internalization_vars recvars mainvars i_typs in
   let nenv = {
     ninterp_var_type = to_map i_vars;
@@ -1188,7 +1207,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
 
 let add_syntax_extension local ((loc,df),mods) =
   let msgs, sy_data, extra = compute_pure_syntax_data df mods in
-  let sy_rules = make_syntax_rules sy_data extra in
+  let sy_rules = make_syntax_rules sy_data extra false in
   Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
@@ -1200,7 +1219,7 @@ let add_notation_interpretation ((loc,df),c,sc) =
 
 let set_notation_for_interpretation impls ((_,df),c,sc) =
   (try ignore
-    (silently (add_notation_interpretation_core false df ~impls c sc) false);
+    (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false) ());
   with NoSyntaxRule ->
     error "Parsing rule for this notation has to be previously declared.");
   Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc