--- a/src/Pure/PIDE/protocol.scala Mon Mar 30 10:35:10 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Mar 30 11:59:44 2020 +0200
@@ -9,6 +9,19 @@
object Protocol
{
+ /* markers for inlined messages */
+
+ val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
+ val Export_Marker = Protocol_Message.Marker("export")
+ val Meta_Info_Marker = Protocol_Message.Marker("meta_info")
+ val Timing_Marker = Protocol_Message.Marker("Timing")
+ val Command_Timing_Marker = Protocol_Message.Marker("command_timing")
+ val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing")
+ val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics")
+ val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics")
+ val Error_Message_Marker = Protocol_Message.Marker("error_message")
+
+
/* document editing */
object Commands_Accepted
@@ -161,8 +174,6 @@
/* export */
- val Export_Marker = Protocol_Message.Marker(Markup.EXPORT)
-
object Export
{
sealed case class Args(