# HG changeset patch
# User wenzelm
# Date 1427998025 -7200
# Node ID c7ba9b133bd48ede9c0c83c20975361ceb90cfca
# Parent  fbf4d5ad500d2ab735f441f9315ba8f130a923ab
export for informative purposes;

diff -r fbf4d5ad500d -r c7ba9b133bd4 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