author | wenzelm |
Thu, 02 Apr 2015 20:07:05 +0200 | |
changeset 59912 | c7ba9b133bd4 |
parent 59909 | fbf4d5ad500d |
child 59913 | a7f6359665c6 |
--- a/src/Pure/General/name_space.ML Thu Apr 02 14:11:00 2015 +0200 +++ b/src/Pure/General/name_space.ML Thu Apr 02 20:07:05 2015 +0200 @@ -32,6 +32,7 @@ val completion: Context.generic -> T -> xstring * Position.T -> Completion.T val merge: T * T -> T type naming + val get_scopes: naming -> Binding.scope list val get_scope: naming -> Binding.scope option val new_scope: naming -> Binding.scope * naming val private: Binding.scope -> naming -> naming