--- a/src/Pure/PIDE/markup.scala Fri Jul 17 16:03:11 2015 +0200
+++ b/src/Pure/PIDE/markup.scala Fri Jul 17 16:23:25 2015 +0200
@@ -42,6 +42,9 @@
val KIND = "kind"
val Kind = new Properties.String(KIND)
+ val SERIAL = "serial"
+ val Serial = new Properties.Long(SERIAL)
+
val INSTANCE = "instance"
val Instance = new Properties.String(INSTANCE)
@@ -69,6 +72,15 @@
if (markup.name == name) Prop.unapply(markup.properties) else None
}
+ class Markup_Long(val name: String, prop: String)
+ {
+ private val Prop = new Properties.Long(prop)
+
+ def apply(i: Long): Markup = Markup(name, Prop(i))
+ def unapply(markup: Markup): Option[Long] =
+ if (markup.name == name) Prop.unapply(markup.properties) else None
+ }
+
/* formal entities */
@@ -231,7 +243,7 @@
val TEXT_FOLD = "text_fold"
- /* ML syntax */
+ /* ML */
val ML_KEYWORD1 = "ML_keyword1"
val ML_KEYWORD2 = "ML_keyword2"
@@ -251,6 +263,9 @@
val ML_STRUCTURE = "ML_structure"
val ML_TYPING = "ML_typing"
+ val ML_BREAKPOINT = "ML_breakpoint"
+ val ML_Breakpoint = new Markup_Long(ML_BREAKPOINT, SERIAL)
+
/* outer syntax */
@@ -341,9 +356,6 @@
/* messages */
- val SERIAL = "serial"
- val Serial = new Properties.Long(SERIAL)
-
val INIT = "init"
val STATUS = "status"
val REPORT = "report"