Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.

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

Author: tomsib2001

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

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

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

lib/clib.mllib

@@ -29,6 +29,7 @@ Util
 Stateid
 Feedback
 Pp
+Ppstyle
 Xml_lexer
 Xml_parser
 Xml_printer

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)

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

printing/ppstyle.ml renamed to lib/ppstyle.ml

@@ -1,6 +1,5 @@
 Genprint
 Pputils
-Ppstyle
 Ppannotation
 Ppconstr
 Ppconstrsig

printing/ppstyle.mli renamed to lib/ppstyle.mli

@@ -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