--- a/src/Pure/System/scala.scala Sat Aug 22 20:32:44 2020 +0200
+++ b/src/Pure/System/scala.scala Sat Aug 22 20:37:31 2020 +0200
@@ -116,16 +116,16 @@
if (!ok && errors.isEmpty) List("Error") else errors
}
}
+ }
- object Toplevel extends Fun("scala_toplevel")
+ object Toplevel extends Fun("scala_toplevel")
+ {
+ def apply(source: String): String =
{
- def apply(source: String): String =
- {
- val errors =
- try { Compiler.context().toplevel(source) }
- catch { case ERROR(msg) => List(msg) }
- locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
- }
+ val errors =
+ try { Compiler.context().toplevel(source) }
+ catch { case ERROR(msg) => List(msg) }
+ locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
}
}
@@ -221,5 +221,5 @@
class Scala_Functions extends Scala.Functions(
Scala.Echo,
Scala.Sleep,
- Scala.Compiler.Toplevel,
- Bibtex.Check)
+ Scala.Toplevel,
+ Bibtex.Check_Database)