diff options
| -rw-r--r-- | checker/check.mllib | 4 | ||||
| -rw-r--r-- | dev/printers.mllib | 4 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 5 | ||||
| -rw-r--r-- | lib/clib.mllib | 1 | ||||
| -rw-r--r-- | lib/errors.ml | 10 | ||||
| -rw-r--r-- | lib/errors.mli | 5 | ||||
| -rw-r--r-- | lib/ppstyle.ml (renamed from printing/ppstyle.ml) | 0 | ||||
| -rw-r--r-- | lib/ppstyle.mli (renamed from printing/ppstyle.mli) | 0 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 6 |
10 files changed, 25 insertions, 11 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 1d8ad34682..246fe64dee 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,6 +1,7 @@ Coq_config Hook +Terminal Canary Hashset Hashcons @@ -23,13 +24,14 @@ Pp Segmenttree Unicodetable Unicode -Errors CObj CList CString CArray CStack Util +Ppstyle +Errors Ephemeron Future CUnix diff --git a/dev/printers.mllib b/dev/printers.mllib index 2f78c2e915..74f36f6f5a 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -27,13 +27,14 @@ Pp Segmenttree Unicodetable Unicode -Errors CObj CList CString CArray CStack Util +Ppstyle +Errors Bigint Dyn CUnix @@ -154,7 +155,6 @@ Tok Lexer Ppextend Pputils -Ppstyle Ppannotation Stdarg Constrarg diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 0b168377d9..60ea0df026 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,6 +1,7 @@ Coq_config Hook +Terminal Canary Hashset Hashcons @@ -19,12 +20,14 @@ Serialize Stateid Feedback Pp -Errors + CList CString CArray CStack Util +Ppstyle +Errors Bigint Predicate Segmenttree diff --git a/lib/clib.mllib b/lib/clib.mllib index 2da81c959f..7ff1d29359 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -29,6 +29,7 @@ Util Stateid Feedback Pp +Ppstyle Xml_lexer Xml_parser Xml_printer diff --git a/lib/errors.ml b/lib/errors.ml index c60442654a..c1d224dfcd 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -129,3 +129,13 @@ let handled e = let bottom _ = raise Bottom in try let _ = print_gen bottom !handle_stack e in true with Bottom -> false + +(** Prints info which is either an error or + an anomaly and then exits with the appropriate + error code *) + +let fatal_error info anomaly = + let msg = info ++ fnl () in + pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; + flush_all (); + exit (if anomaly then 129 else 1) diff --git a/lib/errors.mli b/lib/errors.mli index 8320ce409f..e5dad93fd0 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -92,3 +92,8 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool + +(** Prints info which is either an error or + an anomaly and then exits with the appropriate + error code *) +val fatal_error : Pp.std_ppcmds -> bool -> 'a diff --git a/printing/ppstyle.ml b/lib/ppstyle.ml index fb334c706b..fb334c706b 100644 --- a/printing/ppstyle.ml +++ b/lib/ppstyle.ml diff --git a/printing/ppstyle.mli b/lib/ppstyle.mli index f5d6184cb1..f5d6184cb1 100644 --- a/printing/ppstyle.mli +++ b/lib/ppstyle.mli diff --git a/printing/printing.mllib b/printing/printing.mllib index 7b4c71a8b2..652a34fa1f 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,6 +1,5 @@ Genprint Pputils -Ppstyle Ppannotation Ppconstr Ppconstrsig diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 934e73aae9..a04678a1b9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -20,12 +20,6 @@ let () = at_exit flush_all let ( / ) = Filename.concat -let fatal_error info anomaly = - let msg = info ++ fnl () in - pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; - flush_all (); - exit (if anomaly then 129 else 1) - let get_version_date () = try let ch = open_in (Envars.coqlib () / "revision") in |