Finalizing the only printing feature.

7 files changed, 64 insertions, 29 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 1f08b6a2f1..e91480ded3 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -321,6 +321,10 @@ Sometimes, a notation is expected only for the parser.
 To do so, the option {\em only parsing} is allowed in the list of modifiers of
 \texttt{Notation}.
 
+Conversely, the {\em only printing} can be used to declare
+that a notation should only be used for printing and should not declare a
+parsing rule. In particular, such notations do not modify the parser.
+
 \subsection{The \texttt{Infix} command
 \comindex{Infix}}
 
@@ -480,6 +484,7 @@ Locate "exists _ .. _ , _".
   & $|$ & {\ident} {\tt global} \\
   & $|$ & {\ident} {\tt bigint} \\
   & $|$ & {\tt only parsing} \\
+  & $|$ & {\tt only printing} \\
   & $|$ & {\tt format} {\str} 
 \end{tabular}
 \end{centerframe}
diff --git a/interp/notation.ml b/interp/notation.ml
index 7ad104d036..e777e5c24e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -44,8 +44,14 @@ type level = precedence * tolerability list
 type delimiters = string
 type notation_location = (DirPath.t * DirPath.t) * string
 
+type notation_data = {
+  not_interp : interpretation;
+  not_location : notation_location;
+  not_onlyprinting : bool;
+}
+
 type scope = {
-  notations: (interpretation * notation_location) String.Map.t;
+  notations: notation_data String.Map.t;
   delimiters: delimiters option
 }
 
@@ -380,7 +386,7 @@ let level_of_notation ntn =
 
 (* The mapping between notations and their interpretation *)
 
-let declare_notation_interpretation ntn scopt pat df =
+let declare_notation_interpretation ntn scopt pat df ~onlyprint =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
   let () =
@@ -390,7 +396,12 @@ let declare_notation_interpretation ntn scopt pat df =
     | Some _ -> str " in scope " ++ str scope in
     Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
   in
-  let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in
+  let notdata = {
+    not_interp = pat;
+    not_location = df;
+    not_onlyprinting = onlyprint;
+  } in
+  let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
   let () = scope_map := String.Map.add scope sc !scope_map in
   begin match scopt with
   | None -> scope_stack := SingleNotation ntn :: !scope_stack
@@ -415,7 +426,9 @@ let rec find_interpretation ntn find = function
       find_interpretation ntn find scopes
 
 let find_notation ntn sc =
-  String.Map.find ntn (find_scope sc).notations
+  let n = String.Map.find ntn (find_scope sc).notations in
+  let () = if n.not_onlyprinting then raise Not_found in
+  (n.not_interp, n.not_location)
 
 let notation_of_prim_token = function
   | Numeral n when is_pos_or_zero n -> to_string n
@@ -547,8 +560,8 @@ let exists_notation_in_scope scopt ntn r =
   let scope = match scopt with Some s -> s | None -> default_scope in
   try
     let sc = String.Map.find scope !scope_map in
