--- a/Admin/components/main Wed Jul 06 13:08:33 2022 +0200
+++ b/Admin/components/main Tue Jul 05 13:12:04 2022 +0200
@@ -9,7 +9,7 @@
flatlaf-1.6.4
idea-icons-20210508
isabelle_fonts-20211004
-isabelle_setup-20220323
+isabelle_setup-20220701
jdk-17.0.2+8
jedit-20211103
jfreechart-1.5.3
@@ -21,7 +21,7 @@
pdfjs-2.12.313
polyml-test-15c840d48c9a
postgresql-42.2.24
-scala-2.13.5-1
+scala-3.1.3
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.36.0.3
--- a/NEWS Wed Jul 06 13:08:33 2022 +0200
+++ b/NEWS Tue Jul 05 13:12:04 2022 +0200
@@ -188,6 +188,12 @@
*** System ***
+* Isabelle/Scala is now based on Scala 3. This is a completely different
+compiler ("dotty") and a quite different source language (we are using
+the classic Java-style syntax, not the new Python-style syntax).
+Occasional INCOMPATIBILITY, see also the official Scala documentation
+https://docs.scala-lang.org/scala3/guides/migration/compatibility-intro.html
+
* Command-line tool "isabelle scala_project" supports Gradle as
alternative to Maven: either option -G or -M needs to be specified
explicitly. This increases the chances that the Java/Scala IDE project
--- a/etc/settings Wed Jul 06 13:08:33 2022 +0200
+++ b/etc/settings Tue Jul 05 13:12:04 2022 +0200
@@ -17,7 +17,7 @@
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 11 -target 11"
-ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -deprecation -target:11 -Xsource:3 -J-Xms512m -J-Xmx4g -J-Xss16m"
+ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -deprecation -release 11 -source 3.1 -old-syntax -no-indent -color never -pagewidth 78 -J-Xms512m -J-Xmx4g -J-Xss16m"
ISABELLE_SCALA_JAR="$ISABELLE_HOME/lib/classes/isabelle.jar"
--- a/lib/Tools/scala Wed Jul 06 13:08:33 2022 +0200
+++ b/lib/Tools/scala Tue Jul 05 13:12:04 2022 +0200
@@ -6,16 +6,10 @@
isabelle scala_build || exit $?
-eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
-declare -a SCALA_ARGS=()
-for ARG in "${JAVA_ARGS[@]}"
-do
- SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
-done
-
classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
classpath "$CLASSPATH"; unset CLASSPATH
-isabelle_scala scala "${SCALA_ARGS[@]}" \
- -classpath "$(platform_path "$ISABELLE_CLASSPATH")" \
- -Disabelle.scala.classpath="$(platform_path "$ISABELLE_CLASSPATH")" "$@"
+export jvm_cp_args="$(platform_path "$ISABELLE_CLASSPATH")"
+export JAVA_OPTS="$ISABELLE_JAVA_SYSTEM_OPTIONS -J-Dscala.usejavacp=true"
+
+isabelle_scala scala $ISABELLE_SCALAC_OPTIONS "$@"
--- a/lib/scripts/getsettings Wed Jul 06 13:08:33 2022 +0200
+++ b/lib/scripts/getsettings Tue Jul 05 13:12:04 2022 +0200
@@ -130,7 +130,7 @@
fi
if [ -e "$ISABELLE_SETUP_JAR" ]; then
- ISABELLE_SETUP_CLASSPATH="$(isabelle_jdk java -classpath "$(platform_path "$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath)"
+ ISABELLE_SETUP_CLASSPATH="$(isabelle_jdk java -classpath "$(platform_path "$SCALA_INTERFACES:$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath)"
fi
set +o allexport
--- a/src/HOL/Library/code_test.ML Wed Jul 06 13:08:33 2022 +0200
+++ b/src/HOL/Library/code_test.ML Tue Jul 05 13:12:04 2022 +0200
@@ -506,7 +506,7 @@
}\<close>
val _ = File.write code_path code
val _ = File.write driver_path driver
- val _ = Scala_Compiler.toplevel true (code ^ driver)
+ val _ = Scala_Compiler.toplevel (code ^ driver)
handle ERROR msg => error ("Evaluation for " ^ scalaN ^ " failed:\n" ^ msg)
in File.read out_path end
--- 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
}
--- a/src/Pure/System/scala_compiler.ML Wed Jul 06 13:08:33 2022 +0200
+++ b/src/Pure/System/scala_compiler.ML Tue Jul 05 13:12:04 2022 +0200
@@ -6,7 +6,7 @@
signature SCALA_COMPILER =
sig
- val toplevel: bool -> string -> unit
+ val toplevel: string -> unit
val static_check: string * Position.T -> unit
end;
@@ -15,18 +15,15 @@
(* check declaration *)
-fun toplevel interpret source =
+fun toplevel source =
let val errors =
- (interpret, source)
- |> let open XML.Encode in pair bool string end
- |> YXML.string_of_body
- |> \<^scala>\<open>scala_toplevel\<close>
+ \<^scala>\<open>scala_toplevel\<close> source
|> YXML.parse_body
|> let open XML.Decode in list string end
in if null errors then () else error (cat_lines errors) end;
fun static_check (source, pos) =
- toplevel false ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
+ toplevel ("class __Dummy__ { __dummy__ => " ^ source ^ " }")
handle ERROR msg => error (msg ^ Position.here pos);
--- a/src/Pure/Tools/scala_build.scala Wed Jul 06 13:08:33 2022 +0200
+++ b/src/Pure/Tools/scala_build.scala Tue Jul 05 13:12:04 2022 +0200
@@ -47,11 +47,7 @@
Library.trim_line(output0.toString(UTF8.charset))
}
try {
- Console.withOut(output) {
- Console.withErr(output) {
- isabelle.setup.Build.build(output, java_context, fresh)
- }
- }
+ isabelle.setup.Build.build(output, java_context, fresh)
get_output()
}
catch { case ERROR(msg) => cat_error(get_output(), msg) }
--- a/src/Pure/Tools/scala_project.scala Wed Jul 06 13:08:33 2022 +0200
+++ b/src/Pure/Tools/scala_project.scala Tue Jul 05 13:12:04 2022 +0200
@@ -12,7 +12,7 @@
/** build tools **/
val java_version: String = "17"
- val scala_version: String = "2.13.5"
+ val scala_version: String = "3.1.3"
abstract class Build_Tool {
def project_root: Path
@@ -66,7 +66,7 @@
}
dependencies {
- implementation 'org.scala-lang:scala-library:""" + scala_version + """'
+ implementation 'org.scala-lang:scala3-library_3:scala-library:""" + scala_version + """'
compileOnly files(
""" + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n ", ")") +
"""
--- a/src/Tools/Setup/src/Build.java Wed Jul 06 13:08:33 2022 +0200
+++ b/src/Tools/Setup/src/Build.java Tue Jul 05 13:12:04 2022 +0200
@@ -38,7 +38,10 @@
import javax.tools.StandardJavaFileManager;
import javax.tools.ToolProvider;
-import scala.tools.nsc.MainClass;
+import dotty.tools.dotc.Driver;
+import dotty.tools.dotc.interfaces.Diagnostic;
+import dotty.tools.dotc.interfaces.ReporterResult;
+import dotty.tools.dotc.interfaces.SimpleReporter;
public class Build
@@ -245,7 +248,7 @@
}
public static void compile_scala_sources(
- PrintStream output, // ignored, but see scala.Console.withOut/withErr
+ PrintStream output,
Path target_dir,
String more_options,
List<Path> deps,
@@ -266,8 +269,16 @@
if (p.toString().endsWith(".scala")) { scala_sources = true; }
}
if (scala_sources) {
- boolean ok = new MainClass().process(args.toArray(String[]::new));
- if (!ok) { throw new RuntimeException("Failed to compile Scala sources"); }
+ String[] args_array = args.toArray(String[]::new);
+ SimpleReporter reporter = new SimpleReporter() {
+ @Override
+ public void report(Diagnostic diagnostic) {
+ output.println(diagnostic.message());
+ }
+ };
+ new Driver().process(args_array, reporter, null);
+ ReporterResult result = new Driver().process(args_array);
+ if (result.hasErrors()) { throw new RuntimeException("Failed to compile Scala sources"); }
}
}
--- a/src/Tools/jEdit/jedit_main/scala_console.scala Wed Jul 06 13:08:33 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala Tue Jul 05 13:12:04 2022 +0200
@@ -12,7 +12,7 @@
import console.{Console, ConsolePane, Shell, Output}
import org.gjt.sp.jedit.JARClassLoader
-import java.io.{OutputStream, Writer, PrintWriter}
+import java.io.OutputStream
object Scala_Console {
@@ -67,17 +67,6 @@
}
}
- private val console_writer = new Writer {
- def flush(): Unit = console_stream.flush()
- def close(): Unit = console_stream.flush()
-
- def write(cbuf: Array[Char], off: Int, len: Int): Unit = {
- if (len > 0) {
- UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
- }
- }
- }
-
private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = {
global_console = console
global_out = out
@@ -95,24 +84,18 @@
}
}
- private def report_error(str: String): Unit = {
- if (global_console == null || global_err == null) isabelle.Output.writeln(str)
- else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
- }
-
/* jEdit console methods */
override def openConsole(console: Console): Unit = {
val context =
Scala.Compiler.context(
- print_writer = new PrintWriter(console_writer, true),
- error = report_error,
jar_dirs = JEdit_Lib.directories,
class_loader = Some(new JARClassLoader))
val interpreter = new Scala_Console.Interpreter(context, console)
- interpreter.execute(_.interp.interpret(Scala_Console.init))
+ interpreter.execute((context, state) =>
+ context.compile(Scala_Console.init, state = state).state)
}
override def closeConsole(console: Console): Unit =
@@ -141,12 +124,18 @@
command: String
): Unit = {
Scala_Console.console_interpreter(console).foreach(interpreter =>
- interpreter.execute { context =>
- with_console(console, out, err) { context.interp.interpret(command) }
+ interpreter.execute { (context, state) =>
+ val result = with_console(console, out, err) { context.compile(command, state) }
GUI_Thread.later {
+ val diag = if (err == null) out else err
+ for (message <- result.messages) {
+ val color = if (message.is_error) console.getErrorColor else null
+ diag.print(color, message.text + "\n")
+ }
Option(err).foreach(_.commandDone())
out.commandDone()
}
+ result.state
})
}