--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Jan 10 17:24:15 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 11 14:22:57 2017 +0100
@@ -247,4 +247,16 @@
}
)
}
+
+
+ /* output text */
+
+ def output_text(s: String): String =
+ if (options.bool("vscode_unicode_symbols")) Symbol.decode(s) else Symbol.encode(s)
+
+ def output_pretty(body: XML.Body, margin: Int): String =
+ output_text(Pretty.string_of(body, margin))
+
+ def output_xml(xml: XML.Tree): String =
+ output_text(XML.content(xml))
}