Fixed the pretty-printing of the Program plugin.

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

3 files changed, 31 insertions, 1 deletions

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index bf038dc3c7..c81c709db9 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -975,4 +975,6 @@ and pr_extend s cl =
 
 in pr_vernac
 
+let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v
+
 let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end ()
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli
index 7801de6a2a..6d83ca4741 100644
--- a/parsing/ppvernac.mli
+++ b/parsing/ppvernac.mli
@@ -23,4 +23,8 @@ open Topconstr
 
 val sep_end : unit -> std_ppcmds
 
+(** Prints a vernac expression *)
+val pr_vernac_body : vernac_expr -> std_ppcmds
+
+(** Prints a vernac expression and closes it with a dot. *)
 val pr_vernac : vernac_expr -> std_ppcmds
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index ca1240e5f1..89fbd6ffa4 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -69,7 +69,6 @@ GEXTEND Gram
 
   END
 
-
 type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstract_argument_type
 
 let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
@@ -164,3 +163,28 @@ VERNAC COMMAND EXTEND Subtac_Show_Preterm
 | [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ]
 | [ "Preterm" ] -> [ Subtac_obligations.show_term None ]
 END
+
+open Pp
+
+(* Declare a printer for the content of [Program] *)
+let () =
+  let printer _ _ _ expr = Ppvernac.pr_vernac_body (snd expr) in
+  (* should not happen *)
+  let dummy _ _ _ expr = assert false in
+  Pptactic.declare_extra_genarg_pprule
+    (rawwit_subtac_gallina_loc, printer)
+    (globwit_subtac_gallina_loc, dummy)
+    (wit_subtac_gallina_loc, dummy)
+
+(* Declare a printer for the content of Program tactics *)
+let () =
+  let printer _ _ _ = function
+  | None -> mt ()
+  | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic (Global.env ()) tac
+  in
+  (* should not happen *)
+  let dummy _ _ _ expr = assert false in
+  Pptactic.declare_extra_genarg_pprule
+    (rawwit_subtac_withtac, printer)
+    (globwit_subtac_withtac, dummy)
+    (wit_subtac_withtac, dummy)