# HG changeset patch # User wenzelm # Date 1688323267 -7200 # Node ID d4125fc10c0c2ef42494a2197a6cf689873b8b50 # Parent 4fe65149f3fd642c278dc55b61f3e69805916981# Parent 76dd9b9cf62460be701e19b41d89b29d80c2e8d5 merged diff -r 4fe65149f3fd -r d4125fc10c0c src/HOL/Tools/Nitpick/kodkod.scala --- 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 diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/Concurrent/counter.scala --- 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 } diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/GUI/wrap_panel.scala --- 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 diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/General/bytes.scala --- 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 { diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/General/file.scala --- 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, diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/General/http.scala --- 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) diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/General/scan.scala --- 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 */ diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/PIDE/text.scala --- 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] { diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/System/progress.scala --- 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 { diff -r 4fe65149f3fd -r d4125fc10c0c src/Pure/Tools/build_process.scala --- 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 ...") } diff -r 4fe65149f3fd -r d4125fc10c0c src/Tools/Graphview/mutator_dialog.scala --- 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) { diff -r 4fe65149f3fd -r d4125fc10c0c src/Tools/jEdit/src/debugger_dockable.scala --- 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)) diff -r 4fe65149f3fd -r d4125fc10c0c src/Tools/jEdit/src/query_dockable.scala --- 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)) diff -r 4fe65149f3fd -r d4125fc10c0c src/Tools/jEdit/src/rich_text_area.scala --- 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) } diff -r 4fe65149f3fd -r d4125fc10c0c src/Tools/jEdit/src/syntax_style.scala --- 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