src/Pure/PIDE/document.scala
changeset 59319 677615cba30d
parent 59077 7e0d3da6e6d8
child 59372 503739360344
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Jan 07 18:09:11 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Jan 08 20:56:39 2015 +0100
     1.3 @@ -113,7 +113,7 @@
     1.4            case _ => false
     1.5          }
     1.6  
     1.7 -      def is_theory: Boolean = !theory.isEmpty
     1.8 +      def is_theory: Boolean = theory.nonEmpty
     1.9        override def toString: String = if (is_theory) theory else node
    1.10  
    1.11        def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
    1.12 @@ -208,7 +208,7 @@
    1.13      final class Commands private(val commands: Linear_Set[Command])
    1.14      {
    1.15        lazy val load_commands: List[Command] =
    1.16 -        commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
    1.17 +        commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
    1.18  
    1.19        private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    1.20        {
    1.21 @@ -229,7 +229,7 @@
    1.22  
    1.23        def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    1.24        {
    1.25 -        if (!commands.isEmpty && full_range.contains(i)) {
    1.26 +        if (commands.nonEmpty && full_range.contains(i)) {
    1.27            val (cmd0, start0) = full_index._1(i / Commands.block_size)
    1.28            Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile {
    1.29              case (cmd, start) => start + cmd.length <= i }
    1.30 @@ -628,7 +628,7 @@
    1.31        history.prune(is_stable, retain) match {
    1.32          case Some((dropped, history1)) =>
    1.33            val old_versions = dropped.map(change => change.version.get_finished)
    1.34 -          val removing = !old_versions.isEmpty
    1.35 +          val removing = old_versions.nonEmpty
    1.36            val state1 = copy(history = history1, removing_versions = removing)
    1.37            (old_versions, state1)
    1.38          case None => fail
    1.39 @@ -750,7 +750,7 @@
    1.40  
    1.41          val state = State.this
    1.42          val version = stable.version.get_finished
    1.43 -        val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.44 +        val is_outdated = pending_edits.nonEmpty || latest != stable
    1.45  
    1.46  
    1.47          /* local node content */
    1.48 @@ -770,7 +770,7 @@
    1.49            if (node_name.is_theory) Nil
    1.50            else version.nodes.load_commands(node_name)
    1.51  
    1.52 -        val is_loaded: Boolean = node_name.is_theory || !load_commands.isEmpty
    1.53 +        val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
    1.54  
    1.55          def eq_content(other: Snapshot): Boolean =
    1.56          {