Module Mlw_printer

module Mlw_printer: sig .. end

Printers

type 'a printers = {

val pp_pattern : attr:bool -> Ptree.pattern printers

val pp_expr : attr:bool -> Ptree.expr printers

val pp_term : attr:bool -> Ptree.term printers

val pp_pty : attr:bool -> Ptree.pty printers

val pp_decl : ?attr:bool -> Ptree.decl Pp.pp

val pp_mlw_file : ?attr:bool -> Ptree.mlw_file Pp.pp

Markers

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

val with_marker : ?msg:string -> Loc.position -> 'a Pp.pp -> 'a Pp.pp

val id_loc : unit -> Loc.position

val is_id_loc : Loc.position -> bool