Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit ae3c9526 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: make Mlw_pretty accessible from Mlw_wp

parent 8e33e369
......@@ -393,8 +393,8 @@ install_local: bin/why3
# Whyml (new API)
########
MLW_FILES = mlw_ty mlw_expr mlw_wp mlw_decl mlw_module \
mlw_pretty mlw_dtree mlw_dty mlw_typing mlw_main
MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
mlw_dtree mlw_dty mlw_typing mlw_main
MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
......
......@@ -20,6 +20,7 @@
open Why3
open Util
open Mlw_module
open Mlw_typing
let read_channel env path file c =
......@@ -33,7 +34,9 @@ let read_channel env path file c =
List.fold_left (add_theory_module env path) (Mstr.empty, Mstr.empty) ml
in
Mstr.iter (fun _ m ->
Mlw_pretty.print_module Format.err_formatter m;
Format.fprintf Format.err_formatter
"@[<hov 2>module %a@\n%a@]@\nend@." Pretty.print_th m.mod_theory
(Pp.print_list Pp.newline2 Mlw_pretty.print_pdecl) m.mod_decls;
Format.pp_print_newline Format.err_formatter ()) mm;
mm, tm
......
......@@ -31,7 +31,6 @@ open Mlw_ty
open Mlw_ty.T
open Mlw_expr
open Mlw_decl
open Mlw_module
let debug_print_labels = Debug.register_flag "print_labels"
let debug_print_locs = Debug.register_flag "print_locs"
......@@ -82,9 +81,6 @@ let print_ps fmt ps =
let forget_ps ps = forget_id iprinter ps.ps_name
(* theory names always start with an upper case letter *)
let print_mod fmt m = print_th fmt m.mod_theory
let print_its fmt ts = print_ts fmt ts.its_pure
(** Types *)
......@@ -426,11 +422,6 @@ let print_data_decl = print_data_decl true
let print_next_rec_decl = print_rec_decl false
let print_rec_decl = print_rec_decl true
let print_module fmt m =
fprintf fmt "@[<hov 2>module %a%a@\n%a@]@\nend@."
print_mod m print_ident_labels m.mod_theory.th_name
(print_list newline2 print_pdecl) m.mod_decls
(* Print exceptions *)
let () = Exn_printer.register
......
......@@ -24,7 +24,6 @@ open Mlw_ty
open Mlw_ty.T
open Mlw_expr
open Mlw_decl
open Mlw_module
val forget_all : unit -> unit (* flush id_unique *)
val forget_regs : unit -> unit (* flush id_unique for regions *)
......@@ -63,6 +62,3 @@ val print_next_data_decl : formatter -> data_decl -> unit
val print_pdecl : formatter -> pdecl -> unit
val print_mod : formatter -> modul -> unit (* module name *)
val print_module : formatter -> modul -> unit (* module *)
......@@ -168,7 +168,7 @@ let dity_unit = ts_app ts_unit []
let dity_mark = ts_app ts_mark []
let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
| TypeMismatch (ity1,ity2) -> errorm ~loc
| TypeMismatch (ity1,ity2) -> errorm ~loc
"This expression has type %a, but is expected to have type %a"
Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
| exn -> error ~loc exn
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment