--- a/src/Pure/PIDE/markup.ML Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Jan 18 17:51:50 2013 +0100
@@ -134,6 +134,7 @@
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
val ML_statistics: Properties.entry
+ val task_statistics: Properties.entry
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
val no_output: Output.output * Output.output
@@ -412,6 +413,8 @@
val ML_statistics = (functionN, "ML_statistics");
+val task_statistics = (functionN, "task_statistics");
+
fun loading_theory name = [("function", "loading_theory"), ("name", name)];
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name