src/Pure/System/session_manager.scala
author wenzelm
Mon Aug 23 16:53:22 2010 +0200 (2010-08-23)
changeset 38639 f642faca303e
parent 37072 9105c8237c7a
child 43606 e1a09c2a6248
permissions -rw-r--r--
main session actor as independent thread, to avoid starvation via regular worker pool;
tuned;
wenzelm@34165
     1
/*  Title:      Pure/System/isabelle_manager.scala
wenzelm@34165
     2
    Author:     Makarius
wenzelm@34165
     3
wenzelm@34165
     4
Isabelle session manager.
wenzelm@34165
     5
*/
wenzelm@34165
     6
wenzelm@34165
     7
package isabelle
wenzelm@34165
     8
wenzelm@34165
     9
wenzelm@34165
    10
import java.io.{File, FileFilter}
wenzelm@34165
    11
wenzelm@34165
    12
wenzelm@34165
    13
class Session_Manager(system: Isabelle_System)
wenzelm@34165
    14
{
wenzelm@34165
    15
  val ROOT_NAME = "session.root"
wenzelm@34165
    16
wenzelm@34165
    17
  def is_session_file(file: File): Boolean =
wenzelm@34165
    18
    file.isFile && file.getName == ROOT_NAME
wenzelm@34165
    19
wenzelm@34165
    20
  def is_session_dir(dir: File): Boolean =
wenzelm@34165
    21
    dir.isDirectory && (new File(dir, ROOT_NAME)).isFile
wenzelm@34165
    22
wenzelm@34165
    23
wenzelm@34165
    24
  // FIXME handle (potentially cyclic) directory graph
wenzelm@37072
    25
  private def find_sessions(reverse_prefix: List[String], reverse_sessions: List[List[String]],
wenzelm@34165
    26
    dir: File): List[List[String]] =
wenzelm@34165
    27
  {
wenzelm@37072
    28
    val (reverse_prefix1, reverse_sessions1) =
wenzelm@34165
    29
      if (is_session_dir(dir)) {
wenzelm@34165
    30
        val name = dir.getName  // FIXME from root file
wenzelm@37072
    31
        val reverse_prefix1 = name :: reverse_prefix
wenzelm@37072
    32
        val reverse_sessions1 = reverse_prefix1.reverse :: reverse_sessions
wenzelm@37072
    33
        (reverse_prefix1, reverse_sessions1)
wenzelm@34165
    34
      }
wenzelm@37072
    35
      else (reverse_prefix, reverse_sessions)
wenzelm@34165
    36
wenzelm@34165
    37
    val subdirs =
wenzelm@34165
    38
      dir.listFiles(new FileFilter { def accept(entry: File) = entry.isDirectory })
wenzelm@37072
    39
    (reverse_sessions1 /: subdirs)(find_sessions(reverse_prefix1, _, _))
wenzelm@34165
    40
  }
wenzelm@34165
    41
wenzelm@34165
    42
  def component_sessions(): List[List[String]] =
wenzelm@34165
    43
  {
wenzelm@34165
    44
    val toplevel_sessions =
wenzelm@34165
    45
      system.components().map(system.platform_file(_)).filter(is_session_dir)
wenzelm@34165
    46
    ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
wenzelm@34165
    47
  }
wenzelm@34165
    48
}