1.1 --- a/src/Pure/PIDE/markup.scala	Fri Jul 17 16:03:11 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri Jul 17 16:23:25 2015 +0200
     1.3 @@ -42,6 +42,9 @@
     1.4    val KIND = "kind"
     1.5    val Kind = new Properties.String(KIND)
     1.6  
     1.7 +  val SERIAL = "serial"
     1.8 +  val Serial = new Properties.Long(SERIAL)
     1.9 +
    1.10    val INSTANCE = "instance"
    1.11    val Instance = new Properties.String(INSTANCE)
    1.12  
    1.13 @@ -69,6 +72,15 @@
    1.14        if (markup.name == name) Prop.unapply(markup.properties) else None
    1.15    }
    1.16  
    1.17 +  class Markup_Long(val name: String, prop: String)
    1.18 +  {
    1.19 +    private val Prop = new Properties.Long(prop)
    1.20 +
    1.21 +    def apply(i: Long): Markup = Markup(name, Prop(i))
    1.22 +    def unapply(markup: Markup): Option[Long] =
    1.23 +      if (markup.name == name) Prop.unapply(markup.properties) else None
    1.24 +  }
    1.25 +
    1.26  
    1.27    /* formal entities */
    1.28  
    1.29 @@ -231,7 +243,7 @@
    1.30    val TEXT_FOLD = "text_fold"
    1.31  
    1.32  
    1.33 -  /* ML syntax */
    1.34 +  /* ML */
    1.35  
    1.36    val ML_KEYWORD1 = "ML_keyword1"
    1.37    val ML_KEYWORD2 = "ML_keyword2"
    1.38 @@ -251,6 +263,9 @@
    1.39    val ML_STRUCTURE = "ML_structure"
    1.40    val ML_TYPING = "ML_typing"
    1.41  
    1.42 +  val ML_BREAKPOINT = "ML_breakpoint"
    1.43 +  val ML_Breakpoint = new Markup_Long(ML_BREAKPOINT, SERIAL)
    1.44 +
    1.45  
    1.46    /* outer syntax */
    1.47  
    1.48 @@ -341,9 +356,6 @@
    1.49  
    1.50    /* messages */
    1.51  
    1.52 -  val SERIAL = "serial"
    1.53 -  val Serial = new Properties.Long(SERIAL)
    1.54 -
    1.55    val INIT = "init"
    1.56    val STATUS = "status"
    1.57    val REPORT = "report"