1/* Title: Pure/System/options.scala 2 Author: Makarius 3 4System options with external string representation. 5*/ 6 7package isabelle 8 9 10object Options 11{ 12 type Spec = (String, Option[String]) 13 14 val empty: Options = new Options() 15 16 17 /* representation */ 18 19 sealed abstract class Type 20 { 21 def print: String = Word.lowercase(toString) 22 } 23 case object Bool extends Type 24 case object Int extends Type 25 case object Real extends Type 26 case object String extends Type 27 case object Unknown extends Type 28 29 case class Opt( 30 public: Boolean, 31 pos: Position.T, 32 name: String, 33 typ: Type, 34 value: String, 35 default_value: String, 36 description: String, 37 section: String) 38 { 39 private def print(default: Boolean): String = 40 { 41 val x = if (default) default_value else value 42 "option " + name + " : " + typ.print + " = " + 43 (if (typ == Options.String) quote(x) else x) + 44 (if (description == "") "" else "\n -- " + quote(description)) 45 } 46 47 def print: String = print(false) 48 def print_default: String = print(true) 49 50 def title(strip: String = ""): String = 51 { 52 val words = Word.explode('_', name) 53 val words1 = 54 words match { 55 case word :: rest if word == strip => rest 56 case _ => words 57 } 58 Word.implode(words1.map(Word.perhaps_capitalize(_))) 59 } 60 61 def unknown: Boolean = typ == Unknown 62 } 63 64 65 /* parsing */ 66 67 private val SECTION = "section" 68 private val PUBLIC = "public" 69 private val OPTION = "option" 70 private val OPTIONS = Path.explode("etc/options") 71 private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences") 72 73 val options_syntax = 74 Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded + 75 (SECTION, Keyword.DOCUMENT_HEADING) + 76 (PUBLIC, Keyword.BEFORE_COMMAND) + 77 (OPTION, Keyword.THY_DECL) 78 79 val prefs_syntax = Outer_Syntax.empty + "=" 80 81 trait Parser extends Parse.Parser 82 { 83 val option_name = atom("option name", _.is_name) 84 val option_type = atom("option type", _.is_name) 85 val option_value = 86 opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^ 87 { case s ~ n => if (s.isDefined) "-" + n else n } | 88 atom("option value", tok => tok.is_name || tok.is_float) 89 } 90 91 private object Parser extends Parser 92 { 93 def comment_marker: Parser[String] = 94 $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded) 95 96 val option_entry: Parser[Options => Options] = 97 { 98 command(SECTION) ~! text ^^ 99 { case _ ~ a => (options: Options) => options.set_section(a) } | 100 opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~ 101 $$$("=") ~ option_value ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^ 102 { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) => 103 (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) } 104 } 105 106 val prefs_entry: Parser[Options => Options] = 107 { 108 option_name ~ ($$$("=") ~! option_value) ^^ 109 { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) } 110 } 111 112 def parse_file(options: Options, file_name: String, content: String, 113 syntax: Outer_Syntax = options_syntax, 114 parser: Parser[Options => Options] = option_entry): Options = 115 { 116 val toks = Token.explode(syntax.keywords, content) 117 val ops = 118 parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file_name))) match { 119 case Success(result, _) => result 120 case bad => error(bad.toString) 121 } 122 try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } } 123 catch { case ERROR(msg) => error(msg + Position.File(file_name)) } 124 } 125 126 def parse_prefs(options: Options, content: String): Options = 127 parse_file(options, PREFS.file_name, content, syntax = prefs_syntax, parser = prefs_entry) 128 } 129 130 def read_prefs(file: Path = PREFS): String = 131 if (file.is_file) File.read(file) else "" 132 133 def init(prefs: String = read_prefs(PREFS), opts: List[String] = Nil): Options = 134 { 135 var options = empty 136 for { 137 dir <- Isabelle_System.components() 138 file = dir + OPTIONS if file.is_file 139 } { options = Parser.parse_file(options, file.implode, File.read(file)) } 140 (Options.Parser.parse_prefs(options, prefs) /: opts)(_ + _) 141 } 142 143 144 /* encode */ 145 146 val encode: XML.Encode.T[Options] = (options => options.encode) 147 148 149 /* Isabelle tool wrapper */ 150 151 val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options", args => 152 { 153 var build_options = false 154 var get_option = "" 155 var list_options = false 156 var export_file = "" 157 158 val getopts = Getopts(""" 159Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] 160 161 Options are: 162 -b include $ISABELLE_BUILD_OPTIONS 163 -g OPTION get value of OPTION 164 -l list options 165 -x FILE export options to FILE in YXML format 166 167 Report Isabelle system options, augmented by MORE_OPTIONS given as 168 arguments NAME=VAL or NAME. 169""", 170 "b" -> (_ => build_options = true), 171 "g:" -> (arg => get_option = arg), 172 "l" -> (_ => list_options = true), 173 "x:" -> (arg => export_file = arg)) 174 175 val more_options = getopts(args) 176 if (get_option == "" && !list_options && export_file == "") getopts.usage() 177 178 val options = 179 { 180 val options0 = Options.init() 181 val options1 = 182 if (build_options) 183 (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _) 184 else options0 185 (options1 /: more_options)(_ + _) 186 } 187 188 if (get_option != "") 189 Output.writeln(options.check_name(get_option).value, stdout = true) 190 191 if (export_file != "") 192 File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) 193 194 if (get_option == "" && export_file == "") 195 Output.writeln(options.print, stdout = true) 196 }) 197} 198 199 200final class Options private( 201 val options: Map[String, Options.Opt] = Map.empty, 202 val section: String = "") 203{ 204 override def toString: String = options.iterator.mkString("Options(", ",", ")") 205 206 private def print_opt(opt: Options.Opt): String = 207 if (opt.public) "public " + opt.print else opt.print 208 209 def print: String = cat_lines(options.toList.sortBy(_._1).map(p => print_opt(p._2))) 210 211 def description(name: String): String = check_name(name).description 212 213 214 /* check */ 215 216 def check_name(name: String): Options.Opt = 217 options.get(name) match { 218 case Some(opt) if !opt.unknown => opt 219 case _ => error("Unknown option " + quote(name)) 220 } 221 222 private def check_type(name: String, typ: Options.Type): Options.Opt = 223 { 224 val opt = check_name(name) 225 if (opt.typ == typ) opt 226 else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print) 227 } 228 229 230 /* basic operations */ 231 232 private def put[A](name: String, typ: Options.Type, value: String): Options = 233 { 234 val opt = check_type(name, typ) 235 new Options(options + (name -> opt.copy(value = value)), section) 236 } 237 238 private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A = 239 { 240 val opt = check_type(name, typ) 241 parse(opt.value) match { 242 case Some(x) => x 243 case None => 244 error("Malformed value for option " + quote(name) + 245 " : " + typ.print + " =\n" + quote(opt.value)) 246 } 247 } 248 249 250 /* internal lookup and update */ 251 252 class Bool_Access 253 { 254 def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply) 255 def update(name: String, x: Boolean): Options = 256 put(name, Options.Bool, Value.Boolean(x)) 257 } 258 val bool = new Bool_Access 259 260 class Int_Access 261 { 262 def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply) 263 def update(name: String, x: Int): Options = 264 put(name, Options.Int, Value.Int(x)) 265 } 266 val int = new Int_Access 267 268 class Real_Access 269 { 270 def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply) 271 def update(name: String, x: Double): Options = 272 put(name, Options.Real, Value.Double(x)) 273 } 274 val real = new Real_Access 275 276 class String_Access 277 { 278 def apply(name: String): String = get(name, Options.String, s => Some(s)) 279 def update(name: String, x: String): Options = put(name, Options.String, x) 280 } 281 val string = new String_Access 282 283 def proper_string(name: String): Option[String] = 284 Library.proper_string(string(name)) 285 286 def seconds(name: String): Time = Time.seconds(real(name)) 287 288 289 /* external updates */ 290 291 private def check_value(name: String): Options = 292 { 293 val opt = check_name(name) 294 opt.typ match { 295 case Options.Bool => bool(name); this 296 case Options.Int => int(name); this 297 case Options.Real => real(name); this 298 case Options.String => string(name); this 299 case Options.Unknown => this 300 } 301 } 302 303 def declare( 304 public: Boolean, 305 pos: Position.T, 306 name: String, 307 typ_name: String, 308 value: String, 309 description: String): Options = 310 { 311 options.get(name) match { 312 case Some(other) => 313 error("Duplicate declaration of option " + quote(name) + Position.here(pos) + 314 Position.here(other.pos)) 315 case None => 316 val typ = 317 typ_name match { 318 case "bool" => Options.Bool 319 case "int" => Options.Int 320 case "real" => Options.Real 321 case "string" => Options.String 322 case _ => 323 error("Unknown type for option " + quote(name) + " : " + quote(typ_name) + 324 Position.here(pos)) 325 } 326 val opt = Options.Opt(public, pos, name, typ, value, value, description, section) 327 (new Options(options + (name -> opt), section)).check_value(name) 328 } 329 } 330 331 def add_permissive(name: String, value: String): Options = 332 { 333 if (options.isDefinedAt(name)) this + (name, value) 334 else { 335 val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "") 336 new Options(options + (name -> opt), section) 337 } 338 } 339 340 def + (name: String, value: String): Options = 341 { 342 val opt = check_name(name) 343 (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name) 344 } 345 346 def + (name: String, opt_value: Option[String]): Options = 347 { 348 val opt = check_name(name) 349 opt_value match { 350 case Some(value) => this + (name, value) 351 case None if opt.typ == Options.Bool => this + (name, "true") 352 case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print) 353 } 354 } 355 356 def + (str: String): Options = 357 { 358 str.indexOf('=') match { 359 case -1 => this + (str, None) 360 case i => this + (str.substring(0, i), str.substring(i + 1)) 361 } 362 } 363 364 def ++ (specs: List[Options.Spec]): Options = 365 (this /: specs)({ case (x, (y, z)) => x + (y, z) }) 366 367 368 /* sections */ 369 370 def set_section(new_section: String): Options = 371 new Options(options, new_section) 372 373 def sections: List[(String, List[Options.Opt])] = 374 options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) }) 375 376 377 /* encode */ 378 379 def encode: XML.Body = 380 { 381 val opts = 382 for ((_, opt) <- options.toList; if !opt.unknown) 383 yield (opt.pos, (opt.name, (opt.typ.print, opt.value))) 384 385 import XML.Encode.{string => string_, _} 386 list(pair(properties, pair(string_, pair(string_, string_))))(opts) 387 } 388 389 390 /* save preferences */ 391 392 def save_prefs(file: Path = Options.PREFS) 393 { 394 val defaults: Options = Options.init(prefs = "") 395 val changed = 396 (for { 397 (name, opt2) <- options.iterator 398 opt1 = defaults.options.get(name) 399 if opt1.isEmpty || opt1.get.value != opt2.value 400 } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else "")).toList 401 402 val prefs = 403 changed.sortBy(_._1) 404 .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString 405 406 Isabelle_System.mkdirs(file.dir) 407 File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs) 408 } 409} 410 411 412class Options_Variable(init_options: Options) 413{ 414 private var options = init_options 415 416 def value: Options = synchronized { options } 417 418 private def upd(f: Options => Options): Unit = synchronized { options = f(options) } 419 def += (name: String, x: String): Unit = upd(opts => opts + (name, x)) 420 421 class Bool_Access 422 { 423 def apply(name: String): Boolean = value.bool(name) 424 def update(name: String, x: Boolean): Unit = upd(opts => opts.bool.update(name, x)) 425 } 426 val bool = new Bool_Access 427 428 class Int_Access 429 { 430 def apply(name: String): Int = value.int(name) 431 def update(name: String, x: Int): Unit = upd(opts => opts.int.update(name, x)) 432 } 433 val int = new Int_Access 434 435 class Real_Access 436 { 437 def apply(name: String): Double = value.real(name) 438 def update(name: String, x: Double): Unit = upd(opts => opts.real.update(name, x)) 439 } 440 val real = new Real_Access 441 442 class String_Access 443 { 444 def apply(name: String): String = value.string(name) 445 def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x)) 446 } 447 val string = new String_Access 448 449 def proper_string(name: String): Option[String] = 450 Library.proper_string(string(name)) 451 452 def seconds(name: String): Time = value.seconds(name) 453} 454