src/Pure/PIDE/rendering.scala
changeset 64767 f5c4ffdb1124
parent 64748 155bf8632104
child 64877 31e9920a0dc1
     1.1 --- a/src/Pure/PIDE/rendering.scala	Tue Jan 03 19:22:17 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Jan 03 21:02:46 2017 +0100
     1.3 @@ -58,6 +58,8 @@
     1.4  
     1.5    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
     1.6      Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
     1.7 +
     1.8 +  val caret_focus_elements = Markup.Elements(Markup.ENTITY)
     1.9  }
    1.10  
    1.11  abstract class Rendering(
    1.12 @@ -162,4 +164,53 @@
    1.13          Some(Text.Info(r, all_tips))
    1.14      }
    1.15    }
    1.16 +
    1.17 +
    1.18 +  /* caret focus */
    1.19 +
    1.20 +  private def entity_focus(range: Text.Range,
    1.21 +    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
    1.22 +  {
    1.23 +    val results =
    1.24 +      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
    1.25 +          {
    1.26 +            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    1.27 +              props match {
    1.28 +                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
    1.29 +                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
    1.30 +                case _ => None
    1.31 +              }
    1.32 +            case _ => None
    1.33 +          })
    1.34 +    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
    1.35 +  }
    1.36 +
    1.37 +  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
    1.38 +  {
    1.39 +    val focus_defs = entity_focus(caret_range)
    1.40 +    if (focus_defs.nonEmpty) focus_defs
    1.41 +    else {
    1.42 +      val visible_defs = entity_focus(visible_range)
    1.43 +      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
    1.44 +    }
    1.45 +  }
    1.46 +
    1.47 +  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
    1.48 +  {
    1.49 +    val focus = caret_focus(caret_range, visible_range)
    1.50 +    if (focus.nonEmpty) {
    1.51 +      val results =
    1.52 +        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
    1.53 +          {
    1.54 +            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    1.55 +              props match {
    1.56 +                case Markup.Entity.Def(i) if focus(i) => Some(true)
    1.57 +                case Markup.Entity.Ref(i) if focus(i) => Some(true)
    1.58 +                case _ => None
    1.59 +              }
    1.60 +          })
    1.61 +      for (info <- results if info.info) yield info.range
    1.62 +    }
    1.63 +    else Nil
    1.64 +  }
    1.65  }