summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/options_template.cpp4
-rw-r--r--src/options/mkoptions.py203
2 files changed, 103 insertions, 104 deletions
diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp
index a7a4429e3..98daf41dd 100644
--- a/src/main/options_template.cpp
+++ b/src/main/options_template.cpp
@@ -250,8 +250,8 @@ void parseInternal(api::Solver& solver,
+ "' missing its required argument");
case '?':
default:
- throw OptionException(std::string("can't understand option `") + option
- + "'" + suggestCommandLineOptions(option));
+ throw OptionException(std::string("can't understand option `") + option
+ + "'" + suggestCommandLineOptions(option));
}
}
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 02806d0d8..fe1a08149 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -654,103 +654,111 @@ def generate_cli_help(modules):
return '\n'.join(common), '\n'.join(others)
-class SphinxGenerator:
- def __init__(self):
- self.common = []
- self.others = {}
+################################################################################
+# sphinx command line documentation @ docs/options_generated.rst
- def add(self, module, option):
- if option.category == 'undocumented':
- return
- if not option.long and not option.short:
- return
- names = []
- if option.long:
- if option.long_opt:
- names.append('--{}={}'.format(option.long_name, option.long_opt))
- else:
- names.append('--{}'.format(option.long_name))
- if option.alias:
- if option.long_opt:
- names.extend(['--{}={}'.format(a, option.long_opt) for a in option.alias])
- else:
- names.extend(['--{}'.format(a) for a in option.alias])
-
- if option.short:
- if option.long_opt:
- names.append('-{} {}'.format(option.short, option.long_opt))
- else:
- names.append('-{}'.format(option.short))
+def _sphinx_help_add(module, option, common, others):
+ """Analyze an option and add it to either common or others."""
+ names = []
+ if option.long:
+ if option.long_opt:
+ names.append('--{}={}'.format(option.long_name, option.long_opt))
+ else:
+ names.append('--{}'.format(option.long_name))
- modes = None
- if option.mode:
- modes = {}
- for _, data in option.mode.items():
- assert len(data) == 1
- data = data[0]
- modes[data['name']] = data.get('help', '')
-
- data = {
- 'name': names,
- 'help': option.help,
- 'expert': option.category == 'expert',
- 'alternate': option.alternate,
- 'help_mode': option.help_mode,
- 'modes': modes,
- }
+ if option.alias:
+ if option.long_opt:
+ names.extend(
+ ['--{}={}'.format(a, option.long_opt) for a in option.alias])
+ else:
+ names.extend(['--{}'.format(a) for a in option.alias])
- if option.category == 'common':
- self.common.append(data)
+ if option.short:
+ if option.long_opt:
+ names.append('-{} {}'.format(option.short, option.long_opt))
else:
- if module.name not in self.others:
- self.others[module.name] = []
- self.others[module.name].append(data)
-
- def __render_option(self, res, opt):
- desc = '``{}``'
- val = ' {}'
- if opt['expert']:
- res.append('.. admonition:: This option is intended for Experts only!')
- res.append(' ')
- desc = ' ' + desc
- val = ' ' + val
-
- if opt['alternate']:
- desc += ' (also ``--no-*``)'
- res.append(desc.format(' | '.join(opt['name'])))
- res.append(val.format(opt['help']))
-
- if opt['modes']:
- res.append(val.format(''))
- res.append(val.format(opt['help_mode']))
- res.append(val.format(''))
- for k, v in opt['modes'].items():
- if v == '':
- continue
- res.append(val.format(':{}: {}'.format(k, v)))
- res.append(' ')
-
-
- def render(self, dstdir, filename):
- res = []
-
- res.append('Most Commonly-Used cvc5 Options')
- res.append('===============================')
- for opt in self.common:
- self.__render_option(res, opt)
+ names.append('-{}'.format(option.short))
+ modes = None
+ if option.mode:
+ modes = {}
+ for _, data in option.mode.items():
+ assert len(data) == 1
+ modes[data[0]['name']] = data[0].get('help', '')
+
+ data = {
+ 'name': names,
+ 'help': option.help,
+ 'expert': option.category == 'expert',
+ 'alternate': option.alternate,
+ 'help_mode': option.help_mode,
+ 'modes': modes,
+ }
+
+ if option.category == 'common':
+ common.append(data)
+ else:
+ if module.name not in others:
+ others[module.name] = []
+ others[module.name].append(data)
+
+
+def _sphinx_help_render_option(res, opt):
+ """Render an option to be displayed with sphinx."""
+ indent = ' ' * 4
+ desc = '``{}``'
+ val = indent + '{}'
+ if opt['expert']:
+ res.append('.. admonition:: This option is intended for Experts only!')
+ res.append(indent)
+ desc = indent + desc
+ val = indent + val
+
+ if opt['alternate']:
+ desc += ' (also ``--no-*``)'
+ res.append(desc.format(' | '.join(opt['name'])))
+ res.append(val.format(opt['help']))
+
+ if opt['modes']:
+ res.append(val.format(''))
+ res.append(val.format(opt['help_mode']))
+ res.append(val.format(''))
+ for k, v in opt['modes'].items():
+ if v == '':
+ continue
+ res.append(val.format(':{}: {}'.format(k, v)))
+ res.append(indent)
+
+
+def generate_sphinx_help(modules):
+ """Render the command line help for sphinx."""
+ common = []
+ others = {}
+ for module, option in all_options(modules, False):
+ if option.type == 'undocumented':
+ continue
+ if not option.long and not option.short:
+ continue
+ _sphinx_help_add(module, option, common, others)
+
+ res = []
+ res.append('Most Commonly-Used cvc5 Options')
+ res.append('===============================')
+ for opt in common:
+ _sphinx_help_render_option(res, opt)
+
+ res.append('')
+ res.append('Additional cvc5 Options')
+ res.append('=======================')
+ for module in others:
res.append('')
- res.append('Additional cvc5 Options')
- res.append('=======================')
- for module in self.others:
- res.append('')
- res.append('{} Module'.format(module))
- res.append('-' * (len(module) + 8))
- for opt in self.others[module]:
- self.__render_option(res, opt)
+ res.append('{} Module'.format(module))
+ res.append('-' * (len(module) + 8))
+ for opt in others[module]:
+ _sphinx_help_render_option(res, opt)
- write_file(dstdir, filename, '\n'.join(res))
+ return '\n'.join(res)
def long_get_option(name):
@@ -911,21 +919,16 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
headers_module = [] # generated *_options.h header includes
- sphinxgen = SphinxGenerator()
-
for module in modules:
headers_module.append(format_include(module.header))
- for option in \
- sorted(module.options, key=lambda x: x.long if x.long else x.name):
- assert option.type != 'void' or option.name is None
- assert option.name or option.short or option.long
-
- sphinxgen.add(module, option)
-
short, cmdline_opts, parseinternal = generate_parsing(modules)
help_common, help_others = generate_cli_help(modules)
+ if os.path.isdir('{}/docs/'.format(build_dir)):
+ write_file('{}/docs/'.format(build_dir), 'options_generated.rst',
+ generate_sphinx_help(modules))
+
data = {
# options/options.h
'holder_fwd_decls': generate_holder_fwd_decls(modules),
@@ -953,10 +956,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
write_file(dst_dir, tpl['output'], tpl['content'].format(**data))
- if os.path.isdir('{}/docs/'.format(build_dir)):
- sphinxgen.render('{}/docs/'.format(build_dir), 'options_generated.rst')
-
-
class Checker:
"""Performs a variety of sanity checks on options and option modules, and
constructs `Module` and `Option` from dictionaries."""
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback