src/Pure/PIDE/markup.ML
changeset 74671 df12779c3ce8
parent 74263 be49c660ebbf
child 74673 eae5fa0055bd
--- a/src/Pure/PIDE/markup.ML	Wed Nov 03 12:04:22 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Nov 03 14:26:13 2021 +0100
@@ -85,6 +85,7 @@
   val wordsN: string val words: T
   val hiddenN: string val hidden: T
   val deleteN: string val delete: T
+  val load_commandN: string
   val bash_functionN: string
   val scala_functionN: string
   val system_optionN: string
@@ -476,6 +477,7 @@
 
 (* misc entities *)
 
+val load_commandN = "load_command";
 val bash_functionN = "bash_function";
 val scala_functionN = "scala_function";
 val system_optionN = "system_option";