Skip to content

Conversation

@wadoon
Copy link
Member

@wadoon wadoon commented Oct 4, 2025

User Story

With the chapter "Using KeY" and the FM tutorial, we got two introductory chapters into KeY. Both are written PDF files, and therefore not so interesting or catchy.

For a web, interactive tutorials should be a way to go, but KeY is not a web application. To interact from a website (or a text editor) to KeY, we need a way of remotely controlling it.

Intended Change

This PR an UI extension to start/stop a local integrated webserver which allows (for now) to start a specified example in KeY.

For example, a tutorial can say "Please load 'Binary Search'" and providing the URL http://localhost:8000/openExample?name=Binary Search. Opening this URL opens the example in KeY.

This is just a small investigation of this problem.

Relation to JsonRPC

This is very close to the key api written #3303.

Differences are:

  • This allows control over the MainWindow. Actions and manipulations target the UI. The Rest API is for externalizing the functionality.
    For example, when open an example with the RestAPI, you get a handle for a KeY environment. WebCtrl, the example will be open in the MainWindow.

  • Functionality would also include things like:

    • Open windows or dialogs
    • Highlights certain elements (buttons, sequent, formula, ...)
    • Maybe set options in the MainWindow
  • It comes with an HTTPServer so it can be easily called from a web browser.

A combination with RestAPI is possible.

Plan

  • Discuss
  • Find a set of necessary functionality by reading the tutorials.
  • Rewrite a tutorial for a web version.
  • Code the functionality
  • Document the changes

Type of pull request

  • New feature (non-breaking change which adds functionality)
  • There are changes to the (Java) code

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
  • I added new test case(s) for new functionality.
  • I have tested the feature as follows: ...
  • I have checked that runtime performance has not deteriorated.
  • For new Gradle modules: I added the Gradle module to the test matrix in
    .github/workflows/tests.yml

Additional information and contact(s)

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

@wadoon wadoon self-assigned this Oct 4, 2025
@wadoon wadoon added the Feature New feature or request label Oct 4, 2025
@wadoon wadoon added this to the v2.12.4 milestone Oct 4, 2025
@wadoon wadoon modified the milestones: v2.13.0, v2.14.0 Nov 21, 2025
@wadoon wadoon closed this Dec 20, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Feature New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants