Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Default sidekick parser extension

view this post on Zulip Email Gateway (Sep 21 2023 at 13:12):

From: Nicolas Meric <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users,

I'd like to extend the default sidekick parser so that it can print
another tree-view like chapter - Section - etc. for new commands
declared as document_heading keywords:

mychapter
|
-- mysection
     |
     -- mysubsection
           |
            -- etc.

In ~~/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala, the sidekick
uses Document_Structure.parse_sections:

class Isabelle_Sidekick_Default extends
  Isabelle_Sidekick_Structure("isabelle",
    PIDE.resources.theory_node_name, Document_Structure.parse_sections)

Is there a simple way to enrich the default Document_Structure with new
Items, like the Command_Item class defined in
~~/src/Pure/Isar/document_structure.scala, using for example their
heading_level method?

Or is it better to define a new sidekick parser and a new
Document_Structure?

Best regards,

Nicolas Méric

Last updated: Jan 04 2025 at 20:18 UTC