src/Pure/PIDE/markup.scala
changeset 53055 0fe8a9972eda
parent 52877 9a26ec5739dd
child 53378 07990ba8c0ea
equal deleted inserted replaced
53054:8365d7fca3de 53055:0fe8a9972eda
   351         case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
   351         case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
   352         case _ => None
   352         case _ => None
   353       }
   353       }
   354   }
   354   }
   355 
   355 
       
   356   val SLEDGEHAMMER_PROVERS = "sledgehammer_provers"
       
   357   val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS))
       
   358 
   356   object ML_Statistics
   359   object ML_Statistics
   357   {
   360   {
   358     def unapply(props: Properties.T): Option[Properties.T] =
   361     def unapply(props: Properties.T): Option[Properties.T] =
   359       props match {
   362       props match {
   360         case (FUNCTION, "ML_statistics") :: stats => Some(stats)
   363         case (FUNCTION, "ML_statistics") :: stats => Some(stats)