diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-12 11:10:28 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-12 11:10:28 +0200 |
commit | 32b424902383a99436439a3c8ee24a528d1077a9 (patch) | |
tree | dcf2c6e9e732d153f28e446e5ea748fa529329be | |
parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) | |
parent | df5c63872c2630d79b23c128ac47a62de3e9c322 (diff) |
Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac failure in other file
-rw-r--r-- | lib/loc.ml | 5 | ||||
-rw-r--r-- | lib/loc.mli | 4 | ||||
-rw-r--r-- | plugins/ltac/tactic_debug.ml | 6 |
3 files changed, 11 insertions, 4 deletions
diff --git a/lib/loc.ml b/lib/loc.ml index 6f5283aab..1a09091bf 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -62,6 +62,11 @@ let merge_opt l1 l2 = match l1, l2 with | None, Some l -> Some l | Some l1, Some l2 -> Some (merge l1 l2) +let finer l1 l2 = match l1, l2 with + | None, _ -> false + | Some l , None -> true + | Some l1, Some l2 -> l1.fname = l2.fname && merge l1 l2 = l2 + let unloc loc = (loc.bp, loc.ep) let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp } diff --git a/lib/loc.mli b/lib/loc.mli index 813c45fbb..23df1ebd9 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -42,6 +42,10 @@ val merge : t -> t -> t val merge_opt : t option -> t option -> t option (** Merge locations, usually generating the largest possible span *) +val finer : t option -> t option -> bool +(** Answers [true] when the first location is more defined, or, when + both defined, included in the second one *) + val shift_loc : int -> int -> t -> t (** [shift_loc loc n p] shifts the beginning of location by [n] and the end by [p]; it is assumed that the shifts do not change the diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 57a11d947..105b5c59a 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -399,8 +399,6 @@ let skip_extensions trace = | [] -> [] in List.rev (aux (List.rev trace)) -let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2 - let extract_ltac_trace ?loc trace = let trace = skip_extensions trace in let (tloc,c),tail = List.sep_last trace in @@ -408,7 +406,7 @@ let extract_ltac_trace ?loc trace = (* We entered a user-defined tactic, we display the trace with location of the call *) let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in - (if finer_loc loc tloc then loc else tloc), Some msg + (if Loc.finer loc tloc then loc else tloc), Some msg else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -417,7 +415,7 @@ let extract_ltac_trace ?loc trace = let rec aux best_loc = function | (loc,_)::tail -> if Option.is_empty best_loc || - not (Option.is_empty loc) && finer_loc loc best_loc + not (Option.is_empty loc) && Loc.finer loc best_loc then aux loc tail else |