refactor: mkMapDeclarationExtension as well

Author: Kha

src/Lean/DeclarationRange.lean

@@ -15,7 +15,10 @@ namespace Lean
 
 builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {}
 builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ←
-  mkMapDeclarationExtension (exportEntriesFn := fun _ => #[])
+  mkMapDeclarationExtension (exportEntriesFn := fun _ s level =>
+    if level < .server then
+      #[]
+    else s.toArray)
 
 def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit :=
   builtinDeclRanges.modify (·.insert declName declRanges)

src/Lean/EnvExtension.lean

@@ -127,15 +127,15 @@ structure MapDeclarationExtension (α : Type) extends PersistentEnvExtension (Na
 deriving Inhabited
 
 def mkMapDeclarationExtension (name : Name := by exact decl_name%)
-    (exportEntriesFn : NameMap α → Array (Name × α) := (·.toArray)) : IO (MapDeclarationExtension α) :=
+    (exportEntriesFn : Environment → NameMap α → OLeanLevel → Array (Name × α) :=
+      fun _ s _ => s.toArray) :
+    IO (MapDeclarationExtension α) :=
   .mk <$> registerPersistentEnvExtension {
     name            := name,
     mkInitial       := pure {}
     addImportedFn   := fun _ => pure {}
     addEntryFn      := fun s (n, v) => s.insert n v
-    exportEntriesFnEx _ s
-      | .exported => exportEntriesFn s
-      | _         => s.toArray
+    exportEntriesFnEx env s level := exportEntriesFn env s level
     asyncMode       := .async
     replay?         := some fun _ newState newConsts s =>
       newConsts.foldl (init := s) fun s c =>

src/Lean/Environment.lean

@@ -1465,7 +1465,10 @@ inductive OLeanLevel where
   | server
   /-- Private module data. -/
   | «private»
-deriving DecidableEq
+deriving DecidableEq, Ord
+
+instance : LE OLeanLevel := leOfOrd
+instance : LT OLeanLevel := ltOfOrd
 
 /--
 An environment extension with support for storing/retrieving entries from a .olean file.