From: Claudio Sacerdoti Coen 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