# HG changeset patch # User wenzelm # Date 1482176775 -3600 # Node ID a871fa7c24fcb5fa51782205116eed4e20d8bc05 # Parent 9c1173a7e4cbbd976193f676d9f24dd0f84d0098 clarified modules; diff -r 9c1173a7e4cb -r a871fa7c24fc 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 +} diff -r 9c1173a7e4cb -r a871fa7c24fc src/Pure/build-jars --- a/src/Pure/build-jars Mon Dec 19 20:27:49 2016 +0100 +++ b/src/Pure/build-jars Mon Dec 19 20:46:15 2016 +0100 @@ -49,6 +49,7 @@ General/http_server.scala General/json.scala General/linear_set.scala + General/logger.scala General/long_name.scala General/mercurial.scala General/multi_map.scala @@ -156,7 +157,6 @@ "../Tools/VSCode/src/channel.scala" "../Tools/VSCode/src/document_model.scala" "../Tools/VSCode/src/line.scala" - "../Tools/VSCode/src/logger.scala" "../Tools/VSCode/src/protocol.scala" "../Tools/VSCode/src/server.scala" "../Tools/VSCode/src/uri_resources.scala" diff -r 9c1173a7e4cb -r a871fa7c24fc src/Tools/VSCode/src/logger.scala --- a/src/Tools/VSCode/src/logger.scala Mon Dec 19 20:27:49 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -/* Title: Tools/VSCode/src/logger.scala - Author: Makarius - -Minimal logging support. -*/ - -package isabelle.vscode - - -import 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 -}