src/Pure/Admin/isabelle_cronjob.scala
changeset 64219 c1af670cbe7e
parent 64218 f318cb6ba511
child 64220 e7cbf81ec4b7
equal deleted inserted replaced
64218:f318cb6ba511 64219:c1af670cbe7e
    15 {
    15 {
    16   /* file-system state: owned by main cronjob */
    16   /* file-system state: owned by main cronjob */
    17 
    17 
    18   val main_dir = Path.explode("~/cronjob")
    18   val main_dir = Path.explode("~/cronjob")
    19   val main_state_file = main_dir + Path.explode("run/main.state")
    19   val main_state_file = main_dir + Path.explode("run/main.state")
    20   val main_log = main_dir + Path.explode("log/main.log")  // owned by log service
    20   val current_log = main_dir + Path.explode("run/main.log")  // owned by log service
       
    21   val cumulative_log = main_dir + Path.explode("log/main.log")  // owned by log service
    21 
    22 
    22   val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
    23   val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
    23   val afp_repos = main_dir + Path.explode("AFP-build_history")
    24   val afp_repos = main_dir + Path.explode("AFP-build_history")
    24 
    25 
    25   val release_snapshot = Path.explode("~/html-data/release_snapshot")
    26   val release_snapshot = Path.explode("~/html-data/release_snapshot")
    89 
    90 
    90   sealed case class Logger_Task(name: String = "", body: Logger => Unit)
    91   sealed case class Logger_Task(name: String = "", body: Logger => Unit)
    91 
    92 
    92   class Log_Service private[Isabelle_Cronjob](progress: Progress)
    93   class Log_Service private[Isabelle_Cronjob](progress: Progress)
    93   {
    94   {
       
    95     current_log.file.delete
       
    96 
    94     private val thread: Consumer_Thread[String] =
    97     private val thread: Consumer_Thread[String] =
    95       Consumer_Thread.fork("cronjob: logger", daemon = true)(
    98       Consumer_Thread.fork("cronjob: logger", daemon = true)(
    96         consume = (text: String) =>
    99         consume = (text: String) =>
    97           {
   100           { // critical
    98             File.append(main_log, text + "\n")   // critical
   101             File.append(current_log, text + "\n")
       
   102             File.append(cumulative_log, text + "\n")
    99             progress.echo(text)
   103             progress.echo(text)
   100             true
   104             true
   101           })
   105           })
   102 
   106 
   103     def shutdown() { thread.shutdown() }
   107     def shutdown() { thread.shutdown() }