From bff51607cfdda137d7bc55d802895d7f794d5768 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Dec 2014 20:34:09 +0100
Subject: Getting rid of Exninfo hacks.

Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.

To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.

The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
---
 lib/pp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/pp.ml')

diff --git a/lib/pp.ml b/lib/pp.ml
index 44036ca996..81a19d86de 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -360,7 +360,7 @@ let pp_dirs ?pp_tag ft =
     with reraise ->
       let reraise = Backtrace.add_backtrace reraise in
       let () = Format.pp_print_flush ft () in
-      raise reraise
+      Exninfo.iraise reraise
 
 
 
-- 
cgit v1.2.3


From 5ba84979df97996cd04f44e506742bb58ecf0465 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 16 Dec 2014 14:13:59 +0100
Subject: msg_info now puts infomsg tag in emacs mode.

Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.
---
 lib/pp.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'lib/pp.ml')

diff --git a/lib/pp.ml b/lib/pp.ml
index 81a19d86de..fa21506b33 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -370,10 +370,17 @@ let pp_dirs ?pp_tag ft =
 let emacs_quote_start = String.make 1 (Char.chr 254)
 let emacs_quote_end = String.make 1 (Char.chr 255)
 
+let emacs_quote_info_start = "<infomsg>"
+let emacs_quote_info_end = "</infomsg>"
+
 let emacs_quote g =
   if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end
   else hov 0 g
 
+let emacs_quote_info g =
+  if !print_emacs then str emacs_quote_info_start ++ hov 0 g ++ str emacs_quote_info_end
+  else hov 0 g
+
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ?pp_tag ft strm =
@@ -434,10 +441,11 @@ let make_body info s =
 let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm)
 let warnbody strm = make_body (str "Warning:") strm
 let errorbody strm = make_body (str "Error:") strm
+let infobody strm = emacs_quote_info strm
 
 let std_logger ~id:_ level msg = match level with
 | Debug _ -> msgnl (debugbody msg)
-| Info -> msgnl (hov 0 msg)
+| Info -> msgnl (infobody (hov 0 msg))
 | Notice -> msgnl msg
 | Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) ()
 | Error -> msgnl_with !err_ft (errorbody msg)
-- 
cgit v1.2.3