src/Pure/PIDE/markup.scala
changeset 68148 fb661e4c4717
parent 68101 0699a0bacc50
child 68298 2c3ce27cf4a8
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri May 11 19:27:00 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri May 11 19:57:49 2018 +0200
     1.3 @@ -577,7 +577,7 @@
     1.4      val THEORY_NAME = "theory_name"
     1.5      val COMPRESS = "compress"
     1.6  
     1.7 -    def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
     1.8 +    def dest_inline(props: Properties.T): Option[(Args, Path)] =
     1.9        props match {
    1.10          case
    1.11            List(
    1.12 @@ -585,8 +585,8 @@
    1.13              (THEORY_NAME, theory_name),
    1.14              (NAME, name),
    1.15              (COMPRESS, Value.Boolean(compress)),
    1.16 -            (EXPORT, hex)) =>
    1.17 -          Some((Args(None, serial, theory_name, name, compress), Bytes.hex(hex)))
    1.18 +            (FILE, file)) if isabelle.Path.is_valid(file) =>
    1.19 +          Some((Args(None, serial, theory_name, name, compress), isabelle.Path.explode(file)))
    1.20          case _ => None
    1.21        }
    1.22