cumulate semantic Session_Info, based on syntactic Session_Entry;
authorwenzelm
Wed Jul 18 17:17:38 2012 +0200 (2012-07-18)
changeset 483379c7f8e5805b4
parent 48336 3c55bfad22eb
child 48338 3592a2091c80
cumulate semantic Session_Info, based on syntactic Session_Entry;
tuned errors;
src/Pure/System/build.scala
     1.1 --- a/src/Pure/System/build.scala	Wed Jul 18 16:24:16 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Wed Jul 18 17:17:38 2012 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  
     1.5  import java.io.File
     1.6  
     1.7 +import scala.collection.mutable
     1.8 +
     1.9  
    1.10  object Build
    1.11  {
    1.12 @@ -64,22 +66,37 @@
    1.13    }
    1.14  
    1.15  
    1.16 -  /* session information */
    1.17 -
    1.18 -  val ROOT_NAME = "ROOT"
    1.19 +  /** session information **/
    1.20  
    1.21    type Options = List[(String, Option[String])]
    1.22  
    1.23    case class Session_Info(
    1.24      dir: Path,
    1.25      name: String,
    1.26 -    reset_name: Boolean,
    1.27      parent: String,
    1.28      description: String,
    1.29      options: Options,
    1.30      theories: List[(Options, String)],
    1.31      files: List[String])
    1.32  
    1.33 +  private val pure_info =
    1.34 +    Session_Info(Path.current, "Pure", "", "", Nil, List((Nil, "Pure")), Nil)
    1.35 +
    1.36 +
    1.37 +  /* parsing */
    1.38 +
    1.39 +  val ROOT_NAME = "ROOT"
    1.40 +
    1.41 +  private case class Session_Entry(
    1.42 +    name: String,
    1.43 +    reset: Boolean,
    1.44 +    path: Option[String],
    1.45 +    parent: String,
    1.46 +    description: String,
    1.47 +    options: Options,
    1.48 +    theories: List[(Options, List[String])],
    1.49 +    files: List[String])
    1.50 +
    1.51    private object Parser extends Parse.Parser
    1.52    {
    1.53      val SESSION = "session"
    1.54 @@ -93,15 +110,14 @@
    1.55        Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    1.56          SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
    1.57  
    1.58 -    def session_info(dir: Path): Parser[Session_Info] =
    1.59 +    val session_entry: Parser[Session_Entry] =
    1.60      {
    1.61        val session_name = atom("session name", _.is_name)
    1.62        val theory_name = atom("theory name", _.is_name)
    1.63  
    1.64        val option =
    1.65          name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
    1.66 -      val options: Parser[Options] =
    1.67 -        keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
    1.68 +      val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
    1.69  
    1.70        val theories =
    1.71          keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
    1.72 @@ -109,36 +125,65 @@
    1.73  
    1.74        ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
    1.75          (keyword("!") ^^^ true | success(false)) ~
    1.76 -        (opt(keyword(IN) ~! string ^^ { case _ ~ x => Path.explode(x) })) ~
    1.77 +        (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
    1.78          (keyword("=") ~> session_name <~ keyword("+")) ~
    1.79          (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
    1.80          (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
    1.81 -        rep(theories) ~
    1.82 +        rep1(theories) ~
    1.83          (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
    1.84 -          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
    1.85 -              val dir1 = dir + c.getOrElse(Path.basic(a))
    1.86 -              val thys = g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
    1.87 -              Session_Info(dir1, a, b, d, e, f, thys, h) }
    1.88 +          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
    1.89      }
    1.90  
    1.91 -    def parse_entries(dir: Path, root: File): List[Session_Info] =
    1.92 +    def parse_entries(root: File): List[Session_Entry] =
    1.93      {
    1.94        val toks = syntax.scan(Standard_System.read_file(root))
    1.95 -      parse_all(rep(session_info(dir)), Token.reader(toks, root.toString)) match {
    1.96 +      parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
    1.97          case Success(result, _) => result
    1.98          case bad => error(bad.toString)
    1.99        }
   1.100      }
   1.101    }
   1.102  
   1.103 -  def find_sessions(): List[Session_Info] =
   1.104 +
   1.105 +  /* find session */
   1.106 +
   1.107 +  def find_sessions(more_dirs: List[Path] = Nil): List[Session_Info] =
   1.108    {
   1.109 +    val infos = new mutable.ListBuffer[Session_Info]
   1.110 +    infos += pure_info
   1.111 +
   1.112      for {
   1.113 -      dir <- Isabelle_System.components()
   1.114 +      dir <- Isabelle_System.components() ++ more_dirs
   1.115        root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
   1.116        if root.isFile
   1.117 -      entry <- Parser.parse_entries(dir, root)
   1.118 -    } yield entry
   1.119 +      entry <- Parser.parse_entries(root)
   1.120 +    }
   1.121 +    {
   1.122 +      try {
   1.123 +        val parent =
   1.124 +          infos.find(_.name == entry.parent) getOrElse
   1.125 +           error("Unknown parent session: " + quote(entry.parent))
   1.126 +        val full_name =
   1.127 +          if (entry.reset) entry.name
   1.128 +          else parent.name + "-" + entry.name
   1.129 +        val path =
   1.130 +          entry.path match {
   1.131 +            case Some(p) => Path.explode(p)
   1.132 +            case None => Path.basic(entry.name)
   1.133 +          }
   1.134 +        val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
   1.135 +        val info =
   1.136 +          Session_Info(dir + path, full_name, entry.parent, entry.description,
   1.137 +            entry.options, thys, entry.files)
   1.138 +        infos += info
   1.139 +      }
   1.140 +      catch {
   1.141 +        case ERROR(msg) =>
   1.142 +          error(msg + "\nThe error(s) above occurred in session entry " +
   1.143 +            quote(entry.name) + " (file " + quote(root.toString) + ")")
   1.144 +      }
   1.145 +    }
   1.146 +    infos.toList
   1.147    }
   1.148  }
   1.149