# HG changeset patch
# User wenzelm
# Date 1548855623 -3600
# Node ID da0d533d7f309ed5137fd69f9349b4fd1470bb97
# Parent  1907222d974e95e7686a82188e7ea3c5a2a4affb
tuned;

diff -r 1907222d974e -r da0d533d7f30 src/Tools/jEdit/src/isabelle_vfs.scala
--- a/src/Tools/jEdit/src/isabelle_vfs.scala	Wed Jan 30 14:35:15 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_vfs.scala	Wed Jan 30 14:40:23 2019 +0100
@@ -37,10 +37,8 @@
 {
   /* URL structure */
 
-  def separator: Char = '/'
-
-  def explode_name(s: String): List[String] = space_explode(separator, s)
-  def implode_name(elems: Iterable[String]): String = elems.mkString(separator.toString)
+  def explode_name(s: String): List[String] = space_explode(getFileSeparator, s)
+  def implode_name(elems: Iterable[String]): String = elems.mkString(getFileSeparator.toString)
 
   def explode_url(url: String, component: Component = null): Option[List[String]] =
   {
@@ -56,8 +54,8 @@
   override def constructPath(parent: String, path: String): String =
   {
     if (parent == "") path
-    else if (parent(parent.length - 1) == separator || parent == prefix) parent + path
-    else parent + separator + path
+    else if (parent(parent.length - 1) == getFileSeparator || parent == prefix) parent + path
+    else parent + getFileSeparator + path
   }