--- a/src/Pure/System/scala.scala Sat Nov 28 15:15:53 2020 +0100
+++ b/src/Pure/System/scala.scala Sat Nov 28 15:17:14 2020 +0100
@@ -20,6 +20,8 @@
abstract class Fun(val name: String) extends Function[String, String]
{
override def toString: String = name
+ def position: Properties.T = here.position
+ def here: Scala_Project.Here
def apply(arg: String): String
}
@@ -34,11 +36,13 @@
object Echo extends Fun("echo")
{
+ val here = Scala_Project.here
def apply(arg: String): String = arg
}
object Sleep extends Fun("sleep")
{
+ val here = Scala_Project.here
def apply(seconds: String): String =
{
val t =
@@ -123,6 +127,7 @@
object Toplevel extends Fun("scala_toplevel")
{
+ val here = Scala_Project.here
def apply(arg: String): String =
{
val (interpret, source) =