# HG changeset patch # User haftmann # Date 1167243005 -3600 # Node ID 77372f38aa98d322401e610c395eed302c958b1b # Parent 1224048fb8f9e5f1d6c492c57ae93c2b8e96cf02 added split diff -r 1224048fb8f9 -r 77372f38aa98 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Wed Dec 27 19:10:04 2006 +0100 +++ b/src/Pure/General/name_space.ML Wed Dec 27 19:10:05 2006 +0100 @@ -28,6 +28,7 @@ val qualified: string -> string -> string val base: string -> string val qualifier: string -> string + val split: string -> string * string val map_base: (string -> string) -> string -> string val suffixes_prefixes: 'a list -> 'a list list val suffixes_prefixes_split: int -> int -> 'a list -> 'a list list @@ -87,6 +88,9 @@ fun qualifier "" = "" | qualifier name = implode_name (#1 (split_last (explode_name name))); +fun split "" = ("", "") + | split name = (apfst implode_name o split_last o explode_name) name; + fun map_base _ "" = "" | map_base f name = let val names = explode_name name