diff options
| author | letouzey | 2013-09-10 16:26:20 +0000 |
|---|---|---|
| committer | letouzey | 2013-09-10 16:26:20 +0000 |
| commit | efb6e714097b95a2c6d1de80dde70f5252f90d7f (patch) | |
| tree | a468fc7981c0c6475d59337055498e1916a43de8 | |
| parent | ea37ffa0d9c1bf2e18f843fd2fddba32b7b04de8 (diff) | |
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
| -rw-r--r-- | toplevel/toplevel.ml | 3 |
1 files changed, 3 insertions, 0 deletions
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 |