From efb6e714097b95a2c6d1de80dde70f5252f90d7f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 10 Sep 2013 16:26:20 +0000
Subject: Temporary fix of emacs mode for ProofGeneral

 To the best of my knowledge, even with the latest cvs version of PG:
  - the goals must be finally displayed at each step
  - the <info>...</info> async feedback messages aren't handled yet.
 I'll check with Enrico what he intended with these two lines,
 but meanwhile let's comment them...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16767 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/toplevel.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index bc50eb43de..ee28156a37 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -343,8 +343,11 @@ let feed_emacs = function
 let rec loop () =
   Sys.catch_break true;
   if !Flags.print_emacs then begin
+    (* TODO : check with Enrico ?! *)
+    (*
     Pp.set_feeder feed_emacs;
     Vernacentries.enable_goal_printing := false;
+    *)
     Vernacentries.qed_display_script := false;
   end;
   try
-- 
cgit v1.2.3