Implement hidden sections

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-11-03 17:13:05 -08:00
parent c77bb6f900
commit 0b4a1f2ebd
3 changed files with 17 additions and 7 deletions

View File

@ -8,7 +8,7 @@ import Parser exposing (Parser, Trailing(..), (|.), (|=))
import Set exposing (Set)
reserved : Set String
reserved = Set.fromList ["section"]
reserved = Set.fromList ["hidden", "section"]
strLit : Parser String
strLit =
@ -120,7 +120,13 @@ rules = Parser.sequence
sectionExp : Parser Section
sectionExp =
Parser.succeed (\n rs -> { name = n, rules = rs })
Parser.succeed (\h n rs -> { hidden = h, name = n, rules = rs })
|= Parser.oneOf
[ Parser.succeed True
|. Parser.symbol "hidden"
|. Parser.spaces
, Parser.succeed False
]
|. Parser.symbol "section" |. Parser.spaces
|= strLit |. Parser.spaces
|. Parser.symbol "{" |. Parser.spaces
@ -137,7 +143,7 @@ sectionImp =
_ -> Parser.succeed (Parser.Done <| List.reverse rs)
])
|> Parser.loop []
|> Parser.map (\rs -> { name = "", rules = rs })
|> Parser.map (\rs -> { hidden = False, name = "", rules = rs })
program : Parser RuleEnv
program =

View File

@ -15,6 +15,7 @@ type alias Rule =
type alias Section =
{ name : String
, rules : List Rule
, hidden: Bool
}
type ProofTree = MkProofTree

View File

@ -181,10 +181,13 @@ viewRuleSection env sec =
List.map (viewRule env) sec.rules
|> sequenceMaybes
|> Maybe.map (\rs ->
Html.div [ class "bergamot-rule-section" ]
[ Html.div [ class "bergamot-rule-list" ] rs
, Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
])
case sec.hidden of
True -> Html.div [ class "bergamot-rule-section" ] []
False ->
Html.div [ class "bergamot-rule-section" ]
[ Html.div [ class "bergamot-rule-list" ] rs
, Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
])
viewRules : String -> String -> Html Msg
viewRules renderProgs progs =