src/Pure/PIDE/resources.ML

 
 fun begin_theory master_dir {name, imports, keywords} parents =
   let
     val thy =
       Theory.begin_theory name parents
-      |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, []))
+      |> map_files (fn _ => (Path.explode (File.symbolic_path master_dir), imports, []))
       |> Thy_Header.add_keywords keywords;
     val ctxt = Proof_Context.init_global thy;
     val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords;
   in thy end;
 

         SOME path => check_file Path.current path
       | NONE => check_file dir (thy_path (Path.basic thy_base_name)));
     val text = File.read master_file;
 
     val {name = (name, pos), imports, keywords} =
-      Thy_Header.read (Position.file (Path.implode_symbolic master_file)) text;
+      Thy_Header.read (Position.file (File.symbolic_path master_file)) text;
     val _ =
       thy_base_name <> name andalso
         error ("Bad theory name " ^ quote name ^
           " for file " ^ Path.print (Path.base master_file) ^ Position.here pos);
   in

   let
     fun read_local () =
       let
         val path = File.check_file (File.full_path master_dir src_path);
         val text = File.read path;
-        val file_pos = Position.file (Path.implode_symbolic path);
+        val file_pos = Position.file (File.symbolic_path path);
       in (text, file_pos) end;
 
     fun read_remote () =
       let
         val text = Bytes.content (Isabelle_System.download file_node);

       val pos = Input.pos_of source;
       val delimited = Input.is_delimited source;
       val src_paths = make_paths (Path.explode name);
       val reports =
         src_paths |> maps (fn src_path =>
-          [(pos, Markup.path (Path.implode_symbolic (master_dir + src_path))),
+          [(pos, Markup.path (File.symbolic_path (master_dir + src_path))),
            (pos, Markup.language_path delimited)]);
       val _ = Position.reports reports;
     in map (read_file master_dir o rpair pos) src_paths end
   else map Exn.release files;
 

       (case opt_dir of
         SOME dir => dir
       | NONE => master_directory (Proof_Context.theory_of ctxt));
     val path = dir + Path.explode name handle ERROR msg => err msg;
     val _ = Path.expand path handle ERROR msg => err msg;
-    val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
+    val _ = Context_Position.report ctxt pos (Markup.path (File.symbolic_path path));
     val _ = check path handle ERROR msg => err msg;
   in path end;
 
 val check_path = formal_check I;
 val check_file = formal_check File.check_file;