src/Pure/library.ML
 changeset 4956 a7538e43896e parent 4945 d8c809afafb8 child 4995 905cd6f73429
```--- a/src/Pure/library.ML	Mon May 25 12:55:01 1998 +0200
+++ b/src/Pure/library.ML	Mon May 25 21:10:45 1998 +0200
@@ -73,6 +73,7 @@
val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
+  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
val length: 'a list -> int
val take: int * 'a list -> 'a list
val drop: int * 'a list -> 'a list
@@ -96,6 +97,7 @@
val map2: ('a * 'b -> 'c) -> 'a list * 'b list -> 'c list
val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val forall2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
+  val seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit
val ~~ : 'a list * 'b list -> ('a * 'b) list
val split_list: ('a * 'b) list -> 'a list * 'b list
val prefix: ''a list * ''a list -> bool
@@ -412,6 +414,13 @@
| itr (x::l) = f(x, itr l)
in  itr l  end;

+fun foldl_map _ (x, []) = (x, [])
+  | foldl_map f (x, y :: ys) =
+      let
+        val (x', y') = f (x, y);
+        val (x'', ys') = foldl_map f (x', ys);
+      in (x'', y' :: ys') end;
+

(* basic list functions *)

@@ -540,6 +549,10 @@
| forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
| forall2 _ _ = raise LIST "forall2";

+fun seq2 _ ([], []) = ()
+  | seq2 f (x :: xs, y :: ys) = (f (x, y); seq2 f (xs, ys))
+  | seq2 _ _ = raise LIST "seq2";
+
(*combine two lists forming a list of pairs:
[x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
fun [] ~~ [] = []
@@ -625,7 +638,8 @@
(** strings **)

(*beginning of text*)
-fun beginning cs = implode (take (10, cs)) ^ " ...";
+fun beginning cs =
+  implode (map (fn c => if ord c < ord " " then " " else c) (take (10, cs))) ^ " ...";

(*enclose in brackets*)
fun enclose lpar rpar str = lpar ^ str ^ rpar;```