0 | ||| Functions for generating
  1 | module Katla.HTML
  2 |
  3 | import Core.Metadata
  4 | import Data.String
  5 | import System.File
  6 |
  7 | import Collie
  8 | import Katla.Config
  9 |
 10 | import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML as Lib
 11 |
 12 | export
 13 | escapeHTML : Config -> Char -> List Char
 14 | escapeHTML config ' ' = unpack config.space
 15 | escapeHTML config c = unpack (htmlEscape $ cast c)
 16 |
 17 | export
 18 | annotate : Maybe Decoration -> String -> String
 19 | annotate Nothing    s = s
 20 | annotate (Just dec) s = apply (convert dec) s
 21 |   where
 22 |
 23 |     apply : String -> String -> String
 24 |     apply f a = #"<span class="\#{f}">\#{a}</span>"#
 25 |
 26 | -- /!\ Do not introduce additional empty lines as that would probably
 27 | --     break the markdown backend!
 28 | export
 29 | styleElement : Decoration -> Category -> String
 30 | styleElement dec cat = concat $ intersperse "\n" $ catMaybes
 31 |   [ pure ("." ++ convert dec ++ " {")
 32 |   , ("  \{cat .style}") <$ guard (cat .style /= "")
 33 |   , ("  color: \{cat .colour}") <$ guard (cat .colour /= "")
 34 |   , pure "}"
 35 |   ]
 36 |
 37 | export
 38 | styleHeader : Config -> String
 39 | styleHeader cfg =  """
 40 |     \{styleElement Data cfg.datacons}
 41 |     \{styleElement Typ cfg.typecons}
 42 |     \{styleElement Bound cfg.bound}
 43 |     \{styleElement Function cfg.function}
 44 |     \{styleElement Keyword cfg.keyword}
 45 |     \{styleElement Comment cfg.comment}
 46 |     \{styleElement Namespace cfg.namespce}
 47 |     \{styleElement Postulate cfg.postulte}
 48 |     \{styleElement Module cfg.aModule}
 49 |     """
 50 |
 51 | export
 52 | standalonePre : Config -> String
 53 | standalonePre config = """
 54 |   <!DOCTYPE html><html lang="en">
 55 |
 56 |   <head>
 57 |     <meta charset="utf-8">
 58 |     <style>
 59 |     \{styleHeader config}
 60 |
 61 |     .IdrisLineNumber {
 62 |       text-decoration: none;
 63 |       color: lightgrey;
 64 |       user-select: none;
 65 |     }
 66 |     .IdrisLineNumber:hover {
 67 |       color: darkgray;
 68 |     }
 69 |     .IdrisLineNumber:target {
 70 |       color: gray;
 71 |     }
 72 |     .IdrisHighlight {
 73 |       background-color: yellow;
 74 |     }
 75 |     </style>
 76 |     <script>
 77 |       function initialize() {
 78 |         function handleHash(ev) {
 79 |             if (!location.hash) return
 80 |             let m = location.hash.match(/#(line\\d+)(?:-(line\\d+))?/)
 81 |             if (m) {
 82 |                 let start = document.getElementById(m[1])
 83 |                 let end = document.getElementById(m[2])
 84 |                 if (start) {
 85 |                     if (end && end.compareDocumentPosition(start) === 4) {
 86 |                         ([start, end] = [end, start])
 87 |                     }
 88 |                     // Only on page load
 89 |                     if (!ev) start.scrollIntoView()
 90 |                     let parent = start.parentElement
 91 |                     let lines = parent.children
 92 |                     let className = ''
 93 |                     for (let n = 0; n < lines.length; n++) {
 94 |                         let el = lines[n]
 95 |                         if (el === start) className = 'IdrisHighlight'
 96 |                         el.className = className
 97 |                         if (el === end || className && !end) className = ''
 98 |                     }
 99 |                 }
100 |             }
101 |         }
102 |         let startLine
103 |         let endLine
104 |         function handlePointerMove(ev) {
105 |             if (startLine) {
106 |                 for (let el = document.elementFromPoint(ev.clientX, ev.clientY); el; el = el.parentElement) {
107 |                     if (el.parentElement === startLine.parentElement) {
108 |                         if (endLine !== el) {
109 |                             endLine = el
110 |                             update()
111 |                         }
112 |                         break
113 |                     }
114 |                 }
115 |             }
116 |         }
117 |         function update(ev) {
118 |             window.location.hash = startLine === endLine ? startLine.id : startLine.id + '-' + endLine.id
119 |         }
120 |         function handlePointerDown(ev) {
121 |             let target = ev.target
122 |             if (target.className === 'IdrisLineNumber') {
123 |                 startLine = endLine = target.parentElement
124 |                 window.addEventListener('pointermove', handlePointerMove)
125 |                 update()
126 |                 ev.preventDefault()
127 |             }
128 |         }
129 |         function handlePointerUp(ev) {
130 |             if (startLine) {
131 |                 update()
132 |                 window.removeEventListener('pointermove', handlePointerMove)
133 |                 startLine = endLine = null
134 |             }
135 |         }
136 |         window.addEventListener('hashchange', handleHash)
137 |         window.addEventListener('pointerdown', handlePointerDown)
138 |         window.addEventListener('pointerup', handlePointerUp)
139 |         handleHash()
140 |     }
141 |     </script>
142 |   </head>
143 |   <body onload="initialize()">
144 |   <code class="IdrisCode">
145 |   """
146 |
147 | export
148 | standalonePost : String
149 | standalonePost = """
150 |   </code>
151 |   </body>
152 |   </html>
153 |   """
154 |
155 | export
156 | makeMacroPre : String -> String
157 | makeMacroPre name = """
158 |   <code class="IdrisCode">
159 |   """
160 |
161 | export
162 | makeMacroPost : String
163 | makeMacroPost = """
164 |   </code>
165 |   """
166 |
167 | export
168 | makeInlineMacroPre : String -> String
169 | makeInlineMacroPre name = """
170 |   <code class="IdrisCode">
171 |   """
172 |
173 | export
174 | makeInlineMacroPost : String
175 | makeInlineMacroPost = """
176 |   </code>
177 |   """
178 |
179 | export
180 | mkDriver : Config -> Driver
181 | mkDriver config = MkDriver
182 |   (\ wdth, ln =>
183 |     let ln = show ln
184 |         lineID = "line\{ln}"
185 |         desc = concat (List.replicate (minus wdth (length ln)) "&nbsp;" ++ [ln]) in
186 |     ##"<div id="\##{lineID}"><a href="#\##{lineID}" class="IdrisLineNumber"> \##{desc} | </a>"##
187 |   , "</div>")
188 |   (escapeHTML config)
189 |   annotate
190 |   (standalonePre config, standalonePost)
191 |   (makeInlineMacroPre, makeInlineMacroPost)
192 |   (makeMacroPre, makeMacroPost)
193 |
194 | public export
195 | initHTMLCmd : Command "init"
196 | initHTMLCmd = MkCommand
197 |   { description = "Generate default configuration file"
198 |   , subcommands = []
199 |   , modifiers = []
200 |   , arguments = filePath
201 |   }
202 |
203 | export
204 | init : (ParsedCommand _ HTML.initHTMLCmd) -> IO ()
205 | init parsed = initExec HTML parsed.arguments
206 |