# Views and IDRX
Views are Idris values that render HTML. Most app views should be written in
`.idrx` files because they look like normal HTML while still compiling through
Idris.
## 1. A Page View
In a `.idrx` file you can write HTML directly:
```idris
module Web.View.Articles
import Iwf
import Generated.Schema
%default partial
export
articlePage : Article -> Html
articlePage article =
fragment
[ {article.title}
,
{article.title}
{article.description}
{article.body}
]
```
The `.idrx` preprocessor writes generated Idris under `build/generated/`.
Application code imports the generated module through the normal package build.
For full browser requests, `render` inserts the default shell around the view.
For HTMX requests, `render` returns only the main content and head-update
carrier.
## 2. Dynamic Text
Use `{...}` holes for Idris values:
```idris
{article.title}
{show article.favoritesCount}
{maybe "" id article.description}
```
Child holes use `ToHtml`. Dynamic text is escaped by default.
## 3. Dynamic Attributes
Attribute holes use `ToAttribute`:
```idris
{article.title}
```
Spread attributes use `ToAttributes`:
```idris
let attrs = [classListAttr ["btn", "btn-primary"], dataAttr "role" "save"]
in
```
## 4. Lists And Conditionals
Lists of `Html` render directly:
```idris
tagLink : String -> Html
tagLink tag =
{tag}
tagList : List String -> Html
tagList tags =
{map tagLink tags}
```
Useful helpers:
- `empty`
- `fragment`
- `forEach`
- `maybeHtml`
- `htmlToString`
- `preEscapedToHtml`
Use raw/pre-escaped HTML only for content that has already been sanitized or is
framework-owned.
## 5. Classes And Attributes
Use helpers for dynamic state:
- `classNames`
- `classAttr`
- `classes`
- `classListAttr`
- `whenClass`
- `unlessClass`
- `maybeClass`
- `dataAttr`
- `ariaAttr`
- `whenAttr`
- `unlessAttr`
- `maybeAttr`
- `whenAttrs`
- `unlessAttrs`
- `maybeAttrs`
Example:
```idris
```
## 6. HTMX Attributes
HTMX helpers are normal attributes:
```idris
reloadButton : String -> Html
reloadButton slug =
let commentsPath = pathTo showArticleCommentsRoute (MkArticleSlugInput slug)
in
```
Use server routes and `pathTo` instead of repeating route strings in views when
the route already has a named value. In multi-file apps, views should import
handlerless route specs from `Web.Routes`; executable `handledBy` bindings live
separately in `Web.RouteBindings`.
## 7. Plain `.idr` Files
In plain `.idr` files, use the string-backed macro:
```idris
view : String -> Html
view title =
idrx "
{title}
"
```
Use Idris raw strings when the IDRX contains nested Idris string literals:
```idris
link : ShowArticleInput -> Html
link input =
idrx #"Read"#
```
In `.idrx` files, do not write `idrx `. Write the bare tag.
## 8. Page Head And SEO
Put simple page titles at the top level. When a page needs additional metadata,
return a top-level `` followed by the content:
```idris
articleView : Article -> Html
articleView article =
fragment
[
{article.title}
{descriptionMeta article.description}
{canonicalLink ("https://example.test/article/" ++ article.slug)}
{openGraphTitle article.title}
,
{article.title}
]
```
The renderer merges those head entries into the full document. HTMX responses
carry the same entries in a head-update template while returning only the main
content.
For sitemap responses, use `sitemapXml` with `SitemapUrl` values.
## Next
Read [Forms and Validation](forms-and-validation.md).