From c216daf5d5f8215947bce10e55d30c35be1a56ba Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 31 Jan 2020 15:57:45 +0100
Subject: [exn] Forbid raising in exn printers, make them return Pp.t option

Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.

We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
---
 tactics/declare.ml | 7 ++++---
 tactics/pfedit.ml  | 4 ++--
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index ce2f3ec2c5..5655bdfd4d 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -24,10 +24,11 @@ exception AlreadyDeclared of (string option * Id.t)
 
 let _ = CErrors.register_handler (function
     | AlreadyDeclared (kind, id) ->
-      seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
-          ; Id.print id; str " already exists."]
+      Some
+        (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
+             ; Id.print id; str " already exists."])
     | _ ->
-      raise CErrors.Unhandled)
+      None)
 
 module NamedDecl = Context.Named.Declaration
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 72204e1d24..dbabc4e4e0 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -26,8 +26,8 @@ let use_unification_heuristics () = !use_unification_heuristics_ref
 
 exception NoSuchGoal
 let () = CErrors.register_handler begin function
-  | NoSuchGoal -> Pp.(str "No such goal.")
-  | _ -> raise CErrors.Unhandled
+  | NoSuchGoal -> Some Pp.(str "No such goal.")
+  | _ -> None
 end
 
 let get_nth_V82_goal p i =
-- 
cgit v1.2.3