src/Pure/System/build.scala
changeset 48339 62570361e608
parent 48337 9c7f8e5805b4
child 48340 6f4fc030882a
equal deleted inserted replaced
48338:3592a2091c80 48339:62570361e608
   164           infos.find(_.name == entry.parent) getOrElse
   164           infos.find(_.name == entry.parent) getOrElse
   165            error("Unknown parent session: " + quote(entry.parent))
   165            error("Unknown parent session: " + quote(entry.parent))
   166         val full_name =
   166         val full_name =
   167           if (entry.reset) entry.name
   167           if (entry.reset) entry.name
   168           else parent.name + "-" + entry.name
   168           else parent.name + "-" + entry.name
       
   169 
       
   170         if (entry.name == "") error("Bad session name")
       
   171         if (infos.exists(_.name == full_name))
       
   172           error("Duplicate session name: " + quote(full_name))
       
   173 
   169         val path =
   174         val path =
   170           entry.path match {
   175           entry.path match {
   171             case Some(p) => Path.explode(p)
   176             case Some(p) => Path.explode(p)
   172             case None => Path.basic(entry.name)
   177             case None => Path.basic(entry.name)
   173           }
   178           }
   174         val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
   179         val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
   175         val info =
   180         val info =
   176           Session_Info(dir + path, full_name, entry.parent, entry.description,
   181           Session_Info(dir + path, full_name, entry.parent, entry.description,
   177             entry.options, thys, entry.files)
   182             entry.options, thys, entry.files)
       
   183 
   178         infos += info
   184         infos += info
   179       }
   185       }
   180       catch {
   186       catch {
   181         case ERROR(msg) =>
   187         case ERROR(msg) =>
   182           error(msg + "\nThe error(s) above occurred in session entry " +
   188           error(msg + "\nThe error(s) above occurred in session entry " +