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:
74060
diff
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:
74060
diff
changeset
|
46 |
def build(fresh: Boolean = false): String = |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
47 |
{ |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
48 |
val output0 = new ByteArrayOutputStream |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
49 |
val output = new PrintStream(output0) |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
50 |
def get_output(): String = |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
51 |
{ |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
52 |
output.flush() |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
53 |
Library.trim_line(output0.toString(UTF8.charset)) |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
54 |
} |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
55 |
try { |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
56 |
Console.withOut(output) { |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
57 |
Console.withErr(output) { |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
58 |
isabelle.setup.Build.build(output, java_context, fresh) |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
59 |
} |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
60 |
} |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
61 |
get_output() |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
62 |
} |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
changeset
|
63 |
catch { case ERROR(msg) => cat_error(get_output(), msg) } |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
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:
74060
diff
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:
74060
diff
changeset
|
108 |
|
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
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:
74060
diff
changeset
|
113 |
val output = |
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
wenzelm
parents:
74060
diff
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 |
} |