* minor correction to make the new mathml widget work better

[helm.git] / helm / gTopLevel / xmlDiff.ml

diff --git a/helm/gTopLevel/xmlDiff.ml b/helm/gTopLevel/xmlDiff.ml
index cd19beb0ca1adc754606f02472880676fca6ffd2..c3a35ad34c1b0cf89829989b3a437bfb7e53de47 100644 (file)
--- a/helm/gTopLevel/xmlDiff.ml
+++ b/helm/gTopLevel/xmlDiff.ml
@@ -181,7 +181,7 @@ let update_dom ~(from : Gdome.document) (d : Gdome.document) =
   else
    let t' = from#importNode t true in
     ignore (p#replaceChild ~newChild:t' ~oldChild:f) ;
-    ignore (highlight_node from t')
+    (* ignore (highlight_node from t') *)
   in
   match
    f#get_nodeType,t#get_nodeType
@@ -304,7 +304,8 @@ let update_dom ~(from : Gdome.document) (d : Gdome.document) =
                 (function n ->
                   let n' = from#importNode n true in
                     ignore (f#appendChild n') ;
-                    ignore (highlight_node from n')
+                    (* ignore (highlight_node from n') *)
+                   ()
                 ) tl2
             | tl1,[] ->
                List.iter (function n -> ignore (f#removeChild n)) tl1