src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Sat Mar 30 20:54:47 2019 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Mar 30 22:51:38 2019 +0100
@@ -200,6 +200,9 @@
   val PATH = "path"
   val Path = new Markup_String(PATH, NAME)
 
+  val EXPORT_PATH = "export_path"
+  val Export_Path = new Markup_String(EXPORT_PATH, NAME)
+
   val URL = "url"
   val Url = new Markup_String(URL, NAME)