src/Pure/PIDE/markup.scala
changeset 68090 7c8ed28dd40a
parent 68088 0763d4eb3ebc
child 68101 0699a0bacc50
     1.1 --- a/src/Pure/PIDE/markup.scala	Sun May 06 19:10:21 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sun May 06 22:15:52 2018 +0200
     1.3 @@ -571,25 +571,24 @@
     1.4    val EXPORT = "export"
     1.5    object Export
     1.6    {
     1.7 -    sealed case class Args(id: Option[String], theory_name: String, path: String, compress: Boolean)
     1.8 +    sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean)
     1.9  
    1.10      val THEORY_NAME = "theory_name"
    1.11 -    val PATH = "path"
    1.12      val COMPRESS = "compress"
    1.13  
    1.14      def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
    1.15        props match {
    1.16          case
    1.17 -          List((THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress)),
    1.18 -            (EXPORT, hex)) => Some((Args(None, theory_name, path, compress), Bytes.hex(hex)))
    1.19 +          List((THEORY_NAME, theory_name), (NAME, name), (COMPRESS, Value.Boolean(compress)),
    1.20 +            (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex)))
    1.21          case _ => None
    1.22        }
    1.23  
    1.24      def unapply(props: Properties.T): Option[Args] =
    1.25        props match {
    1.26          case List((FUNCTION, EXPORT), (ID, id),
    1.27 -          (THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress))) =>
    1.28 -            Some(Args(proper_string(id), theory_name, path, compress))
    1.29 +          (THEORY_NAME, theory_name), (PATH, name), (COMPRESS, Value.Boolean(compress))) =>
    1.30 +            Some(Args(proper_string(id), theory_name, name, compress))
    1.31          case _ => None
    1.32        }
    1.33    }