aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/minilib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/minilib.ml')
-rw-r--r--ide/minilib.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/ide/minilib.ml b/ide/minilib.ml
index d11e8c56b..2c24e46f8 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -30,7 +30,7 @@ let debug = ref false
print in the response buffer.
*)
-let log ?(level = `DEBUG) msg =
+let log_pp ?(level = `DEBUG) msg =
let prefix = match level with
| `DEBUG -> "DEBUG"
| `INFO -> "INFO"
@@ -40,10 +40,12 @@ let log ?(level = `DEBUG) msg =
| `FATAL -> "FATAL"
in
if !debug then begin
- try Printf.eprintf "[%s] %s\n%!" prefix msg
+ try Format.eprintf "[%s] @[%a@]\n%!" prefix Pp.pp_with msg
with _ -> ()
end
+let log ?level str = log_pp ?level (Pp.str str)
+
let coqify d = Filename.concat d "coq"
let coqide_config_home () =