# HG changeset patch # User wenzelm # Date 1645909134 -3600 # Node ID d67ec542b5b54aa3e95febe243a446321e1fb895 # Parent 09da7b15162b12239c457c9b79372386c9e3aafb clarified default settings; diff -r 09da7b15162b -r d67ec542b5b5 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 {