fix: Option setting in REPL #71
|
@ -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
|
||||
|
|
|
@ -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) :=
|
||||
|
|
Loading…
Reference in New Issue