# HG changeset patch
# User wenzelm
# Date 1603834477 -3600
# Node ID 460d743010bc570fdad6e26fc16fdea435026d8f
# Parent  a471730347e0c959fc27969676c35c9012e4db29
clarified signature: overloaded "+" for Path.append;

diff -r a471730347e0 -r 460d743010bc NEWS
--- a/NEWS	Mon Oct 26 21:35:39 2020 +0100
+++ b/NEWS	Tue Oct 27 22:34:37 2020 +0100
@@ -184,6 +184,9 @@
 registered Isabelle/Scala functions (of type String => String):
 invocation works via the PIDE protocol.
 
+* Path.append is available as overloaded "+" operator, similar to
+corresponding Isabelle/Scala operation.
+
 
 *** System ***
 
diff -r a471730347e0 -r 460d743010bc src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Library/code_test.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -140,7 +140,7 @@
 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)
 
 fun with_debug_dir name f =
-  Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
+  (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
   |> Isabelle_System.make_directory
   |> Exn.capture f
   |> Exn.release;
@@ -290,9 +290,9 @@
 
 fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir =
   let
-    val code_path = Path.append dir (Path.basic "generated.sml")
-    val driver_path = Path.append dir (Path.basic "driver.sml")
-    val out_path = Path.append dir (Path.basic "out")
+    val code_path = dir + Path.basic "generated.sml"
+    val driver_path = dir + Path.basic "driver.sml"
+    val out_path = dir + Path.basic "out"
 
     val code = #2 (the_single code_files)
     val driver = \<^verbatim>\<open>
@@ -337,9 +337,9 @@
     val driverN = "driver.sml"
     val projectN = "test"
 
-    val code_path = Path.append dir (Path.basic generatedN)
-    val driver_path = Path.append dir (Path.basic driverN)
-    val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb"))
+    val code_path = dir + Path.basic generatedN
+    val driver_path = dir + Path.basic driverN
+    val basis_path = dir + Path.basic (projectN ^ ".mlb")
     val driver = \<^verbatim>\<open>
 fun format (true, _) = \<close> ^ ML_Syntax.print_string success ^ \<^verbatim>\<open> ^ "\n"
   | format (false, NONE) = \<close> ^ ML_Syntax.print_string failure ^ \<^verbatim>\<open> ^ "\n"
@@ -355,7 +355,7 @@
     val _ = File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN)
   in
     compile compiler ("\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path);
-    evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN)))
+    evaluate compiler (File.bash_path (dir + Path.basic projectN))
   end
 
 
@@ -370,8 +370,8 @@
     val generatedN = "generated.sml"
     val driverN = "driver.sml"
 
-    val code_path = Path.append dir (Path.basic generatedN)
-    val driver_path = Path.append dir (Path.basic driverN)
+    val code_path = dir + Path.basic generatedN
+    val driver_path = dir + Path.basic driverN
     val driver = \<^verbatim>\<open>
 structure Test =
 struct
@@ -407,8 +407,8 @@
   let
     val compiler = ocamlN
 
-    val code_path = Path.append dir (Path.basic "generated.ml")
-    val driver_path = Path.append dir (Path.basic "driver.ml")
+    val code_path = dir + Path.basic "generated.ml"
+    val driver_path = dir + Path.basic "driver.ml"
     val driver =
       "let format_term = function\n" ^
       "  | None -> \"\"\n" ^
@@ -422,7 +422,7 @@
       "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
       "  print_string \"" ^ end_marker ^ "\";;\n" ^
       "main ();;"
-    val compiled_path = Path.append dir (Path.basic "test")
+    val compiled_path = dir + Path.basic "test"
 
     val _ = check_settings compiler ISABELLE_OCAMLFIND "ocamlfind executable"
     val _ = List.app (File.write code_path o snd) code_files
@@ -446,7 +446,7 @@
     val compiler = ghcN
     val modules = map fst code_files
 
-    val driver_path = Path.append dir (Path.basic "Main.hs")
+    val driver_path = dir + Path.basic "Main.hs"
     val driver =
       "module Main where {\n" ^
       implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
@@ -465,10 +465,10 @@
       "}\n"
 
     val _ = check_settings compiler ISABELLE_GHC "GHC executable"
-    val _ = List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files
+    val _ = List.app (fn (name, code) => File.write (dir + Path.basic name) code) code_files
     val _ = File.write driver_path driver
 
-    val compiled_path = Path.append dir (Path.basic "test")
+    val compiled_path = dir + Path.basic "test"
     val cmd =
       "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
       Config.get ctxt ghc_options ^ " -o " ^
