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