src/Pure/PIDE/markup.ML
changeset 58048 aa6296d09e0e
parent 57975 c657c68a60ab
child 58464 5e7fc9974aba
--- a/src/Pure/PIDE/markup.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -72,6 +72,7 @@
   val fixedN: string val fixed: string -> T
   val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
+  val method_modifierN: string
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
@@ -365,7 +366,7 @@
 val (hiddenN, hidden) = markup_elem "hidden";
 
 
-(* formal entities *)
+(* misc entities *)
 
 val system_optionN = "system_option";
 
@@ -378,6 +379,8 @@
 val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 
+val method_modifierN = "method_modifier";
+
 
 (* inner syntax *)