tuned;
authorwenzelm
Thu Jan 08 20:56:39 2015 +0100 (2015-01-08)
changeset 59319677615cba30d
parent 59318 3ef6b0b6232e
child 59320 a375de4dc07a
tuned;
src/Pure/General/completion.scala
src/Pure/General/linear_set.scala
src/Pure/General/path.scala
src/Pure/General/scan.scala
src/Pure/General/word.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/bibtex.scala
src/Pure/Tools/build.scala
src/Tools/Graphview/popups.scala
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/spell_checker.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/General/completion.scala	Wed Jan 07 18:09:11 2015 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Thu Jan 08 20:56:39 2015 +0100
     1.3 @@ -416,7 +416,7 @@
     1.4        }
     1.5  
     1.6      (abbrevs_result orElse words_result) match {
     1.7 -      case Some((original, completions)) if !completions.isEmpty =>
     1.8 +      case Some((original, completions)) if completions.nonEmpty =>
     1.9          val range = Text.Range(- original.length, 0) + caret + start
    1.10          val immediate =
    1.11            explicit ||
     2.1 --- a/src/Pure/General/linear_set.scala	Wed Jan 07 18:09:11 2015 +0100
     2.2 +++ b/src/Pure/General/linear_set.scala	Thu Jan 08 20:56:39 2015 +0100
     2.3 @@ -122,7 +122,7 @@
     2.4    override def size: Int = if (isEmpty) 0 else nexts.size + 1
     2.5  
     2.6    def contains(elem: A): Boolean =
     2.7 -    !isEmpty && (end.get == elem || nexts.isDefinedAt(elem))
     2.8 +    nonEmpty && (end.get == elem || nexts.isDefinedAt(elem))
     2.9  
    2.10    private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] {
    2.11      private var next_elem = from
     3.1 --- a/src/Pure/General/path.scala	Wed Jan 07 18:09:11 2015 +0100
     3.2 +++ b/src/Pure/General/path.scala	Thu Jan 08 20:56:39 2015 +0100
     3.3 @@ -118,7 +118,7 @@
     3.4  final class Path private(private val elems: List[Path.Elem]) // reversed elements
     3.5  {
     3.6    def is_current: Boolean = elems.isEmpty
     3.7 -  def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
     3.8 +  def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
     3.9    def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
    3.10  
    3.11    def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
     4.1 --- a/src/Pure/General/scan.scala	Wed Jan 07 18:09:11 2015 +0100
     4.2 +++ b/src/Pure/General/scan.scala	Thu Jan 08 20:56:39 2015 +0100
     4.3 @@ -330,7 +330,7 @@
     4.4        {
     4.5          if (i < len) {
     4.6            tree.branches.get(str.charAt(i)) match {
     4.7 -            case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
     4.8 +            case Some((s, tr)) => look(tr, s.nonEmpty, i + 1)
     4.9              case None => None
    4.10            }
    4.11          }
     5.1 --- a/src/Pure/General/word.scala	Wed Jan 07 18:09:11 2015 +0100
     5.2 +++ b/src/Pure/General/word.scala	Thu Jan 08 20:56:39 2015 +0100
     5.3 @@ -61,7 +61,7 @@
     5.4          case Capitalized => capitalize(str)
     5.5        }
     5.6      def unapply(str: String): Option[Case] =
     5.7 -      if (!str.isEmpty) {
     5.8 +      if (str.nonEmpty) {
     5.9          if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
    5.10          else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
    5.11          else {
     6.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jan 07 18:09:11 2015 +0100
     6.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Jan 08 20:56:39 2015 +0100
     6.3 @@ -194,7 +194,7 @@
     6.4      def ship(span: List[Token])
     6.5      {
     6.6        val kind =
     6.7 -        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
     6.8 +        if (span.nonEmpty && span.head.is_command && !span.exists(_.is_error)) {
     6.9            val name = span.head.source
    6.10            val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
    6.11            Command_Span.Command_Span(name, pos)
    6.12 @@ -206,8 +206,8 @@
    6.13  
    6.14      def flush()
    6.15      {
    6.16 -      if (!content.isEmpty) { ship(content.toList); content.clear }
    6.17 -      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
    6.18 +      if (content.nonEmpty) { ship(content.toList); content.clear }
    6.19 +      if (improper.nonEmpty) { ship(improper.toList); improper.clear }
    6.20      }
    6.21  
    6.22      for (tok <- toks) {
     7.1 --- a/src/Pure/PIDE/document.scala	Wed Jan 07 18:09:11 2015 +0100
     7.2 +++ b/src/Pure/PIDE/document.scala	Thu Jan 08 20:56:39 2015 +0100
     7.3 @@ -113,7 +113,7 @@
     7.4            case _ => false
     7.5          }
     7.6  
     7.7 -      def is_theory: Boolean = !theory.isEmpty
     7.8 +      def is_theory: Boolean = theory.nonEmpty
     7.9        override def toString: String = if (is_theory) theory else node
    7.10  
    7.11        def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
    7.12 @@ -208,7 +208,7 @@
    7.13      final class Commands private(val commands: Linear_Set[Command])
    7.14      {
    7.15        lazy val load_commands: List[Command] =
    7.16 -        commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
    7.17 +        commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
    7.18  
    7.19        private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    7.20        {
    7.21 @@ -229,7 +229,7 @@
    7.22  
    7.23        def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    7.24        {
    7.25 -        if (!commands.isEmpty && full_range.contains(i)) {
    7.26 +        if (commands.nonEmpty && full_range.contains(i)) {
    7.27            val (cmd0, start0) = full_index._1(i / Commands.block_size)
    7.28            Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile {
    7.29              case (cmd, start) => start + cmd.length <= i }
    7.30 @@ -628,7 +628,7 @@
    7.31        history.prune(is_stable, retain) match {
    7.32          case Some((dropped, history1)) =>
    7.33            val old_versions = dropped.map(change => change.version.get_finished)
    7.34 -          val removing = !old_versions.isEmpty
    7.35 +          val removing = old_versions.nonEmpty
    7.36            val state1 = copy(history = history1, removing_versions = removing)
    7.37            (old_versions, state1)
    7.38          case None => fail
    7.39 @@ -750,7 +750,7 @@
    7.40  
    7.41          val state = State.this
    7.42          val version = stable.version.get_finished
    7.43 -        val is_outdated = !(pending_edits.isEmpty && latest == stable)
    7.44 +        val is_outdated = pending_edits.nonEmpty || latest != stable
    7.45  
    7.46  
    7.47          /* local node content */
    7.48 @@ -770,7 +770,7 @@
    7.49            if (node_name.is_theory) Nil
    7.50            else version.nodes.load_commands(node_name)
    7.51  
    7.52 -        val is_loaded: Boolean = node_name.is_theory || !load_commands.isEmpty
    7.53 +        val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
    7.54  
    7.55          def eq_content(other: Snapshot): Boolean =
    7.56          {
     8.1 --- a/src/Pure/PIDE/session.scala	Wed Jan 07 18:09:11 2015 +0100
     8.2 +++ b/src/Pure/PIDE/session.scala	Thu Jan 08 20:56:39 2015 +0100
     8.3 @@ -131,7 +131,7 @@
     8.4                (a, (msg: Prover.Protocol_Output) => f(prover, msg))
     8.5  
     8.6            val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
     8.7 -          if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
     8.8 +          if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
     8.9  
    8.10            (handlers1 + (name -> new_handler), functions1 ++ new_functions)
    8.11          }
    8.12 @@ -287,7 +287,7 @@
    8.13      private var commands: Set[Command] = Set.empty
    8.14  
    8.15      def flush(): Unit = synchronized {
    8.16 -      if (assignment || !nodes.isEmpty || !commands.isEmpty)
    8.17 +      if (assignment || nodes.nonEmpty || commands.nonEmpty)
    8.18          commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
    8.19        assignment = false
    8.20        nodes = Set.empty
    8.21 @@ -533,7 +533,7 @@
    8.22            case Prune_History =>
    8.23              if (prover.defined) {
    8.24                val old_versions = global_state.change_result(_.remove_versions(prune_size))
    8.25 -              if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
    8.26 +              if (old_versions.nonEmpty) prover.get.remove_versions(old_versions)
    8.27              }
    8.28  
    8.29            case Update_Options(options) =>
    8.30 @@ -603,7 +603,7 @@
    8.31    { manager.send(Cancel_Exec(exec_id)) }
    8.32  
    8.33    def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
    8.34 -  { if (!edits.isEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) }
    8.35 +  { if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) }
    8.36  
    8.37    def update_options(options: Options)
    8.38    { manager.send_wait(Update_Options(options)) }
     9.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Jan 07 18:09:11 2015 +0100
     9.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Jan 08 20:56:39 2015 +0100
     9.3 @@ -79,7 +79,7 @@
     9.4        case (name, Document.Node.Deps(header)) =>
     9.5          val node = nodes(name)
     9.6          val update_header =
     9.7 -          !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
     9.8 +          node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
     9.9          if (update_header) {
    9.10            val node1 = node.update_header(header)
    9.11            if (node.header.imports != node1.header.imports ||
    9.12 @@ -334,7 +334,7 @@
    9.13              val commands = node.commands
    9.14  
    9.15              val node1 =
    9.16 -              if (reparse_set(name) && !commands.isEmpty)
    9.17 +              if (reparse_set(name) && commands.nonEmpty)
    9.18                  node.update_commands(
    9.19                    reparse_spans(resources, syntax, get_blob,
    9.20                      name, commands, commands.head, commands.last))
    9.21 @@ -352,6 +352,6 @@
    9.22          (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
    9.23        }
    9.24  
    9.25 -    Session.Change(previous, syntax_changed, !syntax_changed.isEmpty, doc_edits, version)
    9.26 +    Session.Change(previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, version)
    9.27    }
    9.28  }
    10.1 --- a/src/Pure/Tools/bibtex.scala	Wed Jan 07 18:09:11 2015 +0100
    10.2 +++ b/src/Pure/Tools/bibtex.scala	Thu Jan 08 20:56:39 2015 +0100
    10.3 @@ -155,7 +155,7 @@
    10.4  
    10.5      private val content: Option[List[Token]] =
    10.6        tokens match {
    10.7 -        case Token(Token.Kind.KEYWORD, "@") :: body if !body.isEmpty =>
    10.8 +        case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>
    10.9            (body.init.filterNot(_.is_ignored), body.last) match {
   10.10              case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
   10.11              if tok.is_kind => Some(toks)
    11.1 --- a/src/Pure/Tools/build.scala	Wed Jan 07 18:09:11 2015 +0100
    11.2 +++ b/src/Pure/Tools/build.scala	Thu Jan 08 20:56:39 2015 +0100
    11.3 @@ -166,7 +166,7 @@
    11.4        session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
    11.5      {
    11.6        val bad_sessions = sessions.filterNot(isDefinedAt(_))
    11.7 -      if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    11.8 +      if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    11.9  
   11.10        val pre_selected =
   11.11        {
   11.12 @@ -805,7 +805,7 @@
   11.13        for (name <- full_tree.graph.all_succs(selected)) {
   11.14          val files =
   11.15            List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
   11.16 -        if (!files.isEmpty) progress.echo("Cleaning " + name + " ...")
   11.17 +        if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
   11.18          if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   11.19        }
   11.20      }
   11.21 @@ -944,7 +944,7 @@
   11.22        for ((chapter, entries) <- browser_chapters)
   11.23          Present.update_chapter_index(browser_info, chapter, entries)
   11.24  
   11.25 -      if (!browser_chapters.isEmpty && !(browser_info + Path.explode("index.html")).is_file)
   11.26 +      if (browser_chapters.nonEmpty && !(browser_info + Path.explode("index.html")).is_file)
   11.27        {
   11.28          Isabelle_System.mkdirs(browser_info)
   11.29          File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
    12.1 --- a/src/Tools/Graphview/popups.scala	Wed Jan 07 18:09:11 2015 +0100
    12.2 +++ b/src/Tools/Graphview/popups.scala	Thu Jan 08 20:56:39 2015 +0100
    12.3 @@ -126,7 +126,7 @@
    12.4  
    12.5        popup.add(new JPopupMenu.Separator)
    12.6      }
    12.7 -    if (!selected_nodes.isEmpty) {
    12.8 +    if (selected_nodes.nonEmpty) {
    12.9        val text =
   12.10          if (selected_nodes.length > 1) "multiple"
   12.11          else quote(selected_nodes.head.toString)
    13.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Wed Jan 07 18:09:11 2015 +0100
    13.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Jan 08 20:56:39 2015 +0100
    13.3 @@ -82,7 +82,7 @@
    13.4        original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
    13.5        orig = Library.perhaps_unquote(original)
    13.6        entries = complete(name).filter(_ != orig)
    13.7 -      if !entries.isEmpty
    13.8 +      if entries.nonEmpty
    13.9        items =
   13.10          entries.map({
   13.11            case entry =>
    14.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jan 07 18:09:11 2015 +0100
    14.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Jan 08 20:56:39 2015 +0100
    14.3 @@ -228,7 +228,7 @@
    14.4          r2 = Text.Range(r1.start + 1, r1.stop - 1)
    14.5          if Path.is_valid(s2)
    14.6          paths = complete(s2)
    14.7 -        if !paths.isEmpty
    14.8 +        if paths.nonEmpty
    14.9          items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
   14.10        } yield Completion.Result(r2, s2, false, items)
   14.11      }
   14.12 @@ -630,7 +630,7 @@
   14.13  
   14.14    GUI_Thread.require {}
   14.15  
   14.16 -  require(!items.isEmpty)
   14.17 +  require(items.nonEmpty)
   14.18    val multi = items.length > 1
   14.19  
   14.20  
    15.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Jan 07 18:09:11 2015 +0100
    15.2 +++ b/src/Tools/jEdit/src/document_model.scala	Thu Jan 08 20:56:39 2015 +0100
    15.3 @@ -123,7 +123,7 @@
    15.4            cmd <- snapshot.node.load_commands
    15.5            blob_name <- cmd.blobs_names
    15.6            blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
    15.7 -          if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
    15.8 +          if JEdit_Lib.jedit_text_areas(blob_buffer).nonEmpty
    15.9            start <- snapshot.node.command_start(cmd)
   15.10            range = snapshot.convert(cmd.proper_range + start)
   15.11          } yield range
   15.12 @@ -221,7 +221,7 @@
   15.13      private val pending = new mutable.ListBuffer[Text.Edit]
   15.14      private var last_perspective = Document.Node.no_perspective_text
   15.15  
   15.16 -    def is_pending(): Boolean = pending_clear || !pending.isEmpty
   15.17 +    def is_pending(): Boolean = pending_clear || pending.nonEmpty
   15.18      def snapshot(): List[Text.Edit] = pending.toList
   15.19  
   15.20      def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   15.21 @@ -229,7 +229,7 @@
   15.22        val clear = pending_clear
   15.23        val edits = snapshot()
   15.24        val (reparse, perspective) = node_perspective(doc_blobs)
   15.25 -      if (clear || reparse || !edits.isEmpty || last_perspective != perspective) {
   15.26 +      if (clear || reparse || edits.nonEmpty || last_perspective != perspective) {
   15.27          pending_clear = false
   15.28          pending.clear
   15.29          last_perspective = perspective
    16.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Wed Jan 07 18:09:11 2015 +0100
    16.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 08 20:56:39 2015 +0100
    16.3 @@ -58,7 +58,7 @@
    16.4        if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
    16.5      } yield PIDE.options.make_color_component(opt))
    16.6  
    16.7 -  assert(!predefined.isEmpty)
    16.8 +  assert(predefined.nonEmpty)
    16.9  
   16.10    protected val components = PIDE.options.make_components(predefined, _ => false)
   16.11  }
    17.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 07 18:09:11 2015 +0100
    17.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Jan 08 20:56:39 2015 +0100
    17.3 @@ -41,7 +41,7 @@
    17.4          name => (name, Document.Node.no_perspective_text))
    17.5  
    17.6      val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
    17.7 -    if (!edits.isEmpty) session.update(doc_blobs, edits)
    17.8 +    if (edits.nonEmpty) session.update(doc_blobs, edits)
    17.9    }
   17.10  
   17.11    private val delay_flush =
    18.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Jan 07 18:09:11 2015 +0100
    18.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Jan 08 20:56:39 2015 +0100
    18.3 @@ -114,7 +114,7 @@
    18.4  
    18.5    override def commit(change: Session.Change)
    18.6    {
    18.7 -    if (!change.syntax_changed.isEmpty)
    18.8 +    if (change.syntax_changed.nonEmpty)
    18.9        GUI_Thread.later {
   18.10          val changed = change.syntax_changed.toSet
   18.11          for {
    19.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Jan 07 18:09:11 2015 +0100
    19.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Jan 08 20:56:39 2015 +0100
    19.3 @@ -220,7 +220,7 @@
    19.4              val files = thy_info.dependencies("", thys).deps.map(_.name.node).
    19.5                filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
    19.6  
    19.7 -            if (!files.isEmpty) {
    19.8 +            if (files.nonEmpty) {
    19.9                if (PIDE.options.bool("jedit_auto_load")) {
   19.10                  files.foreach(file => jEdit.openFile(null: View, file))
   19.11                }
    20.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Jan 07 18:09:11 2015 +0100
    20.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Jan 08 20:56:39 2015 +0100
    20.3 @@ -465,7 +465,7 @@
    20.4          range, Nil, Rendering.tooltip_message_elements, _ =>
    20.5          {
    20.6            case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    20.7 -          if !body.isEmpty =>
    20.8 +          if body.nonEmpty =>
    20.9              val entry: Command.Results.Entry = (Document_ID.make(), msg)
   20.10              Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   20.11  
   20.12 @@ -665,7 +665,7 @@
   20.13              command_states =>
   20.14                {
   20.15                  case (((status, color), Text.Info(_, XML.Elem(markup, _))))
   20.16 -                if !status.isEmpty && Protocol.proper_status_elements(markup.name) =>
   20.17 +                if status.nonEmpty && Protocol.proper_status_elements(markup.name) =>
   20.18                    Some((markup :: status, color))
   20.19                  case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   20.20                    Some((Nil, Some(bad_color)))
   20.21 @@ -686,7 +686,7 @@
   20.22                })
   20.23          color <-
   20.24            (result match {
   20.25 -            case (markups, opt_color) if !markups.isEmpty =>
   20.26 +            case (markups, opt_color) if markups.nonEmpty =>
   20.27                val status = Protocol.Status.make(markups.iterator)
   20.28                if (status.is_unprocessed) Some(unprocessed1_color)
   20.29                else if (status.is_running) Some(running1_color)
    21.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Jan 07 18:09:11 2015 +0100
    21.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Jan 08 20:56:39 2015 +0100
    21.3 @@ -408,7 +408,7 @@
    21.4                val s2 = str.substring(i, j)
    21.5                val s3 = str.substring(j)
    21.6  
    21.7 -              if (!s1.isEmpty) gfx.drawString(s1, x1, y)
    21.8 +              if (s1.nonEmpty) gfx.drawString(s1, x1, y)
    21.9  
   21.10                val astr = new AttributedString(s2)
   21.11                astr.addAttribute(TextAttribute.FONT, chunk_font)
   21.12 @@ -416,7 +416,7 @@
   21.13                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
   21.14                gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
   21.15  
   21.16 -              if (!s3.isEmpty)
   21.17 +              if (s3.nonEmpty)
   21.18                  gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
   21.19  
   21.20              case _ =>
    22.1 --- a/src/Tools/jEdit/src/spell_checker.scala	Wed Jan 07 18:09:11 2015 +0100
    22.2 +++ b/src/Tools/jEdit/src/spell_checker.scala	Thu Jan 08 20:56:39 2015 +0100
    22.3 @@ -84,7 +84,7 @@
    22.4        range = JEdit_Lib.before_caret_range(text_area, rendering)
    22.5        word <- current_word(text_area, rendering, range)
    22.6        words = spell_checker.complete(word.info)
    22.7 -      if !words.isEmpty
    22.8 +      if words.nonEmpty
    22.9        descr = "(from dictionary " + quote(spell_checker.toString) + ")"
   22.10        items =
   22.11          words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
   22.12 @@ -274,7 +274,7 @@
   22.13          if upd.permanent
   22.14        } yield Spell_Checker.Decl(word, upd.include)).toList
   22.15  
   22.16 -    if (!permanent_decls.isEmpty || dictionary.user_path.is_file) {
   22.17 +    if (permanent_decls.nonEmpty || dictionary.user_path.is_file) {
   22.18        val header = """# User updates for spell-checker dictionary
   22.19  #
   22.20  #   * each line contains at most one word
   22.21 @@ -358,7 +358,7 @@
   22.22        result.getOrElse(Nil).map(recover_case)
   22.23      }
   22.24  
   22.25 -  def complete_enabled(word: String): Boolean = !complete(word).isEmpty
   22.26 +  def complete_enabled(word: String): Boolean = complete(word).nonEmpty
   22.27  }
   22.28  
   22.29  
    23.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Jan 07 18:09:11 2015 +0100
    23.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Jan 08 20:56:39 2015 +0100
    23.3 @@ -161,7 +161,7 @@
    23.4      val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)
    23.5  
    23.6      val theories =
    23.7 -      (for ((node_name, node_timing) <- nodes_timing.toList if !node_timing.commands.isEmpty)
    23.8 +      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty)
    23.9          yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
   23.10      val commands =
   23.11        (for ((command, command_timing) <- timing.commands.toList)