# HG changeset patch
# User wenzelm
# Date 1343298467 -7200
# Node ID 4854ced3e9d77a2b54db5e1a2c4a49b3cc911537
# Parent  5a59e4c0395762b4693cd519469db3b166944514
support session groups;
tuned signature;

diff -r 5a59e4c03957 -r 4854ced3e9d7 doc-src/ROOT
--- a/doc-src/ROOT	Thu Jul 26 11:52:08 2012 +0200
+++ b/doc-src/ROOT	Thu Jul 26 12:27:47 2012 +0200
@@ -1,9 +1,9 @@
-session Classes! in "Classes/Thy" = HOL +
+session Classes! (doc) in "Classes/Thy" = HOL +
   options [browser_info = false, document = false, document_dump = document, document_dump_only]
   theories [document = false] Setup
   theories Classes
 
-session Codegen! in "Codegen/Thy" = "HOL-Library" +
+session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
   options [browser_info = false, document = false, document_dump = document, document_dump_only,
     print_mode = "no_brackets,iff"]
   theories [document = false] Setup
@@ -16,11 +16,11 @@
     Adaptation
     Further
 
-session Functions! in "Functions/Thy" = HOL +
+session Functions! (doc) in "Functions/Thy" = HOL +
   options [browser_info = false, document = false, document_dump = document, document_dump_only]
   theories Functions
 
-session IsarImplementation! in "IsarImplementation/Thy" = HOL +
+session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
   options [browser_info = false, document = false, document_dump = document, document_dump_only]
   theories
     Eq
@@ -34,7 +34,7 @@
     Syntax
     Tactic
 
-session IsarRef in "IsarRef/Thy" = HOL +
+session IsarRef (doc) in "IsarRef/Thy" = HOL +
   options [browser_info = false, document = false, document_dump = document, document_dump_only,
     quick_and_dirty]
   theories
@@ -54,17 +54,17 @@
     Symbols
     ML_Tactic
 
-session IsarRef in "IsarRef/Thy" = HOLCF +
+session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
   options [browser_info = false, document = false, document_dump = document, document_dump_only,
     quick_and_dirty]
   theories HOLCF_Specific
 
-session IsarRef in "IsarRef/Thy" = ZF +
+session IsarRef (doc) in "IsarRef/Thy" = ZF +
   options [browser_info = false, document = false, document_dump = document, document_dump_only,
     quick_and_dirty]
   theories ZF_Specific
 
-session LaTeXsugar! in "LaTeXsugar/Sugar" = HOL +
+session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
   options [browser_info = false, document = false, document_dump = document, document_dump_only,
     threads = 1]  (* FIXME *)
   theories [document_dump = ""]
@@ -72,18 +72,18 @@
     "~~/src/HOL/Library/OptionalSugar"
   theories Sugar
 
-session Locales! in "Locales/Locales" = HOL +
+session Locales! (doc) in "Locales/Locales" = HOL +
   options [browser_info = false, document = false, document_dump = document, document_dump_only]
   theories
     Examples1
     Examples2
     Examples3
 
-session Main! in "Main/Docs" = HOL +
+session Main! (doc) in "Main/Docs" = HOL +
   options [browser_info = false, document = false, document_dump = document, document_dump_only]
   theories Main_Doc
 
-session ProgProve! in "ProgProve/Thys" = HOL +
+session ProgProve! (doc) in "ProgProve/Thys" = HOL +
   options [browser_info = false, document = false, document_dump = document, document_dump_only,
     show_question_marks = false]
   theories
@@ -94,7 +94,7 @@
     Logic
     Isar
 
-session System! in "System/Thy" = Pure +
+session System! (doc) in "System/Thy" = Pure +
   options [browser_info = false, document = false, document_dump = document, document_dump_only]
   theories
     Basics
@@ -103,9 +103,9 @@
     Presentation
     Misc
 
-(* session Tutorial in "Tutorial" = HOL + FIXME *)
+(* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
 
-session examples in "ZF" = ZF +
+session examples (doc) in "ZF" = ZF +
   options [browser_info = false, document = false, document_dump = document, document_dump_only,
     print_mode = "brackets"]
   theories
diff -r 5a59e4c03957 -r 4854ced3e9d7 lib/Tools/build
--- a/lib/Tools/build	Thu Jul 26 11:52:08 2012 +0200
+++ b/lib/Tools/build	Thu Jul 26 12:27:47 2012 +0200
@@ -28,7 +28,8 @@
   echo "  Options are:"
   echo "    -a           all sessions"
   echo "    -b           build target images"
-  echo "    -d DIR       additional session directory with ROOT file"
+  echo "    -d DIR       include session directory with ROOT file"
+  echo "    -g NAME      include session group NAME"
   echo "    -j INT       maximum number of jobs (default 1)"
   echo "    -n           no build -- test dependencies only"
   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
@@ -58,16 +59,16 @@
 
 ALL_SESSIONS=false
 BUILD_IMAGES=false
+declare -a MORE_DIRS=()
+declare -a SESSION_GROUPS=()
 MAX_JOBS=1
 NO_BUILD=false
+eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
 SYSTEM_MODE=false
 TIMING=false
 VERBOSE=false
 
-declare -a MORE_DIRS=()
-eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
-
-while getopts "abd:j:no:stv" OPT
+while getopts "abd:g:j:no:stv" OPT
 do
   case "$OPT" in
     a)
