mkdocs.yml

site_name: KeY Documentation
site_url: https://keyproject.github.io/key-docs/

hooks:
  - hooks/approval.py
  - hooks/author.py

plugins:
  - search
  - mermaid2
  - bibtex:
      bib_file: "refs.bib"
#      cite_style: "pandoc"
#      csl_file: "springer-basic-author-date.csl"
  
markdown_extensions:
  - abbr
  - admonition
  - pymdownx.highlight
  - footnotes
  - meta
  - md_in_html
  - pymdownx.arithmatex
  - pymdownx.betterem:
      smart_enable: all
  - pymdownx.caret
  - pymdownx.critic
  - pymdownx.details
  - pymdownx.emoji:
      emoji_index: !!python/name:material.extensions.emoji.twemoji
      emoji_generator: !!python/name:material.extensions.emoji.to_svg
  - pymdownx.inlinehilite
  - pymdownx.snippets
  - pymdownx.magiclink
  - pymdownx.tabbed:
      alternate_style: true 
  - pymdownx.mark
  - pymdownx.smartsymbols
  - pymdownx.superfences:
      custom_fences:
        - name: mermaid
          class: mermaid
          format: !!python/name:pymdownx.superfences.fence_div_format
            #          format: !!python/name:pymdownx.superfences.fence_code_format
  - pymdownx.tasklist:
      custom_checkbox: true
  - pymdownx.tilde
  - attr_list
  - def_list
  - tables
  - toc:
      permalink: true

extra_javascript:
  - 'https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-MML-AM_CHTML'

theme: # material theme
  name: material
  logo: key.png
  favicon: key.png
  palette:
    - media: "(prefers-color-scheme: light)" 
      scheme: default
      primary: 'blue grey'
      accent: 'teal'
      toggle:
        icon: material/toggle-switch-off-outline
        name: Switch to dark mode
    - media: "(prefers-color-scheme: dark)" 
      scheme: slate
      primary: 'dark'
      accent: 'orange'
      toggle:
        icon: material/toggle-switch
        name: Switch to light mode
  features:
    - navigation.tabs
    - navigation.sections
    - navigation.expand
    - navigation.indexes
    - navigation.top
    - content.code.annotate
    - content.tabs.link

  icon:
    repo: fontawesome/brands/github

