# HG changeset patch # User wenzelm # Date 1475832298 -7200 # Node ID 2e5c0bd708af8f980afcd90e079c55940d8b724e # Parent ff26032b7f2abee5f9f83d50532272199e5649dc clarified modules; CI_Profile: show all settings; diff -r ff26032b7f2a -r 2e5c0bd708af src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Oct 07 11:10:17 2016 +0200 +++ b/src/Pure/Tools/build.scala Fri Oct 07 11:24:58 2016 +0200 @@ -686,16 +686,8 @@ /* Isabelle tool wrapper */ - val build_settings = List("ISABELLE_BUILD_OPTIONS") - val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS") - val all_settings = build_settings ::: ml_settings - val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args => { - def show(a: String): String = a + "=" + quote(Isabelle_System.getenv(a)) - def show_settings(): String = - cat_lines(build_settings.map(show(_)) ::: List("") ::: ml_settings.map(show(_))) - val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var select_dirs: List[Path] = Nil @@ -738,7 +730,7 @@ Build and manage Isabelle sessions, depending on implicit settings: -""" + Library.prefix_lines(" ", show_settings()), +""" + Library.prefix_lines(" ", Build_Log.Setting.show_all()), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "R" -> (_ => requirements = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), @@ -765,7 +757,7 @@ Library.trim_line( Isabelle_System.bash( """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n") - progress.echo(show_settings() + "\n") + progress.echo(Build_Log.Setting.show_all() + "\n") } val start_time = Time.now() diff -r ff26032b7f2a -r 2e5c0bd708af src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Fri Oct 07 11:10:17 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Fri Oct 07 11:24:58 2016 +0200 @@ -16,6 +16,22 @@ object Build_Log { + /** build settings **/ + + val build_settings = List("ISABELLE_BUILD_OPTIONS") + val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS") + val all_settings = build_settings ::: ml_settings + + object Setting + { + def apply(a: String, b: String): String = a + "=" + quote(b) + def getenv(a: String): String = apply(a, Isabelle_System.getenv(a)) + + def show_all(): String = + cat_lines(build_settings.map(getenv(_)) ::: List("") ::: ml_settings.map(getenv(_))) + } + + /** log file **/ object Log_File @@ -167,7 +183,7 @@ Field.build_end -> end_date.toString, Field.isabelle_version -> isabelle_version, Field.afp_version -> afp_version), - log_file.get_settings(Build.all_settings)) + log_file.get_settings(all_settings)) case _ => log_file.err("cannot detect start/end date in afp-test log") } @@ -213,7 +229,7 @@ case i => val a = s.substring(0, i) Library.try_unquote(s.substring(i + 1)) match { - case Some(b) if Build.ml_settings.contains(a) => Some((a, b)) + case Some(b) if ml_settings.contains(a) => Some((a, b)) case _ => None } } diff -r ff26032b7f2a -r 2e5c0bd708af src/Pure/Tools/ci_profile.scala --- a/src/Pure/Tools/ci_profile.scala Fri Oct 07 11:10:17 2016 +0200 +++ b/src/Pure/Tools/ci_profile.scala Fri Oct 07 11:24:58 2016 +0200 @@ -86,7 +86,7 @@ override final def apply(args: List[String]): Unit = { print_section("CONFIGURATION") - Build.ml_settings.foreach(a => println(a + "=" + quote(Isabelle_System.getenv(a)))) + println(Build_Log.Setting.show_all()) val props = load_properties() System.getProperties().putAll(props)