src/Pure/Admin/isabelle_cronjob.scala
changeset 64184 68e95e5b2b7d
parent 64173 85ff21510ba9
child 64186 49816908ae42
equal deleted inserted replaced
64183:c69a77e0124a 64184:68e95e5b2b7d
   143     val log_service = new Log_Service(progress)
   143     val log_service = new Log_Service(progress)
   144 
   144 
   145     File.write(main_state_file, main_start_date + " " + log_service.hostname)
   145     File.write(main_state_file, main_start_date + " " + log_service.hostname)
   146 
   146 
   147 
   147 
   148     /* parallel tasks */
   148     /* manage tasks */
       
   149 
       
   150     def sequential_tasks(tasks: List[Logger_Task])
       
   151     {
       
   152       tasks.map(task => log_service.run_task(Date.now(), task))
       
   153     }
   149 
   154 
   150     def parallel_tasks(tasks: List[Logger_Task])
   155     def parallel_tasks(tasks: List[Logger_Task])
   151     {
   156     {
   152       @tailrec def await(running: List[Task])
   157       @tailrec def join(running: List[Task])
   153       {
   158       {
   154         running.partition(_.is_finished) match {
   159         running.partition(_.is_finished) match {
   155           case (Nil, Nil) =>
   160           case (Nil, Nil) =>
   156           case (Nil, _ :: _) => Thread.sleep(500); await(running)
   161           case (Nil, _ :: _) => Thread.sleep(500); join(running)
   157           case (_ :: _, remaining) => await(remaining)
   162           case (_ :: _, remaining) => join(remaining)
   158         }
   163         }
   159       }
   164       }
   160       val start_date = Date.now()
   165       val start_date = Date.now()
   161       await(tasks.map(task => log_service.fork_task(start_date, task)))
   166       join(tasks.map(task => log_service.fork_task(start_date, task)))
   162     }
   167     }
   163 
   168 
   164 
   169 
   165     /* main */
   170     /* main */
   166 
   171