src/Pure/General/long_name.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 30359 3f9b3ff851ca
child 55669 4612c450b59c
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     1 (*  Title:      Pure/General/long_name.ML
     2     Author:     Makarius
     3 
     4 Long names.
     5 *)
     6 
     7 signature LONG_NAME =
     8 sig
     9   val separator: string
    10   val is_qualified: string -> bool
    11   val implode: string list -> string
    12   val explode: string -> string list
    13   val append: string -> string -> string
    14   val qualify: string -> string -> string
    15   val qualifier: string -> string
    16   val base_name: string -> string
    17   val map_base_name: (string -> string) -> string -> string
    18 end;
    19 
    20 structure Long_Name: LONG_NAME =
    21 struct
    22 
    23 val separator = ".";
    24 val is_qualified = exists_string (fn s => s = separator);
    25 
    26 val implode = space_implode separator;
    27 val explode = space_explode separator;
    28 
    29 fun append name1 "" = name1
    30   | append "" name2 = name2
    31   | append name1 name2 = name1 ^ separator ^ name2;
    32 
    33 fun qualify qual name =
    34   if qual = "" orelse name = "" then name
    35   else qual ^ separator ^ name;
    36 
    37 fun qualifier "" = ""
    38   | qualifier name = implode (#1 (split_last (explode name)));
    39 
    40 fun base_name "" = ""
    41   | base_name name = List.last (explode name);
    42 
    43 fun map_base_name _ "" = ""
    44   | map_base_name f name =
    45       let val names = explode name
    46       in implode (nth_map (length names - 1) f names) end;
    47 
    48 end;
    49