src/Pure/System/scala.scala
changeset 72756 72ac27ea12b2
parent 72332 319dd5c618a5
child 72760 042180540068
--- 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) =