src/Pure/PIDE/session.scala
changeset 68088 0763d4eb3ebc
parent 67825 f9c071cc958b
child 68101 0699a0bacc50
--- a/src/Pure/PIDE/session.scala	Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/PIDE/session.scala	Sat May 05 22:33:35 2018 +0200
@@ -435,6 +435,9 @@
               case Protocol.Theory_Timing(_, _) =>
                 // FIXME
 
+              case Markup.Export(_) =>
+                // FIXME
+
               case Markup.Assign_Update =>
                 msg.text match {
                   case Protocol.Assign_Update(id, update) =>