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

14 files changed, 171 insertions, 90 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
diff --git a/lib/interface.mli b/lib/interface.mli
index 2cffa71ae..4c7c11ebb 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -108,6 +108,11 @@ type message_level =
 | Warning
 | Error
 
+type message = {
+  message_level : message_level;
+  message_content : string;
+}
+
 type location = (int * int) option (* start and end of the error *)
 
 type 'a value =
diff --git a/lib/serialize.ml b/lib/serialize.ml
index fd1c6d055..1d686243f 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -412,10 +412,40 @@ let to_coq_info = function
   }
 | _ -> raise Marshal_error
 
+let of_message_level = function
+| Debug s -> constructor "message_level" "debug" [PCData s]
+| Info -> constructor "message_level" "info" []
+| Notice -> constructor "message_level" "notice" []
+| Warning -> constructor "message_level" "warning" []
+| Error -> constructor "message_level" "error" []
+
+let to_message_level xml = do_match xml "message_level"
+  (fun s args -> match s with
+  | "debug" -> Debug (raw_string args)
+  | "info" -> Info
+  | "notice" -> Notice
+  | "warning" -> Warning
+  | "error" -> Error
+  | _ -> raise Marshal_error)
+
+let of_message msg =
+  let lvl = of_message_level msg.message_level in
+  let content = of_string msg.message_content in
+  Element ("message", [], [lvl; content])
+
+let to_message xml = match xml with
+| Element ("message", [], [lvl; content]) ->
+  { message_level = to_message_level lvl; message_content = to_string content }
+| _ -> raise Marshal_error
+
 let of_hints =
   let of_hint = of_list (of_pair of_string of_string) in
   of_option (of_pair (of_list of_hint) of_hint)
 
