Skip to content
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.

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

Be able to edit the source file in the main interface #3363

Open
fab918 opened this issue Nov 28, 2023 · 1 comment
Open

Be able to edit the source file in the main interface #3363

fab918 opened this issue Nov 28, 2023 · 1 comment
Labels
Feature New feature or request GUI

Comments

@fab918
Copy link

fab918 commented Nov 28, 2023

Please describe your proposal in a ONE sentence

One sentence describing your idea

In order to work more smoothly, it would be good to be able to edit the source file directly. An editor is already present (when loading a file), but it is not available to edit the sources.

Underlying problem

For each change in the source file, this requires opening an external editor, edit the file and save, then reloading the script and the reselecting the proof (which will create a duplicate in the proof section.)

@WolframPfeifer
Copy link
Member

Thanks for the suggestion. Unfortunately, this feature is not easy to implement. At the moment, the source view on the right side shows the source code corresponding to the currently selected proof (basically a shadow copy created at the moment the proof was started). If it was possible to edit the content, then the two view would be inconsistent. It is not clear at all how the feature would look like. In addition, we would have to maintain our own editor, which is much harder to implement than "just" a read-only view of the code (you have to implement and support various edit operations, syntax highlighting during editing, ...). For these reasons, we decided to keep the view read-only at the moment.

@WolframPfeifer WolframPfeifer added GUI Feature New feature or request labels Dec 8, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Feature New feature or request GUI
Projects
None yet
Development

No branches or pull requests

2 participants