PDF Generation: feature parity with the toolbox

Signed-off-by: Federico Ponzi <me@fponzi.me>
tlaplus · Oct 31, 2024 · f7b181d · f7b181d
1 parent 220a265
commit f7b181d
Show file tree

Hide file tree

Showing 3 changed files with 59 additions and 2 deletions.
diff --git a/package.json b/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",

diff --git a/src/tla2tools.ts b/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;
@@ -102,10 +106,34 @@ export async function runSany(tlaFilePath: string): Promise<ToolProcessInfo> {
 }
 
 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 toolArgs = ['-metadir',
+        path.dirname(tlaFilePath),
+        path.basename(tlaFilePath)];
+
+    if (shadeComments) {
+        toolArgs.unshift('-nops',
+            '-shade',
+            '-grayLevel',
+            commentColor.toString());
+    }
+
+    if (numberLines) {
+        toolArgs.unshift('-number');
+    }
+
+    if (noPcalShade) {
+        toolArgs.unshift('-noPcalShade');
+    }
+
     return runTool(
         TlaTool.TEX,
         tlaFilePath,
-        [ path.basename(tlaFilePath) ],
+        toolArgs,
         []
     );
 }
@@ -148,6 +176,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);

diff --git a/src/webview/checkResultView/headerSection/index.tsx b/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>