# HG changeset patch # User wenzelm # Date 1332165571 -3600 # Node ID 0e246130486b00705600db1508d74f094f1045f2 # Parent 1d8601c642cce08a27783450ae8fb09d20da65c4 clarified command span classification: strict Command.is_command, permissive Command.name; diff -r 1d8601c642cc -r 0e246130486b src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sun Mar 18 22:09:00 2012 +0100 +++ b/src/Pure/Isar/token.scala Mon Mar 19 14:59:31 2012 +0100 @@ -81,6 +81,7 @@ def is_space: Boolean = kind == Token.Kind.SPACE def is_comment: Boolean = kind == Token.Kind.COMMENT def is_ignored: Boolean = is_space || is_comment + def is_unparsed: Boolean = kind == Token.Kind.UNPARSED def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin" def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end" diff -r 1d8601c642cc -r 0e246130486b src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sun Mar 18 22:09:00 2012 +0100 +++ b/src/Pure/PIDE/command.scala Mon Mar 19 14:59:31 2012 +0100 @@ -92,9 +92,6 @@ new Command(id, node_name, span.toList, source) } - def apply(node_name: Document.Node.Name, toks: List[Token]): Command = - Command(Document.no_id, node_name, toks) - def unparsed(source: String): Command = Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source))) @@ -131,11 +128,13 @@ def is_defined: Boolean = id != Document.no_id - def is_command: Boolean = !span.isEmpty && span.head.is_command - def is_ignored: Boolean = span.forall(_.is_ignored) - def is_malformed: Boolean = !is_command && !is_ignored + val is_ignored: Boolean = span.forall(_.is_ignored) + val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed)) + def is_command: Boolean = !is_ignored && !is_malformed - def name: String = if (is_command) span.head.content else "" + def name: String = + span.find(_.is_command) match { case Some(tok) => tok.content case _ => "" } + override def toString = id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") diff -r 1d8601c642cc -r 0e246130486b src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sun Mar 18 22:09:00 2012 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Mon Mar 19 14:59:31 2012 +0100 @@ -68,7 +68,7 @@ /* result structure */ val spans = parse_spans(syntax.scan(text)) - spans.foreach(span => add(Command(node_name, span))) + spans.foreach(span => add(Command(Document.no_id, node_name, span))) result() } } @@ -224,12 +224,12 @@ commands: Linear_Set[Command]): Linear_Set[Command] = { commands.iterator.find(cmd => !cmd.is_defined) match { - case Some(first_unparsed) => + case Some(first_undefined) => val first = - commands.reverse_iterator(first_unparsed). + commands.reverse_iterator(first_undefined). dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head val last = - commands.iterator(first_unparsed). + commands.iterator(first_undefined). dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last val range = commands.iterator(first).takeWhile(_ != last).toList ::: List(last)