Proposing a more flexible lexing framework

[mattulbrich]

Intended Change

The syntax highlighting framework in the issue dialog makes the cursor jump around a lot. It does not support KeY files for the moment.

Plan

• Make the "JavaDocument" language-independent
• Implement a corr. Java lexer
• Implement a corr. KeY parser
• Document the changes
• (optional) Make sure the realtime colour update works with the Java version since that may be configured at runtime

The code is there can be reused from other places.

Type of pull request

• Refactoring (behaviour should not change or only minimally change). Actually improvements in the error editor windows.
• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are minor improvements in the UI

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: tried it out.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[wadoon]

There was a branch (weigl/editor or so), where I had robust editors on the RSyntaxArea component.

@mattulbrich Should/Does the highlighting respect the current JML active (conditional) tags?

[wadoon]

One thing I could find here:

https://git.key-project.org/key/key/-/merge_requests/341

I also found the integrative swing editor with support PSDBG on branch weigl/Scripts.

[mattulbrich]

@mattulbrich Should/Does the highlighting respect the current JML active (conditional) tags?

The highlighting machinery is the one currently used by the component to display java source code in KeY.
I must admit that I do not know. ... Moreover, perhaps syntax highlighting should not depend on that after all, at least debatable.

[mattulbrich]

One thing I could find here: https://git.key-project.org/key/key/-/merge_requests/341
I also found the integrative swing editor with support PSDBG on branch weigl/Scripts.

The editor looks nice from the picture! However, on Friday we were pretty sure that we did not want to integrate an editor into the current swing UI. If an editor ... then as a plugin to whatever VSCode or such with decent feedback into the prover UI.

This is really lightweight syntax highlighting for a few bits within KeY.

The current solution lacked highlighting for KeY and made the cursor jump annoyingly in the exception recovery dialog.

[wadoon]

@mattulbrich Should/Does the highlighting respect the current JML active (conditional) tags?

The highlighting machinery is the one currently used by the component to display java source code in KeY. I must admit that I do not know. ... Moreover, perhaps syntax highlighting should not depend on that after all, at least debatable.

If it is inside of the KeY. I see the potential for recognizing errors quickly. For standalone editors, I would say it should be configurable.

[wadoon]

One thing I could find here: https://git.key-project.org/key/key/-/merge_requests/341
I also found the integrative swing editor with support PSDBG on branch weigl/Scripts.

The editor looks nice from the picture! However, on Friday we were pretty sure that we did not want to integrate an editor into the current swing UI. If an editor ... then as a plugin to whatever VSCode or such with decent feedback into the prover UI.

This is really lightweight syntax highlighting for a few bits within KeY.

The current solution lacked highlighting for KeY and made the cursor jump annoyingly in the exception recovery dialog.

1. The "ide" (editor) is standalone and written Kotlin/JavaFX.

   The advantage of using just Java is that we can reuse our grammar easily.

   I once also thought, to reuse JEdit or Netbeans.

2. weigl/Scripts branch contains an RSyntaxArea (Swing) editor and a direct integration into KeY using the docking framework. I got annoyed by the exploding complexity of the UI, and I don't find this as a suitable idea anymore.

3. I am also the author of the vscode-jml plugin. But this is rather a hack. The problem is the following: Every editor has a Java mode. Now you want to extend this for JML comments. And at this point the complexity starts, ... In Emacs, I was not able to achieve something useful.

4. On my pipeline is also the next version of vscode plugin, which uses LSP for the highlighting.

[mattulbrich]

@mattulbrich Should/Does the highlighting respect the current JML active (conditional) tags?

After checking a bit more, it turns out that it did already support this before the change.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 38.33%. Comparing base (cfd8f0f) to head (a0c4f81).
Report is 20 commits behind head on main.

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3537      +/-   ##
============================================
+ Coverage     38.19%   38.33%   +0.14%     
- Complexity    17228    17258      +30     
============================================
  Files          2111     2111              
  Lines        127642   127632      -10     
  Branches      21463    21461       -2     
============================================
+ Hits          48750    48926     +176     
+ Misses        72903    72695     -208     
- Partials       5989     6011      +22     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.