src/Pure/PIDE/markup.scala
changeset 60830 f56e189350b2
parent 60744 4eba53a0ac3d
child 60831 5b99a334fd4c
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Jul 29 11:41:26 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jul 29 13:34:04 2015 +0200
     1.3 @@ -493,6 +493,20 @@
     1.4    val PRINT_OPERATIONS = "print_operations"
     1.5  
     1.6  
     1.7 +  /* debugger output */
     1.8 +
     1.9 +  val DEBUGGER_OUTPUT = "debugger_output"
    1.10 +  object Debugger_Output
    1.11 +  {
    1.12 +    def unapply(props: Properties.T): Option[(String, Long)] =
    1.13 +      props match {
    1.14 +        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
    1.15 +          Some((name, i))
    1.16 +        case _ => None
    1.17 +      }
    1.18 +  }
    1.19 +
    1.20 +
    1.21    /* simplifier trace */
    1.22  
    1.23    val SIMP_TRACE_PANEL = "simp_trace_panel"