From 67d6b1ebf7e193a41f778d2d0e68e4208e1c7b38 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 28 May 2019 10:05:58 +0200
Subject: [PATCH] [Gui] Printer_tag: removes the cache for the printer.
Fixes a bug in the GUI where function contracts disappeared when the
preconditions were unfold at a call site.
---
.../ast_printing/printer_tag.ml | 22 ++++++++-----------
1 file changed, 9 insertions(+), 13 deletions(-)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 023b14d756b..83eeb184084 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -521,19 +521,15 @@ struct
let unfold = ref (fun (_ : stmt) -> false)
- let printer =
- let pref : Printer.extensible_printer option ref = ref None in
- fun () ->
- match !pref with Some pp -> pp | None ->
- let pp = Printer.current_printer () in
- let module PP = (val pp: Printer.PrinterClass) in
- let module TAG = struct
- let create = T.create
- let unfold s = !unfold s
- end in
- let module TagPrinterClass = BUILD(TAG)(PP) in
- let printer = new TagPrinterClass.printer in
- pref := Some printer ; printer
+ let printer () =
+ let pp = Printer.current_printer () in
+ let module PP = (val pp: Printer.PrinterClass) in
+ let module TAG = struct
+ let create = T.create
+ let unfold s = !unfold s
+ end in
+ let module TagPrinterClass = BUILD(TAG)(PP) in
+ new TagPrinterClass.printer
let with_unfold_precond unfolder f fmt x =
let stack = !unfold in
--
GitLab