src/Pure/PIDE/rendering.scala
changeset 72902 3c09adb4b042
parent 72901 16fd39c9e31f
child 72903 8f586c241071
equal deleted inserted replaced
72901:16fd39c9e31f 72902:3c09adb4b042
   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(Markup.ENTITY, props), _))) =>
   449                 props match {
   449                 props match {
   450                   case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
   450                   case Markup.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
   451                   case Markup.Entity.Ref(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
   452                   case _ => None
   453                 }
   453                 }
   454               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
   454               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
   455                 val color =
   455                 val color =
   456                   depth % 4 match {
   456                   depth % 4 match {
   507       snapshot.cumulate[Rendering.Focus](range, Rendering.Focus.empty, Rendering.entity_elements,
   507       snapshot.cumulate[Rendering.Focus](range, Rendering.Focus.empty, Rendering.entity_elements,
   508         _ =>
   508         _ =>
   509           {
   509           {
   510             case (focus, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   510             case (focus, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   511               props match {
   511               props match {
   512                 case Markup.Entity.Def(i) if check(true, i) => Some(focus + i)
   512                 case Markup.Def(i) if check(true, i) => Some(focus + i)
   513                 case Markup.Entity.Ref(i) if check(false, i) => Some(focus + i)
   513                 case Markup.Ref(i) if check(false, i) => Some(focus + i)
   514                 case _ => None
   514                 case _ => None
   515               }
   515               }
   516             case _ => None
   516             case _ => None
   517           }).iterator.map(_.info))
   517           }).iterator.map(_.info))
   518   }
   518   }
   534       val results =
   534       val results =
   535         snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
   535         snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
   536           {
   536           {
   537             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   537             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   538               props match {
   538               props match {
   539                 case Markup.Entity.Def(i) if focus(i) => Some(true)
   539                 case Markup.Def(i) if focus(i) => Some(true)
   540                 case Markup.Entity.Ref(i) if focus(i) => Some(true)
   540                 case Markup.Ref(i) if focus(i) => Some(true)
   541                 case _ => None
   541                 case _ => None
   542               }
   542               }
   543           })
   543           })
   544       for (info <- results if info.info) yield info.range
   544       for (info <- results if info.info) yield info.range
   545     }
   545     }