* More error messages localized.

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 3fa4e93e7bf71ed7c68a74f306fc7f74f4daba4e..7569584274221cc125e438101f329c0da6265c9d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -230,7 +230,6 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   let module CTC = CicTypeChecker in
   let module CU = CicUniv in
   (* no idea why ocaml wants this *)
-  let advance ?statement () = script#advance ?statement () in
   let parsed_text_length = String.length parsed_text in
   let dbd = MatitaDb.instance () in
   match mac with
@@ -347,7 +346,6 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
   let module TAPp = GrafiteAstPp in
   let module MD = MatitaDisambiguator in
   let module ML = MatitacleanLib in
-  let parsed_text_length = String.length parsed_text in
   match ex with
   | TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
       (try 
@@ -396,9 +394,13 @@ let rec eval_statement (buffer : GText.buffer) guistuff status user_goal
        try
         eval_statement buffer guistuff status user_goal script
          (`Raw s)
-       with HExtlib.Localized (floc, exn) ->
-        HExtlib.raise_localized_exception
-         ~offset:parsed_text_length floc exn
+       with
+          HExtlib.Localized (floc, exn) ->
+           HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
+        | MatitaDisambiguator.DisambiguationError (offset,errorll) ->
+           raise
+            (MatitaDisambiguator.DisambiguationError
+              (offset+parsed_text_length, errorll))
       in
       (match s with
       | (status, (text, ast)) :: tl ->