src/Pure/PIDE/markup.scala
changeset 68088 0763d4eb3ebc
parent 67870 586be47e00b3
child 68090 7c8ed28dd40a
     1.1 --- a/src/Pure/PIDE/markup.scala	Sat May 05 21:44:18 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat May 05 22:33:35 2018 +0200
     1.3 @@ -568,6 +568,32 @@
     1.4        }
     1.5    }
     1.6  
     1.7 +  val EXPORT = "export"
     1.8 +  object Export
     1.9 +  {
    1.10 +    sealed case class Args(id: Option[String], theory_name: String, path: String, compress: Boolean)
    1.11 +
    1.12 +    val THEORY_NAME = "theory_name"
    1.13 +    val PATH = "path"
    1.14 +    val COMPRESS = "compress"
    1.15 +
    1.16 +    def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
    1.17 +      props match {
    1.18 +        case
    1.19 +          List((THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress)),
    1.20 +            (EXPORT, hex)) => Some((Args(None, theory_name, path, 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 +        case _ => None
    1.30 +      }
    1.31 +  }
    1.32 +
    1.33    val BUILD_SESSION_FINISHED = "build_session_finished"
    1.34    val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
    1.35