src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Sun May 06 19:10:21 2018 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun May 06 22:15:52 2018 +0200
@@ -571,25 +571,24 @@
   val EXPORT = "export"
   object Export
   {
-    sealed case class Args(id: Option[String], theory_name: String, path: String, compress: Boolean)
+    sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean)
 
     val THEORY_NAME = "theory_name"
-    val PATH = "path"
     val COMPRESS = "compress"
 
     def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
       props match {
         case
-          List((THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress)),
-            (EXPORT, hex)) => Some((Args(None, theory_name, path, compress), Bytes.hex(hex)))
+          List((THEORY_NAME, theory_name), (NAME, name), (COMPRESS, Value.Boolean(compress)),
+            (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex)))
         case _ => None
       }
 
     def unapply(props: Properties.T): Option[Args] =
       props match {
         case List((FUNCTION, EXPORT), (ID, id),
-          (THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress))) =>
-            Some(Args(proper_string(id), theory_name, path, compress))
+          (THEORY_NAME, theory_name), (PATH, name), (COMPRESS, Value.Boolean(compress))) =>
+            Some(Args(proper_string(id), theory_name, name, compress))
         case _ => None
       }
   }