located parse error message

diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/parser.ml
index 1621b3ccc254b8225e547e4a070a650d2a1fca2c..8b53c3aacbf12193783c799bcfc8c5c6375af69c 100644 (file)
--- 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 661d0c36b23605eaec66a59cc87ece4d8889e278..7f855a459e753a817e95784a3fb02e8d3aea8180 100644 (file)
--- 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