diff options
Diffstat (limited to 'vernac/metasyntax.ml')
-rw-r--r-- | vernac/metasyntax.ml | 68 |
1 files changed, 34 insertions, 34 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index fb7c72941..42494dd28 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -60,7 +60,7 @@ let pr_entry e = let pr_registered_grammar name = let gram = try Some (String.Map.find name !grammars) with Not_found -> None in match gram with - | None -> error "Unknown or unprintable grammar entry." + | None -> user_err Pp.(str "Unknown or unprintable grammar entry.") | Some entries -> let pr_one (AnyEntry e) = str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++ @@ -107,11 +107,11 @@ let parse_format ((loc, str) : lstring) = if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in let close_box i b = function | a::(_::_ as l) -> push_token (UnpBox (b,a)) l - | _ -> error "Non terminated box in format." in + | _ -> user_err Pp.(str "Non terminated box in format.") in let close_quotation i = if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ') then i+1 - else error "Incorrectly terminated quoted expression." in + else user_err Pp.(str "Incorrectly terminated quoted expression.") in let rec spaces n i = if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1) else n in @@ -119,10 +119,10 @@ let parse_format ((loc, str) : lstring) = if i < String.length str && str.[i] != ' ' then if str.[i] == '\'' && quoted && (i+1 >= String.length str || str.[i+1] == ' ') - then if Int.equal n 0 then error "Empty quoted token." else n + then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n else nonspaces quoted (n+1) (i+1) else - if quoted then error "Spaces are not allowed in (quoted) symbols." + if quoted then user_err Pp.(str "Spaces are not allowed in (quoted) symbols.") else n in let rec parse_non_format i = let n = nonspaces false 0 i in @@ -153,8 +153,8 @@ let parse_format ((loc, str) : lstring) = (* Parse " [ .. ", *) | ' ' | '\'' -> parse_box (fun n -> PpHOVB n) (i+1) - | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format." - else error "\"v\", \"hv\" or \" \" expected after \"[\" in format." + | _ -> user_err Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.") + else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.") (* Parse "]" *) | ']' -> ([] :: parse_token (close_quotation (i+1))) @@ -165,7 +165,7 @@ let parse_format ((loc, str) : lstring) = (parse_token (close_quotation (i+n)))) else if Int.equal n 0 then [] - else error "Ending spaces non part of a format annotation." + else user_err Pp.(str "Ending spaces non part of a format annotation.") and parse_box box i = let n = spaces 0 i in close_box i (box n) (parse_token (close_quotation (i+n))) @@ -187,9 +187,9 @@ let parse_format ((loc, str) : lstring) = try if not (String.is_empty str) then match parse_token 0 with | [l] -> l - | _ -> error "Box closed without being opened in format." + | _ -> user_err Pp.(str "Box closed without being opened in format.") else - error "Empty format." + user_err Pp.(str "Empty format.") with reraise -> let (e, info) = CErrors.push reraise in let info = Option.cata (Loc.add_loc info) info loc in @@ -243,19 +243,19 @@ let rec find_pattern nt xl = function | [], NonTerminal x' :: l' -> (out_nt nt,x',List.rev xl),l' | _, Break s :: _ | Break s :: _, _ -> - error ("A break occurs on one side of \"..\" but not on the other side.") + user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side.")) | _, Terminal s :: _ | Terminal s :: _, _ -> user_err ~hdr:"Metasyntax.find_pattern" (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") | _, [] -> - error msg_expected_form_of_recursive_notation + user_err Pp.(str msg_expected_form_of_recursive_notation) | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right") let rec interp_list_parser hd = function | [] -> [], List.rev hd | NonTerminal id :: tl when Id.equal id ldots_var -> - if List.is_empty hd then error msg_expected_form_of_recursive_notation; + if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation); let hd = List.rev hd in let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in let xyl,tl'' = interp_list_parser [] tl' in @@ -286,7 +286,7 @@ let quote_notation_token x = let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl - | String "_" :: _ -> error "_ must be quoted." + | String "_" :: _ -> user_err Pp.(str "_ must be quoted.") | String x :: sl when CLexer.is_ident x -> NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> @@ -487,7 +487,7 @@ let make_hunks etyps symbols from = (* Build default printing rules from explicit format *) -let error_format () = error "The format does not match the notation." +let error_format () = user_err Pp.(str "The format does not match the notation.") let rec split_format_at_ldots hd = function | UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt @@ -500,7 +500,7 @@ and check_no_ldots_in_box = function | UnpBox (_,fmt) -> (try let _ = split_format_at_ldots [] fmt in - error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.") + user_err Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.")) with Exit -> ()) | _ -> () @@ -518,7 +518,7 @@ let read_recursive_format sl fmt = let rec get_tail = function | a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *) | [], tail -> skip_var_in_recursive_format tail - | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"." in + | _ -> user_err Pp.(str "The format is not the same on the right and left hand side of the special token \"..\".") in let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) @@ -652,7 +652,7 @@ let make_production etyps symbols = distribute [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll | _ -> - error "Components of recursive patterns in notation must be terms or binders.") + user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.")) symbols [[]] in List.map define_keywords prod @@ -811,7 +811,7 @@ let interp_modifiers modl = let open NotationMods in interp { acc with level = Some n; } l | SetAssoc a :: l -> - if not (Option.is_empty acc.assoc) then error "An associativity is given more than once."; + if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once."); interp { acc with assoc = Some a; } l | SetOnlyParsing :: l -> interp { acc with only_parsing = true; } l @@ -820,7 +820,7 @@ let interp_modifiers modl = let open NotationMods in | SetCompatVersion v :: l -> interp { acc with compat = Some v; } l | SetFormat ("text",s) :: l -> - if not (Option.is_empty acc.format) then error "A format is given more than once."; + if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once."); interp { acc with format = Some s; } l | SetFormat (k,(_,s)) :: l -> interp { acc with extra = (k,s)::acc.extra; } l @@ -829,7 +829,7 @@ let interp_modifiers modl = let open NotationMods in let check_infix_modifiers modifiers = let t = (interp_modifiers modifiers).NotationMods.etyps in if not (List.is_empty t) then - error "Explicit entry level or type unexpected in infix notation." + user_err Pp.(str "Explicit entry level or type unexpected in infix notation.") let check_useless_entry_types recvars mainvars etyps = let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in @@ -901,7 +901,7 @@ let internalization_type_of_entry_type = function | ETBigint | ETReference -> NtnInternTypeConstr | ETBinder _ -> NtnInternTypeBinder | ETName -> NtnInternTypeIdent - | ETPattern | ETOther _ -> error "Not supported." + | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.") | ETBinderList _ | ETConstrList _ -> assert false let set_internalization_type typs = @@ -917,7 +917,7 @@ let make_interpretation_type isrec isonlybinding = function | NtnInternTypeConstr | NtnInternTypeIdent -> if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders." + | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.") let make_interpretation_vars recvars allvars = let eq_subscope (sc1, l1) (sc2, l2) = @@ -938,9 +938,9 @@ let make_interpretation_vars recvars allvars = let check_rule_productivity l = if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then - error "A notation must include at least one symbol."; + user_err Pp.(str "A notation must include at least one symbol."); if (match l with SProdList _ :: _ -> true | _ -> false) then - error "A recursive notation must start with at least one symbol." + user_err Pp.(str "A recursive notation must start with at least one symbol.") let warn_notation_bound_to_variable = CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing" @@ -980,7 +980,7 @@ let find_precedence lev etyps symbols = | Some (NonTerminal x) -> (try match List.assoc x etyps with | ETConstr _ -> - error "The level of the leftmost non-terminal cannot be changed." + user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") | ETName | ETBigint | ETReference -> begin match lev with | None -> @@ -988,31 +988,31 @@ let find_precedence lev etyps symbols = | Some 0 -> ([],0) | _ -> - error "A notation starting with an atomic expression must be at level 0." + user_err Pp.(str "A notation starting with an atomic expression must be at level 0.") end | ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *) if Option.is_empty lev then - error "Need an explicit level." + user_err Pp.(str "Need an explicit level.") else [],Option.get lev | ETConstrList _ | ETBinderList _ -> assert false (* internally used in grammar only *) with Not_found -> if Option.is_empty lev then - error "A left-recursive notation must have an explicit level." + user_err Pp.(str "A left-recursive notation must have an explicit level.") else [],Option.get lev) | Some (Terminal _) when last_is_terminal () -> if Option.is_empty lev then ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) else [],Option.get lev | Some _ -> - if Option.is_empty lev then error "Cannot determine the level."; + if Option.is_empty lev then user_err Pp.(str "Cannot determine the level."); [],Option.get lev let check_curly_brackets_notation_exists () = try let _ = Notation.level_of_notation "{ _ }" in () with Not_found -> - error "Notations involving patterns of the form \"{ _ }\" are treated \n\ -specially and require that the notation \"{ _ }\" is already reserved." + user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\ +specially and require that the notation \"{ _ }\" is already reserved.") (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) let remove_curly_brackets l = @@ -1081,7 +1081,7 @@ let compute_syntax_data df modifiers = let mods = interp_modifiers modifiers in let onlyprint = mods.only_printing in let onlyparse = mods.only_parsing in - if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'."; + if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); let assoc = Option.append mods.assoc (Some NonA) in let toks = split_notation_string df in let recvars,mainvars,symbols = analyze_notation_tokens toks in @@ -1385,7 +1385,7 @@ let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); with NoSyntaxRule -> - error "Parsing rule for this notation has to be previously declared."); + user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc (* Main entry point *) |