Rework the Search popup and highlight what matched

- The search field is a single-line field, so Enter no longer adds a
  line break that made every search come up empty.
- The field, button and list use real font sizes from the theme instead
  of being drawn at half size and scaled up, so the text is sharp, and
  everything fits inside the panel.
- Results have alternating row backgrounds like the other lists, a count
  ("3 of 1045 soundtracks") and a message when nothing matches.
- The letters that matched are highlighted.
- Searches shorter than Settings.LETTERS_FOR_LOOSE_SEARCH (3) only find
  names that contain the text, instead of names with the letters far
  apart, which matched most of the library. The Statistics tab uses the
  same search.

data/settings.gd

@@ -4,6 +4,10 @@ extends Node
 ## Registered as the [code]Settings[/code] autoload.
 
 const MAX_NUMBER_OF_PLAYERS: int = 7
+## How many letters a search needs before it also finds names with the letters in order
+## but apart, e.g. "lttp" for "A Link to the Past". Shorter searches only find names
+## that contain the text, since a letter or two in order matches most of the library.
+const LETTERS_FOR_LOOSE_SEARCH: int = 3
 
 var default_path: String = "https://music.sanplex.xyz"
 ## Password for getting an API token from the server. Any password works when the