src/Tools/VSCode/etc/options

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/etc/options	Tue Dec 20 22:24:16 2016 +0100
@@ -0,0 +1,7 @@
+(* :mode=isabelle-options: *)
+
+option vscode_tooltip_margin : int = 60
+  -- "margin for tooltip pretty-printing"
+
+option vscode_timing_threshold : real = 0.1
+  -- "default threshold for timing display (seconds)"