-    let (r',_) = String.Map.find ntn sc.notations in
-    interpretation_eq r' r
+    let n = String.Map.find ntn sc.notations in
+    interpretation_eq n.not_interp r
   with Not_found -> false
 
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
@@ -805,7 +818,7 @@ let pr_named_scope prglob scope sc =
   ++ fnl ()
   ++ pr_scope_classes scope
   ++ String.Map.fold
-       (fun ntn ((_,r),(_,df)) strm ->
+       (fun ntn { not_interp  = (_, r); not_location = (_, df) } strm ->
 	 pr_notation_info prglob df r ++ fnl () ++ strm)
        sc.notations (mt ())
 
@@ -849,7 +862,7 @@ let browse_notation strict ntn map =
   let l =
     String.Map.fold
       (fun scope_name sc ->
-	String.Map.fold (fun ntn ((_,r),df) l ->
+	String.Map.fold (fun ntn { not_interp  = (_, r); not_location = df } l ->
 	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
       map [] in
   List.sort (fun x y -> String.compare (fst x) (fst y)) l
@@ -915,7 +928,7 @@ let locate_notation prglob ntn scope =
 let collect_notation_in_scope scope sc known =
   assert (not (String.equal scope default_scope));
   String.Map.fold
-    (fun ntn ((_,r),(_,df)) (l,known as acc) ->
+    (fun ntn { not_interp  = (_, r); not_location = (_, df) } (l,known as acc) ->
       if String.List.mem ntn known then acc else ((df,r)::l,ntn::known))
     sc.notations ([],known)
 
@@ -931,7 +944,7 @@ let collect_notations stack =
       | SingleNotation ntn ->
 	  if String.List.mem ntn knownntn then (all,knownntn)
 	  else
-	    let ((_,r),(_,df)) =
+	    let { not_interp  = (_, r); not_location = (_, df) } =
 	      String.Map.find ntn (find_scope default_scope).notations in
 	    let all' = match all with
 	      | (s,lonelyntn)::rest when String.equal s default_scope ->
diff --git a/interp/notation.mli b/interp/notation.mli
index a85dc50f2f..b47e1975e3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -109,7 +109,7 @@ type interp_rule =
   | SynDefRule of kernel_name
 
 val declare_notation_interpretation : notation -> scope_name option ->
-      interpretation -> notation_location -> unit
+      interpretation -> notation_location -> onlyprint:bool -> unit
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
diff --git a/test-suite/output/onlyprinting.out b/test-suite/output/onlyprinting.out
new file mode 100644
index 0000000000..e0a30fcf6b
--- /dev/null
+++ b/test-suite/output/onlyprinting.out
@@ -0,0 +1,2 @@
+0:-) 0
+     : nat
diff --git a/test-suite/output/onlyprinting.v b/test-suite/output/onlyprinting.v
new file mode 100644
index 0000000000..1973385a0a
--- /dev/null
+++ b/test-suite/output/onlyprinting.v
@@ -0,0 +1,5 @@
+Reserved Notation "x :-) y" (at level 50, only printing).
+
+Notation "x :-) y" := (plus x y).
+
+Check 0 + 0.
diff --git a/test-suite/success/onlyprinting.v b/test-suite/success/onlyprinting.v
new file mode 100644
index 0000000000..91a628d792
--- /dev/null
+++ b/test-suite/success/onlyprinting.v
@@ -0,0 +1,7 @@
+Notation "x ++ y" := (plus x y) (only printing).
+
+Fail Check 0 ++ 0.
+
+Notation "x + y" := (max x y) (only printing).
+
+Check (eq_refl : 42 + 18 = 60).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 8d20bf3d14..e772ea0205 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -991,12 +991,7 @@ let compute_pure_syntax_data df mods =
       (Feedback.msg_warning ?loc:None,
       strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
-  let msgs =
-    if onlyprint then
-      (Feedback.msg_warning ?loc:None,
-      strbrk "The only printing modifier has no effect in Reserved Notation.")::msgs
-    else msgs in
-  msgs, sy_data, extra
+  msgs, sy_data, extra, onlyprint
 
 (**********************************************************************)
 (* Registration of notations interpretation                            *)
@@ -1006,6 +1001,7 @@ type notation_obj = {
   notobj_scope : scope_name option;
   notobj_interp : interpretation;
   notobj_onlyparse : bool;
+  notobj_onlyprint : bool;
   notobj_notation : notation * notation_location;
 }
 
@@ -1018,7 +1014,8 @@ let open_notation i (_, nobj) =
   let pat = nobj.notobj_interp in
   if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
     (* Declare the interpretation *)
-    Notation.declare_notation_interpretation ntn scope pat df;
+    let onlyprint = nobj.notobj_onlyprint  in
+    let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
     (* Declare the uninterpretation *)
     if not nobj.notobj_onlyparse then
       Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat
@@ -1098,7 +1095,7 @@ let recover_notation_syntax rawntn =
   let sy = recover_syntax ntn in
   let need_squash = not (String.equal ntn rawntn) in
   let rules = if need_squash then recover_squash_syntax sy else [sy] in
-  sy.synext_notgram.notgram_typs, rules
+  sy.synext_notgram.notgram_typs, rules, sy.synext_notgram.notgram_onlyprinting
 
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
@@ -1163,6 +1160,7 @@ let add_notation_in_scope local df c mods scope =
     notobj_interp = (List.map_filter map i_vars, ac);
     (** Order is important here! *)
     notobj_onlyparse = onlyparse;
+    notobj_onlyprint = onlyprint;
     notobj_notation = df';
   } in
   (* Ready to change the global state *)
@@ -1171,14 +1169,17 @@ let add_notation_in_scope local df c mods scope =
   Lib.add_anonymous_leaf (inNotation notation);
   df'
 
-let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse =
+let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint =
   let dfs = split_notation_string df in
   let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
-  let i_typs = if not (is_numeral symbs) then begin
-    let i_typs,sy_rules = recover_notation_syntax (make_notation_key symbs) in
-    Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)); i_typs
-  end else [] in
+  let i_typs, onlyprint = if not (is_numeral symbs) then begin
+    let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in
+    let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) in
+    (** If the only printing flag has been explicitly requested, put it back *)
+    let onlyprint = onlyprint || onlyprint' in
+    i_typs, onlyprint
+  end else [], false in
   (* Declare interpretation *)
   let path = (Lib.library_dp(),Lib.current_dirpath true) in
   let df' = (make_notation_key symbs,(path,df)) in
@@ -1198,6 +1199,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
     notobj_interp = (List.map_filter map i_vars, ac);
     (** Order is important here! *)
     notobj_onlyparse = onlyparse;
+    notobj_onlyprint = onlyprint;
     notobj_notation = df';
   } in
   Lib.add_anonymous_leaf (inNotation notation);
@@ -1206,20 +1208,20 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
 (* Notations without interpretation (Reserved Notation) *)
 
 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 false in
+  let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in
+  let sy_rules = make_syntax_rules sy_data extra onlyprint in
   Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
 (* Notations with only interpretation *)
 
 let add_notation_interpretation ((loc,df),c,sc) =
-  let df' = add_notation_interpretation_core false df c sc false in
+  let df' = add_notation_interpretation_core false df c sc false false in
   Dumpglob.dump_notation (loc,df') sc true
 
 let set_notation_for_interpretation impls ((_,df),c,sc) =
   (try ignore
-    (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false) ());
+    (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false 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
@@ -1231,7 +1233,8 @@ let add_notation local c ((loc,df),modifiers) sc =
    if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
     let onlyparse = is_only_parsing modifiers in
-    try add_notation_interpretation_core local df c sc onlyparse
+    let onlyprint = is_only_printing modifiers in
+    try add_notation_interpretation_core local df c sc onlyparse onlyprint
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
       add_notation_in_scope local df c modifiers sc