Merge PR #11408: [mltop] Remove error handling hacks in favor of default methods.

Reviewed-by: ppedrot

3 files changed, 25 insertions, 35 deletions

diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml
index aaabd90370..85d8a48eda 100644
--- a/topbin/coqtop_byte_bin.ml
+++ b/topbin/coqtop_byte_bin.ml
@@ -8,6 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* We register this handler for lower-level toplevel loading code *)
+let _ = CErrors.register_handler (function
+    | Symtable.Error e ->
+      Pp.str (Format.asprintf "%a" Symtable.report_error e)
+    | _ ->
+      raise CErrors.Unhandled
+  )
+
 let drop_setup () =
   begin try
     (* Enable rectypes in the toplevel if it has the directive #rectypes *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ba7ae5069b..eb39564fed 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1364,7 +1364,6 @@ let explain_exn_default = function
   | Sys_error msg -> hov 0 (str "System error: " ++ quote (str msg))
   | Out_of_memory -> hov 0 (str "Out of memory.")
   | Stack_overflow -> hov 0 (str "Stack overflow.")
-  | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
   | CErrors.Timeout -> hov 0 (str "Timeout!")
   | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
   (* Otherwise, not handled here *)
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 9c18441d9c..6621c1e6b1 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -94,43 +94,26 @@ let ocaml_toploop () =
     | WithTop t -> Printexc.catch t.ml_loop ()
     | _ -> ()
 
-(* Try to interpret load_obj's (internal) errors *)
-let report_on_load_obj_error exc =
-  let x = Obj.repr exc in
-  (* Try an horrible (fragile) hack to report on Symtable dynlink errors *)
-  (* (we follow ocaml's Printexc.to_string decoding of exceptions) *)
-  if Obj.is_block x && String.equal (Obj.magic (Obj.field (Obj.field x 0) 0)) "Symtable.Error"
-  then
-    let err_block = Obj.field x 1 in
-    if Int.equal (Obj.tag err_block) 0 then
-      (* Symtable.Undefined_global of string *)
-      str "reference to undefined global " ++
-      str (Obj.magic (Obj.field err_block 0))
-    else str (Printexc.to_string exc)
-  else str (Printexc.to_string exc)
-
 (* Dynamic loading of .cmo/.cma *)
 
+(* We register errors at least for Dynlink, it is possible to do so Symtable
+   too, as we do in the bytecode init code.
+*)
+let _ = CErrors.register_handler (function
+    | Dynlink.Error e ->
+      hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
+    | _ ->
+      raise CErrors.Unhandled
+  )
+
 let ml_load s =
-  match !load with
-    | WithTop t ->
-      (try t.load_obj s; s
-       with
-       | e when CErrors.noncritical e ->
-        let e = CErrors.push e in
-        match fst e with
-        | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e)
-        | exc ->
-            let msg = report_on_load_obj_error exc in
-            user_err ~hdr:"Mltop.load_object" (str"Cannot link ml-object " ++
-                  str s ++ str" to Coq code (" ++ msg ++ str ")."))
-    | WithoutTop ->
-        try
-          Dynlink.loadfile s; s
-        with Dynlink.Error a ->
-          user_err ~hdr:"Mltop.load_object"
-            (strbrk "while loading " ++ str s ++
-             strbrk ": " ++ str (Dynlink.error_message a))
+  (match !load with
+   | WithTop t ->
+     t.load_obj s
+   | WithoutTop ->
+     Dynlink.loadfile s
+  );
+  s
 
 let dir_ml_load s =
   match !load with