# HG changeset patch
# User wenzelm
# Date 1441739423 -7200
# Node ID 4010e1559a2428af19b5ed50377e54e273e4752a
# Parent  168f84f457303911748f9b4373b08e26797777d4
more basic Windows path operations -- evade exception InvalidArc with Unicode;

diff -r 168f84f45730 -r 4010e1559a24 src/Pure/ML-Systems/windows_path.ML
--- a/src/Pure/ML-Systems/windows_path.ML	Tue Sep 08 20:06:17 2015 +0200
+++ b/src/Pure/ML-Systems/windows_path.ML	Tue Sep 08 21:10:23 2015 +0200
@@ -13,11 +13,10 @@
             (case Char.fromString drive of
               NONE => drive ^ ":"
             | SOME d => String.str (Char.toUpper d) ^ ":");
-        in OS.Path.toString {vol = vol, arcs = arcs, isAbs = true} end
+        in String.concatWith "\\" (vol :: arcs) end
     | arcs =>
         (case OS.Process.getEnv "CYGWIN_ROOT" of
-          SOME root =>
-            OS.Path.concat (root, OS.Path.toString {vol = "", arcs = arcs, isAbs = false})
+          SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
         | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
   else String.translate (fn #"/" => "\\" | c => String.str c) path;