+let is_message = function
+| Element ("message", _, _) -> true
+| _ -> false
+
 let of_answer (q : 'a call) (r : 'a value) =
   let convert = match q with
   | Interp _ -> Obj.magic (of_string : string -> xml)
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 0a1e9a107..8b24aca15 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -108,6 +108,10 @@ val to_value : (xml -> 'a) -> xml -> 'a value
 val of_call : 'a call -> xml
 val to_call : xml -> 'a call
 
+val of_message : message -> xml
+val to_message : xml -> message
+val is_message : xml -> bool
+
 val of_answer : 'a call -> 'a value -> xml
 val to_answer : xml -> 'a value
 
diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli
index ebb867190..e61cb055f 100644
--- a/lib/xml_lexer.mli
+++ b/lib/xml_lexer.mli
@@ -38,7 +38,7 @@ type token =
 type pos = int * int * int * int
 
 val init : Lexing.lexbuf -> unit 
-val close : Lexing.lexbuf -> unit
+val close : unit -> unit
 val token : Lexing.lexbuf -> token
 val pos : Lexing.lexbuf -> pos
 val restore : pos -> unit
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 014331202..6207763cd 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -50,21 +50,16 @@ exception Error of error
 exception File_not_found of string
 
 type t = {
-	mutable check_eof : bool;
-	mutable concat_pcdata : bool;
+  mutable check_eof : bool;
+  mutable concat_pcdata : bool;
+  source : Lexing.lexbuf;
+  stack : Xml_lexer.token Stack.t;
 }
 
-type source = 
-	| SFile of string
-	| SChannel of in_channel
-	| SString of string
-	| SLexbuf of Lexing.lexbuf
-
-type state = {
-	source : Lexing.lexbuf;
-	stack : Xml_lexer.token Stack.t;
-	xparser : t;
-}
+type source =
+| SChannel of in_channel
+| SString of string
+| SLexbuf of Lexing.lexbuf
 
 exception Internal_error of error_msg
 exception NoMoreData
@@ -88,11 +83,19 @@ let _raises e f =
 	xml_error := e;
 	file_not_found := f
 
-let make () =
-	{
-		check_eof = true;
-		concat_pcdata = true;
-	}
+let make source =
+  let source = match source with
+  | SChannel chan -> Lexing.from_channel chan
+  | SString s -> Lexing.from_string s
+  | SLexbuf lexbuf -> lexbuf
+  in
+  let () = Xml_lexer.init source in
+  {
+    check_eof = true;
+    concat_pcdata = true;
+    source = source;
+    stack = Stack.create ();
+  }
 
 let check_eof p v = p.check_eof <- v
 let concat_pcdata p v = p.concat_pcdata <- v
@@ -162,40 +165,25 @@ let convert = function
 	| Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
 	| Xml_lexer.EUnterminatedEntity -> 	UnterminatedEntity
 
-let do_parse xparser source =
+let do_parse xparser =
 	try
-		Xml_lexer.init source;
-		let s = { source = source; xparser = xparser; stack = Stack.create(); } in
-		let x = read_xml s in
-		if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
-		Xml_lexer.close source;
+		Xml_lexer.init xparser.source;
+		let x = read_xml xparser in
+		if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
+		Xml_lexer.close ();
 		x
 	with
 		| NoMoreData ->
-			Xml_lexer.close source;
-			raise (!xml_error NodeExpected source)
+			Xml_lexer.close ();
+			raise (!xml_error NodeExpected xparser.source)
 		| Internal_error e ->
-			Xml_lexer.close source;
-			raise (!xml_error e source)
+			Xml_lexer.close ();
+			raise (!xml_error e xparser.source)
 		| Xml_lexer.Error e ->
-			Xml_lexer.close source;
-			raise (!xml_error (convert e) source)
-
-let parse p = function
-	| SChannel ch -> do_parse p (Lexing.from_channel ch)
-	| SString str -> do_parse p (Lexing.from_string str)
-	| SLexbuf lex -> do_parse p lex
-	| SFile fname ->
-		let ch = (try open_in fname with Sys_error _ -> raise (!file_not_found fname)) in
-		try
-			let x = do_parse p (Lexing.from_channel ch) in
-			close_in ch;
-			x
-		with
-			e ->
-				close_in ch;
-				raise e
+			Xml_lexer.close ();
+			raise (!xml_error (convert e) xparser.source)
 
+let parse p = do_parse p
 
 let error_msg = function
         | UnterminatedComment -> "Unterminated comment"
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index 2c83eee9d..1cde9dc81 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -82,14 +82,13 @@ val abs_range : error_pos -> int * int
 val pos : Lexing.lexbuf -> error_pos
 
 (** Several kind of resources can contain Xml documents. *)
-type source = 
-	| SFile of string
-	| SChannel of in_channel
-	| SString of string
-	| SLexbuf of Lexing.lexbuf
+type source =
+| SChannel of in_channel
+| SString of string
+| SLexbuf of Lexing.lexbuf
 
 (** This function returns a new parser with default options. *)
-val make : unit -> t
+val make : source -> t
 
 (** When a Xml document is parsed, the parser will check that the end of the
  document is reached, so for example parsing ["<A/><B/>"] will fail instead
@@ -99,4 +98,4 @@ val check_eof : t -> bool -> unit
 
 (** Once the parser is configurated, you can run the parser on a any kind
  of xml document source to parse its contents into an Xml data structure. *)
-val parse :  t -> source -> xml
+val parse :  t -> xml
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index b7a6af494..57f2da8e0 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -396,6 +396,18 @@ let eval_call c =
   ignore (read_stdout ());
   Serialize.abstract_eval_call handler c
 
+(** Message dispatching. *)
+
+let slave_logger level message =
+  (* convert the message into XML *)
+  let message = {
+    Interface.message_level = level;
+    Interface.message_content = Pp.string_of_ppcmds message
+  } in
+  let xml = Serialize.of_message message in
+  (* Send it to stdout *)
+  Xml_utils.print_xml !orig_stdout xml;
+  flush !orig_stdout
 
 (** The main loop *)
 
@@ -410,10 +422,11 @@ let fail err =
   Serialize.of_value (fun _ -> assert false) (Interface.Fail (None, err))
 
 let loop () =
-  let p = Xml_parser.make () in
+  let p = Xml_parser.make (Xml_parser.SChannel stdin) in
   let () = Xml_parser.check_eof p false in
   init_signal_handler ();
   catch_break := false;
+  Pp.set_logger slave_logger;
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -422,7 +435,7 @@ let loop () =
     while true do
       let xml_answer =
         try
-          let xml_query = Xml_parser.parse p (Xml_parser.SChannel stdin) in
+          let xml_query = Xml_parser.parse p in
           let q = Serialize.to_call xml_query in
           let () = pr_debug ("<-- " ^ Serialize.pr_call q) in
           let r = eval_call q in