--- a/src/Pure/General/file.scala Mon Mar 09 16:58:23 2020 +0100
+++ b/src/Pure/General/file.scala Mon Mar 09 19:35:07 2020 +0100
@@ -231,6 +231,9 @@
/* write */
+ def writer(file: JFile): BufferedWriter =
+ new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset))
+
def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
{
val stream = make_stream(new FileOutputStream(file))
--- a/src/Pure/PIDE/yxml.scala Mon Mar 09 16:58:23 2020 +0100
+++ b/src/Pure/PIDE/yxml.scala Mon Mar 09 19:35:07 2020 +0100
@@ -24,6 +24,7 @@
val X_string = X.toString
val Y_string = Y.toString
val XY_string = X_string + Y_string
+ val XYX_string = XY_string + X_string
def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
def detect_elem(s: String): Boolean = s.startsWith(XY_string)
@@ -31,19 +32,26 @@
/* string representation */ // FIXME byte array version with pseudo-utf-8 (!?)
- def string_of_body(body: XML.Body): String =
+ def traversal(string: String => Unit, body: XML.Body): Unit =
{
- val s = new StringBuilder
- def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
def tree(t: XML.Tree): Unit =
t match {
case XML.Elem(Markup(name, atts), ts) =>
- s += X; s += Y; s ++= name; atts.foreach(attrib); s += X
+ string(XY_string)
+ string(name)
+ for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
+ string(X_string)
ts.foreach(tree)
- s += X; s += Y; s += X
- case XML.Text(text) => s ++= text
+ string(XYX_string)
+ case XML.Text(text) => string(text)
}
body.foreach(tree)
+ }
+
+ def string_of_body(body: XML.Body): String =
+ {
+ val s = new StringBuilder
+ traversal(str => s ++= str, body)
s.toString
}
--- a/src/Pure/Tools/dump.scala Mon Mar 09 16:58:23 2020 +0100
+++ b/src/Pure/Tools/dump.scala Mon Mar 09 19:35:07 2020 +0100
@@ -6,6 +6,8 @@
package isabelle
+import java.io.{BufferedWriter, FileOutputStream, OutputStreamWriter}
+
object Dump
{
@@ -19,18 +21,22 @@
snapshot: Document.Snapshot,
status: Document_Status.Node_Status)
{
- def write(file_name: Path, bytes: Bytes)
+ def write_path(file_name: Path): Path =
{
val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
Isabelle_System.mkdirs(path.dir)
- Bytes.write(path, bytes)
+ path
}
+ def write(file_name: Path, bytes: Bytes): Unit =
+ Bytes.write(write_path(file_name), bytes)
+
def write(file_name: Path, text: String): Unit =
write(file_name, Bytes(text))
def write(file_name: Path, body: XML.Body): Unit =
- write(file_name, Symbol.encode(YXML.string_of_body(body)))
+ using(File.writer(write_path(file_name).file))(
+ writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body))
}
sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,