src/Pure/library.ML

 
 exception OPTION of string;
 
 fun the (Some x) = x
   | the None = raise OPTION "the";
+
+fun if_none None y = y
+  | if_none (Some x) _ = x;
 
 fun is_some (Some _) = true
   | is_some None = false;
 
 fun is_none (Some _) = false

 (*inverse of ~~; the old 'split':
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
 fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l);
 
 
-
 (* prefixes, suffixes *)
 
 infix prefix;
 fun [] prefix _ = true
   | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys)

 
 (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., x(i-1)], [xi, ..., xn])
    where xi is the first element that does not satisfy the predicate*)
 fun take_prefix (pred : 'a -> bool)  (xs: 'a list) : 'a list * 'a list =
   let fun take (rxs, []) = (rev rxs, [])
-        | take (rxs, x::xs) =
-            if  pred x  then  take(x::rxs, xs)  else  (rev rxs, x::xs)
+        | take (rxs, x :: xs) =
+            if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
   in  take([], xs)  end;
 
 (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
    where xi is the last element that does not satisfy the predicate*)
 fun take_suffix _ [] = ([], [])

         chr (ord ch - ord "A" + ord "a")
       else ch;
   in implode o (map lower) o explode end;
 
 
+(*parentesize*)
+fun parents lpar rpar str = lpar ^ str ^ rpar;
+
 (*simple quoting (does not escape special chars)*)
-fun quote s = "\"" ^ s ^ "\"";
+val quote = parents "\"" "\"";
 
 (*space_implode "..." (explode "hello"); gives "h...e...l...l...o"*)
 fun space_implode a bs = implode (separate a bs);
 
+val commas = space_implode ", ";
+
 (*concatenate messages, one per line, into a string*)
-val cat_lines = implode o (map (apr (op ^, "\n")));
+val cat_lines = space_implode "\n";
 
 
 
 (** lists as sets **)
 

 (*returns the tail beginning with the first repeated element, or []*)
 fun findrep [] = []
   | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
 
 
+(*returns a list containing all repeated elements exactly once; preserves
+  order, takes first of equal elements*)
+fun gen_duplicates eq lst =
+  let
+    val memb = gen_mem eq;
+
+    fun dups (rev_dups, []) = rev rev_dups
+      | dups (rev_dups, x :: xs) =
+          if memb (x, rev_dups) orelse not (memb (x, xs)) then
+            dups (rev_dups, xs)
+          else dups (x :: rev_dups, xs);
+  in
+    dups ([], lst)
+  end;
+
+val duplicates = gen_duplicates (op =);
+
+
 
 (** association lists **)
 
 (*association list lookup*)
 fun assoc ([], key) = None

 
 fun assocs ps x =
   (case assoc (ps, x) of
     None => []
   | Some ys => ys);
+
+(*two-fold association list lookup*)
+fun assoc2 (aal, (key1, key2)) =
+  (case assoc (aal, key1) of
+    Some al => assoc (al, key2)
+  | None => None);
 
 (*generalized association list lookup*)
 fun gen_assoc eq ([], key) = None
   | gen_assoc eq ((keyi, xi) :: pairs, key) =
       if eq (key, keyi) then Some xi else gen_assoc eq (pairs, key);