more robust error;
authorwenzelm
Wed, 03 Mar 2021 22:28:03 +0100
changeset 73356 819f6033fb4e
parent 73355 ec52a1a6ed31
child 73357 31d4274f32de
more robust error;
src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Wed Mar 03 21:58:29 2021 +0100
+++ b/src/Pure/System/scala.scala	Wed Mar 03 22:28:03 2021 +0100
@@ -108,8 +108,9 @@
       {
         val out = new StringWriter
         val interp = interpreter(new PrintWriter(out))
+        val marker = '\u000b'
         val ok =
-          interp.withLabel("\u0001") {
+          interp.withLabel(marker.toString) {
             if (interpret) interp.interpret(source) == Results.Success
             else (new interp.ReadEvalPrint).compile(source)
           }
@@ -117,7 +118,7 @@
 
         val Error = """(?s)^\S* error: (.*)$""".r
         val errors =
-          space_explode('\u0001', Library.strip_ansi_color(out.toString)).
+          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