diff options
Diffstat (limited to 'toplevel/errors.ml')
| -rw-r--r-- | toplevel/errors.ml | 102 |
1 files changed, 51 insertions, 51 deletions
diff --git a/toplevel/errors.ml b/toplevel/errors.ml index 623ebbfbb..da9ae4a4d 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -18,100 +18,100 @@ open Lexer let print_loc loc = if loc = dummy_loc then - [< 'sTR"<unknown>" >] + (str"<unknown>") else - [< 'iNT (fst loc); 'sTR"-"; 'iNT (snd loc) >] + (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = "\""^s^"\"" let where s = - if !Options.debug then [< 'sTR"in "; 'sTR s; 'sTR":"; 'sPC >] else [<>] + if !Options.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) -let report () = [< 'sTR "."; 'sPC; 'sTR "Please report." >] +let report () = (str "." ++ spc () ++ str "Please report.") (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) let rec explain_exn_default = function | Stream.Failure -> - hOV 0 [< 'sTR "Anomaly: Uncaught Stream.Failure." >] + hov 0 (str "Anomaly: Uncaught Stream.Failure.") | Stream.Error txt -> - hOV 0 [< 'sTR "Syntax error: "; 'sTR txt >] + hov 0 (str "Syntax error: " ++ str txt) | Token.Error txt -> - hOV 0 [< 'sTR "Syntax error: "; 'sTR txt >] + hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> - hOV 0 [< 'sTR "Error: OS: "; 'sTR msg >] + hov 0 (str "Error: OS: " ++ str msg) | UserError(s,pps) -> - hOV 1 [< 'sTR"Error: "; where s; pps >] + hov 1 (str"Error: " ++ where s ++ pps) | Out_of_memory -> - hOV 0 [< 'sTR "Out of memory" >] + hov 0 (str "Out of memory") | Stack_overflow -> - hOV 0 [< 'sTR "Stack overflow" >] + hov 0 (str "Stack overflow") | Ast.No_match s -> - hOV 0 [< 'sTR "Anomaly: Ast matching error: "; 'sTR s; report () >] + hov 0 (str "Anomaly: Ast matching error: " ++ str s ++ report ()) | Anomaly (s,pps) -> - hOV 1 [< 'sTR "Anomaly: "; where s; pps; report () >] + hov 1 (str "Anomaly: " ++ where s ++ pps ++ report ()) | Match_failure(filename,pos1,pos2) -> - hOV 1 [< 'sTR "Anomaly: Match failure in file "; - 'sTR (guill filename); 'sTR " from char #"; - 'iNT pos1; 'sTR " to #"; 'iNT pos2; - report () >] + hov 1 (str "Anomaly: Match failure in file " ++ + str (guill filename) ++ str " from char #" ++ + int pos1 ++ str " to #" ++ int pos2 ++ + report ()) | Not_found -> - hOV 0 [< 'sTR "Anomaly: Search error"; report () >] + hov 0 (str "Anomaly: Search error" ++ report ()) | Failure s -> - hOV 0 [< 'sTR "Anomaly: Failure "; 'sTR (guill s); report () >] + hov 0 (str "Anomaly: Failure " ++ str (guill s) ++ report ()) | Invalid_argument s -> - hOV 0 [< 'sTR "Anomaly: Invalid argument "; 'sTR (guill s); report () >] + hov 0 (str "Anomaly: Invalid argument " ++ str (guill s) ++ report ()) | Sys.Break -> - hOV 0 [< 'fNL; 'sTR"User Interrupt." >] + hov 0 (fnl () ++ str"User Interrupt.") | Univ.UniverseInconsistency -> - hOV 0 [< 'sTR "Error: Universe Inconsistency." >] + hov 0 (str "Error: Universe Inconsistency.") | TypeError(ctx,te) -> - hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error ctx te >] + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te) | PretypeError(ctx,te) -> - hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_pretype_error ctx te >] + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te) | InductiveError e -> - hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_inductive_error e >] + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) | Cases.PatternMatchingError (env,e) -> - hOV 0 - [< 'sTR "Error:"; 'sPC; Himsg.explain_pattern_matching_error env e >] + hov 0 + (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) | Logic.RefinerError e -> - hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_refiner_error e >] + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> - hOV 0 [< 'sTR "Error:"; 'sPC; - 'sTR "The reference"; 'sPC; Nametab.pr_qualid q; - 'sPC ; 'sTR "was not found"; - 'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >] + hov 0 (str "Error:" ++ spc () ++ + str "The reference" ++ spc () ++ Nametab.pr_qualid q ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment") | Nametab.GlobalizationConstantError q -> - hOV 0 [< 'sTR "Error:"; 'sPC; - 'sTR "No constant of this name:"; 'sPC; Nametab.pr_qualid q >] + hov 0 (str "Error:" ++ spc () ++ + str "No constant of this name:" ++ spc () ++ Nametab.pr_qualid q) | Tacmach.FailError i -> - hOV 0 [< 'sTR "Error: Fail tactic always fails (level "; - 'iNT i; 'sTR")." >] + hov 0 (str "Error: Fail tactic always fails (level " ++ + int i ++ str").") | Stdpp.Exc_located (loc,exc) -> - hOV 0 [< if loc = Ast.dummy_loc then [<>] - else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >]; - explain_exn_default exc >] + hov 0 (if loc = Ast.dummy_loc then (mt ()) + else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()) ++ + explain_exn_default exc) | Lexer.Error Illegal_character -> - hOV 0 [< 'sTR "Syntax error: Illegal character." >] + hov 0 (str "Syntax error: Illegal character.") | Lexer.Error Unterminated_comment -> - hOV 0 [< 'sTR "Syntax error: Unterminated comment." >] + hov 0 (str "Syntax error: Unterminated comment.") | Lexer.Error Unterminated_string -> - hOV 0 [< 'sTR "Syntax error: Unterminated string." >] + hov 0 (str "Syntax error: Unterminated string.") | Lexer.Error Undefined_token -> - hOV 0 [< 'sTR "Syntax error: Undefined token." >] + hov 0 (str "Syntax error: Undefined token.") | Lexer.Error (Bad_token s) -> - hOV 0 [< 'sTR "Syntax error: Bad token"; 'sPC; 'sTR s; 'sTR "." >] + hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".") | Assert_failure (s,b,e) -> - hOV 0 [< 'sTR "Anomaly: assert failure"; 'sPC; + hov 0 (str "Anomaly: assert failure" ++ spc () ++ if s <> "" then - [< 'sTR ("(file \"" ^ s ^ "\", characters "); - 'iNT b; 'sTR "-"; 'iNT e; 'sTR ")" >] + (str ("(file \"" ^ s ^ "\", characters ") ++ + int b ++ str "-" ++ int e ++ str ")") else - [< >]; - report () >] + (mt ()) ++ + report ()) | reraise -> - hOV 0 [< 'sTR "Anomaly: Uncaught exception "; - 'sTR (Printexc.to_string reraise); report () >] + hov 0 (str "Anomaly: Uncaught exception " ++ + str (Printexc.to_string reraise) ++ report ()) let raise_if_debug e = if !Options.debug then raise e |