Mise en place traduction des tactiques apres evaluation pour permettre des changements semantiques

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

2 files changed, 26 insertions, 5 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 909757c0cf..ff674bc0bf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -122,6 +122,26 @@ let set_formatter_translator() =
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
+let pre_printing = function
+  | VernacSolve (i,tac,deftac) when Options.do_translate () ->
+      let (_,env) = Pfedit.get_goal_context i in
+      let t = Options.with_option Options.translate_syntax
+	(Tacinterp.glob_tactic_env [] env) tac in
+      let pfts = Pfedit.get_pftreestate () in
+      let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
+      Some (env,t,Pfedit.focus(),List.length gls)
+  | _ -> None
+
+let post_printing loc (env,t,f,n) = function
+  | VernacSolve (i,_,deftac) ->
+      set_formatter_translator();
+      let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in
+      if !translate_file then begin
+	msg (hov 0 (comment (fst loc) ++ pp ++ comment (snd loc - 1)));
+      end
+      else
+	msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp))
+  | _ -> ()
 
 let pr_new_syntax loc ocom =
   if !translate_file then set_formatter_translator();
@@ -131,10 +151,6 @@ let pr_new_syntax loc ocom =
         Options.v7_only := true;
         mt()
     | Some VernacNop -> mt()
-    | Some (VernacImport (false,[Libnames.Ident (_,a)])) when
-	(* Pour ceux qui ont utilisé la couche "Import *_scope" de compat *)
-	let a = Names.string_of_id a in
-	a = "nat_scope" or a = "Z_scope" or a = "R_scope" -> mt()
     | Some com -> pr_vernac com
     | None -> mt() in
   if !translate_file then
@@ -196,8 +212,10 @@ let rec vernac_com interpfun (loc,com) =
   in 
   try
     Options.v7_only := false;
-    if do_translate () then pr_new_syntax loc (Some com);
+    let pp = pre_printing com in
+    if pp = None & do_translate() then pr_new_syntax loc (Some com);
     interp com;
+    if pp <> None & do_translate() then post_printing loc (out_some pp) com
   with e -> 
     Format.set_formatter_out_channel stdout;
     Options.v7_only := false;
diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli
index a444bb5371..94588f1dfa 100644
--- a/translate/ppvernacnew.mli
+++ b/translate/ppvernacnew.mli
@@ -29,3 +29,6 @@ open Topconstr
 val sep_end : unit -> std_ppcmds
 
 val pr_vernac : vernac_expr -> std_ppcmds
+
+val pr_vernac_solve : 
+  int * Environ.env * Tacexpr.glob_tactic_expr * bool -> std_ppcmds