PDF Generation: feature parity with the toolbox

Signed-off-by: Federico Ponzi <[email protected]>

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,

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,33 @@ 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);
+
+    var 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 +175,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);