@@ -487,9 +487,9 @@
     val generatedN = "Generated_Code"
     val driverN = "Driver.scala"
 
-    val code_path = Path.append dir (Path.basic (generatedN ^ ".scala"))
-    val driver_path = Path.append dir (Path.basic driverN)
-    val out_path = Path.append dir (Path.basic "out")
+    val code_path = dir + Path.basic (generatedN ^ ".scala")
+    val driver_path = dir + Path.basic driverN
+    val out_path = dir + Path.basic "out"
 
     val code = #2 (the_single code_files)
     val driver = \<^verbatim>\<open>
diff -r a471730347e0 -r 460d743010bc src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Tue Oct 27 22:34:37 2020 +0100
@@ -18,7 +18,7 @@
       (TPTP_Interpret.interpret_file
        false
        [Path.explode "$TPTP"]
-       (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
+       (tptp_probs_dir + Path.explode "LCL/LCL825-1.p")
        []
        [])
       @{theory}
diff -r a471730347e0 -r 460d743010bc src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -782,9 +782,9 @@
   | dest_fn_type ty = ([], ty)
 
 fun resolve_include_path path_prefixes path_suffix =
-  case find_first (fn prefix => File.exists (Path.append prefix path_suffix))
+  case find_first (fn prefix => File.exists (prefix + path_suffix))
          path_prefixes of
-    SOME prefix => Path.append prefix path_suffix
+    SOME prefix => prefix + path_suffix
   | NONE => error ("Cannot find include file " ^ Path.print path_suffix)
 
 fun is_type_type (Fmla_type (Atom (THF_Atom_term (Term_FuncG (TypeSymbol Type_Type, [], []))))) =
diff -r a471730347e0 -r 460d743010bc src/HOL/TPTP/TPTP_Test.thy
--- a/src/HOL/TPTP/TPTP_Test.thy	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy	Tue Oct 27 22:34:37 2020 +0100
@@ -89,7 +89,7 @@
 
 
 ML \<open>
-  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
+  fun situate file_name = tptp_probs_dir + Path.explode file_name;
 
   fun parser_test ctxt = (*FIXME argument order*)
     test_fn ctxt
diff -r a471730347e0 -r 460d743010bc src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -209,7 +209,7 @@
       {line = 0, file = "generated code", verbose = verbose, debug = false} code)
 
 fun with_overlord_dir name f =
-  Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
+  (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
   |> Isabelle_System.make_directory
   |> Exn.capture f
   |> Exn.release
@@ -258,7 +258,7 @@
               [(narrowing_engine_file,
                 if contains_existentials then pnf_narrowing_engine else narrowing_engine),
                (code_file, code), (main_file, main)])
