| author | wenzelm | 
| Sat, 24 Jul 2021 20:25:36 +0200 | |
| changeset 74062 | 4dbac13d89a5 | 
| parent 74061 | 203dfa8bc0fc | 
| child 75393 | 87ebf5a50283 | 
| permissions | -rw-r--r-- | 
| 74055 | 1 | /* Title: Pure/Tools/scala_build.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 4 | Manage and build Isabelle/Scala/Java components. | |
| 5 | */ | |
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 10 | import java.util.{Properties => JProperties}
 | |
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 11 | import java.io.{ByteArrayOutputStream, PrintStream}
 | 
| 74055 | 12 | import java.nio.file.Files | 
| 13 | ||
| 14 | import scala.jdk.CollectionConverters._ | |
| 15 | ||
| 16 | ||
| 17 | object Scala_Build | |
| 18 | {
 | |
| 74056 | 19 | class Context private[Scala_Build](java_context: isabelle.setup.Build.Context) | 
| 20 |   {
 | |
| 74057 | 21 | override def toString: String = java_context.toString | 
| 22 | ||
| 74056 | 23 | def is_module(path: Path): Boolean = | 
| 24 |     {
 | |
| 74057 | 25 | val module_name = java_context.module_name() | 
| 74056 | 26 | module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file) | 
| 27 | } | |
| 28 | ||
| 74062 | 29 | def module_result: Option[Path] = | 
| 30 |     {
 | |
| 31 |       java_context.module_result() match {
 | |
| 32 | case "" => None | |
| 33 | case module => Some(File.path(java_context.path(module).toFile)) | |
| 34 | } | |
| 35 | } | |
| 36 | ||
| 74056 | 37 | def sources: List[Path] = | 
| 38 | java_context.sources().asScala.toList.map(s => File.path(java_context.path(s).toFile)) | |
| 39 | ||
| 40 | def requirements: List[Path] = | |
| 41 |       (for {
 | |
| 42 | s <- java_context.requirements().asScala.iterator | |
| 43 | p <- java_context.requirement_paths(s).asScala.iterator | |
| 44 | } yield (File.path(p.toFile))).toList | |
| 45 | ||
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 46 | def build(fresh: Boolean = false): String = | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 47 |     {
 | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 48 | val output0 = new ByteArrayOutputStream | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 49 | val output = new PrintStream(output0) | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 50 | def get_output(): String = | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 51 |       {
 | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 52 | output.flush() | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 53 | Library.trim_line(output0.toString(UTF8.charset)) | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 54 | } | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 55 |       try {
 | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 56 |         Console.withOut(output) {
 | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 57 |           Console.withErr(output) {
 | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 58 | isabelle.setup.Build.build(output, java_context, fresh) | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 59 | } | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 60 | } | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 61 | get_output() | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 62 | } | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 63 |       catch { case ERROR(msg) => cat_error(get_output(), msg) }
 | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 64 | } | 
| 74056 | 65 | } | 
| 74055 | 66 | |
| 67 | def context(dir: Path, | |
| 68 | component: Boolean = false, | |
| 74060 | 69 | no_title: Boolean = false, | 
| 74057 | 70 | do_build: Boolean = false, | 
| 71 | module: Option[Path] = None): Context = | |
| 74055 | 72 |   {
 | 
| 73 | val props_name = | |
| 74 | if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS | |
| 75 | else isabelle.setup.Build.BUILD_PROPS | |
| 76 | val props_path = dir + Path.explode(props_name) | |
| 77 | ||
| 78 | val props = new JProperties | |
| 79 | props.load(Files.newBufferedReader(props_path.java_path)) | |
| 74060 | 80 | if (no_title) props.remove(isabelle.setup.Build.TITLE) | 
| 74057 | 81 | if (do_build) props.remove(isabelle.setup.Build.NO_BUILD) | 
| 82 | if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get)) | |
| 74055 | 83 | |
| 74056 | 84 | new Context(new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode)) | 
| 74055 | 85 | } | 
| 86 | ||
| 87 | def build(dir: Path, | |
| 88 | fresh: Boolean = false, | |
| 89 | component: Boolean = false, | |
| 74060 | 90 | no_title: Boolean = false, | 
| 74057 | 91 | do_build: Boolean = false, | 
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 92 | module: Option[Path] = None): String = | 
| 74055 | 93 |   {
 | 
| 74060 | 94 | context(dir, component = component, no_title = no_title, do_build = do_build, module = module) | 
| 95 | .build(fresh = fresh) | |
| 96 | } | |
| 97 | ||
| 74062 | 98 | sealed case class Result(output: String, jar_bytes: Bytes, jar_path: Option[Path]) | 
| 99 |   {
 | |
| 100 | def write(): Unit = | |
| 101 |     {
 | |
| 102 |       if (jar_path.isDefined) {
 | |
| 103 | Isabelle_System.make_directory(jar_path.get.dir) | |
| 104 | Bytes.write(jar_path.get, jar_bytes) | |
| 105 | } | |
| 106 | } | |
| 107 | } | |
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 108 | |
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 109 | def build_result(dir: Path, component: Boolean = false): Result = | 
| 74060 | 110 |   {
 | 
| 111 |     Isabelle_System.with_tmp_file("result", "jar")(tmp_file =>
 | |
| 112 |     {
 | |
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 113 | val output = | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 114 | build(dir, component = component, no_title = true, do_build = true, module = Some(tmp_file)) | 
| 74062 | 115 | val jar_bytes = Bytes.read(tmp_file) | 
| 116 | val jar_path = context(dir, component = component).module_result | |
| 117 | Result(output, jar_bytes, jar_path) | |
| 74060 | 118 | }) | 
| 74055 | 119 | } | 
| 120 | ||
| 121 | def component_contexts(): List[Context] = | |
| 74056 | 122 | isabelle.setup.Build.component_contexts().asScala.toList.map(new Context(_)) | 
| 74055 | 123 | } |