# HG changeset patch
# User wenzelm
# Date 1614806883 -3600
# Node ID 819f6033fb4ee0074253023484866399e28070d9
# Parent  ec52a1a6ed31f877637f5771efd912f91425238c
more robust error;

diff -r ec52a1a6ed31 -r 819f6033fb4e 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