]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/xmlDiff.ml
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / gTopLevel / xmlDiff.ml
index e162100285afeee0fc8e5f014785c2121d0ecbd7..307e02ac0db8c325fd45b0b5ebb3158a89118a3c 100644 (file)
@@ -53,7 +53,7 @@ let highlight_node ?(color="yellow") (doc: Gdome.document) (n: Gdome.node) =
     ~namespaceURI:(Some (Gdome.domString mathmlns))
     ~qualifiedName:(Gdome.domString "m:mstyle")
   in
-   highlighter#setAttribute ~name:(Gdome.domString "background")
+   highlighter#setAttribute ~name:(Gdome.domString "mathbackground")
     ~value:(Gdome.domString color) ;
    highlighter#setAttributeNS
     ~namespaceURI:(Some (Gdome.domString xmldiffns))
@@ -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