# HG changeset patch
# User wenzelm
# Date 1310295622 -7200
# Node ID 8a63c95b1d5bbf03d33a5b53c04e0e6de2c14388
# Parent  9b5dadb0c28da54b99dbc80346a77c9fb4cc4d07
less currying in Scala;

diff -r 9b5dadb0c28d -r 8a63c95b1d5b src/Pure/General/xml_data.scala
--- 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)))
diff -r 9b5dadb0c28d -r 8a63c95b1d5b src/Pure/PIDE/isar_document.scala
--- 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),
diff -r 9b5dadb0c28d -r 8a63c95b1d5b src/Pure/Thy/thy_header.scala
--- 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)