# HG changeset patch
# User wenzelm
# Date 1610280269 -3600
# Node ID c3589f2dff318d0bd02789f226ce1495ea836b00
# Parent  83a2b6976515a6006ea34a0c526a2d2cd8cfe6d8
more informative errors: simplify diagnosis of spurious failures reported by users;

diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Admin/build_cygwin.scala
--- 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 =>
       {
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Admin/build_status.scala
--- 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)
 
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Concurrent/counter.scala
--- 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
   }
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Concurrent/future.scala
--- 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) }
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Concurrent/isabelle_thread.scala
--- 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
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/GUI/gui_thread.scala
--- 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
   }
 
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/General/date.scala
--- 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)
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/General/scan.scala
--- 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)
     }
 
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/General/symbol.scala
--- 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
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/General/utf8.scala
--- 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)
   }
 }
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Isar/outer_syntax.scala
--- 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,
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/ML/ml_statistics.scala
--- 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)
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/PIDE/command.scala
--- 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 })
     }
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/PIDE/document.scala
--- 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 {
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/PIDE/headless.scala
--- 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)
       }
 
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/PIDE/line.scala
--- 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 {
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/PIDE/markup_tree.scala
--- 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)
               }
           })
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/PIDE/session.scala
--- 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
       {
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/System/cygwin.scala
--- 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*)
     {
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/System/linux.scala
--- 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
   }
 }
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Thy/bibtex.scala
--- 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) =
         {
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Thy/presentation.scala
--- 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) {
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Thy/thy_syntax.scala
--- 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
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/Tools/phabricator.scala
--- 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) :::
diff -r 83a2b6976515 -r c3589f2dff31 src/Pure/library.scala
--- 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)
 
diff -r 83a2b6976515 -r c3589f2dff31 src/Tools/VSCode/src/lsp.scala
--- 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
   }
diff -r 83a2b6976515 -r c3589f2dff31 src/Tools/jEdit/src/completion_popup.scala
--- 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
 
 
diff -r 83a2b6976515 -r c3589f2dff31 src/Tools/jEdit/src/pretty_text_area.scala
--- 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
diff -r 83a2b6976515 -r c3589f2dff31 src/Tools/jEdit/src/syntax_style.scala
--- 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 }