equal
deleted
inserted
replaced
323 val is_unparsed: Boolean = span.content.exists(_.is_unparsed) |
323 val is_unparsed: Boolean = span.content.exists(_.is_unparsed) |
324 val is_unfinished: Boolean = span.content.exists(_.is_unfinished) |
324 val is_unfinished: Boolean = span.content.exists(_.is_unfinished) |
325 |
325 |
326 def is_command: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span] |
326 def is_command: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span] |
327 def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span |
327 def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span |
328 def is_malformed: Boolean = span.kind == Thy_Syntax.Malformed_Span |
|
329 |
328 |
330 def name: String = |
329 def name: String = |
331 span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" } |
330 span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" } |
332 |
331 |
333 override def toString = |
332 override def toString = id + "/" + span.kind.toString |
334 id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
|
335 |
333 |
336 |
334 |
337 /* blobs */ |
335 /* blobs */ |
338 |
336 |
339 def blobs_names: List[Document.Node.Name] = |
337 def blobs_names: List[Document.Node.Name] = |