nav:
  - Home: index.md
  - User Guide:
      - "Welcome": user/index.md
      - "1. Getting Started":
          - "The Quicktour": quicktour/index.md
          - "Installation": quicktour/install.md
          - "Loading JML Contracts": quicktour/loading.md
          - "Proving JML Contracts": quicktour/proving.md
          - "Appendix: Tips and Background": quicktour/appendix.md
      - "2. Working with the Prover":
          - "Overview": user/UiFeatures/index.md
          - "The Taclet Match Dialog": user/TacletMatchDialog/index.md
          - "Excluding Goals from Automation": user/Interactive.md
          - "Proof Exploration": user/Exploration.md
          - "Comparing Proof Nodes": user/NodeDiff.md
          - "Linearized Proof Tree": user/ProofTreeLinearMode.md
          - "Proof Caching": user/ProofCaching/index.md
          - "Proof Slicing": user/ProofSlicing/index.md
      - "3. Structuring Verification Projects":
          - "The Classpath Directive": user/Classpath.md
          - "Programs with Generics": user/RemoveGenerics.md
          - "User-Defined Data Types": user/ADTs.md
          - "JavaDL Escapes in JML": user/JavaDLinJML.md
      - "4. Proof Scripts":
          - "Overview": user/ProofScripts/index.md
          - "Language Constructs": user/ProofScripts/language.md
          - "Command Reference": user/ProofScripts/commands.md
          - "Script Variables": user/ProofScripts/variables.md
          - "Macros": user/ProofScripts/macros.md
          - "Linear Proof Scripts": user/ProofScripts/linearScripts.md
          - "Proof Scripts in JML": user/ProofScripts/jml.md
          - "Historical Notes (2015)": user/ProofScripts/original.md
      - "5. SMT Solvers":
          - "Adding SMT Solvers": user/SMT/AddingSMTSolvers.md
      - "6. Bridges to Other Tools":
          - "Isabelle Translation": user/IsabelleTranslation/index.md
          # - "LLM Support": user/LLM/index.md  # empty skeleton page, re-add when written
      - "7. Language Reference":
          - "JML Grammar": user/JMLGrammar.md
          - "The KeY Language": user/KeyGrammar.md
          - "KeY's Java Extensions": user/JavaGrammar.md
      - "8. FAQ": user/FAQ.md
      - "Release Notes": changelog.md

  - Developer Guide:
      - "Welcome": devel/index.md
      - "1. Architecture": devel/Architecture.md
      - "2. Building KeY": devel/Gradle.md
      - "3. Working on the Code":
          - "Coding Conventions": devel/CodingConventions.md
          - "Formatting with Spotless": devel/SpotlessAutomaticFormatting.md
          - "Logging": devel/Logging.md
      - "4. Extending KeY":
          - "Overview": devel/ExtendingKeY.md
          - "How-Tos (verified recipes)":
              - "Overview": devel/howto/index.md
              - "Add an Extension Module": devel/howto/AddExtension.md
              - "Add a Menu Entry": devel/howto/AddMenuEntry.md
              - "Add a Toolbar": devel/howto/AddToolbarAction.md
              - "Add Taclets": devel/howto/AddTaclets.md
              - "Add a Proof Macro": devel/howto/AddProofMacro.md
              - "Add a Script Command": devel/howto/AddScriptCommand.md
              - "Add a Term Label": devel/howto/AddTermLabel.md
          - "Writing Taclets": devel/HowToTaclet.md
          - "Polarity Triggers for Rewrite Taclets": user/Polarity.md
          - "GUI Extension Points": devel/GUIExtensions.md
          - "Script Commands in Depth": devel/ScriptCommands.md
          - "Adding SMT Solvers": devel/AddingSMTSolvers.md
          - "Event Listeners": devel/Listeners.md
      - "5. Using KeY as a Library":
          - "KeY in External Projects": devel/ExternalProject.md
          - "JSON-RPC Interface": devel/rpc/index.md
      - "6. Internals":
          - "Proof search":
              - "The Rule Application Pipeline": devel/RuleApplicationPipeline.md
              - "Strategy Costs and the Cost-Band Ladder": devel/StrategyCosts.md
              - "Multi-Core Proving": devel/Multithreading.md
          - "Terms and parsing":
              - "The KeY Parser": devel/NewKeyParser.md
              - "Term Labels": devel/TermLabels.md
          - "Proofs and external solvers":
              - "Proof Loading and Saving": devel/ProofLoadSave.md
              - "SMT Translation": devel/SMTTranslation.md
              - "Counterexample Generation": devel/CounterExampleGeneration.md
          - "Legacy":
              - "Extending Recoder (obsolete)": devel/How2ExtRecoder.md
      - "7. Testing":
          - "Overview": devel/Testing/index.md
          - "Proved Rules": devel/Testing/ProveRules.md
          - "RunAllProofs": devel/Testing/RunAllProves.md
          - "Deterministic Test Order (outdated)": devel/Testing/deterministicTestOrder.md
          - "Parser Message Tests": devel/Testing/parserMessageTest.md
          - "CI Infrastructure": devel/Testing/TestingInfrastructure.md
      - "8. Writing Documentation": devel/howtodoc/index.md
      - "9. Appendices":
          - "Strategy Cost Tables": devel/StrategyCostTables.md

  - Historical:
      - Eclipse plugins (unsupported):
          - "Overview": eclipse/index.md
          - "KeY basics": eclipse/CrossProject/index.md
          - "SED": eclipse/SED/index.md
          - "Stubby": eclipse/Stubby/index.md
          - "KeY IDE": eclipse/KeYIDE/index.md
          - "MonKeY": eclipse/MonKeY/index.md
          - "Starter": eclipse/Starter/index.md
          - "VisualDBC": eclipse/VisualDbC/index.md
          - "JML Editing": eclipse/JMLEditing/index.md
          - "Resources" : eclipse/KeYResources/index.md

  - KeY Enhancement Proposals:
      - "About KEPs": keps/index.md
      - "KEP-1: Taclet-Generating Transformers": keps/kep-0001-taclet-generating-transformers/index.md

extra_css:
  - extra.css

  
#  nav_style: dark
#  logo: 'https://git.key-project.org/uploads/-/system/appearance/logo/1/key-color.png'
  #feature:
  #  tabs: true
repo_name: key-docs
repo_url: https://github.com/KeYProject/key-docs/
edit_uri: edit/master/docs/