Initial release.

1 files changed, 48 insertions, 0 deletions

diff --git a/sources/scala/Executable.scala b/sources/scala/Executable.scala
new file mode 100644
index 0000000000..651d5d136d
--- /dev/null
+++ b/sources/scala/Executable.scala
@@ -0,0 +1,48 @@
+/*                     __                                               *\
+**     ________ ___   / /  ___     Scala API                            **
+**    / __/ __// _ | / /  / _ |    (c) 2002, LAMP/EPFL                  **
+**  __\ \/ /__/ __ |/ /__/ __ |                                         **
+** /____/\___/_/ |_/____/_/ | |                                         **
+**                          |/                                          **
+\*                                                                      */
+
+package scala;
+
+
+/** The <code>Executable</code> class can be used to quickly turn objects
+ *  into executable programs. Here is an example:
+ *  <pre>
+ *  object Main with Executable {
+ *    Console.println("Hello World!");
+ *  }
+ *  </pre>
+ *  Here, object <code>Main</code> inherits the <code>main</code> method
+ *  of <code>Executable</code>. The body of the <code>Main</code> object
+ *  defines the main program. This technique does not work if the main
+ *  program depends on command-line arguments (which are not accessible
+ *  with the technique presented here).
+ *
+ *  It is possible to time the execution of objects that inherit from
+ *  class <code>Executable</code> by setting the global scala.time property.
+ *  Here is an example for benchmarking object <code>Main</code>:
+ *  <pre>
+ *  java -Dscala.time Main
+ *  </pre>
+ *
+ *  @author  Matthias Zenger
+ *  @version 1.0, 10/09/03
+ */
+class Executable {
+
+    /** The time when execution of this program started.
+     */
+	val executionStart: Long = System.currentTimeMillis();
+
+	/** The default main method.
+	 */
+    def main(args: Array[String]) = {
+    	if (System.getProperty("scala.time") != null)
+    		System.out.println("[total " +
+    			(System.currentTimeMillis() - executionStart) + "ms]");
+    }
+}