DisambiguationError exceptions (that have locations inside) are now relocated

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4413f9b8a3bbc0726c752a1cdd53fcafe564df71..7569584274221cc125e438101f329c0da6265c9d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -230,14 +230,13 @@ 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
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
       let term = disambiguate_macro_term term status user_goal in
-      let l =  MQ.match_term ~dbd term in
+      let l =  Whelp.match_term ~dbd term in
       let query_url =
         MatitaMisc.strip_suffix ~suffix:"."
           (HExtlib.trim_blanks unparsed_text)
@@ -247,12 +246,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
       [], parsed_text_length
   | TA.WInstance (loc, term) ->
       let term = disambiguate_macro_term term status user_goal in
-      let l = MQ.instance ~dbd term in
+      let l = Whelp.instance ~dbd term in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WLocate (loc, s) -> 
-      let l = MQ.locate ~dbd s in
+      let l = Whelp.locate ~dbd s in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
@@ -263,7 +262,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
         | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None 
         | _ -> failwith "Not a MutInd"
       in
-      let l = MQ.elim ~dbd uri in
+      let l = Whelp.elim ~dbd uri in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
@@ -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 ->