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