Add div margin styles to improve vertical spacing of typeset maths. R…

…emove \> controls (tabs), which don't seem to serve any useful purpose, using katexMacros.
fjwright · Sep 13, 2020 · 6fd6d7d · 6fd6d7d
1 parent 211db6a
commit 6fd6d7d
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/fjwright/runreduce/REDUCEPanel.java b/src/fjwright/runreduce/REDUCEPanel.java
@@ -128,7 +128,7 @@ public void log(String message) {
         webEngine.loadContent("<!DOCTYPE html><html><head>" +
                 "<link rel='stylesheet' href='" + REDUCEPanel.class.getResource("katex/katex.min.css") + "'>" +
                 "<script src='" + REDUCEPanel.class.getResource("katex/katex.min.js") + "'></script>" +
-                "<style>pre{margin:0}</style>" +
+                "<style>pre{margin:0}div{margin-top:-1em;margin-bottom:2em}</style>" +
                 "</head><body></body></html>");
         webEngine.getLoadWorker().stateProperty().addListener(
                 (ov, oldState, newState) -> {
@@ -192,7 +192,8 @@ private void outputWebViewAvailable() {
         head = (HTMLElement) html.getElementsByTagName("head").item(0);
         body = doc.getBody();
         katex = (JSObject) webEngine.executeScript("katex");
-        katexMacros = (JSObject) webEngine.executeScript("var katexMacros={'\\\\Int': '\\\\int'};katexMacros;");
+        katexMacros = (JSObject) webEngine.executeScript(
+                "var katexMacros={'\\\\Int':'\\\\int','\\\\>':''};katexMacros;");
 
         // Create default style elements: