# HG changeset patch
# User wenzelm
# Date 1614635400 -3600
# Node ID d0378baf7d067ddf9b0bf7022b77f1b5b406c381
# Parent  0bf768567d9f7b920eeef933d39196c2f395d271
tuned --- avoid deprecated conversions between certain number type;

diff -r 0bf768567d9f -r d0378baf7d06 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Mon Mar 01 22:37:33 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Mon Mar 01 22:50:00 2021 +0100
@@ -415,18 +415,18 @@
               File.write(data_file,
                 cat_lines(
                   session.finished_entries.map(entry =>
-                    List(entry.date,
-                      entry.timing.elapsed.minutes,
-                      entry.timing.resources.minutes,
-                      entry.ml_timing.elapsed.minutes,
-                      entry.ml_timing.resources.minutes,
-                      entry.maximum_code,
-                      entry.maximum_code,
-                      entry.average_stack,
-                      entry.maximum_stack,
-                      entry.average_heap,
-                      entry.average_heap,
-                      entry.stored_heap).mkString(" "))))
+                    List(entry.date.toString,
+                      entry.timing.elapsed.minutes.toString,
+                      entry.timing.resources.minutes.toString,
+                      entry.ml_timing.elapsed.minutes.toString,
+                      entry.ml_timing.resources.minutes.toString,
+                      entry.maximum_code.toString,
+                      entry.maximum_code.toString,
+                      entry.average_stack.toString,
+                      entry.maximum_stack.toString,
+                      entry.average_heap.toString,
+                      entry.average_heap.toString,
+                      entry.stored_heap.toString).mkString(" "))))
 
               val max_time =
                 ((0.0 /: session.finished_entries){ case (m, entry) =>
diff -r 0bf768567d9f -r d0378baf7d06 src/Pure/General/graphics_file.scala
--- a/src/Pure/General/graphics_file.scala	Mon Mar 01 22:37:33 2021 +0100
+++ b/src/Pure/General/graphics_file.scala	Mon Mar 01 22:50:00 2021 +0100
@@ -63,13 +63,13 @@
     {
       val document = new Document()
       try {
-        document.setPageSize(new Rectangle(width, height))
+        document.setPageSize(new Rectangle(width.toFloat, height.toFloat))
         val writer = PdfWriter.getInstance(document, out)
         document.open()
 
         val cb = writer.getDirectContent()
-        val tp = cb.createTemplate(width, height)
-        val gfx = tp.createGraphics(width, height, font_mapper())
+        val tp = cb.createTemplate(width.toFloat, height.toFloat)
+        val gfx = tp.createGraphics(width.toFloat, height.toFloat, font_mapper())
 
         paint(gfx)
         gfx.dispose
diff -r 0bf768567d9f -r d0378baf7d06 src/Tools/jEdit/src/font_info.scala
--- a/src/Tools/jEdit/src/font_info.scala	Mon Mar 01 22:37:33 2021 +0100
+++ b/src/Tools/jEdit/src/font_info.scala	Mon Mar 01 22:50:00 2021 +0100
@@ -22,7 +22,7 @@
   val min_size = 5
   val max_size = 250
 
-  def restrict_size(size: Float): Float = size max min_size min max_size
+  def restrict_size(size: Float): Float = size max min_size.toFloat min max_size.toFloat
 
 
   /* main jEdit font */
diff -r 0bf768567d9f -r d0378baf7d06 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 01 22:37:33 2021 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 01 22:50:00 2021 +0100
@@ -523,7 +523,8 @@
               try {
                 val line_start = buffer.getLineStartOffset(line)
                 gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
-                val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
+                val w =
+                  paint_chunk_list(rendering, gfx, line_start, chunks, x0.toFloat, y0.toFloat).toInt
                 gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
                 orig_text_painter.paintValidLine(gfx,
                   screen_line, line, start(i), end(i), y + line_height * i)