diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 54 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 6 |
2 files changed, 32 insertions, 28 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 46ef2ac031..418d4a0b8f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -535,16 +535,25 @@ open Decl_kinds | SsFwdClose e -> "("^aux e^")*" in Pp.str (aux e) - let rec pr_vernac_body v = + let rec pr_vernac_expr v = let return = tag_vernac v in match v with | VernacPolymorphic (poly, v) -> let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in - return (s ++ spc () ++ pr_vernac_body v) + return (s ++ spc () ++ pr_vernac_expr v) | VernacProgram v -> - return (keyword "Program" ++ spc() ++ pr_vernac_body v) + return (keyword "Program" ++ spc() ++ pr_vernac_expr v) | VernacLocal (local, v) -> - return (pr_locality local ++ spc() ++ pr_vernac_body v) + return (pr_locality local ++ spc() ++ pr_vernac_expr v) + + | VernacLoad (f,s) -> + return ( + keyword "Load" + ++ if f then + (spc() ++ keyword "Verbose" ++ spc()) + else + spc() ++ qs s + ) (* Proof management *) | VernacAbortAll -> @@ -607,24 +616,6 @@ open Decl_kinds | VernacRestoreState s -> return (keyword "Restore State" ++ spc() ++ qs s) - (* Control *) - | VernacLoad (f,s) -> - return ( - keyword "Load" - ++ if f then - (spc() ++ keyword "Verbose" ++ spc()) - else - spc() ++ qs s - ) - | VernacTime (_,v) -> - return (keyword "Time" ++ spc() ++ pr_vernac_body v) - | VernacRedirect (s, (_,v)) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_body v) - | VernacTimeout(n,v) -> - return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v) - | VernacFail v -> - return (keyword "Fail" ++ spc() ++ pr_vernac_body v) - (* Syntax *) | VernacOpenCloseScope (opening,sc) -> return ( @@ -1228,6 +1219,19 @@ open Decl_kinds with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") - let pr_vernac v = - try pr_vernac_body v ++ sep_end v - with e -> CErrors.print e + let rec pr_vernac_control v = + let return = tag_vernac v in + match v with + | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v' + | VernacTime (_,v) -> + return (keyword "Time" ++ spc() ++ pr_vernac_control v) + | VernacRedirect (s, (_,v)) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) + | VernacTimeout(n,v) -> + return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) + | VernacFail v -> + return (keyword "Fail" ++ spc() ++ pr_vernac_control v) + + let pr_vernac v = + try pr_vernac_control v + with e -> CErrors.print e diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index cf27b413c0..34b4fb97f6 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -12,11 +12,11 @@ (** Prints a fixpoint body *) val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t -(** Prints a vernac expression *) -val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t +(** Prints a vernac expression without dot *) +val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t (** Prints a "proof using X" clause. *) val pr_using : Vernacexpr.section_subset_expr -> Pp.t (** Prints a vernac expression and closes it with a dot. *) -val pr_vernac : Vernacexpr.vernac_expr -> Pp.t +val pr_vernac : Vernacexpr.vernac_control -> Pp.t |