Mentions légales du service

Skip to content
Snippets Groups Projects
Open Why3 IDE - close a file/tab from the IDE directly
  • View options
  • Why3 IDE - close a file/tab from the IDE directly

  • View options
  • Open Issue created by Delphine Demange

    Suppose I start a fresh why3 module in file1.mlw. Then, suppose I want to either read, or reuse some definitions in another previous file, file2.mlw. So I add file2.mlw to the current session to be able to read it in the IDE.

    Now, suppose I'm done consulting file2.mlw, and that I don't want to see it appear in the source tabs, or that I don't want to bother with the VCs in that file.

    Currently, it doesn't seem to be possible to close the tab for file2.mlw from the IDE. When I try to remove the "module proof node", the IDE tells me : "Cannot remove attached proof nodes or theories, and proof_attempt that did not yet return"

    So, I have to close the IDE, remove the directory corresponding to the session, and relaunch the IDE, and re-start all proofs related to file1.mlw.

    Being able to remove a file (file2.mlw) from a session would be more convenient.

    • Merge request
    • Branch

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading