src/Pure/PIDE/protocol.scala
changeset 60882 45bfd18835f1
parent 60879 3dc649cfd512
child 60992 89effcb342df
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Aug 10 20:25:04 2015 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 10 20:42:59 2015 +0200
     1.3 @@ -238,6 +238,18 @@
     1.4      !(is_result(msg) || is_tracing(msg) || is_state(msg))
     1.5  
     1.6  
     1.7 +  /* breakpoints */
     1.8 +
     1.9 +  object ML_Breakpoint
    1.10 +  {
    1.11 +    def unapply(tree: XML.Tree): Option[Long] =
    1.12 +    tree match {
    1.13 +      case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
    1.14 +      case _ => None
    1.15 +    }
    1.16 +  }
    1.17 +
    1.18 +
    1.19    /* dialogs */
    1.20  
    1.21    object Dialog_Args