]> matita.cs.unibo.it Git - helm.git/commitdiff
1. Warnings are now printed in orange (yellow was unvisible on a white
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 7 Jul 2005 15:33:18 +0000 (15:33 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 7 Jul 2005 15:33:18 +0000 (15:33 +0000)
   background!)
2. the "Bad name" error is now a "Bad name" warning

helm/matita/matitaEngine.ml
helm/matita/matitaGui.ml

index c204adf06457e91ff897b53130ace40e8f8e600c..bb2e3c1a66cfc675fe2dc015a93119429fc0f295 100644 (file)
@@ -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
index de8e361965066595f51ac9bd75cc319197f2ece4..5ea3903835f05dafa4a83dc4c6b2711b84aa3a5d 100644 (file)
@@ -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