tuned;
authorwenzelm
Mon Oct 09 17:08:37 2017 +0200 (19 months ago)
changeset 66819064c80e9d1cf
parent 66818 5bc903a60932
child 66820 fc516da7ee4f
tuned;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 09 16:43:15 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 17:08:37 2017 +0200
     1.3 @@ -618,7 +618,7 @@
     1.4              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
     1.5      }
     1.6  
     1.7 -    def parse_root(options: Options, select: Boolean, path: Path): List[Entry] =
     1.8 +    def parse_root(path: Path): List[Entry] =
     1.9      {
    1.10        val toks = Token.explode(root_syntax.keywords, File.read(path))
    1.11        val start = Token.Pos.file(path.implode)
    1.12 @@ -630,8 +630,11 @@
    1.13      }
    1.14    }
    1.15  
    1.16 -  def parse_root(options: Options, select: Boolean, path: Path): List[Entry] =
    1.17 -    Parser.parse_root(options, select, path)
    1.18 +  def parse_root(path: Path): List[Entry] = Parser.parse_root(path)
    1.19 +
    1.20 +  def parse_root_entries(path: Path): List[Session_Entry] =
    1.21 +    for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry])
    1.22 +    yield entry.asInstanceOf[Session_Entry]
    1.23  
    1.24    def read_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
    1.25    {
    1.26 @@ -682,7 +685,7 @@
    1.27  
    1.28      var entry_chapter = "Unsorted"
    1.29      val infos = new mutable.ListBuffer[(String, Info)]
    1.30 -    parse_root(options, select, path).foreach {
    1.31 +    parse_root(path).foreach {
    1.32        case Chapter(name) => entry_chapter = name
    1.33        case entry: Session_Entry => infos += make_info(entry_chapter, entry)
    1.34      }