diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
index 66cf347..3e0b146 100644
--- a/DocGen4/Output/Definition.lean
+++ b/DocGen4/Output/Definition.lean
@@ -11,7 +11,7 @@ open Lean Widget
 def equationLimit : Nat := 200
 
 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
-  pure <li «class»="equation">[←infoFormatToHtml c]</li>
+  pure <li class="equation">[←infoFormatToHtml c]</li>
 
 def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
   if let some eqs := i.equations then
@@ -21,8 +21,8 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
       pure #[
         <details>
           <summary>Equations</summary>
-          <ul «class»="equations">
-            <li «class»="equation">One or more equations did not get rendered due to their size.</li>
+          <ul class="equations">
+            <li class="equation">One or more equations did not get rendered due to their size.</li>
             [filteredEquationsHtml]
           </ul>
         </details>
@@ -31,7 +31,7 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
       pure #[
         <details>
           <summary>Equations</summary>
-          <ul «class»="equations">
+          <ul class="equations">
             [filteredEquationsHtml]
           </ul>
         </details>
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index ab29718..a51031a 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -9,7 +9,7 @@ open scoped DocGen4.Jsx
 def ctorToHtml (i : NameInfo) : HtmlM Html := do
   let shortName := i.name.components'.head!.toString
   let name := i.name.toString
-  pure <li «class»="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
+  pure <li class="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
 
 def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
   let constructorsHtml := <ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index a703ccf..062a3ca 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -33,17 +33,17 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   let inner := Html.element "span" true #[("class", "fn")] nodes
   let html := Html.element "span" false #[("class", "decl_args")] #[inner]
   if implicit then
-    pure <span «class»="impl_arg">{html}</span>
+    pure <span class="impl_arg">{html}</span>
   else
     pure html
 
 def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
   let mut nodes := #[]
   if s.parents.size > 0 then
-    nodes := nodes.push <span «class»="decl_extends">extends</span>
+    nodes := nodes.push <span class="decl_extends">extends</span>
     let mut parents := #[]
     for parent in s.parents do
-      let link := <a «class»="break_within" href={←declNameToLink parent}>{parent.toString}</a>
+      let link := <a class="break_within" href={←declNameToLink parent}>{parent.toString}</a>
       let inner := Html.element "span" true #[("class", "fn")] #[link]
       let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
       parents := parents.push html
@@ -52,10 +52,10 @@ def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
 
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
-  nodes := nodes.push <span «class»="decl_kind">{doc.getKindDescription}</span>
+  nodes := nodes.push <span class="decl_kind">{doc.getKindDescription}</span>
   nodes := nodes.push
-    <span «class»="decl_name">
-      <a «class»="break_within" href={←declNameToLink doc.getName}>
+    <span class="decl_name">
+      <a class="break_within" href={←declNameToLink doc.getName}>
         -- TODO: HTMLify the name
         {doc.getName.toString}
       </a>
@@ -69,9 +69,9 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo)
   | _ => nodes := nodes
 
-  nodes := nodes.push <span «class»="decl_args">:</span>
+  nodes := nodes.push <span class="decl_args">:</span>
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
-  pure <div «class»="decl_header"> [nodes] </div>
+  pure <div class="decl_header"> [nodes] </div>
 
 def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   -- basic info like headers, types, structure fields, etc.
@@ -101,9 +101,9 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
       #[]
 
   pure
-    <div «class»="decl" id={doc.getName.toString}>
-      <div «class»={doc.getKind}>
-        <div «class»="gh_link">
+    <div class="decl" id={doc.getName.toString}>
+      <div class={doc.getKind}>
+        <div class="gh_link">
           <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
         </div>
         [attrsHtml]
@@ -116,7 +116,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
 
 def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
   pure 
-    <div «class»="mod_doc">
+    <div class="mod_doc">
       [←docStringToHtml mdoc.doc]
     </div>
 
@@ -126,8 +126,8 @@ def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := d
   | ModuleMember.modDoc d => modDocToHtml module d
 
 def declarationToNavLink (module : Name) : Html :=
-  <div «class»="nav_link">
-    <a «class»="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
+  <div class="nav_link">
+    <a class="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
   </div>
 
 -- TODO: Similar functions are used all over the place, we should dedup them
@@ -165,10 +165,10 @@ def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
 
 def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
   pure
-    <nav «class»="internal_nav">
-      <h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
-      <p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
-      <div «class»="imports">
+    <nav class="internal_nav">
+      <h3><a class="break_within" href="#top">{moduleName.toString}</a></h3>
+      <p class="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
+      <div class="imports">
         <details>
           <summary>Imports</summary>
           <ul>
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index 1a75288..480f3b3 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -14,7 +14,7 @@ open Lean
 open scoped DocGen4.Jsx
 
 def moduleListFile (file : Name) : HtmlM Html := do
