src/Pure/PIDE/rendering.scala
changeset 65101 4263b2a201b3
parent 64877 31e9920a0dc1
child 65104 66b19d05dcee
     1.1 --- a/src/Pure/PIDE/rendering.scala	Sat Mar 04 08:41:32 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Sat Mar 04 09:27:51 2017 +0100
     1.3 @@ -10,6 +10,26 @@
     1.4  
     1.5  object Rendering
     1.6  {
     1.7 +  /* color */
     1.8 +
     1.9 +  object Color extends Enumeration
    1.10 +  {
    1.11 +    val unprocessed1 = Value("unprocessed1")
    1.12 +    val running1 = Value("running1")
    1.13 +    val bad = Value("bad")
    1.14 +    val intensify = Value("intensify")
    1.15 +    val entity = Value("entity")
    1.16 +    val quoted = Value("quoted")
    1.17 +    val antiquoted = Value("antiquoted")
    1.18 +    val active = Value("active")
    1.19 +    val active_result = Value("active_result")
    1.20 +    val markdown_item1 = Value("markdown_item1")
    1.21 +    val markdown_item2 = Value("markdown_item2")
    1.22 +    val markdown_item3 = Value("markdown_item3")
    1.23 +    val markdown_item4 = Value("markdown_item4")
    1.24 +  }
    1.25 +
    1.26 +
    1.27    /* message priorities */
    1.28  
    1.29    val state_pri = 1
    1.30 @@ -39,6 +59,22 @@
    1.31  
    1.32    /* markup elements */
    1.33  
    1.34 +  val active_elements =
    1.35 +    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    1.36 +      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
    1.37 +
    1.38 +  private val background_elements =
    1.39 +    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
    1.40 +      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    1.41 +      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    1.42 +      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    1.43 +      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
    1.44 +      Markup.Markdown_Item.name ++ active_elements
    1.45 +
    1.46 +  private val foreground_elements =
    1.47 +    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    1.48 +      Markup.CARTOUCHE, Markup.ANTIQUOTED)
    1.49 +
    1.50    private val semantic_completion_elements =
    1.51      Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    1.52  
    1.53 @@ -187,6 +223,76 @@
    1.54    }
    1.55  
    1.56  
    1.57 +  /* text background */
    1.58 +
    1.59 +  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
    1.60 +  {
    1.61 +    for {
    1.62 +      Text.Info(r, result) <-
    1.63 +        snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
    1.64 +          range, (List(Markup.Empty), None), Rendering.background_elements,
    1.65 +          command_states =>
    1.66 +            {
    1.67 +              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
    1.68 +              if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
    1.69 +                Some((markup :: markups, color))
    1.70 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
    1.71 +                Some((Nil, Some(Rendering.Color.bad)))
    1.72 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    1.73 +                Some((Nil, Some(Rendering.Color.intensify)))
    1.74 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    1.75 +                props match {
    1.76 +                  case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
    1.77 +                  case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
    1.78 +                  case _ => None
    1.79 +                }
    1.80 +              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
    1.81 +                val color =
    1.82 +                  depth match {
    1.83 +                    case 1 => Rendering.Color.markdown_item1
    1.84 +                    case 2 => Rendering.Color.markdown_item2
    1.85 +                    case 3 => Rendering.Color.markdown_item3
    1.86 +                    case _ => Rendering.Color.markdown_item4
    1.87 +                  }
    1.88 +                Some((Nil, Some(color)))
    1.89 +              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    1.90 +                command_states.collectFirst(
    1.91 +                  { case st if st.results.defined(serial) => st.results.get(serial).get }) match
    1.92 +                {
    1.93 +                  case Some(Protocol.Dialog_Result(res)) if res == result =>
    1.94 +                    Some((Nil, Some(Rendering.Color.active_result)))
    1.95 +                  case _ =>
    1.96 +                    Some((Nil, Some(Rendering.Color.active)))
    1.97 +                }
    1.98 +              case (_, Text.Info(_, elem)) =>
    1.99 +                if (Rendering.active_elements(elem.name))
   1.100 +                  Some((Nil, Some(Rendering.Color.active)))
   1.101 +                else None
   1.102 +            })
   1.103 +      color <-
   1.104 +        (result match {
   1.105 +          case (markups, opt_color) if markups.nonEmpty =>
   1.106 +            val status = Protocol.Status.make(markups.iterator)
   1.107 +            if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
   1.108 +            else if (status.is_running) Some(Rendering.Color.running1)
   1.109 +            else opt_color
   1.110 +          case (_, opt_color) => opt_color
   1.111 +        })
   1.112 +    } yield Text.Info(r, color)
   1.113 +  }
   1.114 +
   1.115 +
   1.116 +  /* text foreground */
   1.117 +
   1.118 +  def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   1.119 +    snapshot.select(range, Rendering.foreground_elements, _ =>
   1.120 +      {
   1.121 +        case Text.Info(_, elem) =>
   1.122 +          if (elem.name == Markup.ANTIQUOTED) Some(Rendering.Color.antiquoted)
   1.123 +          else Some(Rendering.Color.quoted)
   1.124 +      })
   1.125 +
   1.126 +
   1.127    /* caret focus */
   1.128  
   1.129    private def entity_focus(range: Text.Range,