X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fcommon%2Fhbugs_messages.ml;h=0cc0f1b1fe599d079c21f79248a7253ebe361e10;hb=d2c60bae1c4badba0a0f29e3fd2faed6d3a1869e;hp=c0f70948462badd3f2a6678a7fafea2e365ce758;hpb=4651ed901a51659c31dbcb9a8b4f75d17321be14;p=helm.git

diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml
index c0f709484..0cc0f1b1f 100644
--- 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