-        val executable = Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")
+        val executable = in_path + Path.basic "isabelle_quickcheck_narrowing"
         val cmd =
           "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
             (space_implode " "
diff -r a471730347e0 -r 460d743010bc src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -234,8 +234,7 @@
 fun select_certificates name context = context |> Data.map (put_certs (
   if name = "" then NONE
   else
-    Path.explode name
-    |> Path.append (Resources.master_directory (Context.theory_of context))
+    (Resources.master_directory (Context.theory_of context) + Path.explode name)
     |> SOME o Cache_IO.unsynchronized_init))
 
 val setup_certificates =
diff -r a471730347e0 -r 460d743010bc src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -155,7 +155,7 @@
       if dest_dir = "" then
         File.tmp_path problem_file_name
       else if File.exists (Path.explode dest_dir) then
-        Path.append (Path.explode dest_dir) problem_file_name
+        Path.explode dest_dir + problem_file_name
       else
         error ("No such directory: " ^ quote dest_dir)
     val exec = exec full_proofs
diff -r a471730347e0 -r 460d743010bc src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/General/file.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -60,17 +60,16 @@
   let
     val path' = Path.expand path;
     val _ = Path.is_current path' andalso error "Bad file specification";
-    val path'' = Path.append dir path';
+    val path'' = dir + path';
   in
     if Path.is_absolute path'' then path''
-    else Path.append (Path.explode (ML_System.standard_path (OS.FileSys.getDir ()))) path''
+    else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path''
   end;
 
 
 (* tmp_path *)
 
-fun tmp_path path =
-  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
+fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path;
 
 
 (* directory entries *)
diff -r a471730347e0 -r 460d743010bc src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/General/path.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -294,3 +294,5 @@
 val explode = explode_path;
 
 end;
+
+ML_system_overload (uncurry Path.append) "+";
diff -r a471730347e0 -r 460d743010bc src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/General/url.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -32,10 +32,10 @@
 
 (* append *)
 
-fun append (File p) (File p') = File (Path.append p p')
-  | append (Http (h, p)) (File p') = Http (h, Path.append p p')
-  | append (Https (h, p)) (File p') = Https (h, Path.append p p')
-  | append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p')
+fun append (File p) (File p') = File (p + p')
+  | append (Http (h, p)) (File p') = Http (h, p + p')
+  | append (Https (h, p)) (File p') = Https (h, p + p')
+  | append (Ftp (h, p)) (File p') = Ftp (h, p + p')
   | append _ url = url;
 
 
@@ -67,7 +67,7 @@
   Scan.this_string "file:///" |-- scan_path_root >> File ||
   Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
   Scan.this_string "file://" |-- scan_host -- scan_path
-    >> (fn (h, p) => File (Path.append (Path.named_root h) p)) ||
+    >> (fn (h, p) => File (Path.named_root h + p)) ||
   Scan.this_string "file:/" |-- scan_path_root >> File ||
   Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
   Scan.this_string "https://" |-- scan_host -- scan_path >> Https ||
diff -r a471730347e0 -r 460d743010bc src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -155,7 +155,7 @@
     val dirs = Symtab.lookup_list (get_session_base #session_directories) session;
   in
     dirs |> get_first (fn dir =>
-      let val path = Path.append dir thy_file
+      let val path = dir + thy_file
       in if File.is_file path then SOME path else NONE end)
   end;
 
@@ -257,7 +257,7 @@
       (case opt_dir of
         SOME dir => dir
       | NONE => master_directory (Proof_Context.theory_of ctxt));
-    val path = Path.append dir (Path.explode name) handle ERROR msg => err msg;
+    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 _ = check_file path handle ERROR msg => err msg;
diff -r a471730347e0 -r 460d743010bc src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/System/isabelle_system.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -83,7 +83,7 @@
   let
     val src = Path.expand src0;
     val dst = Path.expand dst0;
-    val target = if File.is_dir dst then Path.append dst (Path.base src) else dst;
+    val target = if File.is_dir dst then dst + Path.base src else dst;
   in
     if File.eq (src, target) then ()
     else
@@ -97,7 +97,7 @@
     val _ =
       if Path.starts_basic src then ()
       else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
-  in copy_file (Path.append base_dir src) (make_directory (Path.append target_dir src_dir)) end;
+  in copy_file (base_dir + src) (make_directory (target_dir + src_dir)) end;
 
 
 (* tmp files *)
diff -r a471730347e0 -r 460d743010bc src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Thy/export.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -27,7 +27,7 @@
   let
     val theory_name = Context.theory_long_name thy;
     val (path, pos) = Path.dest_binding binding;
-    val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path));
+    val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
   in Context_Position.report_generic (Context.Theory thy) pos markup end;
 
 type params =
@@ -63,7 +63,7 @@
 
 fun markup thy path =
   let
-    val thy_path = Path.append (Path.basic (Context.theory_long_name thy)) path;
+    val thy_path = Path.basic (Context.theory_long_name thy) + path;
     val name = (Markup.nameN, Path.implode thy_path);
   in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;
 
diff -r a471730347e0 -r 460d743010bc src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Thy/present.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -205,7 +205,7 @@
     val script =
       "isabelle document -d " ^ File.bash_path dir ^ " -n " ^ Bash.string doc_name ^
       (if tags = "" then "" else " -t " ^ Bash.string tags);
-    val doc_path = Path.appends [dir, Path.parent, document_path doc_name];
+    val doc_path = dir + Path.parent + document_path doc_name;
     val _ = if verbose then writeln script else ();
     val {out, err, rc, ...} = Bash.process script;
     val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
@@ -219,7 +219,7 @@
 fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
 
 fun write_tex src name path =
-  File.write_buffer (Path.append path (tex_path name)) src;
+  File.write_buffer (path + tex_path name) src;
 
 fun write_tex_index tex_index path =
   write_tex (index_buffer tex_index) doc_indexN path;
@@ -231,16 +231,15 @@
     val {theories, tex_index, html_index} = Synchronized.value browser_info;
     val thys = Symtab.dest theories;
 
-    val session_prefix =
-      Path.append (Path.append info_path (Path.basic chapter)) (Path.basic name);
+    val session_prefix = info_path + Path.basic chapter + Path.basic name;
 
     fun finish_html (a, {html_source, ...}: theory_info) =
