src/Pure/Tools/scala_build.scala
author wenzelm
Sat, 24 Jul 2021 18:07:07 +0200
changeset 74060 8cd746a5c291
parent 74057 22ad3ac2152c
child 74061 203dfa8bc0fc
permissions -rw-r--r--
clarified signature: more operations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/scala_build.scala
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     3
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     4
Manage and build Isabelle/Scala/Java components.
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     5
*/
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     6
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     7
package isabelle
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     8
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     9
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    10
import java.util.{Properties => JProperties}
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    11
import java.nio.file.Files
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    12
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    13
import scala.jdk.CollectionConverters._
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    14
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    15
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    16
object Scala_Build
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    17
{
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    18
  class Context private[Scala_Build](java_context: isabelle.setup.Build.Context)
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    19
  {
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    20
    override def toString: String = java_context.toString
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    21
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    22
    def is_module(path: Path): Boolean =
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    23
    {
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    24
      val module_name = java_context.module_name()
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    25
      module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file)
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    26
    }
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    27
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    28
    def sources: List[Path] =
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    29
      java_context.sources().asScala.toList.map(s => File.path(java_context.path(s).toFile))
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    30
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    31
    def requirements: List[Path] =
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    32
      (for {
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    33
        s <- java_context.requirements().asScala.iterator
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    34
        p <- java_context.requirement_paths(s).asScala.iterator
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    35
      } yield (File.path(p.toFile))).toList
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    36
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    37
    def build(fresh: Boolean = false): Unit =
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    38
      isabelle.setup.Build.build(java_context, fresh)
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    39
  }
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    40
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    41
  def context(dir: Path,
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    42
    component: Boolean = false,
74060
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    43
    no_title: Boolean = false,
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    44
    do_build: Boolean = false,
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    45
    module: Option[Path] = None): Context =
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    46
  {
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    47
    val props_name =
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    48
      if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    49
      else isabelle.setup.Build.BUILD_PROPS
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    50
    val props_path = dir + Path.explode(props_name)
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    51
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    52
    val props = new JProperties
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    53
    props.load(Files.newBufferedReader(props_path.java_path))
74060
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    54
    if (no_title) props.remove(isabelle.setup.Build.TITLE)
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    55
    if (do_build) props.remove(isabelle.setup.Build.NO_BUILD)
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    56
    if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get))
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    57
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    58
    new Context(new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode))
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    59
  }
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    60
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    61
  def build(dir: Path,
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    62
    fresh: Boolean = false,
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    63
    component: Boolean = false,
74060
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    64
    no_title: Boolean = false,
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    65
    do_build: Boolean = false,
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    66
    module: Option[Path] = None): Unit =
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    67
  {
74060
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    68
    context(dir, component = component, no_title = no_title, do_build = do_build, module = module)
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    69
      .build(fresh = fresh)
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    70
  }
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    71
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    72
  def build_result(dir: Path, component: Boolean = false): Bytes =
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    73
  {
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    74
    Isabelle_System.with_tmp_file("result", "jar")(tmp_file =>
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    75
    {
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    76
      build(dir, component = component, no_title = true, do_build = true, module = Some(tmp_file))
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    77
      Bytes.read(tmp_file)
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    78
    })
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    79
  }
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    80
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    81
  def component_contexts(): List[Context] =
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    82
    isabelle.setup.Build.component_contexts().asScala.toList.map(new Context(_))
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    83
}