From a2a00ee2c3a01c63891d5c48f88d3c507c8a83e4 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 16 Apr 2003 12:51:25 +0000
Subject: [PATCH] - use an exception to handle empty status nodes - removed
 some ancient comments

---
 helm/hbugs/common/hbugs_messages.ml | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml
index 836008e40..b7e6f5ddc 100644
--- a/helm/hbugs/common/hbugs_messages.ml
+++ b/helm/hbugs/common/hbugs_messages.ml
@@ -36,6 +36,7 @@ open Pxp_yacc;;
 let debug = true;;
 
 exception Attribute_not_found of string;;
+exception Empty_node;;  (** found a node with no _element_ children *)
 exception No_element_found of string;;
 exception Parse_error of string * string;;  (* parsing subject, reason *)
 exception Unexpected_message of message;;
@@ -47,17 +48,18 @@ let get_attr node name =
     | Value s -> s
     | _ -> raise Not_found)
   with Not_found -> raise (Attribute_not_found name)
+let assert_element n name =
+  match n#node_type with
+  | T_element n when n = name ->
+      ()
+  | _ -> raise (Parse_error ("", "Expected node: " ^ name))
 
   (** given a string representation of a proof asistant state (e.g. the first
   child of the XML root of a State_change or Start_musing message), build from
   it an HBugs view of a proof assistant state *)
 let parse_state (root: ('a node extension as 'a) node) =
-  let assert_element n name =
-    match n#node_type with
-    | T_element n when n = name ->
-        ()
-    | _ -> raise (Parse_error ("", "Expected node: " ^ name))
-  in
+  if (List.filter is_xml_element root#sub_nodes) = [] then
+    raise Empty_node;
   let buf = Buffer.create 10240 in
   let node_to_string (node: ('a node extension as 'a) node) =
     Buffer.clear buf;
@@ -69,15 +71,14 @@ let parse_state (root: ('a node extension as 'a) node) =
   let (goal_node, type_node, body_node) =
     try
       (find_element "CurrentGoal" root,
-       find_element "ConstantType" root,  (* TODO e' sempre ConstantType? *)
+       find_element "ConstantType" root,
        find_element "CurrentProof" root)
     with Not_found ->
       raise (Parse_error ("", "Malformed HBugs status XML document"))
   in
   assert_element root "gTopLevelStatus";
   assert_element goal_node "CurrentGoal";
-  assert_element type_node "ConstantType";  (* TODO: tutti gli xml 'type' hanno
-                                            come root element "ConstantType"? *)
+  assert_element type_node "ConstantType";
   assert_element body_node "CurrentProof";
   goal_node#write (`Out_buffer buf) `Enc_utf8;
   let (type_string, body_string) =
@@ -154,12 +155,7 @@ let msg_of_string' s =
       State_change
         (get_attr root "id",
         match state_node with
-        | Some n ->
-            if n#sub_nodes = [] then  (* TODO don't trust all sub_nodes,
-                                      consider only element sub_nodes *)
-              None
-            else
-              Some (parse_state n)
+        | Some n -> (try Some (parse_state n) with Empty_node -> None)
         | None -> None)
   | T_element "wow" -> Wow (get_attr root "id")
 
-- 
2.39.2