# HG changeset patch
# User wenzelm
# Date 1484140977 -3600
# Node ID 41e2797af4963b09327b8acdb30130c6f4182695
# Parent  a73ac955822086a274c10d9d35d2c135630d531e
clarified text output wrt. symbols;

diff -r a73ac9558220 -r 41e2797af496 src/Tools/VSCode/etc/options
--- a/src/Tools/VSCode/etc/options	Tue Jan 10 17:24:15 2017 +0100
+++ b/src/Tools/VSCode/etc/options	Wed Jan 11 14:22:57 2017 +0100
@@ -17,3 +17,6 @@
 
 option vscode_timing_threshold : real = 0.1
   -- "default threshold for timing display (seconds)"
+
+option vscode_unicode_symbols : bool = false
+  -- "output Isabelle symbols via Unicode (according to etc/symbols)"
diff -r a73ac9558220 -r 41e2797af496 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Jan 10 17:24:15 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Jan 11 14:22:57 2017 +0100
@@ -164,7 +164,7 @@
   private val syslog =
     Session.Consumer[Prover.Message](getClass.getName) {
       case output: Prover.Output if output.is_syslog =>
-        channel.log_writeln(XML.content(output.message))
+        channel.log_writeln(resources.output_xml(output.message))
       case _ =>
     }
 
@@ -289,7 +289,7 @@
         val doc = rendering.model.content.doc
         val range = doc.range(info.range)
         val contents =
-          info.info.map(tree => Pretty.string_of(List(tree), margin = rendering.tooltip_margin))
+          info.info.map(tree => resources.output_pretty(List(tree), rendering.tooltip_margin))
         (range, contents)
       }
     channel.write(Protocol.Hover.reply(id, result))
diff -r a73ac9558220 -r 41e2797af496 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jan 10 17:24:15 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jan 11 14:22:57 2017 +0100
@@ -64,7 +64,7 @@
       range = model.content.doc.range(text_range)
       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
     } yield {
-      val message = Pretty.string_of(body, margin = diagnostics_margin)
+      val message = resources.output_pretty(body, diagnostics_margin)
       val severity = VSCode_Rendering.message_severity.get(name)
       Protocol.Diagnostic(range, message, severity = severity)
     }).toList
diff -r a73ac9558220 -r 41e2797af496 src/Tools/VSCode/src/vscode_resources.scala
--- 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))
 }