# HG changeset patch
# User wenzelm
# Date 1281628523 -7200
# Node ID f7d2574dc3a639c2d8ab2b4fe7aeaf8c243297e6
# Parent  fea82d1add7495e1fca6c8b4d2aa056d682ecc74
more basic notion of unparsed input;

diff -r fea82d1add74 -r f7d2574dc3a6 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu Aug 12 17:37:58 2010 +0200
+++ b/src/Pure/General/scan.scala	Thu Aug 12 17:55:23 2010 +0200
@@ -285,8 +285,8 @@
 
       val junk = many1(sym => !(symbols.is_blank(sym)))
       val bad_delimiter =
-        ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.BAD_INPUT, x + y) }
-      val bad = junk ^^ (x => Token(Token.Kind.BAD_INPUT, x))
+        ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.UNPARSED, x + y) }
+      val bad = junk ^^ (x => Token(Token.Kind.UNPARSED, x))
 
 
       /* tokens */
diff -r fea82d1add74 -r f7d2574dc3a6 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Thu Aug 12 17:37:58 2010 +0200
+++ b/src/Pure/Isar/token.scala	Thu Aug 12 17:55:23 2010 +0200
@@ -27,7 +27,6 @@
     val VERBATIM = Value("verbatim text")
     val SPACE = Value("white space")
     val COMMENT = Value("comment text")
-    val BAD_INPUT = Value("bad input")
     val UNPARSED = Value("unparsed input")
   }
 
@@ -79,7 +78,6 @@
   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 content: String =
     if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
diff -r fea82d1add74 -r f7d2574dc3a6 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Aug 12 17:37:58 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Aug 12 17:55:23 2010 +0200
@@ -141,6 +141,12 @@
         case _ => add_result(message)
       }
   }
+
+
+  /* unparsed dummy commands */
+
+  def unparsed(source: String) =
+    new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
 }
 
 
@@ -156,6 +162,8 @@
   def is_ignored: Boolean = span.forall(_.is_ignored)
   def is_malformed: Boolean = !is_command && !is_ignored
 
+  def is_unparsed = id == Document.NO_ID
+
   def name: String = if (is_command) span.head.content else ""
   override def toString =
     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
diff -r fea82d1add74 -r f7d2574dc3a6 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Aug 12 17:37:58 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 12 17:55:23 2010 +0200
@@ -130,14 +130,6 @@
     require(old_doc.assignment.is_finished)
 
 
-    /* unparsed dummy commands */
-
-    def unparsed(source: String) =
-      new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source)))
-
-    def is_unparsed(command: Command) = command.id == NO_ID
-
-
     /* phase 1: edit individual command source */
 
     @tailrec def edit_text(eds: List[Text_Edit],
@@ -152,15 +144,15 @@
           } match {
             case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
               val (rest, text) = e.edit(cmd.source, cmd_start)
-              val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
+              val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
               edit_text(rest.toList ::: es, new_commands)
 
             case Some((cmd, cmd_start)) =>
-              edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
+              edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
 
             case None =>
               require(e.is_insert && e.start == 0)
-              edit_text(es, commands.insert_after(None, unparsed(e.text)))
+              edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
           }
         case Nil => commands
       }
@@ -171,7 +163,7 @@
 
     @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
     {
-      commands.iterator.find(is_unparsed) match {
+      commands.iterator.find(_.is_unparsed) match {
         case Some(first_unparsed) =>
           val first =
             commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head