vscode-tlaplus icon indicating copy to clipboard operation
vscode-tlaplus copied to clipboard

Add "creation and last modified" footer to specs

Open lemmy opened this issue 3 years ago • 2 comments

The Toolbox automatically adds a footer to every spec that shows the original author and creation date and all modifications by other authors.

Toolbox implementation: https://github.com/tlaplus/tlaplus/blob/df144c5f0e93b996362a199afa43cf453f4c2856/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/TLAEditor.java#L551-L640

lemmy avatar Dec 22 '21 18:12 lemmy

Don't think this is very useful in the era of ubiquitous automated version control systems.

ahelwer avatar Feb 01 '22 18:02 ahelwer

This feature is for those who have seen SCMs come and go or who have experienced specs being moved around; others can turn it off (like it is possible in the Toolbox).

lemmy avatar Feb 01 '22 18:02 lemmy