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.;
wenzelm@30359
     1
(*  Title:      Pure/General/long_name.ML
wenzelm@30359
     2
    Author:     Makarius
wenzelm@30359
     3
wenzelm@30359
     4
Long names.
wenzelm@30359
     5
*)
wenzelm@30359
     6
wenzelm@30359
     7
signature LONG_NAME =
wenzelm@30359
     8
sig
wenzelm@30359
     9
  val separator: string
wenzelm@30359
    10
  val is_qualified: string -> bool
wenzelm@30359
    11
  val implode: string list -> string
wenzelm@30359
    12
  val explode: string -> string list
wenzelm@30359
    13
  val append: string -> string -> string
wenzelm@30359
    14
  val qualify: string -> string -> string
wenzelm@30359
    15
  val qualifier: string -> string
wenzelm@30359
    16
  val base_name: string -> string
wenzelm@30359
    17
  val map_base_name: (string -> string) -> string -> string
wenzelm@30359
    18
end;
wenzelm@30359
    19
wenzelm@30359
    20
structure Long_Name: LONG_NAME =
wenzelm@30359
    21
struct
wenzelm@30359
    22
wenzelm@30359
    23
val separator = ".";
wenzelm@30359
    24
val is_qualified = exists_string (fn s => s = separator);
wenzelm@30359
    25
wenzelm@30359
    26
val implode = space_implode separator;
wenzelm@30359
    27
val explode = space_explode separator;
wenzelm@30359
    28
wenzelm@30359
    29
fun append name1 "" = name1
wenzelm@30359
    30
  | append "" name2 = name2
wenzelm@30359
    31
  | append name1 name2 = name1 ^ separator ^ name2;
wenzelm@30359
    32
wenzelm@30359
    33
fun qualify qual name =
wenzelm@30359
    34
  if qual = "" orelse name = "" then name
wenzelm@30359
    35
  else qual ^ separator ^ name;
wenzelm@30359
    36
wenzelm@30359
    37
fun qualifier "" = ""
wenzelm@30359
    38
  | qualifier name = implode (#1 (split_last (explode name)));
wenzelm@30359
    39
wenzelm@30359
    40
fun base_name "" = ""
wenzelm@30359
    41
  | base_name name = List.last (explode name);
wenzelm@30359
    42
wenzelm@30359
    43
fun map_base_name _ "" = ""
wenzelm@30359
    44
  | map_base_name f name =
wenzelm@30359
    45
      let val names = explode name
wenzelm@30359
    46
      in implode (nth_map (length names - 1) f names) end;
wenzelm@30359
    47
wenzelm@30359
    48
end;
wenzelm@30359
    49