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) =>