# HG changeset patch
# User wenzelm
# Date 1648034473 -3600
# Node ID 5960bae73afe4907572a89cd73026af955ff12fd
# Parent  42baf7ffa088697a562ff39d2a57fb91129e3467
tuned;

diff -r 42baf7ffa088 -r 5960bae73afe src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Wed Mar 23 12:15:25 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Wed Mar 23 12:21:13 2022 +0100
@@ -14,8 +14,6 @@
 {
   /* vscodium command-line interface */
 
-  private def platform_path(s: String): String = File.platform_path(Path.explode(s))
-
   def server_log_path: Path =
     Path.explode("$ISABELLE_VSCODE_SETTINGS/server.log").expand
 
@@ -34,6 +32,8 @@
     background: Boolean = false,
     progress: Progress = new Progress): Process_Result =
   {
+    def platform_path(s: String): String = File.platform_path(Path.explode(s))
+
     val args_json =
       JSON.optional("options" -> proper_list(options)) ++
       JSON.optional("logic" -> proper_string(logic)) ++