# HG changeset patch # User wenzelm # Date 1585910714 -7200 # Node ID 88dfbc382a3dc37caf857c1f7515e9a03bceee25 # Parent d7fa4daf7ba76c0398b42c5077f3f025290fc751 clarified signature; diff -r d7fa4daf7ba7 -r 88dfbc382a3d src/Pure/PIDE/markup.scala --- 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" diff -r d7fa4daf7ba7 -r 88dfbc382a3d src/Pure/PIDE/protocol.scala --- 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 diff -r d7fa4daf7ba7 -r 88dfbc382a3d src/Pure/PIDE/protocol_handlers.scala --- 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 => diff -r d7fa4daf7ba7 -r 88dfbc382a3d src/Pure/PIDE/session.scala --- 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 { diff -r d7fa4daf7ba7 -r 88dfbc382a3d src/Pure/System/invoke_scala.scala --- 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) } diff -r d7fa4daf7ba7 -r 88dfbc382a3d src/Pure/Tools/build.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 =