src/Pure/System/options.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48605 e777363440d6
child 48693 ceeea46bdeba
permissions -rw-r--r--
more official command specifications, including source position;
     1 /*  Title:      Pure/System/options.scala
     2     Author:     Makarius
     3 
     4 Stand-alone options with external string representation.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object 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 = toString.toLowerCase
    22   }
    23   private case object Bool extends Type
    24   private case object Int extends Type
    25   private case object Real extends Type
    26   private case object String extends Type
    27 
    28   case class Opt(typ: Type, value: String, description: String)
    29 
    30 
    31   /* parsing */
    32 
    33   private object Parser extends Parse.Parser
    34   {
    35     val DECLARE = "declare"
    36     val DEFINE = "define"
    37 
    38     val syntax = Outer_Syntax.empty + ":" + "=" + "--" + DECLARE + DEFINE
    39 
    40     val entry: Parser[Options => Options] =
    41     {
    42       val option_name = atom("option name", _.is_xname)
    43       val option_type = atom("option type", _.is_ident)
    44 
    45       val option_value =
    46         opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
    47           { case s ~ n => if (s.isDefined) "-" + n else n } |
    48         atom("option value", tok => tok.is_name || tok.is_float)
    49 
    50       keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
    51       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    52         { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) } |
    53       keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
    54         { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
    55     }
    56 
    57     def parse_entries(file: Path): List[Options => Options] =
    58     {
    59       parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.implode)) match {
    60         case Success(result, _) => result
    61         case bad => error(bad.toString)
    62       }
    63     }
    64   }
    65 
    66   private val OPTIONS = Path.explode("etc/options")
    67 
    68   def init(): Options =
    69   {
    70     var options = empty
    71     for {
    72       dir <- Isabelle_System.components()
    73       file = dir + OPTIONS if file.is_file
    74       entry <- Parser.parse_entries(file)
    75     } {
    76       try { options = entry(options) }
    77       catch { case ERROR(msg) => error(msg + Position.str_of(file.position)) }
    78     }
    79     options
    80   }
    81 
    82 
    83   /* encode */
    84 
    85   val encode: XML.Encode.T[Options] = (options => options.encode)
    86 }
    87 
    88 
    89 final class Options private(options: Map[String, Options.Opt] = Map.empty)
    90 {
    91   override def toString: String = options.iterator.mkString("Options (", ",", ")")
    92 
    93 
    94   /* check */
    95 
    96   private def check_name(name: String): Options.Opt =
    97     options.get(name) match {
    98       case Some(opt) => opt
    99       case None => error("Unknown option " + quote(name))
   100     }
   101 
   102   private def check_type(name: String, typ: Options.Type): Options.Opt =
   103   {
   104     val opt = check_name(name)
   105     if (opt.typ == typ) opt
   106     else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
   107   }
   108 
   109 
   110   /* basic operations */
   111 
   112   private def put[A](name: String, typ: Options.Type, value: String): Options =
   113   {
   114     val opt = check_type(name, typ)
   115     new Options(options + (name -> opt.copy(value = value)))
   116   }
   117 
   118   private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
   119   {
   120     val opt = check_type(name, typ)
   121     parse(opt.value) match {
   122       case Some(x) => x
   123       case None =>
   124         error("Malformed value for option " + quote(name) +
   125           " : " + typ.print + " =\n" + quote(opt.value))
   126     }
   127   }
   128 
   129 
   130   /* internal lookup and update */
   131 
   132   val bool = new Object
   133   {
   134     def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
   135     def update(name: String, x: Boolean): Options =
   136       put(name, Options.Bool, Properties.Value.Boolean(x))
   137   }
   138 
   139   val int = new Object
   140   {
   141     def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
   142     def update(name: String, x: Int): Options =
   143       put(name, Options.Int, Properties.Value.Int(x))
   144   }
   145 
   146   val real = new Object
   147   {
   148     def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
   149     def update(name: String, x: Double): Options =
   150       put(name, Options.Real, Properties.Value.Double(x))
   151   }
   152 
   153   val string = new Object
   154   {
   155     def apply(name: String): String = get(name, Options.String, s => Some(s))
   156     def update(name: String, x: String): Options = put(name, Options.String, x)
   157   }
   158 
   159 
   160   /* external declare and define */
   161 
   162   private def check_value(name: String): Options =
   163   {
   164     val opt = check_name(name)
   165     opt.typ match {
   166       case Options.Bool => bool(name); this
   167       case Options.Int => int(name); this
   168       case Options.Real => real(name); this
   169       case Options.String => string(name); this
   170     }
   171   }
   172 
   173   def declare(name: String, typ_name: String, value: String, description: String = ""): Options =
   174   {
   175     options.get(name) match {
   176       case Some(_) => error("Duplicate declaration of option " + quote(name))
   177       case None =>
   178         val typ =
   179           typ_name match {
   180             case "bool" => Options.Bool
   181             case "int" => Options.Int
   182             case "real" => Options.Real
   183             case "string" => Options.String
   184             case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
   185           }
   186         (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name)
   187     }
   188   }
   189 
   190   def define(name: String, value: String): Options =
   191   {
   192     val opt = check_name(name)
   193     (new Options(options + (name -> opt.copy(value = value)))).check_value(name)
   194   }
   195 
   196   def define(name: String, opt_value: Option[String]): Options =
   197   {
   198     val opt = check_name(name)
   199     opt_value match {
   200       case Some(value) => define(name, value)
   201       case None if opt.typ == Options.Bool => define(name, "true")
   202       case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
   203     }
   204   }
   205 
   206   def ++ (specs: List[Options.Spec]): Options =
   207     (this /: specs)({ case (x, (y, z)) => x.define(y, z) })
   208 
   209   def define_simple(str: String): Options =
   210   {
   211     str.indexOf('=') match {
   212       case -1 => define(str, None)
   213       case i => define(str.substring(0, i), str.substring(i + 1))
   214     }
   215   }
   216 
   217 
   218   /* encode */
   219 
   220   def encode: XML.Body =
   221   {
   222     import XML.Encode.{string => str, _}
   223     list(triple(str, str, str))(
   224       options.toList.map({ case (name, opt) => (name, opt.typ.print, opt.value) }))
   225   }
   226 }