feat!: Display public name only if name is private
This commit is contained in:
parent
9f2b07757f
commit
da74258dd1
|
@ -85,7 +85,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||||
return .ok {
|
return .ok {
|
||||||
type := ← serialize_expression state.options info.type,
|
type := ← serialize_expression state.options info.type,
|
||||||
value? := ← value?.mapM (λ v => serialize_expression state.options v),
|
value? := ← value?.mapM (λ v => serialize_expression state.options v),
|
||||||
isPrivate := Lean.isPrivateName name,
|
publicName? := Lean.privateToUserName? name |>.map (·.toString),
|
||||||
typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
|
typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
|
||||||
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
|
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
|
||||||
module? := module?
|
module? := module?
|
||||||
|
|
|
@ -120,7 +120,8 @@ structure LibInspectResult where
|
||||||
type: Expression
|
type: Expression
|
||||||
value?: Option Expression := .none
|
value?: Option Expression := .none
|
||||||
module?: Option String
|
module?: Option String
|
||||||
isPrivate: Bool
|
-- If the name is private, displays the public facing name
|
||||||
|
publicName?: Option String := .none
|
||||||
typeDependency?: Option (Array String) := .none
|
typeDependency?: Option (Array String) := .none
|
||||||
valueDependency?: Option (Array String) := .none
|
valueDependency?: Option (Array String) := .none
|
||||||
deriving Lean.ToJson
|
deriving Lean.ToJson
|
||||||
|
|
|
@ -52,7 +52,7 @@ def test_option_modify : IO LSpec.TestSeq :=
|
||||||
subroutine_step "lib.inspect"
|
subroutine_step "lib.inspect"
|
||||||
[("name", .str "Nat.add_one")]
|
[("name", .str "Nat.add_one")]
|
||||||
(Lean.toJson ({
|
(Lean.toJson ({
|
||||||
type := { pp? }, module?, isPrivate := false }:
|
type := { pp? }, module? }:
|
||||||
Protocol.LibInspectResult)),
|
Protocol.LibInspectResult)),
|
||||||
subroutine_step "options.set"
|
subroutine_step "options.set"
|
||||||
[("printExprAST", .bool true)]
|
[("printExprAST", .bool true)]
|
||||||
|
@ -61,7 +61,7 @@ def test_option_modify : IO LSpec.TestSeq :=
|
||||||
subroutine_step "lib.inspect"
|
subroutine_step "lib.inspect"
|
||||||
[("name", .str "Nat.add_one")]
|
[("name", .str "Nat.add_one")]
|
||||||
(Lean.toJson ({
|
(Lean.toJson ({
|
||||||
type := { pp?, sexp? }, module?, isPrivate := false }:
|
type := { pp?, sexp? }, module? }:
|
||||||
Protocol.LibInspectResult)),
|
Protocol.LibInspectResult)),
|
||||||
subroutine_step "options.print"
|
subroutine_step "options.print"
|
||||||
[]
|
[]
|
||||||
|
|
Loading…
Reference in New Issue