add unput_line function for Stream. With it, a line can unput to stream in 1 ope…

…ration. It's most useful than unput_byte.

add unput_line function for Stream. With it, a line can unput to stream in 1 ope…
…ration. It's most useful than unput_byte.
David René
1 parent 66a7d78b
Showing 1 changed file with 8 additions and 1 deletions Show diff stats
anubis_dev/library/tools/streams.anubis
@@ -460,7 +460,14 @@ public define List(String)
   ) = 
   read_lines(s, []).
  
-   
+public define One
+  unput_line
+  (
+    Stream  s,
+    String  line
+  )=
+  forget(map((Word8 c) |-> ub(s)(c) , reverse(explode(line)))).
+  
 public define One
    skip_blanks
      (