diff -r ea4f5b0ef497 -r 21164fd15e3d src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Wed Jul 06 13:08:33 2022 +0200 +++ b/src/Pure/System/scala.scala Tue Jul 05 13:12:04 2022 +0200 @@ -7,11 +7,23 @@ package isabelle -import java.io.{File => JFile, StringWriter, PrintWriter} +import java.io.{File => JFile, PrintStream, ByteArrayOutputStream, OutputStream} + +import scala.collection.mutable +import scala.annotation.tailrec -import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter} -import scala.tools.nsc.interpreter.{IMain, Results} -import scala.tools.nsc.interpreter.shell.ReplReporterImpl +import dotty.tools.dotc.CompilationUnit +import dotty.tools.dotc.ast.Trees.PackageDef +import dotty.tools.dotc.ast.untpd +import dotty.tools.dotc.core.Contexts.{Context => CompilerContext} +import dotty.tools.dotc.core.NameOps.moduleClassName +import dotty.tools.dotc.core.{Phases, StdNames} +import dotty.tools.dotc.interfaces +import dotty.tools.dotc.reporting.{Diagnostic, ConsoleReporter} +import dotty.tools.dotc.util.{SourceFile, SourcePosition, NoSourcePosition} +import dotty.tools.repl +import dotty.tools.repl.{ReplCompiler, ReplDriver} + object Scala { /** registered functions **/ @@ -89,78 +101,109 @@ /** compiler **/ def class_path(): List[String] = - for { - prop <- List("isabelle.scala.classpath", "java.class.path") - elems = System.getProperty(prop, "") if elems.nonEmpty - elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty - } yield elem + space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", "")) + .filter(_.nonEmpty) object Compiler { - def default_print_writer: PrintWriter = - new NewLinePrintWriter(new ConsoleWriter, true) + object Message { + object Kind extends Enumeration { + val error, warning, info, other = Value + } + private val Header = """^--.* (Error|Warning|Info): .*$""".r + val header_kind: String => Kind.Value = + { + case "Error" => Kind.error + case "Warning" => Kind.warning + case "Info" => Kind.info + case _ => Kind.other + } + + // see compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala + def split(str: String): List[Message] = { + var kind = Kind.other + val text = new mutable.StringBuilder + val result = new mutable.ListBuffer[Message] + + def flush(): Unit = { + if (text.nonEmpty) { result += Message(kind, text.toString) } + kind = Kind.other + text.clear() + } + + for (line <- Library.trim_split_lines(str)) { + line match { + case Header(k) => flush(); kind = header_kind(k) + case _ => if (line.startsWith("-- ")) flush() + } + if (text.nonEmpty) { text += '\n' } + text ++= line + } + flush() + result.toList + } + } + + sealed case class Message(kind: Message.Kind.Value, text: String) + { + def is_error: Boolean = kind == Message.Kind.error + override def toString: String = text + } + + sealed case class Result( + state: repl.State, + messages: List[Message], + unit: Option[CompilationUnit] = None + ) { + val errors: List[String] = messages.flatMap(msg => if (msg.is_error) Some(msg.text) else None) + def ok: Boolean = errors.isEmpty + def check_state: repl.State = if (ok) state else error(cat_lines(errors)) + override def toString: String = if (ok) "Result(ok)" else "Result(error)" + } def context( - print_writer: PrintWriter = default_print_writer, - error: String => Unit = Exn.error, + settings: List[String] = Nil, jar_dirs: List[JFile] = Nil, class_loader: Option[ClassLoader] = None ): Context = { + val isabelle_settings = + Word.explode(Isabelle_System.getenv_strict("ISABELLE_SCALAC_OPTIONS")) + def find_jars(dir: JFile): List[String] = File.find_files(dir, file => file.getName.endsWith(".jar")). map(File.absolute_name) - val settings = new GenericRunnerSettings(error) - settings.classpath.value = - (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) - - new Context(settings, print_writer, class_loader) + val classpath = (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) + val settings1 = isabelle_settings ::: settings ::: List("-classpath", classpath) + new Context(settings1, class_loader) } class Context private [Compiler]( - val settings: GenericRunnerSettings, - val print_writer: PrintWriter, - val class_loader: Option[ClassLoader] + val settings: List[String], + val class_loader: Option[ClassLoader] = None ) { - override def toString: String = settings.toString + private val out_stream = new ByteArrayOutputStream(1024) + private val out = new PrintStream(out_stream) + private val driver: ReplDriver = new ReplDriver(settings.toArray, out, class_loader) - val interp: IMain = - new IMain(settings, new ReplReporterImpl(settings, print_writer)) { - override def parentClassLoader: ClassLoader = - class_loader getOrElse super.parentClassLoader - } - } + def init_state: repl.State = driver.initialState - def toplevel(interpret: Boolean, source: String): List[String] = { - val out = new StringWriter - val interp = Compiler.context(print_writer = new PrintWriter(out)).interp - val marker = '\u000b' - val ok = - interp.withLabel(marker.toString) { - if (interpret) interp.interpret(source) == Results.Success - else (new interp.ReadEvalPrint).compile(source) - } - out.close() - - val Error = """(?s)^\S* error: (.*)$""".r - val errors = - space_explode(marker, Library.strip_ansi_color(out.toString)). - collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) - - if (!ok && errors.isEmpty) List("Error") else errors + def compile(source: String, state: repl.State = init_state): Result = { + out.flush() + out_stream.reset() + val state1 = driver.run(source)(state) + out.flush() + val messages = Message.split(out_stream.toString(UTF8.charset)) + out_stream.reset() + Result(state1, messages) + } } } object Toplevel extends Fun_String("scala_toplevel") { val here = Scala_Project.here - def apply(arg: String): String = { - val (interpret, source) = - YXML.parse_body(arg) match { - case Nil => (false, "") - case List(XML.Text(source)) => (false, source) - case body => import XML.Decode._; pair(bool, string)(body) - } + def apply(source: String): String = { val errors = - try { Compiler.toplevel(interpret, source) } + try { Compiler.context().compile(source).errors.map("Scala error: " + _) } catch { case ERROR(msg) => List(msg) } locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } @@ -174,7 +217,7 @@ /* requests */ sealed abstract class Request - case class Execute(command: Compiler.Context => Unit) extends Request + case class Execute(command: (Compiler.Context, repl.State) => repl.State) extends Request case object Shutdown extends Request @@ -189,19 +232,21 @@ known.value.collectFirst(which) } - class Interpreter(context: Compiler.Context) { + class Interpreter(context: Compiler.Context, out: OutputStream = Console.out) { interpreter => private val running = Synchronized[Option[Thread]](None) def running_thread(thread: Thread): Boolean = running.value.contains(thread) def interrupt_thread(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt }) + private var state = context.init_state + private lazy val thread: Consumer_Thread[Interpreter.Request] = Consumer_Thread.fork("Scala.Interpreter") { case Interpreter.Execute(command) => try { running.change(_ => Some(Thread.currentThread())) - command(context) + state = command(context, state) } finally { running.change(_ => None) @@ -219,9 +264,12 @@ thread.shutdown() } - def execute(command: Compiler.Context => Unit): Unit = + def execute(command: (Compiler.Context, repl.State) => repl.State): Unit = thread.send(Interpreter.Execute(command)) + def reset(): Unit = + thread.send(Interpreter.Execute((context, _) => context.init_state)) + Interpreter.add(interpreter) thread }