--- a/src/Pure/PIDE/markup.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/PIDE/markup.scala Fri Apr 01 23:19:12 2022 +0200
@@ -730,12 +730,12 @@
/* XML data representation */
- def encode: XML.Encode.T[Markup] = (markup: Markup) => {
+ def encode: XML.Encode.T[Markup] = { (markup: Markup) =>
import XML.Encode._
pair(string, properties)((markup.name, markup.properties))
}
- def decode: XML.Decode.T[Markup] = (body: XML.Body) => {
+ def decode: XML.Decode.T[Markup] = { (body: XML.Body) =>
import XML.Decode._
val (name, props) = pair(string, properties)(body)
Markup(name, props)