src/Pure/General/name_space.ML
changeset 59887 43dc3c660f41
parent 59886 e0dc738eb08c
child 59888 27e4d0ab0948
equal deleted inserted replaced
59886:e0dc738eb08c 59887:43dc3c660f41
    46   val parent_path: naming -> naming
    46   val parent_path: naming -> naming
    47   val mandatory_path: string -> naming -> naming
    47   val mandatory_path: string -> naming -> naming
    48   val qualified_path: bool -> binding -> naming -> naming
    48   val qualified_path: bool -> binding -> naming -> naming
    49   val global_naming: naming
    49   val global_naming: naming
    50   val local_naming: naming
    50   val local_naming: naming
       
    51   val transform_naming: naming -> naming -> naming
    51   val transform_binding: naming -> binding -> binding
    52   val transform_binding: naming -> binding -> binding
    52   val full_name: naming -> binding -> string
    53   val full_name: naming -> binding -> string
    53   val base_name: binding -> string
    54   val base_name: binding -> string
    54   val hide: bool -> string -> T -> T
    55   val hide: bool -> string -> T -> T
    55   val alias: naming -> binding -> string -> T -> T
    56   val alias: naming -> binding -> string -> T -> T
   340 
   341 
   341 val global_naming = make_naming ([], NONE, false, NONE, "", []);
   342 val global_naming = make_naming ([], NONE, false, NONE, "", []);
   342 val local_naming = global_naming |> add_path Long_Name.localN;
   343 val local_naming = global_naming |> add_path Long_Name.localN;
   343 
   344 
   344 
   345 
   345 (* full name *)
   346 (* visibility flags *)
       
   347 
       
   348 fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
       
   349   fold private (the_list private') #>
       
   350   concealed' ? concealed;
   346 
   351 
   347 fun transform_binding (Naming {private, concealed, ...}) =
   352 fun transform_binding (Naming {private, concealed, ...}) =
   348   Binding.private_default private #>
   353   Binding.private_default private #>
   349   concealed ? Binding.concealed;
   354   concealed ? Binding.concealed;
       
   355 
       
   356 
       
   357 (* full name *)
   350 
   358 
   351 fun name_spec naming binding =
   359 fun name_spec naming binding =
   352   Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
   360   Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
   353 
   361 
   354 fun full_name naming =
   362 fun full_name naming =