1.1 --- a/src/Pure/System/build.scala	Wed Jul 18 08:44:05 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Wed Jul 18 13:43:36 2012 +0200
     1.3 @@ -60,11 +60,72 @@
     1.4  
     1.5    /* session information */
     1.6  
     1.7 +  val ROOT_NAME = "ROOT"
     1.8 +
     1.9 +  type Options = List[(String, Option[String])]
    1.10 +
    1.11    case class Session_Info(
    1.12 -    val dir: Path,
    1.13 -    val text: String)
    1.14 +    dir: Path,
    1.15 +    name: String,
    1.16 +    path: String,
    1.17 +    parent: String,
    1.18 +    alt_name: Option[String],
    1.19 +    description: String,
    1.20 +    options: Options,
    1.21 +    theories: List[(Options, String)],
    1.22 +    files: List[String])
    1.23  
    1.24 -  val ROOT_NAME = "ROOT"
    1.25 +  private object Parser extends Parse.Parser
    1.26 +  {
    1.27 +    val SESSION = "session"
    1.28 +    val IN = "in"
    1.29 +    val NAME = "name"
    1.30 +    val DESCRIPTION = "description"
    1.31 +    val OPTIONS = "options"
    1.32 +    val THEORIES = "theories"
    1.33 +    val FILES = "files"
    1.34 +
    1.35 +    val syntax =
    1.36 +      Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    1.37 +        SESSION + IN + NAME + DESCRIPTION + OPTIONS + THEORIES + FILES
    1.38 +
    1.39 +    val session_info: Parser[Session_Info] =
    1.40 +    {
    1.41 +      val session_name = atom("session name", _.is_name)
    1.42 +      val theory_name = atom("theory name", _.is_name)
    1.43 +      val file_name = atom("file name", _.is_name)
    1.44 +
    1.45 +      val option =
    1.46 +        name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
    1.47 +      val options: Parser[Options] =
    1.48 +        keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
    1.49 +
    1.50 +      val theories =
    1.51 +        keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
    1.52 +          { case _ ~ (x ~ y) => (x, y) }
    1.53 +
    1.54 +      ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
    1.55 +        (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
    1.56 +        (keyword("=") ~> session_name <~ keyword("+")) ~
    1.57 +        (opt(keyword(NAME) ~! session_name ^^ { case _ ~ x => x })) ~
    1.58 +        (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
    1.59 +        (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
    1.60 +        rep(theories) ~
    1.61 +        (keyword(FILES) ~! rep1(file_name) ^^ { case _ ~ x => x } | success(Nil)) ^^
    1.62 +          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
    1.63 +            Session_Info(Path.current, a, b getOrElse a, c, d, e, f,
    1.64 +              g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, h) }
    1.65 +    }
    1.66 +
    1.67 +    def parse_entries(source: CharSequence): List[Session_Info] =
    1.68 +    {
    1.69 +      val in = Token.reader(syntax.scan(source))
    1.70 +      parse_all(rep(session_info), in) match {
    1.71 +        case Success(result, _) => result
    1.72 +        case bad => error(bad.toString)
    1.73 +      }
    1.74 +    }
    1.75 +  }
    1.76  
    1.77    def find_sessions(): List[Session_Info] =
    1.78    {
    1.79 @@ -72,8 +133,8 @@
    1.80        dir <- Isabelle_System.components()
    1.81        root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
    1.82        if root.isFile
    1.83 -    }
    1.84 -    yield Session_Info(dir, Standard_System.read_file(root))
    1.85 +      entry <- Parser.parse_entries(Standard_System.read_file(root))
    1.86 +    } yield entry.copy(dir = dir)
    1.87    }
    1.88  }
    1.89