1 /* Title: Pure/System/options.scala
4 Stand-alone options with external string representation.
10 import java.io.{File => JFile}
15 type Spec = (String, Option[String])
17 val empty: Options = new Options()
22 sealed abstract class Type
24 def print: String = toString.toLowerCase
26 private case object Bool extends Type
27 private case object Int extends Type
28 private case object Real extends Type
29 private case object String extends Type
31 case class Opt(typ: Type, value: String, description: String)
36 private object Parser extends Parse.Parser
38 val DECLARE = "declare"
41 val syntax = Outer_Syntax.empty + ":" + "=" + DECLARE + DEFINE
43 val entry: Parser[Options => Options] =
45 val option_name = atom("option name", _.is_xname)
46 val option_type = atom("option type", _.is_ident)
47 val option_value = atom("option value", tok => tok.is_name || tok.is_float)
49 keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
50 keyword("=") ~ option_value ~ opt(text)) ^^
51 { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) =>
52 (options: Options) => options.declare(a, b, c, d.getOrElse("")) } |
53 keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
54 { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
57 def parse_entries(file: JFile): List[Options => Options] =
59 parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match {
60 case Success(result, _) => result
61 case bad => error(bad.toString)
66 private val OPTIONS = Path.explode("etc/options")
72 dir <- Isabelle_System.components()
73 file = (dir + OPTIONS).file
75 entry <- Parser.parse_entries(file)
77 try { options = entry(options) }
78 catch { case ERROR(msg) => error(msg + Position.str_of(Position.file(file))) }
85 final class Options private(options: Map[String, Options.Opt] = Map.empty)
87 override def toString: String = options.iterator.mkString("Options (", ",", ")")
92 private def check_name(name: String): Options.Opt =
93 options.get(name) match {
95 case None => error("Unknown option " + quote(name))
98 private def check_type(name: String, typ: Options.Type): Options.Opt =
100 val opt = check_name(name)
101 if (opt.typ == typ) opt
102 else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
106 /* basic operations */
108 private def put[A](name: String, typ: Options.Type, value: String): Options =
110 val opt = check_type(name, typ)
111 new Options(options + (name -> opt.copy(value = value)))
114 private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
116 val opt = check_type(name, typ)
117 parse(opt.value) match {
120 error("Malformed value for option " + quote(name) +
121 " : " + typ.print + " =\n" + quote(opt.value))
126 /* internal lookup and update */
128 val bool = new Object
130 def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
131 def update(name: String, x: Boolean): Options =
132 put(name, Options.Bool, Properties.Value.Boolean(x))
137 def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
138 def update(name: String, x: Int): Options =
139 put(name, Options.Int, Properties.Value.Int(x))
142 val real = new Object
144 def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
145 def update(name: String, x: Double): Options =
146 put(name, Options.Real, Properties.Value.Double(x))
149 val string = new Object
151 def apply(name: String): String = get(name, Options.String, s => Some(s))
152 def update(name: String, x: String): Options = put(name, Options.String, x)
156 /* external declare and define */
158 private def check_value(name: String): Options =
160 val opt = check_name(name)
162 case Options.Bool => bool(name); this
163 case Options.Int => int(name); this
164 case Options.Real => real(name); this
165 case Options.String => string(name); this
169 def declare(name: String, typ_name: String, value: String, description: String = ""): Options =
171 options.get(name) match {
172 case Some(_) => error("Duplicate declaration of option " + quote(name))
176 case "bool" => Options.Bool
177 case "int" => Options.Int
178 case "real" => Options.Real
179 case "string" => Options.String
180 case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name))
182 (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name)
186 def define(name: String, value: String): Options =
188 val opt = check_name(name)
189 (new Options(options + (name -> opt.copy(value = value)))).check_value(name)
192 def define(name: String, opt_value: Option[String]): Options =
194 val opt = check_name(name)
196 case Some(value) => define(name, value)
197 case None if opt.typ == Options.Bool => define(name, "true")
198 case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
202 def ++ (specs: List[Options.Spec]): Options =
203 (this /: specs)({ case (x, (y, z)) => x.define(y, z) })
205 def define_simple(str: String): Options =
207 str.indexOf('=') match {
208 case -1 => define(str, None)
209 case i => define(str.substring(0, i), str.substring(i + 1))