chore: elaborate open scoped

src/Lean/Elab/Open.lean

@@ -39,6 +39,11 @@ private def elabOpenSimple (n : Syntax) : M (m:=m) Unit :=
     addOpenDecl (OpenDecl.simple ns [])
     activateScoped ns
 
+private def elabOpenScoped (n : Syntax) : M (m:=m) Unit :=
+  -- `open` `scoped` id+
+  for ns in n[1].getArgs do
+    activateScoped (← resolveNamespace ns.getId)
+
 -- `open` id `(` id+ `)`
 private def elabOpenOnly (n : Syntax) : M (m:=m) Unit := do
   let ns ← resolveNamespace n[0].getId
@@ -69,6 +74,8 @@ def elabOpenDecl [MonadResolveName m] (openDeclStx : Syntax) : m (List OpenDecl)
   StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
     if openDeclStx.getKind == ``Parser.Command.openSimple then
       elabOpenSimple openDeclStx
+    else if openDeclStx.getKind == ``Parser.Command.openScoped then
+      elabOpenScoped openDeclStx
     else if openDeclStx.getKind == ``Parser.Command.openOnly then
       elabOpenOnly openDeclStx
     else if openDeclStx.getKind == ``Parser.Command.openHiding then

tests/lean/openScoped.lean

@@ -0,0 +1,25 @@
+#check @epsilon -- Error
+
+noncomputable def foo1 (f g : Nat → Nat) : Nat :=
+  if f = g then 1 else 2 -- Error
+
+section
+open Classical
+
+#check @epsilon
+
+noncomputable def foo2 (f g : Nat → Nat) : Nat :=
+  if f = g then 1 else 2 -- Ok
+end
+
+#check @epsilon -- Error
+
+section
+
+open scoped Classical
+#check @epsilon -- Error
+
+noncomputable def foo3 (f g : Nat → Nat) : Nat :=
+  if f = g then 1 else 2 -- Ok
+
+end

tests/lean/openScoped.lean.expected.out

@@ -0,0 +1,6 @@
+openScoped.lean:1:8-1:15: error: unknown identifier 'epsilon'
+openScoped.lean:4:2-4:24: error: failed to synthesize instance
+  Decidable (f = g)
+epsilon : {α : Sort u_1} → [h : Nonempty α] → (α → Prop) → α
+openScoped.lean:15:8-15:15: error: unknown identifier 'epsilon'
+openScoped.lean:20:8-20:15: error: unknown identifier 'epsilon'