src/Pure/PIDE/markup.scala
changeset 65313 347ed6219dab
parent 65176 908d8be90533
child 65317 b9f5cd845616
     1.1 --- a/src/Pure/PIDE/markup.scala	Sat Mar 18 20:35:58 2017 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Mar 18 20:51:42 2017 +0100
     1.3 @@ -541,15 +541,8 @@
     1.4        }
     1.5    }
     1.6  
     1.7 -  val BUILD_THEORIES_RESULT = "build_theories_result"
     1.8 -  object Build_Theories_Result
     1.9 -  {
    1.10 -    def unapply(props: Properties.T): Option[String] =
    1.11 -      props match {
    1.12 -        case List((FUNCTION, BUILD_THEORIES_RESULT), (ID, id)) => Some(id)
    1.13 -        case _ => None
    1.14 -      }
    1.15 -  }
    1.16 +  val BUILD_SESSION_FINISHED = "build_session_finished"
    1.17 +  val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
    1.18  
    1.19    val PRINT_OPERATIONS = "print_operations"
    1.20