Bugs fixed:

1. It was assumed that no CDATA nodes were put between XML elements.
   But the generated hint XML files had newlines to pretty-print the XML.
   The current fix ignores every CDATA nodes. Maybe it should just ignore the
   ones made of blancks.
2. Tree-structured hints were not parsed correctly (the coe was simply
   wrong). Trivially fixed.

Open issue: my code is full of "assert false". Should it raise exceptions
instead? I firmly think so.

diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml
index c0f70948462badd3f2a6678a7fafea2e365ce758..0cc0f1b1fe599d079c21f79248a7253ebe361e10 100644 (file)
--- a/helm/hbugs/common/hbugs_messages.ml
+++ b/helm/hbugs/common/hbugs_messages.ml
@@ -93,23 +93,29 @@ let parse_state (root: ('a node extension as 'a) node) =
 
   (** parse an hint from an XML node, XML node should have type 'T_element _'
   (the name is ignored), attributes on it are ignored *)
-let rec parse_hint node =
-  let child = node#nth_node 0 in
-  match child#node_type with
-  | T_element "ring" -> Use_ring_Luke
-  | T_element "fourier" -> Use_fourier_Luke
-  | T_element "reflexivity" -> Use_reflexivity_Luke
-  | T_element "symmetry" -> Use_symmetry_Luke
-  | T_element "assumption" -> Use_assumption_Luke
-  | T_element "contradiction" -> Use_contradiction_Luke
-  | T_element "exists" -> Use_exists_Luke
-  | T_element "split" -> Use_split_Luke
-  | T_element "left" -> Use_left_Luke
-  | T_element "right" -> Use_right_Luke
-  | T_element "apply" -> Use_apply_Luke node#data
-  | T_element "hints" ->
-      Hints (List.map parse_hint (List.filter is_xml_element node#sub_nodes))
-  | _ -> assert false
+let parse_hint node =
+ let rec parse_hint_node node =
+   match node#node_type with
+   | T_element "ring" -> Use_ring_Luke
+   | T_element "fourier" -> Use_fourier_Luke
+   | T_element "reflexivity" -> Use_reflexivity_Luke
+   | T_element "symmetry" -> Use_symmetry_Luke
+   | T_element "assumption" -> Use_assumption_Luke
+   | T_element "contradiction" -> Use_contradiction_Luke
+   | T_element "exists" -> Use_exists_Luke
+   | T_element "split" -> Use_split_Luke
+   | T_element "left" -> Use_left_Luke
+   | T_element "right" -> Use_right_Luke
+   | T_element "apply" -> Use_apply_Luke node#data
+   | T_element "hints" ->
+       Hints
+        (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
+   | _ -> assert false (* CSC: should this assert false be a raise something? *)
+ in
+  match List.filter is_xml_element node#sub_nodes with
+     [node] -> parse_hint_node node
+   | _ -> assert false (* CSC: should this assert false be a raise something? *)
+
 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
 let parse_tutor_dscs n =
   List.map