src/Pure/PIDE/markup.scala
changeset 68148 fb661e4c4717
parent 68101 0699a0bacc50
child 68298 2c3ce27cf4a8
--- a/src/Pure/PIDE/markup.scala	Fri May 11 19:27:00 2018 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri May 11 19:57:49 2018 +0200
@@ -577,7 +577,7 @@
     val THEORY_NAME = "theory_name"
     val COMPRESS = "compress"
 
-    def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
+    def dest_inline(props: Properties.T): Option[(Args, Path)] =
       props match {
         case
           List(
@@ -585,8 +585,8 @@
             (THEORY_NAME, theory_name),
             (NAME, name),
             (COMPRESS, Value.Boolean(compress)),
-            (EXPORT, hex)) =>
-          Some((Args(None, serial, theory_name, name, compress), Bytes.hex(hex)))
+            (FILE, file)) if isabelle.Path.is_valid(file) =>
+          Some((Args(None, serial, theory_name, name, compress), isabelle.Path.explode(file)))
         case _ => None
       }