--- 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 ||
--- 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
--- 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))
--- 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
}
}
--- 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 {
--- 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) {
--- 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 =
{
--- 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)) }
--- 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)
}
}
--- 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)
--- 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"),
--- 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)
--- 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 =>
--- 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
--- 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
--- 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)
}
--- 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 =
--- 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 {
--- 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))
}
--- 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)
--- 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 _ =>
--- 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
}
--- 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)