From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 22 Jan 2004 12:26:43 +0000 (+0000)
Subject: located parse error message
X-Git-Tag: V_0_5_1_4~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4426c9ebff12c236150841eb04374ae5f9cc733f;p=helm.git

located parse error message
---

diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/parser.ml
index 1621b3ccc..8b53c3aac 100644
--- a/helm/ocaml/cic_disambiguation/parser.ml
+++ b/helm/ocaml/cic_disambiguation/parser.ml
@@ -31,6 +31,10 @@ let debug_print s =
     prerr_endline "</NEW_TEXTUAL_PARSER>"
   end
 
+open Printf
+
+exception Parse_error of string
+
 let grammar = Grammar.gcreate Lexer.lex
 
 let term = Grammar.Entry.create grammar "term"
@@ -156,5 +160,10 @@ EXTEND
     ];
 END
 
-let parse_term = Grammar.Entry.parse term
+let parse_term stream =
+  try
+    Grammar.Entry.parse term stream
+  with Stdpp.Exc_located ((x, y), exn) ->
+    raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
+        (Printexc.to_string exn)))
 
diff --git a/helm/ocaml/cic_disambiguation/parser.mli b/helm/ocaml/cic_disambiguation/parser.mli
index 661d0c36b..7f855a459 100644
--- a/helm/ocaml/cic_disambiguation/parser.mli
+++ b/helm/ocaml/cic_disambiguation/parser.mli
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+exception Parse_error of string
+
 (** {2 Parsing functions} *)
 
 val parse_term: char Stream.t -> Ast.term