# HG changeset patch
# User wenzelm
# Date 1315259476 -7200
# Node ID 81f683feaead6397866cd516668395d25474b2b3
# Parent  a8331fb5c959de8f037cf1985281f84bae4f9e6f
more visible outdated_color;

diff -r a8331fb5c959 -r 81f683feaead src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Mon Sep 05 23:26:41 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Mon Sep 05 23:51:16 2011 +0200
@@ -24,7 +24,6 @@
   def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
 
   val outdated_color = new Color(238, 227, 227)
-  val outdated1_color = new Color(238, 227, 227, 50)
   val running_color = new Color(97, 0, 97)
   val running1_color = new Color(97, 0, 97, 100)
   val unfinished_color = new Color(255, 160, 160)
@@ -57,7 +56,7 @@
   def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   {
     val state = snapshot.command_state(command)
-    if (snapshot.is_outdated) Some(outdated1_color)
+    if (snapshot.is_outdated) Some(outdated_color)
     else
       Isar_Document.command_status(state.status) match {
         case Isar_Document.Forked(i) if i > 0 => Some(running1_color)