chore: reduce namespace pollution (#14384)

This PR moves more declarations out of public namespaces which did not
belong there.

Author: TwoFX

src/Lean/Data/FuzzyMatching.lean

@@ -21,6 +21,9 @@ import Lean.Server.Completion.CompletionUtils
 public section
 
 namespace Lean
+
+open Lean
+
 namespace FuzzyMatching
 
 section Utils

src/Lean/Data/JsonRpc.lean

@@ -420,8 +420,9 @@ def MessageKind.ofMessage : Message → MessageKind
 
 end Lean.JsonRpc
 
-namespace IO.FS.Stream
+namespace Lean.IO.FS.Stream
 
+open _root_.IO
 open Lean
 open Lean.JsonRpc
 
@@ -493,4 +494,4 @@ section
     h.writeMessage e
 end
 
-end IO.FS.Stream
+end Lean.IO.FS.Stream

src/Lean/Data/Position.lean

@@ -119,5 +119,5 @@ def lineStart (map : FileMap) (line : Nat) : String.Pos.Raw :=
 end FileMap
 end Lean
 
-def String.toFileMap (s : String) : Lean.FileMap :=
+def Lean.String.toFileMap (s : String) : Lean.FileMap :=
   Lean.FileMap.ofString s

src/Lean/Elab/DocString/Builtin/Postponed.lean

@@ -13,13 +13,17 @@ set_option linter.missingDocs true
 
 public section
 
+namespace Lean
+
 /-- Enables the deferred checks recorded while elaborating Verso docstrings, such as forward
 references. -/
 register_builtin_option linter.doc.deferred : Bool := {
   defValue := true
   descr := "if true, run the deferred checks recorded while elaborating Verso docstrings"
 }
 
+end Lean
+
 namespace Lean.Doc
 open Lean Elab Term
 

src/Lean/Elab/Parallel.lean

@@ -62,7 +62,7 @@ information.
 
 public section
 
-namespace Std.Iterators.Types
+namespace Std.Iterators.Types.Internal
 
 /--
 Internal state for an iterator over tasks.
@@ -87,11 +87,11 @@ private instance {α : Type} : Iterator (TaskIterator α) BaseIO α where
           .yield ⟨{ tasks := remaining }⟩ result,
           trivial⟩
 
-end Std.Iterators.Types
+end Std.Iterators.Types.Internal
 
 namespace IO
 
-open Std Std.Iterators.Types
+open Std Std.Iterators.Types.Internal
 
 /--
 Creates an iterator over a list of tasks that yields results in completion order.

src/Lean/Elab/ParseImportsFast.lean

@@ -11,6 +11,9 @@ public import Lean.Parser.Module
 public section
 
 namespace Lean
+
+open Lean
+
 namespace ParseImports
 
 structure State where

src/Lean/Server/Completion/CompletionCollectors.lean

@@ -15,7 +15,7 @@ public import Lean.Server.RequestCancellation
 public section
 
 namespace Lean.Server.Completion
-open Elab
+open Lean Elab
 open Lean.Lsp
 open Meta
 open FuzzyMatching

src/Lean/Server/Completion/CompletionUtils.lean

@@ -10,7 +10,7 @@ public import Lean.Meta.WHNF
 
 public section
 
-partial def String.charactersIn (a b : String) : Bool :=
+partial def Lean.String.charactersIn (a b : String) : Bool :=
   goFastScalar ⟨0⟩ ⟨0⟩
 where
   /-

src/Lean/Server/Utils.lean

@@ -15,7 +15,7 @@ public import Lean.Server.InfoUtils
 
 public section
 
-open IO FS
+open Lean IO FS
 
 namespace Lean.IO
 

src/Lean/SubExpr.lean

@@ -123,18 +123,16 @@ protected def toString (p : Pos) : String :=
   |> String.intercalate "/"
   |> ("/" ++ ·)
 
-open Except in
 private def ofStringCoord : String → Except String Nat
-  | "0" => ok 0 | "1" => ok 1 | "2" => ok 2 | "3" => ok 3
-  | c => error s!"Invalid coordinate {c}"
+  | "0" => .ok 0 | "1" => .ok 1 | "2" => .ok 2 | "3" => .ok 3
+  | c => .error s!"Invalid coordinate {c}"
 
-open Except in
 protected def fromString? : String → Except String Pos
-  | "/" => Except.ok Pos.root
+  | "/" => .ok Pos.root
   | s =>
     match String.split s '/' |>.toStringList with
     | "" :: tail => Pos.ofArray <$> tail.toArray.mapM ofStringCoord
-    | ss => error s!"malformed {ss}"
+    | ss => .error s!"malformed {ss}"
 
 protected def fromString! (s : String) : Pos :=
   match Pos.fromString? s with