/
Log.scala
333 lines (277 loc) · 10.3 KB
/
Log.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
package info.kwarc.mmt.api.frontend
import java.io.IOException
import info.kwarc.mmt.api._
import utils._
/** extended by all classes that use the logging aspect */
trait Logger {
// fields are defs not vals to avoid surprises during instantiation/inheritance
protected def report: Report
def logPrefix: String
/** logs a message with this logger's logprefix */
protected def log(s: => String, subgroup: Option[String] = None): Unit =
report(logPrefix + subgroup.map("-" + _).getOrElse(""), s)
/** temporary logging - always logged */
// calls to this method are for debugging; if they are committed, they should be removed
protected def logTemp(s: => String): Unit =
report("temp", s"($logPrefix) $s")
/** log as an error message */
protected def logError(s: => String): Unit = report("error", s"($logPrefix) $s")
/** logs an error - always logged */
protected def log(e: Error): Unit = report(e)
/** wraps around a group to create nested logging */
protected def logGroup[A](a: => A): A = {
report.indent
try {
a
} finally {
report.unindent
}
}
}
/** Instances of Report handle all output to the user */
class Report extends Logger {
val logPrefix = "report"
val report = this
/** output is categorized, the elements of group determine which categories are considered
* the categories "user" (for user input), "error" are output by default, and "temp" (for temporary logging during debugging) */
private[mmt] val groups = scala.collection.mutable.Set[String]("user", "error", "temp", "response")
/** true if debug logging is enabled */
def checkDebug = groups contains "debug"
private var counter = -1
private def nextId = {counter += 1; counter}
/** this does nothing and should only be called during debugging:
* it provides a convenient way to hit a breakpoint at a specific call to "log"
* to use, set a breakpoint in this method and call "breakOnId(i)" after the call to "log" at which you want to break
*/
def breakOnId(id: Int): Unit = {
if (id <= counter)
return
}
/** gets a list of active groups */
def active : List[String] = groups.toList
/** logs a message if logging is switched on for the group */
def apply(prefix: => String, msg: => String): Unit = {
lazy val caller = {
val s = Thread.currentThread.getStackTrace
//TODO this is not always the most helpful entry
var i = s.lastIndexWhere(e => e.getMethodName == "log")
if (i == -1) i = 0
s(i+1).toString
}
val prefixList = utils.stringToList(prefix, "#")
if (prefixList.forall(p => groups.contains(p)) || groups.contains("all")) {
var msgParts = utils.stringToList(msg, "\\n")
if (checkDebug) {
val id = nextId
val (hd,tl) = msgParts match {
case Nil => ("",Nil)
case h::t => (h,t)
}
msgParts = (hd + s" [message id: $id]") :: tl
}
handlers.foreach(_.apply(ind, caller, prefix, msgParts))
}
}
/** logs an error */
def apply(e: Error): Unit = {
val debug = checkDebug
if (groups.contains("error") || debug)
handlers.foreach(_.apply(ind, e, debug))
}
/** flushes all handlers */
def flush: Unit = {
handlers.foreach(_.flush)
}
/** closes all handlers */
def cleanup: Unit = {
handlers.foreach(_.cleanup)
}
/** the registered handlers */
private var handlers: List[ReportHandler] = Nil
/** adds a ReportHandler */
def addHandler(h: ReportHandler): Unit = {
log("logging to " + h)
h.init
handlers = (handlers ::: List(h)).distinct
}
/** removes all ReportHandlers with a certain id */
def removeHandler(id: String): Unit = {
handlers = handlers.filter(_.id != id)
}
/** the current indentation level */
private var ind = 0
/** increase indentation */
private[frontend] def indent: Unit = {
ind += 1
}
/** decrease indentation */
private[frontend] def unindent: Unit = {
if (ind >= 1) ind -= 1
}
/** enables logging for a set of groups within a block */
def withGroups[A](groups: String*)(a: => A): A = {
val theGroups = groups.filterNot(this.groups.contains) // the groups that we did not have beforehand
theGroups.foreach(this.groups += _)
try {
a
} finally {
theGroups.foreach(this.groups -= _)
}
}
}
object Report {
val df = new java.text.SimpleDateFormat("HH:mm:ss.S")
}
/**
* takes a log message from [[Report]] and displays/stores etc. it
*
* @param id an identifier for this handler
*/
abstract class ReportHandler(val id: String) {
/**
* logs a message
*
* @param ind indentation level
* @param group generating component
* @param msgParts the multi-line message
*/
def apply(ind: Int, caller: => String, group: String, msgParts: List[String]): Unit
/** logs as an error (categories "error" and "debug" for short and long message, respectively) */
def apply(ind: Int, e: Error, debug: Boolean): Unit = {
val caller = e.getStackTrace()(0).toString
val (msg,content) = e match {
case _: ContentError => (contentErrorHighlight(e.shortMsg), e.getCausedBy.isEmpty)
case _ => (systemErrorHighlight(e.shortMsg), false)
}
apply(ind, caller, "error", List(s"(${e.levelString}) " + msg))
if (debug && !content) {
apply(ind, caller, "debug", utils.stringToList(e.toStringLong, "\\n"))
}
}
def systemErrorHighlight(s: String): String = s
def contentErrorHighlight(s: String): String = s
/** produces a timestamp */
def time: String = Report.df.format(new java.util.Date())
/** turns indentation level into a string of spaces */
def indentString(i: Int): String = Range(0, i).map(_ => " ").mkString("")
/** flushes the handler, nothing by default */
def flush: Unit = {}
/** initializes the handler, nothing by default */
def init: Unit = {}
/** closes the handler, nothing by default */
def cleanup: Unit = {}
/** returns the id */
override def toString: String = id
}
/** outputs to standard output */
object ConsoleHandler extends ReportHandler("console") {
def apply(ind: Int, caller: => String, group: String, msgParts: List[String]): Unit = {
msgParts.foreach { msg =>
val m = indentString(ind) + group + ": " + msg
println(m)
}
}
/* see http://mihai-nita.net/2013/06/03/eclipse-plugin-ansi-in-console/ for ANSI escape codes
* e.g., 30-37: colors, 1 bold, 3 italic, 0 reset
*/
override def systemErrorHighlight(s: String): String = "\u001b[31;1m" + s + "\u001b[0m"
override def contentErrorHighlight(s: String): String = "\u001b[34;103m" + s + "\u001b[0m"
}
/** common methods for logging to a file */
abstract class FileHandler(val filename: File) extends ReportHandler(filename.toString) {
protected val file = utils.File.Writer(filename)
protected var alreadyClosed = false
override def flush: Unit = {
file.flush
}
override def cleanup: Unit = {
if (!alreadyClosed) {
file.close
alreadyClosed = true
}
}
}
/** outputs to a file */
class TextFileHandler(filename: File, timestamps: Boolean) extends FileHandler(filename) {
def apply(ind: Int, caller: => String, group: String, msgParts: List[String]): Unit = {
val t = if (timestamps) time + "\t" else ""
msgParts.foreach { msg =>
val m = t + indentString(ind) + group + ": " + msg
file.println(m)
}
flush
}
override def toString: String = "file " + filename
}
/** outputs to a file in html syntax */
class HtmlFileHandler(filename: File) extends FileHandler(filename) {
override def init: Unit = {
super.init
val scrfile = filename.up / "logaux" / "script.js"
val jqfile = filename.up / "logaux" / "jquery.js"
val cssfile = filename.up / "logaux" / "style.css"
if (!scrfile.exists) File.write(scrfile,MMTSystem.getResourceAsString("/log-html/script.js"))
if (!jqfile.exists) File.write(jqfile,MMTSystem.getResourceAsString("/mmt-web/script/jquery/jquery.js"))
if (!cssfile.exists) File.write(cssfile,MMTSystem.getResourceAsString("/log-html/style.css"))
val script = """<script type="text/javascript" src="logaux/script.js"></script>"""
val jquery = "<script type=\"text/javascript\" src=" +
"\"logaux/jquery.js\"></script>"
val css = """<link rel="stylesheet" type="text/css" href="logaux/style.css"></link>"""
val pref = """<!DOCTYPE html><html><head><meta charset="UTF-8">"""
file.println(s"$pref\n$jquery$script$css</head><body>\n")
}
def apply(ind: Int, caller: => String, group: String, msgParts: List[String]): Unit = {
file.println( s"""<div class="log $group" style="margin-left: $ind%">""")
file.println( s"""<div><span class="timestamp">$time</span><span class="caller">$caller</span></div>""")
val msg = msgParts.mkString("<br/>")
file.println( s"""<div><span class="group">$group:</span><span class="message">$msg</span></div>""")
file.println("</div>")
flush
}
override def apply(ind: Int, e: Error, debug: Boolean): Unit = {
val (cls,refO) = e match {
case e: ContentError => ("content-error", e.sourceRef)
case _ => ("error", None)
}
file.println( s"""<div class="log $cls" style="margin-left: $ind%">""")
file.println( s"""<div><span class="timestamp">$time</span><span class="error-short">${e.shortMsg}</span></div>""")
refO.foreach {ref =>
file.println(s"""<div class="sourceref"><span class="sourceref" data-mmt-ref="${ref.toString}">${ref.toString}</span></div>""")
}
if (debug) {
e.toStringLong.split("\\n").toList.foreach { line =>
file.println( s"""<div class="error-long"><span>$line</span></div>""")
}
}
file.println("</div>")
}
override def toString: String = "html " + filename
override def cleanup: Unit = {
if (!alreadyClosed) {
file.println("</body>\n</html>\n")
super.cleanup
}
}
}
/** remembers logged lines */
class RecordingHandler(id: String) extends ReportHandler(id) {
private var memory: List[String] = Nil
private var recording = false
def record: Unit = {
recording = true
}
def stop: List[String] = {
recording = false
memory.reverse
}
def clear: Unit = {
memory = Nil
}
def apply(ind: Int, caller: => String, group: String, msgParts: List[String]): Unit = {
if (recording) {
msgParts.foreach { msg =>
memory ::= indentString(ind) + group + ": " + msg
}
}
}
}