more uniform treatment of settings;
authorwenzelm
Fri Oct 07 11:45:30 2016 +0200 (2016-10-07)
changeset 6408138bb09ed965b
parent 64080 2e5c0bd708af
child 64082 d57c7295f601
more uniform treatment of settings;
src/Pure/Tools/build.scala
src/Pure/Tools/build_log.scala
src/Pure/Tools/ci_profile.scala
     1.1 --- a/src/Pure/Tools/build.scala	Fri Oct 07 11:24:58 2016 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Oct 07 11:45:30 2016 +0200
     1.3 @@ -730,7 +730,7 @@
     1.4  
     1.5    Build and manage Isabelle sessions, depending on implicit settings:
     1.6  
     1.7 -""" + Library.prefix_lines("  ", Build_Log.Setting.show_all()),
     1.8 +""" + Library.prefix_lines("  ", Build_Log.Settings.show()),
     1.9        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    1.10        "R" -> (_ => requirements = true),
    1.11        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    1.12 @@ -757,7 +757,7 @@
    1.13          Library.trim_line(
    1.14            Isabelle_System.bash(
    1.15              """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
    1.16 -      progress.echo(Build_Log.Setting.show_all() + "\n")
    1.17 +      progress.echo(Build_Log.Settings.show() + "\n")
    1.18      }
    1.19  
    1.20      val start_time = Time.now()
     2.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 11:24:58 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 11:45:30 2016 +0200
     2.3 @@ -16,19 +16,34 @@
     2.4  
     2.5  object Build_Log
     2.6  {
     2.7 -  /** build settings **/
     2.8 +  /** settings **/
     2.9  
    2.10 -  val build_settings = List("ISABELLE_BUILD_OPTIONS")
    2.11 -  val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    2.12 -  val all_settings = build_settings ::: ml_settings
    2.13 +  object Settings
    2.14 +  {
    2.15 +    val build_settings = List("ISABELLE_BUILD_OPTIONS")
    2.16 +    val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    2.17 +    val all_settings = build_settings ::: ml_settings
    2.18 +
    2.19 +    type Entry = (String, String)
    2.20 +    type T = List[Entry]
    2.21  
    2.22 -  object Setting
    2.23 -  {
    2.24 -    def apply(a: String, b: String): String = a + "=" + quote(b)
    2.25 -    def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
    2.26 +    object Entry
    2.27 +    {
    2.28 +      def unapply(s: String): Option[Entry] =
    2.29 +        s.indexOf('=') match {
    2.30 +          case -1 => None
    2.31 +          case i =>
    2.32 +            val a = s.substring(0, i)
    2.33 +            val b = Library.perhaps_unquote(s.substring(i + 1))
    2.34 +            Some((a, b))
    2.35 +        }
    2.36 +      def apply(a: String, b: String): String = a + "=" + quote(b)
    2.37 +      def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
    2.38 +    }
    2.39  
    2.40 -    def show_all(): String =
    2.41 -      cat_lines(build_settings.map(getenv(_)) ::: List("") ::: ml_settings.map(getenv(_)))
    2.42 +    def show(): String =
    2.43 +      cat_lines(
    2.44 +        build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
    2.45    }
    2.46  
    2.47  
    2.48 @@ -67,11 +82,11 @@
    2.49  
    2.50      /* settings */
    2.51  
    2.52 -    def get_setting(setting: String): String =
    2.53 -      lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting)
    2.54 +    def get_setting(a: String): Settings.Entry =
    2.55 +      Settings.Entry.unapply(
    2.56 +        lines.find(_.startsWith(a + "=")) getOrElse err("missing " + a)).get
    2.57  
    2.58 -    def get_settings(settings: List[String]): List[String] =
    2.59 -      settings.map(get_setting(_))
    2.60 +    def get_settings(as: List[String]): Settings.T = as.map(get_setting(_))
    2.61  
    2.62  
    2.63      /* properties (YXML) */
    2.64 @@ -139,7 +154,8 @@
    2.65      val JENKINS = Value("jenkins")
    2.66    }
    2.67  
    2.68 -  sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String])
    2.69 +  sealed case class Header(
    2.70 +    kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
    2.71  
    2.72    object Field
    2.73    {
    2.74 @@ -183,7 +199,7 @@
    2.75                  Field.build_end -> end_date.toString,
    2.76                  Field.isabelle_version -> isabelle_version,
    2.77                  Field.afp_version -> afp_version),
    2.78 -              log_file.get_settings(all_settings))
    2.79 +              log_file.get_settings(Settings.all_settings))
    2.80  
    2.81            case _ => log_file.err("cannot detect start/end date in afp-test log")
    2.82          }
    2.83 @@ -203,7 +219,7 @@
    2.84    /* main log: produced by isatest, afp-test, jenkins etc. */
    2.85  
    2.86    sealed case class Info(
    2.87 -    ml_options: List[(String, String)],
    2.88 +    settings: List[(String, String)],
    2.89      finished: Map[String, Timing],
    2.90      timing: Map[String, Timing],
    2.91      threads: Map[String, Int])
    2.92 @@ -221,23 +237,9 @@
    2.93    private val Session_Timing =
    2.94      new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
    2.95  
    2.96 -  private object ML_Option
    2.97 -  {
    2.98 -    def unapply(s: String): Option[(String, String)] =
    2.99 -      s.indexOf('=') match {
   2.100 -        case -1 => None
   2.101 -        case i =>
   2.102 -          val a = s.substring(0, i)
   2.103 -          Library.try_unquote(s.substring(i + 1)) match {
   2.104 -            case Some(b) if ml_settings.contains(a) => Some((a, b))
   2.105 -            case _ => None
   2.106 -          }
   2.107 -      }
   2.108 -  }
   2.109 -
   2.110    private def parse_info(log_file: Log_File): Info =
   2.111    {
   2.112 -    val ml_options = new mutable.ListBuffer[(String, String)]
   2.113 +    val settings = new mutable.ListBuffer[(String, String)]
   2.114      var finished = Map.empty[String, Timing]
   2.115      var timing = Map.empty[String, Timing]
   2.116      var threads = Map.empty[String, Int]
   2.117 @@ -261,11 +263,12 @@
   2.118            val gc = Time.seconds(g)
   2.119            timing += (name -> Timing(elapsed, cpu, gc))
   2.120            threads += (name -> t)
   2.121 -        case ML_Option(a, b) => ml_options += (a -> b)
   2.122 +        case Settings.Entry(a, b) if Settings.all_settings.contains(a) =>
   2.123 +          settings += (a -> b)
   2.124          case _ =>
   2.125        }
   2.126      }
   2.127  
   2.128 -    Info(ml_options.toList, finished, timing, threads)
   2.129 +    Info(settings.toList, finished, timing, threads)
   2.130    }
   2.131  }
     3.1 --- a/src/Pure/Tools/ci_profile.scala	Fri Oct 07 11:24:58 2016 +0200
     3.2 +++ b/src/Pure/Tools/ci_profile.scala	Fri Oct 07 11:45:30 2016 +0200
     3.3 @@ -86,7 +86,7 @@
     3.4    override final def apply(args: List[String]): Unit =
     3.5    {
     3.6      print_section("CONFIGURATION")
     3.7 -    println(Build_Log.Setting.show_all())
     3.8 +    println(Build_Log.Settings.show())
     3.9      val props = load_properties()
    3.10      System.getProperties().putAll(props)
    3.11