feat!: Display public name only if name is private

This commit is contained in:
Leni Aniva 2023-12-05 20:20:08 -08:00
parent cdb1e8576f
commit dbfee00420
3 changed files with 5 additions and 4 deletions

View File

@ -85,7 +85,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok {
type := ← serialize_expression state.options info.type,
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,
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
module? := module?

View File

@ -120,7 +120,8 @@ structure LibInspectResult where
type: Expression
value?: Option Expression := .none
module?: Option String
isPrivate: Bool
-- If the name is private, displays the public facing name
publicName?: Option String := .none
typeDependency?: Option (Array String) := .none
valueDependency?: Option (Array String) := .none
deriving Lean.ToJson

View File

@ -52,7 +52,7 @@ def test_option_modify : IO LSpec.TestSeq :=
subroutine_step "lib.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp? }, module?, isPrivate := false }:
type := { pp? }, module? }:
Protocol.LibInspectResult)),
subroutine_step "options.set"
[("printExprAST", .bool true)]
@ -61,7 +61,7 @@ def test_option_modify : IO LSpec.TestSeq :=
subroutine_step "lib.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp?, sexp? }, module?, isPrivate := false }:
type := { pp?, sexp? }, module? }:
Protocol.LibInspectResult)),
subroutine_step "options.print"
[]