equal
deleted
inserted
replaced
|
1 /* Title: Tools/VSCode/src/logger.scala |
|
2 Author: Makarius |
|
3 |
|
4 Minimal logging support. |
|
5 */ |
|
6 |
|
7 package isabelle.vscode |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 |
|
13 object Logger |
|
14 { |
|
15 def make(log_file: Option[Path]): Logger = |
|
16 log_file match { case Some(file) => new File_Logger(file) case None => No_Logger } |
|
17 } |
|
18 |
|
19 trait Logger |
|
20 { |
|
21 def apply(msg: => String): Unit |
|
22 } |
|
23 |
|
24 object No_Logger extends Logger |
|
25 { |
|
26 def apply(msg: => String) { } |
|
27 } |
|
28 |
|
29 class File_Logger(path: Path) extends Logger |
|
30 { |
|
31 def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } } |
|
32 |
|
33 override def toString: String = path.toString |
|
34 } |