allow explicit specification of additional session directories;

--- a/lib/Tools/build	Wed Jul 18 17:27:28 2012 +0200
+++ b/lib/Tools/build	Wed Jul 18 19:47:10 2012 +0200
@@ -17,6 +17,7 @@
   echo "  Options are:"
   echo "    -a           all sessions"
   echo "    -b           build target images"
+  echo "    -d DIR       additional session directory with ROOT file"
   echo "    -l           list sessions only"
   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
   echo
@@ -44,9 +45,10 @@
 BUILD_IMAGES=false
 LIST_ONLY=false
 
+declare -a MORE_DIRS=()
 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
 
-while getopts "ablo:" OPT
+while getopts "abd:lo:" OPT
 do
   case "$OPT" in
     a)
@@ -55,6 +57,9 @@
     b)
       BUILD_IMAGES="true"
       ;;
+    d)
+      MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
+      ;;
     l)
       LIST_ONLY="true"
       ;;
@@ -75,4 +80,5 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 exec "$ISABELLE_TOOL" java isabelle.Build \
-  "$ALL_SESSIONS" "$BUILD_IMAGES" "$LIST_ONLY" "${BUILD_OPTIONS[@]}" $'\n' "$@"
+  "$ALL_SESSIONS" "$BUILD_IMAGES" "$LIST_ONLY" \
+  "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"

--- a/src/Pure/System/build.scala	Wed Jul 18 17:27:28 2012 +0200
+++ b/src/Pure/System/build.scala	Wed Jul 18 19:47:10 2012 +0200
@@ -10,6 +10,7 @@
 import java.io.File
 
 import scala.collection.mutable
+import scala.annotation.tailrec
 
 
 object Build
@@ -26,28 +27,33 @@
       }
   }
 
+  private object Chunks
+  {
+    private def chunks(list: List[String]): List[List[String]] =
+      list.indexWhere(_ == "\n") match {
+        case -1 => List(list)
+        case i =>
+          val (chunk, rest) = list.splitAt(i)
+          chunk :: chunks(rest.tail)
+      }
+    def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
+  }
+
   def main(args: Array[String])
   {
-    def bad_args(): Nothing = error("Bad arguments: " + args.toString)
-
     val rc =
       try {
         args.toList match {
-          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
-            rest.indexWhere(_ == "\n") match {
-              case -1 => bad_args()
-              case i =>
-                val (options, rest1) = rest.splitAt(i)
-                val sessions = rest1.tail
-                build(all_sessions, build_images, list_only, options, sessions)
-            }
-          case _ => bad_args()
+          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) ::
+            Chunks(more_dirs, options, sessions) =>
+              build(all_sessions, build_images, list_only,
+                more_dirs.map(Path.explode), options, sessions)
+          case _ => error("Bad arguments:\n" + cat_lines(args))
         }
       }
       catch {
         case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
       }
-
     sys.exit(rc)
   }
 
@@ -55,12 +61,13 @@
   /* build */
 
   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
-    options: List[String], sessions: List[String]): Int =
+    more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   {
+    println("more_dirs = " + more_dirs.toString)
     println("options = " + options.toString)
     println("sessions = " + sessions.toString)
 
-    find_sessions() foreach println
+    find_sessions(more_dirs) foreach println
 
     0
   }
@@ -147,14 +154,15 @@
 
   /* find session */
 
-  def find_sessions(more_dirs: List[Path] = Nil): List[Session_Info] =
+  def find_sessions(more_dirs: List[Path]): List[Session_Info] =
   {
     val infos = new mutable.ListBuffer[Session_Info]
     infos += pure_info
 
     for {
-      dir <- Isabelle_System.components() ++ more_dirs
+      (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true))
       root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
+      _ = (strict && !root.isFile && error("Bad session root file: " + quote(root.toString)))
       if root.isFile
       entry <- Parser.parse_entries(root)
     }