src/Tools/jEdit/src/isabelle_markup.scala
changeset 44611 857c52a1c3f7
parent 44602 795978192588
child 44706 fe319b45315c
equal deleted inserted replaced
44610:49657380fba6 44611:857c52a1c3f7
    22   // see http://www.w3schools.com/css/css_colornames.asp
    22   // see http://www.w3schools.com/css/css_colornames.asp
    23 
    23 
    24   def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
    24   def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
    25 
    25 
    26   val outdated_color = new Color(238, 227, 227)
    26   val outdated_color = new Color(238, 227, 227)
    27   val unfinished_color = new Color(255, 228, 225)
    27   val outdated1_color = new Color(238, 227, 227, 50)
       
    28   val running_color = new Color(97, 0, 97)
       
    29   val running1_color = new Color(97, 0, 97, 100)
       
    30   val unfinished_color = new Color(255, 160, 160)
       
    31   val unfinished1_color = new Color(255, 160, 160, 50)
    28 
    32 
    29   val light_color = new Color(240, 240, 240)
    33   val light_color = new Color(240, 240, 240)
    30   val regular_color = new Color(192, 192, 192)
    34   val regular_color = new Color(192, 192, 192)
    31   val warning_color = new Color(255, 140, 0)
    35   val warning_color = new Color(255, 140, 0)
    32   val error_color = new Color(178, 34, 34)
    36   val error_color = new Color(178, 34, 34)
    51   /* command status */
    55   /* command status */
    52 
    56 
    53   def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    57   def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    54   {
    58   {
    55     val state = snapshot.command_state(command)
    59     val state = snapshot.command_state(command)
    56     if (snapshot.is_outdated) Some(outdated_color)
    60     if (snapshot.is_outdated) Some(outdated1_color)
    57     else
    61     else
    58       Isar_Document.command_status(state.status) match {
    62       Isar_Document.command_status(state.status) match {
    59         case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    63         case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
    60         case Isar_Document.Unprocessed => Some(unfinished_color)
    64         case Isar_Document.Unprocessed => Some(unfinished1_color)
    61         case _ => None
    65         case _ => None
    62       }
    66       }
    63   }
    67   }
    64 
    68 
    65   def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    69   def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    66   {
    70   {
    67     val state = snapshot.command_state(command)
    71     val state = snapshot.command_state(command)
    68     if (snapshot.is_outdated) None
    72     if (snapshot.is_outdated) None
    69     else
    73     else
    70       Isar_Document.command_status(state.status) match {
    74       Isar_Document.command_status(state.status) match {
    71         case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
    75         case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
    72         case Isar_Document.Unprocessed => Some(unfinished_color)
    76         case Isar_Document.Unprocessed => Some(unfinished_color)
    73         case Isar_Document.Failed => Some(error_color)
    77         case Isar_Document.Failed => Some(error_color)
    74         case Isar_Document.Finished =>
    78         case Isar_Document.Finished =>
    75           if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
    79           if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
    76           else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
    80           else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)