fix: Option setting in REPL
This commit is contained in:
parent
72dd20ea87
commit
adbb07af2d
|
@ -81,6 +81,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||||
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
|
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
|
||||||
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
|
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
|
||||||
printExprAST := args.printExprAST?.getD options.printExprAST,
|
printExprAST := args.printExprAST?.getD options.printExprAST,
|
||||||
|
printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
|
||||||
noRepeat := args.noRepeat?.getD options.noRepeat,
|
noRepeat := args.noRepeat?.getD options.noRepeat,
|
||||||
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
|
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
|
||||||
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
|
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
|
||||||
|
|
|
@ -82,23 +82,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
|
||||||
def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
|
def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
|
||||||
Environment.catalog ({}: Protocol.EnvCatalog)
|
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]
|
@[export pantograph_env_inspect_m]
|
||||||
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
|
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
|
||||||
Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
|
Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
|
||||||
|
|
Loading…
Reference in New Issue