src/Pure/PIDE/markup.ML
changeset 69650 c95edf19133b
parent 69648 97ddaec3e2ae
child 69788 c175499a7537
--- a/src/Pure/PIDE/markup.ML	Sun Jan 13 20:25:41 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Jan 14 13:58:12 2019 +0100
@@ -60,7 +60,6 @@
   val pathN: string val path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
-  val theory_exportsN: string val theory_exports: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
@@ -193,6 +192,7 @@
   val intensifyN: string val intensify: T
   val browserN: string
   val graphviewN: string
+  val theory_exportsN: string
   val sendbackN: string
   val paddingN: string
   val padding_line: Properties.entry
@@ -374,7 +374,6 @@
 val (pathN, path) = markup_string "path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
-val (theory_exportsN, theory_exports) = markup_string "theory_exports" nameN;
 
 
 (* pretty printing *)
@@ -631,6 +630,7 @@
 
 val browserN = "browser"
 val graphviewN = "graphview";
+val theory_exportsN = "theory_exports";
 
 val sendbackN = "sendback";
 val paddingN = "padding";