1.1 --- a/src/Pure/System/build.scala	Fri Jul 27 13:01:19 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Fri Jul 27 13:08:46 2012 +0200
     1.3 @@ -24,7 +24,6 @@
     1.4      /* Info */
     1.5  
     1.6      sealed case class Info(
     1.7 -      base_name: String,
     1.8        groups: List[String],
     1.9        dir: Path,
    1.10        parent: Option[String],
    1.11 @@ -32,7 +31,7 @@
    1.12        options: Options,
    1.13        theories: List[(Options, List[Path])],
    1.14        files: List[Path],
    1.15 -      digest: SHA1.Digest)
    1.16 +      entry_digest: SHA1.Digest)
    1.17  
    1.18  
    1.19      /* Queue */
    1.20 @@ -92,7 +91,7 @@
    1.21    /* parsing */
    1.22  
    1.23    private case class Session_Entry(
    1.24 -    name: String,
    1.25 +    base_name: String,
    1.26      this_name: Boolean,
    1.27      groups: List[String],
    1.28      path: Option[String],
    1.29 @@ -162,19 +161,19 @@
    1.30    {
    1.31      (queue /: Parser.parse_entries(root))((queue1, entry) =>
    1.32        try {
    1.33 -        if (entry.name == "") error("Bad session name")
    1.34 +        if (entry.base_name == "") error("Bad session name")
    1.35  
    1.36          val full_name =
    1.37 -          if (is_pure(entry.name)) {
    1.38 +          if (is_pure(entry.base_name)) {
    1.39              if (entry.parent.isDefined) error("Illegal parent session")
    1.40 -            else entry.name
    1.41 +            else entry.base_name
    1.42            }
    1.43            else
    1.44              entry.parent match {
    1.45                case Some(parent_name) if queue1.isDefinedAt(parent_name) =>
    1.46                  val full_name =
    1.47 -                  if (entry.this_name) entry.name
    1.48 -                  else parent_name + "-" + entry.name
    1.49 +                  if (entry.this_name) entry.base_name
    1.50 +                  else parent_name + "-" + entry.base_name
    1.51                  full_name
    1.52                case _ => error("Bad parent session")
    1.53              }
    1.54 @@ -182,7 +181,7 @@
    1.55          val path =
    1.56            entry.path match {
    1.57              case Some(p) => Path.explode(p)
    1.58 -            case None => Path.basic(entry.name)
    1.59 +            case None => Path.basic(entry.base_name)
    1.60            }
    1.61  
    1.62          val session_options = options ++ entry.options
    1.63 @@ -191,18 +190,19 @@
    1.64            entry.theories.map({ case (opts, thys) =>
    1.65              (session_options ++ opts, thys.map(Path.explode(_))) })
    1.66          val files = entry.files.map(Path.explode(_))
    1.67 -        val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    1.68 +        val entry_digest =
    1.69 +          SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    1.70  
    1.71          val info =
    1.72 -          Session.Info(entry.name, entry.groups, dir + path, entry.parent,
    1.73 -            entry.description, session_options, theories, files, digest)
    1.74 +          Session.Info(entry.groups, dir + path, entry.parent, entry.description,
    1.75 +            session_options, theories, files, entry_digest)
    1.76  
    1.77          queue1 + (full_name, info)
    1.78        }
    1.79        catch {
    1.80          case ERROR(msg) =>
    1.81            error(msg + "\nThe error(s) above occurred in session entry " +
    1.82 -            quote(entry.name) + Position.str_of(Position.file(root)))
    1.83 +            quote(entry.base_name) + Position.str_of(Position.file(root)))
    1.84        })
    1.85    }
    1.86  
    1.87 @@ -450,7 +450,7 @@
    1.88      val deps = dependencies(verbose, queue)
    1.89  
    1.90      def make_stamp(name: String): String =
    1.91 -      sources_stamp(queue(name).digest :: deps.sources(name))
    1.92 +      sources_stamp(queue(name).entry_digest :: deps.sources(name))
    1.93  
    1.94      val (input_dirs, output_dir, browser_info) =
    1.95        if (system_mode) {