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