export for informative purposes;
authorwenzelm
Thu, 02 Apr 2015 20:07:05 +0200
changeset 59912 c7ba9b133bd4
parent 59909 fbf4d5ad500d
child 59913 a7f6359665c6
export for informative purposes;
src/Pure/General/name_space.ML
--- 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