author  wenzelm 
Fri, 03 Apr 2015 18:36:19 +0200  
changeset 59916  f673ce6b1e2b 
parent 59888  27e4d0ab0948 
child 65358  e345e9420109 
permissions  rwrr 
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 
59916  12 
val is_hidden: string > bool 
59888  13 
val dest_hidden: string > string option 
56162
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset

14 
val localN: string 
59888  15 
val dest_local: string > string option 
30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

16 
val implode: string list > string 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

17 
val explode: string > string list 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

18 
val append: string > string > string 
56023  19 
val qualification: string > int 
30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

20 
val qualify: string > string > string 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

21 
val qualifier: string > string 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

22 
val base_name: string > string 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

23 
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

24 
end; 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

25 

3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

26 
structure Long_Name: LONG_NAME = 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

27 
struct 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

28 

3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

29 
val separator = "."; 
56800  30 

30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

31 
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

32 

59916  33 
val hidden_prefix = "??." 
34 
val hidden = prefix hidden_prefix; 

35 
val is_hidden = String.isPrefix hidden_prefix; 

36 
val dest_hidden = try (unprefix hidden_prefix); 

55669  37 

56162
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset

38 
val localN = "local"; 
59888  39 
val dest_local = try (unprefix "local."); 
56162
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset

40 

30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

41 
val implode = space_implode separator; 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

42 
val explode = space_explode separator; 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

43 

3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

44 
fun append name1 "" = name1 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

45 
 append "" name2 = name2 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

46 
 append name1 name2 = name1 ^ separator ^ name2; 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

47 

56023  48 
fun qualification "" = 0 
49 
 qualification name = fold_string (fn s => s = separator ? Integer.add 1) name 1; 

50 

30359
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

51 
fun qualify qual name = 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

52 
if qual = "" orelse name = "" then name 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

53 
else qual ^ separator ^ 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 qualifier "" = "" 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

56 
 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

57 

3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

58 
fun base_name "" = "" 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

59 
 base_name name = List.last (explode name); 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

60 

3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

61 
fun map_base_name _ "" = "" 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

62 
 map_base_name f name = 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

63 
let val names = explode name 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

64 
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

65 

3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

66 
end; 
3f9b3ff851ca
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff
changeset

67 