# HG changeset patch
# User wenzelm
# Date 1711304096 -3600
# Node ID ee04ce2ac13f17fdc1b94e6fe700122ac3fe07a9
# Parent  a4100b7ab9514ece227c0b2b00a2aad8f1f7d34a
clarified signature;

diff -r a4100b7ab951 -r ee04ce2ac13f src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Mar 24 19:10:55 2024 +0100
+++ b/src/Pure/General/file.scala	Sun Mar 24 19:14:56 2024 +0100
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import java.util.{Properties => JProperties}
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
   InputStreamReader, File => JFile, IOException}
@@ -253,6 +254,15 @@
   }
 
 
+  /* read properties */
+
+  def read_props(path: Path): JProperties = {
+    val props = new JProperties
+    props.load(Files.newBufferedReader(path.java_path))
+    props
+  }
+
+
   /* write */
 
   def writer(file: JFile): BufferedWriter =
diff -r a4100b7ab951 -r ee04ce2ac13f src/Pure/Tools/scala_build.scala
--- a/src/Pure/Tools/scala_build.scala	Sun Mar 24 19:10:55 2024 +0100
+++ b/src/Pure/Tools/scala_build.scala	Sun Mar 24 19:14:56 2024 +0100
@@ -7,7 +7,6 @@
 package isabelle
 
 
-import java.util.{Properties => JProperties}
 import java.io.{ByteArrayOutputStream, PrintStream}
 import java.nio.file.Files
 import java.nio.file.{Path => JPath}
@@ -73,8 +72,7 @@
       else isabelle.setup.Build.BUILD_PROPS
     val props_path = dir + Path.explode(props_name)
 
-    val props = new JProperties
-    props.load(Files.newBufferedReader(props_path.java_path))
+    val props = File.read_props(props_path)
     if (no_title) props.remove(isabelle.setup.Build.TITLE)
     if (do_build) props.remove(isabelle.setup.Build.NO_BUILD)
     if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get))