replace adjacent whitespace characters with a single SPACE character
This commit is contained in:
@@ -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)
|
||||
).
|
||||
|
||||
Reference in New Issue
Block a user