Thu, 21 Nov 2024 23:07:06 +0100 | wenzelm | more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry); | changeset | files |
Thu, 21 Nov 2024 12:47:42 +0100 | wenzelm | clarified signature and object initialization; | changeset | files |