From ad767500db4f2f7ef24e56fd86b2004d715e4a9d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 25 Jul 2005 12:45:09 +0000 Subject: [PATCH] - MatitaLog output redirected to stderr for every message <> Message - matitadep gracefully recovers from the inclusion of a non-existent .ma file --- helm/matita/matitaLog.ml | 14 +++++++------- helm/matita/matitadep.ml | 8 +++++++- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/helm/matita/matitaLog.ml b/helm/matita/matitaLog.ml index 6ac82da58..8d9fbe958 100644 --- a/helm/matita/matitaLog.ml +++ b/helm/matita/matitaLog.ml @@ -40,15 +40,15 @@ let red = "" let black = "" let default_callback tag s = - let prefix = + let prefix,ch = match tag with - | `Message -> green ^ "Info: " - | `Warning -> yellow ^ "Warn: " - | `Error -> red ^ "Error: " - | `Debug -> blue ^ "Debug: " + | `Message -> green ^ "Info: ", stdout + | `Warning -> yellow ^ "Warn: ", stderr + | `Error -> red ^ "Error: ", stderr + | `Debug -> blue ^ "Debug: ", stderr in - print_endline (prefix ^ black ^ s); - flush stdout + output_string ch (prefix ^ black ^ s ^ "\n"); + flush ch let callback = ref default_callback diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 88cac8280..e355ab59c 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -95,7 +95,13 @@ let main () = (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> Hashtbl.add aliases file uri | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> - Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find path)) + (try + Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find path)) + with + Sys_error _ -> + MatitaLog.error + ("In file " ^ file ^ " unable to include " ^ path) + ) | _ -> () with CicNotationParser.Parse_error _ as exn -> -- 2.39.2