search

tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
357 stars 33 forks source link

Generating PDF does not gray shade comments #348

Closed chris-ortiz-wdc closed 3 weeks ago

chris-ortiz-wdc commented 4 weeks ago

Description:

In the ToolBox, this what it looks like generating PDF. image But in VScode, this what it looks like generating the same PDF. image

Steps to reproduce:

In VSCode command palette execute TLA+ Export module to PDF

Expectations:

I expect the same comment to appear with gray shading as in the ToolBox.

Version Information:

FedericoPonzi commented 4 weeks ago

Thanks for reporting! The production process seems identical to the toolbox's, but in there additional parameters are set: https://github.com/tlaplus/tlaplus/blob/ab14a33e39c78e4c88e81b664b9a8c916b943cab/toolbox/org.lamport.tla.toolbox.tool.tla2tex/src/org/lamport/tla/toolbox/tool/tla2tex/handler/ProducePDFHandler.java#L130

                    tla2texArgs.add("-grayLevel");
                    tla2texArgs
                            .add(Double.toString(preferenceStore
                                    .getDouble(ITLA2TeXPreferenceConstants.GRAY_LEVEL)));

These are customizable from the toolbox's settings. I think we would need to add the same settings in the vscode plugin.

FedericoPonzi commented 3 weeks ago

Just merged a fix for this one, can you please download the latest plugin version and try it out? Feel free to reopen this if anything looks off.

chris-ortiz-wdc commented 3 weeks ago

I checked it out, it works. Thanks for the quick fixing of this issue. Only thing I noticed is that I was not able to see the Pdf Options you mentioned in #349 . Maybe I am missing something but that is separate concern from what is reported here so this issue is no need to reopen. I really appreciate the support provided here.

I am using latest TLA+: v2024.11.41524

Thanks, Chris

FedericoPonzi commented 3 weeks ago

Can you please search for tlaplus.pdf. or tlaplus.pdf.commentsShadeColor in the settings and let me know if they show up?

image

chris-ortiz-wdc commented 3 weeks ago

I able to see it now. What I did, even they were already uninstalled, I made sure I have deleted the 2 TLA+ alygin versions (released and nightly) from my home.vscode\extensions and home.vscode-insiders\extensions and reloaded my VScode. I can now see the Pdf options in the User tab, but not yet in the Workspace tab. Thank you for the help.

image