# HG changeset patch # User wenzelm # Date 1667210694 -3600 # Node ID 9d3b9e89455f937f311a0acfae21d7ebf10f4135 # Parent f227ff7bff500b9f19a7bf3251ce1a2184cd42dc clarified signature; diff -r f227ff7bff50 -r 9d3b9e89455f src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Oct 29 21:36:33 2022 +0200 +++ b/src/Pure/PIDE/markup.ML Mon Oct 31 11:04:54 2022 +0100 @@ -237,7 +237,7 @@ val padding_command: Properties.entry val dialogN: string val dialog: serial -> string -> T val jedit_actionN: string - val functionN: string + val function: string -> Properties.entry val ML_statistics: {pid: int, stats_dir: string} -> Properties.T val commands_accepted: Properties.T val assign_update: Properties.T @@ -750,33 +750,33 @@ (* protocol message functions *) -val functionN = "function" +fun function name = ("function", name); fun ML_statistics {pid, stats_dir} = - [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)]; + [function "ML_statistics", ("pid", Value.print_int pid), ("stats_dir", stats_dir)]; -val commands_accepted = [(functionN, "commands_accepted")]; +val commands_accepted = [function "commands_accepted"]; -val assign_update = [(functionN, "assign_update")]; -val removed_versions = [(functionN, "removed_versions")]; +val assign_update = [function "assign_update"]; +val removed_versions = [function "removed_versions"]; -fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; +fun invoke_scala name id = [function "invoke_scala", (nameN, name), (idN, id)]; -fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; +fun cancel_scala id = [function "cancel_scala", (idN, id)]; -val task_statistics = (functionN, "task_statistics"); +val task_statistics = function "task_statistics"; -val command_timing = (functionN, "command_timing"); +val command_timing = function "command_timing"; -val theory_timing = (functionN, "theory_timing"); +val theory_timing = function "theory_timing"; -val session_timing = (functionN, "session_timing"); +val session_timing = function "session_timing"; -fun loading_theory name = [(functionN, "loading_theory"), (nameN, name)]; +fun loading_theory name = [function "loading_theory", (nameN, name)]; -val build_session_finished = [(functionN, "build_session_finished")]; +val build_session_finished = [function "build_session_finished"]; -val print_operations = [(functionN, "print_operations")]; +val print_operations = [function "print_operations"]; (* export *) @@ -793,7 +793,7 @@ strict: bool}; fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) = - [(functionN, exportN), + [function exportN, (idN, the_default "" id), (serialN, Value.print_int serial), ("theory_name", theory_name), @@ -805,8 +805,8 @@ (* debugger *) -fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)]; -fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)]; +fun debugger_state name = [function "debugger_state", (nameN, name)]; +fun debugger_output name = [function "debugger_output", (nameN, name)]; (* simplifier trace *) @@ -819,7 +819,7 @@ val simp_trace_hintN = "simp_trace_hint"; val simp_trace_ignoreN = "simp_trace_ignore"; -fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)]; +fun simp_trace_cancel i = [function "simp_trace_cancel", (serialN, Value.print_int i)]; diff -r f227ff7bff50 -r 9d3b9e89455f src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Oct 29 21:36:33 2022 +0200 +++ b/src/Pure/PIDE/markup.scala Mon Oct 31 11:04:54 2022 +0100 @@ -612,13 +612,13 @@ val FUNCTION = "function" class Function(val name: String) { - val PROPERTY: Properties.Entry = (FUNCTION, name) + val THIS: Properties.Entry = (FUNCTION, name) } class Properties_Function(name: String) extends Function(name) { def unapply(props: Properties.T): Option[Properties.T] = props match { - case PROPERTY :: args => Some(args) + case THIS :: args => Some(args) case _ => None } } @@ -626,7 +626,7 @@ class Name_Function(name: String) extends Function(name) { def unapply(props: Properties.T): Option[String] = props match { - case List(PROPERTY, (NAME, a)) => Some(a) + case List(THIS, (NAME, a)) => Some(a) case _ => None } } @@ -634,7 +634,7 @@ object ML_Statistics extends Function("ML_statistics") { def unapply(props: Properties.T): Option[(Long, String)] = props match { - case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) => + case List(THIS, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) => Some((pid, stats_dir)) case _ => None } @@ -660,7 +660,7 @@ object Invoke_Scala extends Function("invoke_scala") { def unapply(props: Properties.T): Option[(String, String)] = props match { - case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id)) + case List(THIS, (NAME, name), (ID, id)) => Some((name, id)) case _ => None } } @@ -668,7 +668,7 @@ object Cancel_Scala extends Function("cancel_scala") { def unapply(props: Properties.T): Option[String] = props match { - case List(PROPERTY, (ID, id)) => Some(id) + case List(THIS, (ID, id)) => Some(id) case _ => None } } diff -r f227ff7bff50 -r 9d3b9e89455f src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Oct 29 21:36:33 2022 +0200 +++ b/src/Pure/PIDE/session.scala Mon Oct 31 11:04:54 2022 +0100 @@ -487,7 +487,7 @@ try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) } catch { case _: Document.State.Fail => bad_output() } - case List(Markup.Commands_Accepted.PROPERTY) => + case List(Markup.Commands_Accepted.THIS) => msg.text match { case Protocol.Commands_Accepted(ids) => ids.foreach(id => @@ -495,7 +495,7 @@ case _ => bad_output() } - case List(Markup.Assign_Update.PROPERTY) => + case List(Markup.Assign_Update.THIS) => msg.text match { case Protocol.Assign_Update(id, edited, update) => try { @@ -509,7 +509,7 @@ } delay_prune.invoke() - case List(Markup.Removed_Versions.PROPERTY) => + case List(Markup.Removed_Versions.THIS) => msg.text match { case Protocol.Removed(removed) => try {