src/Pure/General/file.scala
changeset 75824 a2b2e8964e1a
parent 75823 6eb8d6cdb686
child 75825 ad00fbf64bff
equal deleted inserted replaced
75823:6eb8d6cdb686 75824:a2b2e8964e1a
   299   }
   299   }
   300 
   300 
   301 
   301 
   302   /* content */
   302   /* content */
   303 
   303 
   304   object Content {
   304   def content(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content)
   305     def apply(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content)
   305   def content(path: Path, content: String): Content_String = new Content_String(path, content)
   306     def apply(path: Path, content: String): Content_String = new Content_String(path, content)
   306   def content(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
   307     def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
       
   308   }
       
   309 
   307 
   310   trait Content {
   308   trait Content {
   311     def path: Path
   309     def path: Path
   312     def write(dir: Path): Unit
   310     def write(dir: Path): Unit
   313     override def toString: String = path.toString
   311     override def toString: String = path.toString