src/Pure/System/build.scala
changeset 48336 3c55bfad22eb
parent 48335 2f923e994056
child 48337 9c7f8e5805b4
     1.1 --- a/src/Pure/System/build.scala	Wed Jul 18 14:07:31 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Wed Jul 18 16:24:16 2012 +0200
     1.3 @@ -73,9 +73,8 @@
     1.4    case class Session_Info(
     1.5      dir: Path,
     1.6      name: String,
     1.7 -    path: String,
     1.8 +    reset_name: Boolean,
     1.9      parent: String,
    1.10 -    alt_name: Option[String],
    1.11      description: String,
    1.12      options: Options,
    1.13      theories: List[(Options, String)],
    1.14 @@ -85,21 +84,19 @@
    1.15    {
    1.16      val SESSION = "session"
    1.17      val IN = "in"
    1.18 -    val NAME = "name"
    1.19      val DESCRIPTION = "description"
    1.20      val OPTIONS = "options"
    1.21      val THEORIES = "theories"
    1.22      val FILES = "files"
    1.23  
    1.24      val syntax =
    1.25 -      Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    1.26 -        SESSION + IN + NAME + DESCRIPTION + OPTIONS + THEORIES + FILES
    1.27 +      Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    1.28 +        SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
    1.29  
    1.30      def session_info(dir: Path): Parser[Session_Info] =
    1.31      {
    1.32        val session_name = atom("session name", _.is_name)
    1.33        val theory_name = atom("theory name", _.is_name)
    1.34 -      val file_name = atom("file name", _.is_name)
    1.35  
    1.36        val option =
    1.37          name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
    1.38 @@ -111,16 +108,17 @@
    1.39            { case _ ~ (x ~ y) => (x, y) }
    1.40  
    1.41        ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
    1.42 -        (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
    1.43 +        (keyword("!") ^^^ true | success(false)) ~
    1.44 +        (opt(keyword(IN) ~! string ^^ { case _ ~ x => Path.explode(x) })) ~
    1.45          (keyword("=") ~> session_name <~ keyword("+")) ~
    1.46 -        (opt(keyword(NAME) ~! session_name ^^ { case _ ~ x => x })) ~
    1.47          (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
    1.48          (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
    1.49          rep(theories) ~
    1.50 -        (keyword(FILES) ~! rep1(file_name) ^^ { case _ ~ x => x } | success(Nil)) ^^
    1.51 +        (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
    1.52            { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
    1.53 -            Session_Info(dir, a, b getOrElse a, c, d, e, f,
    1.54 -              g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, h) }
    1.55 +              val dir1 = dir + c.getOrElse(Path.basic(a))
    1.56 +              val thys = g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
    1.57 +              Session_Info(dir1, a, b, d, e, f, thys, h) }
    1.58      }
    1.59  
    1.60      def parse_entries(dir: Path, root: File): List[Session_Info] =