Now CoqIDE separates answer and messages. This should hopefully

be backward compatible...

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

7 files changed, 77 insertions, 35 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 31de9cf4b..b862454a2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -179,6 +179,7 @@ type handle = {
   cout : in_channel;
   cin : out_channel;
   mutable alive : bool;
+  xml_parser : Xml_parser.t;
 }
 
 type coqtop = {
@@ -205,6 +206,8 @@ type coqtop = {
     taken.
 *)
 
+type logger = Interface.message_level -> string -> unit
+
 exception DeadCoqtop
 
 (** * Count of all active coqtops *)
@@ -249,12 +252,15 @@ let unsafe_spawn_handle args =
   let prog = coqtop_path () in
   let args = Array.of_list (prog :: "-ideslave" :: args) in
   let (pid, ic, oc) = open_process_pid prog args in
+  let p = Xml_parser.make (Xml_parser.SChannel ic) in
+  Xml_parser.check_eof p false;
   incr toplvl_ctr;
   {
     pid = pid;
     cin = oc;
     cout = ic;
     alive = true;
+    xml_parser = p;
   }
 
 (** This clears any potentially remaining open garbage. *)
@@ -345,15 +351,22 @@ let try_grab coqtop f g =
 
 (** Cf [Ide_intf] for more details *)
 
-let p = Xml_parser.make ()
-let () = Xml_parser.check_eof p false
-
-let eval_call coqtop (c:'a Serialize.call) =
+let eval_call coqtop logger (c:'a Serialize.call) =
+  (** Retrieve the messages sent by coqtop until an answer has been received *)
+  let rec loop () =
+    let xml = Xml_parser.parse coqtop.xml_parser in
+    if Serialize.is_message xml then
+      let message = Serialize.to_message xml in
+      let level = message.Interface.message_level in
+      let content = message.Interface.message_content in
+      let () = logger level content  in
+      loop ()
+    else (Serialize.to_answer xml : 'a Interface.value)
+  in
   try
     Xml_utils.print_xml coqtop.cin (Serialize.of_call c);
     flush coqtop.cin;
-    let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
-    (Serialize.to_answer xml : 'a Interface.value)
+    loop ()
   with
   | Serialize.Marshal_error ->
     (* the protocol was not respected... *)
@@ -366,20 +379,20 @@ let eval_call coqtop (c:'a Serialize.call) =
     Minilib.log msg;
     raise DeadCoqtop
 
-let interp coqtop ?(raw=false) ?(verbose=true) s =
-  eval_call coqtop (Serialize.interp (raw,verbose,s))
-let rewind coqtop i = eval_call coqtop (Serialize.rewind i)
-let inloadpath coqtop s = eval_call coqtop (Serialize.inloadpath s)
-let mkcases coqtop s = eval_call coqtop (Serialize.mkcases s)
-let status coqtop = eval_call coqtop Serialize.status
-let hints coqtop = eval_call coqtop Serialize.hints
-let search coqtop flags = eval_call coqtop (Serialize.search flags)
+let interp coqtop log ?(raw=false) ?(verbose=true) s =
+  eval_call coqtop log (Serialize.interp (raw,verbose,s))
+let rewind coqtop i = eval_call coqtop default_logger (Serialize.rewind i)
+let inloadpath coqtop s = eval_call coqtop default_logger (Serialize.inloadpath s)
+let mkcases coqtop s = eval_call coqtop default_logger (Serialize.mkcases s)
+let status coqtop = eval_call coqtop default_logger Serialize.status
+let hints coqtop = eval_call coqtop default_logger Serialize.hints
+let search coqtop flags = eval_call coqtop default_logger (Serialize.search flags)
 
 let unsafe_close coqtop =
   if Mutex.try_lock coqtop.lock then begin
     let () =
       try
-        match eval_call coqtop.handle Serialize.quit with
+        match eval_call coqtop.handle default_logger Serialize.quit with
         | Interface.Good _ -> ()
         | _ -> raise Exit
       with err -> kill_coqtop coqtop
@@ -448,7 +461,7 @@ struct
     let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in
     let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in
     let options = (width, Interface.IntValue !width_ref):: options in
-    match eval_call coqtop (Serialize.set_options options) with
+    match eval_call coqtop default_logger (Serialize.set_options options) with
     | Interface.Good () -> ()
     | _ -> raise (Failure "Cannot set options.")
 
@@ -460,8 +473,8 @@ end
 
 let goals coqtop =
   let () = PrintOpt.enforce_hack coqtop in
-  eval_call coqtop Serialize.goals
+  eval_call coqtop default_logger Serialize.goals
 
 let evars coqtop =
   let () = PrintOpt.enforce_hack coqtop in
-  eval_call coqtop Serialize.evars
+  eval_call coqtop default_logger Serialize.evars
diff --git a/ide/coq.mli b/ide/coq.mli
index f168aff80..c082893ba 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -87,8 +87,11 @@ val interrupter : (int -> unit) ref
 
 (** * Calls to Coqtop, cf [Serialize] for more details *)
 
+type logger = Interface.message_level -> string -> unit
+(** Except for interp, we use the default logger for any call. *)
+
 val interp :
-  handle -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
+  handle -> logger -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
 val rewind : handle -> int -> int Interface.value
 val status : handle -> Interface.status Interface.value
 val goals : handle -> Interface.goals option Interface.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1f6482cbf..b1f7b9616 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -577,6 +577,9 @@ object(self)
     message_view#clear ();
     message_view#push Interface.Notice s
 
+  method private push_message level content =
+    message_view#push level content
+
   method get_start_of_input =  input_buffer#get_iter_at_mark (`NAME "start_of_input")
 
   method get_insert = get_insert input_buffer
@@ -649,7 +652,7 @@ object(self)
         flash_info "This error is so nasty that I can't even display it."
       else self#insert_message s;
     in
-    match Coq.interp handle ~raw:true ~verbose:false phrase with
+    match Coq.interp handle self#push_message ~raw:true ~verbose:false phrase with
     | Interface.Fail (_, err) -> sync display_error err
     | Interface.Good msg -> sync self#insert_message msg
 
@@ -690,6 +693,7 @@ object(self)
   method private process_command_queue ?(verbose = false) queue handle =
     let error = ref None in
     let info = ref [] in
+    let push_info level message = info := (level, message) :: !info in
     (* First, process until error *)
     Minilib.log "Begin command processing";
     while not (Queue.is_empty queue) && !error = None do
@@ -699,9 +703,9 @@ object(self)
         let start = input_buffer#get_iter_at_mark sentence.start in
         let stop = input_buffer#get_iter_at_mark sentence.stop in
         let phrase = start#get_slice ~stop in
-        match Coq.interp handle ~verbose phrase with
+        match Coq.interp handle push_info ~verbose phrase with
         | Interface.Fail (loc, msg) -> error := Some (phrase, loc, msg);
-        | Interface.Good msg -> info := msg :: !info
+        | Interface.Good msg -> push_info Interface.Notice msg
       end;
       (* If there is no error, then we mark it done *)
       if !error = None then begin
@@ -758,8 +762,8 @@ object(self)
     self#show_goals handle;
     match error with
     | None ->
-      let msg = try List.hd msg with _ -> "" in
-      if verbose then self#set_message msg;
+      if verbose then
+        List.iter (fun (lvl, msg) -> self#push_message lvl msg) msg;
       finish ();
       self#recenter_insert
     | Some (phrase, loc, msg) ->
@@ -855,7 +859,7 @@ object(self)
         else self#insert_message s
       in
       Minilib.log "Send_to_coq starting now";
-      match Coq.interp handle ~verbose:false phrase with
+      match Coq.interp handle default_logger ~verbose:false phrase with
         | Interface.Fail (l,str) -> sync display_error (l,str); None
         | Interface.Good msg -> sync self#insert_message msg; Some Safe
           (* TODO: Restore someday the access to Decl_mode.get_damon_flag,
@@ -934,7 +938,7 @@ object(self)
 	  | Interface.Good true -> ()
 	  | Interface.Good false ->
 	    let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-	    match Coq.interp handle cmd with
+	    match Coq.interp handle default_logger cmd with
 	      | Interface.Fail (l,str) ->
 		self#set_message ("Couln't add loadpath:\n"^str)
 	      | Interface.Good _ -> ()
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 2a5df0ea9..e9dd8e7e3 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -332,3 +332,14 @@ let textview_width (view : #GText.view) =
   let metrics = view#misc#pango_context#get_metrics ()  in
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
+
+let default_logger level message =
+  let level = match level with
+  | Interface.Debug _ -> `DEBUG
+  | Interface.Info -> `INFO
+  | Interface.Notice -> `NOTICE
+  | Interface.Warning -> `WARNING
+  | Interface.Error -> `ERROR
+  in
+  Minilib.log ~level message
+
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 553c4c2bc..e7cfc4390 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -70,3 +70,6 @@ val requote : string -> string
 
 val textview_width : #GText.view -> int
 (** Returns an approximate value of the character width of a textview *)
+
+val default_logger : Interface.message_level -> string -> unit
+(** Default logger. It logs messages that the casual user should not see. *)
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index a43fdc7c8..931572da2 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -111,14 +111,21 @@ object(self)
 	if String.get com (String.length com - 1) = '.'
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
-      Coq.try_grab coqtop begin fun handle ->
-          result#buffer#set_text
-            (match Coq.interp handle ~raw:true phrase with
-              | Interface.Fail (l,str) ->
-                  ("Error while interpreting "^phrase^":\n"^str)
-              | Interface.Good results ->
-                  ("Result for command " ^ phrase ^ ":\n" ^ results))
-      end ignore
+      let insert level message =
+        result#buffer#insert message;
+        result#buffer#insert "\n"
+      in
+      let process handle =
+        let answer = match Coq.interp handle insert ~raw:true phrase with
+        | Interface.Fail (l,str) ->
+            "Error while interpreting "^phrase^":\n"^str
+        | Interface.Good results ->
+            "Result for command " ^ phrase ^ ":\n" ^ results
+        in
+        result#buffer#insert answer
+      in
+      result#buffer#set_text "";
+      Coq.try_grab coqtop process ignore
     in
     ignore (combo#entry#connect#activate ~callback:(on_activate callback));
     ignore (ok_b#connect#clicked ~callback:(on_activate callback));
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index cae6cf3c7..2b0339631 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -31,7 +31,8 @@ let message_view () : message_view =
       | Interface.Error -> [Tags.Message.error]
       | _ -> []
       in
-      buffer#insert ~tags msg
+      buffer#insert ~tags msg;
+      buffer#insert ~tags "\n"
 
     method add_selection_clipboard cb =
       buffer#add_selection_clipboard cb