src/Pure/General/markup.ML

--- a/src/Pure/General/markup.ML	Tue Jul 05 10:54:05 2011 +0200
+++ b/src/Pure/General/markup.ML	Tue Jul 05 11:16:37 2011 +0200
@@ -110,7 +110,7 @@
   val versionN: string
   val execN: string
   val assignN: string val assign: int -> T
-  val editN: string val edit: int -> int -> T
+  val editN: string val edit: int * int -> T
   val serialN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
@@ -123,6 +123,7 @@
   val output: T -> Output.output * Output.output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
+  val markup_only: T -> string
 end;
 
 structure Markup: MARKUP =
@@ -347,7 +348,7 @@
 val (assignN, assign) = markup_int "assign" versionN;
 
 val editN = "edit";
-fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
+fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
 
 
 (* messages *)
@@ -387,4 +388,6 @@
   let val (bg, en) = output m
   in Library.enclose (Output.escape bg) (Output.escape en) end;
 
+fun markup_only m = markup m "";
+
 end;