renamed NameSpace.drop_base to NameSpace.qualifier;
authorwenzelm
Wed Sep 13 21:41:25 2006 +0200 (2006-09-13)
changeset 20530448594cbd82b
parent 20529 1ca27b3ed2e7
child 20531 7de9caf4fd78
renamed NameSpace.drop_base to NameSpace.qualifier;
doc-src/IsarImplementation/Thy/document/prelim.tex
doc-src/IsarImplementation/Thy/prelim.thy
src/Pure/General/name_space.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Sep 13 12:40:39 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Sep 13 21:41:25 2006 +0200
     1.3 @@ -802,7 +802,7 @@
     1.4  \begin{isamarkuptext}%
     1.5  \begin{mldecls}
     1.6    \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
     1.7 -  \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\  %FIXME qualifier
     1.8 +  \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
     1.9    \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
    1.10    \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
    1.11    \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
    1.12 @@ -823,7 +823,7 @@
    1.13    \item \verb|NameSpace.base|~\isa{name} returns the base name of a
    1.14    qualified name.
    1.15  
    1.16 -  \item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
    1.17 +  \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier
    1.18    of a qualified name.
    1.19  
    1.20    \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
     2.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Wed Sep 13 12:40:39 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Wed Sep 13 21:41:25 2006 +0200
     2.3 @@ -694,7 +694,7 @@
     2.4  text %mlref {*
     2.5    \begin{mldecls}
     2.6    @{index_ML NameSpace.base: "string -> string"} \\
     2.7 -  @{index_ML NameSpace.drop_base: "string -> string"} \\  %FIXME qualifier
     2.8 +  @{index_ML NameSpace.qualifier: "string -> string"} \\
     2.9    @{index_ML NameSpace.append: "string -> string -> string"} \\
    2.10    @{index_ML NameSpace.pack: "string list -> string"} \\
    2.11    @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
    2.12 @@ -715,7 +715,7 @@
    2.13    \item @{ML NameSpace.base}~@{text "name"} returns the base name of a
    2.14    qualified name.
    2.15  
    2.16 -  \item @{ML NameSpace.drop_base}~@{text "name"} returns the qualifier
    2.17 +  \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier
    2.18    of a qualified name.
    2.19  
    2.20    \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
     3.1 --- a/src/Pure/General/name_space.ML	Wed Sep 13 12:40:39 2006 +0200
     3.2 +++ b/src/Pure/General/name_space.ML	Wed Sep 13 21:41:25 2006 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4    val append: string -> string -> string
     3.5    val qualified: string -> string -> string
     3.6    val base: string -> string
     3.7 -  val drop_base: string -> string
     3.8 +  val qualifier: string -> string
     3.9    val map_base: (string -> string) -> string -> string
    3.10    val suffixes_prefixes: 'a list -> 'a list list
    3.11    val suffixes_prefixes_split: int -> int -> 'a list -> 'a list list
    3.12 @@ -84,8 +84,8 @@
    3.13  fun base "" = ""
    3.14    | base name = List.last (unpack name);
    3.15  
    3.16 -fun drop_base "" = ""
    3.17 -  | drop_base name = pack (#1 (split_last (unpack name)));
    3.18 +fun qualifier "" = ""
    3.19 +  | qualifier name = pack (#1 (split_last (unpack name)));
    3.20  
    3.21  fun map_base _ "" = ""
    3.22    | map_base f name =
    3.23 @@ -248,7 +248,7 @@
    3.24  fun add_path elems (Naming (path, policy)) =
    3.25    if elems = "//" then Naming ("", (qualified, #2 policy))
    3.26    else if elems = "/" then Naming ("", policy)
    3.27 -  else if elems = ".." then Naming (drop_base path, policy)
    3.28 +  else if elems = ".." then Naming (qualifier path, policy)
    3.29    else Naming (append path elems, policy);
    3.30  
    3.31  fun no_base_names (Naming (path, (qualify, accs))) =