Fixed bug in VernacExtend printing + missing vernacular printing rules +

revival of option -translate as a -beautify option.

PS: compilation checked against 11610.



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

2 files changed, 23 insertions, 22 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2ad5117b9..b2589d42f 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -85,8 +85,8 @@ let add_load_vernacular verb s =
 let load_vernacular () =
   List.iter
     (fun (s,b) -> 
-      if Flags.do_translate () then
-	with_option translate_file (Vernac.load_vernac b) s
+      if Flags.do_beautify () then
+	with_option beautify_file (Vernac.load_vernac b) s
       else
 	Vernac.load_vernac b s)
     (List.rev !load_vernacular_list)
@@ -115,8 +115,8 @@ let compile_files () =
       (fun (v,f) ->
 	 States.unfreeze init_state;
 	 Dumpglob.coqdoc_unfreeze coqdoc_init_state;
-	 if Flags.do_translate () then
-	   with_option translate_file (Vernac.compile v) f
+	 if Flags.do_beautify () then
+	   with_option beautify_file (Vernac.compile v) f
 	 else
 	   Vernac.compile v f)
       (List.rev !compile_list)
@@ -260,7 +260,7 @@ let parse_args is_ide =
 
     | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem
 
-    | "-translate" :: rem -> make_translate true; parse rem
+    | "-beautify" :: rem -> make_beautify true; parse rem
 
     | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
     | "-unsafe" :: []       -> usage ()
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 92d2bbf28..cdfa85328 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -93,23 +93,24 @@ let parse_phrase (po, verbch) =
  * parses, and is verbose on "primitives" commands if verbosely is true *)
 
 let just_parsing = ref false
-let chan_translate = ref stdout
+let chan_beautify = ref stdout
+let beautify_suffix = ".beautified"
 
 let set_formatter_translator() =
-  let ch = !chan_translate in
+  let ch = !chan_beautify 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 pr_new_syntax loc ocom =
   let loc = unloc loc in
-  if !translate_file then set_formatter_translator();
+  if !beautify_file then set_formatter_translator();
   let fs = States.freeze () in
   let com = match ocom with
     | Some VernacNop -> mt()
     | Some com -> pr_vernac com
     | None -> mt() in
-  if !translate_file then
+  if !beautify_file then
     msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
     msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
@@ -121,30 +122,30 @@ let rec vernac_com interpfun (loc,com) =
     | VernacLoad (verbosely, fname) ->
 	let fname = expand_path_macros fname in
         (* translator state *)
-        let ch = !chan_translate in
+        let ch = !chan_beautify in
         let cs = Lexer.com_state() in
         let cl = !Pp.comments in
         (* end translator state *)
         (* coqdoc state *)
         let cds = Dumpglob.coqdoc_freeze() in
-          if !Flags.translate_file then 
+          if !Flags.beautify_file then 
 	    begin
               let _,f = find_file_in_path (Library.get_load_paths ())
 		(make_suffix fname ".v") in
-		chan_translate := open_out (f^"8");
+		chan_beautify := open_out (f^beautify_suffix);
 		Pp.comments := []
             end;
           begin 
 	    try
 	      read_vernac_file verbosely (make_suffix fname ".v");
-              if !Flags.translate_file then close_out !chan_translate;
-              chan_translate := ch;
+              if !Flags.beautify_file then close_out !chan_beautify;
+              chan_beautify := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
               Dumpglob.coqdoc_unfreeze cds
 	    with e -> 
-	      if !Flags.translate_file then close_out !chan_translate;
-              chan_translate := ch;
+	      if !Flags.beautify_file then close_out !chan_beautify;
+              chan_beautify := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
               Dumpglob.coqdoc_unfreeze cds;
@@ -164,7 +165,7 @@ let rec vernac_com interpfun (loc,com) =
 
   in 
     try
-      if do_translate () then pr_new_syntax loc (Some com);
+      if do_beautify () then pr_new_syntax loc (Some com);
       interp com
     with e -> 
       Format.set_formatter_out_channel stdout;
@@ -191,7 +192,7 @@ and read_vernac_file verbosely s =
     close_input in_chan input;    (* we must close the file first *)
     match real_error e with
       | End_of_input ->
-          if do_translate () then pr_new_syntax (make_loc (max_int,max_int)) None
+          if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname e
 
 (* raw_do_vernac : char Stream.t -> unit
@@ -214,13 +215,13 @@ let set_xml_end_library f = xml_end_library := f
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
-  chan_translate :=
-    if !Flags.translate_file then open_out (file^"8") else stdout;
+  chan_beautify :=
+    if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try 
     read_vernac_file verb file;
-    if !Flags.translate_file then close_out !chan_translate;
+    if !Flags.beautify_file then close_out !chan_beautify;
   with e -> 
-    if !Flags.translate_file then close_out !chan_translate;
+    if !Flags.beautify_file then close_out !chan_beautify;
     raise_with_file file e
 
 (* Compile a vernac file (f is assumed without .v suffix) *)