-      File.write (Path.append session_prefix (html_path a)) html_source;
+      File.write (session_prefix + html_path a) html_source;
 
     val _ =
       if info then
        (Isabelle_System.make_directory session_prefix;
-        File.write_buffer (Path.append session_prefix index_path)
+        File.write_buffer (session_prefix + index_path)
           (index_buffer html_index |> Buffer.add HTML.end_document);
         (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
         List.app finish_html thys;
@@ -251,15 +250,15 @@
 
     fun document_job doc_prefix backdrop (doc_name, tags) =
       let
-        val doc_dir = Path.append doc_prefix (Path.basic doc_name);
+        val doc_dir = doc_prefix + Path.basic doc_name;
         fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else ();
         val _ = purge ();
         val _ = Isabelle_System.make_directory doc_dir;
         val _ =
           Isabelle_System.bash ("isabelle latex -o sty " ^
-            File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
+            File.bash_path (doc_dir + Path.basic "root.tex"));
         val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
-        val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
+        val _ = Isabelle_System.copy_file graph_file (doc_dir + session_graph_path);
         val _ = write_tex_index tex_index doc_dir;
         val _ =
           List.app (fn (a, {tex_source, ...}) =>
@@ -303,9 +302,9 @@
   in
     if curr_session = session then SOME link
     else if curr_chapter = chapter then
-      SOME (Path.appends [Path.parent, Path.basic session, link])
+      SOME (Path.parent + Path.basic session + link)
     else if chapter = Context.PureN then NONE
-    else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
+    else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link)
   end;
 
 fun begin_theory bibtex_entries update_time mk_text thy =
diff -r a471730347e0 -r 460d743010bc src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -67,7 +67,7 @@
         else
           let
             val thy_name = Context.theory_name thy;
-            val document_path = Path.append (Path.basic "document") (Present.tex_path thy_name);
+            val document_path = Path.basic "document" + Present.tex_path thy_name;
 
             val latex = Latex.isabelle_body thy_name body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
@@ -416,7 +416,7 @@
                   Position.here require_pos ^ required_by "\n" initiators);
 
           val qualifier' = Resources.theory_qualifier theory_name;
-          val dir' = Path.append dir (master_dir_deps (Option.map #1 deps));
+          val dir' = dir + master_dir_deps (Option.map #1 deps);
 
           val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
           val (parents_current, tasks') =
diff -r a471730347e0 -r 460d743010bc src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Tools/generated_files.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -146,7 +146,7 @@
 
 fun write_file dir (file: file) =
   let
-    val path = Path.expand (Path.append dir (#path file));
+    val path = Path.expand (dir + #path file);
     val _ = Isabelle_System.make_directory (Path.dir path);
     val _ = File.generate path (#content file);
   in () end;
@@ -298,7 +298,7 @@
               val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
               val (path, pos) = Path.dest_binding binding;
               val content =
-                (case try File.read (Path.append dir path) of
+                (case try File.read (dir + path) of
                   SOME context => context
                 | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
               val _ = Export.report_export thy export_prefix;
diff -r a471730347e0 -r 460d743010bc src/Pure/Tools/ghc.ML
--- a/src/Pure/Tools/ghc.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Tools/ghc.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -81,7 +81,7 @@
 
 fun new_project dir {name, depends, modules} =
   let
-    val template_path = Path.append dir (Path.basic name |> Path.ext "hsfiles");
+    val template_path = dir + (Path.basic name |> Path.ext "hsfiles");
     val _ = File.write template_path (project_template {depends = depends, modules = modules});
     val {rc, err, ...} =
       Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
diff -r a471730347e0 -r 460d743010bc src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Tools/Code/code_ml.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -879,14 +879,14 @@
   (Code_Target.add_language
     (target_SML, {serializer = serializer_sml, literals = literals_sml,
       check = {env_var = "",
-        make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
+        make_destination = fn p => p + Path.explode "ROOT.ML",
         make_command = fn _ =>
           "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"},
       evaluation_args = []})
   #> Code_Target.add_language
     (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
       check = {env_var = "ISABELLE_OCAMLFIND",
-        make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
+        make_destination = fn p => p + Path.explode "ROOT.ml"
           (*extension demanded by OCaml compiler*),
         make_command = fn _ =>
           "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"},
diff -r a471730347e0 -r 460d743010bc src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Tools/Code/code_scala.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -465,7 +465,7 @@
   (Code_Target.add_language
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "SCALA_HOME",
-        make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
+        make_destination = fn p => p + Path.explode "ROOT.scala",
         make_command = fn _ =>
           "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"},
       evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"})
diff -r a471730347e0 -r 460d743010bc src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -304,7 +304,7 @@
       Singleton (ext, p) => export (binding (Path.ext ext prefix)) (format p)
     | Hierarchy modules =>
         fold (fn (names, p) =>
-          export (binding (Path.append prefix (Path.make names))) (format p)) modules)
+          export (binding (prefix + Path.make names)) (format p)) modules)
     #> tap code_export_message
   end;