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)
More granular control on how lints can be configured. These are some of the options:
How should the options be available? (jEdit)