1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
|
{-# LANGUAGE OverloadedStrings #-}
module Test.Unit.Html (unitTests) where
import Base
import Api qualified
import Felix.Parse qualified as Parse
import Felix.Source
import Felix.Source.Graph
import Render.Html qualified as Html
import Render.Html.Context
import Render.Html.Layout
import Report.Location (Location, pattern Nowhere)
import Syntax.Abstract
import Data.Text qualified as Text
import Data.Text.IO qualified as TextIO
import Data.List.NonEmpty qualified as NonEmpty
import System.Directory qualified as Directory
import Test.Tasty
import Test.Tasty.HUnit
unitTests :: TestTree
unitTests = testGroup "HTML renderer"
[ testCase "one shared index resolves local and cross-page previews" referencePreviews
, testCase "missing reference preview data falls back to readable text" missingReferenceFallback
, testCase "datatype rendering omits unchecked derived facts" datatypeDerivedFactsAreOmitted
]
referencePreviews :: Assertion
referencePreviews = do
graph <-
expectRight =<<
Api.prepareDefaultSourceGraph
"test/html-fixtures/root-preview.tex"
workspace <-
expectRight =<< Parse.parseResolvedSourceGraph graph
hints <- TextIO.readFile "library/lexicon.tsv"
layout <-
expectRight
(layoutHtmlSourceGraph
Api.defaultHtmlMountPrefixes
graph)
let nodes = Parse.parsedWorkspaceImportedBeforeImporter workspace
sourceBlocks =
(\node ->
( Parse.parsedModuleResolved node
, Parse.parsedModuleBlocks node
))
<$> nodes
(renderIndex, pages) =
Html.buildRenderIndex sourceBlocks
rootPage = NonEmpty.last pages
context <-
expectRight
(htmlRenderContext
layout
(Html.htmlPagePresentationSource rootPage))
html <-
expectRight
(Html.renderDocument
context
hints
renderIndex
rootPage)
let supportScript = Html.supportScriptAssetContents
assertContains "local references keep page anchors" "href=\"#local_prop\"" html
assertContains "local references point previews at the visible target block" "data-reference-label=\"local_prop\" data-preview-target-id=\"local_prop\"" html
assertNotContains "local references do not use hidden preview ids" "data-reference-label=\"local_prop\" data-preview-id=\"" html
assertContains "visible target blocks expose preview metadata" "id=\"local_prop\" data-preview-kind=\"Proposition\" data-preview-label=\"local_prop\"" html
assertContains "imported references get preview metadata" "data-reference-label=\"imported_prop\"" html
assertContains "imported references link to their relative encoded theory route" "href=\"imported-preview#imported_prop\"" html
assertContains "imported references still use hidden preview templates" "data-reference-label=\"imported_prop\" data-preview-id=\"reference-preview-" html
assertNotContains "imported references do not get broken page anchors" "href=\"#imported_prop\"" html
assertNotContains "imported references are not non-clickable spans" "<span class=\"ref-badge has-preview\" data-reference-label=\"imported_prop\"" html
assertCount "hidden preview store only contains the imported fixture preview" 1 "class=\"reference-preview-template\"" html
assertContains "page grid is scoped to an explicit shell" "class=\"page-layout\"" html
assertNotContains "page grid does not apply to every body div" "body > div" html
assertContains "page heading uses the selected mounted source" "<h1>project:test/html-fixtures/root-preview.tex</h1>" html
assertContains "imported preview records its mounted source" "project:test/html-fixtures/imported-preview.tex" html
assertContains "imported preview source links to the same route" "href=\"imported-preview\"><code>project:test/html-fixtures/imported-preview.tex</code>" html
assertContains "imported source renders on its own line" "class=\"reference-preview-source\"" html
assertContains "multi-reference rendering preserves the comma separator" ", <a href=\"imported-preview#imported_prop\" class=\"ref-badge has-preview\" data-reference-label=\"imported_prop\"" html
assertContains "calculation justifications also use target previews" "Step 2: by <a href=\"#local_prop\" class=\"ref-badge has-preview\" data-reference-label=\"local_prop\" data-preview-target-id=\"local_prop\"" html
assertContains "large reference lists collapse to an ellipsis trigger" "Follows by <span class=\"ref-badge has-preview ref-badge-group\" data-preview-group=\"true\" data-reference-label=\"5 references\"" html
assertContains "collapsed references keep current-page item metadata" "data-reference-label=\"group_source\" data-preview-link=\"#group_source\" data-preview-target-id=\"group_source\"" html
assertContains "collapsed references keep imported item metadata" "data-reference-label=\"imported_prop\" data-preview-link=\"imported-preview#imported_prop\" data-preview-id=\"reference-preview-" html
assertNotContains "collapsed references do not inline the long list" "Follows by <a href=\"#local_prop\" class=\"ref-badge has-preview\" data-reference-label=\"local_prop\" data-preview-target-id=\"local_prop\" aria-describedby=\"reference-preview-popup\">local_prop</a>, <a href=\"#uses_refs\"" html
assertContains "collapsed tooltips compose full preview templates" "const preview = cloneHiddenPreview(item) || buildCurrentPreview(item) || buildMissingPreview(item);" supportScript
assertContains "collapsed tooltip labels become links" "template.append(linkGroupHeading(item, preview));" supportScript
assertContains "collapsed tooltip labels use generated reference links" "link.href = href;" supportScript
assertContains "collapsed tooltip heading links have hover affordance" ".reference-preview-heading a:hover," html
assertContains "collapsed tooltips use stacked preview sections" "className = 'reference-preview-group-template'" supportScript
assertContains "visible preview popup accepts pointer interaction" "pointer-events: auto;" html
assertContains "preview popup uses a wider bounded layout" "width: 44rem;" html
assertContains "preview popup uses a taller bounded layout" "max-height: min(34rem, calc(100vh - 2rem));" html
assertContains "behavior loads from the shared external script asset" "src=\"../../_static/naproche-html.js\"" html
assertNotContains "inline script bundles are not emitted" "<script type=\"text/javascript\">" html
assertContains "preview popup cancels delayed hide on pointer entry" "popup.addEventListener('pointerenter', clearHideTimer);" supportScript
assertContains "preview popup schedules delayed hide on pointer exit" "popup.addEventListener('pointerleave', scheduleHide);" supportScript
assertContains "group click pins the preview popup" "showPreview(trigger, event, true);" supportScript
assertContains "group keyboard activation pins the preview popup" "showPreview(trigger, null, true);" supportScript
assertContains "preview statements use a full-width paragraph" "class=\"reference-preview-statement\"" html
assertContains "preview popup is emitted once" "id=\"reference-preview-popup\"" html
missingReferenceFallback :: Assertion
missingReferenceFallback = do
let proof = Qed (Just Nowhere) (JustificationRef ("missing_ref" :| []))
blocks = [BlockProof Nowhere proof Nowhere]
html <- renderSynthetic blocks
assertContains "missing references remain visible" "missing_ref" html
assertNotContains "missing references do not claim preview content" "data-preview-id=" html
datatypeDerivedFactsAreOmitted :: Assertion
datatypeDerivedFactsAreOmitted = do
let blocks =
[ propformDatatypeBlock Nowhere
, referenceClaimBlock "uses_datatype_fact"
, referenceProofBlock "propform_induct"
]
html <- renderSynthetic blocks
assertContains "datatype declarations remain visible" "Datatype of " html
assertContains "derived fact references remain readable" "propform_induct" html
assertNotContains "unchecked datatype facts are not rendered" "<summary>Derived facts</summary>" html
assertNotContains "unchecked datatype facts do not become preview targets" "data-preview-label=\"propform_induct\"" html
renderSynthetic :: [Block] -> IO Text
renderSynthetic blocks = do
currentDirectory <- Directory.getCurrentDirectory
mounts <-
expectRight =<<
prepareSourceMounts
[(sourceMountId "project", currentDirectory)]
request <-
expectRight
(searchedRoot "test/html-fixtures/root-preview.tex")
graph <-
expectRight =<<
buildResolvedSourceGraph mounts request
layout <-
expectRight
(layoutHtmlSourceGraph
[(sourceMountId "project", [])]
graph)
context <-
expectRight
(htmlRenderContext
layout
(sourceGraphRootSource graph))
let (renderIndex, page :| _remainingPages) =
Html.buildRenderIndex
((sourceGraphRootSource graph, blocks) :| [])
expectRight
(Html.renderDocument
context
""
renderIndex
page)
expectRight :: (Show e, HasCallStack) => Either e a -> IO a
expectRight = \case
Left err ->
assertFailure ("expected Right, got Left " <> show err)
Right value ->
pure value
propformDatatypeBlock :: Location -> Block
propformDatatypeBlock blockLoc =
BlockData blockLoc Nothing "propform" propformDatatype
propformDatatype :: Datatype
propformDatatype =
Datatype
{ datatypeHeadExpr = ExprOp Nowhere (constSymbol "propform") []
, datatypeClauses =
DatatypeClause (ExprOp Nowhere (constSymbol "propbot") []) (ExprOp Nowhere (constSymbol "propform") []) [] :|
[ DatatypeClause (ExprOp Nowhere (unarySymbol "propvar") [ExprVar "n"]) (ExprOp Nowhere (constSymbol "propform") []) [("n", ExprOp Nowhere (constSymbol "naturals") [])]
, DatatypeClause
(ExprOp Nowhere (infixSymbol "propto") [ExprVar "p", ExprVar "q"])
(ExprOp Nowhere (constSymbol "propform") [])
[ ("p", ExprOp Nowhere (constSymbol "propform") [])
, ("q", ExprOp Nowhere (constSymbol "propform") [])
]
]
}
referenceClaimBlock :: Marker -> Block
referenceClaimBlock marker =
BlockClaim Proposition Nowhere Nothing marker (Claim [] (StmtFormula (PropositionalConstant Nowhere IsTop)))
referenceProofBlock :: Marker -> Block
referenceProofBlock marker =
BlockProof Nowhere (Qed (Just Nowhere) (JustificationRef (marker :| []))) Nowhere
constSymbol :: Text -> FunctionSymbol
constSymbol name =
mkMixfixItem [Just (Command name)] (Marker name) NonAssoc
unarySymbol :: Text -> FunctionSymbol
unarySymbol name =
mkMixfixItem [Just (Command name), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] (Marker name) NonAssoc
infixSymbol :: Text -> FunctionSymbol
infixSymbol name =
mkMixfixItem [Nothing, Just (Command name), Nothing] (Marker name) NonAssoc
assertContains :: HasCallStack => String -> Text -> Text -> Assertion
assertContains label needle haystack =
assertBool
(label <> "\nExpected to find: " <> Text.unpack needle)
(needle `Text.isInfixOf` haystack)
assertNotContains :: HasCallStack => String -> Text -> Text -> Assertion
assertNotContains label needle haystack =
assertBool
(label <> "\nDid not expect to find: " <> Text.unpack needle)
(not (needle `Text.isInfixOf` haystack))
assertCount :: HasCallStack => String -> Int -> Text -> Text -> Assertion
assertCount label expected needle haystack =
assertEqual
(label <> "\nExpected count for: " <> Text.unpack needle)
expected
(Text.count needle haystack)
|
