diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 41fc7a08cf5b6b73c9271d8f3f4d2eead9af2418..46a17d9e1422e7e5d1569cf3da7cf30b5291bd8f 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -965,7 +965,7 @@ let () = Information.register ~title:"Property Consolidated Status" begin fun fmt loc -> match loc with - | PIP prop -> + | PIP prop when Property.has_status prop -> Property_status.Feedback.pretty fmt @@ Property_status.Feedback.get prop | _ -> raise Not_found diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml index 78c179100d96b421ab445e4db6b558164252f1c9..57d3d0305f4bfaa0aaf686adb88ccdae1f3d18ba 100644 --- a/src/plugins/server/kernel_properties.ml +++ b/src/plugins/server/kernel_properties.ml @@ -268,7 +268,13 @@ let () = States.column model ~name:"names" let () = States.column model ~name:"status" ~descr:(Md.plain "Status") ~data:(module PropStatus) - ~get:(Property_status.Feedback.get) + ~get: + begin fun ip -> + if Property.has_status ip + then Property_status.Feedback.get ip + else Property_status.Feedback.Never_tried + end + let () = States.option model ~name:"scope" ~descr:(Md.plain "Declaration Scope")