# HG changeset patch # User wenzelm # Date 1475833530 -7200 # Node ID 38bb09ed965b6ce70443d6419c0569c7c9feb321 # Parent 2e5c0bd708af8f980afcd90e079c55940d8b724e more uniform treatment of settings; diff -r 2e5c0bd708af -r 38bb09ed965b src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Oct 07 11:24:58 2016 +0200 +++ b/src/Pure/Tools/build.scala Fri Oct 07 11:45:30 2016 +0200 @@ -730,7 +730,7 @@ Build and manage Isabelle sessions, depending on implicit settings: -""" + Library.prefix_lines(" ", Build_Log.Setting.show_all()), +""" + Library.prefix_lines(" ", Build_Log.Settings.show()), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "R" -> (_ => requirements = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), @@ -757,7 +757,7 @@ Library.trim_line( Isabelle_System.bash( """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n") - progress.echo(Build_Log.Setting.show_all() + "\n") + progress.echo(Build_Log.Settings.show() + "\n") } val start_time = Time.now() diff -r 2e5c0bd708af -r 38bb09ed965b src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Fri Oct 07 11:24:58 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Fri Oct 07 11:45:30 2016 +0200 @@ -16,19 +16,34 @@ object Build_Log { - /** build settings **/ + /** 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 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 + + type Entry = (String, String) + type T = List[Entry] - object Setting - { - def apply(a: String, b: String): String = a + "=" + quote(b) - def getenv(a: String): String = apply(a, Isabelle_System.getenv(a)) + object Entry + { + def unapply(s: String): Option[Entry] = + s.indexOf('=') match { + case -1 => None + case i => + val a = s.substring(0, i) + val b = Library.perhaps_unquote(s.substring(i + 1)) + Some((a, b)) + } + 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(_))) + def show(): String = + cat_lines( + build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_))) } @@ -67,11 +82,11 @@ /* settings */ - def get_setting(setting: String): String = - lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting) + def get_setting(a: String): Settings.Entry = + Settings.Entry.unapply( + lines.find(_.startsWith(a + "=")) getOrElse err("missing " + a)).get - def get_settings(settings: List[String]): List[String] = - settings.map(get_setting(_)) + def get_settings(as: List[String]): Settings.T = as.map(get_setting(_)) /* properties (YXML) */ @@ -139,7 +154,8 @@ val JENKINS = Value("jenkins") } - sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String]) + sealed case class Header( + kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)]) object Field { @@ -183,7 +199,7 @@ Field.build_end -> end_date.toString, Field.isabelle_version -> isabelle_version, Field.afp_version -> afp_version), - log_file.get_settings(all_settings)) + log_file.get_settings(Settings.all_settings)) case _ => log_file.err("cannot detect start/end date in afp-test log") } @@ -203,7 +219,7 @@ /* main log: produced by isatest, afp-test, jenkins etc. */ sealed case class Info( - ml_options: List[(String, String)], + settings: List[(String, String)], finished: Map[String, Timing], timing: Map[String, Timing], threads: Map[String, Int]) @@ -221,23 +237,9 @@ private val Session_Timing = new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") - private object ML_Option - { - def unapply(s: String): Option[(String, String)] = - s.indexOf('=') match { - case -1 => None - case i => - val a = s.substring(0, i) - Library.try_unquote(s.substring(i + 1)) match { - case Some(b) if ml_settings.contains(a) => Some((a, b)) - case _ => None - } - } - } - private def parse_info(log_file: Log_File): Info = { - val ml_options = new mutable.ListBuffer[(String, String)] + val settings = new mutable.ListBuffer[(String, String)] var finished = Map.empty[String, Timing] var timing = Map.empty[String, Timing] var threads = Map.empty[String, Int] @@ -261,11 +263,12 @@ val gc = Time.seconds(g) timing += (name -> Timing(elapsed, cpu, gc)) threads += (name -> t) - case ML_Option(a, b) => ml_options += (a -> b) + case Settings.Entry(a, b) if Settings.all_settings.contains(a) => + settings += (a -> b) case _ => } } - Info(ml_options.toList, finished, timing, threads) + Info(settings.toList, finished, timing, threads) } } diff -r 2e5c0bd708af -r 38bb09ed965b src/Pure/Tools/ci_profile.scala --- a/src/Pure/Tools/ci_profile.scala Fri Oct 07 11:24:58 2016 +0200 +++ b/src/Pure/Tools/ci_profile.scala Fri Oct 07 11:45:30 2016 +0200 @@ -86,7 +86,7 @@ override final def apply(args: List[String]): Unit = { print_section("CONFIGURATION") - println(Build_Log.Setting.show_all()) + println(Build_Log.Settings.show()) val props = load_properties() System.getProperties().putAll(props)