src/Pure/PIDE/markup.scala
changeset 60830 f56e189350b2
parent 60744 4eba53a0ac3d
child 60831 5b99a334fd4c
equal deleted inserted replaced
60829:4b16b778ce0d 60830:f56e189350b2
   491   }
   491   }
   492 
   492 
   493   val PRINT_OPERATIONS = "print_operations"
   493   val PRINT_OPERATIONS = "print_operations"
   494 
   494 
   495 
   495 
       
   496   /* debugger output */
       
   497 
       
   498   val DEBUGGER_OUTPUT = "debugger_output"
       
   499   object Debugger_Output
       
   500   {
       
   501     def unapply(props: Properties.T): Option[(String, Long)] =
       
   502       props match {
       
   503         case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
       
   504           Some((name, i))
       
   505         case _ => None
       
   506       }
       
   507   }
       
   508 
       
   509 
   496   /* simplifier trace */
   510   /* simplifier trace */
   497 
   511 
   498   val SIMP_TRACE_PANEL = "simp_trace_panel"
   512   val SIMP_TRACE_PANEL = "simp_trace_panel"
   499 
   513 
   500   val SIMP_TRACE_LOG = "simp_trace_log"
   514   val SIMP_TRACE_LOG = "simp_trace_log"