- severe bug fixing

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

diff --git a/helm/gTopLevel/xmlDiff.mli b/helm/gTopLevel/xmlDiff.mli
index c62df033ba40c92f76195814590caa2900d5a558..cf084af946818780aceedd7c40e8af03aecddc8d 100644 (file)
--- a/helm/gTopLevel/xmlDiff.mli
+++ b/helm/gTopLevel/xmlDiff.mli
@@ -24,3 +24,7 @@
  *)
 
 val update_dom: from: Gdome.document -> Gdome.document -> unit
+
+type highlighted_nodes
+val highlight_nodes: xrefs:(string list) -> Gdome.document -> highlighted_nodes
+val dim_nodes: highlighted_nodes -> unit