src/Pure/PIDE/markup.scala
changeset 63474 f66e3c3b0fb1
parent 63347 e344dc82f6c2
child 63475 31016a88197b
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Jul 13 14:28:15 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jul 13 15:19:16 2016 +0200
     1.3 @@ -372,7 +372,17 @@
     1.4    val COMMAND_TIMING = "command_timing"
     1.5  
     1.6  
     1.7 -  /* toplevel */
     1.8 +  /* command indentation */
     1.9 +
    1.10 +  object Command_Indent
    1.11 +  {
    1.12 +    val name = "command_indent"
    1.13 +    def unapply(markup: Markup): Option[Int] =
    1.14 +      if (markup.name == name) Indent.unapply(markup.properties) else None
    1.15 +  }
    1.16 +
    1.17 +
    1.18 +  /* goals */
    1.19  
    1.20    val SUBGOALS = "subgoals"
    1.21    val PROOF_STATE = "proof_state"