merged
authorwenzelm
Sun, 02 Jul 2023 20:41:07 +0200
changeset 78247 d4125fc10c0c
parent 78239 4fe65149f3fd (current diff)
parent 78246 76dd9b9cf624 (diff)
child 78249 1260be3f33a4
merged
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -35,7 +35,7 @@
   def execute(source: String,
     solve_all: Boolean = false,
     prove: Boolean = false,
-    max_solutions: Int = Integer.MAX_VALUE,
+    max_solutions: Int = Int.MaxValue,
     cleanup_inst: Boolean = false,
     timeout: Time = Time.zero,
     max_threads: Int = 0
--- a/src/Pure/Concurrent/counter.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/Concurrent/counter.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -18,7 +18,7 @@
   private var count: Counter.ID = 0
 
   def apply(): Counter.ID = synchronized {
-    require(count > java.lang.Long.MIN_VALUE, "counter overflow")
+    require(count > Long.MinValue, "counter overflow")
     count -= 1
     count
   }
--- a/src/Pure/GUI/wrap_panel.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/GUI/wrap_panel.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -33,7 +33,7 @@
     private def layout_size(target: Container, preferred: Boolean): Dimension = {
       target.getTreeLock.synchronized {
         val target_width =
-          if (target.getSize.width == 0) Integer.MAX_VALUE
+          if (target.getSize.width == 0) Int.MaxValue
           else target.getSize.width
 
         val hgap = getHgap
--- a/src/Pure/General/bytes.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/General/bytes.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -52,10 +52,10 @@
 
   /* read */
 
-  def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
+  def read_stream(stream: InputStream, limit: Int = Int.MaxValue, hint: Int = 1024): Bytes =
     if (limit == 0) empty
     else {
-      val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024
+      val out_size = (if (limit == Int.MaxValue) hint else limit) max 1024
       val out = new ByteArrayOutputStream(out_size)
       val buf = new Array[Byte](8192)
       var m = 0
@@ -74,7 +74,7 @@
   def read_file(file: JFile, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
     val start = offset.max(0L)
     val len = (file.length - start).max(0L).min(limit)
-    if (len > Integer.MAX_VALUE) error("Cannot read large file slice: " + Space.bytes(len).print)
+    if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print)
     else if (len == 0L) empty
     else {
       using(FileChannel.open(file.toPath, StandardOpenOption.READ)) { java_path =>
@@ -246,7 +246,7 @@
   def uncompress_zstd(cache: Compress.Cache = Compress.Cache.none): Bytes = {
     Zstd.init()
     val n = zstd.Zstd.decompressedSize(bytes, offset, length)
-    if (n > 0 && n < Integer.MAX_VALUE) {
+    if (n > 0 && n < Int.MaxValue) {
       Bytes(zstd.Zstd.decompress(array, n.toInt))
     }
     else {
--- a/src/Pure/General/file.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/General/file.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -183,7 +183,7 @@
       val options =
         if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS)
         else EnumSet.noneOf(classOf[FileVisitOption])
-      Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE,
+      Files.walkFileTree(start.toPath, options, Int.MaxValue,
         new SimpleFileVisitor[JPath] {
           override def preVisitDirectory(
             path: JPath,
--- a/src/Pure/General/http.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/General/http.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -69,7 +69,7 @@
     ): HttpURLConnection = {
       url.openConnection match {
         case connection: HttpURLConnection =>
-          if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) {
+          if (0 < timeout.ms && timeout.ms <= Int.MaxValue) {
             val ms = timeout.ms.toInt
             connection.setConnectTimeout(ms)
             connection.setReadTimeout(ms)
--- a/src/Pure/General/scan.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/General/scan.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -73,10 +73,10 @@
       repeated(pred, 0, 1)
 
     def many(pred: Symbol.Symbol => Boolean): Parser[String] =
-      repeated(pred, 0, Integer.MAX_VALUE)
+      repeated(pred, 0, Int.MaxValue)
 
     def many1(pred: Symbol.Symbol => Boolean): Parser[String] =
-      repeated(pred, 1, Integer.MAX_VALUE)
+      repeated(pred, 1, Int.MaxValue)
 
 
     /* character */
--- a/src/Pure/PIDE/text.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/PIDE/text.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -25,7 +25,7 @@
     def length(text: CharSequence): Range = Range(0, text.length)
 
     val zero: Range = apply(0)
-    val full: Range = apply(0, Integer.MAX_VALUE / 2)
+    val full: Range = apply(0, Int.MaxValue / 2)
     val offside: Range = apply(-1)
 
     object Ordering extends scala.math.Ordering[Range] {
--- a/src/Pure/System/progress.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/System/progress.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -57,6 +57,7 @@
     object Agents {
       val agent_uuid = SQL.Column.string("agent_uuid").make_primary_key
       val context_uuid = SQL.Column.string("context_uuid").make_primary_key
+      val kind = SQL.Column.string("kind")
       val hostname = SQL.Column.string("hostname")
       val java_pid = SQL.Column.long("java_pid")
       val java_start = SQL.Column.date("java_start")
@@ -66,7 +67,7 @@
       val seen = SQL.Column.long("seen")
 
       val table = make_table("agents",
-        List(agent_uuid, context_uuid, hostname, java_pid, java_start, start, stamp, stop, seen))
+        List(agent_uuid, context_uuid, kind, hostname, java_pid, java_start, start, stamp, stop, seen))
     }
 
     object Messages {
@@ -106,17 +107,22 @@
       db: SQL.Database,
       agent_uuid: String,
       seen: Long,
-      stop: Boolean = false
+      stop_now: Boolean = false
     ): Unit = {
-      val sql =
-        Agents.table.update(List(Agents.stamp, Agents.stop, Agents.seen),
-          sql = Agents.agent_uuid.where_equal(agent_uuid))
-      db.execute_statement(sql, body = { stmt =>
-        val now = db.now()
-        stmt.date(1) = now
-        stmt.date(2) = if (stop) Some(now) else None
-        stmt.long(3) = seen
-      })
+      val sql = Agents.agent_uuid.where_equal(agent_uuid)
+
+      val stop =
+        db.execute_query_statementO(
+          Agents.table.select(List(Agents.stop), sql = sql), _.get_date(Agents.stop)).flatten
+
+      db.execute_statement(
+        Agents.table.update(List(Agents.stamp, Agents.stop, Agents.seen), sql = sql),
+        body = { stmt =>
+          val now = db.now()
+          stmt.date(1) = now
+          stmt.date(2) = if (stop_now) Some(now) else stop
+          stmt.long(3) = seen
+        })
     }
 
     def next_messages_serial(db: SQL.Database, context: Long): Long =
@@ -238,6 +244,7 @@
 class Database_Progress(
   val db: SQL.Database,
   val base_progress: Progress,
+  val kind: String = "progress",
   val hostname: String = Isabelle_System.hostname(),
   val context_uuid: String = UUID.random().toString)
 extends Progress {
@@ -272,25 +279,27 @@
 
         stmt.string(1) = _agent_uuid
         stmt.string(2) = context_uuid
-        stmt.string(3) = hostname
-        stmt.long(4) = java_pid
-        stmt.date(5) = java_start
-        stmt.date(6) = now
+        stmt.string(3) = kind
+        stmt.string(4) = hostname
+        stmt.long(5) = java_pid
+        stmt.date(6) = java_start
         stmt.date(7) = now
-        stmt.date(8) = None
-        stmt.long(9) = 0L
+        stmt.date(8) = now
+        stmt.date(9) = None
+        stmt.long(10) = 0L
       })
     }
     if (context_uuid == _agent_uuid) Progress.Data.vacuum(db)
   }
 
-  def exit(): Unit = synchronized {
+  def exit(close: Boolean = false): Unit = synchronized {
     if (_context > 0) {
       Progress.Data.transaction_lock(db) {
-        Progress.Data.update_agent(db, _agent_uuid, _seen, stop = true)
+        Progress.Data.update_agent(db, _agent_uuid, _seen, stop_now = true)
       }
       _context = 0
     }
+    if (close) db.close()
   }
 
   private def sync_database[A](body: => A): A = synchronized {
--- a/src/Pure/Tools/build_process.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -219,7 +219,7 @@
     type Results = Map[String, Result]
 
     def inc_serial(serial: Long): Long = {
-      require(serial < java.lang.Long.MAX_VALUE, "serial overflow")
+      require(serial < Long.MaxValue, "serial overflow")
       serial + 1
     }
   }
@@ -282,7 +282,7 @@
   object Data extends SQL.Data("isabelle_build") {
     val database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
 
-    def pull_data[A <: Library.Named](
+    def pull[A <: Library.Named](
       data_domain: Set[String],
       data_iterator: Set[String] => Iterator[A],
       old_data: Map[String, A]
@@ -297,7 +297,7 @@
       new_data: Map[String, A],
       old_data: Map[String, A]
     ): Map[String, A] = {
-      pull_data(new_data.keySet, dom => new_data.valuesIterator.filter(a => dom(a.name)), old_data)
+      pull(new_data.keySet, dom => new_data.valuesIterator.filter(a => dom(a.name)), old_data)
     }
 
     def pull1[A <: Library.Named](
@@ -305,7 +305,7 @@
       data_base: Set[String] => Map[String, A],
       old_data: Map[String, A]
     ): Map[String, A] = {
-      pull_data(data_domain, dom => data_base(dom).valuesIterator, old_data)
+      pull(data_domain, dom => data_base(dom).valuesIterator, old_data)
     }
 
     object Generic {
@@ -548,16 +548,20 @@
       db: SQL.Database,
       worker_uuid: String,
       serial: Long,
-      stop: Boolean = false
+      stop_now: Boolean = false
     ): Unit = {
-      val sql =
-        Workers.table.update(List(Workers.stamp, Workers.stop, Workers.serial),
-          sql = Workers.worker_uuid.where_equal(worker_uuid))
-      db.execute_statement(sql, body =
-        { stmt =>
+      val sql = Workers.worker_uuid.where_equal(worker_uuid)
+
+      val stop =
+        db.execute_query_statementO(
+          Workers.table.select(List(Workers.stop), sql = sql), _.get_date(Workers.stop)).flatten
+
+      db.execute_statement(
+        Workers.table.update(List(Workers.stamp, Workers.stop, Workers.serial), sql = sql),
+        body = { stmt =>
           val now = db.now()
           stmt.date(1) = now
-          stmt.date(2) = if (stop) Some(now) else None
+          stmt.date(2) = if (stop_now) Some(now) else stop
           stmt.long(3) = serial
         })
     }
@@ -866,7 +870,8 @@
           val progress =
             new Database_Progress(progress_db, build_progress,
               hostname = hostname,
-              context_uuid = build_uuid)
+              context_uuid = build_uuid,
+              kind = "build_process")
           (progress, progress.agent_uuid)
         }
         catch { case exn: Throwable => close(); throw exn }
@@ -881,8 +886,7 @@
     Option(_host_database).flatten.foreach(_.close())
     progress match {
       case db_progress: Database_Progress =>
-        db_progress.exit()
-        db_progress.db.close()
+        db_progress.exit(close = true)
       case _ =>
     }
   }
@@ -1039,7 +1043,7 @@
 
   protected final def stop_worker(): Unit = synchronized_database {
     for (db <- _build_database) {
-      Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop = true)
+      Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop_now = true)
     }
   }
 
@@ -1074,8 +1078,8 @@
     }
     else {
       if (build_context.master) start_build()
+      start_worker()
 
-      start_worker()
       if (build_context.master && !build_context.worker_active) {
         progress.echo("Waiting for external workers ...")
       }
--- a/src/Tools/Graphview/mutator_dialog.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Tools/Graphview/mutator_dialog.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -158,7 +158,7 @@
     private val enabledBox = new Check_Box_Input("Enabled", initials.enabled)
 
     border = new EmptyBorder(5, 5, 5, 5)
-    maximumSize = new Dimension(Integer.MAX_VALUE, 30)
+    maximumSize = new Dimension(Int.MaxValue, 30)
     background = initials.color
 
     contents += new Label(initials.mutator.name) {
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -236,7 +236,7 @@
         }
         super.processKeyEvent(evt)
       }
-      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
+      { val max = getPreferredSize; max.width = Int.MaxValue; setMaximumSize(max) }
       setColumns(40)
       setToolTipText(expression_label.tooltip)
       setFont(GUI.imitate_font(getFont, scale = 1.2))
--- a/src/Tools/jEdit/src/query_dockable.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -43,7 +43,7 @@
         if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
         super.processKeyEvent(evt)
       }
-      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
+      { val max = getPreferredSize; max.width = Int.MaxValue; setMaximumSize(max) }
       setColumns(40)
       setToolTipText(tooltip)
       setFont(GUI.imitate_font(getFont, scale = 1.2))
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -533,11 +533,11 @@
             if (chunks != null) {
               try {
                 val line_start = buffer.getLineStartOffset(line)
-                gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
+                gfx.clipRect(x0, y + line_height * i, Int.MaxValue, line_height)
                 val w =
                   paint_chunk_list(rendering, font_subst, gfx,
                     line_start, chunks, x0.toFloat, y0.toFloat)
-                gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
+                gfx.clipRect(x0 + w.toInt, 0, Int.MaxValue, Int.MaxValue)
                 orig_text_painter.paintValidLine(gfx,
                   screen_line, line, start(i), end(i), y + line_height * i)
               } finally { gfx.setClip(clip) }
@@ -699,7 +699,7 @@
 
             val clip = gfx.getClip
             try {
-              gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight)
+              gfx.clipRect(x, y, Int.MaxValue, painter.getLineHeight)
               gfx.drawString(astr.getIterator, x, y1)
             }
             finally { gfx.setClip(clip) }
--- a/src/Tools/jEdit/src/syntax_style.scala	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Sun Jul 02 20:41:07 2023 +0200
@@ -67,7 +67,7 @@
 
   object Base_Extender extends SyntaxUtilities.StyleExtender {
     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = {
-      val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0))
+      val new_styles = Array.fill[SyntaxStyle](Byte.MaxValue)(styles(0))
       for (i <- 0 until full_range) {
         new_styles(i) = styles(i % plain_range)
       }
@@ -85,7 +85,7 @@
       val style0 = styles(0)
       val font0 = style0.getFont
 
-      val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0))
+      val new_styles = Array.fill[SyntaxStyle](Byte.MaxValue)(styles(0))
       for (i <- 0 until plain_range) {
         val style = styles(i)
         new_styles(i) = style