From 75aec69de1affc63719150b9c7f28489e497877e Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 27 Aug 2023 12:55:29 +0200 Subject: [PATCH] replace adjacent whitespace characters with a single SPACE character --- src/lib/xpath.pl | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/lib/xpath.pl b/src/lib/xpath.pl index 4ec01203..10f0fdef 100644 --- a/src/lib/xpath.pl +++ b/src/lib/xpath.pl @@ -642,7 +642,8 @@ normalize_space(Cs0, Cs) :- no_leading_whitespace(Cs0, Cs1), reverse(Cs1, Cs2), no_leading_whitespace(Cs2, Cs3), - reverse(Cs3, Cs). + reverse(Cs3, Cs4), + single_intermediate_space(Cs4, Cs). no_leading_whitespace([], []). no_leading_whitespace([C0|Cs0], Cs) :- @@ -650,3 +651,13 @@ no_leading_whitespace([C0|Cs0], Cs) :- no_leading_whitespace(Cs0, Cs) ; Cs = [C0|Cs0] ). + +single_intermediate_space([], []). +single_intermediate_space([C0|Cs0], [C|Cs]) :- + ( char_type(C0, whitespace) -> + no_leading_whitespace(Cs0, Cs1), + C = ' ', + single_intermediate_space(Cs1, Cs) + ; C = C0, + single_intermediate_space(Cs0, Cs) + ). -- 2.54.0