aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r--parsing/printer.ml100
1 files changed, 50 insertions, 50 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 77d0f59a1..3076213e5 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -25,29 +25,29 @@ open Nametab
let emacs_str s = if !Options.print_emacs then s else ""
-let dfltpr ast = [< 'sTR"#GENTERM " ; print_ast ast >];;
+let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
let pr_global ref = pr_global_env (Global.env()) ref
let global_const_name sp =
try pr_global (ConstRef sp)
with Not_found -> (* May happen in debug *)
- [< 'sTR ("CONST("^(string_of_path sp)^")") >]
+ (str ("CONST("^(string_of_path sp)^")"))
let global_ind_name (sp,tyi) =
try pr_global (IndRef (sp,tyi))
with Not_found -> (* May happen in debug *)
- [< 'sTR ("IND("^(string_of_path sp)^","^(string_of_int tyi)^")") >]
+ (str ("IND("^(string_of_path sp)^","^(string_of_int tyi)^")"))
let global_constr_name ((sp,tyi),i) =
try pr_global (ConstructRef ((sp,tyi),i))
with Not_found -> (* May happen in debug *)
- [< 'sTR ("CONSTRUCT("^(string_of_path sp)^","^(string_of_int tyi)
- ^","^(string_of_int i)^")") >]
+ (str ("CONSTRUCT("^(string_of_path sp)^","^(string_of_int tyi)
+ ^","^(string_of_int i)^")"))
let globpr gt = match gt with
- | Nvar(_,s) -> [< pr_id s >]
- | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
+ | Nvar(_,s) -> (pr_id s)
+ | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
| Node(_,"CONST",[Path(_,sl)]) ->
global_const_name (section_path sl)
| Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
@@ -55,16 +55,16 @@ let globpr gt = match gt with
| Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
global_constr_name ((section_path sl, tyi), i)
| Dynamic(_,d) ->
- if (Dyn.tag d) = "constr" then [< 'sTR"<dynamic [constr]>" >]
+ if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
else dfltpr gt
| gt -> dfltpr gt
let wrap_exception = function
Anomaly (s1,s2) ->
- warning ("Anomaly ("^s1^")");pP s2;
- [< 'sTR"<PP error: non-printable term>" >]
+ warning ("Anomaly ("^s1^")"); pp s2;
+ str"<PP error: non-printable term>"
| Failure _ | UserError _ | Not_found ->
- [< 'sTR"<PP error: non-printable term>" >]
+ str"<PP error: non-printable term>"
| s -> raise s
(* These are the names of the universes where the pp rules for constr and
@@ -135,10 +135,10 @@ let rec gentacpr gt =
Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt
and default_tacpr = function
- | Nvar(_,s) -> [< pr_id s >]
+ | Nvar(_,s) -> (pr_id s)
(* constr's may occur inside tac expressions ! *)
- | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
+ | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
| Node(_,"CONST",[Path(_,sl)]) ->
let sp = section_path sl in
pr_global (ConstRef sp)
@@ -150,39 +150,39 @@ and default_tacpr = function
pr_global (ConstructRef ((sp,tyi),i))
(* This should be tactics *)
- | Node(_,s,[]) -> [< 'sTR s >]
+ | Node(_,s,[]) -> (str s)
| Node(_,s,ta) ->
- [< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
+ (str s ++ brk(1,2) ++ hov 0 (prlist_with_sep pr_spc gentacpr ta))
| Dynamic(_,d) as gt ->
let tg = Dyn.tag d in
- if tg = "tactic" then [< 'sTR"<dynamic [tactic]>" >]
- else if tg = "value" then [< 'sTR"<dynamic [value]>" >]
- else if tg = "constr" then [< 'sTR"<dynamic [constr]>" >]
+ if tg = "tactic" then (str"<dynamic [tactic]>")
+ else if tg = "value" then (str"<dynamic [value]>")
+ else if tg = "constr" then (str"<dynamic [constr]>")
else dfltpr gt
| gt -> dfltpr gt
let pr_var_decl env (id,c,typ) =
let pbody = match c with
- | None -> [< >]
+ | None -> (mt ())
| Some c ->
(* Force evaluation *)
let pb = prterm_env env c in
- [< 'sTR" := "; pb >] in
+ (str" := " ++ pb) in
let pt = prtype_env env typ in
- let ptyp = [< 'sTR" : "; pt >] in
- [< pr_id id ; hOV 0 [< pbody; ptyp >] >]
+ let ptyp = (str" : " ++ pt) in
+ (pr_id id ++ hov 0 (pbody ++ ptyp))
let pr_rel_decl env (na,c,typ) =
let pbody = match c with
- | None -> [< >]
+ | None -> (mt ())
| Some c ->
(* Force evaluation *)
let pb = prterm_env env c in
- [< 'sTR":="; 'sPC; pb; 'sPC >] in
+ (str":=" ++ spc () ++ pb ++ spc ()) in
let ptyp = prtype_env env typ in
match na with
- | Anonymous -> [< 'sTR"<>" ; 'sPC; pbody; 'sTR":"; 'sPC; ptyp >]
- | Name id -> [< pr_id id ; 'sPC; pbody; 'sTR":"; 'sPC; ptyp >]
+ | Anonymous -> (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+ | Name id -> (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
(* Prints out an "env" in a nice format. We print out the
@@ -191,18 +191,18 @@ let pr_rel_decl env (na,c,typ) =
(* Prints a signature, all declarations on the same line if possible *)
let pr_named_context_of env =
- hV 0 [< (fold_named_context
- (fun env d pps -> [< pps; 'wS 2; pr_var_decl env d >])
- env) [< >] >]
+ hv 0 (fold_named_context
+ (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
+ env ~init:(mt ()))
let pr_rel_context env rel_context =
let rec prec env = function
- | [] -> [<>]
+ | [] -> (mt ())
| [b] -> pr_rel_decl env b
| b::rest ->
let pb = pr_rel_decl env b in
let penvtl = prec (push_rel b env) rest in
- [< pb; 'sTR";"; 'sPC; penvtl >]
+ (pb ++ str";" ++ spc () ++ penvtl)
in
prec env (List.rev rel_context)
@@ -211,21 +211,21 @@ let pr_context_unlimited env =
let sign_env =
fold_named_context
(fun env d pps ->
- let pidt = pr_var_decl env d in [< pps; 'fNL; pidt >])
- env [< >]
+ let pidt = pr_var_decl env d in (pps ++ fnl () ++ pidt))
+ env ~init:(mt ())
in
let db_env =
fold_rel_context
(fun env d pps ->
- let pnat = pr_rel_decl env d in [< pps; 'fNL; pnat >])
- env [< >]
+ let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
+ env ~init:(mt ())
in
- [< sign_env; db_env >]
+ (sign_env ++ db_env)
let pr_ne_context_of header env =
if Environ.rel_context env = empty_rel_context &
- Environ.named_context env = empty_named_context then [< >]
- else let penv = pr_context_unlimited env in [< header; penv; 'fNL >]
+ Environ.named_context env = empty_named_context then (mt ())
+ else let penv = pr_context_unlimited env in (header ++ penv ++ fnl ())
let pr_context_limit n env =
let named_context = Environ.named_context env in
@@ -238,25 +238,25 @@ let pr_context_limit n env =
fold_named_context
(fun env d (i,pps) ->
if i < k then
- (i+1, [< pps ;'sTR "." >])
+ (i+1, (pps ++str "."))
else
let pidt = pr_var_decl env d in
- (i+1, [< pps ; 'fNL ;
- 'sTR (emacs_str (String.make 1 (Char.chr 253)));
- pidt >]))
- env (0,[< >])
+ (i+1, (pps ++ fnl () ++
+ str (emacs_str (String.make 1 (Char.chr 253))) ++
+ pidt)))
+ env ~init:(0,(mt ()))
in
let db_env =
fold_rel_context
(fun env d pps ->
let pnat = pr_rel_decl env d in
- [< pps; 'fNL;
- 'sTR (emacs_str (String.make 1 (Char.chr 253)));
- pnat >])
- env [< >]
+ (pps ++ fnl () ++
+ str (emacs_str (String.make 1 (Char.chr 253))) ++
+ pnat))
+ env ~init:(mt ())
in
- [< sign_env; db_env >]
+ (sign_env ++ db_env)
let pr_context_of env = match Options.print_hyps_limit () with
- | None -> hV 0 (pr_context_unlimited env)
- | Some n -> hV 0 (pr_context_limit n env)
+ | None -> hv 0 (pr_context_unlimited env)
+ | Some n -> hv 0 (pr_context_limit n env)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 07:02:49 +0000