From: Claudio Sacerdoti Coen Date: Mon, 26 Nov 2007 12:06:29 +0000 (+0000) Subject: Some code clean-up. X-Git-Tag: make_still_working~5778 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=90a9bd0479b78753498625a85a378720cad35437;p=helm.git Some code clean-up. --- diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 03f0be3dc..8888b8dfe 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -152,6 +152,31 @@ let rec to_string = | CoercDb.EqCarrNotImplemented msg -> None, ("EqCarrNotImplemented: " ^ Lazy.force msg) | GrafiteDisambiguator.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 + let annotated_errorll = + List.rev + (snd + (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) + (0,[]) errorll)) in + let choices = compact_disambiguation_errors true annotated_errorll in + let errorll = + (List.map + (function (loffset,l) -> + List.map + (function + passes,envs_and_diffs,msg,significant -> + let _,env,diff = List.hd envs_and_diffs in + passes,env,diff,loffset,msg,significant + ) l + ) choices) in let rec aux = function [] -> [] @@ -170,15 +195,6 @@ let rec to_string = passes) phase) in msg@aux tl in - 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 let rec explain = function [] -> "" @@ -189,26 +205,6 @@ let rec to_string = String.concat "," (List.map string_of_int phases) ^": *****\n"^ msg ^ "\n\n" in - (* --- *) - let annotated_errorll = - List.rev - (snd - (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) (0,[]) - errorll)) in - let choices = compact_disambiguation_errors true annotated_errorll in - (* --- *) - let errorll = - (List.map - (function (loffset,l) -> - List.map - (function - passes,envs_and_diffs,msg,significant -> - let _,env,diff = List.hd envs_and_diffs in - passes,env,diff,loffset,msg,significant - ) l - ) choices) in - (* --- *) - loc, "********** DISAMBIGUATION ERRORS: **********\n" ^ explain (aux errorll)