Stream: Isabelle/ML

Topic: Functions Retrieving and Printing Proof State

Jonathan Julian Huerta y Munive (Nov 10 2023 at 13:18):

Hello, could anybody point me to the Isabelle/ML and Isabelle/Scala functions used by the State panel in jEdit to show outputs such as the one below?:

proof (prove)
goal (1 subgoal):
 1. xs ≠ [] ⟹ head xs = hd xs

Fabian Huch (Nov 10 2023 at 13:22):

This is Isabelle/Scala (not /ML) - have a look at Tools/jEdit/src/state_dockable.scala, the print_state function should populate the panel.

Jonathan Julian Huerta y Munive (Nov 10 2023 at 13:22):

Thanks @Fabian Huch!

Lukas Stevens (Nov 10 2023 at 13:22):

But to generate the output I think Proof_Display.print_results is used.

Jonathan Julian Huerta y Munive (Nov 14 2023 at 16:27):

@Lukas Stevens how do you know that the Query_Operation called print_state calls Proof_Display.print_results?

Lukas Stevens (Nov 14 2023 at 16:34):

If you look at the implementation of e.g. lemma, then you see that it uses Proof_Display.print_results. This tells me that this function is used to generate the string that is then displayed by the state panel.

Last updated: May 04 2024 at 12:26 UTC