diff -r e61b0b819d28 -r c95edf19133b src/Pure/PIDE/markup.ML --- 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";