# HG changeset patch # User wenzelm # Date 1420746999 -3600 # Node ID 677615cba30dcbd2339bc245b2a2b7d8f2874386 # Parent 3ef6b0b6232edcde9240bcf7abc7588b07641a2c tuned; diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/General/completion.scala Thu Jan 08 20:56:39 2015 +0100 @@ -416,7 +416,7 @@ } (abbrevs_result orElse words_result) match { - case Some((original, completions)) if !completions.isEmpty => + case Some((original, completions)) if completions.nonEmpty => val range = Text.Range(- original.length, 0) + caret + start val immediate = explicit || diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/General/linear_set.scala Thu Jan 08 20:56:39 2015 +0100 @@ -122,7 +122,7 @@ override def size: Int = if (isEmpty) 0 else nexts.size + 1 def contains(elem: A): Boolean = - !isEmpty && (end.get == elem || nexts.isDefinedAt(elem)) + nonEmpty && (end.get == elem || nexts.isDefinedAt(elem)) private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] { private var next_elem = from diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/General/path.scala --- a/src/Pure/General/path.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/General/path.scala Thu Jan 08 20:56:39 2015 +0100 @@ -118,7 +118,7 @@ final class Path private(private val elems: List[Path.Elem]) // reversed elements { def is_current: Boolean = elems.isEmpty - def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root] + def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root] def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false } def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem)) diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/General/scan.scala Thu Jan 08 20:56:39 2015 +0100 @@ -330,7 +330,7 @@ { if (i < len) { tree.branches.get(str.charAt(i)) match { - case Some((s, tr)) => look(tr, !s.isEmpty, i + 1) + case Some((s, tr)) => look(tr, s.nonEmpty, i + 1) case None => None } } diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/General/word.scala --- a/src/Pure/General/word.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/General/word.scala Thu Jan 08 20:56:39 2015 +0100 @@ -61,7 +61,7 @@ case Capitalized => capitalize(str) } def unapply(str: String): Option[Case] = - if (!str.isEmpty) { + if (str.nonEmpty) { if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase) else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase) else { diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Thu Jan 08 20:56:39 2015 +0100 @@ -194,7 +194,7 @@ def ship(span: List[Token]) { val kind = - if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) { + if (span.nonEmpty && span.head.is_command && !span.exists(_.is_error)) { val name = span.head.source val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1) Command_Span.Command_Span(name, pos) @@ -206,8 +206,8 @@ def flush() { - if (!content.isEmpty) { ship(content.toList); content.clear } - if (!improper.isEmpty) { ship(improper.toList); improper.clear } + if (content.nonEmpty) { ship(content.toList); content.clear } + if (improper.nonEmpty) { ship(improper.toList); improper.clear } } for (tok <- toks) { diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/PIDE/document.scala Thu Jan 08 20:56:39 2015 +0100 @@ -113,7 +113,7 @@ 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) @@ -208,7 +208,7 @@ 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) = { @@ -229,7 +229,7 @@ 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 } @@ -628,7 +628,7 @@ 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 @@ -750,7 +750,7 @@ 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 */ @@ -770,7 +770,7 @@ 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 = { diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/PIDE/session.scala Thu Jan 08 20:56:39 2015 +0100 @@ -131,7 +131,7 @@ (a, (msg: Prover.Protocol_Output) => f(prover, msg)) val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a - if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) + if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) (handlers1 + (name -> new_handler), functions1 ++ new_functions) } @@ -287,7 +287,7 @@ private var commands: Set[Command] = Set.empty def flush(): Unit = synchronized { - if (assignment || !nodes.isEmpty || !commands.isEmpty) + if (assignment || nodes.nonEmpty || commands.nonEmpty) commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) assignment = false nodes = Set.empty @@ -533,7 +533,7 @@ case Prune_History => if (prover.defined) { val old_versions = global_state.change_result(_.remove_versions(prune_size)) - if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) + if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) } case Update_Options(options) => @@ -603,7 +603,7 @@ { manager.send(Cancel_Exec(exec_id)) } def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) - { if (!edits.isEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) } + { if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) } def update_options(options: Options) { manager.send_wait(Update_Options(options)) } diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Thu Jan 08 20:56:39 2015 +0100 @@ -79,7 +79,7 @@ case (name, Document.Node.Deps(header)) => val node = nodes(name) val update_header = - !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header + node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header if (update_header) { val node1 = node.update_header(header) if (node.header.imports != node1.header.imports || @@ -334,7 +334,7 @@ val commands = node.commands val node1 = - if (reparse_set(name) && !commands.isEmpty) + if (reparse_set(name) && commands.nonEmpty) node.update_commands( reparse_spans(resources, syntax, get_blob, name, commands, commands.head, commands.last)) @@ -352,6 +352,6 @@ (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes)) } - Session.Change(previous, syntax_changed, !syntax_changed.isEmpty, doc_edits, version) + Session.Change(previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, version) } } diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/Tools/bibtex.scala --- a/src/Pure/Tools/bibtex.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/Tools/bibtex.scala Thu Jan 08 20:56:39 2015 +0100 @@ -155,7 +155,7 @@ private val content: Option[List[Token]] = tokens match { - case Token(Token.Kind.KEYWORD, "@") :: body if !body.isEmpty => + case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty => (body.init.filterNot(_.is_ignored), body.last) match { case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}")) if tok.is_kind => Some(toks) diff -r 3ef6b0b6232e -r 677615cba30d src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/Tools/build.scala Thu Jan 08 20:56:39 2015 +0100 @@ -166,7 +166,7 @@ session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) = { val bad_sessions = sessions.filterNot(isDefinedAt(_)) - if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions)) + if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions)) val pre_selected = { @@ -805,7 +805,7 @@ for (name <- full_tree.graph.all_succs(selected)) { val files = List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file) - if (!files.isEmpty) progress.echo("Cleaning " + name + " ...") + if (files.nonEmpty) progress.echo("Cleaning " + name + " ...") if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete") } } @@ -944,7 +944,7 @@ for ((chapter, entries) <- browser_chapters) Present.update_chapter_index(browser_info, chapter, entries) - if (!browser_chapters.isEmpty && !(browser_info + Path.explode("index.html")).is_file) + if (browser_chapters.nonEmpty && !(browser_info + Path.explode("index.html")).is_file) { Isabelle_System.mkdirs(browser_info) File.copy(Path.explode("~~/lib/logo/isabelle.gif"), diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/Graphview/popups.scala --- a/src/Tools/Graphview/popups.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/Graphview/popups.scala Thu Jan 08 20:56:39 2015 +0100 @@ -126,7 +126,7 @@ popup.add(new JPopupMenu.Separator) } - if (!selected_nodes.isEmpty) { + if (selected_nodes.nonEmpty) { val text = if (selected_nodes.length > 1) "multiple" else quote(selected_nodes.head.toString) diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/bibtex_jedit.scala --- a/src/Tools/jEdit/src/bibtex_jedit.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala Thu Jan 08 20:56:39 2015 +0100 @@ -82,7 +82,7 @@ original <- JEdit_Lib.try_get_text(text_area.getBuffer, r) orig = Library.perhaps_unquote(original) entries = complete(name).filter(_ != orig) - if !entries.isEmpty + if entries.nonEmpty items = entries.map({ case entry => diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Thu Jan 08 20:56:39 2015 +0100 @@ -228,7 +228,7 @@ r2 = Text.Range(r1.start + 1, r1.stop - 1) if Path.is_valid(s2) paths = complete(s2) - if !paths.isEmpty + if paths.nonEmpty items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false)) } yield Completion.Result(r2, s2, false, items) } @@ -630,7 +630,7 @@ GUI_Thread.require {} - require(!items.isEmpty) + require(items.nonEmpty) val multi = items.length > 1 diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Thu Jan 08 20:56:39 2015 +0100 @@ -123,7 +123,7 @@ cmd <- snapshot.node.load_commands blob_name <- cmd.blobs_names blob_buffer <- JEdit_Lib.jedit_buffer(blob_name) - if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty + if JEdit_Lib.jedit_text_areas(blob_buffer).nonEmpty start <- snapshot.node.command_start(cmd) range = snapshot.convert(cmd.proper_range + start) } yield range @@ -221,7 +221,7 @@ private val pending = new mutable.ListBuffer[Text.Edit] private var last_perspective = Document.Node.no_perspective_text - def is_pending(): Boolean = pending_clear || !pending.isEmpty + def is_pending(): Boolean = pending_clear || pending.nonEmpty def snapshot(): List[Text.Edit] = pending.toList def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] = @@ -229,7 +229,7 @@ val clear = pending_clear val edits = snapshot() val (reparse, perspective) = node_perspective(doc_blobs) - if (clear || reparse || !edits.isEmpty || last_perspective != perspective) { + if (clear || reparse || edits.nonEmpty || last_perspective != perspective) { pending_clear = false pending.clear last_perspective = perspective diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/isabelle_options.scala Thu Jan 08 20:56:39 2015 +0100 @@ -58,7 +58,7 @@ if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION) } yield PIDE.options.make_color_component(opt)) - assert(!predefined.isEmpty) + assert(predefined.nonEmpty) protected val components = PIDE.options.make_components(predefined, _ => false) } diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Jan 08 20:56:39 2015 +0100 @@ -41,7 +41,7 @@ name => (name, Document.Node.no_perspective_text)) val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective - if (!edits.isEmpty) session.update(doc_blobs, edits) + if (edits.nonEmpty) session.update(doc_blobs, edits) } private val delay_flush = diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Jan 08 20:56:39 2015 +0100 @@ -114,7 +114,7 @@ override def commit(change: Session.Change) { - if (!change.syntax_changed.isEmpty) + if (change.syntax_changed.nonEmpty) GUI_Thread.later { val changed = change.syntax_changed.toSet for { diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Thu Jan 08 20:56:39 2015 +0100 @@ -220,7 +220,7 @@ val files = thy_info.dependencies("", thys).deps.map(_.name.node). filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file)) - if (!files.isEmpty) { + if (files.nonEmpty) { if (PIDE.options.bool("jedit_auto_load")) { files.foreach(file => jEdit.openFile(null: View, file)) } diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Thu Jan 08 20:56:39 2015 +0100 @@ -465,7 +465,7 @@ range, Nil, Rendering.tooltip_message_elements, _ => { case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body))) - if !body.isEmpty => + if body.nonEmpty => val entry: Command.Results.Entry = (Document_ID.make(), msg) Some(Text.Info(snapshot.convert(info_range), entry) :: msgs) @@ -665,7 +665,7 @@ command_states => { case (((status, color), Text.Info(_, XML.Elem(markup, _)))) - if !status.isEmpty && Protocol.proper_status_elements(markup.name) => + if status.nonEmpty && Protocol.proper_status_elements(markup.name) => Some((markup :: status, color)) case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => Some((Nil, Some(bad_color))) @@ -686,7 +686,7 @@ }) color <- (result match { - case (markups, opt_color) if !markups.isEmpty => + case (markups, opt_color) if markups.nonEmpty => val status = Protocol.Status.make(markups.iterator) if (status.is_unprocessed) Some(unprocessed1_color) else if (status.is_running) Some(running1_color) diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Jan 08 20:56:39 2015 +0100 @@ -408,7 +408,7 @@ val s2 = str.substring(i, j) val s3 = str.substring(j) - if (!s1.isEmpty) gfx.drawString(s1, x1, y) + if (s1.nonEmpty) gfx.drawString(s1, x1, y) val astr = new AttributedString(s2) astr.addAttribute(TextAttribute.FONT, chunk_font) @@ -416,7 +416,7 @@ astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) gfx.drawString(astr.getIterator, x1 + string_width(s1), y) - if (!s3.isEmpty) + if (s3.nonEmpty) gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y) case _ => diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/spell_checker.scala --- a/src/Tools/jEdit/src/spell_checker.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/spell_checker.scala Thu Jan 08 20:56:39 2015 +0100 @@ -84,7 +84,7 @@ range = JEdit_Lib.before_caret_range(text_area, rendering) word <- current_word(text_area, rendering, range) words = spell_checker.complete(word.info) - if !words.isEmpty + if words.nonEmpty descr = "(from dictionary " + quote(spell_checker.toString) + ")" items = words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false)) @@ -274,7 +274,7 @@ if upd.permanent } yield Spell_Checker.Decl(word, upd.include)).toList - if (!permanent_decls.isEmpty || dictionary.user_path.is_file) { + if (permanent_decls.nonEmpty || dictionary.user_path.is_file) { val header = """# User updates for spell-checker dictionary # # * each line contains at most one word @@ -358,7 +358,7 @@ result.getOrElse(Nil).map(recover_case) } - def complete_enabled(word: String): Boolean = !complete(word).isEmpty + def complete_enabled(word: String): Boolean = complete(word).nonEmpty } diff -r 3ef6b0b6232e -r 677615cba30d src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Jan 08 20:56:39 2015 +0100 @@ -161,7 +161,7 @@ val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing) val theories = - (for ((node_name, node_timing) <- nodes_timing.toList if !node_timing.commands.isEmpty) + (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty) yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering) val commands = (for ((command, command_timing) <- timing.commands.toList)