--- a/src/Pure/PIDE/command.scala Mon Aug 11 22:46:27 2014 +0200
+++ b/src/Pure/PIDE/command.scala Mon Aug 11 22:59:38 2014 +0200
@@ -317,20 +317,20 @@
val init_results: Command.Results,
val init_markup: Markup_Tree)
{
- /* classification */
-
- def is_undefined: Boolean = id == Document_ID.none
- val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
- val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
-
- def is_command: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
- def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
+ /* name and classification */
def name: String =
span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
override def toString = id + "/" + span.kind.toString
+ def is_proper: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
+ def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
+
+ def is_undefined: Boolean = id == Document_ID.none
+ val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
+ val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
+
/* blobs */