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) |