# HG changeset patch
# User wenzelm
# Date 1281124369 -7200
# Node ID b30aa2dbedca05fbd427d7466a87febc2c17e56d
# Parent  521f10c13e61e27d02ccbc97dbe1a1354d4cd5a8
avoid null in Scala;
tuned comments;

diff -r 521f10c13e61 -r b30aa2dbedca src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Aug 06 14:37:04 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Aug 06 21:52:49 2010 +0200
@@ -37,7 +37,7 @@
 class Command(
     val id: Document.Command_ID,
     val span: Thy_Syntax.Span,
-    val static_parent: Option[Command] = None)
+    val static_parent: Option[Command] = None)  // FIXME !?
   extends Session.Entity
 {
   /* classification */
diff -r 521f10c13e61 -r b30aa2dbedca src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 06 14:37:04 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 06 21:52:49 2010 +0200
@@ -102,9 +102,9 @@
     /* unparsed dummy commands */
 
     def unparsed(source: String) =
-      new Command(null, List(Token(Token.Kind.UNPARSED, source)))
+      new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source)))
 
-    def is_unparsed(command: Command) = command.id == null
+    def is_unparsed(command: Command) = command.id == NO_ID
 
 
     /* phase 1: edit individual command source */
@@ -182,7 +182,7 @@
       for ((name, text_edits) <- edits) {
         val commands0 = nodes(name).commands
         val commands1 = edit_text(text_edits, commands0)
-        val commands2 = parse_spans(commands1)
+        val commands2 = parse_spans(commands1)   // FIXME somewhat slow
 
         val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
         val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList