143 /* command line entry point */ |
143 /* command line entry point */ |
144 |
144 |
145 def main(args: Array[String]) |
145 def main(args: Array[String]) |
146 { |
146 { |
147 Command_Line.tool0 { |
147 Command_Line.tool0 { |
148 args.toList match { |
148 var build_options = false |
149 case get_option :: export_file :: more_options => |
149 var get_option = "" |
150 val options = (Options.init() /: more_options)(_ + _) |
150 var list_options = false |
151 |
151 var export_file = "" |
152 if (get_option != "") |
152 |
153 Console.println(options.check_name(get_option).value) |
153 val getopts = Getopts(() => """ |
154 |
154 Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] |
155 if (export_file != "") |
155 |
156 File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) |
156 Options are: |
157 |
157 -b include $ISABELLE_BUILD_OPTIONS |
158 if (get_option == "" && export_file == "") |
158 -g OPTION get value of OPTION |
159 Console.println(options.print) |
159 -l list options |
160 |
160 -x FILE export options to FILE in YXML format |
161 case _ => error("Bad arguments:\n" + cat_lines(args)) |
161 |
|
162 Report Isabelle system options, augmented by MORE_OPTIONS given as |
|
163 arguments NAME=VAL or NAME. |
|
164 """, |
|
165 "b" -> (_ => build_options = true), |
|
166 "g:" -> (arg => get_option = arg), |
|
167 "l" -> (_ => list_options = true), |
|
168 "x:" -> (arg => export_file = arg)) |
|
169 |
|
170 val more_options = getopts(args) |
|
171 if (get_option == "" && !list_options && export_file == "") getopts.usage() |
|
172 |
|
173 val options = |
|
174 { |
|
175 val options0 = Options.init() |
|
176 val options1 = |
|
177 if (build_options) |
|
178 (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _) |
|
179 else options0 |
|
180 (options1 /: more_options)(_ + _) |
162 } |
181 } |
|
182 |
|
183 if (get_option != "") |
|
184 Console.println(options.check_name(get_option).value) |
|
185 |
|
186 if (export_file != "") |
|
187 File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) |
|
188 |
|
189 if (get_option == "" && export_file == "") |
|
190 Console.println(options.print) |
163 } |
191 } |
164 } |
192 } |
165 } |
193 } |
166 |
194 |
167 |
195 |