From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 28 Jul 2003 13:28:11 +0000 (+0000)
Subject: Bug fixed: it could have happened that the tree structured becomes scrambled
X-Git-Tag: LucaOK~27
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=122304a548cba036c8bb3769e00276b2eb3f179d

Bug fixed: it could have happened that the tree structured becomes scrambled
by the highlighting operation.
---

diff --git a/helm/gTopLevel/xmlDiff.ml b/helm/gTopLevel/xmlDiff.ml
index e16210028..9468ccc3f 100644
--- a/helm/gTopLevel/xmlDiff.ml
+++ b/helm/gTopLevel/xmlDiff.ml
@@ -64,8 +64,9 @@ let highlight_node ?(color="yellow") (doc: Gdome.document) (n: Gdome.node) =
        None -> assert false
      | Some p -> p
    in
+    ignore
+     (parent#replaceChild ~oldChild:n ~newChild:(highlighter :> Gdome.node)) ;
     ignore (highlighter#appendChild n) ;
-    ignore (parent#appendChild (highlighter :> Gdome.node)) ;
     (highlighter :> Gdome.node)
  in
   let rec find_mstylable_node n =
@@ -365,32 +366,28 @@ prerr_endline ("Rimpiazzo" ^ (match f#get_namespaceURI with Some s -> s#to_strin
     (d#get_documentElement :> Gdome.node)
   with
      (GdomeInit.DOMException (e,msg) as ex) ->
-(*
+(* CSC: Non si puo' per problemi di linking ;-(
     let module E = GdomeDOMExceptionT in
 *)
        prerr_endline
         ("DOM EXCEPTION: " ^ msg ^ " --- " ^
-string_of_int (Obj.magic e)) ;
-       raise ex
- (*
-        match e with
-           E.NO_ERR -> "NO_ERR"
-         | E.INDEX_SIZE_ERR -> "INDEX_SIZE_ERR"
-         | E.DOMSTRING_SIZE_ERR -> "DOMSTRING_SIZE_ERR"
-         | E.HIERARCHY_REQUEST_ERR -> "HIERARCHY_REQUEST_ERR"
-         | E.WRONG_DOCUMENT_ERR -> "WRONG_DOCUMENT_ERR"
-         | E.INVALID_CHARACTER_ERR -> "INVALID_CHARACTER_ERR"
-         | E.NO_DATA_ALLOWED_ERR -> "NO_DATA_ALLOWER_ERR"
-         | E.NO_MODIFICATION_ALLOWED_ERR -> "NO_MODIFICATION_ALLOWED_ERR"
-         | E.NOT_FOUND_ERR -> "NOT_FOUND_ERR"
-         | E.NOT_SUPPORTED_ERR -> "NOT_SUPPORTED_ERR"
-         | E.INUSE_ATTRIBUTE_ERR -> "INUSE_ATTRIBUTE_ERR"
-         | E.INVALID_STATE_ERR -> "INVALID_STATE_ERR"
-         | E.SYNTAX_ERR -> "SYNTAX_ERR"
-         | E.INVALID_MODIFICATION_ERR -> "INVALID_MODIFICATION_ERR"
-         | E.NAMESPACE_ERR -> "NAMESPACE_ERR"
-         | E.INVALID_ACCESS_ERR -> "INVALID_ACCESS_ERR"
-*)
+          match e with
+             GdomeDOMExceptionT.NO_ERR -> "NO_ERR"
+           | GdomeDOMExceptionT.INDEX_SIZE_ERR -> "INDEX_SIZE_ERR"
+           | GdomeDOMExceptionT.DOMSTRING_SIZE_ERR -> "DOMSTRING_SIZE_ERR"
+           | GdomeDOMExceptionT.HIERARCHY_REQUEST_ERR -> "HIERARCHY_REQUEST_ERR"
+           | GdomeDOMExceptionT.WRONG_DOCUMENT_ERR -> "WRONG_DOCUMENT_ERR"
+           | GdomeDOMExceptionT.INVALID_CHARACTER_ERR -> "INVALID_CHARACTER_ERR"
+           | GdomeDOMExceptionT.NO_DATA_ALLOWED_ERR -> "NO_DATA_ALLOWER_ERR"
+           | GdomeDOMExceptionT.NO_MODIFICATION_ALLOWED_ERR -> "NO_MODIFICATION_ALLOWED_ERR"
+           | GdomeDOMExceptionT.NOT_FOUND_ERR -> "NOT_FOUND_ERR"
+           | GdomeDOMExceptionT.NOT_SUPPORTED_ERR -> "NOT_SUPPORTED_ERR"
+           | GdomeDOMExceptionT.INUSE_ATTRIBUTE_ERR -> "INUSE_ATTRIBUTE_ERR"
+           | GdomeDOMExceptionT.INVALID_STATE_ERR -> "INVALID_STATE_ERR"
+           | GdomeDOMExceptionT.SYNTAX_ERR -> "SYNTAX_ERR"
+           | GdomeDOMExceptionT.INVALID_MODIFICATION_ERR -> "INVALID_MODIFICATION_ERR"
+           | GdomeDOMExceptionT.NAMESPACE_ERR -> "NAMESPACE_ERR"
+           | GdomeDOMExceptionT.INVALID_ACCESS_ERR -> "INVALID_ACCESS_ERR")
   | e ->
     prerr_endline "PROBLEMA" ;
     raise e