src/Pure/PIDE/markup.ML
changeset 52111 1fd184eaa310
parent 51990 cc66addbba6d
child 52563 f9a20c2c3b70
     1.1 --- a/src/Pure/PIDE/markup.ML	Wed May 22 08:46:39 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Wed May 22 14:10:45 2013 +0200
     1.3 @@ -142,6 +142,7 @@
     1.4    val functionN: string
     1.5    val assign_execs: Properties.T
     1.6    val removed_versions: Properties.T
     1.7 +  val protocol_handler: string -> Properties.T
     1.8    val invoke_scala: string -> string -> Properties.T
     1.9    val cancel_scala: string -> Properties.T
    1.10    val ML_statistics: Properties.entry
    1.11 @@ -461,6 +462,8 @@
    1.12  val assign_execs = [(functionN, "assign_execs")];
    1.13  val removed_versions = [(functionN, "removed_versions")];
    1.14  
    1.15 +fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)];
    1.16 +
    1.17  fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    1.18  fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
    1.19