src/Pure/General/logger.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/logger.scala	Mon Dec 19 20:46:15 2016 +0100
@@ -0,0 +1,31 @@
+/*  Title:      Pure/General/logger.scala
+    Author:     Makarius
+
+Minimal logging support.
+*/
+
+package isabelle
+
+
+object Logger
+{
+  def make(log_file: Option[Path]): Logger =
+    log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }
+}
+
+trait Logger
+{
+  def apply(msg: => String): Unit
+}
+
+object No_Logger extends Logger
+{
+  def apply(msg: => String) { }
+}
+
+class File_Logger(path: Path) extends Logger
+{
+  def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } }
+
+  override def toString: String = path.toString
+}