diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 30 | ||||
| -rw-r--r-- | vernac/misctypes.ml | 8 |
2 files changed, 28 insertions, 10 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index da14358ef..240147c8d 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -487,6 +487,15 @@ and check_no_ldots_in_box = function let error_not_same ?loc () = user_err ?loc Pp.(str "The format is not the same on the right- and left-hand sides of the special token \"..\".") +let find_prod_list_loc sfmt fmt = + (* [fmt] is some [UnpTerminal x :: sfmt @ UnpTerminal ".." :: sfmt @ UnpTerminal y :: rest] *) + if List.is_empty sfmt then + (* No separators; we highlight the sequence "x .." *) + Loc.merge_opt (fst (List.hd fmt)) (fst (List.hd (List.tl fmt))) + else + (* A separator; we highlight the separating sequence *) + Loc.merge_opt (fst (List.hd sfmt)) (fst (List.last sfmt)) + let skip_var_in_recursive_format = function | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) -> (* To do, though not so important: check that the names match @@ -496,6 +505,8 @@ let skip_var_in_recursive_format = function | [] -> assert false let read_recursive_format sl fmt = + (* Turn [[UnpTerminal s :: some-list @ UnpTerminal ".." :: same-some-list @ UnpTerminal s' :: rest] *) + (* into [(some-list,rest)] *) let get_head fmt = let sl = skip_var_in_recursive_format fmt in try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in @@ -528,10 +539,10 @@ let hunks_of_format (from,(vars,typs)) symfmt = let i = index_id m vars in let typ = List.nth typs (i-1) in let _,prec = precedence_of_entry_type from typ in - let slfmt,fmt = read_recursive_format sl fmt in - let sl, slfmt = aux (sl,slfmt) in - if not (List.is_empty sl) then error_format ?loc:(fst (List.last fmt)) (); - let symbs, l = aux (symbs,fmt) 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 (i,prec,slfmt) | ETBinder isopen -> @@ -1312,8 +1323,15 @@ let make_pa_rule level (typs,symbols) ntn need_squash = let make_pp_rule level (typs,symbols) fmt = match fmt with - | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols level)] - | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt) + | None -> + let hunks = make_hunks typs symbols level in + if List.exists (function _,(UnpCut (PpBrk _) | UnpListMetaVar _) -> true | _ -> false) hunks then + [UnpBox (PpHOVB 0,hunks)] + else + (* Optimization to work around what seems an ocaml Format bug (see Mantis #7804/#7807) *) + List.map snd hunks (* drop locations which are dummy *) + | Some fmt -> + hunks_of_format (level, List.split typs) (symbols, parse_format fmt) (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) let make_syntax_rules (sd : SynData.syn_data) = let open SynData in diff --git a/vernac/misctypes.ml b/vernac/misctypes.ml index ae725efaa..ef9cd3c35 100644 --- a/vernac/misctypes.ml +++ b/vernac/misctypes.ml @@ -17,10 +17,10 @@ type 'a or_by_notation = 'a Constrexpr.or_by_notation [@@ocaml.deprecated "use [Constrexpr.or_by_notation]"] type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr = - | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Evarutil]"] - | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Evarutil]"] - | IntroAnonymous [@ocaml.deprecated "Use version in [Evarutil]"] -[@@ocaml.deprecated "use [Evarutil.intro_pattern_naming_expr]"] + | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Namegen]"] + | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Namegen]"] + | IntroAnonymous [@ocaml.deprecated "Use version in [Namegen]"] +[@@ocaml.deprecated "use [Namegen.intro_pattern_naming_expr]"] type 'a or_var = 'a Locus.or_var = | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"] |