I am trying to follow the Isabelle 2020 documentation implementation.pdf (pp. 55). But I do not understand some ML things such as \<^binding> (in terms of what it does; it seems to be a new language outside of SML).
ML ‹
val airspeed_velocity =
Attrib.setup_config_real \<^binding>‹airspeed_velocity› (K 0.0)
›
Following the question How to show the defintion of functions in Isabelle, I did Ctrl+Click on the word "binding" in the jEdit/Isabelle PIDE, which leads me to the following definition in ml_antiquotation.ml:
value_embedded (Binding.make ("binding", ⌂))
(Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #>
However, going-to-definition seems to stop working here. I tried to get to further definitions of items such as Binding.make and Scan.lift to understand how those were defined. But Ctrl+Click on them no longer works.
I read in this SO answer that the Isabelle PIDE can serve as an ML editor.
My question is:
Is there way to let jEdit/Isabelle PIDE jump to definition of items in the ML files after the first jump from a .thy file, or in an arbitrary SML file?
