useless box removed

[helm.git] / helm / software / matita / lablGraphviz.ml

diff --git a/helm/software/matita/lablGraphviz.ml b/helm/software/matita/lablGraphviz.ml
index d67584c8c99d4f700d99f39afa625c654a0c311b..ab817e2940394c19a197810fecd79d6d825711f9 100644 (file)
--- a/helm/software/matita/lablGraphviz.ml
+++ b/helm/software/matita/lablGraphviz.ml
@@ -114,7 +114,8 @@ class graphviz_impl ?packing () =
           "coords", min_x^","^min_y^" "^max_x^","^max_y
          | x -> x) l
       in
-      let p =
+      try
+       let p =
         XmlPushParser.create_parser
           { XmlPushParser.default_callbacks with
             XmlPushParser.start_element =
@@ -123,8 +124,9 @@ class graphviz_impl ?packing () =
                 | "area" when is_rect attrs -> areas := attrs :: !areas
                 | "area" when is_poly attrs -> areas := rectify attrs :: !areas
                 | _ -> ()) } in
-      XmlPushParser.parse p (`File fname);
-      map <- !areas
+       XmlPushParser.parse p (`File fname);
+       map <- !areas  
+      with XmlPushParser.Parse_error _ -> ()
 
     method private find_href x y =
       List.find