1.1 --- a/src/Pure/System/build.scala	Fri Jul 20 11:46:37 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Fri Jul 20 11:52:20 2012 +0200
     1.3 @@ -145,9 +145,12 @@
     1.4  
     1.5    /* find sessions */
     1.6  
     1.7 -  private def sessions_root(dir: Path, root: File, sessions: Session.Queue): Session.Queue =
     1.8 +  private val ROOT = Path.explode("ROOT")
     1.9 +  private val SESSIONS = Path.explode("etc/sessions")
    1.10 +
    1.11 +  private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
    1.12    {
    1.13 -    (sessions /: Parser.parse_entries(root))((sessions1, entry) =>
    1.14 +    (queue /: Parser.parse_entries(root))((queue1, entry) =>
    1.15        try {
    1.16          if (entry.name == "") error("Bad session name")
    1.17  
    1.18 @@ -158,7 +161,7 @@
    1.19            }
    1.20            else
    1.21              entry.parent match {
    1.22 -              case Some(parent_name) if sessions1.defined(parent_name) =>
    1.23 +              case Some(parent_name) if queue1.defined(parent_name) =>
    1.24                  if (entry.reset) entry.name
    1.25                  else parent_name + "-" + entry.name
    1.26                case _ => error("Bad parent session")
    1.27 @@ -174,7 +177,7 @@
    1.28          val info = Session.Info(dir + path, entry.description, entry.options,
    1.29            entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
    1.30  
    1.31 -        sessions1 + (key, info, entry.parent)
    1.32 +        queue1 + (key, info, entry.parent)
    1.33        }
    1.34        catch {
    1.35          case ERROR(msg) =>
    1.36 @@ -183,23 +186,23 @@
    1.37        })
    1.38    }
    1.39  
    1.40 -  private def sessions_dir(strict: Boolean, dir: Path, sessions: Session.Queue): Session.Queue =
    1.41 +  private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
    1.42    {
    1.43 -    val root = Isabelle_System.platform_file(dir + Path.basic("ROOT"))
    1.44 -    if (root.isFile) sessions_root(dir, root, sessions)
    1.45 +    val root = Isabelle_System.platform_file(dir + ROOT)
    1.46 +    if (root.isFile) sessions_root(dir, root, queue)
    1.47      else if (strict) error("Bad session root file: " + quote(root.toString))
    1.48 -    else sessions
    1.49 +    else queue
    1.50    }
    1.51  
    1.52 -  private def sessions_catalog(dir: Path, catalog: File, sessions: Session.Queue): Session.Queue =
    1.53 +  private def sessions_catalog(dir: Path, catalog: File, queue: Session.Queue): Session.Queue =
    1.54    {
    1.55      val dirs =
    1.56        split_lines(Standard_System.read_file(catalog)).
    1.57          filterNot(line => line == "" || line.startsWith("#"))
    1.58 -    (sessions /: dirs)((sessions1, dir1) =>
    1.59 +    (queue /: dirs)((queue1, dir1) =>
    1.60        try {
    1.61          val dir2 = dir + Path.explode(dir1)
    1.62 -        if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, sessions1)
    1.63 +        if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, queue1)
    1.64          else error("Bad session directory: " + dir2.toString)
    1.65        }
    1.66        catch {
    1.67 @@ -210,19 +213,19 @@
    1.68  
    1.69    def find_sessions(more_dirs: List[Path]): Session.Queue =
    1.70    {
    1.71 -    var sessions = Session.Queue.empty
    1.72 +    var queue = Session.Queue.empty
    1.73  
    1.74      for (dir <- Isabelle_System.components()) {
    1.75 -      sessions = sessions_dir(false, dir, sessions)
    1.76 +      queue = sessions_dir(false, dir, queue)
    1.77  
    1.78 -      val catalog = Isabelle_System.platform_file(dir + Path.explode("etc/sessions"))
    1.79 +      val catalog = Isabelle_System.platform_file(dir + SESSIONS)
    1.80        if (catalog.isFile)
    1.81 -        sessions = sessions_catalog(dir, catalog, sessions)
    1.82 +        queue = sessions_catalog(dir, catalog, queue)
    1.83      }
    1.84  
    1.85 -    for (dir <- more_dirs) sessions = sessions_dir(true, dir, sessions)
    1.86 +    for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
    1.87  
    1.88 -    sessions
    1.89 +    queue
    1.90    }
    1.91  
    1.92