avoid null in Scala;
authorwenzelm
Fri Aug 06 21:52:49 2010 +0200 (2010-08-06)
changeset 38220b30aa2dbedca
parent 38219 521f10c13e61
child 38221 e0f00f0945b4
avoid null in Scala;
tuned comments;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Aug 06 14:37:04 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Aug 06 21:52:49 2010 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  class Command(
     1.5      val id: Document.Command_ID,
     1.6      val span: Thy_Syntax.Span,
     1.7 -    val static_parent: Option[Command] = None)
     1.8 +    val static_parent: Option[Command] = None)  // FIXME !?
     1.9    extends Session.Entity
    1.10  {
    1.11    /* classification */
     2.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 06 14:37:04 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 06 21:52:49 2010 +0200
     2.3 @@ -102,9 +102,9 @@
     2.4      /* unparsed dummy commands */
     2.5  
     2.6      def unparsed(source: String) =
     2.7 -      new Command(null, List(Token(Token.Kind.UNPARSED, source)))
     2.8 +      new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source)))
     2.9  
    2.10 -    def is_unparsed(command: Command) = command.id == null
    2.11 +    def is_unparsed(command: Command) = command.id == NO_ID
    2.12  
    2.13  
    2.14      /* phase 1: edit individual command source */
    2.15 @@ -182,7 +182,7 @@
    2.16        for ((name, text_edits) <- edits) {
    2.17          val commands0 = nodes(name).commands
    2.18          val commands1 = edit_text(text_edits, commands0)
    2.19 -        val commands2 = parse_spans(commands1)
    2.20 +        val commands2 = parse_spans(commands1)   // FIXME somewhat slow
    2.21  
    2.22          val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
    2.23          val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList