# HG changeset patch
# User wenzelm
# Date 1343914495 -7200
# Node ID 47330b712f8f97e6e2f24ae6ab72d83a8bf4ca3f
# Parent  bf9bff84a61d2ab5e87f29f365d6d79192ce9149
discontinued unused etc/sessions catalog;

diff -r bf9bff84a61d -r 47330b712f8f doc-src/System/Thy/Sessions.thy
--- a/doc-src/System/Thy/Sessions.thy	Thu Aug 02 15:23:28 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Thu Aug 02 15:34:55 2012 +0200
@@ -195,11 +195,7 @@
   component directories (\secref{sec:components}), augmented by more
   directories given via options @{verbatim "-d"}~@{text "DIR"} on the
   command line.  Each such directory may contain a session
-  \texttt{ROOT} file and an additional catalog file @{verbatim
-  "etc/sessions"} with further sub-directories (list of lines).  Note
-  that a single \texttt{ROOT} file usually defines many sessions;
-  catalogs are only required for extra scalability and modularity
-  of large libraries.
+  \texttt{ROOT} file with several session specifications.
 
   \medskip The subset of sessions to be managed is determined via
   individual @{text "SESSIONS"} given as command-line arguments, or
diff -r bf9bff84a61d -r 47330b712f8f doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Thu Aug 02 15:23:28 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Thu Aug 02 15:34:55 2012 +0200
@@ -311,10 +311,7 @@
   component directories (\secref{sec:components}), augmented by more
   directories given via options \verb|-d|~\isa{{\isaliteral{22}{\isachardoublequote}}DIR{\isaliteral{22}{\isachardoublequote}}} on the
   command line.  Each such directory may contain a session
-  \texttt{ROOT} file and an additional catalog file \verb|etc/sessions| with further sub-directories (list of lines).  Note
-  that a single \texttt{ROOT} file usually defines many sessions;
-  catalogs are only required for extra scalability and modularity
-  of large libraries.
+  \texttt{ROOT} file with several session specifications.
 
   \medskip The subset of sessions to be managed is determined via
   individual \isa{{\isaliteral{22}{\isachardoublequote}}SESSIONS{\isaliteral{22}{\isachardoublequote}}} given as command-line arguments, or
diff -r bf9bff84a61d -r 47330b712f8f src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Aug 02 15:23:28 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Aug 02 15:34:55 2012 +0200
@@ -187,7 +187,7 @@
 
   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
 
-  private def sessions_root(options: Options, dir: Path, root: Path, queue: Session.Queue)
+  private def sessions_root(options: Options, dir: Path, queue: Session.Queue, root: Path)
     : Session.Queue =
   {
     (queue /: Parser.parse_entries(root))((queue1, entry) =>
@@ -235,46 +235,21 @@
       })
   }
 
-  private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
+  private def sessions_dir(options: Options, strict: Boolean, queue: Session.Queue, dir: Path)
     : Session.Queue =
   {
     val root = dir + ROOT
-    if (root.is_file) sessions_root(options, dir, root, queue)
+    if (root.is_file) sessions_root(options, dir, queue, root)
     else if (strict) error("Bad session root file: " + root.toString)
     else queue
   }
 
-  private def sessions_catalog(options: Options, dir: Path, catalog: Path, queue: Session.Queue)
-    : Session.Queue =
-  {
-    val dirs =
-      split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
-    (queue /: dirs)((queue1, dir1) =>
-      try {
-        val dir2 = dir + Path.explode(dir1)
-        if (dir2.is_dir) sessions_dir(options, true, dir2, queue1)
-        else error("Bad session directory: " + dir2.toString)
-      }
-      catch {
-        case ERROR(msg) =>
-          error(msg + "\nThe error(s) above occurred in session catalog " + catalog.toString)
-      })
-  }
-
   def find_sessions(options: Options, more_dirs: List[Path]): Session.Queue =
   {
-    var queue = Session.Queue.empty
-
-    for (dir <- Isabelle_System.components()) {
-      queue = sessions_dir(options, false, dir, queue)
-
-      val catalog = dir + SESSIONS
-      if (catalog.is_file) queue = sessions_catalog(options, dir, catalog, queue)
-    }
-
-    for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
-
-    queue
+    val queue1 =
+      (Session.Queue.empty /: Isabelle_System.components())(sessions_dir(options, false, _, _))
+    val queue2 = (queue1 /: more_dirs)(sessions_dir(options, true, _, _))
+    queue2
   }