src/Pure/PIDE/markup.ML
changeset 63347 e344dc82f6c2
parent 63337 ae9330fdbc16
child 63474 f66e3c3b0fb1
equal deleted inserted replaced
63346:c8366fb67538 63347:e344dc82f6c2
   101   val inner_cartoucheN: string val inner_cartouche: T
   101   val inner_cartoucheN: string val inner_cartouche: T
   102   val inner_commentN: string val inner_comment: T
   102   val inner_commentN: string val inner_comment: T
   103   val token_rangeN: string val token_range: T
   103   val token_rangeN: string val token_range: T
   104   val sortingN: string val sorting: T
   104   val sortingN: string val sorting: T
   105   val typingN: string val typing: T
   105   val typingN: string val typing: T
       
   106   val class_parameterN: string val class_parameter: T
   106   val ML_keyword1N: string val ML_keyword1: T
   107   val ML_keyword1N: string val ML_keyword1: T
   107   val ML_keyword2N: string val ML_keyword2: T
   108   val ML_keyword2N: string val ML_keyword2: T
   108   val ML_keyword3N: string val ML_keyword3: T
   109   val ML_keyword3N: string val ML_keyword3: T
   109   val ML_delimiterN: string val ML_delimiter: T
   110   val ML_delimiterN: string val ML_delimiter: T
   110   val ML_tvarN: string val ML_tvar: T
   111   val ML_tvarN: string val ML_tvar: T
   466 
   467 
   467 val (token_rangeN, token_range) = markup_elem "token_range";
   468 val (token_rangeN, token_range) = markup_elem "token_range";
   468 
   469 
   469 val (sortingN, sorting) = markup_elem "sorting";
   470 val (sortingN, sorting) = markup_elem "sorting";
   470 val (typingN, typing) = markup_elem "typing";
   471 val (typingN, typing) = markup_elem "typing";
       
   472 val (class_parameterN, class_parameter) = markup_elem "class_parameter";
   471 
   473 
   472 
   474 
   473 (* ML *)
   475 (* ML *)
   474 
   476 
   475 val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
   477 val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";