* New implementation of localized exceptions

[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index cf2f7b1fce827425e78c96322a55c057a22d878e..e7c54213d8f64f1ebc29d7548e7ec75b7ed5e268 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -161,9 +161,9 @@ EXTEND
     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
         let (pt,_,_) = p in
           if pt <> None then
-            raise (CicNotationParser.Parse_error
-              (loc, "the pattern cannot specify the term to replace, only its"
-              ^ " paths in the hypotheses and in the conclusion"))
+            raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
+              ("the pattern cannot specify the term to replace, only its"
+              ^ " paths in the hypotheses and in the conclusion")))
         else
          GrafiteAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
@@ -203,8 +203,9 @@ EXTEND
        let (pt,_,_) = p in
         if pt <> None then
          raise
-          (CicNotationParser.Parse_error
-            (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))
+          (HExtlib.Localized (loc,
+           (CicNotationParser.Parse_error
+            "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
         else
          GrafiteAst.Rewrite (loc, d, t, p)
     | IDENT "right" ->
@@ -350,10 +351,11 @@ EXTEND
         then
           GrafiteAst.Ident_alias (id, uri)
         else 
-          raise (CicNotationParser.Parse_error (loc,sprintf "Not a valid uri: %s" uri))
+          raise
+           (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
       else
-        raise (CicNotationParser.Parse_error (loc,
-          sprintf "Not a valid identifier: %s" id))
+        raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
+          sprintf "Not a valid identifier: %s" id)))
     | IDENT "symbol"; symbol = QSTRING;
       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
       SYMBOL "="; dsc = QSTRING ->
@@ -493,7 +495,7 @@ EXTEND
     | IDENT "metadata"; [ IDENT "dependency" | IDENT "baseuri" ] ; URI ->
         (** metadata commands lives only in .moo, where they are in marshalled
          * form *)
-        raise (CicNotationParser.Parse_error (loc, "metadata not allowed here"))
+        raise (HExtlib.Localized (loc,CicNotationParser.Parse_error "metadata not allowed here"))
 
     | IDENT "dump" -> GrafiteAst.Dump loc
     | IDENT "render"; u = URI ->
@@ -528,9 +530,10 @@ let exc_located_wrapper f =
   with
   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
   | Stdpp.Exc_located (floc, Stream.Error msg) ->
-      raise (CicNotationParser.Parse_error (floc, msg))
+      raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
   | Stdpp.Exc_located (floc, exn) ->
-      raise (CicNotationParser.Parse_error (floc, (Printexc.to_string exn)))
+      raise
+       (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 
 let parse_statement lexbuf =
   exc_located_wrapper