src/Pure/PIDE/markup.scala
changeset 60830 f56e189350b2
parent 60744 4eba53a0ac3d
child 60831 5b99a334fd4c
--- a/src/Pure/PIDE/markup.scala	Wed Jul 29 11:41:26 2015 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Jul 29 13:34:04 2015 +0200
@@ -493,6 +493,20 @@
   val PRINT_OPERATIONS = "print_operations"
 
 
+  /* debugger output */
+
+  val DEBUGGER_OUTPUT = "debugger_output"
+  object Debugger_Output
+  {
+    def unapply(props: Properties.T): Option[(String, Long)] =
+      props match {
+        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
+          Some((name, i))
+        case _ => None
+      }
+  }
+
+
   /* simplifier trace */
 
   val SIMP_TRACE_PANEL = "simp_trace_panel"