# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1719754359 -7200
# Node ID b2df8bf17071247dcd0e802535a0490b19aa8ea1
# Parent  fe9ae6b67c29598d67eff9395328277d0637f5db
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;

diff -r fe9ae6b67c29 -r b2df8bf17071 src/Tools/VSCode/etc/options
--- a/src/Tools/VSCode/etc/options	Sun Jun 30 15:32:32 2024 +0200
+++ b/src/Tools/VSCode/etc/options	Sun Jun 30 15:32:39 2024 +0200
@@ -21,8 +21,11 @@
 option vscode_pide_extensions : bool = false for vscode
   -- "use PIDE extensions for Language Server Protocol"
 
-option vscode_unicode_symbols : bool = false for vscode
-  -- "output Isabelle symbols via Unicode (according to etc/symbols)"
+option vscode_unicode_symbols_output : bool = false for vscode
+  -- "output Isabelle symbols via Unicode in Output (e.g. tooltips and panels) (according to etc/symbols)"
+
+option vscode_unicode_symbols_edits : bool = false for vscode
+  -- "output Isabelle symbols via Unicode in Edits (e.g. completions and code actions) (according to etc/symbols)"
 
 option vscode_caret_perspective : int = 50 for vscode
   -- "number of visible lines above and below the caret (0: unrestricted)"
diff -r fe9ae6b67c29 -r b2df8bf17071 src/Tools/VSCode/src/component_vscode_extension.scala
--- a/src/Tools/VSCode/src/component_vscode_extension.scala	Sun Jun 30 15:32:32 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala	Sun Jun 30 15:32:39 2024 +0200
@@ -160,7 +160,8 @@
       }
 
       val default = opt.name match {
-        case "vscode_unicode_symbols" => "true"
+        case "vscode_unicode_symbols_output" => "true"
+        case "vscode_unicode_symbols_edits" => "false"
         case "vscode_pide_extensions" => "true"
         case "vscode_html_output" => "true"
         case _ => ""
diff -r fe9ae6b67c29 -r b2df8bf17071 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sun Jun 30 15:32:32 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Sun Jun 30 15:32:39 2024 +0200
@@ -228,7 +228,7 @@
 
   private val syslog_messages =
     Session.Consumer[Prover.Output](getClass.getName) {
-      case output => channel.log_writeln(resources.output_xml(output.message))
+      case output => channel.log_writeln(resources.output_xml_text(output.message))
     }
 
 
diff -r fe9ae6b67c29 -r b2df8bf17071 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Jun 30 15:32:32 2024 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Jun 30 15:32:39 2024 +0200
@@ -61,12 +61,14 @@
       def convert_symbols(body: XML.Body): XML.Body = {
         body.map {
           case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body))
-          case XML.Text(content) => XML.Text(Symbol.output(resources.unicode_symbols, content))
+          case XML.Text(content) => XML.Text(resources.output_text(content))
         }
       }
 
-      val tree = Markup_Tree.from_XML(convert_symbols(formatted))
-      val text = resources.output_text(XML.content(formatted))
+      val converted = convert_symbols(formatted)
+
+      val tree = Markup_Tree.from_XML(converted)
+      val text = XML.content(converted)
 
       val document = Line.Document(text)
       val decorations = tree
diff -r fe9ae6b67c29 -r b2df8bf17071 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jun 30 15:32:32 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jun 30 15:32:39 2024 +0200
@@ -80,7 +80,7 @@
   def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] = {
     val doc = model.content.doc
     val line = node_pos.pos.line
-    val unicode = File.is_thy(node_pos.name)
+    val unicode = resources.unicode_symbols_edits
     doc.offset(Line.Position(line)) match {
       case None => Nil
       case Some(line_start) =>
diff -r fe9ae6b67c29 -r b2df8bf17071 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jun 30 15:32:32 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jun 30 15:32:39 2024 +0200
@@ -80,12 +80,14 @@
   /* options */
 
   def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
-  def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
   def html_output: Boolean = options.bool("vscode_html_output")
   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
   def message_margin: Int = options.int("vscode_message_margin")
   def output_delay: Time = options.seconds("vscode_output_delay")
 
+  def unicode_symbols_output: Boolean = options.bool("vscode_unicode_symbols_output")
+  def unicode_symbols_edits: Boolean = options.bool("vscode_unicode_symbols_edits")
+
 
   /* document node name */
 
@@ -332,11 +334,13 @@
 
   /* output text */
 
-  def output_text(text: String): String =
-    Symbol.output(unicode_symbols, text)
+  def output_text(content: String): String =
+    Symbol.output(unicode_symbols_output, content)
+  def output_edit(content: String): String =
+    Symbol.output(unicode_symbols_edits, content)
 
-  def output_xml(xml: XML.Tree): String =
-    output_text(XML.content(xml))
+  def output_xml_text(body: XML.Tree): String =
+    output_text(XML.content(body))
 
   def output_pretty(body: XML.Body, margin: Double): String =
     output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))