From adbb07af2d12d170fb097f8186be3526e8bade7b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 12 Apr 2024 22:39:47 -0700
Subject: [PATCH] fix: Option setting in REPL

---
 Pantograph.lean         |  1 +
 Pantograph/Library.lean | 17 -----------------
 2 files changed, 1 insertion(+), 17 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index f59bc11..c637303 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -81,6 +81,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
         printExprPretty := args.printExprPretty?.getD options.printExprPretty,
         printExprAST := args.printExprAST?.getD options.printExprAST,
+        printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
         noRepeat := args.noRepeat?.getD options.noRepeat,
         printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
         printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 6b8e2e2..6505fec 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -82,23 +82,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
 def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
   Environment.catalog ({}: Protocol.EnvCatalog)
 
-@[export pantograph_mk_options]
-def mkOptions
-  (printJsonPretty: Bool)
-  (printExprPretty: Bool)
-  (printExprAST: Bool)
-  (noRepeat: Bool)
-  (printAuxDecls: Bool)
-  (printImplementationDetailHyps: Bool)
-  : Protocol.Options := {
-    printJsonPretty,
-    printExprPretty,
-    printExprAST,
-    noRepeat,
-    printAuxDecls,
-    printImplementationDetailHyps,
-  }
-
 @[export pantograph_env_inspect_m]
 def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
     Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=