Various small display improvement

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15505 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 15 insertions, 3 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index b862454a20..0a0bdffffe 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -447,7 +447,7 @@ struct
   let width = ["Printing"; "Width"]
   let implicit = ["Printing"; "Implicit"]
   let coercions = ["Printing"; "Coercions"]
-  let raw_matching = ["Printing"; "Matching"; "Synth"]
+  let raw_matching = ["Printing"; "Matching"]
   let notations = ["Printing"; "Notations"]
   let all_basic = ["Printing"; "All"]
   let existential = ["Printing"; "Existential"; "Instances"]
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 04bd4c454d..825fc58cc7 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -26,4 +26,15 @@ let debug = ref false
 *)
 
 let log ?(level = `DEBUG) msg =
-  if !debug then try prerr_endline msg; flush stderr with _ -> ()
+  let prefix = match level with
+  | `DEBUG -> "DEBUG"
+  | `INFO -> "INFO"
+  | `NOTICE -> "NOTICE"
+  | `WARNING -> "WARNING"
+  | `ERROR -> "ERROR"
+  | `FATAL -> "FATAL"
+  in
+  if !debug then begin
+    try Printf.eprintf "[%s] %s\n%!" prefix msg
+    with _ -> ()
+  end
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 6e0a3c787b..8b8de43ee1 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -400,9 +400,10 @@ let eval_call c =
 
 let slave_logger level message =
   (* convert the message into XML *)
+  let msg = Pp.string_of_ppcmds (hov 0 message) in
   let message = {
     Interface.message_level = level;
-    Interface.message_content = Pp.string_of_ppcmds message
+    Interface.message_content = msg;
   } in
   let xml = Serialize.of_message message in
   (* Send it to stdout *)