DisambiguationError exceptions (that have locations inside) are now relocated

correctly after a (** comment *).

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index d46f9a1bfbefd5b059623adabfa65dbab046cfbd..325e290a74f4636d231d136b2b2f2995808cc597 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -28,8 +28,9 @@ open Printf
 open MatitaTypes
 
 exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
 exception DisambiguationError of
- (Token.flocation option * string Lazy.t) list list
+ int * (Token.flocation option * string Lazy.t) list list
 
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list
@@ -110,12 +111,12 @@ let disambiguate_thing ~aliases ~universe
     | [ pass ] ->
         (try
           set_aliases pass (try_pass pass)
-         with Disambiguate.NoWellTypedInterpretation newerrors ->
-          raise (DisambiguationError (errors @ [newerrors])))
+         with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
+          raise (DisambiguationError (offset, errors @ [newerrors])))
     | hd :: tl ->
         (try
           set_aliases hd (try_pass hd)
-        with Disambiguate.NoWellTypedInterpretation newerrors ->
+        with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
          aux (errors @ [newerrors]) tl)
     | [] -> assert false
   in

diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli
index 64cd5563b1d691d6035b54c03f03607f35b976fb..4cd1bd0dde0fc798544ff21cfe09996e57927fc5 100644 (file)
--- a/helm/matita/matitaDisambiguator.mli
+++ b/helm/matita/matitaDisambiguator.mli
@@ -28,8 +28,9 @@ open MatitaTypes
 (** raised when ambiguous input is found but not expected (e.g. in the batch
   * compiler) *)
 exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
 exception DisambiguationError of
- (Token.flocation option * string Lazy.t) list list
+ int * (Token.flocation option * string Lazy.t) list list
 
 type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
 type choose_interp_callback = (string * string) list list -> int list

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 10d29cac200c122153348ae0aa2d9fbb94f6f6e7..84291dcc6582866cdfa31c06d5683cbb4130788d 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -253,7 +253,7 @@ let disambiguate_tactic status goal tactic =
               with
               | Cic.MutInd (uri, tyno, _) ->
                   (GrafiteAst.Type (uri, tyno) :: types)
-              | _ -> raise (MatitaDisambiguator.DisambiguationError [[None,lazy "Decompose works only on inductive types"]]))
+              | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]])))
         in
         let types = List.fold_left disambiguate [] types in
         GrafiteAst.Decompose (loc, types, what, names)

diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml
index 38951713eab19127332836aa3d6f84aed11b2205..b79fea6631212e79be1374aa8041800af9c91bc2 100644 (file)
--- a/helm/matita/matitaExcPp.ml
+++ b/helm/matita/matitaExcPp.ml
@@ -61,7 +61,7 @@ let rec to_string =
      None, "Type checking error: " ^ Lazy.force msg
   | CicTypeChecker.AssertFailure msg ->
      None, "Type checking assertion failed: " ^ Lazy.force msg
-  | MatitaDisambiguator.DisambiguationError errorll ->
+  | MatitaDisambiguator.DisambiguationError (offset,errorll) ->
      let rec aux n =
       function
          [] -> ""
@@ -75,13 +75,21 @@ let rec to_string =
                    None -> ""
                  | Some floc ->
                     let (x, y) = HExtlib.loc_of_floc floc in
-                     sprintf " at %d-%d" x y
+                     sprintf " at %d-%d" (x+offset) (y+offset)
                in
                 "*Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase) ^
             "\n\n\n" in
      let loc =
       match errorll with
-         ((Some _ as loc,_)::_)::_ -> loc
+         ((Some floc,_)::_)::_ ->
+          let (x, y) = HExtlib.loc_of_floc floc in
+          let x = x + offset in
+          let y = y + offset in
+          let flocb,floce = floc in
+          let floc =
+           {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y}
+          in
+           Some floc
        | _ -> None
      in
       loc,

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 08e3a45991ce6a53fbd9dbc5d2916e2245d6aa30..7569584274221cc125e438101f329c0da6265c9d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -394,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 ->

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 1bb8ac9550570c0e1883a86a2dbe753cfe10e5e5..bee671ee8ecbdfec342daa090a16638f300143b5 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -28,8 +28,9 @@ open Printf
 open DisambiguateTypes
 open UriManager
 
+(* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- (Token.flocation option * string Lazy.t) list
+ int * (Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -962,7 +963,7 @@ in refine_profiler.HExtlib.profile foo ()
       try
         let res =
          match aux aliases [] None todo_dom base_univ with
-         | [],errors -> raise (NoWellTypedInterpretation errors)
+         | [],errors -> raise (NoWellTypedInterpretation (0,errors))
          | [_,diff,metasenv,t,ugraph],_ ->
              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index fc88b6cf84d54320fb092cb9a3f67763a1585897..a2cc0d0e7b04489333cadfb33572aa9b60dfbb49 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -25,8 +25,9 @@
 
 (** {2 Disambiguation interface} *)
 
+(* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- (Token.flocation option * string Lazy.t) list
+ int * (Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
 val interpretate_path :