src/Pure/System/scala.scala

   /** registered functions **/
 
   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
   }
 
   class Functions(val functions: Fun*) extends Isabelle_System.Service
 

 
   /** demo functions **/
 
   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 =
         seconds match {
           case Value.Double(s) => Time.seconds(s)

     }
   }
 
   object Toplevel extends Fun("scala_toplevel")
   {
+    val here = Scala_Project.here
     def apply(arg: String): String =
     {
       val (interpret, source) =
         YXML.parse_body(arg) match {
           case Nil => (false, "")