1.1 --- a/doc-src/ROOT Thu Jul 26 11:52:08 2012 +0200
1.2 +++ b/doc-src/ROOT Thu Jul 26 12:27:47 2012 +0200
1.3 @@ -1,9 +1,9 @@
1.4 -session Classes! in "Classes/Thy" = HOL +
1.5 +session Classes! (doc) in "Classes/Thy" = HOL +
1.6 options [browser_info = false, document = false, document_dump = document, document_dump_only]
1.7 theories [document = false] Setup
1.8 theories Classes
1.9
1.10 -session Codegen! in "Codegen/Thy" = "HOL-Library" +
1.11 +session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
1.12 options [browser_info = false, document = false, document_dump = document, document_dump_only,
1.13 print_mode = "no_brackets,iff"]
1.14 theories [document = false] Setup
1.15 @@ -16,11 +16,11 @@
1.16 Adaptation
1.17 Further
1.18
1.19 -session Functions! in "Functions/Thy" = HOL +
1.20 +session Functions! (doc) in "Functions/Thy" = HOL +
1.21 options [browser_info = false, document = false, document_dump = document, document_dump_only]
1.22 theories Functions
1.23
1.24 -session IsarImplementation! in "IsarImplementation/Thy" = HOL +
1.25 +session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
1.26 options [browser_info = false, document = false, document_dump = document, document_dump_only]
1.27 theories
1.28 Eq
1.29 @@ -34,7 +34,7 @@
1.30 Syntax
1.31 Tactic
1.32
1.33 -session IsarRef in "IsarRef/Thy" = HOL +
1.34 +session IsarRef (doc) in "IsarRef/Thy" = HOL +
1.35 options [browser_info = false, document = false, document_dump = document, document_dump_only,
1.36 quick_and_dirty]
1.37 theories
1.38 @@ -54,17 +54,17 @@
1.39 Symbols
1.40 ML_Tactic
1.41
1.42 -session IsarRef in "IsarRef/Thy" = HOLCF +
1.43 +session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
1.44 options [browser_info = false, document = false, document_dump = document, document_dump_only,
1.45 quick_and_dirty]
1.46 theories HOLCF_Specific
1.47
1.48 -session IsarRef in "IsarRef/Thy" = ZF +
1.49 +session IsarRef (doc) in "IsarRef/Thy" = ZF +
1.50 options [browser_info = false, document = false, document_dump = document, document_dump_only,
1.51 quick_and_dirty]
1.52 theories ZF_Specific
1.53
1.54 -session LaTeXsugar! in "LaTeXsugar/Sugar" = HOL +
1.55 +session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
1.56 options [browser_info = false, document = false, document_dump = document, document_dump_only,
1.57 threads = 1] (* FIXME *)
1.58 theories [document_dump = ""]
1.59 @@ -72,18 +72,18 @@
1.60 "~~/src/HOL/Library/OptionalSugar"
1.61 theories Sugar
1.62
1.63 -session Locales! in "Locales/Locales" = HOL +
1.64 +session Locales! (doc) in "Locales/Locales" = HOL +
1.65 options [browser_info = false, document = false, document_dump = document, document_dump_only]
1.66 theories
1.67 Examples1
1.68 Examples2
1.69 Examples3
1.70
1.71 -session Main! in "Main/Docs" = HOL +
1.72 +session Main! (doc) in "Main/Docs" = HOL +
1.73 options [browser_info = false, document = false, document_dump = document, document_dump_only]
1.74 theories Main_Doc
1.75
1.76 -session ProgProve! in "ProgProve/Thys" = HOL +
1.77 +session ProgProve! (doc) in "ProgProve/Thys" = HOL +
1.78 options [browser_info = false, document = false, document_dump = document, document_dump_only,
1.79 show_question_marks = false]
1.80 theories
1.81 @@ -94,7 +94,7 @@
1.82 Logic
1.83 Isar
1.84
1.85 -session System! in "System/Thy" = Pure +
1.86 +session System! (doc) in "System/Thy" = Pure +
1.87 options [browser_info = false, document = false, document_dump = document, document_dump_only]
1.88 theories
1.89 Basics
1.90 @@ -103,9 +103,9 @@
1.91 Presentation
1.92 Misc
1.93
1.94 -(* session Tutorial in "Tutorial" = HOL + FIXME *)
1.95 +(* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
1.96
1.97 -session examples in "ZF" = ZF +
1.98 +session examples (doc) in "ZF" = ZF +
1.99 options [browser_info = false, document = false, document_dump = document, document_dump_only,
1.100 print_mode = "brackets"]
1.101 theories
2.1 --- a/lib/Tools/build Thu Jul 26 11:52:08 2012 +0200
2.2 +++ b/lib/Tools/build Thu Jul 26 12:27:47 2012 +0200
2.3 @@ -28,7 +28,8 @@
2.4 echo " Options are:"
2.5 echo " -a all sessions"
2.6 echo " -b build target images"
2.7 - echo " -d DIR additional session directory with ROOT file"
2.8 + echo " -d DIR include session directory with ROOT file"
2.9 + echo " -g NAME include session group NAME"
2.10 echo " -j INT maximum number of jobs (default 1)"
2.11 echo " -n no build -- test dependencies only"
2.12 echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)"
2.13 @@ -58,16 +59,16 @@
2.14
2.15 ALL_SESSIONS=false
2.16 BUILD_IMAGES=false
2.17 +declare -a MORE_DIRS=()
2.18 +declare -a SESSION_GROUPS=()
2.19 MAX_JOBS=1
2.20 NO_BUILD=false
2.21 +eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
2.22 SYSTEM_MODE=false
2.23 TIMING=false
2.24 VERBOSE=false
2.25
2.26 -declare -a MORE_DIRS=()
2.27 -eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
2.28 -
2.29 -while getopts "abd:j:no:stv" OPT
2.30 +while getopts "abd:g:j:no:stv" OPT
2.31 do
2.32 case "$OPT" in
2.33 a)
2.34 @@ -79,6 +80,9 @@
2.35 d)
2.36 MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
2.37 ;;
2.38 + g)
2.39 + SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
2.40 + ;;
2.41 j)
2.42 check_number "$OPTARG"
2.43 MAX_JOBS="$OPTARG"
2.44 @@ -122,8 +126,8 @@
2.45 fi
2.46
2.47 "$ISABELLE_TOOL" java isabelle.Build \
2.48 - "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" \
2.49 - "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
2.50 + "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \
2.51 + "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
2.52 RC="$?"
2.53
2.54 if [ "$NO_BUILD" = false ]; then
3.1 --- a/src/HOL/ROOT Thu Jul 26 11:52:08 2012 +0200
3.2 +++ b/src/HOL/ROOT Thu Jul 26 12:27:47 2012 +0200
3.3 @@ -1,4 +1,4 @@
3.4 -session HOL! in "." = Pure +
3.5 +session HOL! (main) in "." = Pure +
3.6 description {* Classical Higher-order Logic *}
3.7 options [document_graph]
3.8 theories Complex_Main
3.9 @@ -19,8 +19,8 @@
3.10 options [document = false]
3.11 theories Main
3.12
3.13 -session "HOL-Proofs"! in "." = Pure +
3.14 - description {* HOL-Main with proof terms *}
3.15 +session "HOL-Proofs"! (main) in "." = Pure +
3.16 + description {* HOL-Main with explicit proof terms *}
3.17 options [document = false, proofs = 2, parallel_proofs = 0]
3.18 theories Main
3.19
3.20 @@ -571,7 +571,7 @@
3.21 "ex/Koepf_Duermuth_Countermeasure"
3.22 files "document/root.tex"
3.23
3.24 -session Nominal = HOL +
3.25 +session Nominal (main) = HOL +
3.26 options [document = false]
3.27 theories Nominal
3.28
3.29 @@ -760,7 +760,7 @@
3.30 Predicate_Compile_Tests
3.31 Specialisation_Examples
3.32
3.33 -session HOLCF! = HOL +
3.34 +session HOLCF! (main) = HOL +
3.35 description {*
3.36 Author: Franz Regensburger
3.37 Author: Brian Huffman
4.1 --- a/src/Pure/System/build.scala Thu Jul 26 11:52:08 2012 +0200
4.2 +++ b/src/Pure/System/build.scala Thu Jul 26 12:27:47 2012 +0200
4.3 @@ -25,6 +25,7 @@
4.4
4.5 sealed case class Info(
4.6 base_name: String,
4.7 + groups: List[String],
4.8 dir: Path,
4.9 parent: Option[String],
4.10 parent_base_name: Option[String],
4.11 @@ -65,8 +66,15 @@
4.12
4.13 def - (name: String): Queue = new Queue(graph.del_node(name))
4.14
4.15 - def required(names: List[String]): Queue =
4.16 - new Queue(graph.restrict(graph.all_preds(names).toSet))
4.17 + def required(groups: List[String], names: List[String]): Queue =
4.18 + {
4.19 + val selected_group = groups.toSet
4.20 + val selected_name = names.toSet
4.21 + val selected =
4.22 + graph.keys.filter(name =>
4.23 + selected_name(name) || apply(name).groups.exists(selected_group)).toList
4.24 + new Queue(graph.restrict(graph.all_preds(selected).toSet))
4.25 + }
4.26
4.27 def dequeue(skip: String => Boolean): Option[(String, Info)] =
4.28 {
4.29 @@ -87,6 +95,7 @@
4.30 private case class Session_Entry(
4.31 name: String,
4.32 this_name: Boolean,
4.33 + groups: List[String],
4.34 path: Option[String],
4.35 parent: Option[String],
4.36 description: String,
4.37 @@ -121,13 +130,14 @@
4.38
4.39 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
4.40 (keyword("!") ^^^ true | success(false)) ~
4.41 + (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
4.42 (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
4.43 (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
4.44 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
4.45 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
4.46 rep(theories) ~
4.47 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
4.48 - { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
4.49 + { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
4.50 }
4.51
4.52 def parse_entries(root: JFile): List[Session_Entry] =
4.53 @@ -186,7 +196,7 @@
4.54 val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
4.55
4.56 val info =
4.57 - Session.Info(entry.name, dir + path, entry.parent, parent_base_name,
4.58 + Session.Info(entry.name, entry.groups, dir + path, entry.parent, parent_base_name,
4.59 entry.description, session_options, theories, files, digest)
4.60
4.61 queue1 + (full_name, info)
4.62 @@ -224,8 +234,8 @@
4.63 })
4.64 }
4.65
4.66 - def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
4.67 - more_dirs: List[Path]): Session.Queue =
4.68 + def find_sessions(options: Options, more_dirs: List[Path],
4.69 + all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
4.70 {
4.71 var queue = Session.Queue.empty
4.72
4.73 @@ -244,7 +254,7 @@
4.74 case bad => error("Undefined session(s): " + commas_quote(bad))
4.75 }
4.76
4.77 - if (all_sessions) queue else queue.required(sessions)
4.78 + if (all_sessions) queue else queue.required(session_groups, sessions)
4.79 }
4.80
4.81
4.82 @@ -419,12 +429,21 @@
4.83
4.84 /* build */
4.85
4.86 - def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
4.87 - no_build: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean,
4.88 - more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
4.89 + def build(
4.90 + all_sessions: Boolean = false,
4.91 + build_images: Boolean = false,
4.92 + more_dirs: List[Path] = Nil,
4.93 + session_groups: List[String] = Nil,
4.94 + max_jobs: Int = 1,
4.95 + no_build: Boolean = false,
4.96 + build_options: List[String] = Nil,
4.97 + system_mode: Boolean = false,
4.98 + timing: Boolean = false,
4.99 + verbose: Boolean = false,
4.100 + sessions: List[String] = Nil): Int =
4.101 {
4.102 - val options = (Options.init() /: more_options)(_.define_simple(_))
4.103 - val queue = find_sessions(options, all_sessions, sessions, more_dirs)
4.104 + val options = (Options.init() /: build_options)(_.define_simple(_))
4.105 + val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
4.106 val deps = dependencies(verbose, queue)
4.107
4.108 def make_stamp(name: String): String =
4.109 @@ -534,9 +553,9 @@
4.110 Properties.Value.Boolean(system_mode) ::
4.111 Properties.Value.Boolean(timing) ::
4.112 Properties.Value.Boolean(verbose) ::
4.113 - Command_Line.Chunks(more_dirs, options, sessions) =>
4.114 - build(all_sessions, build_images, max_jobs, no_build, system_mode, timing,
4.115 - verbose, more_dirs.map(Path.explode), options, sessions)
4.116 + Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
4.117 + build(all_sessions, build_images, more_dirs.map(Path.explode), session_groups,
4.118 + max_jobs, no_build, build_options, system_mode, timing, verbose, sessions)
4.119 case _ => error("Bad arguments:\n" + cat_lines(args))
4.120 }
4.121 }