diff -r 64df1e514005 -r 3fa75db844f5 src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Fri Aug 14 13:26:12 2020 +0200 +++ b/src/Pure/System/scala.scala Fri Aug 14 13:59:09 2020 +0200 @@ -15,6 +15,25 @@ object Scala { + /** demo functions **/ + + def echo(arg: String): String = arg + + def sleep(seconds: String): String = + { + val t = + seconds match { + case Value.Double(s) => Time.seconds(s) + case _ => error("Malformed argument: " + quote(seconds)) + } + val t0 = Time.now() + t.sleep + val t1 = Time.now() + (t1 - t0).toString + } + + + /** compiler **/ object Compiler @@ -192,6 +211,7 @@ class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service class Functions extends Isabelle_Scala_Functions( - Scala.Fun("echo", identity), + Scala.Fun("echo", Scala.echo), + Scala.Fun("sleep", Scala.sleep), Scala.Fun("scala_toplevel", Scala.toplevel_yxml), Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))