src/Tools/jEdit/src/rendering.scala
changeset 60880 fa958e24ff24
parent 60878 1f0d2bbcf38b
child 60882 45bfd18835f1
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 19:17:49 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 20:22:49 2015 +0200
     1.3 @@ -343,13 +343,18 @@
     1.4  
     1.5    /* breakpoints */
     1.6  
     1.7 -  def breakpoints(range: Text.Range): List[Long] =
     1.8 -    snapshot.select(range, Rendering.breakpoint_elements, _ =>
     1.9 -      {
    1.10 -        case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
    1.11 -          Some(serial)
    1.12 -        case _ => None
    1.13 -      }).map(_.info)
    1.14 +  def breakpoint(range: Text.Range): Option[(Command, Long)] =
    1.15 +    if (snapshot.is_outdated) None
    1.16 +    else
    1.17 +      snapshot.select(range, Rendering.breakpoint_elements, command_states =>
    1.18 +        {
    1.19 +          case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
    1.20 +            command_states match {
    1.21 +              case st :: _ => Some((st.command, serial))
    1.22 +              case _ => None
    1.23 +            }
    1.24 +          case _ => None
    1.25 +        }).headOption.map(_.info)
    1.26  
    1.27  
    1.28    /* command status overview */