--- 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