src/Pure/General/name_space.ML
changeset 35200 aaddb2b526d6
parent 33724 5ee13e0428d2
child 35432 b8863ee98f56
equal deleted inserted replaced
35199:2e37cdae7b9c 35200:aaddb2b526d6
    41   val reset_group: naming -> naming
    41   val reset_group: naming -> naming
    42   val add_path: string -> naming -> naming
    42   val add_path: string -> naming -> naming
    43   val root_path: naming -> naming
    43   val root_path: naming -> naming
    44   val parent_path: naming -> naming
    44   val parent_path: naming -> naming
    45   val mandatory_path: string -> naming -> naming
    45   val mandatory_path: string -> naming -> naming
       
    46   val qualified_path: bool -> binding -> naming -> naming
    46   val transform_binding: naming -> binding -> binding
    47   val transform_binding: naming -> binding -> binding
    47   val full_name: naming -> binding -> string
    48   val full_name: naming -> binding -> string
    48   val external_names: naming -> string -> string list
    49   val external_names: naming -> string -> string list
    49   val declare: bool -> naming -> binding -> T -> string * T
    50   val declare: bool -> naming -> binding -> T -> string * T
    50   type 'a table = T * 'a Symtab.table
    51   type 'a table = T * 'a Symtab.table
   259 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
   260 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
   260 val root_path = map_path (fn _ => []);
   261 val root_path = map_path (fn _ => []);
   261 val parent_path = map_path (perhaps (try (#1 o split_last)));
   262 val parent_path = map_path (perhaps (try (#1 o split_last)));
   262 fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
   263 fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
   263 
   264 
       
   265 fun qualified_path mandatory binding = map_path (fn path =>
       
   266   path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
       
   267 
   264 
   268 
   265 (* full name *)
   269 (* full name *)
   266 
   270 
   267 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
   271 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
   268   | transform_binding _ = I;
   272   | transform_binding _ = I;