From 6ec31f029ecd6c629d3be532437897d1ffeb01a8 Mon Sep 17 00:00:00 2001 From: hallgren Date: Thu, 1 Jun 2017 18:21:52 +0000 Subject: [PATCH] Add a Quick Links menu to the Libary Synopsis web page. The menu is generated dynamically by JavaScript functions defined in quicklinks.js, by traversing the Detailed Table of Contents in the generated synopsis.html. --- lib/doc/MkSynopsis.hs | 4 ++ lib/doc/quicklinks.js | 109 ++++++++++++++++++++++++++++++++++++++++ lib/doc/revealpopup.css | 27 +++++++++- 3 files changed, 139 insertions(+), 1 deletion(-) create mode 100644 lib/doc/quicklinks.js diff --git a/lib/doc/MkSynopsis.hs b/lib/doc/MkSynopsis.hs index 4628df7ba..13c52c0ac 100644 --- a/lib/doc/MkSynopsis.hs +++ b/lib/doc/MkSynopsis.hs @@ -45,6 +45,8 @@ main = do append "%!postproc(html): '(SRC=\"categories.png\")' '\\1 USEMAP=\"#categories\"'" append "%!postproc(html): '#LParadigms' ''" append "%!postproc(tex): '#LParadigms' ''" + append "%!postproc(html): '#quicklinks' ''" + append "%!postproc(tex): '#quicklinks' ''" delimit $ addToolTips cs include "synopsis-intro.txt" title "Categories" @@ -95,6 +97,8 @@ main = do space append "%%toc" space + append "#quicklinks" + space let format = if isLatex then "tex" else "html" system $ "txt2tags -t" ++ format ++ " " ++ " --toc " ++ synopsis if isLatex then (system $ "pdflatex synopsis.tex") >> return () else return () diff --git a/lib/doc/quicklinks.js b/lib/doc/quicklinks.js new file mode 100644 index 000000000..4bb41d437 --- /dev/null +++ b/lib/doc/quicklinks.js @@ -0,0 +1,109 @@ + +// Find an element with a certain tag containing a certain text. +function findElement(tagname,text) { + var els=document.body.getElementsByTagName(tagname) + for(var i=0;i div.expand { display: block; } @@ -24,3 +24,28 @@ table { border-collapse: collapse; } td, th { padding: 5px; } th { background: #9df; } td { background: white } + +/* Quick links */ + +/* To prevent Quick links from overlapping page header: */ +h1 { margin-right: 2.5em; } + +div.quicklinks { + position: fixed; + top:0; right:0; + max-height: 97%; + overflow: scroll; + background-color: rgba(255,255,192,0.9); + font-family: sans-serif; + box-shadow: 4px 4px 12px rgba(0,0,0,0.33); + padding: 5px; +} + +table.quicklinks th, td.quicklinks { + border: 1px solid black; + vertical-align: top; + font-size: 90%; + line-height: 130%; +} +div.quicklinks a { display: block; } +