clarified signature;

--- 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)];
 
 
 

--- 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
       }
   }

--- 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 {