author | wenzelm |
Wed, 30 Apr 2014 13:11:24 +0200 | |
changeset 56800 | b904ea8edd73 |
parent 56162 | ea6303e2261b |
child 59888 | 27e4d0ab0948 |
permissions | -rw-r--r-- |
30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/General/long_name.ML |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
3 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
4 |
Long names. |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
5 |
*) |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
6 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
7 |
signature LONG_NAME = |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
8 |
sig |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
9 |
val separator: string |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
10 |
val is_qualified: string -> bool |
55669 | 11 |
val hidden: string -> string |
12 |
val is_hidden: string -> bool |
|
56162
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset
|
13 |
val localN: string |
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset
|
14 |
val is_local: string -> bool |
30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
15 |
val implode: string list -> string |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
16 |
val explode: string -> string list |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
17 |
val append: string -> string -> string |
56023 | 18 |
val qualification: string -> int |
30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
19 |
val qualify: string -> string -> string |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
20 |
val qualifier: string -> string |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
21 |
val base_name: string -> string |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
22 |
val map_base_name: (string -> string) -> string -> string |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
23 |
end; |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
24 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
25 |
structure Long_Name: LONG_NAME = |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
26 |
struct |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
27 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
28 |
val separator = "."; |
56800 | 29 |
|
30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
30 |
val is_qualified = exists_string (fn s => s = separator); |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
31 |
|
55669 | 32 |
fun hidden name = "??." ^ name; |
33 |
val is_hidden = String.isPrefix "??."; |
|
34 |
||
56162
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset
|
35 |
val localN = "local"; |
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset
|
36 |
val is_local = String.isPrefix "local."; |
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset
|
37 |
|
30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
38 |
val implode = space_implode separator; |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
39 |
val explode = space_explode separator; |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
40 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
41 |
fun append name1 "" = name1 |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
42 |
| append "" name2 = name2 |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
43 |
| append name1 name2 = name1 ^ separator ^ name2; |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
44 |
|
56023 | 45 |
fun qualification "" = 0 |
46 |
| qualification name = fold_string (fn s => s = separator ? Integer.add 1) name 1; |
|
47 |
||
30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
48 |
fun qualify qual name = |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
49 |
if qual = "" orelse name = "" then name |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
50 |
else qual ^ separator ^ name; |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
51 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
52 |
fun qualifier "" = "" |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
53 |
| qualifier name = implode (#1 (split_last (explode name))); |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
54 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
55 |
fun base_name "" = "" |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
56 |
| base_name name = List.last (explode name); |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
57 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
58 |
fun map_base_name _ "" = "" |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
59 |
| map_base_name f name = |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
60 |
let val names = explode name |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
61 |
in implode (nth_map (length names - 1) f names) end; |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
62 |
|
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
63 |
end; |
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset
|
64 |