src/Pure/System/build.scala
changeset 48352 7fbf98ee265f
parent 48351 a0b95a762abb
child 48354 aa1e730c3fdd
     1.1 --- a/src/Pure/System/build.scala	Thu Jul 19 16:09:48 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Thu Jul 19 19:12:58 2012 +0200
     1.3 @@ -83,8 +83,6 @@
     1.4  
     1.5    /* parsing */
     1.6  
     1.7 -  val ROOT_NAME = "ROOT"
     1.8 -
     1.9    private case class Session_Entry(
    1.10      name: String,
    1.11      reset: Boolean,
    1.12 @@ -147,18 +145,9 @@
    1.13  
    1.14    /* find sessions */
    1.15  
    1.16 -  def find_sessions(more_dirs: List[Path]): Session.Queue =
    1.17 +  private def sessions_root(dir: Path, root: File, sessions: Session.Queue): Session.Queue =
    1.18    {
    1.19 -    var sessions = Session.Queue.empty
    1.20 -
    1.21 -    for {
    1.22 -      (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true))
    1.23 -      root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
    1.24 -      _ = (strict && !root.isFile && error("Bad session root file: " + quote(root.toString)))
    1.25 -      if root.isFile
    1.26 -      entry <- Parser.parse_entries(root)
    1.27 -    }
    1.28 -    {
    1.29 +    (sessions /: Parser.parse_entries(root))((sessions1, entry) =>
    1.30        try {
    1.31          if (entry.name == "") error("Bad session name")
    1.32  
    1.33 @@ -169,7 +158,7 @@
    1.34            }
    1.35            else
    1.36              entry.parent match {
    1.37 -              case Some(parent_name) if sessions.defined(parent_name) =>
    1.38 +              case Some(parent_name) if sessions1.defined(parent_name) =>
    1.39                  if (entry.reset) entry.name
    1.40                  else parent_name + "-" + entry.name
    1.41                case _ => error("Bad parent session")
    1.42 @@ -185,14 +174,52 @@
    1.43          val info = Session.Info(dir + path, entry.description, entry.options,
    1.44            entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
    1.45  
    1.46 -        sessions += (key, info, entry.parent)
    1.47 +        sessions1 + (key, info, entry.parent)
    1.48        }
    1.49        catch {
    1.50          case ERROR(msg) =>
    1.51            error(msg + "\nThe error(s) above occurred in session entry " +
    1.52              quote(entry.name) + " (file " + quote(root.toString) + ")")
    1.53 +      })
    1.54 +  }
    1.55 +
    1.56 +  private def sessions_dir(strict: Boolean, dir: Path, sessions: Session.Queue): Session.Queue =
    1.57 +  {
    1.58 +    val root = Isabelle_System.platform_file(dir + Path.basic("ROOT"))
    1.59 +    if (root.isFile) sessions_root(dir, root, sessions)
    1.60 +    else if (strict) error("Bad session root file: " + quote(root.toString))
    1.61 +    else sessions
    1.62 +  }
    1.63 +
    1.64 +  private def sessions_catalog(dir: Path, catalog: File, sessions: Session.Queue): Session.Queue =
    1.65 +  {
    1.66 +    val dirs = split_lines(Standard_System.read_file(catalog)).filter(_ != "")
    1.67 +    (sessions /: dirs)((sessions1, dir1) =>
    1.68 +      try {
    1.69 +        val dir2 = dir + Path.explode(dir1)
    1.70 +        if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, sessions1)
    1.71 +        else error("Bad session directory: " + dir2.toString)
    1.72        }
    1.73 +      catch {
    1.74 +        case ERROR(msg) =>
    1.75 +          error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
    1.76 +      })
    1.77 +  }
    1.78 +
    1.79 +  def find_sessions(more_dirs: List[Path]): Session.Queue =
    1.80 +  {
    1.81 +    var sessions = Session.Queue.empty
    1.82 +
    1.83 +    for (dir <- Isabelle_System.components()) {
    1.84 +      sessions = sessions_dir(false, dir, sessions)
    1.85 +
    1.86 +      val catalog = Isabelle_System.platform_file(dir + Path.explode("etc/sessions"))
    1.87 +      if (catalog.isFile)
    1.88 +        sessions = sessions_catalog(dir, catalog, sessions)
    1.89      }
    1.90 +
    1.91 +    for (dir <- more_dirs) sessions = sessions_dir(true, dir, sessions)
    1.92 +
    1.93      sessions
    1.94    }
    1.95