# HG changeset patch
# User wenzelm
# Date 1488749553 -3600
# Node ID 1edb570f5b174c89d62591fced3ad76f11199781
# Parent  12c6774a8f65e71083669f4f81d028912d423ea5
decorations for dotted underline: less intrusive;
tuned;

diff -r 12c6774a8f65 -r 1edb570f5b17 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Sun Mar 05 22:06:13 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Sun Mar 05 22:32:33 2017 +0100
@@ -93,7 +93,11 @@
                 "isabelle.quoted_light_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
                 "isabelle.quoted_dark_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
                 "isabelle.antiquoted_light_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" },
-                "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" }
+                "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" },
+                "isabelle.writeln_light_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
+                "isabelle.writeln_dark_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
+                "isabelle.information_light_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" },
+                "isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }
             }
         }
     },
diff -r 12c6774a8f65 -r 1edb570f5b17 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 05 22:06:13 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 05 22:32:33 2017 +0100
@@ -30,11 +30,15 @@
   "antiquoted"
 ]
 
-function property(prop: string, config: string): Object
+const dotted_colors = [
+  "writeln",
+  "information"
+]
+
+function get_color(color: string, light: boolean): string
 {
-  let res = {}
-  res[prop] = vscode.workspace.getConfiguration("isabelle").get<string>(config)
-  return res
+  const config = color.concat(light ? "_light" : "_dark").concat("_color")
+  return vscode.workspace.getConfiguration("isabelle").get<string>(config)
 }
 
 export function init(context: ExtensionContext)
@@ -48,10 +52,17 @@
 
   function background(color: string): TextEditorDecorationType
   {
-    const prop = "backgroundColor"
-    const light = property(prop, color.concat("_light_color"))
-    const dark = property(prop, color.concat("_dark_color"))
-    return decoration({ light: light, dark: dark })
+    return decoration(
+      { light: { backgroundColor: get_color(color, true) },
+        dark: { backgroundColor: get_color(color, false) } })
+  }
+
+  function dotted(color: string): TextEditorDecorationType
+  {
+    const border = "2px none; border-bottom-style: dotted; border-color: "
+    return decoration(
+      { light: { border: border.concat(get_color(color, true)) },
+        dark: { border: border.concat(get_color(color, false)) } })
   }
 
   types.clear
@@ -61,6 +72,9 @@
   for (let color of foreground_colors) {
     types["foreground_".concat(color)] = background(color) // approximation
   }
+  for (let color of dotted_colors) {
+    types["dotted_".concat(color)] = dotted(color)
+  }
   types["hover_message"] = decoration({})
 }
 
diff -r 12c6774a8f65 -r 1edb570f5b17 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 05 22:06:13 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 05 22:32:33 2017 +0100
@@ -17,7 +17,7 @@
 {
   /* decorations */
 
-  private def color_decorations(prefix: String, types: Rendering.Color.ValueSet,
+  private def color_decorations(prefix: String, types: Set[Rendering.Color.Value],
     colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] =
   {
     val color_ranges =
@@ -29,13 +29,16 @@
         color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: List[XML.Body]))))
   }
 
+  private val dotted_colors =
+    Set(Rendering.Color.writeln, Rendering.Color.information)
+
 
   /* diagnostic messages */
 
   private val message_severity =
     Map(
-      Markup.WRITELN -> Protocol.DiagnosticSeverity.Information,
-      Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
+      Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
+      Markup.INFORMATION -> Protocol.DiagnosticSeverity.Hint,
       Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
       Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
       Markup.ERROR -> Protocol.DiagnosticSeverity.Error)
@@ -46,6 +49,9 @@
   private val diagnostics_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
 
+  private val dotted_elements =
+    Markup.Elements(Markup.WRITELN, Markup.INFORMATION)
+
   private val hover_message_elements = Markup.Elements(Markup.BAD)
 
   private val hyperlink_elements =
@@ -107,6 +113,12 @@
   }
 
 
+  /* dotted underline */
+
+  def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
+    message_underline_color(VSCode_Rendering.dotted_elements, range)
+
+
   /* decorations */
 
   def hover_message: Document_Model.Decoration =
@@ -133,7 +145,9 @@
     VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
       background(model.content.text_range, Set.empty)) :::
     VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
-      foreground(model.content.text_range))
+      foreground(model.content.text_range)) :::
+    VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
+      dotted(model.content.text_range))
 
   def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
   {