# HG changeset patch
# User wenzelm
# Date 1507561717 -7200
# Node ID 064c80e9d1cfd7a3a2458d704e904b68fa4ff763
# Parent  5bc903a60932562aa4f60f374a6134fa6df2f949
tuned;

diff -r 5bc903a60932 -r 064c80e9d1cf src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Oct 09 16:43:15 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 17:08:37 2017 +0200
@@ -618,7 +618,7 @@
             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
     }
 
-    def parse_root(options: Options, select: Boolean, path: Path): List[Entry] =
+    def parse_root(path: Path): List[Entry] =
     {
       val toks = Token.explode(root_syntax.keywords, File.read(path))
       val start = Token.Pos.file(path.implode)
@@ -630,8 +630,11 @@
     }
   }
 
-  def parse_root(options: Options, select: Boolean, path: Path): List[Entry] =
-    Parser.parse_root(options, select, path)
+  def parse_root(path: Path): List[Entry] = Parser.parse_root(path)
+
+  def parse_root_entries(path: Path): List[Session_Entry] =
+    for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry])
+    yield entry.asInstanceOf[Session_Entry]
 
   def read_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
   {
@@ -682,7 +685,7 @@
 
     var entry_chapter = "Unsorted"
     val infos = new mutable.ListBuffer[(String, Info)]
-    parse_root(options, select, path).foreach {
+    parse_root(path).foreach {
       case Chapter(name) => entry_chapter = name
       case entry: Session_Entry => infos += make_info(entry_chapter, entry)
     }