From 8fb673e93e59b9876ce72c61dac66766fd88ea59 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Tue, 22 Feb 2022 23:51:01 +0100 Subject: [PATCH] use newly available get_n_chars/3 from library(charsio) --- src/lib/sgml.pl | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/lib/sgml.pl b/src/lib/sgml.pl index 507da1c6..0289278e 100644 --- a/src/lib/sgml.pl +++ b/src/lib/sgml.pl @@ -58,6 +58,7 @@ :- use_module(library(error)). :- use_module(library(dcgs)). :- use_module(library(pio)). +:- use_module(library(charsio)). load_html(Source, Es, Options) :- load_structure_(Source, Es, Options, html). @@ -75,15 +76,8 @@ load_structure_(file(Fs), [E], Options, What) :- load_(What, Cs, E, Options). load_structure_(stream(Stream), [E], Options, What) :- must_be(list, Options), - read_to_end(Stream, Cs), + get_n_chars(Stream, _, Cs), load_(What, Cs, E, Options). load_(html, Cs, E, Options) :- '$load_html'(Cs, E, Options). load_(xml, Cs, E, Options) :- '$load_xml'(Cs, E, Options). - -read_to_end(Stream, Cs) :- - '$get_n_chars'(Stream, 4096, Cs0), - ( Cs0 = [] -> Cs = [] - ; partial_string(Cs0, Cs, Rest), - read_to_end(Stream, Rest) - ). -- 2.54.0