src/Pure/System/options.ML
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48698 2585042b1a30
child 51942 527e39becafc
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48456
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/System/options.ML
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     3
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     4
Stand-alone options with external string representation.
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     5
*)
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     6
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     7
signature OPTIONS =
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     8
sig
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
     9
  type T
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    10
  val empty: T
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    11
  val bool: T -> string -> bool
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    12
  val int: T -> string -> int
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    13
  val real: T -> string -> real
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    14
  val string: T -> string -> string
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    15
  val declare: {name: string, typ: string, value: string} -> T -> T
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    16
  val decode: XML.body -> T
48698
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    17
  val default: unit -> T
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    18
  val set_default: T -> unit
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    19
  val reset_default: unit -> unit
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    20
  val load_default: unit -> unit
48456
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    21
end;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    22
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    23
structure Options: OPTIONS =
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    24
struct
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    25
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    26
(* representation *)
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    27
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    28
val boolT = "bool";
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    29
val intT = "int";
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    30
val realT = "real";
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    31
val stringT = "string";
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    32
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    33
datatype T = Options of {typ: string, value: string} Symtab.table;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    34
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    35
val empty = Options Symtab.empty;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    36
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    37
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    38
(* get *)
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    39
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    40
fun get T parse (Options tab) name =
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    41
  (case Symtab.lookup tab name of
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    42
    SOME {typ, value} =>
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    43
      if typ = T then
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    44
        (case parse value of
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    45
          SOME x => x
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    46
        | NONE =>
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    47
            error ("Malformed value for option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote value))
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    48
      else error ("Ill-typed option " ^ quote name ^ " : " ^ typ ^ " vs. " ^ T)
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    49
  | NONE => error ("Unknown option " ^ quote name));
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    50
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    51
val bool = get boolT Bool.fromString;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    52
val int = get intT Int.fromString;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    53
val real = get realT Real.fromString;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    54
val string = get stringT SOME;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    55
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    56
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    57
(* declare *)
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    58
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    59
fun declare {name, typ, value} (Options tab) =
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    60
  let
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    61
    val check_value =
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    62
      if typ = boolT then ignore oo bool
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    63
      else if typ = intT then ignore oo int
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    64
      else if typ = realT then ignore oo real
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    65
      else if typ = stringT then ignore oo string
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    66
      else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    67
    val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    68
      handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name);
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    69
    val _ = check_value options' name;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    70
  in options' end;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    71
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    72
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    73
(* decode *)
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    74
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    75
fun decode body =
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    76
  fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    77
    (let open XML.Decode in list (triple string string string) end body) empty;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
    78
48698
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    79
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    80
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    81
(** global default **)
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    82
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    83
val global_default = Synchronized.var "Options.default" (NONE: T option);
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    84
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    85
fun default () =
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    86
  (case Synchronized.value global_default of
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    87
    SOME options => options
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    88
  | NONE => error "No global default options");
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    89
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    90
fun set_default options = Synchronized.change global_default (K (SOME options));
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    91
fun reset_default () = Synchronized.change global_default (K NONE);
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    92
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    93
fun load_default () =
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    94
  (case getenv "ISABELLE_PROCESS_OPTIONS" of
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    95
    "" => ()
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    96
  | name =>
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    97
      let val path = Path.explode name in
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    98
        (case try File.read path of
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
    99
          SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path))
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
   100
        | NONE => ())
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
   101
      end);
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
   102
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
   103
val _ = load_default ();
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48456
diff changeset
   104
48456
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
   105
end;
d8ff14f44a40 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff changeset
   106