# HG changeset patch
# User wenzelm
# Date 1477218879 -7200
# Node ID ebbe7cf0c2b80b2b24564c093d297cde82064e3b
# Parent  c6a1031cf9253ef98be20d1ef266f7341610d4ce
tuned;

diff -r c6a1031cf925 -r ebbe7cf0c2b8 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Oct 23 12:30:57 2016 +0200
+++ b/src/Pure/Thy/html.scala	Sun Oct 23 12:34:39 2016 +0200
@@ -81,14 +81,16 @@
   def output(tree: XML.Tree): String = output(List(tree))
 
 
-  /* structured markup */
+  /* markup operators */
+
+  type Operator = XML.Body => XML.Elem
 
-  def chapter(body: XML.Body): XML.Elem = XML.elem("h1", body)
-  def section(body: XML.Body): XML.Elem = XML.elem("h2", body)
-  def subsection(body: XML.Body): XML.Elem = XML.elem("h3", body)
-  def subsubsection(body: XML.Body): XML.Elem = XML.elem("h4", body)
-  def paragraph(body: XML.Body): XML.Elem = XML.elem("h5", body)
-  def subparagraph(body: XML.Body): XML.Elem = XML.elem("h6", body)
+  val chapter: Operator = XML.elem("h1", _)
+  val section: Operator = XML.elem("h2", _)
+  val subsection: Operator = XML.elem("h3", _)
+  val subsubsection: Operator = XML.elem("h4", _)
+  val paragraph: Operator = XML.elem("h5", _)
+  val subparagraph: Operator = XML.elem("h6", _)
 
 
   /* document */