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

6 files changed, 79 insertions, 53 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
index 2cffa71aed..4c7c11ebb2 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 fd1c6d0555..1d686243fe 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 0a1e9a107a..8b24aca156 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 ebb867190a..e61cb055f7 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 014331202f..6207763cda 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 2c83eee9d7..1cde9dc811 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