added merge_alists;
authorwenzelm
Mon Mar 09 16:08:37 1998 +0100 (1998-03-09)
changeset 4692748f4e365d14
parent 4691 b159f5d98ceb
child 4693 2e47ea2c6109
added merge_alists;
moced is_letter etc. to Syntax/symbol.ML;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Mar 09 16:08:06 1998 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Mar 09 16:08:37 1998 +0100
     1.3 @@ -111,13 +111,7 @@
     1.4    val string_of_indexname: string * int -> string
     1.5  
     1.6    (*strings*)
     1.7 -  val is_letter: string -> bool
     1.8 -  val is_digit: string -> bool
     1.9 -  val is_quasi_letter: string -> bool
    1.10 -  val is_blank: string -> bool
    1.11 -  val is_letdig: string -> bool
    1.12 -  val is_printable: string -> bool
    1.13 -  val to_lower: string -> string
    1.14 +  val beginning: string list -> string
    1.15    val enclose: string -> string -> string -> string
    1.16    val quote: string -> string
    1.17    val space_implode: string -> string list -> string
    1.18 @@ -176,6 +170,7 @@
    1.19    val generic_merge: ('a * 'a -> bool) -> ('b -> 'a list) -> ('a list -> 'b) -> 'b -> 'b -> 'b
    1.20    val extend_list: ''a list -> ''a list -> ''a list
    1.21    val merge_lists: ''a list -> ''a list -> ''a list
    1.22 +  val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
    1.23    val merge_rev_lists: ''a list -> ''a list -> ''a list
    1.24  
    1.25    (*balanced trees*)
    1.26 @@ -602,37 +597,8 @@
    1.27  
    1.28  (** strings **)
    1.29  
    1.30 -fun is_letter ch =
    1.31 -  size ch = 1 andalso
    1.32 -   (ord "A" <= ord ch andalso ord ch <= ord "Z" orelse
    1.33 -    ord "a" <= ord ch andalso ord ch <= ord "z");
    1.34 -
    1.35 -fun is_digit ch =
    1.36 -  size ch = 1 andalso ord "0" <= ord ch andalso ord ch <= ord "9";
    1.37 -
    1.38 -(*letter or _ or prime (')*)
    1.39 -fun is_quasi_letter "_" = true
    1.40 -  | is_quasi_letter "'" = true
    1.41 -  | is_quasi_letter ch = is_letter ch;
    1.42 -
    1.43 -(*white space: blanks, tabs, newlines, formfeeds*)
    1.44 -val is_blank : string -> bool =					(* FIXME *)
    1.45 -  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\160" => true
    1.46 -    | _ => false;
    1.47 -
    1.48 -val is_letdig = is_quasi_letter orf is_digit;
    1.49 -
    1.50 -(*printable chars*)
    1.51 -fun is_printable c = size c = 1 andalso ord c > ord " " andalso ord c <= ord "~";
    1.52 -
    1.53 -(*lower all chars of string*)
    1.54 -val to_lower =
    1.55 -  let
    1.56 -    fun lower ch =
    1.57 -      if size ch = 1 andalso ch >= "A" andalso ch <= "Z" then
    1.58 -        chr (ord ch - ord "A" + ord "a")
    1.59 -      else ch;
    1.60 -  in implode o (map lower) o explode end;
    1.61 +(*beginning of text*)
    1.62 +fun beginning cs = implode (take (10, cs)) ^ " ...";
    1.63  
    1.64  (*enclose in brackets*)
    1.65  fun enclose lpar rpar str = lpar ^ str ^ rpar;
    1.66 @@ -894,6 +860,7 @@
    1.67  (*lists as tables*)
    1.68  fun extend_list tab = generic_extend (op =) I I tab;
    1.69  fun merge_lists tab = generic_merge (op =) I I tab;
    1.70 +fun merge_alists tab = generic_merge eq_fst I I tab;
    1.71  
    1.72  fun merge_rev_lists xs [] = xs
    1.73    | merge_rev_lists [] ys = ys