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