-  pure <div «class»={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
+  pure <div class={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
     <a href={← moduleNameToLink file}>{file.toString}</a>
   </div>
 
@@ -48,17 +48,17 @@ def moduleList : HtmlM Html := do
 
 def navbar : HtmlM Html := do
   pure
-    <nav «class»="nav">
+    <nav class="nav">
       <h3>General documentation</h3>
-      <div «class»="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
+      <div class="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
       /-
       TODO: Add these in later
-      <div «class»="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>
-      <div «class»="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</a></div>
-      <div «class»="nav_link"><a href={s!"{←getRoot}hole_commands.html"}>hole commands</a></div>
-      <div «class»="nav_link"><a href={s!"{←getRoot}attributes.html"}>attributes</a></div>
-      <div «class»="nav_link"><a href={s!"{←getRoot}notes.html"}>notes</a></div>
-      <div «class»="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
+      <div class="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>
+      <div class="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</a></div>
+      <div class="nav_link"><a href={s!"{←getRoot}hole_commands.html"}>hole commands</a></div>
+      <div class="nav_link"><a href={s!"{←getRoot}attributes.html"}>attributes</a></div>
+      <div class="nav_link"><a href={s!"{←getRoot}notes.html"}>notes</a></div>
+      <div class="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
       -/
       <h3>Library</h3>
       {← moduleList}
diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
index 8bc03e5..aa0b8d8 100644
--- a/DocGen4/Output/Structure.lean
+++ b/DocGen4/Output/Structure.lean
@@ -13,30 +13,30 @@ def fieldToHtml (f : NameInfo) : HtmlM Html := do
   if let some doc := f.doc then
     let renderedDoc ← docStringToHtml doc
     pure
-      <li id={name} «class»="structure_field">
-        <div «class»="structure_field_doc">[renderedDoc]</div>
-        <div «class»="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
+      <li id={name} class="structure_field">
+        <div class="structure_field_doc">[renderedDoc]</div>
+        <div class="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
       </li>
   else
     pure
-      <li id={name} «class»="structure_field">
-        <div «class»="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
+      <li id={name} class="structure_field">
+        <div class="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
       </li>
 
 def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
   let structureHtml :=
     if Name.isSuffixOf `mk i.ctor.name then
-      (<ul «class»="structure_fields" id={i.ctor.name.toString}>
+      (<ul class="structure_fields" id={i.ctor.name.toString}>
         [←i.fieldInfo.mapM fieldToHtml]
       </ul>)
     else
       let ctorShortName := i.ctor.name.components'.head!.toString
-      (<ul «class»="structure_ext">
-        <li id={i.ctor.name.toString} «class»="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
-        <ul «class»="structure_ext_fields">
+      (<ul class="structure_ext">
+        <li id={i.ctor.name.toString} class="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
+        <ul class="structure_ext_fields">
           [←i.fieldInfo.mapM fieldToHtml]
         </ul>
-        <li «class»="structure_ext_ctor">)</li>
+        <li class="structure_ext_ctor">)</li>
       </ul>)
   pure #[structureHtml]
 
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index c34051d..aed65c7 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -42,8 +42,8 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
         <input id="nav_toggle" type="checkbox"/>
 
         <header>
-          <h1><label «for»="nav_toggle"></label>Documentation</h1>
-          <p «class»="header_filename break_within">{title}</p>
+          <h1><label for="nav_toggle"></label>Documentation</h1>
+          <p class="header_filename break_within">{title}</p>
           -- TODO: Replace this form with our own search
           <form action="https://google.com/search" method="get" id="search_form">
             <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs"/>
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean
index c8f83d1..bd6f875 100644
--- a/DocGen4/ToHtmlFormat.lean
+++ b/DocGen4/ToHtmlFormat.lean
@@ -81,14 +81,14 @@ def jsxText : Parser :=
 @[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
 @[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
 
-syntax jsxAttrName := ident <|> str
+syntax jsxAttrName := rawIdent <|> str
 syntax jsxAttrVal := str <|> group("{" term "}")
 syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal
 syntax jsxAttrSpread := "[" term "]"
 syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
 
-syntax "<" ident jsxAttr* "/>" : jsxElement
-syntax "<" ident jsxAttr* ">" jsxChild* "</" ident ">" : jsxElement
+syntax "<" rawIdent jsxAttr* "/>" : jsxElement
+syntax "<" rawIdent jsxAttr* ">" jsxChild* "</" rawIdent ">" : jsxElement
 
 syntax jsxText      : jsxChild
 syntax "{" term "}" : jsxChild