# HG changeset patch
# User wenzelm
# Date 1597406349 -7200
# Node ID 3fa75db844f5eaa6b29d3493ccd29686904de863
# Parent  64df1e5140055a7c1b6780ac08bb3ed3e7df27e3
clarified demo functions;

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))