Skip to content

Commit a1cb904

Browse files
fix: easier access to remote link targets (#712)
Link target insertion became more difficult to connect to remote links in the tutorials branch due to the phase separation that it introduced. This PR makes it once again easy to have remote targets, and adds them by default.
1 parent 31cf223 commit a1cb904

File tree

1 file changed

+18
-3
lines changed

1 file changed

+18
-3
lines changed

src/verso-manual/VersoManual.lean

Lines changed: 18 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ structure RenderConfig extends Config where
214214
/--
215215
How to insert links in rendered code
216216
-/
217-
linkTargets : TraverseState → LinkTargets Manual.TraverseContext := TraverseState.localTargets
217+
linkTargets : TraverseState → Multi.AllRemotes → LinkTargets Manual.TraverseContext := .localTargets ++ ·.remoteTargets)
218218

219219
namespace Config
220220

@@ -232,6 +232,21 @@ def addSearch (config : Config) : Config := { config with features := config.fea
232232

233233
end Config
234234

235+
namespace RenderConfig
236+
237+
/--
238+
Adds a bundled version of KaTeX to the document.
239+
-/
240+
@[deprecated "Set the `features` field instead (though KaTeX is enabled by default, so this is probably not needed)" (since := "2025-11-12")]
241+
def addKaTeX (config : Config) : Config := { config with features := config.features.insert .KaTeX }
242+
243+
/--
244+
Adds search dependencies to the configuration.
245+
-/
246+
@[deprecated "Set the `features` field instead (though search is enabled by default, so this is probably not needed)" (since := "2025-11-12")]
247+
def addSearch (config : Config) : Config := { config with features := config.features.insert .search }
248+
249+
end RenderConfig
235250

236251
/--
237252
Removes all parts that are specified as draft-only.
@@ -576,7 +591,7 @@ where
576591
let opts : Html.Options IO := {logError := fun msg => logError msg}
577592
let ctxt := {logError}
578593
let definitionIds := state.definitionIds ctxt
579-
let linkTargets := config.linkTargets state
594+
let linkTargets := config.linkTargets state (← read)
580595
let titleHtml ← Html.seq <$> text.title.mapM (Manual.toHtml opts.lift ctxt state definitionIds linkTargets {})
581596
let introHtml ← Html.seq <$> text.content.mapM (Manual.toHtml opts.lift ctxt state definitionIds linkTargets {})
582597
let bookToc ← text.subParts.mapM (fun p => toc 0 opts (ctxt.inPart p) state definitionIds linkTargets p)
@@ -668,7 +683,7 @@ where
668683
let opts : Html.Options IO := {logError := fun msg => logError msg}
669684
let ctxt := {logError}
670685
let definitionIds := state.definitionIds ctxt
671-
let linkTargets := config.linkTargets state
686+
let linkTargets := config.linkTargets state (← read)
672687
let toc ← text.subParts.toList.mapM fun p =>
673688
toc config.htmlDepth opts (ctxt.inPart p) state definitionIds linkTargets p
674689
let titleHtml ← Html.seq <$> text.title.mapM (Manual.toHtml opts.lift ctxt state definitionIds linkTargets {} ·)

0 commit comments

Comments
 (0)