src/Pure/PIDE/markup.ML
changeset 63347 e344dc82f6c2
parent 63337 ae9330fdbc16
child 63474 f66e3c3b0fb1
     1.1 --- a/src/Pure/PIDE/markup.ML	Wed Jun 22 11:10:18 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jun 22 16:04:03 2016 +0200
     1.3 @@ -103,6 +103,7 @@
     1.4    val token_rangeN: string val token_range: T
     1.5    val sortingN: string val sorting: T
     1.6    val typingN: string val typing: T
     1.7 +  val class_parameterN: string val class_parameter: T
     1.8    val ML_keyword1N: string val ML_keyword1: T
     1.9    val ML_keyword2N: string val ML_keyword2: T
    1.10    val ML_keyword3N: string val ML_keyword3: T
    1.11 @@ -468,6 +469,7 @@
    1.12  
    1.13  val (sortingN, sorting) = markup_elem "sorting";
    1.14  val (typingN, typing) = markup_elem "typing";
    1.15 +val (class_parameterN, class_parameter) = markup_elem "class_parameter";
    1.16  
    1.17  
    1.18  (* ML *)