clarified logs;
authorwenzelm
Sat Oct 15 11:26:31 2016 +0200 (2016-10-15)
changeset 64219c1af670cbe7e
parent 64218 f318cb6ba511
child 64220 e7cbf81ec4b7
clarified logs;
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 15 11:18:46 2016 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 15 11:26:31 2016 +0200
     1.3 @@ -17,7 +17,8 @@
     1.4  
     1.5    val main_dir = Path.explode("~/cronjob")
     1.6    val main_state_file = main_dir + Path.explode("run/main.state")
     1.7 -  val main_log = main_dir + Path.explode("log/main.log")  // owned by log service
     1.8 +  val current_log = main_dir + Path.explode("run/main.log")  // owned by log service
     1.9 +  val cumulative_log = main_dir + Path.explode("log/main.log")  // owned by log service
    1.10  
    1.11    val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
    1.12    val afp_repos = main_dir + Path.explode("AFP-build_history")
    1.13 @@ -91,11 +92,14 @@
    1.14  
    1.15    class Log_Service private[Isabelle_Cronjob](progress: Progress)
    1.16    {
    1.17 +    current_log.file.delete
    1.18 +
    1.19      private val thread: Consumer_Thread[String] =
    1.20        Consumer_Thread.fork("cronjob: logger", daemon = true)(
    1.21          consume = (text: String) =>
    1.22 -          {
    1.23 -            File.append(main_log, text + "\n")   // critical
    1.24 +          { // critical
    1.25 +            File.append(current_log, text + "\n")
    1.26 +            File.append(cumulative_log, text + "\n")
    1.27              progress.echo(text)
    1.28              true
    1.29            })