src/Pure/General/markup.scala
changeset 29185 26fcfca1db9d
parent 29184 85889d58b5da
child 29195 ea51797fa416
equal deleted inserted replaced
29184:85889d58b5da 29185:26fcfca1db9d
    91   val VERBATIM = "verbatim"
    91   val VERBATIM = "verbatim"
    92   val COMMENT = "comment"
    92   val COMMENT = "comment"
    93   val CONTROL = "control"
    93   val CONTROL = "control"
    94   val MALFORMED = "malformed"
    94   val MALFORMED = "malformed"
    95 
    95 
       
    96   val COMMAND_SPAN = "command_span"
       
    97   val IGNORED_SPAN = "ignored_span"
       
    98   val MALFORMED_SPAN = "malformed_span"
       
    99 
    96 
   100 
    97   /* toplevel */
   101   /* toplevel */
    98 
   102 
    99   val STATE = "state"
   103   val STATE = "state"
   100   val SUBGOAL = "subgoal"
   104   val SUBGOAL = "subgoal"