--- a/src/Pure/PIDE/markup.scala Fri Apr 03 11:47:08 2020 +0200
+++ b/src/Pure/PIDE/markup.scala Fri Apr 03 12:45:14 2020 +0200
@@ -549,79 +549,65 @@
/* protocol message functions */
val FUNCTION = "function"
- val Function = new Properties.String(FUNCTION)
- val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
- val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
+ class Function(val name: String)
+ {
+ val PROPERTY: Properties.Entry = (FUNCTION, name)
+ }
- val Commands_Accepted: Properties.T = List((FUNCTION, "commands_accepted"))
- val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
- val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
-
- object Protocol_Handler
+ class Properties_Function(name: String) extends Function(name)
{
- def unapply(props: Properties.T): Option[(String)] =
+ def unapply(props: Properties.T): Option[Properties.T] =
props match {
- case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
+ case PROPERTY :: args => Some(args)
case _ => None
}
}
- val INVOKE_SCALA = "invoke_scala"
- object Invoke_Scala
+ class Name_Function(name: String) extends Function(name)
{
- def unapply(props: Properties.T): Option[(String, String)] =
+ def unapply(props: Properties.T): Option[(String)] =
props match {
- case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
+ case List(PROPERTY, (NAME, a)) => Some(a)
case _ => None
}
}
- val CANCEL_SCALA = "cancel_scala"
- object Cancel_Scala
+ object Command_Timing extends Properties_Function("command_timing")
+ object Theory_Timing extends Properties_Function("theory_timing")
+ object ML_Statistics extends Properties_Function("ML_statistics")
+ object Task_Statistics extends Properties_Function("task_statistics")
+
+ object Loading_Theory extends Name_Function("loading_theory")
+ object Build_Session_Finished extends Function("build_session_finished")
+
+ object Protocol_Handler extends Name_Function("protocol_handler")
+
+ object Commands_Accepted extends Function("commands_accepted")
+ object Assign_Update extends Function("assign_update")
+ object Removed_Versions extends Function("removed_versions")
+
+ object Invoke_Scala extends Function("invoke_scala")
{
- def unapply(props: Properties.T): Option[String] =
+ def unapply(props: Properties.T): Option[(String, String)] =
props match {
- case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
- case _ => None
- }
- }
-
- object ML_Statistics
- {
- def unapply(props: Properties.T): Option[Properties.T] =
- props match {
- case (FUNCTION, "ML_statistics") :: props => Some(props)
+ case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
case _ => None
}
}
- object Task_Statistics
+ object Cancel_Scala extends Function("cancel_scala")
{
- def unapply(props: Properties.T): Option[Properties.T] =
+ def unapply(props: Properties.T): Option[String] =
props match {
- case (FUNCTION, "task_statistics") :: props => Some(props)
+ case List(PROPERTY, (ID, id)) => Some(id)
case _ => None
}
}
- val LOADING_THEORY = "loading_theory"
- object Loading_Theory
- {
- def unapply(props: Properties.T): Option[String] =
- props match {
- case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name)
- case _ => None
- }
- }
-
- val BUILD_SESSION_FINISHED = "build_session_finished"
- val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
-
val PRINT_OPERATIONS = "print_operations"
-
/* export */
val EXPORT = "export"
--- a/src/Pure/PIDE/protocol.scala Fri Apr 03 11:47:08 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Apr 03 12:45:14 2020 +0200
@@ -72,11 +72,11 @@
object Command_Timing
{
- def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
+ def unapply(props: Properties.T): Option[(Properties.T, Document_ID.Generic, isabelle.Timing)] =
props match {
- case Markup.COMMAND_TIMING :: args =>
+ case Markup.Command_Timing(args) =>
(args, args) match {
- case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
+ case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((args, id, timing))
case _ => None
}
case _ => None
@@ -90,7 +90,7 @@
{
def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
props match {
- case Markup.THEORY_TIMING :: args =>
+ case Markup.Theory_Timing(args) =>
(args, args) match {
case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
case _ => None
--- a/src/Pure/PIDE/protocol_handlers.scala Fri Apr 03 11:47:08 2020 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala Fri Apr 03 12:45:14 2020 +0200
@@ -58,7 +58,7 @@
def invoke(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
- case Markup.Function(a) if functions.isDefinedAt(a) =>
+ case (Markup.FUNCTION, a) :: _ if functions.isDefinedAt(a) =>
try { functions(a)(msg) }
catch {
case exn: Throwable =>
--- a/src/Pure/PIDE/session.scala Fri Apr 03 11:47:08 2020 +0200
+++ b/src/Pure/PIDE/session.scala Fri Apr 03 12:45:14 2020 +0200
@@ -485,13 +485,13 @@
case Markup.Protocol_Handler(name) if prover.defined =>
init_protocol_handler(name)
- case Protocol.Command_Timing(state_id, timing) if prover.defined =>
- command_timings.post(Session.Command_Timing(msg.properties.tail))
+ case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
+ command_timings.post(Session.Command_Timing(props))
val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
- case Protocol.Theory_Timing(_, _) =>
- theory_timings.post(Session.Theory_Timing(msg.properties.tail))
+ case Markup.Theory_Timing(props) =>
+ theory_timings.post(Session.Theory_Timing(props))
case Markup.ML_Statistics(props) =>
runtime_statistics.post(Session.Runtime_Statistics(props))
@@ -505,7 +505,7 @@
val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
change_command(_.add_export(id, (args.serial, export)))
- case Markup.Commands_Accepted =>
+ case List(Markup.Commands_Accepted.PROPERTY) =>
msg.text match {
case Protocol.Commands_Accepted(ids) =>
ids.foreach(id =>
@@ -513,7 +513,7 @@
case _ => bad_output()
}
- case Markup.Assign_Update =>
+ case List(Markup.Assign_Update.PROPERTY) =>
msg.text match {
case Protocol.Assign_Update(id, edited, update) =>
try {
@@ -527,7 +527,7 @@
}
delay_prune.invoke()
- case Markup.Removed_Versions =>
+ case List(Markup.Removed_Versions.PROPERTY) =>
msg.text match {
case Protocol.Removed(removed) =>
try {
--- a/src/Pure/System/invoke_scala.scala Fri Apr 03 11:47:08 2020 +0200
+++ b/src/Pure/System/invoke_scala.scala Fri Apr 03 12:45:14 2020 +0200
@@ -123,6 +123,6 @@
val functions =
List(
- Markup.INVOKE_SCALA -> invoke_scala,
- Markup.CANCEL_SCALA -> cancel_scala)
+ Markup.Invoke_Scala.name -> invoke_scala,
+ Markup.Cancel_Scala.name -> cancel_scala)
}
--- a/src/Pure/Tools/build.scala Fri Apr 03 11:47:08 2020 +0200
+++ b/src/Pure/Tools/build.scala Fri Apr 03 12:45:14 2020 +0200
@@ -257,8 +257,8 @@
val functions =
List(
- Markup.BUILD_SESSION_FINISHED -> build_session_finished,
- Markup.LOADING_THEORY -> loading_theory)
+ Markup.Build_Session_Finished.name -> build_session_finished,
+ Markup.Loading_Theory.name -> loading_theory)
})
val session_consumer =