File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -151,3 +151,13 @@ Run-REDUCE-FX currently uses a bundled copy of
151151* Handle more of the non-standard TeX markup generated by fmprint.
152152
153153### Updates since last release
154+
155+ * v1.91 Replace all KaTeX woff2 fonts with woff versions.
156+ This fixes the big delimiters problem. I hope that WebView in a later
157+ version of JavaFX will accept woff2 fonts and I can switch back.
158+ * Add WebEngine debugging code from debugWebEngine branch.
159+ * Add div margin styles to improve vertical spacing of typeset maths.
160+ * Remove \> controls (tabs) from fmprint output, which don't seem to serve any
161+ useful purpose, using katexMacros.
162+ * Always insert parentheses when calling a function using the pop-up keyboard,
163+ and rewrite ln to log.
Original file line number Diff line number Diff line change @@ -373,19 +373,23 @@ private static void btmKbdButtonAction(MouseEvent mouseEvent, boolean trigHyp) {
373373 // FixMe but can't do that from this static context!
374374 } else
375375 switch (text ) {
376+ case "ln" :
377+ text = "log" ;
378+ break ;
376379 case "√‾" :
377- text = "\u200C √ " ;
380+ text = "\u200C √" ;
378381 break ;
379382 case "!" :
380383 text = "factorial" ;
381384 break ;
382385 }
383- // Wrap selected text in target TextInputControl or
384- // insert text at caret if no text is selected:
386+ // Wrap selected text in target TextInputControl or insert text
387+ // followed by () at caret and backup if no text is selected:
385388 final TextInputControl textInput = (TextInputControl ) target ;
386- if (textInput .getSelectedText ().isEmpty ())
387- textInput .insertText (textInput .getCaretPosition (), text );
388- else {
389+ if (textInput .getSelectedText ().isEmpty ()) {
390+ textInput .insertText (textInput .getCaretPosition (), text + "()" );
391+ textInput .backward ();
392+ } else {
389393 final IndexRange selection = textInput .getSelection ();
390394 textInput .insertText (selection .getStart (), text + "(" );
391395 textInput .insertText (selection .getEnd () + text .length () + 1 , ")" );
You can’t perform that action at this time.
0 commit comments