--- a/src/Pure/PIDE/markup.ML Fri Jan 11 22:38:12 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Jan 12 14:47:17 2013 +0100
@@ -125,14 +125,14 @@
val graphviewN: string
val sendbackN: string
val paddingN: string
- val padding_line: string * string
+ val padding_line: Properties.entry
val dialogN: string val dialog: serial -> string -> T
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
- val ML_statistics: string * string
+ val ML_statistics: Properties.entry
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit