aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/miscprint.ml25
-rw-r--r--printing/miscprint.mli13
-rw-r--r--printing/ppconstr.ml18
-rw-r--r--printing/ppvernac.ml12
-rw-r--r--printing/prettyp.ml2
-rw-r--r--printing/printer.ml6
-rw-r--r--printing/printer.mli13
7 files changed, 54 insertions, 35 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 360843711c..a4ecbdf5e5 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -47,3 +47,28 @@ let pr_move_location pr_id = function
| MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
| MoveFirst -> str " at top"
| MoveLast -> str " at bottom"
+
+(** Printing of bindings *)
+let pr_binding prc = function
+ | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+let pr_bindings prc prlc = function
+ | ImplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ pr_sequence prc l
+ | ExplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+let pr_bindings_no_with prc prlc = function
+ | ImplicitBindings l ->
+ brk (0,1) ++ prlist_with_sep spc prc l
+ | ExplicitBindings l ->
+ brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+let pr_with_bindings prc prlc (c,bl) =
+ hov 1 (prc c ++ pr_bindings prc prlc bl)
+
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index fe8c779ff4..dbbe3dcfd8 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -22,3 +22,16 @@ val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
val pr_move_location :
('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
+
+val pr_bindings :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+
+val pr_bindings_no_with :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+
+val pr_with_bindings :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds
+
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f76555b047..626464b96f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -151,8 +151,8 @@ let tag_var = tag Tag.variable
let pr_univ l =
match l with
- | [_,x] -> pr_name x
- | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")"
+ | [_,x] -> Name.print x
+ | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")"
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
@@ -166,7 +166,7 @@ let tag_var = tag Tag.variable
| GProp -> tag_type (str "Prop")
| GSet -> tag_type (str "Set")
| GType None -> tag_type (str "Type")
- | GType (Some (_, u)) -> tag_type (pr_name u)
+ | GType (Some (_, u)) -> tag_type (Name.print u)
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
@@ -191,7 +191,7 @@ let tag_var = tag Tag.variable
tag_type (str "Set")
| GType u ->
(match u with
- | Some (_,u) -> pr_name u
+ | Some (_,u) -> Name.print u
| None -> tag_type (str "Type"))
let pr_universe_instance l =
@@ -208,7 +208,7 @@ let tag_var = tag Tag.variable
match expl with
| None -> pr (lapp,L) a
| Some (_,ExplByPos (n,_id)) ->
- anomaly (Pp.str "Explicitation by position not implemented")
+ anomaly (Pp.str "Explicitation by position not implemented.")
| Some (_,ExplByName id) ->
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
@@ -224,7 +224,7 @@ let tag_var = tag Tag.variable
let pr_lname = function
| (loc,Name id) -> pr_lident (loc,id)
- | lna -> pr_located pr_name lna
+ | lna -> pr_located Name.print lna
let pr_or_var pr = function
| ArgArg x -> pr x
@@ -423,7 +423,7 @@ let tag_var = tag Tag.variable
| CLambdaN ([[na],bk,t],c) -> (na,t,c)
| CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c))
| CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c))
- | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+ | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
)
let rename na na' t c =
@@ -438,7 +438,7 @@ let tag_var = tag Tag.variable
| CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c))
| CProdN ((na::nal,bk,t)::bl,c) ->
rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c))
- | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+ | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
)
let rec split_fix n typ def =
@@ -485,7 +485,7 @@ let tag_var = tag Tag.variable
pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
let pr_recursive pr_decl id = function
- | [] -> anomaly (Pp.str "(co)fixpoint with no definition")
+ | [] -> anomaly (Pp.str "(co)fixpoint with no definition.")
| [d1] -> pr_decl false d1
| dl ->
prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ())
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c328b6032b..781af47892 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -56,7 +56,7 @@ open Decl_kinds
let pr_lname = function
| (loc,Name id) -> pr_lident (loc,id)
- | lna -> pr_located pr_name lna
+ | lna -> pr_located Name.print lna
let pr_smart_global = Pputils.pr_or_by_notation pr_reference
@@ -118,7 +118,7 @@ open Decl_kinds
let pr_explanation (e,b,f) =
let a = match e with
- | ExplByPos (n,_) -> anomaly (Pp.str "No more supported")
+ | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.")
| ExplByName id -> pr_id id in
let a = if f then str"!" ++ a else a in
if b then str "[" ++ a ++ str "]" else a
@@ -318,7 +318,7 @@ open Decl_kinds
keyword (if many then "Local Parameters" else "Local Parameter")
| (Global,Conjectural) -> str"Conjecture"
| ((Discharge | Local),Conjectural) ->
- anomaly (Pp.str "Don't know how to beautify a local conjecture")
+ anomaly (Pp.str "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() ++
@@ -1022,13 +1022,13 @@ open Decl_kinds
| n, { name = id; recarg_like = k;
notation_scope = s;
implicit_status = imp } :: tl ->
- spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+ spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
print_arguments (Option.map pred n) tl
in
let rec print_implicits = function
| [] -> mt ()
| (name, impl) :: rest ->
- spc() ++ pr_br impl (pr_name name) ++ print_implicits rest
+ spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
in
print_arguments nargs args ++
if not (List.is_empty more_implicits) then
@@ -1075,7 +1075,7 @@ open Decl_kinds
)
| VernacSetOpacity _ ->
return (
- CErrors.anomaly (keyword "VernacSetOpacity used to set something else")
+ CErrors.anomaly (keyword "VernacSetOpacity used to set something else.")
)
| VernacSetStrategy l ->
let pr_lev = function
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 0f7da36133..2b21b3f9e8 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -132,7 +132,7 @@ let print_impargs_list prefix l =
let print_renames_list prefix l =
if List.is_empty l then [] else
[add_colon prefix ++ str "Arguments are renamed to " ++
- hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
+ hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
let need_expansion impl ref =
let typ = Global.type_of_global_unsafe ref in
diff --git a/printing/printer.ml b/printing/printer.ml
index ebe68680fb..3c31dd96bf 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -26,9 +26,6 @@ module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
module CompactedDecl = Context.Compacted.Declaration
-let emacs_str s =
- if !Flags.print_emacs then s else ""
-
let get_current_context () =
Pfedit.get_current_context ()
@@ -656,9 +653,6 @@ let print_dependent_evars gl sigma seeds =
in
cut () ++ cut () ++
str "(dependent evars:" ++ evars ++ str ")"
- else if !Flags.print_emacs then
- (* IDEs prefer something dummy instead of nothing *)
- cut () ++ cut () ++ str "(dependent evars: (printing disabled) )"
else mt ()
in
constraints ++ evars ()
diff --git a/printing/printer.mli b/printing/printer.mli
index 24107394e6..3fce065613 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -169,19 +169,6 @@ val pr_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map ->
val pr_prim_rule : prim_rule -> std_ppcmds
-(** Emacs/proof general support
- (emacs_str s) outputs
- - s if emacs mode,
- - nothing otherwise.
- This function was previously used to insert special chars like
- [(String.make 1 (Char.chr 253))] to parenthesize sub-parts of the
- proof context for proof by pointing. This part of the code is
- removed for now because it interacted badly with utf8. We may put
- it back some day using some xml-like tags instead of special
- chars. See for example the <prompt> tag in the prompt when in
- emacs mode. *)
-val emacs_str : string -> string
-
(** Backwards compatibility *)
val prterm : constr -> std_ppcmds (** = pr_lconstr *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:46:48 +0000