src/Pure/PIDE/markup.scala
changeset 68101 0699a0bacc50
parent 68090 7c8ed28dd40a
child 68148 fb661e4c4717
     1.1 --- a/src/Pure/PIDE/markup.scala	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon May 07 17:11:01 2018 +0200
     1.3 @@ -571,7 +571,8 @@
     1.4    val EXPORT = "export"
     1.5    object Export
     1.6    {
     1.7 -    sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean)
     1.8 +    sealed case class Args(
     1.9 +      id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean)
    1.10  
    1.11      val THEORY_NAME = "theory_name"
    1.12      val COMPRESS = "compress"
    1.13 @@ -579,16 +580,26 @@
    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), (NAME, name), (COMPRESS, Value.Boolean(compress)),
    1.18 -            (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex)))
    1.19 +          List(
    1.20 +            (SERIAL, Value.Long(serial)),
    1.21 +            (THEORY_NAME, theory_name),
    1.22 +            (NAME, name),
    1.23 +            (COMPRESS, Value.Boolean(compress)),
    1.24 +            (EXPORT, hex)) =>
    1.25 +          Some((Args(None, serial, theory_name, name, compress), Bytes.hex(hex)))
    1.26          case _ => None
    1.27        }
    1.28  
    1.29      def unapply(props: Properties.T): Option[Args] =
    1.30        props match {
    1.31 -        case List((FUNCTION, EXPORT), (ID, id),
    1.32 -          (THEORY_NAME, theory_name), (PATH, name), (COMPRESS, Value.Boolean(compress))) =>
    1.33 -            Some(Args(proper_string(id), theory_name, name, compress))
    1.34 +        case List(
    1.35 +            (FUNCTION, EXPORT),
    1.36 +            (ID, id),
    1.37 +            (SERIAL, Value.Long(serial)),
    1.38 +            (THEORY_NAME, theory_name),
    1.39 +            (NAME, name),
    1.40 +            (COMPRESS, Value.Boolean(compress))) =>
    1.41 +          Some(Args(proper_string(id), serial, theory_name, name, compress))
    1.42          case _ => None
    1.43        }
    1.44    }