src/Pure/General/name_space.ML
changeset 59939 7d46aa03696e
parent 59925 32402fe5ae6a
child 59990 a81dc82ecba3
     1.1 --- a/src/Pure/General/name_space.ML	Mon Apr 06 17:28:07 2015 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Apr 06 22:11:01 2015 +0200
     1.3 @@ -35,8 +35,11 @@
     1.4    val get_scopes: naming -> Binding.scope list
     1.5    val get_scope: naming -> Binding.scope option
     1.6    val new_scope: naming -> Binding.scope * naming
     1.7 +  val limited: bool -> Position.T -> naming -> naming
     1.8    val private_scope: Binding.scope -> naming -> naming
     1.9    val private: Position.T -> naming -> naming
    1.10 +  val restricted_scope: Binding.scope -> naming -> naming
    1.11 +  val restricted: Position.T -> naming -> naming
    1.12    val concealed: naming -> naming
    1.13    val get_group: naming -> serial option
    1.14    val set_group: serial option -> naming -> naming
    1.15 @@ -297,62 +300,73 @@
    1.16  
    1.17  datatype naming = Naming of
    1.18   {scopes: Binding.scope list,
    1.19 -  private: Binding.scope option,
    1.20 +  limited: (bool * Binding.scope) option,
    1.21    concealed: bool,
    1.22    group: serial option,
    1.23    theory_name: string,
    1.24    path: (string * bool) list};
    1.25  
    1.26 -fun make_naming (scopes, private, concealed, group, theory_name, path) =
    1.27 -  Naming {scopes = scopes, private = private, concealed = concealed,
    1.28 +fun make_naming (scopes, limited, concealed, group, theory_name, path) =
    1.29 +  Naming {scopes = scopes, limited = limited, concealed = concealed,
    1.30      group = group, theory_name = theory_name, path = path};
    1.31  
    1.32 -fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
    1.33 -  make_naming (f (scopes, private, concealed, group, theory_name, path));
    1.34 +fun map_naming f (Naming {scopes, limited, concealed, group, theory_name, path}) =
    1.35 +  make_naming (f (scopes, limited, concealed, group, theory_name, path));
    1.36  
    1.37 -fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    1.38 -  (scopes, private, concealed, group, theory_name, f path));
    1.39  
    1.40 +(* scope and access limitation *)
    1.41  
    1.42  fun get_scopes (Naming {scopes, ...}) = scopes;
    1.43  val get_scope = try hd o get_scopes;
    1.44  
    1.45 -fun put_scope scope =
    1.46 -  map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    1.47 -    (scope :: scopes, private, concealed, group, theory_name, path));
    1.48 -
    1.49  fun new_scope naming =
    1.50    let
    1.51      val scope = Binding.new_scope ();
    1.52      val naming' =
    1.53 -      naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    1.54 -        (scope :: scopes, private, concealed, group, theory_name, path));
    1.55 +      naming |> map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
    1.56 +        (scope :: scopes, limited, concealed, group, theory_name, path));
    1.57    in (scope, naming') end;
    1.58  
    1.59 -fun private_scope scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
    1.60 -  (scopes, SOME scope, concealed, group, theory_name, path));
    1.61 +fun limited_scope strict scope =
    1.62 +  map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
    1.63 +    (scopes, SOME (strict, scope), concealed, group, theory_name, path));
    1.64  
    1.65 -fun private pos naming =
    1.66 +fun limited strict pos naming =
    1.67    (case get_scope naming of
    1.68 -    SOME scope => private_scope scope naming
    1.69 -  | NONE => error ("Missing local scope -- cannot declare private names" ^ Position.here pos));
    1.70 +    SOME scope => limited_scope strict scope naming
    1.71 +  | NONE => error ("Missing local scope -- cannot limit name space accesses" ^ Position.here pos));
    1.72 +
    1.73 +val private_scope = limited_scope true;
    1.74 +val private = limited true;
    1.75 +
    1.76 +val restricted_scope = limited_scope false;
    1.77 +val restricted = limited false;
    1.78  
    1.79 -val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
    1.80 -  (scopes, private, true, group, theory_name, path));
    1.81 +val concealed = map_naming (fn (scopes, limited, _, group, theory_name, path) =>
    1.82 +  (scopes, limited, true, group, theory_name, path));
    1.83 +
    1.84  
    1.85 -fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
    1.86 -  (scopes, private, concealed, group, theory_name, path));
    1.87 +(* additional structural info *)
    1.88 +
    1.89 +fun set_theory_name theory_name = map_naming (fn (scopes, limited, concealed, group, _, path) =>
    1.90 +  (scopes, limited, concealed, group, theory_name, path));
    1.91  
    1.92  fun get_group (Naming {group, ...}) = group;
    1.93  
    1.94 -fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
    1.95 -  (scopes, private, concealed, group, theory_name, path));
    1.96 +fun set_group group = map_naming (fn (scopes, limited, concealed, _, theory_name, path) =>
    1.97 +  (scopes, limited, concealed, group, theory_name, path));
    1.98  
    1.99  fun new_group naming = set_group (SOME (serial ())) naming;
   1.100  val reset_group = set_group NONE;
   1.101  
   1.102 +
   1.103 +(* name entry path *)
   1.104 +
   1.105  fun get_path (Naming {path, ...}) = path;
   1.106  
   1.107 +fun map_path f = map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
   1.108 +  (scopes, limited, concealed, group, theory_name, f path));
   1.109 +
   1.110  fun add_path elems = map_path (fn path => path @ [(elems, false)]);
   1.111  val root_path = map_path (fn _ => []);
   1.112  val parent_path = map_path (perhaps (try (#1 o split_last)));
   1.113 @@ -365,14 +379,16 @@
   1.114  val local_naming = global_naming |> add_path Long_Name.localN;
   1.115  
   1.116  
   1.117 -(* visibility flags *)
   1.118 +(* transform *)
   1.119  
   1.120 -fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
   1.121 -  fold private_scope (the_list private') #>
   1.122 +fun transform_naming (Naming {limited = limited', concealed = concealed', ...}) =
   1.123 +  (case limited' of
   1.124 +    SOME (strict, scope) => limited_scope strict scope
   1.125 +  | NONE => I) #>
   1.126    concealed' ? concealed;
   1.127  
   1.128 -fun transform_binding (Naming {private, concealed, ...}) =
   1.129 -  Binding.private_default private #>
   1.130 +fun transform_binding (Naming {limited, concealed, ...}) =
   1.131 +  Binding.limited_default limited #>
   1.132    concealed ? Binding.concealed;
   1.133  
   1.134  
   1.135 @@ -400,11 +416,12 @@
   1.136  
   1.137  fun accesses naming binding =
   1.138    (case name_spec naming binding of
   1.139 -    {accessible = false, ...} => ([], [])
   1.140 -  | {spec, ...} =>
   1.141 +    {limitation = SOME true, ...} => ([], [])
   1.142 +  | {limitation, spec, ...} =>
   1.143        let
   1.144 -        val sfxs = mandatory_suffixes spec;
   1.145 -        val pfxs = mandatory_prefixes spec;
   1.146 +        val restrict = is_some limitation ? filter (fn [_] => false | _ => true);
   1.147 +        val sfxs = restrict (mandatory_suffixes spec);
   1.148 +        val pfxs = restrict (mandatory_prefixes spec);
   1.149        in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
   1.150  
   1.151