diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 67 |
1 files changed, 30 insertions, 37 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e88284fb1c..7e68a97e44 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -31,12 +31,6 @@ open Decl_kinds let pr_lconstr = pr_lconstr_expr let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr - let pr_lident (loc,id) = - match loc with - | None -> pr_id id - | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id - let pr_uconstraint (l, d, r) = pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_glob_level r @@ -77,10 +71,6 @@ open Decl_kinds | Some loc -> let (b,_) = Loc.unloc loc in pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid - let pr_lname = function - | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located Name.print lna - let pr_smart_global = Pputils.pr_or_by_notation pr_reference let pr_ltac_ref = Libnames.pr_reference @@ -91,7 +81,7 @@ open Decl_kinds let sep_end = function | VernacBullet _ - | VernacSubproof None + | VernacSubproof _ | VernacEndSubproof -> str"" | _ -> str"." @@ -535,17 +525,25 @@ open Decl_kinds | SsFwdClose e -> "("^aux e^")*" in Pp.str (aux e) - let rec pr_vernac_expr v = + let pr_extend s cl = + let pr_arg a = + try pr_gen a + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in + try + let rl = Egramml.get_extend_vernac_rule s in + let rec aux rl cl = + match rl, cl with + | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl + | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl + | [], [] -> [] + | _ -> assert false in + hov 1 (pr_sequence identity (aux rl cl)) + with Not_found -> + hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") + + let 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_expr v) - | VernacProgram v -> - return (keyword "Program" ++ spc() ++ pr_vernac_expr v) - | VernacLocal (local, v) -> - return (pr_locality local ++ spc() ++ pr_vernac_expr v) - | VernacLoad (f,s) -> return ( keyword "Load" @@ -1199,30 +1197,25 @@ open Decl_kinds | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (keyword "BeginSubproof" ++ spc () ++ int i) + return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") - and pr_extend s cl = - let pr_arg a = - try pr_gen a - with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in - try - let rl = Egramml.get_extend_vernac_rule s in - let rec aux rl cl = - match rl, cl with - | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl - | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl - | [], [] -> [] - | _ -> assert false in - hov 1 (pr_sequence identity (aux rl cl)) - with Not_found -> - hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") +let pr_vernac_flag = + function + | VernacPolymorphic true -> keyword "Polymorphic" + | VernacPolymorphic false -> keyword "Monomorphic" + | VernacProgram -> keyword "Program" + | VernacLocal local -> pr_locality local let rec pr_vernac_control v = let return = tag_vernac v in match v with - | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v' + | VernacExpr (f, v') -> + List.fold_right + (fun f a -> pr_vernac_flag f ++ spc() ++ a) + f + (pr_vernac_expr v' ++ sep_end v') | VernacTime (_,(_,v)) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) | VernacRedirect (s, (_,v)) -> |