-
Notifications
You must be signed in to change notification settings - Fork 37.7k
Description
I have an extension and would like to "fully" open an editor that is already open, but only in preview mode (italic file name). So I would like to change the state of an TextEditor that is already open as if it was opened with the preview=false option in TextDocumentShowOptions.
I would also like to check if the current editor is in preview mode or "fully" opened from the API.
(The use case is the extension for the proof assistant coq: Source files are processed interactively in the editor and involve "augmenting" each command in the file with the current proof state. Those operations can be quire resource intensive and it would be a shame if the user accidently closes the file (while a lot of 'compilation' work was done in the background that augments the document) because he only opened the file in preview mode).
I know that I probably can disable preview mode all together, but that would only be a workaround, as the preview mode can be handy.