less currying in Scala;
authorwenzelm
Sun Jul 10 13:00:22 2011 +0200 (2011-07-10)
changeset 437238a63c95b1d5b
parent 43722 9b5dadb0c28d
child 43724 4e58485fa320
less currying in Scala;
src/Pure/General/xml_data.scala
src/Pure/PIDE/isar_document.scala
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/General/xml_data.scala	Sun Jul 10 00:21:19 2011 +0200
     1.2 +++ b/src/Pure/General/xml_data.scala	Sun Jul 10 13:00:22 2011 +0200
     1.3 @@ -100,21 +100,21 @@
     1.4    def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
     1.5  
     1.6  
     1.7 -  def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body =
     1.8 +  def make_pair[A, B](make1: A => XML.Body, make2: B => XML.Body)(p: (A, B)): XML.Body =
     1.9      List(make_node(make1(p._1)), make_node(make2(p._2)))
    1.10  
    1.11 -  def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) =
    1.12 +  def dest_pair[A, B](dest1: XML.Body => A, dest2: XML.Body => B)(ts: XML.Body): (A, B) =
    1.13      ts match {
    1.14        case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
    1.15        case _ => throw new XML_Body(ts)
    1.16      }
    1.17  
    1.18  
    1.19 -  def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body)
    1.20 +  def make_triple[A, B, C](make1: A => XML.Body, make2: B => XML.Body, make3: C => XML.Body)
    1.21        (p: (A, B, C)): XML.Body =
    1.22      List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
    1.23  
    1.24 -  def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C)
    1.25 +  def dest_triple[A, B, C](dest1: XML.Body => A, dest2: XML.Body => B, dest3: XML.Body => C)
    1.26        (ts: XML.Body): (A, B, C) =
    1.27      ts match {
    1.28        case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
     2.1 --- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 00:21:19 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 13:00:22 2011 +0200
     2.3 @@ -144,14 +144,14 @@
     2.4    {
     2.5      val arg1 =
     2.6        XML_Data.make_list(
     2.7 -        XML_Data.make_pair(XML_Data.make_string)(
     2.8 +        XML_Data.make_pair(XML_Data.make_string,
     2.9            XML_Data.make_option(XML_Data.make_list(
    2.10                XML_Data.make_pair(
    2.11 -                XML_Data.make_option(XML_Data.make_long))(
    2.12 +                XML_Data.make_option(XML_Data.make_long),
    2.13                  XML_Data.make_option(XML_Data.make_long))))))(edits)
    2.14  
    2.15      val arg2 =
    2.16 -      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string)(Thy_Header.make_xml_data))(headers)
    2.17 +      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string, Thy_Header.make_xml_data))(headers)
    2.18  
    2.19      input("Isar_Document.edit_version",
    2.20        Document.ID(old_id), Document.ID(new_id),
     3.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 00:21:19 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:00:22 2011 +0200
     3.3 @@ -32,8 +32,8 @@
     3.4    }
     3.5  
     3.6    def make_xml_data(header: Header): XML.Body =
     3.7 -    XML_Data.make_triple(XML_Data.make_string)(
     3.8 -      XML_Data.make_list(XML_Data.make_string))(
     3.9 +    XML_Data.make_triple(XML_Data.make_string,
    3.10 +      XML_Data.make_list(XML_Data.make_string),
    3.11          XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)
    3.12  
    3.13