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.
---
 proofs/proof.ml        | 18 +++++++++---------
 proofs/proof_bullet.ml | 10 +++++-----
 2 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index e2ee5426b5..7d0b31734e 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -69,16 +69,16 @@ exception FullyUnfocused
 
 let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
-    Pp.str "This proof is focused, but cannot be unfocused this way"
+    Some (Pp.str "This proof is focused, but cannot be unfocused this way")
   | NoSuchGoals (i,j) when Int.equal i j ->
-    Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
+    Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-    Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
+    Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
   | NoSuchGoal id ->
-    Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+    Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
   | FullyUnfocused ->
-    Pp.str "The proof is not focused"
-  | _ -> raise CErrors.Unhandled
+    Some (Pp.str "The proof is not focused")
+  | _ -> None
 end
 
 let check_cond_kind c k =
@@ -325,9 +325,9 @@ exception OpenProof of Names.Id.t option * open_error_reason
 let _ = CErrors.register_handler begin function
     | OpenProof (pid, reason) ->
       let open Pp in
-      Option.cata (fun pid ->
-          str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason
-    | _ -> raise CErrors.Unhandled
+      Some (Option.cata (fun pid ->
+          str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason)
+    | _ -> None
   end
 
 let warn_remaining_shelved_goals =
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 3ff0533b6b..d978885d62 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -79,8 +79,8 @@ module Strict = struct
       (function
       | FailedBullet (b,sugg) ->
         let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in
-        Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg)
-      | _ -> raise CErrors.Unhandled)
+        Some Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg)
+      | _ -> None)
 
 
   (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
@@ -203,7 +203,7 @@ exception SuggestNoSuchGoals of int * Proof.t
 let _ = CErrors.register_handler begin function
     | SuggestNoSuchGoals(n,proof) ->
       let suffix = suggest proof in
-      Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
-          pr_non_empty_arg (fun x -> x) suffix)
-    | _ -> raise CErrors.Unhandled
+      Some (Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
+                pr_non_empty_arg (fun x -> x) suffix))
+    | _ -> None
   end
-- 
cgit v1.2.3