5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.lang.reflect.{Method, Modifier, InvocationTargetException} |
10 import java.lang.reflect.{Modifier, InvocationTargetException} |
11 import java.io.{File => JFile} |
11 import java.io.{File => JFile, StringWriter, PrintWriter} |
12 |
12 |
13 import scala.util.matching.Regex |
13 import scala.util.matching.Regex |
14 import scala.tools.nsc.GenericRunnerSettings |
14 import scala.tools.nsc.GenericRunnerSettings |
|
15 import scala.tools.nsc.interpreter.IMain |
15 |
16 |
16 |
17 |
17 object Scala |
18 object Scala |
18 { |
19 { |
19 /* compiler classpath and settings */ |
20 /* compiler */ |
20 |
21 |
21 def compiler_classpath(jar_dirs: List[JFile]): String = |
22 object Compiler |
22 { |
23 { |
23 def find_jars(dir: JFile): List[String] = |
24 def classpath(jar_dirs: List[JFile]): String = |
24 File.find_files(dir, file => file.getName.endsWith(".jar")). |
25 { |
25 map(File.absolute_name) |
26 def find_jars(dir: JFile): List[String] = |
|
27 File.find_files(dir, file => file.getName.endsWith(".jar")). |
|
28 map(File.absolute_name) |
26 |
29 |
27 val class_path = |
30 val class_path = |
28 for { |
31 for { |
29 prop <- List("scala.boot.class.path", "java.class.path") |
32 prop <- List("scala.boot.class.path", "java.class.path") |
30 path = System.getProperty(prop, "") if path != "\"\"" |
33 path = System.getProperty(prop, "") if path != "\"\"" |
31 elem <- space_explode(JFile.pathSeparatorChar, path) |
34 elem <- space_explode(JFile.pathSeparatorChar, path) |
32 } yield elem |
35 } yield elem |
33 |
36 |
34 (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) |
37 (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) |
35 } |
38 } |
36 |
39 |
37 def compiler_settings( |
40 type Settings = scala.tools.nsc.Settings |
38 error: String => Unit = Exn.error, |
41 |
39 jar_dirs: List[JFile] = Nil): GenericRunnerSettings = |
42 def settings( |
40 { |
43 error: String => Unit = Exn.error, |
41 val settings = new GenericRunnerSettings(error) |
44 jar_dirs: List[JFile] = Nil): Settings = |
42 settings.classpath.value = compiler_classpath(jar_dirs) |
45 { |
43 settings |
46 val settings = new GenericRunnerSettings(error) |
|
47 settings.classpath.value = classpath(jar_dirs) |
|
48 settings |
|
49 } |
|
50 |
|
51 def toplevel(settings: Settings, source: String): List[String] = |
|
52 { |
|
53 val out = new StringWriter |
|
54 val interp = new IMain(settings, new PrintWriter(out)) |
|
55 val rep = new interp.ReadEvalPrint |
|
56 val ok = interp.withLabel("\u0001") { rep.compile(source) } |
|
57 out.close |
|
58 |
|
59 val Error = """(?s)^\S* error: (.*)$""".r |
|
60 val errors = |
|
61 space_explode('\u0001', Library.strip_ansi_color(out.toString)). |
|
62 collect({ case Error(msg) => Word.capitalize(Library.trim_line(msg)) }) |
|
63 |
|
64 if (!ok && errors.isEmpty) List("Error") else errors |
|
65 } |
44 } |
66 } |
45 |
67 |
46 |
68 |
47 |
69 |
48 /** invoke JVM method via Isabelle/Scala **/ |
70 /** invoke JVM method via Isabelle/Scala **/ |