From b9986f0b426ca37502d6f3bcbccc9c5e2cfc18ee Mon Sep 17 00:00:00 2001
From: Markus Koch <markus@notsyncing.net>
Date: Mon, 20 Apr 2020 17:57:49 +0200
Subject: [PATCH] Scale street labels depending on zoom level

---
 htdocs/mapscript.js | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/htdocs/mapscript.js b/htdocs/mapscript.js
index 365a41d..b5417f1 100644
--- a/htdocs/mapscript.js
+++ b/htdocs/mapscript.js
@@ -7,8 +7,8 @@ var streetLabelsRenderer = new L.StreetLabels({
 		return layer.geometry.type == "LineString";
 	},
 	fontStyle: {
-		dynamicFontSize: false,
-		fontSize: 10,
+		dynamicFontSize: true,
+		fontSize: 11,
 		fontSizeUnit: "px",
 		lineWidth: 4.0,
 		fillStyle: "black",
@@ -16,6 +16,15 @@ var streetLabelsRenderer = new L.StreetLabels({
 	},
 });
 
+streetLabelsRenderer._getDynamicFontSize = function () {
+	zoom = mymap.getZoom();
+	if (zoom <= 7)
+		return 11;
+	else
+		return 2**(zoom - 8) * 11;
+}
+
+
 // Projection fix from: https://gis.stackexchange.com/questions/200865/leaflet-crs-simple-custom-scale
 var factorx = 1 / 256 * 4;
 var factory = factorx;