1.1 --- a/src/Pure/General/markup.ML	Tue Jul 05 10:54:05 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Tue Jul 05 11:16:37 2011 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4    val versionN: string
     1.5    val execN: string
     1.6    val assignN: string val assign: int -> T
     1.7 -  val editN: string val edit: int -> int -> T
     1.8 +  val editN: string val edit: int * int -> T
     1.9    val serialN: string
    1.10    val promptN: string val prompt: T
    1.11    val readyN: string val ready: T
    1.12 @@ -123,6 +123,7 @@
    1.13    val output: T -> Output.output * Output.output
    1.14    val enclose: T -> Output.output -> Output.output
    1.15    val markup: T -> string -> string
    1.16 +  val markup_only: T -> string
    1.17  end;
    1.18  
    1.19  structure Markup: MARKUP =
    1.20 @@ -347,7 +348,7 @@
    1.21  val (assignN, assign) = markup_int "assign" versionN;
    1.22  
    1.23  val editN = "edit";
    1.24 -fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
    1.25 +fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
    1.26  
    1.27  
    1.28  (* messages *)
    1.29 @@ -387,4 +388,6 @@
    1.30    let val (bg, en) = output m
    1.31    in Library.enclose (Output.escape bg) (Output.escape en) end;
    1.32  
    1.33 +fun markup_only m = markup m "";
    1.34 +
    1.35  end;