# 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