# HG changeset patch # User wenzelm # Date 1688317559 -7200 # Node ID 0e221a8128e41876e48818eac1d56014d93402d4 # Parent 633ae08625d1534463d29ec8ec99d0525627c5ab tuned: prefer Scala over Java; diff -r 633ae08625d1 -r 0e221a8128e4 src/HOL/Tools/Nitpick/kodkod.scala --- 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 diff -r 633ae08625d1 -r 0e221a8128e4 src/Pure/Concurrent/counter.scala --- 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 } diff -r 633ae08625d1 -r 0e221a8128e4 src/Pure/GUI/wrap_panel.scala --- 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 diff -r 633ae08625d1 -r 0e221a8128e4 src/Pure/General/bytes.scala --- 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 { diff -r 633ae08625d1 -r 0e221a8128e4 src/Pure/General/file.scala --- 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, diff -r 633ae08625d1 -r 0e221a8128e4 src/Pure/General/http.scala --- 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) diff -r 633ae08625d1 -r 0e221a8128e4 src/Pure/General/scan.scala --- 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 */ diff -r 633ae08625d1 -r 0e221a8128e4 src/Pure/PIDE/text.scala --- 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] { diff -r 633ae08625d1 -r 0e221a8128e4 src/Pure/Tools/build_process.scala --- 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 } } diff -r 633ae08625d1 -r 0e221a8128e4 src/Tools/Graphview/mutator_dialog.scala --- 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) { diff -r 633ae08625d1 -r 0e221a8128e4 src/Tools/jEdit/src/debugger_dockable.scala --- 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)) diff -r 633ae08625d1 -r 0e221a8128e4 src/Tools/jEdit/src/query_dockable.scala --- 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)) diff -r 633ae08625d1 -r 0e221a8128e4 src/Tools/jEdit/src/rich_text_area.scala --- 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) } diff -r 633ae08625d1 -r 0e221a8128e4 src/Tools/jEdit/src/syntax_style.scala --- 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