From: Claudio Sacerdoti Coen Date: Mon, 28 Nov 2005 12:58:02 +0000 (+0000) Subject: DisambiguationError exceptions (that have locations inside) are now relocated X-Git-Tag: make_still_working~8078 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8653d506aacaf019deb3438bd4681ad1000061bd;p=helm.git 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 d46f9a1bf..325e290a7 100644 --- 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 64cd5563b..4cd1bd0dd 100644 --- 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 10d29cac2..84291dcc6 100644 --- 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 38951713e..b79fea663 100644 --- 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 08e3a4599..756958427 100644 --- 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 1bb8ac955..bee671ee8 100644 --- 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 fc88b6cf8..a2cc0d0e7 100644 --- 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 :