src/Pure/Tools/scala_build.scala
changeset 75393 87ebf5a50283
parent 74062 4dbac13d89a5
child 75394 42267c650205
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
    12 import java.nio.file.Files
    12 import java.nio.file.Files
    13 
    13 
    14 import scala.jdk.CollectionConverters._
    14 import scala.jdk.CollectionConverters._
    15 
    15 
    16 
    16 
    17 object Scala_Build
    17 object Scala_Build {
    18 {
    18   class Context private[Scala_Build](java_context: isabelle.setup.Build.Context) {
    19   class Context private[Scala_Build](java_context: isabelle.setup.Build.Context)
       
    20   {
       
    21     override def toString: String = java_context.toString
    19     override def toString: String = java_context.toString
    22 
    20 
    23     def is_module(path: Path): Boolean =
    21     def is_module(path: Path): Boolean = {
    24     {
       
    25       val module_name = java_context.module_name()
    22       val module_name = java_context.module_name()
    26       module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file)
    23       module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file)
    27     }
    24     }
    28 
    25 
    29     def module_result: Option[Path] =
    26     def module_result: Option[Path] = {
    30     {
       
    31       java_context.module_result() match {
    27       java_context.module_result() match {
    32         case "" => None
    28         case "" => None
    33         case module => Some(File.path(java_context.path(module).toFile))
    29         case module => Some(File.path(java_context.path(module).toFile))
    34       }
    30       }
    35     }
    31     }
    41       (for {
    37       (for {
    42         s <- java_context.requirements().asScala.iterator
    38         s <- java_context.requirements().asScala.iterator
    43         p <- java_context.requirement_paths(s).asScala.iterator
    39         p <- java_context.requirement_paths(s).asScala.iterator
    44       } yield (File.path(p.toFile))).toList
    40       } yield (File.path(p.toFile))).toList
    45 
    41 
    46     def build(fresh: Boolean = false): String =
    42     def build(fresh: Boolean = false): String = {
    47     {
       
    48       val output0 = new ByteArrayOutputStream
    43       val output0 = new ByteArrayOutputStream
    49       val output = new PrintStream(output0)
    44       val output = new PrintStream(output0)
    50       def get_output(): String =
    45       def get_output(): String = {
    51       {
       
    52         output.flush()
    46         output.flush()
    53         Library.trim_line(output0.toString(UTF8.charset))
    47         Library.trim_line(output0.toString(UTF8.charset))
    54       }
    48       }
    55       try {
    49       try {
    56         Console.withOut(output) {
    50         Console.withOut(output) {
    66 
    60 
    67   def context(dir: Path,
    61   def context(dir: Path,
    68     component: Boolean = false,
    62     component: Boolean = false,
    69     no_title: Boolean = false,
    63     no_title: Boolean = false,
    70     do_build: Boolean = false,
    64     do_build: Boolean = false,
    71     module: Option[Path] = None): Context =
    65     module: Option[Path] = None
    72   {
    66   ): Context = {
    73     val props_name =
    67     val props_name =
    74       if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS
    68       if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS
    75       else isabelle.setup.Build.BUILD_PROPS
    69       else isabelle.setup.Build.BUILD_PROPS
    76     val props_path = dir + Path.explode(props_name)
    70     val props_path = dir + Path.explode(props_name)
    77 
    71 
    87   def build(dir: Path,
    81   def build(dir: Path,
    88     fresh: Boolean = false,
    82     fresh: Boolean = false,
    89     component: Boolean = false,
    83     component: Boolean = false,
    90     no_title: Boolean = false,
    84     no_title: Boolean = false,
    91     do_build: Boolean = false,
    85     do_build: Boolean = false,
    92     module: Option[Path] = None): String =
    86     module: Option[Path] = None
    93   {
    87   ): String = {
    94     context(dir, component = component, no_title = no_title, do_build = do_build, module = module)
    88     context(dir, component = component, no_title = no_title, do_build = do_build, module = module)
    95       .build(fresh = fresh)
    89       .build(fresh = fresh)
    96   }
    90   }
    97 
    91 
    98   sealed case class Result(output: String, jar_bytes: Bytes, jar_path: Option[Path])
    92   sealed case class Result(output: String, jar_bytes: Bytes, jar_path: Option[Path]) {
    99   {
    93     def write(): Unit = {
   100     def write(): Unit =
       
   101     {
       
   102       if (jar_path.isDefined) {
    94       if (jar_path.isDefined) {
   103         Isabelle_System.make_directory(jar_path.get.dir)
    95         Isabelle_System.make_directory(jar_path.get.dir)
   104         Bytes.write(jar_path.get, jar_bytes)
    96         Bytes.write(jar_path.get, jar_bytes)
   105       }
    97       }
   106     }
    98     }
   107   }
    99   }
   108 
   100 
   109   def build_result(dir: Path, component: Boolean = false): Result =
   101   def build_result(dir: Path, component: Boolean = false): Result = {
   110   {
   102     Isabelle_System.with_tmp_file("result", "jar")(tmp_file => {
   111     Isabelle_System.with_tmp_file("result", "jar")(tmp_file =>
       
   112     {
       
   113       val output =
   103       val output =
   114         build(dir, component = component, no_title = true, do_build = true, module = Some(tmp_file))
   104         build(dir, component = component, no_title = true, do_build = true, module = Some(tmp_file))
   115       val jar_bytes = Bytes.read(tmp_file)
   105       val jar_bytes = Bytes.read(tmp_file)
   116       val jar_path = context(dir, component = component).module_result
   106       val jar_path = context(dir, component = component).module_result
   117       Result(output, jar_bytes, jar_path)
   107       Result(output, jar_bytes, jar_path)