New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Configuration Options: Lints #13

Open

TheMC47 opened this issue Dec 10, 2021 · 0 comments

Labels

enhancement question

Collaborator

TheMC47 commented Dec 10, 2021

More granular control on how lints can be configured. These are some of the options:

bad_style_command, counter_example_finder, diagnostic_command, unfinished proof: adding/removing commands
complex_method: nesting threshold
low_level_apply_chain: number of apply commands allowed
short_name: length of the name

How should the options be available? (jEdit)

A new Linter section under Plugins > Plugin Options > Isabelle > Linter
Just extra options in the existing Linter section
An external configuration file/string (e.g. json format)

TheMC47 added enhancement question labels

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment