src/Pure/PIDE/markup.scala
changeset 72782 98ecb951d911
parent 72781 15a8de807f21
child 72842 6aae62f55c2b
equal deleted inserted replaced
72781:15a8de807f21 72782:98ecb951d911
   377   val STRING = "string"
   377   val STRING = "string"
   378   val ALT_STRING = "alt_string"
   378   val ALT_STRING = "alt_string"
   379   val VERBATIM = "verbatim"
   379   val VERBATIM = "verbatim"
   380   val CARTOUCHE = "cartouche"
   380   val CARTOUCHE = "cartouche"
   381   val COMMENT = "comment"
   381   val COMMENT = "comment"
       
   382 
       
   383   val LOAD_COMMAND = "load_command"
   382 
   384 
   383 
   385 
   384   /* comments */
   386   /* comments */
   385 
   387 
   386   val COMMENT1 = "comment1"
   388   val COMMENT1 = "comment1"