diff --git a/README.md b/README.md index 059834f..19c9ff5 100644 --- a/README.md +++ b/README.md @@ -151,3 +151,13 @@ Run-REDUCE-FX currently uses a bundled copy of * Handle more of the non-standard TeX markup generated by fmprint. ### Updates since last release + +* v1.91 Replace all KaTeX woff2 fonts with woff versions. + This fixes the big delimiters problem. I hope that WebView in a later + version of JavaFX will accept woff2 fonts and I can switch back. +* Add WebEngine debugging code from debugWebEngine branch. +* Add div margin styles to improve vertical spacing of typeset maths. +* Remove \> controls (tabs) from fmprint output, which don't seem to serve any + useful purpose, using katexMacros. +* Always insert parentheses when calling a function using the pop-up keyboard, + and rewrite ln to log. diff --git a/src/fjwright/runreduce/PopupKeyboard.java b/src/fjwright/runreduce/PopupKeyboard.java index b5ef3af..f4c1f48 100644 --- a/src/fjwright/runreduce/PopupKeyboard.java +++ b/src/fjwright/runreduce/PopupKeyboard.java @@ -373,19 +373,23 @@ private static void btmKbdButtonAction(MouseEvent mouseEvent, boolean trigHyp) { // FixMe but can't do that from this static context! } else switch (text) { + case "ln": + text = "log"; + break; case "āˆšā€¾": - text = "\u200Cāˆš "; + text = "\u200Cāˆš"; break; case "!": text = "factorial"; break; } - // Wrap selected text in target TextInputControl or - // insert text at caret if no text is selected: + // Wrap selected text in target TextInputControl or insert text + // followed by () at caret and backup if no text is selected: final TextInputControl textInput = (TextInputControl) target; - if (textInput.getSelectedText().isEmpty()) - textInput.insertText(textInput.getCaretPosition(), text); - else { + if (textInput.getSelectedText().isEmpty()) { + textInput.insertText(textInput.getCaretPosition(), text + "()"); + textInput.backward(); + } else { final IndexRange selection = textInput.getSelection(); textInput.insertText(selection.getStart(), text + "("); textInput.insertText(selection.getEnd() + text.length() + 1, ")");