Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.

This allows fatal_error to be used for printing anomalies at loading time.

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