--- a/src/HOL/Tools/Nitpick/kodkod.scala Sun Jul 02 18:56:52 2023 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Pure/Concurrent/counter.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Pure/GUI/wrap_panel.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Pure/General/bytes.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Pure/General/file.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Pure/General/http.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Pure/General/scan.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Pure/PIDE/text.scala Sun Jul 02 19:05:59 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/Tools/build_process.scala Sun Jul 02 18:56:52 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Sun Jul 02 19:05:59 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
}
}
--- a/src/Tools/Graphview/mutator_dialog.scala Sun Jul 02 18:56:52 2023 +0200
+++ b/src/Tools/Graphview/mutator_dialog.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sun Jul 02 19:05:59 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 18:56:52 2023 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala Sun Jul 02 19:05:59 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