clarified default settings;
authorwenzelm
Sat, 26 Feb 2022 21:58:54 +0100
changeset 75157 d67ec542b5b5
parent 75156 09da7b15162b
child 75158 a2311e4441f0
clarified default settings;
src/Tools/VSCode/src/vscode_setup.scala
--- a/src/Tools/VSCode/src/vscode_setup.scala	Sat Feb 26 21:48:25 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Sat Feb 26 21:58:54 2022 +0100
@@ -19,6 +19,7 @@
 
   def vscode_home: Path = Path.variable("ISABELLE_VSCODE_HOME")
   def vscode_settings: Path = Path.variable("ISABELLE_VSCODE_SETTINGS")
+  def vscode_settings_user: Path = vscode_settings + Path.explode("user-data/User/settings.json")
   def vscode_version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION")
 
   def exe_path(dir: Path): Path = dir + Path.explode("bin/codium")
@@ -35,6 +36,22 @@
     (install_ok, install_dir)
   }
 
+  def init_settings(): Unit =
+  {
+    if (!vscode_settings_user.is_file) {
+      Isabelle_System.make_directory(vscode_settings_user.dir)
+      File.write(vscode_settings_user, """
+{
+  "editor.fontFamily": "'Isabelle DejaVu Sans Mono'",
+  "editor.fontSize": 18,
+  "editor.lineNumbers": "off",
+  "editor.renderIndentGuides": false,
+  "editor.rulers": [80, 100]
+}
+""".stripMargin)
+    }
+  }
+
 
   /* patch resources */
 
@@ -110,6 +127,8 @@
   {
     val (install_ok, install_dir) = vscode_installation(version, platform)
 
+    init_settings()
+
     if (check) {
       if (install_ok) progress.echo(install_dir.expand.implode)
       else {