Pantograph.lean

@@ -1,7 +1,6 @@
 import Pantograph.Goal
 import Pantograph.Protocol
 import Pantograph.Serial
-import Pantograph.Symbol
 import Pantograph.Environment
 import Lean.Data.HashMap
 

Pantograph/Environment.lean

@@ -1,5 +1,4 @@
 import Pantograph.Protocol
-import Pantograph.Symbol
 import Pantograph.Serial
 import Lean
 
@@ -10,6 +9,29 @@ namespace Pantograph.Environment
 
 abbrev CR α := Except Protocol.InteractionError α
 
+def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
+  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe
+  where
+  isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
+    | .str _ name => name == "Lean"
+    | _ => true
+
+def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+  let pref := match info with
+  | .axiomInfo  _ => "a"
+  | .defnInfo   _ => "d"
+  | .thmInfo    _ => "t"
+  | .opaqueInfo _ => "o"
+  | .quotInfo   _ => "q"
+  | .inductInfo _ => "i"
+  | .ctorInfo   _ => "c"
+  | .recInfo    _ => "r"
+  s!"{pref}{toString n}"
+
+def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
+  if is_symbol_unsafe_or_internal n info
+  then Option.none
+  else Option.some <| to_compact_symbol_name n info
 def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := do
   let env ← Lean.MonadEnv.getEnv
   let names := env.constants.fold (init := #[]) (λ acc name info =>

Pantograph/Goal.lean

@@ -1,7 +1,5 @@
 import Lean
 
-import Pantograph.Symbol
-
 def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
   {
     msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false

Pantograph/Symbol.lean

@@ -1,29 +0,0 @@
-import Lean
-
-namespace Pantograph
-
-def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
-  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe
-  where
-  isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
-    | .str _ name => name == "Lean"
-    | _ => true
-
-def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
-  let pref := match info with
-  | .axiomInfo  _ => "a"
-  | .defnInfo   _ => "d"
-  | .thmInfo    _ => "t"
-  | .opaqueInfo _ => "o"
-  | .quotInfo   _ => "q"
-  | .inductInfo _ => "i"
-  | .ctorInfo   _ => "c"
-  | .recInfo    _ => "r"
-  s!"{pref}{toString n}"
-
-def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
-  if is_symbol_unsafe_or_internal n info
-  then Option.none
-  else Option.some <| to_compact_symbol_name n info
-
-end Pantograph

Test/Catalog.lean

@@ -1,6 +1,6 @@
 import LSpec
 import Pantograph.Serial
-import Pantograph.Symbol
+import Pantograph.Environment
 
 namespace Pantograph.Test.Catalog
 
@@ -14,7 +14,7 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
   ]
   let suite := entries.foldl (λ suites (symbol, target) =>
     let constant := env.constants.find! symbol
-    let test := LSpec.check symbol.toString ((is_symbol_unsafe_or_internal symbol constant) == target)
+    let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target)
     LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   return suite
 

Test/Serial.lean

@@ -1,6 +1,5 @@
 import LSpec
 import Pantograph.Serial
-import Pantograph.Symbol
 
 namespace Pantograph.Test.Serial