# HG changeset patch # User wenzelm # Date 1583778907 -3600 # Node ID f10bffaa2bae4db5c58d80ee070ab5718c732841 # Parent d7175626d61e8027e66506a7de10c06b4100c8aa more scalable output of YXML files; diff -r d7175626d61e -r f10bffaa2bae src/Pure/General/file.scala --- 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)) diff -r d7175626d61e -r f10bffaa2bae src/Pure/PIDE/yxml.scala --- 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 } diff -r d7175626d61e -r f10bffaa2bae src/Pure/Tools/dump.scala --- 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,