Autres suppressions de composantes du traducteur

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

4 files changed, 12 insertions, 97 deletions

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 0a3a3c92b5..f54904fa31 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -25,7 +25,7 @@ GEXTEND Gram
   GLOBAL: 
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference
-    ne_string;
+    ne_string string;
   preident:
     [ [ s = IDENT -> s ] ]
   ;
@@ -74,6 +74,9 @@ GEXTEND Gram
         if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s
     ] ]
   ;
+  string:
+    [ [ s = STRING -> s ] ]
+  ;
   integer:
     [ [ i = INT      -> int_of_string i
       | "-"; i = INT -> - int_of_string i ] ]
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b8a73b37f2..f7782d6d53 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -69,8 +69,7 @@ let pr_gen env t =
     pr_lconstr
     (pr_raw_tactic_level env) pr_reference t
 
-let pr_raw_tactic tac =
-  pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic tac)
+let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac
 
 let rec extract_signature = function
   | [] -> []
@@ -376,34 +375,6 @@ let pr_paren_reln_or_extern = function
   | Some pprim,Any -> qsnew pprim
   | Some pprim,Prec p -> qsnew pprim ++ spc() ++ str":" ++ spc() ++ int p
   | _ -> mt()
-(*
-let rec pr_next_hunks = function 
-  | UNP_FNL -> str"FNL"
-  | UNP_TAB -> str"TAB"
-  | RO c -> qsnew c
-  | UNP_BOX (b,ll) -> str"[" ++ pr_box b ++ prlist_with_sep sep pr_next_hunks ll ++ str"]"
-  | UNP_BRK (n,m) -> str"[" ++ int n ++ spc() ++ int m ++ str"]"
-  | UNP_TBRK (n,m) -> str"[ TBRK" ++ int n ++ spc() ++ int m ++ str"]"
-  | PH (e,None,_) -> print_ast e
-  | PH (e,Some ext,pr) -> print_ast e ++ spc() ++ str":" ++ spc() ++ pr_paren_reln_or_extern (Some ext,pr)
-  | UNP_SYMBOLIC _ -> mt()
-
-let pr_unparsing u =
-  str "[ " ++ prlist_with_sep sep pr_next_hunks u ++ str " ]"
-
-let pr_astpat a = str"<<" ++ print_ast a ++ str">>"
-
-let pr_syntax_rule (nm,s,u) = str nm ++ spc() ++ str"[" ++ pr_astpat s ++ str"]" ++ spc() ++ str"->" ++ spc() ++ pr_unparsing u
-
-let pr_syntax_entry (p,rl) =
-  str"level" ++ spc() ++ int p ++ str" :" ++ fnl() ++
-  prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_syntax_rule rl
-*)
-let pr_vernac_solve (i,env,tac,deftac) =
-  (if i = 1 then mt() else int i ++ str ": ") ++
-  pr_glob_tactic env tac
-  ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
-      with UserError _|Stdpp.Exc_located _ -> mt())
 
 (**************************************)
 (* Pretty printer for vernac commands *)
@@ -708,14 +679,10 @@ let rec pr_vernac = function
 
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
-      (* Normally shunted by vernac.ml *)
-      let env =
-        try snd (Pfedit.get_goal_context i)
-        with UserError _ -> Global.env() in
-      let tac = 
-	Options.with_option Options.translate_syntax 
-	  (Constrintern.for_grammar (Tacinterp.glob_tactic_env [] env)) tac in
-      pr_vernac_solve (i,env,tac,deftac)
+      (if i = 1 then mt() else int i ++ str ": ") ++
+      pr_raw_tactic tac
+      ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
+      with UserError _|Stdpp.Exc_located _ -> mt())
 
   | VernacSolveExistential (i,c) ->
       str"Existential " ++ int i ++ pr_lconstrarg c
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli
index e76f1b579b..48e3698d43 100644
--- a/parsing/ppvernac.mli
+++ b/parsing/ppvernac.mli
@@ -26,6 +26,3 @@ 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
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8a2cb41759..d44227a808 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -94,53 +94,13 @@ let parse_phrase (po, verbch) =
 
 let just_parsing = ref false
 let chan_translate = ref stdout
-let last_char = ref '\000'
 
-(* postprocessor to avoid lexical icompatibilities between V7 and V8.
-   Ex: auto.(* comment *)  or  simpl.auto
- *)
 let set_formatter_translator() =
   let ch = !chan_translate in
-  let out s b e =
-    let n = e-b in
-    if n > 0 then begin
-      (match !last_char with
-          '.' -> 
-            (match s.[b] with
-                '('|'a'..'z'|'A'..'Z' -> output ch " " 0 1 
-              | _ -> ())
-        | _ -> ());
-      last_char := s.[e-1]
-    end;
-    output ch s b e
-  in
+  let out s b e = output ch s b e in
   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 () ->
-      (try
-        let (_,env) = Pfedit.get_goal_context i in
-        let t = 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)
-      with UserError _|Stdpp.Exc_located _ -> None)
-  | _ -> None
-
-let post_printing loc (env,t,f,n) = function
-  | VernacSolve (i,_,deftac) ->
-      let loc = unloc loc in
-      set_formatter_translator();
-      let pp = Ppvernac.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)));
-      Format.set_formatter_out_channel stdout
-  | _ -> ()
-
 let pr_new_syntax loc ocom =
   let loc = unloc loc in
   if !translate_file then set_formatter_translator();
@@ -200,20 +160,8 @@ let rec vernac_com interpfun (loc,com) =
 
   in 
   try
-    if do_translate () then
-      match pre_printing com with
-          None ->
-            pr_new_syntax loc (Some com);
-            interp com
-        | Some state ->
-            (try
-              interp com;
-              post_printing loc state com
-            with e ->
-              post_printing loc state com;
-              raise e)
-    else
-      interp com
+    if do_translate () then pr_new_syntax loc (Some com);
+    interp com
   with e -> 
     Format.set_formatter_out_channel stdout;
     raise (DuringCommandInterp (loc, e))