irvin (Nov 05 2024 at 18:35): irvin (Nov 05 2024 at 18:35):Hi I been trying to create clickable stuff in Isabelle/ML where the stuff is in a non theory file.
I have a few other side questions. How is the clickable stuff ml stuff implemented when i hover over an ML_file implemented in isabelle.
How is ROOT.ML able to run ML_file from what i see it seems to source from external_file ROOT.ML
irvin (Nov 05 2024 at 18:39):For example, I would like to be able to do something like
theory Scratch
imports Main
keywords "include_file"
begin
include_file "file"
end
file:
clickablefilelink "filelink"
Ok i think this is done by component_jedit.scala
Fabian Huch (Nov 08 2024 at 13:55):This is many questions mixed into one.
Tools/jEdit/src/isabelle.scala).isabelle-markup in sidekick. For example, there is a specific 'URL' markup. Fabian Huch (Nov 08 2024 at 13:57):The Component_JEdit module is to pre-compile the downloadable jEdit component for Isabelle/jEdit and is unlikely to be what you want.
irvin (Nov 08 2024 at 16:48):Fabian Huch said:
This is many questions mixed into one.
- There are different modes for different languages, each defining its own syntax (have a look at
Tools/jEdit/src/isabelle.scala).- Commands can report markup (as untyped markup trees); you can inspect it by selecting
isabelle-markupin sidekick. For example, there is a specific 'URL' markup.- The IDE is responsible for making such source markup interactive.
Thanks I will have a look at it
irvin (Nov 08 2024 at 17:07):Btw my use case is for trying to get a HOL4 proof ide working in isabelle. Its basically based on the work on the Virtualization of HOL4 in Isabelle.
Fabian Huch (Nov 11 2024 at 09:39):Interesting. Make sure to have a look at the Naproche project: This is another ITP that uses Isabelle infrastructure for IDE and such.
Last updated: Dec 21 2024 at 16:20 UTC