X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaExcPp.ml;h=f141b129a73b686448c694a334af057e8d5f7de6;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=c672e2e704598755f91cb943ae05a8b94eecddf9;hpb=fd23c1f47cc9e98f7c0f5251076e2df1198d49e2;p=helm.git diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index c672e2e70..f141b129a 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -23,14 +23,22 @@ * http://helm.cs.unibo.it/ *) -open MatitaTypes;; -open Printf;; +open Printf let to_string = function - | Option_error ("baseuri", "not found" ) -> - "Baseuri not set for this script. Use 'set \"baseuri\" \"\".' to set it." - | CicTextualParser2.Parse_error (floc,err) -> - let (x, y) = CicAst.loc_of_floc floc in + | MatitaTypes.Option_error ("baseuri", "not found" ) -> + "Baseuri not set for this script. " + ^ "Use 'set \"baseuri\" \"\".' to set it." + | MatitaTypes.Command_error msg -> "Error: " ^ msg + | CicNotationParser.Parse_error (floc,err) -> + let (x, y) = CicNotationPt.loc_of_floc floc in sprintf "Parse error at %d-%d: %s" x y err + | UriManager.IllFormedUri uri -> sprintf "invalid uri: %s" uri + | CicEnvironment.Object_not_found uri -> + sprintf "object not found: %s" (UriManager.string_of_uri uri) + | Unix.Unix_error (code, api, param) -> + let err = Unix.error_message code in + "Unix Error (" ^ api ^ "): " ^ err | exn -> "Uncaught exception: " ^ Printexc.to_string exn +