From b7aa648034f73c390ba2b49c8d47c3c8277002ef Mon Sep 17 00:00:00 2001 From: ddr Date: Wed, 20 Feb 2002 11:06:07 +0000 Subject: Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce qu'il entre en conflit avec le module Errors ajouté dans OCaml courant (future version OCaml 3.05). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2489 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 38 ++++++------- Makefile | 4 +- contrib/interface/centaur.ml | 2 +- contrib/interface/debug_tac.ml | 2 +- contrib/interface/parse.ml | 18 +++--- dev/top_printers.ml | 2 +- toplevel/cerrors.ml | 121 +++++++++++++++++++++++++++++++++++++++++ toplevel/cerrors.mli | 24 ++++++++ toplevel/coqtop.ml | 4 +- toplevel/errors.ml | 121 ----------------------------------------- toplevel/errors.mli | 24 -------- toplevel/protectedtoplevel.ml | 4 +- toplevel/toplevel.ml | 8 +-- 13 files changed, 186 insertions(+), 186 deletions(-) create mode 100644 toplevel/cerrors.ml create mode 100644 toplevel/cerrors.mli delete mode 100644 toplevel/errors.ml delete mode 100644 toplevel/errors.mli diff --git a/.depend b/.depend index 77449ac257..e34be00fb2 100644 --- a/.depend +++ b/.depend @@ -211,7 +211,7 @@ toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \ pretyping/tacred.cmi kernel/term.cmi toplevel/coqinit.cmi: kernel/names.cmi toplevel/discharge.cmi: kernel/names.cmi -toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi +toplevel/cerrors.cmi: parsing/coqast.cmi lib/pp.cmi toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi toplevel/himsg.cmi: pretyping/cases.cmi kernel/environ.cmi \ @@ -320,13 +320,13 @@ config/coq_config.cmx: config/coq_config.cmi dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx dev/top_printers.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/environ.cmi \ - toplevel/errors.cmi pretyping/evd.cmi library/nameops.cmi \ + toplevel/cerrors.cmi pretyping/evd.cmi library/nameops.cmi \ kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi lib/system.cmi \ proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \ pretyping/termops.cmi kernel/univ.cmi dev/top_printers.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/environ.cmx \ - toplevel/errors.cmx pretyping/evd.cmx library/nameops.cmx \ + toplevel/cerrors.cmx pretyping/evd.cmx library/nameops.cmx \ kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \ proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \ @@ -1404,13 +1404,13 @@ toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \ lib/system.cmx toplevel/toplevel.cmx toplevel/vernac.cmx \ toplevel/coqinit.cmi toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \ - toplevel/errors.cmi library/lib.cmi library/library.cmi \ + toplevel/cerrors.cmi library/lib.cmi library/library.cmi \ toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi lib/options.cmi lib/pp.cmi lib/profile.cmi \ library/states.cmi lib/system.cmi toplevel/toplevel.cmi \ toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \ - toplevel/errors.cmx library/lib.cmx library/library.cmx \ + toplevel/cerrors.cmx library/lib.cmx library/library.cmx \ toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx lib/options.cmx lib/pp.cmx lib/profile.cmx \ library/states.cmx lib/system.cmx toplevel/toplevel.cmx \ @@ -1433,16 +1433,16 @@ toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \ lib/pp.cmx toplevel/recordobj.cmx pretyping/recordops.cmx \ kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx toplevel/discharge.cmi -toplevel/errors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ +toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ kernel/indtypes.cmi parsing/lexer.cmi proofs/logic.cmi \ library/nametab.cmi lib/options.cmi lib/pp.cmi \ pretyping/pretype_errors.cmi proofs/tacmach.cmi kernel/type_errors.cmi \ - kernel/univ.cmi lib/util.cmi toplevel/errors.cmi -toplevel/errors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \ + kernel/univ.cmi lib/util.cmi toplevel/cerrors.cmi +toplevel/cerrors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \ kernel/indtypes.cmx parsing/lexer.cmx proofs/logic.cmx \ library/nametab.cmx lib/options.cmx lib/pp.cmx \ pretyping/pretype_errors.cmx proofs/tacmach.cmx kernel/type_errors.cmx \ - kernel/univ.cmx lib/util.cmx toplevel/errors.cmi + kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.cmi \ kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi @@ -1489,11 +1489,11 @@ toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \ kernel/names.cmx lib/options.cmx lib/pp.cmx library/summary.cmx \ lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/mltop.cmi -toplevel/protectedtoplevel.cmo: toplevel/errors.cmi \ +toplevel/protectedtoplevel.cmo: toplevel/cerrors.cmi \ toplevel/line_oriented_parser.cmi parsing/pcoq.cmi lib/pp.cmi \ toplevel/vernac.cmi toplevel/vernacinterp.cmi \ toplevel/protectedtoplevel.cmi -toplevel/protectedtoplevel.cmx: toplevel/errors.cmx \ +toplevel/protectedtoplevel.cmx: toplevel/cerrors.cmx \ toplevel/line_oriented_parser.cmx parsing/pcoq.cmx lib/pp.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx \ toplevel/protectedtoplevel.cmi @@ -1525,11 +1525,11 @@ toplevel/recordobj.cmx: pretyping/classops.cmx library/declare.cmx \ library/lib.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \ lib/pp.cmx pretyping/recordops.cmx kernel/term.cmx pretyping/termops.cmx \ lib/util.cmx toplevel/recordobj.cmi -toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi library/lib.cmi \ +toplevel/toplevel.cmo: parsing/ast.cmi toplevel/cerrors.cmi library/lib.cmi \ toplevel/mltop.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ proofs/pfedit.cmi lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \ toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi -toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \ +toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \ toplevel/mltop.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ proofs/pfedit.cmx lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi @@ -1970,7 +1970,7 @@ contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ toplevel/command.cmi parsing/coqast.cmi contrib/interface/ctast.cmo \ contrib/interface/dad.cmi contrib/interface/debug_tac.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - toplevel/errors.cmi pretyping/evd.cmi library/global.cmi \ + toplevel/cerrors.cmi pretyping/evd.cmi library/global.cmi \ contrib/interface/history.cmi library/lib.cmi library/libobject.cmi \ library/library.cmi toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \ contrib/interface/name_to_ast.cmi library/nameops.cmi kernel/names.cmi \ @@ -1989,7 +1989,7 @@ contrib/interface/centaur.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \ toplevel/command.cmx parsing/coqast.cmx contrib/interface/ctast.cmx \ contrib/interface/dad.cmx contrib/interface/debug_tac.cmx \ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - toplevel/errors.cmx pretyping/evd.cmx library/global.cmx \ + toplevel/cerrors.cmx pretyping/evd.cmx library/global.cmx \ contrib/interface/history.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \ contrib/interface/name_to_ast.cmx library/nameops.cmx kernel/names.cmx \ @@ -2024,11 +2024,11 @@ contrib/interface/dad.cmx: parsing/astterm.cmx contrib/interface/ctast.cmx \ parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/interface/dad.cmi contrib/interface/debug_tac.cmo: parsing/ast.cmi parsing/coqast.cmi \ - toplevel/errors.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + toplevel/cerrors.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ lib/util.cmi contrib/interface/debug_tac.cmi contrib/interface/debug_tac.cmx: parsing/ast.cmx parsing/coqast.cmx \ - toplevel/errors.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + toplevel/cerrors.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ proofs/proof_type.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ lib/util.cmx contrib/interface/debug_tac.cmi contrib/interface/history.cmo: contrib/interface/paths.cmi \ @@ -2054,14 +2054,14 @@ contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \ pretyping/syntax_def.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ contrib/interface/name_to_ast.cmi contrib/interface/parse.cmo: contrib/interface/ascent.cmi \ - config/coq_config.cmi contrib/interface/ctast.cmo toplevel/errors.cmi \ + config/coq_config.cmi contrib/interface/ctast.cmo toplevel/cerrors.cmi \ parsing/esyntax.cmi library/libobject.cmi library/library.cmi \ contrib/interface/line_parser.cmi toplevel/metasyntax.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi \ lib/pp.cmi lib/system.cmi lib/util.cmi contrib/interface/vtp.cmi \ contrib/interface/xlate.cmi contrib/interface/parse.cmx: contrib/interface/ascent.cmi \ - config/coq_config.cmx contrib/interface/ctast.cmx toplevel/errors.cmx \ + config/coq_config.cmx contrib/interface/ctast.cmx toplevel/cerrors.cmx \ parsing/esyntax.cmx library/libobject.cmx library/library.cmx \ contrib/interface/line_parser.cmx toplevel/metasyntax.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx \ diff --git a/Makefile b/Makefile index b48cca2db2..7be6b4c2c9 100644 --- a/Makefile +++ b/Makefile @@ -122,7 +122,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ tactics/tacticals.cmo tactics/tactics.cmo tactics/tacentries.cmo \ tactics/hiddentac.cmo tactics/elim.cmo -TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo \ +TOPLEVEL=toplevel/himsg.cmo toplevel/cerrors.cmo \ toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \ toplevel/record.cmo toplevel/recordobj.cmo \ toplevel/discharge.cmo toplevel/vernacinterp.cmo toplevel/mltop.cmo \ @@ -189,7 +189,7 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \ proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \ proofs/evar_refiner.cmo proofs/tacmach.cmo toplevel/himsg.cmo \ parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \ - toplevel/errors.cmo + toplevel/cerrors.cmo ML4FILES += contrib/correctness/psyntax.ml4 contrib/field/field.ml4 diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml index 1cd2070479..6f5281d565 100644 --- a/contrib/interface/centaur.ml +++ b/contrib/interface/centaur.ml @@ -102,7 +102,7 @@ let ctf_acknowledge_command request_id command_count opt_exn = int goal_index ++ fnl () ++ str !current_proof_name ++ fnl() ++ (match opt_exn with - Some e -> Errors.explain_exn e + Some e -> Cerrors.explain_exn e | None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; let ctf_undoResults = ctf_header "undo_results";; diff --git a/contrib/interface/debug_tac.ml b/contrib/interface/debug_tac.ml index 80d9d72018..be469108fb 100644 --- a/contrib/interface/debug_tac.ml +++ b/contrib/interface/debug_tac.ml @@ -463,7 +463,7 @@ let descr_first_error = function with e -> (msgnl (str "Execution of this tactic raised message " ++ fnl () ++ - fnl () ++ Errors.explain_exn e ++ fnl () ++ + fnl () ++ Cerrors.explain_exn e ++ fnl () ++ fnl () ++ str "on goal" ++ fnl () ++ pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++ str "faulty tactic is" ++ fnl () ++ fnl () ++ diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index f68628eab6..389fa8cda8 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -171,7 +171,7 @@ let parse_command_list reqid stream string_list = with | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> begin - msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e)); + msgnl (ctf_SyntaxWarningMessage reqid (Cerrors.explain_exn e)); try discard_to_dot stream; msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ @@ -244,11 +244,11 @@ let parse_string_action reqid phylum char_stream string_list = | Stdpp.Exc_located(l,Match_failure(_,_,_)) -> flush_until_end_of_stream char_stream; msgnl (ctf_SyntaxErrorMessage reqid - (Errors.explain_exn + (Cerrors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")))) | e -> flush_until_end_of_stream char_stream; - msgnl (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));; + msgnl (ctf_SyntaxErrorMessage reqid (Cerrors.explain_exn e));; let quiet_parse_string_action char_stream = @@ -282,7 +282,7 @@ let parse_file_action reqid file_name = msgnl (ctf_SyntaxWarningMessage reqid (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ - Errors.explain_exn + Cerrors.explain_exn (Stdpp.Exc_located(l,Stream.Error txt)))); (try begin @@ -328,13 +328,13 @@ let parse_file_action reqid file_name = (ctf_SyntaxErrorMessage reqid (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ - Errors.explain_exn + Cerrors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")))) | e -> msgnl (ctf_SyntaxErrorMessage reqid (str "Error with file" ++ spc () ++ str file_name ++ - fnl () ++ Errors.explain_exn e));; + fnl () ++ Cerrors.explain_exn e));; (* This function is taken from Mltop.add_path *) @@ -442,7 +442,7 @@ Libobject.relax true; with | End_of_file -> () | e -> - (msgnl (Errors.explain_exn e); + (msgnl (Cerrors.explain_exn e); msgnl (str "could not load the VERNACRC file")); try msgnl (str vernacrc) @@ -459,11 +459,11 @@ Libobject.relax true; with | End_of_file -> () | e -> - msgnl (Errors.explain_exn e); + msgnl (Cerrors.explain_exn e); msgnl (str "error in your .vernacrc file")); msgnl (str "Starting Centaur Specialized Parser Loop"); try coqparser_loop stdin with | End_of_file -> () - | e -> msgnl(Errors.explain_exn e)) + | e -> msgnl(Cerrors.explain_exn e)) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6d7a6b3675..b179428845 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -23,7 +23,7 @@ open Tacmach open Term open Termops open Clenv -open Errors +open Cerrors let _ = Termast.print_evar_arguments := true diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml new file mode 100644 index 0000000000..da9ae4a4de --- /dev/null +++ b/toplevel/cerrors.ml @@ -0,0 +1,121 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ") + else + (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 (mt ()) + +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.") + | Stream.Error txt -> + hov 0 (str "Syntax error: " ++ str txt) + | Token.Error txt -> + hov 0 (str "Syntax error: " ++ str txt) + | Sys_error msg -> + hov 0 (str "Error: OS: " ++ str msg) + | UserError(s,pps) -> + hov 1 (str"Error: " ++ where s ++ pps) + | Out_of_memory -> + hov 0 (str "Out of memory") + | Stack_overflow -> + hov 0 (str "Stack overflow") + | Ast.No_match s -> + hov 0 (str "Anomaly: Ast matching error: " ++ str s ++ report ()) + | Anomaly (s,pps) -> + 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 ()) + | Not_found -> + hov 0 (str "Anomaly: Search error" ++ report ()) + | Failure s -> + hov 0 (str "Anomaly: Failure " ++ str (guill s) ++ report ()) + | Invalid_argument s -> + hov 0 (str "Anomaly: Invalid argument " ++ str (guill s) ++ report ()) + | Sys.Break -> + hov 0 (fnl () ++ str"User Interrupt.") + | Univ.UniverseInconsistency -> + hov 0 (str "Error: Universe Inconsistency.") + | TypeError(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) + | InductiveError 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) + | Logic.RefinerError 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") + | Nametab.GlobalizationConstantError 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").") + | Stdpp.Exc_located (loc,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.") + | Lexer.Error Unterminated_comment -> + hov 0 (str "Syntax error: Unterminated comment.") + | Lexer.Error Unterminated_string -> + hov 0 (str "Syntax error: Unterminated string.") + | Lexer.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 ".") + | Assert_failure (s,b,e) -> + hov 0 (str "Anomaly: assert failure" ++ spc () ++ + if s <> "" then + (str ("(file \"" ^ s ^ "\", characters ") ++ + int b ++ str "-" ++ int e ++ str ")") + else + (mt ()) ++ + report ()) + | reraise -> + hov 0 (str "Anomaly: Uncaught exception " ++ + str (Printexc.to_string reraise) ++ report ()) + +let raise_if_debug e = + if !Options.debug then raise e + +let explain_exn_function = ref explain_exn_default + +let explain_exn e = !explain_exn_function e diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli new file mode 100644 index 0000000000..2207608a87 --- /dev/null +++ b/toplevel/cerrors.mli @@ -0,0 +1,24 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds + +val explain_exn : exn -> std_ppcmds + +val explain_exn_function : (exn -> std_ppcmds) ref +val explain_exn_default : exn -> std_ppcmds + +val raise_if_debug : exn -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b273034df9..c174877dff 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -206,9 +206,9 @@ let parse_args () = try Stream.empty s; exit 1 with Stream.Failure -> - msgnl (Errors.explain_exn e); exit 1 + msgnl (Cerrors.explain_exn e); exit 1 end - | e -> begin msgnl (Errors.explain_exn e); exit 1 end + | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end (* To prevent from doing the initialization twice *) diff --git a/toplevel/errors.ml b/toplevel/errors.ml deleted file mode 100644 index da9ae4a4de..0000000000 --- a/toplevel/errors.ml +++ /dev/null @@ -1,121 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ") - else - (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 (mt ()) - -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.") - | Stream.Error txt -> - hov 0 (str "Syntax error: " ++ str txt) - | Token.Error txt -> - hov 0 (str "Syntax error: " ++ str txt) - | Sys_error msg -> - hov 0 (str "Error: OS: " ++ str msg) - | UserError(s,pps) -> - hov 1 (str"Error: " ++ where s ++ pps) - | Out_of_memory -> - hov 0 (str "Out of memory") - | Stack_overflow -> - hov 0 (str "Stack overflow") - | Ast.No_match s -> - hov 0 (str "Anomaly: Ast matching error: " ++ str s ++ report ()) - | Anomaly (s,pps) -> - 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 ()) - | Not_found -> - hov 0 (str "Anomaly: Search error" ++ report ()) - | Failure s -> - hov 0 (str "Anomaly: Failure " ++ str (guill s) ++ report ()) - | Invalid_argument s -> - hov 0 (str "Anomaly: Invalid argument " ++ str (guill s) ++ report ()) - | Sys.Break -> - hov 0 (fnl () ++ str"User Interrupt.") - | Univ.UniverseInconsistency -> - hov 0 (str "Error: Universe Inconsistency.") - | TypeError(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) - | InductiveError 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) - | Logic.RefinerError 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") - | Nametab.GlobalizationConstantError 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").") - | Stdpp.Exc_located (loc,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.") - | Lexer.Error Unterminated_comment -> - hov 0 (str "Syntax error: Unterminated comment.") - | Lexer.Error Unterminated_string -> - hov 0 (str "Syntax error: Unterminated string.") - | Lexer.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 ".") - | Assert_failure (s,b,e) -> - hov 0 (str "Anomaly: assert failure" ++ spc () ++ - if s <> "" then - (str ("(file \"" ^ s ^ "\", characters ") ++ - int b ++ str "-" ++ int e ++ str ")") - else - (mt ()) ++ - report ()) - | reraise -> - hov 0 (str "Anomaly: Uncaught exception " ++ - str (Printexc.to_string reraise) ++ report ()) - -let raise_if_debug e = - if !Options.debug then raise e - -let explain_exn_function = ref explain_exn_default - -let explain_exn e = !explain_exn_function e diff --git a/toplevel/errors.mli b/toplevel/errors.mli deleted file mode 100644 index 2207608a87..0000000000 --- a/toplevel/errors.mli +++ /dev/null @@ -1,24 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* std_ppcmds - -val explain_exn : exn -> std_ppcmds - -val explain_exn_function : (exn -> std_ppcmds) ref -val explain_exn_default : exn -> std_ppcmds - -val raise_if_debug : exn -> unit diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index 730b6768db..0e28a8373f 100644 --- a/toplevel/protectedtoplevel.ml +++ b/toplevel/protectedtoplevel.ml @@ -55,7 +55,7 @@ let acknowledge_command_ref = str "successfully executed " ++ int command_count ++ fnl () ++ str "error message" ++ fnl () ++ (match opt_exn with - Some e -> Errors.explain_exn e + Some e -> Cerrors.explain_exn e | None -> (mt ())) ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ())) @@ -151,7 +151,7 @@ let rec parse_one_command_group input_channel = let protected_loop input_chan = let rec explain_and_restart e = begin - output_results_nl(Errors.explain_exn e); + output_results_nl(Cerrors.explain_exn e); rearm_break(); looprec input_chan; end diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 8bd6ba8e4a..29c0e60551 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -11,7 +11,7 @@ open Pp open Util open Options -open Errors +open Cerrors open Vernac open Pcoq open Protectedtoplevel @@ -124,7 +124,7 @@ let print_highlight_location ib (bp,ep) = str sn ++ str dn) in (l1 ++ li ++ ln) in - (str"Toplevel input, characters " ++ Errors.print_loc (bp,ep) ++ fnl () ++ + (str"Toplevel input, characters " ++ Cerrors.print_loc (bp,ep) ++ fnl () ++ highlight_lines ++ fnl ()) (* Functions to report located errors in a file. *) @@ -147,7 +147,7 @@ let print_location_in_file s fname (bp,ep) = let (line, bol) = line_of_pos 1 0 0 in close_in ic; (errstrm ++ str", line " ++ int line ++ - str", characters " ++ Errors.print_loc (bp-bol,ep-bol) ++ fnl ()) + str", characters " ++ Cerrors.print_loc (bp-bol,ep-bol) ++ fnl ()) with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ())) let print_command_location ib dloc = @@ -235,7 +235,7 @@ let print_toplevel_error exc = raise Vernacinterp.Quit | _ -> (if is_pervasive_exn exc then (mt ()) else locstrm) ++ - Errors.explain_exn exc + Cerrors.explain_exn exc (* Read the input stream until a dot is encountered *) let parse_to_dot = -- cgit v1.2.3