src/Pure/General/markup.ML
changeset 45173 b8f8488704e2
parent 44705 fad7758421bf
child 45397 e8a87398f35d
     1.1 --- a/src/Pure/General/markup.ML	Fri Aug 19 13:55:32 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Fri Aug 19 14:01:20 2011 +0200
     1.3 @@ -119,6 +119,7 @@
     1.4    val badN: string val bad: T
     1.5    val functionN: string
     1.6    val invoke_scala: string -> string -> Properties.T
     1.7 +  val cancel_scala: string -> Properties.T
     1.8    val no_output: Output.output * Output.output
     1.9    val default_output: T -> Output.output * Output.output
    1.10    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    1.11 @@ -377,6 +378,7 @@
    1.12  val functionN = "function"
    1.13  
    1.14  fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    1.15 +fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
    1.16  
    1.17  
    1.18