299 } |
299 } |
300 |
300 |
301 |
301 |
302 /* content */ |
302 /* content */ |
303 |
303 |
304 def content(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content) |
304 def content(path: Path, content: Bytes): Content = new Content(path, content) |
305 def content(path: Path, content: String): Content_String = new Content_String(path, content) |
305 def content(path: Path, content: String): Content = new Content(path, Bytes(content)) |
306 def content(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content) |
306 def content(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content) |
307 |
307 |
308 trait Content { |
308 final class Content private[File](val path: Path, val content: Bytes) { |
309 def path: Path |
|
310 def write(dir: Path): Unit |
|
311 override def toString: String = path.toString |
309 override def toString: String = path.toString |
312 } |
310 |
313 |
|
314 final class Content_Bytes private[File](val path: Path, val content: Bytes) extends Content { |
|
315 def write(dir: Path): Unit = { |
311 def write(dir: Path): Unit = { |
316 val full_path = dir + path |
312 val full_path = dir + path |
317 Isabelle_System.make_directory(full_path.expand.dir) |
313 Isabelle_System.make_directory(full_path.expand.dir) |
318 Bytes.write(full_path, content) |
314 Bytes.write(full_path, content) |
319 } |
315 } |
320 } |
316 } |
321 |
317 |
322 final class Content_String private[File](val path: Path, val content: String) extends Content { |
|
323 def write(dir: Path): Unit = { |
|
324 val full_path = dir + path |
|
325 Isabelle_System.make_directory(full_path.expand.dir) |
|
326 File.write(full_path, content) |
|
327 } |
|
328 } |
|
329 |
|
330 final class Content_XML private[File](val path: Path, val content: XML.Body) { |
318 final class Content_XML private[File](val path: Path, val content: XML.Body) { |
331 override def toString: String = path.toString |
319 override def toString: String = path.toString |
332 |
320 |
333 def output(out: XML.Body => String): Content_String = |
321 def output(out: XML.Body => String): Content = new Content(path, Bytes(out(content))) |
334 new Content_String(path, out(content)) |
|
335 } |
322 } |
336 } |
323 } |