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