clarified modules;
authorwenzelm
Tue Mar 15 22:01:26 2016 +0100 (2016-03-15)
changeset 62631c39614ddb80b
parent 62630 bc772694cfbd
child 62632 cd991ba01ffd
clarified modules;
src/Pure/PIDE/batch_session.scala
src/Pure/Thy/present.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_doc.scala
src/Pure/build-jars
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_logic.scala
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Tue Mar 15 16:23:27 2016 +0100
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Tue Mar 15 22:01:26 2016 +0100
     1.3 @@ -18,8 +18,7 @@
     1.4      dirs: List[Path] = Nil,
     1.5      session: String): Batch_Session =
     1.6    {
     1.7 -    val (_, session_tree) =
     1.8 -      Build.find_sessions(options, dirs).selection(sessions = List(session))
     1.9 +    val (_, session_tree) = Sessions.find(options, dirs).selection(sessions = List(session))
    1.10      val session_info = session_tree(session)
    1.11      val parent_session =
    1.12        session_info.parent getOrElse error("No parent session for " + quote(session))
     2.1 --- a/src/Pure/Thy/present.scala	Tue Mar 15 16:23:27 2016 +0100
     2.2 +++ b/src/Pure/Thy/present.scala	Tue Mar 15 22:01:26 2016 +0100
     2.3 @@ -96,7 +96,7 @@
     2.4      progress: Progress,
     2.5      browser_info: Path,
     2.6      graph_file: JFile,
     2.7 -    info: Build.Session_Info,
     2.8 +    info: Sessions.Info,
     2.9      name: String)
    2.10    {
    2.11      val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Thy/sessions.scala	Tue Mar 15 22:01:26 2016 +0100
     3.3 @@ -0,0 +1,319 @@
     3.4 +/*  Title:      Pure/Thy/sessions.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Session information.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +import scala.collection.SortedSet
    3.14 +import scala.collection.mutable
    3.15 +
    3.16 +
    3.17 +object Sessions
    3.18 +{
    3.19 +  /* info */
    3.20 +
    3.21 +  val ROOT = Path.explode("ROOT")
    3.22 +  val ROOTS = Path.explode("ROOTS")
    3.23 +
    3.24 +  def is_pure(name: String): Boolean = name == "Pure"
    3.25 +
    3.26 +  sealed case class Info(
    3.27 +    chapter: String,
    3.28 +    select: Boolean,
    3.29 +    pos: Position.T,
    3.30 +    groups: List[String],
    3.31 +    dir: Path,
    3.32 +    parent: Option[String],
    3.33 +    description: String,
    3.34 +    options: Options,
    3.35 +    theories: List[(Boolean, Options, List[Path])],
    3.36 +    files: List[Path],
    3.37 +    document_files: List[(Path, Path)],
    3.38 +    meta_digest: SHA1.Digest)
    3.39 +  {
    3.40 +    def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    3.41 +  }
    3.42 +
    3.43 +
    3.44 +  /* session tree */
    3.45 +
    3.46 +  object Tree
    3.47 +  {
    3.48 +    def apply(infos: Seq[(String, Info)]): Tree =
    3.49 +    {
    3.50 +      val graph1 =
    3.51 +        (Graph.string[Info] /: infos) {
    3.52 +          case (graph, (name, info)) =>
    3.53 +            if (graph.defined(name))
    3.54 +              error("Duplicate session " + quote(name) + Position.here(info.pos) +
    3.55 +                Position.here(graph.get_node(name).pos))
    3.56 +            else graph.new_node(name, info)
    3.57 +        }
    3.58 +      val graph2 =
    3.59 +        (graph1 /: graph1.iterator) {
    3.60 +          case (graph, (name, (info, _))) =>
    3.61 +            info.parent match {
    3.62 +              case None => graph
    3.63 +              case Some(parent) =>
    3.64 +                if (!graph.defined(parent))
    3.65 +                  error("Bad parent session " + quote(parent) + " for " +
    3.66 +                    quote(name) + Position.here(info.pos))
    3.67 +
    3.68 +                try { graph.add_edge_acyclic(parent, name) }
    3.69 +                catch {
    3.70 +                  case exn: Graph.Cycles[_] =>
    3.71 +                    error(cat_lines(exn.cycles.map(cycle =>
    3.72 +                      "Cyclic session dependency of " +
    3.73 +                        cycle.map(c => quote(c.toString)).mkString(" via "))) +
    3.74 +                          Position.here(info.pos))
    3.75 +                }
    3.76 +            }
    3.77 +        }
    3.78 +      new Tree(graph2)
    3.79 +    }
    3.80 +  }
    3.81 +
    3.82 +  final class Tree private(val graph: Graph[String, Info])
    3.83 +    extends PartialFunction[String, Info]
    3.84 +  {
    3.85 +    def apply(name: String): Info = graph.get_node(name)
    3.86 +    def isDefinedAt(name: String): Boolean = graph.defined(name)
    3.87 +
    3.88 +    def selection(
    3.89 +      requirements: Boolean = false,
    3.90 +      all_sessions: Boolean = false,
    3.91 +      exclude_session_groups: List[String] = Nil,
    3.92 +      exclude_sessions: List[String] = Nil,
    3.93 +      session_groups: List[String] = Nil,
    3.94 +      sessions: List[String] = Nil): (List[String], Tree) =
    3.95 +    {
    3.96 +      val bad_sessions =
    3.97 +        SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
    3.98 +      if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    3.99 +
   3.100 +      val excluded =
   3.101 +      {
   3.102 +        val exclude_group = exclude_session_groups.toSet
   3.103 +        val exclude_group_sessions =
   3.104 +          (for {
   3.105 +            (name, (info, _)) <- graph.iterator
   3.106 +            if apply(name).groups.exists(exclude_group)
   3.107 +          } yield name).toList
   3.108 +        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
   3.109 +      }
   3.110 +
   3.111 +      val pre_selected =
   3.112 +      {
   3.113 +        if (all_sessions) graph.keys
   3.114 +        else {
   3.115 +          val select_group = session_groups.toSet
   3.116 +          val select = sessions.toSet
   3.117 +          (for {
   3.118 +            (name, (info, _)) <- graph.iterator
   3.119 +            if info.select || select(name) || apply(name).groups.exists(select_group)
   3.120 +          } yield name).toList
   3.121 +        }
   3.122 +      }.filterNot(excluded)
   3.123 +
   3.124 +      val selected =
   3.125 +        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   3.126 +        else pre_selected
   3.127 +
   3.128 +      val graph1 = graph.restrict(graph.all_preds(selected).toSet)
   3.129 +      (selected, new Tree(graph1))
   3.130 +    }
   3.131 +
   3.132 +    def ancestors(name: String): List[String] =
   3.133 +      graph.all_preds(List(name)).tail.reverse
   3.134 +
   3.135 +    def topological_order: List[(String, Info)] =
   3.136 +      graph.topological_order.map(name => (name, apply(name)))
   3.137 +
   3.138 +    override def toString: String = graph.keys_iterator.mkString("Sessions.Tree(", ", ", ")")
   3.139 +  }
   3.140 +
   3.141 +
   3.142 +  /* parser */
   3.143 +
   3.144 +  private val CHAPTER = "chapter"
   3.145 +  private val SESSION = "session"
   3.146 +  private val IN = "in"
   3.147 +  private val DESCRIPTION = "description"
   3.148 +  private val OPTIONS = "options"
   3.149 +  private val GLOBAL_THEORIES = "global_theories"
   3.150 +  private val THEORIES = "theories"
   3.151 +  private val FILES = "files"
   3.152 +  private val DOCUMENT_FILES = "document_files"
   3.153 +
   3.154 +  lazy val root_syntax =
   3.155 +    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   3.156 +      (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
   3.157 +      IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
   3.158 +
   3.159 +  object Parser extends Parse.Parser
   3.160 +  {
   3.161 +    private abstract class Entry
   3.162 +    private sealed case class Chapter(name: String) extends Entry
   3.163 +    private sealed case class Session_Entry(
   3.164 +      pos: Position.T,
   3.165 +      name: String,
   3.166 +      groups: List[String],
   3.167 +      path: String,
   3.168 +      parent: Option[String],
   3.169 +      description: String,
   3.170 +      options: List[Options.Spec],
   3.171 +      theories: List[(Boolean, List[Options.Spec], List[String])],
   3.172 +      files: List[String],
   3.173 +      document_files: List[(String, String)]) extends Entry
   3.174 +
   3.175 +    private val chapter: Parser[Chapter] =
   3.176 +    {
   3.177 +      val chapter_name = atom("chapter name", _.is_name)
   3.178 +
   3.179 +      command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
   3.180 +    }
   3.181 +
   3.182 +    private val session_entry: Parser[Session_Entry] =
   3.183 +    {
   3.184 +      val session_name = atom("session name", _.is_name)
   3.185 +
   3.186 +      val option =
   3.187 +        name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   3.188 +      val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
   3.189 +
   3.190 +      val theories =
   3.191 +        ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
   3.192 +          ((options | success(Nil)) ~ rep(theory_xname)) ^^
   3.193 +          { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
   3.194 +
   3.195 +      val document_files =
   3.196 +        $$$(DOCUMENT_FILES) ~!
   3.197 +          (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
   3.198 +              { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
   3.199 +            rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
   3.200 +
   3.201 +      command(SESSION) ~!
   3.202 +        (position(session_name) ~
   3.203 +          (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   3.204 +          (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   3.205 +          ($$$("=") ~!
   3.206 +            (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
   3.207 +              (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   3.208 +              (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   3.209 +              rep1(theories) ~
   3.210 +              (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
   3.211 +              (rep(document_files) ^^ (x => x.flatten))))) ^^
   3.212 +        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
   3.213 +            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
   3.214 +    }
   3.215 +
   3.216 +    def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
   3.217 +    {
   3.218 +      def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
   3.219 +      {
   3.220 +        try {
   3.221 +          val name = entry.name
   3.222 +
   3.223 +          if (name == "") error("Bad session name")
   3.224 +          if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
   3.225 +          if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
   3.226 +
   3.227 +          val session_options = options ++ entry.options
   3.228 +
   3.229 +          val theories =
   3.230 +            entry.theories.map({ case (global, opts, thys) =>
   3.231 +              (global, session_options ++ opts, thys.map(Path.explode(_))) })
   3.232 +          val files = entry.files.map(Path.explode(_))
   3.233 +          val document_files =
   3.234 +            entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
   3.235 +
   3.236 +          val meta_digest =
   3.237 +            SHA1.digest((entry_chapter, name, entry.parent, entry.options,
   3.238 +              entry.theories, entry.files, entry.document_files).toString)
   3.239 +
   3.240 +          val info =
   3.241 +            Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
   3.242 +              entry.parent, entry.description, session_options, theories, files,
   3.243 +              document_files, meta_digest)
   3.244 +
   3.245 +          (name, info)
   3.246 +        }
   3.247 +        catch {
   3.248 +          case ERROR(msg) =>
   3.249 +            error(msg + "\nThe error(s) above occurred in session entry " +
   3.250 +              quote(entry.name) + Position.here(entry.pos))
   3.251 +        }
   3.252 +      }
   3.253 +
   3.254 +      val root = dir + ROOT
   3.255 +      if (root.is_file) {
   3.256 +        val toks = Token.explode(root_syntax.keywords, File.read(root))
   3.257 +        val start = Token.Pos.file(root.implode)
   3.258 +
   3.259 +        parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
   3.260 +          case Success(result, _) =>
   3.261 +            var entry_chapter = "Unsorted"
   3.262 +            val infos = new mutable.ListBuffer[(String, Info)]
   3.263 +            result.foreach {
   3.264 +              case Chapter(name) => entry_chapter = name
   3.265 +              case entry: Session_Entry => infos += make_info(entry_chapter, entry)
   3.266 +            }
   3.267 +            infos.toList
   3.268 +          case bad => error(bad.toString)
   3.269 +        }
   3.270 +      }
   3.271 +      else Nil
   3.272 +    }
   3.273 +  }
   3.274 +
   3.275 +
   3.276 +  /* find sessions within certain directories */
   3.277 +
   3.278 +  private def is_session_dir(dir: Path): Boolean =
   3.279 +    (dir + ROOT).is_file || (dir + ROOTS).is_file
   3.280 +
   3.281 +  private def check_session_dir(dir: Path): Path =
   3.282 +    if (is_session_dir(dir)) dir
   3.283 +    else error("Bad session root directory: " + dir.toString)
   3.284 +
   3.285 +  def find(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
   3.286 +  {
   3.287 +    def find_dir(select: Boolean, dir: Path): List[(String, Info)] =
   3.288 +      find_root(select, dir) ::: find_roots(select, dir)
   3.289 +
   3.290 +    def find_root(select: Boolean, dir: Path): List[(String, Info)] =
   3.291 +      Parser.parse(options, select, dir)
   3.292 +
   3.293 +    def find_roots(select: Boolean, dir: Path): List[(String, Info)] =
   3.294 +    {
   3.295 +      val roots = dir + ROOTS
   3.296 +      if (roots.is_file) {
   3.297 +        for {
   3.298 +          line <- split_lines(File.read(roots))
   3.299 +          if !(line == "" || line.startsWith("#"))
   3.300 +          dir1 =
   3.301 +            try { check_session_dir(dir + Path.explode(line)) }
   3.302 +            catch {
   3.303 +              case ERROR(msg) =>
   3.304 +                error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   3.305 +            }
   3.306 +          info <- find_dir(select, dir1)
   3.307 +        } yield info
   3.308 +      }
   3.309 +      else Nil
   3.310 +    }
   3.311 +
   3.312 +    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
   3.313 +    dirs.foreach(check_session_dir(_))
   3.314 +    select_dirs.foreach(check_session_dir(_))
   3.315 +
   3.316 +    Tree(
   3.317 +      for {
   3.318 +        (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
   3.319 +        info <- find_dir(select, dir)
   3.320 +      } yield info)
   3.321 +  }
   3.322 +}
     4.1 --- a/src/Pure/Tools/build.scala	Tue Mar 15 16:23:27 2016 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 15 22:01:26 2016 +0100
     4.3 @@ -19,324 +19,13 @@
     4.4  
     4.5  object Build
     4.6  {
     4.7 -  /** session information **/
     4.8 -
     4.9 -  // external version
    4.10 -  abstract class Entry
    4.11 -  sealed case class Chapter(name: String) extends Entry
    4.12 -  sealed case class Session_Entry(
    4.13 -    pos: Position.T,
    4.14 -    name: String,
    4.15 -    groups: List[String],
    4.16 -    path: String,
    4.17 -    parent: Option[String],
    4.18 -    description: String,
    4.19 -    options: List[Options.Spec],
    4.20 -    theories: List[(Boolean, List[Options.Spec], List[String])],
    4.21 -    files: List[String],
    4.22 -    document_files: List[(String, String)]) extends Entry
    4.23 -
    4.24 -  // internal version
    4.25 -  sealed case class Session_Info(
    4.26 -    chapter: String,
    4.27 -    select: Boolean,
    4.28 -    pos: Position.T,
    4.29 -    groups: List[String],
    4.30 -    dir: Path,
    4.31 -    parent: Option[String],
    4.32 -    description: String,
    4.33 -    options: Options,
    4.34 -    theories: List[(Boolean, Options, List[Path])],
    4.35 -    files: List[Path],
    4.36 -    document_files: List[(Path, Path)],
    4.37 -    entry_digest: SHA1.Digest)
    4.38 -  {
    4.39 -    def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    4.40 -  }
    4.41 -
    4.42 -  def is_pure(name: String): Boolean = name == "Pure"
    4.43 -
    4.44 -  def session_info(options: Options, select: Boolean, dir: Path,
    4.45 -      chapter: String, entry: Session_Entry): (String, Session_Info) =
    4.46 -    try {
    4.47 -      val name = entry.name
    4.48 -
    4.49 -      if (name == "") error("Bad session name")
    4.50 -      if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    4.51 -      if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
    4.52 -
    4.53 -      val session_options = options ++ entry.options
    4.54 -
    4.55 -      val theories =
    4.56 -        entry.theories.map({ case (global, opts, thys) =>
    4.57 -          (global, session_options ++ opts, thys.map(Path.explode(_))) })
    4.58 -      val files = entry.files.map(Path.explode(_))
    4.59 -      val document_files =
    4.60 -        entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    4.61 -
    4.62 -      val entry_digest =
    4.63 -        SHA1.digest((chapter, name, entry.parent, entry.options,
    4.64 -          entry.theories, entry.files, entry.document_files).toString)
    4.65 -
    4.66 -      val info =
    4.67 -        Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
    4.68 -          entry.parent, entry.description, session_options, theories, files,
    4.69 -          document_files, entry_digest)
    4.70 -
    4.71 -      (name, info)
    4.72 -    }
    4.73 -    catch {
    4.74 -      case ERROR(msg) =>
    4.75 -        error(msg + "\nThe error(s) above occurred in session entry " +
    4.76 -          quote(entry.name) + Position.here(entry.pos))
    4.77 -    }
    4.78 -
    4.79 -
    4.80 -  /* session tree */
    4.81 -
    4.82 -  object Session_Tree
    4.83 -  {
    4.84 -    def apply(infos: Seq[(String, Session_Info)]): Session_Tree =
    4.85 -    {
    4.86 -      val graph1 =
    4.87 -        (Graph.string[Session_Info] /: infos) {
    4.88 -          case (graph, (name, info)) =>
    4.89 -            if (graph.defined(name))
    4.90 -              error("Duplicate session " + quote(name) + Position.here(info.pos) +
    4.91 -                Position.here(graph.get_node(name).pos))
    4.92 -            else graph.new_node(name, info)
    4.93 -        }
    4.94 -      val graph2 =
    4.95 -        (graph1 /: graph1.iterator) {
    4.96 -          case (graph, (name, (info, _))) =>
    4.97 -            info.parent match {
    4.98 -              case None => graph
    4.99 -              case Some(parent) =>
   4.100 -                if (!graph.defined(parent))
   4.101 -                  error("Bad parent session " + quote(parent) + " for " +
   4.102 -                    quote(name) + Position.here(info.pos))
   4.103 -
   4.104 -                try { graph.add_edge_acyclic(parent, name) }
   4.105 -                catch {
   4.106 -                  case exn: Graph.Cycles[_] =>
   4.107 -                    error(cat_lines(exn.cycles.map(cycle =>
   4.108 -                      "Cyclic session dependency of " +
   4.109 -                        cycle.map(c => quote(c.toString)).mkString(" via "))) +
   4.110 -                          Position.here(info.pos))
   4.111 -                }
   4.112 -            }
   4.113 -        }
   4.114 -      new Session_Tree(graph2)
   4.115 -    }
   4.116 -  }
   4.117 -
   4.118 -  final class Session_Tree private(val graph: Graph[String, Session_Info])
   4.119 -    extends PartialFunction[String, Session_Info]
   4.120 -  {
   4.121 -    def apply(name: String): Session_Info = graph.get_node(name)
   4.122 -    def isDefinedAt(name: String): Boolean = graph.defined(name)
   4.123 -
   4.124 -    def selection(
   4.125 -      requirements: Boolean = false,
   4.126 -      all_sessions: Boolean = false,
   4.127 -      exclude_session_groups: List[String] = Nil,
   4.128 -      exclude_sessions: List[String] = Nil,
   4.129 -      session_groups: List[String] = Nil,
   4.130 -      sessions: List[String] = Nil): (List[String], Session_Tree) =
   4.131 -    {
   4.132 -      val bad_sessions =
   4.133 -        SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
   4.134 -      if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
   4.135 -
   4.136 -      val excluded =
   4.137 -      {
   4.138 -        val exclude_group = exclude_session_groups.toSet
   4.139 -        val exclude_group_sessions =
   4.140 -          (for {
   4.141 -            (name, (info, _)) <- graph.iterator
   4.142 -            if apply(name).groups.exists(exclude_group)
   4.143 -          } yield name).toList
   4.144 -        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
   4.145 -      }
   4.146 -
   4.147 -      val pre_selected =
   4.148 -      {
   4.149 -        if (all_sessions) graph.keys
   4.150 -        else {
   4.151 -          val select_group = session_groups.toSet
   4.152 -          val select = sessions.toSet
   4.153 -          (for {
   4.154 -            (name, (info, _)) <- graph.iterator
   4.155 -            if info.select || select(name) || apply(name).groups.exists(select_group)
   4.156 -          } yield name).toList
   4.157 -        }
   4.158 -      }.filterNot(excluded)
   4.159 -
   4.160 -      val selected =
   4.161 -        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   4.162 -        else pre_selected
   4.163 -
   4.164 -      val graph1 = graph.restrict(graph.all_preds(selected).toSet)
   4.165 -      (selected, new Session_Tree(graph1))
   4.166 -    }
   4.167 -
   4.168 -    def ancestors(name: String): List[String] =
   4.169 -      graph.all_preds(List(name)).tail.reverse
   4.170 -
   4.171 -    def topological_order: List[(String, Session_Info)] =
   4.172 -      graph.topological_order.map(name => (name, apply(name)))
   4.173 -
   4.174 -    override def toString: String = graph.keys_iterator.mkString("Session_Tree(", ", ", ")")
   4.175 -  }
   4.176 -
   4.177 -
   4.178 -  /* parser */
   4.179 -
   4.180 -  val chapter_default = "Unsorted"
   4.181 -
   4.182 -  private val CHAPTER = "chapter"
   4.183 -  private val SESSION = "session"
   4.184 -  private val IN = "in"
   4.185 -  private val DESCRIPTION = "description"
   4.186 -  private val OPTIONS = "options"
   4.187 -  private val GLOBAL_THEORIES = "global_theories"
   4.188 -  private val THEORIES = "theories"
   4.189 -  private val FILES = "files"
   4.190 -  private val DOCUMENT_FILES = "document_files"
   4.191 -
   4.192 -  lazy val root_syntax =
   4.193 -    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   4.194 -      (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
   4.195 -      IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
   4.196 -
   4.197 -  object Parser extends Parse.Parser
   4.198 -  {
   4.199 -    private val chapter: Parser[Chapter] =
   4.200 -    {
   4.201 -      val chapter_name = atom("chapter name", _.is_name)
   4.202 -
   4.203 -      command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
   4.204 -    }
   4.205 -
   4.206 -    private val session_entry: Parser[Session_Entry] =
   4.207 -    {
   4.208 -      val session_name = atom("session name", _.is_name)
   4.209 -
   4.210 -      val option =
   4.211 -        name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   4.212 -      val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
   4.213 -
   4.214 -      val theories =
   4.215 -        ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
   4.216 -          ((options | success(Nil)) ~ rep(theory_xname)) ^^
   4.217 -          { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
   4.218 -
   4.219 -      val document_files =
   4.220 -        $$$(DOCUMENT_FILES) ~!
   4.221 -          (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
   4.222 -              { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
   4.223 -            rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
   4.224 -
   4.225 -      command(SESSION) ~!
   4.226 -        (position(session_name) ~
   4.227 -          (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   4.228 -          (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   4.229 -          ($$$("=") ~!
   4.230 -            (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
   4.231 -              (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   4.232 -              (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   4.233 -              rep1(theories) ~
   4.234 -              (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
   4.235 -              (rep(document_files) ^^ (x => x.flatten))))) ^^
   4.236 -        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
   4.237 -            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
   4.238 -    }
   4.239 -
   4.240 -    def parse_entries(root: Path): List[(String, Session_Entry)] =
   4.241 -    {
   4.242 -      val toks = Token.explode(root_syntax.keywords, File.read(root))
   4.243 -      val start = Token.Pos.file(root.implode)
   4.244 -
   4.245 -      parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
   4.246 -        case Success(result, _) =>
   4.247 -          var chapter = chapter_default
   4.248 -          val entries = new mutable.ListBuffer[(String, Session_Entry)]
   4.249 -          result.foreach {
   4.250 -            case Chapter(name) => chapter = name
   4.251 -            case session_entry: Session_Entry => entries += ((chapter, session_entry))
   4.252 -          }
   4.253 -          entries.toList
   4.254 -        case bad => error(bad.toString)
   4.255 -      }
   4.256 -    }
   4.257 -  }
   4.258 -
   4.259 -
   4.260 -  /* find sessions within certain directories */
   4.261 -
   4.262 -  private val ROOT = Path.explode("ROOT")
   4.263 -  private val ROOTS = Path.explode("ROOTS")
   4.264 -
   4.265 -  private def is_session_dir(dir: Path): Boolean =
   4.266 -    (dir + ROOT).is_file || (dir + ROOTS).is_file
   4.267 -
   4.268 -  private def check_session_dir(dir: Path): Path =
   4.269 -    if (is_session_dir(dir)) dir
   4.270 -    else error("Bad session root directory: " + dir.toString)
   4.271 -
   4.272 -  def find_sessions(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil)
   4.273 -    : Session_Tree =
   4.274 -  {
   4.275 -    def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
   4.276 -      find_root(select, dir) ::: find_roots(select, dir)
   4.277 -
   4.278 -    def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
   4.279 -    {
   4.280 -      val root = dir + ROOT
   4.281 -      if (root.is_file)
   4.282 -        Parser.parse_entries(root).map(p => session_info(options, select, dir, p._1, p._2))
   4.283 -      else Nil
   4.284 -    }
   4.285 -
   4.286 -    def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
   4.287 -    {
   4.288 -      val roots = dir + ROOTS
   4.289 -      if (roots.is_file) {
   4.290 -        for {
   4.291 -          line <- split_lines(File.read(roots))
   4.292 -          if !(line == "" || line.startsWith("#"))
   4.293 -          dir1 =
   4.294 -            try { check_session_dir(dir + Path.explode(line)) }
   4.295 -            catch {
   4.296 -              case ERROR(msg) =>
   4.297 -                error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   4.298 -            }
   4.299 -          info <- find_dir(select, dir1)
   4.300 -        } yield info
   4.301 -      }
   4.302 -      else Nil
   4.303 -    }
   4.304 -
   4.305 -    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
   4.306 -    dirs.foreach(check_session_dir(_))
   4.307 -    select_dirs.foreach(check_session_dir(_))
   4.308 -
   4.309 -    Session_Tree(
   4.310 -      for {
   4.311 -        (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
   4.312 -        info <- find_dir(select, dir)
   4.313 -      } yield info)
   4.314 -  }
   4.315 -
   4.316 -
   4.317 -
   4.318 -  /** build **/
   4.319 +  /** auxiliary **/
   4.320  
   4.321    /* queue */
   4.322  
   4.323 -  object Queue
   4.324 +  private object Queue
   4.325    {
   4.326 -    def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
   4.327 +    def apply(tree: Sessions.Tree, load_timings: String => (List[Properties.T], Double)): Queue =
   4.328      {
   4.329        val graph = tree.graph
   4.330        val sessions = graph.keys
   4.331 @@ -378,8 +67,8 @@
   4.332      }
   4.333    }
   4.334  
   4.335 -  final class Queue private(
   4.336 -    graph: Graph[String, Session_Info],
   4.337 +  private final class Queue private(
   4.338 +    graph: Graph[String, Sessions.Info],
   4.339      order: SortedSet[String],
   4.340      val command_timings: String => List[Properties.T])
   4.341    {
   4.342 @@ -392,7 +81,7 @@
   4.343          order - name,  // FIXME scala-2.10.0 TreeSet problem!?
   4.344          command_timings)
   4.345  
   4.346 -    def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
   4.347 +    def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
   4.348      {
   4.349        val it = order.iterator.dropWhile(name =>
   4.350          skip(name)
   4.351 @@ -427,7 +116,7 @@
   4.352        verbose: Boolean = false,
   4.353        list_files: Boolean = false,
   4.354        check_keywords: Set[String] = Set.empty,
   4.355 -      tree: Session_Tree): Deps =
   4.356 +      tree: Sessions.Tree): Deps =
   4.357      Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   4.358        { case (deps, (name, info)) =>
   4.359            if (progress.stopped) throw Exn.Interrupt()
   4.360 @@ -520,7 +209,7 @@
   4.361      dirs: List[Path],
   4.362      sessions: List[String]): Deps =
   4.363    {
   4.364 -    val (_, tree) = find_sessions(options, dirs = dirs).selection(sessions = sessions)
   4.365 +    val (_, tree) = Sessions.find(options, dirs = dirs).selection(sessions = sessions)
   4.366      dependencies(inlined_files = inlined_files, tree = tree)
   4.367    }
   4.368  
   4.369 @@ -540,7 +229,7 @@
   4.370    /* jobs */
   4.371  
   4.372    private class Job(progress: Progress,
   4.373 -    name: String, val info: Session_Info, output: Path, do_output: Boolean, verbose: Boolean,
   4.374 +    name: String, val info: Sessions.Info, output: Path, do_output: Boolean, verbose: Boolean,
   4.375      browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
   4.376    {
   4.377      def output_path: Option[Path] = if (do_output) Some(output) else None
   4.378 @@ -564,7 +253,7 @@
   4.379      private val future_result: Future[Process_Result] =
   4.380        Future.thread("build") {
   4.381          val process =
   4.382 -          if (is_pure(name)) {
   4.383 +          if (Sessions.is_pure(name)) {
   4.384              val eval =
   4.385                "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
   4.386                " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
   4.387 @@ -623,7 +312,7 @@
   4.388      {
   4.389        val result = future_result.join
   4.390  
   4.391 -      if (result.ok && !is_pure(name))
   4.392 +      if (result.ok && !Sessions.is_pure(name))
   4.393          Present.finish(progress, browser_info, graph_file, info, name)
   4.394  
   4.395        graph_file.delete
   4.396 @@ -731,7 +420,8 @@
   4.397      else None
   4.398  
   4.399  
   4.400 -  /* build_results */
   4.401 +
   4.402 +  /** build_results **/
   4.403  
   4.404    class Build_Results private [Build](results: Map[String, Option[Process_Result]])
   4.405    {
   4.406 @@ -765,7 +455,7 @@
   4.407    {
   4.408      /* session tree and dependencies */
   4.409  
   4.410 -    val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
   4.411 +    val full_tree = Sessions.find(options.int("completion_limit") = 0, dirs, select_dirs)
   4.412      val (selected, selected_tree) =
   4.413        full_tree.selection(requirements, all_sessions,
   4.414          exclude_session_groups, exclude_sessions, session_groups, sessions)
   4.415 @@ -773,7 +463,7 @@
   4.416      val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
   4.417  
   4.418      def session_sources_stamp(name: String): String =
   4.419 -      sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
   4.420 +      sources_stamp(selected_tree(name).meta_digest :: deps.sources(name))
   4.421  
   4.422  
   4.423      /* persistent information */
   4.424 @@ -924,7 +614,7 @@
   4.425                  val ancestor_heaps = ancestor_results.map(_.heaps).flatten
   4.426  
   4.427                  val output = output_dir + Path.basic(name)
   4.428 -                val do_output = build_heap || is_pure(name) || queue.is_inner(name)
   4.429 +                val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   4.430  
   4.431                  val (current, heaps) =
   4.432                  {
   4.433 @@ -990,7 +680,7 @@
   4.434        val browser_chapters =
   4.435          (for {
   4.436            (name, result) <- results.iterator
   4.437 -          if result.ok && !is_pure(name)
   4.438 +          if result.ok && !Sessions.is_pure(name)
   4.439            info = full_tree(name)
   4.440            if info.options.bool("browser_info")
   4.441          } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   4.442 @@ -1006,7 +696,8 @@
   4.443    }
   4.444  
   4.445  
   4.446 -  /* build */
   4.447 +
   4.448 +  /** build **/
   4.449  
   4.450    def build(
   4.451      options: Options,
     5.1 --- a/src/Pure/Tools/build_doc.scala	Tue Mar 15 16:23:27 2016 +0100
     5.2 +++ b/src/Pure/Tools/build_doc.scala	Tue Mar 15 22:01:26 2016 +0100
     5.3 @@ -24,7 +24,7 @@
     5.4    {
     5.5      val selection =
     5.6        for {
     5.7 -        (name, info) <- Build.find_sessions(options).topological_order
     5.8 +        (name, info) <- Sessions.find(options).topological_order
     5.9          if info.groups.contains("doc")
    5.10          doc = info.options.string("document_variants")
    5.11          if all_docs || docs.contains(doc)
     6.1 --- a/src/Pure/build-jars	Tue Mar 15 16:23:27 2016 +0100
     6.2 +++ b/src/Pure/build-jars	Tue Mar 15 22:01:26 2016 +0100
     6.3 @@ -90,6 +90,7 @@
     6.4    System/utf8.scala
     6.5    Thy/html.scala
     6.6    Thy/present.scala
     6.7 +  Thy/sessions.scala
     6.8    Thy/thy_header.scala
     6.9    Thy/thy_info.scala
    6.10    Thy/thy_syntax.scala
     7.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 15 16:23:27 2016 +0100
     7.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 15 22:01:26 2016 +0100
     7.3 @@ -51,7 +51,7 @@
     7.4      mode match {
     7.5        case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
     7.6        case "isabelle-options" => Some(Options.options_syntax)
     7.7 -      case "isabelle-root" => Some(Build.root_syntax)
     7.8 +      case "isabelle-root" => Some(Sessions.root_syntax)
     7.9        case "isabelle-ml" => Some(ml_syntax)
    7.10        case "isabelle-news" => Some(news_syntax)
    7.11        case "isabelle-output" => None
     8.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Mar 15 16:23:27 2016 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Mar 15 22:01:26 2016 +0100
     8.3 @@ -83,7 +83,7 @@
     8.4  
     8.5    def session_list(): List[String] =
     8.6    {
     8.7 -    val session_tree = Build.find_sessions(PIDE.options.value, dirs = session_dirs())
     8.8 +    val session_tree = Sessions.find(PIDE.options.value, dirs = session_dirs())
     8.9      val (main_sessions, other_sessions) =
    8.10        session_tree.topological_order.partition(p => p._2.groups.contains("main"))
    8.11      main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted