module Mlw_printer:sig
..end
type 'a
printers = {
|
marked : |
|
closed : |
}
The marked
printer potentially adds the marker, the closed
printer adds
parentheses to the potentially marked node
val pp_pattern : attr:bool -> Ptree.pattern printers
Printer for patterns
val pp_expr : attr:bool -> Ptree.expr printers
Printer for expressions
val pp_term : attr:bool -> Ptree.term printers
Printer for terms
val pp_pty : attr:bool -> Ptree.pty printers
Printer for types
val pp_decl : ?attr:bool -> Ptree.decl Pp.pp
Printer for declarations
val pp_mlw_file : ?attr:bool -> Ptree.mlw_file Pp.pp
Printer for mlw files
When Ptree
elements are generated (instead of being parsed from a
whyml file), locations of typing errors are useless, because they do not
correspond to any concrete syntax.
Alternatively, we can give every Ptree
element a unique location,
for example using the function Mlw_printer.next_pos
. When a
located error is encountered, the function Mlw_printer.with_marker
can
then be used to instruct the mlw-printer to insert a message as a
comment just before an expression, term, or pattern with the given
location.
For example, this can be used to indicate and show a typing error in the printed mlw-file:
try
let mm = Typing.type_mlw_file env path filename mlw_file in
(* ... well typed mlw_file ... *)
with Loc.Located (loc, e) -> (* A located exception [e] *)
let msg = Format.asprintf "%a" Exn_printer.exn_printer e in
Format.fprintf fmt "%a@."
(Mlw_printer.with_marker ~msg loc Mlw_printer.pp_mlw_file)
mlw_file
val next_pos : unit -> Loc.position
Generate a unique location.
val with_marker : ?msg:string -> Loc.position -> 'a Pp.pp -> 'a Pp.pp
Inform a printer to include the message (default: "XXX"
) as a comment
before the expression, term, or pattern with the given location.
NOTE: This is currently implemented by a global reference and is therefore unsafe in threaded programs.
val id_loc : unit -> Loc.position
Create a unique dummy location
val is_id_loc : Loc.position -> bool