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 object Parser extends Parse.Parser with 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.base_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 class Seconds_Access 284 { 285 def apply(name: String): Time = Time.seconds(real(name)) 286 } 287 val seconds = new Seconds_Access 288 289 290 /* external updates */ 291 292 private def check_value(name: String): Options = 293 { 294 val opt = check_name(name) 295 opt.typ match { 296 case Options.Bool => bool(name); this 297 case Options.Int => int(name); this 298 case Options.Real => real(name); this 299 case Options.String => string(name); this 300 case Options.Unknown => this 301 } 302 } 303 304 def declare( 305 public: Boolean, 306 pos: Position.T, 307 name: String, 308 typ_name: String, 309 value: String, 310 description: String): Options = 311 { 312 options.get(name) match { 313 case Some(other) => 314 error("Duplicate declaration of option " + quote(name) + Position.here(pos) + 315 Position.here(other.pos)) 316 case None => 317 val typ = 318 typ_name match { 319 case "bool" => Options.Bool 320 case "int" => Options.Int 321 case "real" => Options.Real 322 case "string" => Options.String 323 case _ => 324 error("Unknown type for option " + quote(name) + " : " + quote(typ_name) + 325 Position.here(pos)) 326 } 327 val opt = Options.Opt(public, pos, name, typ, value, value, description, section) 328 (new Options(options + (name -> opt), section)).check_value(name) 329 } 330 } 331 332 def add_permissive(name: String, value: String): Options = 333 { 334 if (options.isDefinedAt(name)) this + (name, value) 335 else { 336 val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "") 337 new Options(options + (name -> opt), section) 338 } 339 } 340 341 def + (name: String, value: String): Options = 342 { 343 val opt = check_name(name) 344 (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name) 345 } 346 347 def + (name: String, opt_value: Option[String]): Options = 348 { 349 val opt = check_name(name) 350 opt_value match { 351 case Some(value) => this + (name, value) 352 case None if opt.typ == Options.Bool => this + (name, "true") 353 case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print) 354 } 355 } 356 357 def + (str: String): Options = 358 { 359 str.indexOf('=') match { 360 case -1 => this + (str, None) 361 case i => this + (str.substring(0, i), str.substring(i + 1)) 362 } 363 } 364 365 def ++ (specs: List[Options.Spec]): Options = 366 (this /: specs)({ case (x, (y, z)) => x + (y, z) }) 367 368 369 /* sections */ 370 371 def set_section(new_section: String): Options = 372 new Options(options, new_section) 373 374 def sections: List[(String, List[Options.Opt])] = 375 options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) }) 376 377 378 /* encode */ 379 380 def encode: XML.Body = 381 { 382 val opts = 383 for ((_, opt) <- options.toList; if !opt.unknown) 384 yield (opt.pos, (opt.name, (opt.typ.print, opt.value))) 385 386 import XML.Encode.{string => string_, _} 387 list(pair(properties, pair(string_, pair(string_, string_))))(opts) 388 } 389 390 391 /* save preferences */ 392 393 def save_prefs(file: Path = Options.PREFS) 394 { 395 val defaults: Options = Options.init(prefs = "") 396 val changed = 397 (for { 398 (name, opt2) <- options.iterator 399 opt1 = defaults.options.get(name) 400 if opt1.isEmpty || opt1.get.value != opt2.value 401 } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else "")).toList 402 403 val prefs = 404 changed.sortBy(_._1) 405 .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString 406 407 Isabelle_System.mkdirs(file.dir) 408 File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs) 409 } 410} 411 412 413class Options_Variable(init_options: Options) 414{ 415 private var options = init_options 416 417 def value: Options = synchronized { options } 418 419 private def upd(f: Options => Options): Unit = synchronized { options = f(options) } 420 def += (name: String, x: String): Unit = upd(opts => opts + (name, x)) 421 422 class Bool_Access 423 { 424 def apply(name: String): Boolean = value.bool(name) 425 def update(name: String, x: Boolean): Unit = upd(opts => opts.bool.update(name, x)) 426 } 427 val bool = new Bool_Access 428 429 class Int_Access 430 { 431 def apply(name: String): Int = value.int(name) 432 def update(name: String, x: Int): Unit = upd(opts => opts.int.update(name, x)) 433 } 434 val int = new Int_Access 435 436 class Real_Access 437 { 438 def apply(name: String): Double = value.real(name) 439 def update(name: String, x: Double): Unit = upd(opts => opts.real.update(name, x)) 440 } 441 val real = new Real_Access 442 443 class String_Access 444 { 445 def apply(name: String): String = value.string(name) 446 def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x)) 447 } 448 val string = new String_Access 449 450 class Seconds_Access 451 { 452 def apply(name: String): Time = value.seconds(name) 453 } 454 val seconds = new Seconds_Access 455} 456