src/Pure/General/name_space.ML
changeset 59912 c7ba9b133bd4
parent 59889 30eef3e45bd0
child 59917 9830c944670f
equal deleted inserted replaced
59909:fbf4d5ad500d 59912:c7ba9b133bd4
    30   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
    30   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
    31   val pretty: Proof.context -> T -> string -> Pretty.T
    31   val pretty: Proof.context -> T -> string -> Pretty.T
    32   val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
    32   val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
    33   val merge: T * T -> T
    33   val merge: T * T -> T
    34   type naming
    34   type naming
       
    35   val get_scopes: naming -> Binding.scope list
    35   val get_scope: naming -> Binding.scope option
    36   val get_scope: naming -> Binding.scope option
    36   val new_scope: naming -> Binding.scope * naming
    37   val new_scope: naming -> Binding.scope * naming
    37   val private: Binding.scope -> naming -> naming
    38   val private: Binding.scope -> naming -> naming
    38   val concealed: naming -> naming
    39   val concealed: naming -> naming
    39   val get_group: naming -> serial option
    40   val get_group: naming -> serial option