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

5 files changed, 33 insertions, 21 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 770a54a78e..7f2a6dd482 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -163,16 +163,27 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl =
     end
   >>
 
-let declare_vernac_argument loc s cl =
+let declare_vernac_argument loc s pr cl =
   let se = mlexpr_of_string s in
+  let wit = <:expr< $lid:"wit_"^s$ >> in
   let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
+  let globwit = <:expr< $lid:"globwit_"^s$ >> in
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+  let pr_rules = match pr with
+    | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >>
+    | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in
   <:str_item<
     declare
-      value $lid:"rawwit_"^s$ = let (_,_,x) = Genarg.create_arg $se$ in x;
+      value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
+             ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
+              $lid:"rawwit_"^s$) = Genarg.create_arg $se$;
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
       Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None 
         [(None, None, $rules$)];
+      Pptactic.declare_extra_genarg_pprule
+        ($rawwit$, $pr_rules$)
+        ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer")
+        ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer");
     end
   >>
 
@@ -202,11 +213,12 @@ EXTEND
 	    failwith "Argument entry names must be lowercase";
          declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l
       | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+        pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr];
         OPT "|"; l = LIST1 argrule SEP "|";
         "END" ->
 	  if String.capitalize s = s then
 	    failwith "Argument entry names must be lowercase";
-         declare_vernac_argument loc s l ] ]
+         declare_vernac_argument loc s pr l ] ]
   ;
   argtype:
     [ "2" 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 26377013f0..5984f7415d 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -237,7 +237,7 @@ let rec string bp len = parser
 let xml_output_comment = ref (fun _ -> ())
 let set_xml_output_comment f = xml_output_comment := f
 
-(* Utilities for comment translation *)
+(* Utilities for comments in beautify *)
 let comment_begin = ref None
 let comm_loc bp = if !comment_begin=None then comment_begin := Some bp
 
@@ -280,7 +280,7 @@ let comment_stop ep =
   if !Flags.xml_export && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
       !xml_output_comment current_s;
-  (if Flags.do_translate() && Buffer.length current > 0 &&
+  (if Flags.do_beautify() && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
@@ -315,7 +315,7 @@ let rec comment bp = parser bp2
          | [< '')' >] -> push_string "*)";
          | [< s >] -> real_push_char '*'; comment bp s >] -> ()
   | [< ''"'; s >] ->
-      if Flags.do_translate() then (push_string"\"";comm_string bp2 s)
+      if Flags.do_beautify() then (push_string"\"";comm_string bp2 s)
       else ignore (string bp2 0 s);
       comment bp s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
@@ -405,7 +405,7 @@ let rec next_token = parser bp
       (("METAIDENT", get_buff len), (bp,ep))
   | [< ''.' as c; t = parse_after_dot bp c >] ep ->
       comment_stop bp;
-      if Flags.do_translate() & t=("",".") then between_com := true;
+      if Flags.do_beautify() & t=("",".") then between_com := true;
       (t, (bp,ep))
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 19446b7d19..f5fe151eda 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -101,7 +101,7 @@ let pr_generalization bk ak c =
     str "`" ++ str hd ++ c ++ str tl
 
 let pr_com_at n =
-  if Flags.do_translate() && n <> 0 then comment n 
+  if Flags.do_beautify() && n <> 0 then comment n 
   else mt()
 
 let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0fc28d35fa..01e44f84c9 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -331,7 +331,7 @@ let pr_assumption_token many = function
       str (if many then "Parameters" else "Parameter")
   | (Global,Conjectural) -> str"Conjecture"
   | (Local,Conjectural) -> 
-      anomaly "Don't know how to translate a local conjecture"
+      anomaly "Don't know how to beautify a local conjecture"
 
 let pr_params pr_c (xl,(c,t)) =
   hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
@@ -612,7 +612,7 @@ let rec pr_vernac = function
       let pr_onerec = function
         | ((loc,id),(n,ro),bl,type_,def),ntn ->
             let (bl',def,type_) =
-              if Flags.do_translate() then extract_def_binders def type_
+              if Flags.do_beautify() then extract_def_binders def type_
               else ([],def,type_) in
             let bl = bl @ bl' in
             let ids = List.flatten (List.map name_of_binder bl) in
@@ -644,7 +644,7 @@ let rec pr_vernac = function
   | VernacCoFixpoint (corecs,b) ->
       let pr_onecorec (((loc,id),bl,c,def),ntn) =
         let (bl',def,c) =
-              if Flags.do_translate() then extract_def_binders def c
+              if Flags.do_beautify() then extract_def_binders def c
               else ([],def,c) in
         let bl = bl @ bl' in
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -942,19 +942,16 @@ and pr_extend s cl =
     let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
     let start,rl,cl =
       match rl with
-	| Egrammar.TacTerm s :: rl -> str s, rl, cl
-	| Egrammar.TacNonTerm _ :: rl ->
-	    (* Will put an unnecessary extra space in front *)
-	    pr_gen (Global.env()) (List.hd cl), rl, List.tl cl 
-	| [] -> anomaly "Empty entry" in
+      | Egrammar.TacTerm s :: rl -> str s, rl, cl
+      | Egrammar.TacNonTerm _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl 
+      | [] -> anomaly "Empty entry" in
     let (pp,_) =
       List.fold_left
         (fun (strm,args) pi ->
-          match pi with
-              Egrammar.TacNonTerm _ -> 
-                (strm ++ pr_gen (Global.env()) (List.hd args),
-                List.tl args)
-            | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
+          let pp,args = match pi with
+          | Egrammar.TacNonTerm _ -> (pr_arg (List.hd args), List.tl args)
+          | Egrammar.TacTerm s -> (str s, args) in
+          (strm ++ spc() ++ pp), args)
         (start,cl) rl in
     hov 1 pp
   with Not_found ->
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 29e30bca7f..f661800a15 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -118,6 +118,9 @@ EXTEND
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let t, g = Q_util.interp_entry_name loc e "" in
         VernacNonTerm (loc, t, g, Some s)
+      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
+        let t, g = Q_util.interp_entry_name loc e sep in
+        VernacNonTerm (loc, t, g, Some s)
       | s = STRING ->
         VernacTerm s
     ] ]