Support Proof General

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 29 insertions, 2 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6013a3abfd..4ab85e0e6c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -686,7 +686,7 @@ let check_no_explicitation l =
 
 (* This code is taken from dumpglob, and should be shared with it *)
 let feedback_global loc ref =
-  if !Flags.ide_slave then
+  if !Flags.ide_slave || !Flags.print_emacs then
     let remove_sections dir =
       if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
         Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2f8ab38133..9a26668cd0 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -222,6 +222,7 @@ type 'a stm_vernac =
   | Finish
   | Observe of Stateid.state_id
   | Command of 'a (* An out of flow command not to be recorded by Stm *)
+  | PGLast of 'a (* To ease the life of PG *)
 
 (** {6 Types concerning the module layer} *)
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 97b0ab51c0..33f375a839 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -83,6 +83,7 @@ GEXTEND Gram
       | IDENT "Stm"; IDENT "Observe"; id = INT; "." ->
           VernacStm (Observe (Stateid.state_id_of_int (int_of_string id)))
       | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
+      | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
 
       | v = vernac_aux -> v ] 
     ]
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index eae6d09d69..b5277b62e3 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -482,6 +482,7 @@ let rec pr_vernac = function
   | VernacStm (Observe id) ->
       str"Stm Observe " ++ str(Stateid.string_of_state_id id)
   | VernacStm (Command v) -> str"Stm Command " ++ pr_vernac v
+  | VernacStm (PGLast v) -> str"Stm PGLast " ++ pr_vernac v
 
   (* Proof management *)
   | VernacAbortAll -> str "Abort All"
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index a6d120d5c5..c1376079ec 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -831,6 +831,14 @@ let process_transaction verbosely (loc, expr) =
       | VtUnknown, VtLater ->
           anomaly(str"classifier: VtUnknown must imply VtNow")
     end;
+    (* Proof General *)
+    begin match v with 
+      | VernacStm (PGLast _) ->
+        if head <> VCS.master then
+          interp dummy_state_id
+            (true,Loc.ghost,VernacShow (ShowGoal OpenSubgoals))
+      | _ -> ()
+    end;
     prerr_endline "executed }}}";
     VCS.print ()
   with e ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index dcf2b0b3d7..eb9f4a03d0 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -306,7 +306,9 @@ let do_vernac () =
   msgerrnl (mt ());
   if !print_emacs then msgerr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
-  try Vernac.eval_expr (read_sentence ()); Stm.finish ()
+  try
+    Vernac.eval_expr (read_sentence ());
+    if not !Flags.print_emacs then Stm.finish ()
   with
     | End_of_input | Errors.Quit ->
         msgerrnl (mt ()); pp_flush(); raise Errors.Quit
@@ -331,8 +333,20 @@ let do_vernac () =
     exit the loop are Drop and Quit. Any other exception there indicates
     an issue with [print_toplevel_error] above. *)
 
+let feed_emacs = function
+  | { Interface.id = Interface.State id;
+      Interface.content = Interface.GlobRef (_,a,_,c,_) }  -> 
+    prerr_endline ("<info>" ^"<id>"^Stateid.string_of_state_id id ^"</id>"
+		   ^a^" "^c^ "</info>")
+  | _  -> ()
+
 let rec loop () =
   Sys.catch_break true;
+  if !Flags.print_emacs then begin
+    Pp.set_feeder feed_emacs;
+    Vernacentries.enable_goal_printing := false;
+    Vernacentries.qed_display_script := false;
+  end;
   try
     reset_input_buffer stdin top_buffer;
     while true do do_vernac(); flush_all() done
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml
index d7b9553a0a..46e04d87e1 100644
--- a/toplevel/vernac_classifier.ml
+++ b/toplevel/vernac_classifier.ml
@@ -50,6 +50,7 @@ let rec classify_vernac e =
     | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
     | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
     | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
+    | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
     (* Impossible, Vernac handles these *)
     | VernacList _ -> anomaly (str "VernacList not handled by Vernac")
     | VernacLoad _ -> anomaly (str "VernacLoad not handled by Vernac")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 706b757db4..5316e9d467 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1814,6 +1814,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     | VernacLocal (b, c) when locality = None -> aux ~locality:b isprogcmd c
     | VernacLocal _ -> Errors.error "Locality specified twice"
     | VernacStm (Command c) -> aux ?locality isprogcmd c
+    | VernacStm (PGLast c) -> aux ?locality isprogcmd c
     | VernacStm _ -> assert false (* Done by Stm *)
     | VernacFail v ->
 	begin try