PDF Generation: feature parity with the toolbox

Signed-off-by: Federico Ponzi <me@fponzi.me>

CHANGELOG.md

@@ -1,3 +1,9 @@
+## 1.7.0 
+
+### Enhancements
+* Generate PDF feature matching the toolbox by adding missing settings.
+
+
 ## 1.5.4 – 21st March, 2021
 
 ### Enhancements

package.json

@@ -382,6 +382,31 @@
                     "maxLength": 1000,
                     "description": "Command to produce PDFs from .tex files."
                 },
+                "tlaplus.pdf.commentsShade": {
+                    "default": true,
+                    "type": "boolean",
+                    "scope": "application",
+                    "description": "If enabled, comments will have a gray background."
+                },
+                "tlaplus.pdf.commentsShadeColor": {
+                    "default": 0.85,
+                    "type": "number",
+                    "scope": "application",
+                    "maxLength": 10,
+                    "description": "If comments are shaded in gray, this config changes the darkness of the shading. This must be a number between 0.0 (completely black) and 1.0 (no shading)."
+                },
+                "tlaplus.pdf.numberLines": {
+                    "default": false,
+                    "type": "boolean",
+                    "scope": "application",
+                    "description": "Show line numbers in PDFs."
+                },
+                "tlaplus.pdf.noPcalShade": {
+                    "default": false,
+                    "type": "boolean",
+                    "scope": "application",
+                    "description": "Causes a PlusCal algorithm (which appear in a comment) not to be shaded.  (The algorithm's comments will be shaded.)"
+                },
                 "tlaplus.tlaps.enabled": {
                     "type": "boolean",
                     "default": false,
@@ -504,6 +529,7 @@
         "vscode:prepublish": "npm run compile -- --production",
         "compile": "node ./esbuild.js",
         "lint": "eslint --ext .ts,.tsx src/ tests/",
+        "lint:fix": "eslint --fix --ext .ts,.tsx src/ tests/",
         "watch": "npm run compile -- --watch",
         "pretest": "tsc -p ./",
         "test": "node ./out/tests/runTest.js",

src/tla2tools.ts

@@ -17,6 +17,10 @@ const CFG_JAVA_OPTIONS = 'tlaplus.java.options';
 const CFG_TLC_OPTIONS = 'tlaplus.tlc.modelChecker.options';
 const CFG_PLUSCAL_OPTIONS = 'tlaplus.pluscal.options';
 const CFG_TLC_OPTIONS_PROMPT = 'tlaplus.tlc.modelChecker.optionsPrompt';
+const CFG_TLA_PDF_NUMBER_LINES = 'tlaplus.pdf.numberLines';
+const CFG_TLA_PDF_NO_PCAL_SHADE = 'tlaplus.pdf.noPcalShade';
+const CFG_TLA_PDF_COMMENTS_SHADE = 'tlaplus.pdf.commentsShade';
+const CFG_TLA_PDF_COMMENTS_SHADE_COLOR = 'tlaplus.pdf.commentsShadeColor';
 
 const VAR_TLC_SPEC_NAME = /\$\{specName\}/g;
 const VAR_TLC_MODEL_NAME = /\$\{modelName\}/g;
@@ -101,11 +105,38 @@ export async function runSany(tlaFilePath: string): Promise<ToolProcessInfo> {
     );
 }
 
+function buildTexOptions(tlaFilePath: string, shadeComments: boolean, commentColor: number, numberLines: boolean, noPcalShade: boolean): string[] {
+    const toolArgs = [path.basename(tlaFilePath)];
+
+    if (shadeComments) {
+        toolArgs.unshift('-nops',
+            '-shade',
+            '-grayLevel',
+            commentColor.toString());
+    }
+
+    if (numberLines) {
+        toolArgs.unshift('-number');
+    }
+
+    if (noPcalShade) {
+        toolArgs.unshift('-noPcalShade');
+    }
+    return toolArgs;
+}
+
 export async function runTex(tlaFilePath: string): Promise<ToolProcessInfo> {
+    const shadeComments = vscode.workspace.getConfiguration().get<boolean>(CFG_TLA_PDF_COMMENTS_SHADE, true);
+    const commentColor = vscode.workspace.getConfiguration().get<number>(CFG_TLA_PDF_COMMENTS_SHADE_COLOR, 0.85);
+    const numberLines = vscode.workspace.getConfiguration().get<boolean>(CFG_TLA_PDF_NUMBER_LINES, false);
+    const noPcalShade = vscode.workspace.getConfiguration().get<boolean>(CFG_TLA_PDF_NO_PCAL_SHADE, false);
+
+    const options = buildTexOptions(tlaFilePath, shadeComments, commentColor, numberLines, noPcalShade);
+
     return runTool(
         TlaTool.TEX,
         tlaFilePath,
-        [ path.basename(tlaFilePath) ],
+        options,
         []
     );
 }
@@ -148,6 +179,8 @@ async function runTool(
     toolOptions: string[],
     javaOptions: string[]
 ): Promise<ToolProcessInfo> {
+    // log the arugments:
+    //console.log(toolName + ': ' + filePath + ' ' + toolOptions.join(' ') + ' ' + javaOptions.join(' '));
     const javaPath = await obtainJavaPath();
     // TODO: Merge cfgOptions with javaOptions to avoid complete overrides.
     const cfgOptions = getConfigOptions(CFG_JAVA_OPTIONS);

src/webview/checkResultView/headerSection/index.tsx

@@ -34,7 +34,8 @@ export const HeaderSection = React.memo(({checkResult}: HeaderSectionI) => {
                 <span hidden={checkResult.state !== 'R'}>
                     (<VSCodeLink onClick={vscode.stopProcess} href="#"> stop </VSCodeLink>)
                 </span>
-                <span hidden={ checkResult.statusDetails === undefined || checkResult.statusDetails === null}>: {' ' + checkResult.statusDetails} </span>
+                <span hidden={ checkResult.statusDetails === undefined
+                    || checkResult.statusDetails === null}>: {' ' + checkResult.statusDetails} </span>
             </div>
 
             <div className="timeInfo"> Start: {checkResult.startDateTimeStr}, end: {checkResult.endDateTimeStr} </div>