src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Wed Jul 13 14:28:15 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Jul 13 15:19:16 2016 +0200
@@ -372,7 +372,17 @@
   val COMMAND_TIMING = "command_timing"
 
 
-  /* toplevel */
+  /* command indentation */
+
+  object Command_Indent
+  {
+    val name = "command_indent"
+    def unapply(markup: Markup): Option[Int] =
+      if (markup.name == name) Indent.unapply(markup.properties) else None
+  }
+
+
+  /* goals */
 
   val SUBGOALS = "subgoals"
   val PROOF_STATE = "proof_state"