--- a/src/Pure/PIDE/markup.ML Wed May 27 20:38:59 2020 +0200
+++ b/src/Pure/PIDE/markup.ML Wed May 27 20:51:25 2020 +0200
@@ -68,8 +68,6 @@
val export_pathN: string val export_path: string -> T
val urlN: string val url: string -> T
val docN: string val doc: string -> T
- val bash_functionN: string val bash_function: string -> T
- val scala_functionN: string val scala_function: string -> T
val markupN: string
val consistentN: string
val unbreakableN: string
@@ -83,6 +81,8 @@
val wordsN: string val words: T
val hiddenN: string val hidden: T
val deleteN: string val delete: T
+ val bash_functionN: string
+ val scala_functionN: string
val system_optionN: string
val sessionN: string
val theoryN: string
@@ -407,8 +407,6 @@
val (export_pathN, export_path) = markup_string "export_path" nameN;
val (urlN, url) = markup_string "url" nameN;
val (docN, doc) = markup_string "doc" nameN;
-val (bash_functionN, bash_function) = markup_string "bash_function" nameN;
-val (scala_functionN, scala_function) = markup_string "scala_function" nameN;
(* pretty printing *)
@@ -450,6 +448,8 @@
(* misc entities *)
+val bash_functionN = "bash_function";
+val scala_functionN = "scala_function";
val system_optionN = "system_option";
val sessionN = "session";