src/Tools/Metis/src/Options.sml
author blanchet
Thu, 24 Mar 2011 17:49:27 +0100
changeset 42102 fcfd07f122d4
parent 39502 cffceed8e7fa
child 45778 df6e210fb44c
permissions -rw-r--r--
new version of Metis 2.3 (29 Dec. 2010)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* PROCESSING COMMAND LINE OPTIONS                                           *)
39502
cffceed8e7fa fix license
blanchet
parents: 39501
diff changeset
     3
(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
structure Options :> Options =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
infix ##
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
open Useful;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
(* One command line option: names, arguments, description and a processor    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
type proc = string * string list -> unit;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
type ('a,'x) mkProc = ('x -> proc) -> ('a -> 'x) -> proc;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
type opt = {switches : string list, arguments : string list,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
            description : string, processor : proc};
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* Option processors may raise an OptionExit exception                       *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
type optionExit = {message : string option, usage : bool, success : bool};
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
exception OptionExit of optionExit;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
(* Wrappers for option processors                                            *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
fun beginOpt f p (s : string, l : string list) : unit = f (p s) (s,l);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
fun endOpt () (_ : string, [] : string list) = ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
  | endOpt _ (_, _ :: _) = raise Bug "endOpt";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
fun stringOpt _ _ (_ : string, []) = raise Bug "stringOpt"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
  | stringOpt f p (s, (h : string) :: t) : unit = f (p h) (s,t);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
  fun range NONE NONE = "Z"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
    | range (SOME i) NONE = "{n IN Z | " ^ Int.toString i ^ " <= n}"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
    | range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
    | range (SOME i) (SOME j) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
    "{n IN Z | " ^ Int.toString i ^ " <= n <= " ^ Int.toString j ^ "}";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
  fun oLeq (SOME x) (SOME y) = x <= y | oLeq _ _ = true;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
  fun argToInt arg omin omax x =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
    (case Int.fromString x of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
       SOME i =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
       if oLeq omin (SOME i) andalso oLeq (SOME i) omax then i else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
         raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
           {success = false, usage = false, message =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
            SOME (arg ^ " option needs an integer argument in the range "
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
                  ^ range omin omax ^ " (not " ^ x ^ ")")}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
     | NONE =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
       raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
         {success = false, usage = false, message =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
          SOME (arg ^ " option needs an integer argument (not \"" ^ x ^ "\")")})
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
    handle Overflow =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
       raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
         {success = false, usage = false, message =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
          SOME (arg ^ " option suffered integer overflow on argument " ^ x)};
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
  fun intOpt _ _ _ (_,[]) = raise Bug "intOpt"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
    | intOpt (omin,omax) f p (s:string, h :: (t : string list)) : unit =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
      f (p (argToInt s omin omax h)) (s,t);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
  fun range NONE NONE = "R"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
    | range (SOME i) NONE = "{n IN R | " ^ Real.toString i ^ " <= n}"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
    | range NONE (SOME j) = "{n IN R | n <= " ^ Real.toString j ^ "}"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
    | range (SOME i) (SOME j) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
    "{n IN R | " ^ Real.toString i ^ " <= n <= " ^ Real.toString j ^ "}";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
  fun oLeq (SOME (x:real)) (SOME y) = x <= y | oLeq _ _ = true;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
  fun argToReal arg omin omax x =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
    (case Real.fromString x of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
       SOME i =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
       if oLeq omin (SOME i) andalso oLeq (SOME i) omax then i else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
         raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
           {success = false, usage = false, message =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
            SOME (arg ^ " option needs an real argument in the range "
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
                  ^ range omin omax ^ " (not " ^ x ^ ")")}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
     | NONE =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
       raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
         {success = false, usage = false, message =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
          SOME (arg ^ " option needs an real argument (not \"" ^ x ^ "\")")})
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
  fun realOpt _ _ _ (_,[]) = raise Bug "realOpt"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
    | realOpt (omin,omax) f p (s:string, h :: (t : string list)) : unit =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
      f (p (argToReal s omin omax h)) (s,t);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
fun enumOpt _ _ _ (_,[]) = raise Bug "enumOpt"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
  | enumOpt (choices : string list) f p (s : string, h :: t) : unit =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
    if mem h choices then f (p h) (s,t) else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
      raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
        {success = false, usage = false,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
         message = SOME ("follow parameter " ^ s ^ " with one of {" ^
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
                         join "," choices ^ "}, not \"" ^ h ^ "\"")};
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
fun optionOpt _ _ _ (_,[]) = raise Bug "optionOpt"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
  | optionOpt (x : string, p) f q (s : string, l as h :: t) : unit =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
    if h = x then f (q NONE) (s,t) else p f (q o SOME) (s,l);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
(* Basic options useful for all programs                                     *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
val basicOptions : opt list =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
  [{switches = ["--"], arguments = [],
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
    description = "no more options",
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
    processor = fn _ => raise Fail "basicOptions: --"},
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
   {switches = ["-?","-h","--help"], arguments = [],
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
    description = "display option information and exit",
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
    processor = fn _ => raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
    {message = SOME "displaying option information",
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
     usage = true, success = true}},
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
   {switches = ["-v", "--version"], arguments = [],
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
    description = "display version information",
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
    processor = fn _ => raise Fail "basicOptions: -v, --version"}];
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
(* All the command line options of a program                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
type allOptions =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
     {name : string, version : string, header : string,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
      footer : string, options : opt list};
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
(* Usage information                                                         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   137
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   138
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   139
fun versionInformation ({version, ...} : allOptions) = version;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   140
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   141
fun usageInformation ({name,version,header,footer,options} : allOptions) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   142
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   143
    fun listOpts {switches = n, arguments = r, description = s,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   144
                  processor = _} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
          fun indent (s, "" :: l) = indent (s ^ "  ", l) | indent x = x
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
          val (res,n) = indent ("  ",n)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
          val res = res ^ join ", " n
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39353
diff changeset
   149
          val res = List.foldl (fn (x,y) => y ^ " " ^ x) res r
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
          [res ^ " ...", " " ^ s]
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
    val alignment =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
        [{leftAlign = true, padChar = #"."},
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
         {leftAlign = true, padChar = #" "}]
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   158
    val table = alignTable alignment (List.map listOpts options)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
    header ^ join "\n" table ^ "\n" ^ footer
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
(* Exit the program gracefully                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
fun exit (allopts : allOptions) (optexit : optionExit) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
    val {name, options, ...} = allopts
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
    val {message, usage, success} = optexit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
    fun err s = TextIO.output (TextIO.stdErr, s)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
    case message of NONE => () | SOME m => err (name ^ ": " ^ m ^ "\n");
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
    if usage then err (usageInformation allopts) else ();
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
    OS.Process.exit (if success then OS.Process.success else OS.Process.failure)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
fun succeed allopts =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
    exit allopts {message = NONE, usage = false, success = true};
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
fun fail allopts mesg =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
    exit allopts {message = SOME mesg, usage = false, success = false};
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   184
fun usage allopts mesg =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
    exit allopts {message = SOME mesg, usage = true, success = false};
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   186
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
fun version allopts =
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39353
diff changeset
   188
    (TextIO.print (versionInformation allopts);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   189
     exit allopts {message = NONE, usage = false, success = true});
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   191
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   192
(* Process the command line options passed to the program                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   193
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   194
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   195
fun processOptions (allopts : allOptions) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   196
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   197
    fun findOption x =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   198
      case List.find (fn {switches = n, ...} => mem x n) (#options allopts) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   199
        NONE => raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   200
                        {message = SOME ("unknown switch \"" ^ x ^ "\""),
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   201
                         usage = true, success = false}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   202
      | SOME {arguments = r, processor = f, ...} => (r,f)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   203
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   204
    fun getArgs x r xs =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   205
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   206
        fun f 1 = "a following argument"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   207
          | f m = Int.toString m ^ " following arguments"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   208
        val m = length r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   209
        val () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   210
          if m <= length xs then () else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   211
            raise OptionExit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   212
              {usage = false, success = false, message = SOME
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   213
               (x ^ " option needs " ^ f m ^ ": " ^ join " " r)}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   214
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   215
        divide xs m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   216
      end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   217
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   218
    fun process [] = ([], [])
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   219
      | process ("--" :: xs) = ([("--",[])], xs)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   220
      | process ("-v" :: _) = version allopts
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   221
      | process ("--version" :: _) = version allopts
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   222
      | process (x :: xs) =
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39353
diff changeset
   223
      if x = "" orelse x = "-" orelse hd (String.explode x) <> #"-" then
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39353
diff changeset
   224
        ([], x :: xs)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   225
      else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   226
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   227
          val (r,f) = findOption x
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   228
          val (ys,xs) = getArgs x r xs
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   229
          val () = f (x,ys)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   230
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   231
          (cons (x,ys) ## I) (process xs)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   232
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   233
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   234
    fn l =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   235
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   236
      val (a,b) = process l
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39353
diff changeset
   237
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39353
diff changeset
   238
      val a = List.foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (rev a)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   239
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   240
      (a,b)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   241
    end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   242
    handle OptionExit x => exit allopts x
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   243
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   244
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   245
end