--- a/src/Tools/VSCode/etc/options Wed Dec 28 11:28:31 2016 +0100
+++ b/src/Tools/VSCode/etc/options Wed Dec 28 16:45:00 2016 +0100
@@ -1,7 +1,10 @@
(* :mode=isabelle-options: *)
option vscode_tooltip_margin : int = 60
- -- "margin for tooltip pretty-printing"
+ -- "margin for pretty-printing of tooltips"
+
+option vscode_diagnostics_margin : int = 80
+ -- "margin for pretty-printing of diagnostic messages"
option vscode_timing_threshold : real = 0.1
-- "default threshold for timing display (seconds)"