@@ -79,6 +80,9 @@
     d)
       MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
       ;;
+    g)
+      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
+      ;;
     j)
       check_number "$OPTARG"
       MAX_JOBS="$OPTARG"
@@ -122,8 +126,8 @@
 fi
 
 "$ISABELLE_TOOL" java isabelle.Build \
-  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" \
-  "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
+  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \
+  "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
 RC="$?"
 
 if [ "$NO_BUILD" = false ]; then
diff -r 5a59e4c03957 -r 4854ced3e9d7 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Jul 26 11:52:08 2012 +0200
+++ b/src/HOL/ROOT	Thu Jul 26 12:27:47 2012 +0200
@@ -1,4 +1,4 @@
-session HOL! in "." = Pure +
+session HOL! (main) in "." = Pure +
   description {* Classical Higher-order Logic *}
   options [document_graph]
   theories Complex_Main
@@ -19,8 +19,8 @@
   options [document = false]
   theories Main
 
-session "HOL-Proofs"! in "." = Pure +
-  description {* HOL-Main with proof terms *}
+session "HOL-Proofs"! (main) in "." = Pure +
+  description {* HOL-Main with explicit proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Main
 
@@ -571,7 +571,7 @@
     "ex/Koepf_Duermuth_Countermeasure"
   files "document/root.tex"
 
-session Nominal = HOL +
+session Nominal (main) = HOL +
   options [document = false]
   theories Nominal
 
@@ -760,7 +760,7 @@
     Predicate_Compile_Tests
     Specialisation_Examples
 
-session HOLCF! = HOL +
+session HOLCF! (main) = HOL +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman
diff -r 5a59e4c03957 -r 4854ced3e9d7 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Jul 26 11:52:08 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Jul 26 12:27:47 2012 +0200
@@ -25,6 +25,7 @@
 
     sealed case class Info(
       base_name: String,
+      groups: List[String],
       dir: Path,
       parent: Option[String],
       parent_base_name: Option[String],
@@ -65,8 +66,15 @@
 
       def - (name: String): Queue = new Queue(graph.del_node(name))
 
-      def required(names: List[String]): Queue =
-        new Queue(graph.restrict(graph.all_preds(names).toSet))
+      def required(groups: List[String], names: List[String]): Queue =
+      {
+        val selected_group = groups.toSet
+        val selected_name = names.toSet
+        val selected =
+          graph.keys.filter(name =>
+            selected_name(name) || apply(name).groups.exists(selected_group)).toList
+        new Queue(graph.restrict(graph.all_preds(selected).toSet))
+      }
 
       def dequeue(skip: String => Boolean): Option[(String, Info)] =
       {
@@ -87,6 +95,7 @@
   private case class Session_Entry(
     name: String,
     this_name: Boolean,
+    groups: List[String],
     path: Option[String],
     parent: Option[String],
     description: String,
@@ -121,13 +130,14 @@
 
       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
         (keyword("!") ^^^ true | success(false)) ~
+        (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
         (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
         rep(theories) ~
         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
-          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
+          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
     }
 
     def parse_entries(root: JFile): List[Session_Entry] =
@@ -186,7 +196,7 @@
         val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
 
         val info =
-          Session.Info(entry.name, dir + path, entry.parent, parent_base_name,
+          Session.Info(entry.name, entry.groups, dir + path, entry.parent, parent_base_name,
             entry.description, session_options, theories, files, digest)
 
         queue1 + (full_name, info)
@@ -224,8 +234,8 @@
       })
   }
 
-  def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
-    more_dirs: List[Path]): Session.Queue =
+  def find_sessions(options: Options, more_dirs: List[Path],
+    all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
   {
     var queue = Session.Queue.empty
 
@@ -244,7 +254,7 @@
       case bad => error("Undefined session(s): " + commas_quote(bad))
     }
 
-    if (all_sessions) queue else queue.required(sessions)
+    if (all_sessions) queue else queue.required(session_groups, sessions)
   }
 
 
@@ -419,12 +429,21 @@
 
   /* build */
 
-  def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
-    no_build: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean,
-    more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
+  def build(
+    all_sessions: Boolean = false,
+    build_images: Boolean = false,
+    more_dirs: List[Path] = Nil,
+    session_groups: List[String] = Nil,
+    max_jobs: Int = 1,
+    no_build: Boolean = false,
+    build_options: List[String] = Nil,
+    system_mode: Boolean = false,
+    timing: Boolean = false,
+    verbose: Boolean = false,
+    sessions: List[String] = Nil): Int =
   {
-    val options = (Options.init() /: more_options)(_.define_simple(_))
-    val queue = find_sessions(options, all_sessions, sessions, more_dirs)
+    val options = (Options.init() /: build_options)(_.define_simple(_))
+    val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
     val deps = dependencies(verbose, queue)
 
     def make_stamp(name: String): String =
@@ -534,9 +553,9 @@
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(timing) ::
           Properties.Value.Boolean(verbose) ::
-          Command_Line.Chunks(more_dirs, options, sessions) =>
-            build(all_sessions, build_images, max_jobs, no_build, system_mode, timing,
-              verbose, more_dirs.map(Path.explode), options, sessions)
+          Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
+            build(all_sessions, build_images, more_dirs.map(Path.explode), session_groups,
+              max_jobs, no_build, build_options, system_mode, timing, verbose, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }