more informative errors: simplify diagnosis of spurious failures reported by users;
--- a/src/Pure/Admin/build_cygwin.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Admin/build_cygwin.scala Sun Jan 10 13:04:29 2021 +0100
@@ -18,7 +18,7 @@
mirror: String = default_mirror,
more_packages: List[String] = Nil)
{
- require(Platform.is_windows)
+ require(Platform.is_windows, "Windows platform expected")
Isabelle_System.with_tmp_dir("cygwin")(tmp_dir =>
{
--- a/src/Pure/Admin/build_status.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Admin/build_status.scala Sun Jan 10 13:04:29 2021 +0100
@@ -83,7 +83,7 @@
name: String, threads: Int, entries: List[Entry],
ml_statistics: ML_Statistics, ml_statistics_date: Long)
{
- require(entries.nonEmpty)
+ require(entries.nonEmpty, "no entries")
lazy val sorted_entries: List[Entry] = entries.sortBy(entry => - entry.date)
--- a/src/Pure/Concurrent/counter.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Concurrent/counter.scala Sun Jan 10 13:04:29 2021 +0100
@@ -20,7 +20,7 @@
private var count: Counter.ID = 0
def apply(): Counter.ID = synchronized {
- require(count > java.lang.Long.MIN_VALUE)
+ require(count > java.lang.Long.MIN_VALUE, "counter overflow")
count -= 1
count
}
--- a/src/Pure/Concurrent/future.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Concurrent/future.scala Sun Jan 10 13:04:29 2021 +0100
@@ -34,7 +34,7 @@
{
def peek: Option[Exn.Result[A]]
def is_finished: Boolean = peek.isDefined
- def get_finished: A = { require(is_finished); Exn.release(peek.get) }
+ def get_finished: A = { require(is_finished, "future not finished"); Exn.release(peek.get) }
def join_result: Exn.Result[A]
def join: A = Exn.release(join_result)
def map[B](f: A => B): Future[B] = Future.fork { f(join) }
--- a/src/Pure/Concurrent/isabelle_thread.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala Sun Jan 10 13:04:29 2021 +0100
@@ -179,7 +179,7 @@
def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A =
if (new_handler == null) body
else {
- require(is_self)
+ require(is_self, "interrupt handler on other thread")
val old_handler = handler
handler = new_handler
--- a/src/Pure/GUI/gui_thread.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/GUI/gui_thread.scala Sun Jan 10 13:04:29 2021 +0100
@@ -22,7 +22,7 @@
def require[A](body: => A): A =
{
- Predef.require(SwingUtilities.isEventDispatchThread)
+ Predef.require(SwingUtilities.isEventDispatchThread, "GUI thread expected")
body
}
--- a/src/Pure/General/date.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/General/date.scala Sun Jan 10 13:04:29 2021 +0100
@@ -23,7 +23,7 @@
{
def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
{
- require(fmts.nonEmpty)
+ require(fmts.nonEmpty, "no date formats")
new Format {
def apply(date: Date): String = fmts.head.format(date.rep)
--- a/src/Pure/General/scan.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/General/scan.scala Sun Jan 10 13:04:29 2021 +0100
@@ -107,7 +107,7 @@
def quoted_content(quote: Symbol.Symbol, source: String): String =
{
- require(parseAll(quoted(quote), source).successful)
+ require(parseAll(quoted(quote), source).successful, "no quoted text")
val body = source.substring(1, source.length - 1)
if (body.exists(_ == '\\')) {
val content =
@@ -149,7 +149,7 @@
def verbatim_content(source: String): String =
{
- require(parseAll(verbatim, source).successful)
+ require(parseAll(verbatim, source).successful, "no verbatim text")
source.substring(2, source.length - 2)
}
@@ -176,7 +176,7 @@
def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
{
- require(depth >= 0)
+ require(depth >= 0, "bad cartouche depth")
def apply(in: Input) =
{
@@ -235,7 +235,7 @@
private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
{
- require(depth >= 0)
+ require(depth >= 0, "bad comment depth")
val comment_text: Parser[List[String]] =
rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
@@ -286,7 +286,7 @@
def comment_content(source: String): String =
{
- require(parseAll(comment, source).successful)
+ require(parseAll(comment, source).successful, "no comment")
source.substring(2, source.length - 2)
}
--- a/src/Pure/General/symbol.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/General/symbol.scala Sun Jan 10 13:04:29 2021 +0100
@@ -30,7 +30,7 @@
def spaces(n: Int): String =
{
- require(n >= 0)
+ require(n >= 0, "negative spaces")
if (n < static_spaces.length) static_spaces.substring(0, n)
else space * n
}
@@ -96,7 +96,7 @@
private val matcher = symbol_total.pattern.matcher(text)
def apply(start: Int, end: Int): Int =
{
- require(0 <= start && start < end && end <= text.length)
+ require(0 <= start && start < end && end <= text.length, "bad matcher range")
if (is_plain(text.charAt(start))) 1
else {
matcher.region(start, end).lookingAt
--- a/src/Pure/General/utf8.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/General/utf8.scala Sun Jan 10 13:04:29 2021 +0100
@@ -84,7 +84,7 @@
def decode_chars(decode: String => String,
buffer: Array[Byte], start: Int, end: Int): CharSequence =
{
- require(0 <= start && start <= end && end <= buffer.length)
+ require(0 <= start && start <= end && end <= buffer.length, "bad decode range")
new Decode_Chars(decode, buffer, start, end)
}
}
--- a/src/Pure/Isar/outer_syntax.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Sun Jan 10 13:04:29 2021 +0100
@@ -147,7 +147,7 @@
def no_tokens: Outer_Syntax =
{
- require(keywords.is_empty)
+ require(keywords.is_empty, "bad syntax keywords")
new Outer_Syntax(
rev_abbrevs = rev_abbrevs,
language_context = language_context,
--- a/src/Pure/ML/ml_statistics.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala Sun Jan 10 13:04:29 2021 +0100
@@ -201,7 +201,7 @@
def apply(ml_statistics0: List[Properties.T], heading: String = "",
domain: String => Boolean = (key: String) => true): ML_Statistics =
{
- require(ml_statistics0.forall(props => Now.unapply(props).isDefined))
+ require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
val ml_statistics = ml_statistics0.sortBy(now)
val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
--- a/src/Pure/PIDE/command.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/PIDE/command.scala Sun Jan 10 13:04:29 2021 +0100
@@ -424,8 +424,8 @@
{
val cmds1 = this.commands
val cmds2 = that.commands
- require(!cmds1.exists(_.is_undefined))
- require(!cmds2.exists(_.is_undefined))
+ require(!cmds1.exists(_.is_undefined), "cmds1 not defined")
+ require(!cmds2.exists(_.is_undefined), "cmds2 not defined")
cmds1.length == cmds2.length &&
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
}
--- a/src/Pure/PIDE/document.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/PIDE/document.scala Sun Jan 10 13:04:29 2021 +0100
@@ -835,12 +835,12 @@
{
override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")"
- def check_finished: Assignment = { require(is_finished); this }
+ def check_finished: Assignment = { require(is_finished, "assignment not finished"); this }
def unfinished: Assignment = new Assignment(command_execs, false)
def assign(update: Assign_Update): Assignment =
{
- require(!is_finished)
+ require(!is_finished, "assignment already finished")
val command_execs1 =
(command_execs /: update) {
case (res, (command_id, exec_ids)) =>
@@ -1120,7 +1120,7 @@
def command_id_map(version: Version, commands: Iterable[Command])
: Map[Document_ID.Generic, Command] =
{
- require(is_assigned(version))
+ require(is_assigned(version), "version not assigned (command_id_map)")
val assignment = the_assignment(version).check_finished
(for {
command <- commands.iterator
@@ -1130,7 +1130,7 @@
def command_maybe_consolidated(version: Version, command: Command): Boolean =
{
- require(is_assigned(version))
+ require(is_assigned(version), "version not assigned (command_maybe_consolidated)")
try {
the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
case eval_id :: print_ids =>
@@ -1145,7 +1145,7 @@
private def command_states_self(version: Version, command: Command)
: List[(Document_ID.Generic, Command.State)] =
{
- require(is_assigned(version))
+ require(is_assigned(version), "version not assigned (command_states_self)")
try {
the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
.map(id => id -> the_dynamic_state(id)) match {
--- a/src/Pure/PIDE/headless.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/PIDE/headless.scala Sun Jan 10 13:04:29 2021 +0100
@@ -517,7 +517,7 @@
def remove_theories(remove: List[Document.Node.Name]): State =
{
- require(remove.forall(name => !is_required(name)))
+ require(remove.forall(name => !is_required(name)), "attempt to remove required nodes")
copy(theories = theories -- remove)
}
--- a/src/Pure/PIDE/line.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/PIDE/line.scala Sun Jan 10 13:04:29 2021 +0100
@@ -147,7 +147,7 @@
@tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
{
lines_rest match {
- case Nil => require(i == 0); Position(lines_count)
+ case Nil => require(i == 0, "bad Line.position.move"); Position(lines_count)
case line :: ls =>
val n = line.text.length
if (ls.isEmpty || i <= n)
@@ -241,7 +241,7 @@
final class Line private(val text: String)
{
- require(text.forall(c => c != '\r' && c != '\n'))
+ require(text.forall(c => c != '\r' && c != '\n'), "bad line text")
override def equals(that: Any): Boolean =
that match {
--- a/src/Pure/PIDE/markup_tree.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Sun Jan 10 13:04:29 2021 +0100
@@ -31,7 +31,7 @@
case (branches, tree) =>
(branches /: tree.branches) {
case (bs, (r, entry)) =>
- require(!bs.isDefinedAt(r))
+ require(!bs.isDefinedAt(r), "cannot merge markup trees")
bs + (r -> entry)
}
})
--- a/src/Pure/PIDE/session.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/PIDE/session.scala Sun Jan 10 13:04:29 2021 +0100
@@ -164,7 +164,7 @@
def require_dispatcher[A](body: => A): A =
{
- require(dispatcher.check_thread)
+ require(dispatcher.check_thread, "not on dispatcher thread")
body
}
@@ -404,7 +404,7 @@
consolidate: List[Document.Node.Name] = Nil)
//{{{
{
- require(prover.defined)
+ require(prover.defined, "prover process not defined (handle_raw_edits)")
if (edits.nonEmpty) prover.get.discontinue_execution()
@@ -423,7 +423,7 @@
def handle_change(change: Session.Change)
//{{{
{
- require(prover.defined)
+ require(prover.defined, "prover process not defined (handle_change)")
// define commands
{
--- a/src/Pure/System/cygwin.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/System/cygwin.scala Sun Jan 10 13:04:29 2021 +0100
@@ -19,7 +19,7 @@
def init(isabelle_root: String, cygwin_root: String)
{
- require(Platform.is_windows)
+ require(Platform.is_windows, "Windows platform expected")
def exec(cmdline: String*)
{
--- a/src/Pure/System/linux.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/System/linux.scala Sun Jan 10 13:04:29 2021 +0100
@@ -97,7 +97,7 @@
system: Boolean = false,
ssh_setup: Boolean = false)
{
- require(!description.contains(','))
+ require(!description.contains(','), "malformed description")
if (user_exists(name)) error("User already exists: " + quote(name))
@@ -153,7 +153,7 @@
def generate_password(length: Int = 10): String =
{
- require(length >= 6)
+ require(length >= 6, "password too short")
Isabelle_System.bash("pwgen " + length + " 1").check.out
}
}
--- a/src/Pure/Thy/bibtex.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Thy/bibtex.scala Sun Jan 10 13:04:29 2021 +0100
@@ -445,7 +445,8 @@
private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
new Parser[(String, Delimited)]
{
- require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0)
+ require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0,
+ "bad delimiter depth")
def apply(in: Input) =
{
--- a/src/Pure/Thy/presentation.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Sun Jan 10 13:04:29 2021 +0100
@@ -148,7 +148,7 @@
elements: Elements,
plain_text: Boolean = false): HTML_Document =
{
- require(!snapshot.is_outdated)
+ require(!snapshot.is_outdated, "document snapshot outdated")
val name = snapshot.node_name
if (plain_text) {
--- a/src/Pure/Thy/thy_syntax.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Sun Jan 10 13:04:29 2021 +0100
@@ -140,7 +140,7 @@
edit_text(es, insert_text(Some(cmd), e.text))
case None =>
- require(e.is_insert && e.start == 0)
+ require(e.is_insert && e.start == 0, "bad text edit")
edit_text(es, insert_text(None, e.text))
}
case Nil => commands
--- a/src/Pure/Tools/phabricator.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/Tools/phabricator.scala Sun Jan 10 13:04:29 2021 +0100
@@ -927,7 +927,7 @@
{
/* connection */
- require(ssh_host.nonEmpty && ssh_port >= 0)
+ require(ssh_host.nonEmpty && ssh_port >= 0, "bad ssh host or port")
private def ssh_user_prefix: String = SSH.user_prefix(ssh_user)
private def ssh_port_suffix: String = SSH.port_suffix(ssh_port)
@@ -1060,7 +1060,7 @@
public: Boolean = false,
vcs: API.VCS.Value = API.VCS.hg): API.Repository =
{
- require(name.nonEmpty)
+ require(name.nonEmpty, "bad repository name")
val transactions =
API.edits("vcs", vcs.toString) :::
--- a/src/Pure/library.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/library.scala Sun Jan 10 13:04:29 2021 +0100
@@ -168,7 +168,7 @@
class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
{
- require(0 <= start && start <= end && end <= text.length)
+ require(0 <= start && start <= end && end <= text.length, "bad reverse range")
def this(text: CharSequence) = this(text, 0, text.length)
--- a/src/Tools/VSCode/src/lsp.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Tools/VSCode/src/lsp.scala Sun Jan 10 13:04:29 2021 +0100
@@ -71,7 +71,7 @@
id.isInstanceOf[Int] ||
id.isInstanceOf[Long] ||
id.isInstanceOf[Double] ||
- id.isInstanceOf[String])
+ id.isInstanceOf[String], "bad id type")
override def toString: String = id.toString
}
--- a/src/Tools/jEdit/src/completion_popup.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Sun Jan 10 13:04:29 2021 +0100
@@ -568,7 +568,7 @@
GUI_Thread.require {}
- require(items.nonEmpty)
+ require(items.nonEmpty, "no completion items")
val multi: Boolean = items.length > 1
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sun Jan 10 13:04:29 2021 +0100
@@ -127,7 +127,7 @@
def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
{
GUI_Thread.require {}
- require(!base_snapshot.is_outdated)
+ require(!base_snapshot.is_outdated, "document snapshot outdated")
current_base_snapshot = base_snapshot
current_base_results = base_results
--- a/src/Tools/jEdit/src/syntax_style.scala Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala Sun Jan 10 13:04:29 2021 +0100
@@ -23,7 +23,7 @@
/* extended syntax styles */
private val plain_range: Int = JEditToken.ID_COUNT
- private def check_range(i: Int) { require(0 <= i && i < plain_range) }
+ private def check_range(i: Int) { require(0 <= i && i < plain_range, "bad syntax style range") }
def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }