--- a/src/Pure/PIDE/markup.ML Wed May 22 08:46:39 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Wed May 22 14:10:45 2013 +0200
@@ -142,6 +142,7 @@
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
+ val protocol_handler: string -> Properties.T
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
val ML_statistics: Properties.entry
@@ -461,6 +462,8 @@
val assign_execs = [(functionN, "assign_execs")];
val removed_versions = [(functionN, "removed_versions")];
+fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)];
+
fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];