From: Claudio Sacerdoti Coen Date: Thu, 7 Jul 2005 15:33:18 +0000 (+0000) Subject: 1. Warnings are now printed in orange (yellow was unvisible on a white X-Git-Tag: V_0_7_1~10 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6a78ec39e3f2ddceb9d0836e6c2a494aa0f2e421;p=helm.git 1. Warnings are now printed in orange (yellow was unvisible on a white background!) 2. the "Bad name" error is now a "Bad name" warning --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index c204adf06..bb2e3c1a6 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -524,7 +524,7 @@ let eval_command status cmd = Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> let name = UriManager.name_of_uri uri in if not(CicPp.check name ty) then - MatitaLog.error ("Bad name: "^name); + MatitaLog.warn ("Bad name: " ^ name); assert (metasenv = metasenv'); let goalno = match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index de8e36196..5ea390383 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -42,7 +42,7 @@ end class console ~(buffer: GText.buffer) () = object (self) val error_tag = buffer#create_tag [ `FOREGROUND "red" ] - val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ] + val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ] val message_tag = buffer#create_tag [] val debug_tag = buffer#create_tag [ `FOREGROUND "#888888" ] method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s