Pantograph/Frontend/Basic.lean

@@ -40,7 +40,6 @@ def stxByteRange (stx : Syntax) : String.Pos × String.Pos :=
 abbrev FrontendM := Elab.Frontend.FrontendM
 
 structure CompilationStep where
-  scope : Elab.Command.Scope
   fileName : String
   fileMap : FileMap
   src : Substring
@@ -75,7 +74,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let msgs := s'.messages.toList.drop s.messages.toList.length
   let trees := s'.infoState.trees.drop s.infoState.trees.size
   let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
-  return ({ scope := s.scopes.head!, fileName, fileMap, src, stx, before, after, msgs, trees }, done)
+  return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
 
 partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
   let (cmd, done) ← processOneCommand

Pantograph/Protocol.lean

@@ -346,11 +346,6 @@ structure FrontendProcess where
   -- One of these two must be supplied: Either supply the file name or the content.
   fileName?: Option String := .none
   file?: Option String := .none
-  -- If set to true, read the header (otherwise discards the header)
-  readHeader : Bool := false
-  -- If set to true, Pantograph's environment will be altered to whatever is
-  -- after the compilation units.
-  inheritEnv : Bool := false
   -- collect tactic invocations
   invocations: Bool := false
   -- collect `sorry`s

Repl.lean

@@ -53,10 +53,11 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
     | .none, .some file =>
       pure ("<anonymous>", file)
     | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
-  let env?: Option Environment ← if args.readHeader then
+  let env?: Option Environment ← if args.fileName?.isSome then
       pure .none
     else do
-      .some <$> getEnv
+      let env ← getEnv
+      pure <| .some env
   let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
   let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
     Frontend.mapCompilationSteps λ step => do
@@ -82,9 +83,7 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
       messages,
       newConstants
     }
-  let (li, state') ← frontendM.run context |>.run state
+  let li ← frontendM.run context |>.run' state
-  if args.inheritEnv then
-    setEnv state'.commandState.env
   let units ← li.mapM λ step => withEnv step.env do
     let newConstants? := if args.newConstants then
         .some $ step.newConstants.toArray.map λ name => name.toString
@@ -142,7 +141,7 @@ def execute (command: Protocol.Command): MainM Json := do
     | "goal.print"    => run goal_print
     | "goal.save"     => run goal_save
     | "goal.load"     => run goal_load
-    | "frontend.process" => run frontend_process
+    | "frontend.process"  => run frontend_process
     | cmd =>
       let error: Protocol.InteractionError :=
         errorCommand s!"Unknown command {cmd}"

Test/Frontend.lean

@@ -1,28 +1,11 @@
+import LSpec
 import Pantograph
 import Repl
 import Test.Common
 
-import LSpec
-
 open Lean Pantograph
 namespace Pantograph.Test.Frontend
 
-def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) : MetaM (List α) := do
-  let filename := "<anonymous>"
-  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
-  let m := Frontend.mapCompilationSteps f
-  m.run context |>.run' state
-
-def test_open : TestT MetaM Unit := do
-  let sketch := "
-open Nat
-example : ∀ (n : Nat), n + 1 = Nat.succ n := by
-  intro
-  apply add_one
-  "
-  let errors ← runFrontend sketch λ step => step.msgs.mapM (·.toString)
-  checkEq "errors" errors [[], []]
-
 def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
     : MetaM (List GoalState) := do
   let filename := "<anonymous>"
@@ -250,7 +233,6 @@ theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
-    ("open", test_open),
     ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
     ("sorry_in_middle", test_sorry_in_middle),
     ("sorry_in_induction", test_sorry_in_induction),

Test/Integration.lean

@@ -173,8 +173,6 @@ def test_frontend_process : Test :=
       [
         ("file",              .str file),
         ("invocations",       .bool true),
-        ("readHeader",        .bool false),
-        ("inheritEnv",        .bool false),
         ("sorrys",            .bool false),
         ("typeErrorsAsGoals", .bool false),
         ("newConstants",      .bool false),
@@ -216,8 +214,6 @@ def test_frontend_process_sorry : Test :=
     step "frontend.process"
       [
         ("file", .str file),
-        ("readHeader",        .bool false),
-        ("inheritEnv",        .bool false),
         ("invocations", .bool false),
         ("sorrys", .bool true),
         ("typeErrorsAsGoals", .bool false),