src/Tools/jEdit/src/rendering.scala
changeset 60878 1f0d2bbcf38b
parent 60876 52edced9cce5
child 60880 fa958e24ff24
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 16:14:50 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 17:49:36 2015 +0200
     1.3 @@ -149,6 +149,8 @@
     1.4  
     1.5    private val citation_elements = Markup.Elements(Markup.CITATION)
     1.6  
     1.7 +  private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
     1.8 +
     1.9    private val highlight_elements =
    1.10      Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
    1.11        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    1.12 @@ -339,6 +341,17 @@
    1.13        }).headOption.map(_.info)
    1.14  
    1.15  
    1.16 +  /* breakpoints */
    1.17 +
    1.18 +  def breakpoints(range: Text.Range): List[Long] =
    1.19 +    snapshot.select(range, Rendering.breakpoint_elements, _ =>
    1.20 +      {
    1.21 +        case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
    1.22 +          Some(serial)
    1.23 +        case _ => None
    1.24 +      }).map(_.info)
    1.25 +
    1.26 +
    1.27    /* command status overview */
    1.28  
    1.29    def overview_limit: Int = options.int("jedit_text_overview_limit")