changeset 59912 | c7ba9b133bd4 |
parent 59889 | 30eef3e45bd0 |
child 59917 | 9830c944670f |
--- 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