src/Pure/General/name_space.ML
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