src/Pure/PIDE/rendering.scala
changeset 72903 8f586c241071
parent 72902 3c09adb4b042
child 72904 b44b2d2380f0
equal deleted inserted replaced
72902:3c09adb4b042 72903:8f586c241071
   443                 Some((markup :: markups, color))
   443                 Some((markup :: markups, color))
   444               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   444               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   445                 Some((Nil, Some(Rendering.Color.bad)))
   445                 Some((Nil, Some(Rendering.Color.bad)))
   446               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   446               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   447                 Some((Nil, Some(Rendering.Color.intensify)))
   447                 Some((Nil, Some(Rendering.Color.intensify)))
   448               case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   448               case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) =>
   449                 props match {
   449                 Some((Nil, Some(Rendering.Color.entity)))
   450                   case Markup.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
       
   451                   case Markup.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
       
   452                   case _ => None
       
   453                 }
       
   454               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
   450               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
   455                 val color =
   451                 val color =
   456                   depth % 4 match {
   452                   depth % 4 match {
   457                     case 1 => Rendering.Color.markdown_bullet1
   453                     case 1 => Rendering.Color.markdown_bullet1
   458                     case 2 => Rendering.Color.markdown_bullet2
   454                     case 2 => Rendering.Color.markdown_bullet2
   532     val focus = caret_focus(caret_range, visible_range)
   528     val focus = caret_focus(caret_range, visible_range)
   533     if (focus.defined) {
   529     if (focus.defined) {
   534       val results =
   530       val results =
   535         snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
   531         snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
   536           {
   532           {
   537             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   533             case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => Some(true)
   538               props match {
   534             case _ => None
   539                 case Markup.Def(i) if focus(i) => Some(true)
       
   540                 case Markup.Ref(i) if focus(i) => Some(true)
       
   541                 case _ => None
       
   542               }
       
   543           })
   535           })
   544       for (info <- results if info.info) yield info.range
   536       for (info <- results if info.info) yield info.range
   545     }
   537     }
   546     else Nil
   538     else Nil
   547   }
   539   }