Merge PR #11650: Set Printing Parens

Reviewed-by: ejgallego

2 files changed, 21 insertions, 14 deletions

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index afff0347f5..3937f887ad 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -294,15 +294,15 @@ let precedence_of_position_and_level from_level = function
      | RightA, Right -> LevelLe n
      | LeftA, Left -> LevelLe n
      | LeftA, Right -> LevelLt n
-     | NonA, _ -> LevelLt n)
-  | NumLevel n, _ -> LevelLe n
-  | NextLevel, _ -> LevelLt from_level
-  | DefaultLevel, _ -> LevelSome
+     | NonA, _ -> LevelLt n), Some b
+  | NumLevel n, _ -> LevelLe n, None
+  | NextLevel, _ -> LevelLt from_level, None
+  | DefaultLevel, _ -> LevelSome, None
 
 (** Computing precedences of subentries for parsing *)
 let precedence_of_entry_type (from_custom,from_level) = function
   | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
-    precedence_of_position_and_level from_level x
+    fst (precedence_of_position_and_level from_level x)
   | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n
   | ETConstr (custom,_,(NextLevel,_)) ->
     user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
@@ -323,9 +323,9 @@ let unparsing_precedence_of_entry_type from_level = function
     (* Precedence of printing for a custom entry is managed using
        explicit insertion of entry coercions at the time of building
        a [constr_expr] *)
-    LevelSome
-  | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0)
-  | _ -> LevelSome (* should not matter *)
+    LevelSome, None
+  | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0), None
+  | _ -> LevelSome, None (* should not matter *)
 
 (* Some breaking examples *)
 (* "x = y" : "x /1 = y" (breaks before any symbol) *)
@@ -392,10 +392,10 @@ let check_open_binder isopen sl m =
 
 let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) in
-  let prec = unparsing_precedence_of_entry_type from x in
+  let prec,side = unparsing_precedence_of_entry_type from x in
   match x with
   | ETConstr _ | ETGlobal | ETBigint ->
-     UnpMetaVar prec
+     UnpMetaVar (prec,side)
   | ETPattern _ ->
      UnpBinderMetaVar prec
   | ETIdent ->
@@ -446,14 +446,14 @@ let make_hunks etyps symbols from_level =
     | SProdList (m,sl) :: prods ->
         let i = index_id m vars in
         let typ = List.nth typs (i-1) in
-        let prec = unparsing_precedence_of_entry_type from_level typ in
+        let prec,side = unparsing_precedence_of_entry_type from_level typ in
         let sl' =
           (* If no separator: add a break *)
           if List.is_empty sl then add_break 1 []
           (* We add NonTerminal for simulation but remove it afterwards *)
           else make true sl in
         let hunk = match typ with
-          | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl')
+          | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl',side)
           | ETBinder isopen ->
               check_open_binder isopen sl m;
               UnpBinderListMetaVar (isopen,List.map snd sl')
@@ -589,13 +589,13 @@ let hunks_of_format (from_level,(vars,typs)) symfmt =
   | SProdList (m,sl) :: symbs, fmt when has_ldots fmt ->
       let i = index_id m vars in
       let typ = List.nth typs (i-1) in
-      let prec = unparsing_precedence_of_entry_type from_level typ in
+      let prec,side = unparsing_precedence_of_entry_type from_level typ in
       let loc_slfmt,rfmt = read_recursive_format sl fmt in
       let sl, slfmt = aux (sl,loc_slfmt) in
       if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
       let symbs, l = aux (symbs,rfmt) in
       let hunk = match typ with
-        | ETConstr _ -> UnpListMetaVar (prec,slfmt)
+        | ETConstr _ -> UnpListMetaVar (prec,slfmt,side)
         | ETBinder isopen ->
             check_open_binder isopen sl m;
             UnpBinderListMetaVar (isopen,slfmt)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 63fc587f71..2eb1aa39b0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1282,6 +1282,13 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
+      optkey   = ["Printing";"Parentheses"];
+      optread  = (fun () -> !Constrextern.print_parentheses);
+      optwrite = (fun b ->  Constrextern.print_parentheses := b) }
+
+let () =
+  declare_bool_option
+    { optdepr  = false;
       optkey   = ["Printing";"Existential";"Instances"];
       optread  = (fun () -> !Detyping.print_evar_arguments);
       optwrite = (:=) Detyping.print_evar_arguments }