changement nouvelle syntaxe (pt fixes)

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

2 files changed, 22 insertions, 21 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 1211faba0..45af3a3c5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -616,6 +616,9 @@ let make_syntax_rule n name symbols typs ast ntn sc =
     syn_hunks =
       [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}]
 
+let make_pp_rule (n,typs,symbols) =
+  [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
+
 let make_pp_rule (n,typs,symbols,fmt) =
   match fmt with
     | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
@@ -875,7 +878,6 @@ let make_old_pp_rule n symbols typs r ntn scope vars =
 let add_notation_in_scope local df c mods omodv8 scope toks =
   let ((onlyparse,vars,notation),prec,(n,typs,symbols,_ as ppdata)) =
     compute_syntax_data !Options.v7 (df,mods) in
-
   (* Declare the parsing and printing rules if not already done *)
     (* For both v7 and translate: parsing is as described for v7 in v7 file *)
     (* For v8: parsing is as described in v8 file *)
@@ -885,21 +887,23 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
     (* In short: parsing does not depend on omodv8 *)
     (* Printing depends on mv8 if defined, otherwise of mods (scaled by 10) *)
     (* if in v7, or of mods without scaling if in v8 *)
-  let ppprec,pp_rule =
+  let ppnot,ppprec,pp_rule =
     match omodv8 with
-    | Some mv8 -> let _,p,d = compute_syntax_data false mv8 in p,make_pp_rule d
+    | Some mv8 ->
+        let (_,_,ntn8),p,d = compute_syntax_data false mv8 in
+        ntn8,p,make_pp_rule d
     | _ -> 
 	(* means the rule already exists: recover it *)
 	try 
 	  let _, oldprec8 = Symbols.level_of_notation notation in
 	  let rule,_ = Symbols.find_notation_printing_rule notation in
-	  oldprec8,rule
+	  notation,oldprec8,rule
 	with Not_found -> error "No known parsing rule for this notation in V8"
   in
-  let gram_rule = make_grammar_rule n typs symbols notation in
+  let gram_rule = make_grammar_rule n typs symbols ppnot in
   Lib.add_anonymous_leaf
     (inSyntaxExtension
-      (local,(Some prec,ppprec),notation,Some gram_rule,pp_rule));
+      (local,(Some prec,ppprec),ppnot,Some gram_rule,pp_rule));
 
   (* Declare interpretation *)
   let a = interp_aconstr vars c in
@@ -912,7 +916,7 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
   let onlyparse = onlyparse or !Options.v7_only in
   let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
   Lib.add_anonymous_leaf
-    (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,false,df))
+    (inNotation(local,old_pp_rule,ppnot,scope,a,onlyparse,false,df))
 
 let level_rule (n,p) = if p = E then n else max (n-1) 0
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 853b3f594..00020a85a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -100,10 +100,11 @@ let parse_phrase (po, verbch) =
 let just_parsing = ref false
 let chan_translate = ref stdout
 
-
 let pr_new_syntax loc ocom =
-  Format.set_formatter_out_channel !chan_translate;
-  Format.set_max_boxes max_int;
+  if !translate_file then begin
+    Format.set_formatter_out_channel !chan_translate;
+    Format.set_max_boxes max_int;
+  end;
   let fs = States.freeze () in
   let com = match ocom with
     | Some (VernacV7only _) ->
@@ -117,11 +118,7 @@ let pr_new_syntax loc ocom =
     | Some com -> pr_vernac com
     | None -> mt() in
   if !translate_file then
-    msg (hov 0 (
-(*str"{"++int (fst loc)++str"}"++List.fold_right (fun ((b,e),s) strm -> str"("++int b++str","++int
-  e++str":"++str s++str")"++strm)
-  !Pp.comments (mt()) ++*)
-comment (fst loc) ++ com ++ comment (snd loc - 1)))
+    msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
     msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ com));
   States.unfreeze fs;
@@ -135,7 +132,7 @@ let rec vernac_com interpfun (loc,com) =
         let ch = !chan_translate in
         let cs = Lexer.com_state() in
         let cl = !Pp.comments in
-        if Options.do_translate() then begin
+        if !Options.translate_file then begin
           let _,f = find_file_in_path (Library.get_load_path ())
             (make_suffix fname ".v") in
           chan_translate := open_out (f^"8");
@@ -143,12 +140,12 @@ let rec vernac_com interpfun (loc,com) =
         end;
         begin try
           read_vernac_file verbosely (make_suffix fname ".v");
-          if Options.do_translate () then close_out !chan_translate;
+          if !Options.translate_file then close_out !chan_translate;
           chan_translate := ch;
           Lexer.restore_com_state cs;
           Pp.comments := cl
         with e ->
-          if Options.do_translate() then close_out !chan_translate;
+          if !Options.translate_file then close_out !chan_translate;
           chan_translate := ch;
           Lexer.restore_com_state cs;
           Pp.comments := cl;
@@ -221,12 +218,12 @@ let raw_do_vernac po =
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
   chan_translate :=
-    if Options.do_translate () then open_out (file^"8") else stdout;
+    if !Options.translate_file then open_out (file^"8") else stdout;
   try 
     read_vernac_file verb file;
-    if Options.do_translate () then close_out !chan_translate;
+    if !Options.translate_file then close_out !chan_translate;
   with e -> 
-    if Options.do_translate () then close_out !chan_translate;
+    if !Options.translate_file then close_out !chan_translate;
     raise_with_file file e
 
 (* Compile a vernac file (f is assumed without .v suffix) *)