From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 2 Apr 2003 10:59:38 +0000 (+0000)
Subject: Bugs fixed:
X-Git-Tag: before_refactoring~60
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=cc963878cd6a37db5958d0ec3aaa74c88d71b6fd;hp=a3eced7e154a26057a5840b2f38366cae0f1eb03;p=helm.git

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 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