# HG changeset patch
# User wenzelm
# Date 1507560195 -7200
# Node ID 5bc903a60932562aa4f60f374a6134fa6df2f949
# Parent  6b76a5d1b7a569b6fc7578afbe6250cabf9e3d61
clarified signature: public access to ROOT file syntax;

diff -r 6b76a5d1b7a5 -r 5bc903a60932 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 16:43:15 2017 +0200
@@ -550,26 +550,26 @@
       (THEORIES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
 
+  abstract class Entry
+  sealed case class Chapter(name: String) extends Entry
+  sealed case class Session_Entry(
+    pos: Position.T,
+    name: String,
+    groups: List[String],
+    path: String,
+    parent: Option[String],
+    description: String,
+    options: List[Options.Spec],
+    imports: List[String],
+    theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
+    document_files: List[(String, String)]) extends Entry
+  {
+    def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
+      theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
+  }
+
   private object Parser extends Parse.Parser with Options.Parser
   {
-    private abstract class Entry
-    private sealed case class Chapter(name: String) extends Entry
-    private sealed case class Session_Entry(
-      pos: Position.T,
-      name: String,
-      groups: List[String],
-      path: String,
-      parent: Option[String],
-      description: String,
-      options: List[Options.Spec],
-      imports: List[String],
-      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
-      document_files: List[(String, String)]) extends Entry
-    {
-      def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
-        theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
-    }
-
     private val chapter: Parser[Chapter] =
     {
       val chapter_name = atom("chapter name", _.is_name)
@@ -618,70 +618,85 @@
             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
     }
 
-    def parse_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
+    def parse_root(options: Options, select: Boolean, path: Path): List[Entry] =
     {
-      def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
-      {
-        try {
-          val name = entry.name
-
-          if (name == "" || name == DRAFT) error("Bad session name")
-          if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
-          if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
-
-          val session_options = options ++ entry.options
-
-          val theories =
-            entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
-
-          val global_theories =
-            for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
-            yield {
-              val thy_name = Path.explode(thy).expand.base_name
-              if (Long_Name.is_qualified(thy_name))
-                error("Bad qualified name for global theory " +
-                  quote(thy_name) + Position.here(pos))
-              else thy_name
-            }
-
-          val document_files =
-            entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
-
-          val meta_digest =
-            SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
-              entry.theories_no_position, entry.document_files).toString)
-
-          val info =
-            Info(name, entry_chapter, select, entry.pos, entry.groups,
-              path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
-              entry.imports, theories, global_theories, document_files, meta_digest)
-
-          (name, info)
-        }
-        catch {
-          case ERROR(msg) =>
-            error(msg + "\nThe error(s) above occurred in session entry " +
-              quote(entry.name) + Position.here(entry.pos))
-        }
-      }
-
       val toks = Token.explode(root_syntax.keywords, File.read(path))
       val start = Token.Pos.file(path.implode)
 
       parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
-        case Success(result, _) =>
-          var entry_chapter = "Unsorted"
-          val infos = new mutable.ListBuffer[(String, Info)]
-          result.foreach {
-            case Chapter(name) => entry_chapter = name
-            case entry: Session_Entry => infos += make_info(entry_chapter, entry)
-          }
-          infos.toList
+        case Success(result, _) => result
         case bad => error(bad.toString)
       }
     }
   }
 
+  def parse_root(options: Options, select: Boolean, path: Path): List[Entry] =
+    Parser.parse_root(options, select, path)
+
+  def read_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
+  {
+    def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
+    {
+      try {
+        val name = entry.name
+
+        if (name == "" || name == DRAFT) error("Bad session name")
+        if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
+        if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
+
+        val session_options = options ++ entry.options
+
+        val theories =
+          entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
+
+        val global_theories =
+          for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
+          yield {
+            val thy_name = Path.explode(thy).expand.base_name
+            if (Long_Name.is_qualified(thy_name))
+              error("Bad qualified name for global theory " +
+                quote(thy_name) + Position.here(pos))
+            else thy_name
+          }
+
+        val document_files =
+          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
+
+        val meta_digest =
+          SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
+            entry.theories_no_position, entry.document_files).toString)
+
+        val info =
+          Info(name, entry_chapter, select, entry.pos, entry.groups,
+            path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
+            entry.imports, theories, global_theories, document_files, meta_digest)
+
+        (name, info)
+      }
+      catch {
+        case ERROR(msg) =>
+          error(msg + "\nThe error(s) above occurred in session entry " +
+            quote(entry.name) + Position.here(entry.pos))
+      }
+    }
+
+    var entry_chapter = "Unsorted"
+    val infos = new mutable.ListBuffer[(String, Info)]
+    parse_root(options, select, path).foreach {
+      case Chapter(name) => entry_chapter = name
+      case entry: Session_Entry => infos += make_info(entry_chapter, entry)
+    }
+    infos.toList
+  }
+
+  def parse_roots(roots: Path): List[String] =
+  {
+    for {
+      line <- split_lines(File.read(roots))
+      if !(line == "" || line.startsWith("#"))
+    } yield line
+  }
+
 
   /* load sessions from certain directories */
 
@@ -714,10 +729,9 @@
       val roots = dir + ROOTS
       if (roots.is_file) {
         for {
-          line <- split_lines(File.read(roots))
-          if !(line == "" || line.startsWith("#"))
+          entry <- parse_roots(roots)
           dir1 =
-            try { check_session_dir(dir + Path.explode(line)) }
+            try { check_session_dir(dir + Path.explode(entry)) }
             catch {
               case ERROR(msg) =>
                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
@@ -743,7 +757,7 @@
         }
       }).toList.map(_._2)
 
-    make(unique_roots.flatMap(p => Parser.parse_root(options, p._1, p._2)))
+    make(unique_roots.flatMap(p => read_root(options, p._1, p._2)))
   }