--- a/src/Pure/General/xml_data.scala Sun Jul 10 00:21:19 2011 +0200
+++ b/src/Pure/General/xml_data.scala Sun Jul 10 13:00:22 2011 +0200
@@ -100,21 +100,21 @@
def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
- def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body =
+ def make_pair[A, B](make1: A => XML.Body, make2: B => XML.Body)(p: (A, B)): XML.Body =
List(make_node(make1(p._1)), make_node(make2(p._2)))
- def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) =
+ def dest_pair[A, B](dest1: XML.Body => A, dest2: XML.Body => B)(ts: XML.Body): (A, B) =
ts match {
case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
case _ => throw new XML_Body(ts)
}
- def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body)
+ def make_triple[A, B, C](make1: A => XML.Body, make2: B => XML.Body, make3: C => XML.Body)
(p: (A, B, C)): XML.Body =
List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
- def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C)
+ def dest_triple[A, B, C](dest1: XML.Body => A, dest2: XML.Body => B, dest3: XML.Body => C)
(ts: XML.Body): (A, B, C) =
ts match {
case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
--- a/src/Pure/PIDE/isar_document.scala Sun Jul 10 00:21:19 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Sun Jul 10 13:00:22 2011 +0200
@@ -144,14 +144,14 @@
{
val arg1 =
XML_Data.make_list(
- XML_Data.make_pair(XML_Data.make_string)(
+ XML_Data.make_pair(XML_Data.make_string,
XML_Data.make_option(XML_Data.make_list(
XML_Data.make_pair(
- XML_Data.make_option(XML_Data.make_long))(
+ XML_Data.make_option(XML_Data.make_long),
XML_Data.make_option(XML_Data.make_long))))))(edits)
val arg2 =
- XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string)(Thy_Header.make_xml_data))(headers)
+ XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string, Thy_Header.make_xml_data))(headers)
input("Isar_Document.edit_version",
Document.ID(old_id), Document.ID(new_id),
--- a/src/Pure/Thy/thy_header.scala Sun Jul 10 00:21:19 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala Sun Jul 10 13:00:22 2011 +0200
@@ -32,8 +32,8 @@
}
def make_xml_data(header: Header): XML.Body =
- XML_Data.make_triple(XML_Data.make_string)(
- XML_Data.make_list(XML_Data.make_string))(
+ XML_Data.make_triple(XML_Data.make_string,
+ XML_Data.make_list(XML_Data.make_string),
XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)