(List.map
(fun (pass,l) ->
List.map
- (fun (env,diff,offset,msg,significant) ->
- offset, [[pass], [[pass], env, diff], msg, significant]) l
+ (fun (env,diff,offset_msg,significant) ->
+ let offset, msg = Lazy.force offset_msg in
+ offset, [[pass], [[pass], env, diff], lazy msg, significant]) l
) errorll) in
(* Here we are doing a stable sort and list_uniq returns the latter
"equal" element. I.e. we are showing the error corresponding to the
| CicRefine.RefineFailure msg
| CicRefine.AssertFailure msg ->
None, "Refiner error: " ^ Lazy.force msg
+ | NCicRefiner.RefineFailure msg ->
+ None, "NRefiner failure: " ^ snd (Lazy.force msg)
+ | NCicTypeChecker.TypeCheckerFailure msg ->
+ None, "NTypeChecker failure: " ^ Lazy.force msg
+ | NCicTypeChecker.AssertFailure msg ->
+ None, "NTypeChecker assert failure: " ^ Lazy.force msg
+ | NCicRefiner.AssertFailure msg ->
+ None, "NRefiner assert failure: " ^ Lazy.force msg
+ | NCicEnvironment.BadDependency (msg,e) ->
+ None, "NCicEnvironment bad dependency: " ^ Lazy.force msg ^
+ snd (to_string e)
+ | NCicEnvironment.BadConstraint msg ->
+ None, "NCicEnvironment bad constraint: " ^ Lazy.force msg
| CicTypeChecker.TypeCheckerFailure msg ->
None, "Type checking error: " ^ Lazy.force msg
| CicTypeChecker.AssertFailure msg ->
None, "Type checking assertion failed: " ^ Lazy.force msg
| LibrarySync.AlreadyDefined s ->
None, "Already defined: " ^ UriManager.string_of_uri s
- | CoercDb.EqCarrNotImplemented msg ->
- None, ("EqCarrNotImplemented: " ^ Lazy.force msg)
+ | DisambiguateChoices.Choice_not_found msg ->
+ None, ("Disambiguation choice not found: " ^ Lazy.force msg)
| MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->
None, "EnrichedWithLexiconStatus "^snd(to_string exn)
- | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+ | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
let loc =
match errorll with
- ((_,_,Some floc,_,_)::_)::_ ->
- let (x, y) = HExtlib.loc_of_floc floc in
- let x = x + offset in
- let y = y + offset in
- let floc = HExtlib.floc_of_loc (x,y) in
- Some floc
- | _ -> None in
+ | ((_,_,loc_msg,_)::_)::_ ->
+ let floc, _ = Lazy.force loc_msg in
+ if floc = Stdpp.dummy_loc then None else
+ let (x, y) = HExtlib.loc_of_floc floc in
+ let x = x + offset in
+ let y = y + offset in
+ let floc = HExtlib.floc_of_loc (x,y) in
+ Some floc
+ | _ -> assert false
+ in
let annotated_errorll =
List.rev
(snd
let msg =
(List.map (fun (passes,_,_,floc,msg,significant) ->
let loc_descr =
- match floc with
- None -> ""
- | Some floc ->
- let (x, y) = HExtlib.loc_of_floc floc in
- sprintf " at %d-%d" (x+offset) (y+offset)
+ if floc = HExtlib.dummy_floc then ""
+ else
+ let (x, y) = HExtlib.loc_of_floc floc in
+ sprintf " at %d-%d" (x+offset) (y+offset)
in
"*" ^ (if not significant then "(Spurious?) " else "")
^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg,