src/Pure/PIDE/document.scala

         that match {
           case other: Name => node == other.node
           case _ => false
         }
 
-      def is_theory: Boolean = !theory.isEmpty
+      def is_theory: Boolean = theory.nonEmpty
       override def toString: String = if (is_theory) theory else node
 
       def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
     }
 

     }
 
     final class Commands private(val commands: Linear_Set[Command])
     {
       lazy val load_commands: List[Command] =
-        commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
+        commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
 
       private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
       {
         val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
         var next_block = 0

 
       private def full_range: Text.Range = full_index._2
 
       def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       {
-        if (!commands.isEmpty && full_range.contains(i)) {
+        if (commands.nonEmpty && full_range.contains(i)) {
           val (cmd0, start0) = full_index._1(i / Commands.block_size)
           Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile {
             case (cmd, start) => start + cmd.length <= i }
         }
         else Iterator.empty

     def remove_versions(retain: Int = 0): (List[Version], State) =
     {
       history.prune(is_stable, retain) match {
         case Some((dropped, history1)) =>
           val old_versions = dropped.map(change => change.version.get_finished)
-          val removing = !old_versions.isEmpty
+          val removing = old_versions.nonEmpty
           val state1 = copy(history = history1, removing_versions = removing)
           (old_versions, state1)
         case None => fail
       }
     }

       {
         /* global information */
 
         val state = State.this
         val version = stable.version.get_finished
-        val is_outdated = !(pending_edits.isEmpty && latest == stable)
+        val is_outdated = pending_edits.nonEmpty || latest != stable
 
 
         /* local node content */
 
         def convert(offset: Text.Offset) =

 
         val load_commands: List[Command] =
           if (node_name.is_theory) Nil
           else version.nodes.load_commands(node_name)
 
-        val is_loaded: Boolean = node_name.is_theory || !load_commands.isEmpty
+        val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
 
         def eq_content(other: Snapshot): Boolean =
         {
           def eq_commands(commands: (Command, Command)): Boolean =
           {