From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 11 May 2005 16:39:00 +0000 (+0000)
Subject: handle XmlPushParser.Parse_error exception
X-Git-Tag: single_binding~85
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=c1564f164c3acee3b74593ebc2154d718db7856b;p=helm.git

handle XmlPushParser.Parse_error exception
---

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index 4365184bb..9a0566ec2 100644
--- a/helm/ocaml/cic/cicPushParser.ml
+++ b/helm/ocaml/cic/cicPushParser.ml
@@ -645,6 +645,7 @@ let parse uri filename =
   with
   | Failure "int_of_string" -> parse_error ctxt "integer number expected"
   | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
+  | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg)
   | Parser_failure _
   | Getter_failure _ as exn ->
       raise exn