# HG changeset patch
# User wenzelm
# Date 1601928445 -7200
# Node ID 04bce347868838e88426f0b2fa500861ae2ad58f
# Parent  e48d93811ed77ac1770fb4f67f3b294d9a5caf56
clarified signature;

diff -r e48d93811ed7 -r 04bce3478688 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Mon Oct 05 22:07:25 2020 +0200
@@ -140,11 +140,10 @@
 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)
 
 fun with_debug_dir name f =
-  let
-    val dir =
-      Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
-    val _ = Isabelle_System.make_directory dir
-  in Exn.release (Exn.capture f dir) end
+  Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
+  |> Isabelle_System.make_directory
+  |> Exn.capture f
+  |> Exn.release;
 
 fun dynamic_value_strict ctxt t compiler =
   let
diff -r e48d93811ed7 -r 04bce3478688 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 05 22:07:25 2020 +0200
@@ -209,11 +209,10 @@
       {line = 0, file = "generated code", verbose = verbose, debug = false} code)
 
 fun with_overlord_dir name f =
-  let
-    val path =
-      Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
-    val _ = Isabelle_System.make_directory path
-  in Exn.release (Exn.capture f path) end
+  Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
+  |> Isabelle_System.make_directory
+  |> Exn.capture f
+  |> Exn.release
 
 fun elapsed_time description e =
   let val ({elapsed, ...}, result) = Timing.timing e ()
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/build_cygwin.scala
--- a/src/Pure/Admin/build_cygwin.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/build_cygwin.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -24,8 +24,7 @@
       {
         val cygwin = tmp_dir + Path.explode("cygwin")
         val cygwin_etc = cygwin + Path.explode("etc")
-        val cygwin_isabelle = cygwin + Path.explode("isabelle")
-        Isabelle_System.make_directory(cygwin_isabelle)
+        val cygwin_isabelle = Isabelle_System.make_directory(cygwin + Path.explode("isabelle"))
 
         val cygwin_exe_name = mirror + "/setup-x86_64.exe"
         val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe")
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/build_e.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -43,8 +43,7 @@
         proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
           .getOrElse(error("No 64bit platform"))
 
-      val platform_dir = component_dir + Path.basic(platform_name)
-      Isabelle_System.make_directory(platform_dir)
+      val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
 
 
       /* runepar.pl */
@@ -111,8 +110,7 @@
 
       /* settings */
 
-      val etc_dir = component_dir + Path.basic("etc")
-      Isabelle_System.make_directory(etc_dir)
+      val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
       File.write(etc_dir + Path.basic("settings"),
         """# -*- shell-script -*- :mode=shellscript:
 
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/build_fonts.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -307,8 +307,7 @@
 
     // etc/settings
 
-    val settings_path = Components.settings(target_dir)
-    Isabelle_System.make_directory(settings_path.dir)
+    val settings_path = Isabelle_System.make_directory(Components.settings(target_dir))
 
     def fonts_settings(hinted: Boolean): String =
       "\n  isabelle_fonts \\\n" +
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/build_jdk.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -94,8 +94,7 @@
   def extract_archive(dir: Path, archive: Path): (String, JDK_Platform) =
   {
     try {
-      val tmp_dir = dir + Path.explode("tmp")
-      Isabelle_System.make_directory(tmp_dir)
+      val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp"))
 
       if (archive.get_ext == "zip") {
         Isabelle_System.bash(
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -241,8 +241,7 @@
 
     File.copy(Path.explode("~~/Admin/polyml/README"), component_dir)
 
-    val etc_dir = component_dir + Path.explode("etc")
-    Isabelle_System.make_directory(etc_dir)
+    val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
     File.copy(Path.explode("~~/Admin/polyml/settings"), etc_dir)
 
     sha1_root match {
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/build_release.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -117,8 +117,7 @@
   def make_news(other_isabelle: Other_Isabelle, dist_version: String)
   {
     val target = other_isabelle.isabelle_home + Path.explode("doc")
-    val target_fonts = target + Path.explode("fonts")
-    Isabelle_System.make_directory(target_fonts)
+    val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts"))
     other_isabelle.copy_fonts(target_fonts)
 
     HTML.write_document(target, "NEWS.html",
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/build_sqlite.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -43,8 +43,7 @@
 
     /* settings */
 
-    val etc_dir = component_dir + Path.basic("etc")
-    Isabelle_System.make_directory(etc_dir)
+    val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
 
     File.write(etc_dir + Path.basic("settings"),
 """# -*- shell-script -*- :mode=shellscript:
@@ -76,8 +75,7 @@
           "org/sqlite/native/Windows/x86_64/sqlitejdbc.dll" -> "x86_64-windows")
 
       for ((file, dir) <- jar_files) {
-        val target = component_dir + Path.explode(dir)
-        Isabelle_System.make_directory(target)
+        val target = Isabelle_System.make_directory(component_dir + Path.explode(dir))
         File.copy(jar_dir + Path.explode(file), target)
       }
 
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/build_status.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -397,8 +397,7 @@
 
       progress.echo("output " + quote(data_name))
 
-      val dir = target_dir + Path.basic(clean_name(data_name))
-      Isabelle_System.make_directory(dir)
+      val dir = Isabelle_System.make_directory(target_dir + Path.basic(clean_name(data_name)))
 
       val data_files =
         (for (session <- data_entry.sessions) yield {
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -474,9 +474,8 @@
       log(end_date, msg)
     }
 
-    val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
+    val log_dir = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date))
 
-    Isabelle_System.make_directory(log_dir)
     log(start_date, "started")
   }
 
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/General/ssh.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -378,12 +378,15 @@
       try { sftp.lstat(remote_path(path)).isLink }
       catch { case _: SftpException => false }
 
-    override def make_directory(path: Path): Unit =
+    override def make_directory(path: Path): Path =
+    {
       if (!is_dir(path)) {
         execute(
           "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
         if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
       }
+      path
+    }
 
     def read_dir(path: Path): List[Dir_Entry] =
     {
@@ -494,7 +497,7 @@
     def bash_path(path: Path): String = File.bash_path(path)
     def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file
-    def make_directory(path: Path): Unit = Isabelle_System.make_directory(path)
+    def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
 
     def execute(command: String,
         progress_stdout: String => Unit = (_: String) => (),
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/System/isabelle_system.ML	Mon Oct 05 22:07:25 2020 +0200
@@ -12,7 +12,7 @@
   val bash_functions: unit -> string list
   val check_bash_function: Proof.context -> string * Position.T -> string
   val rm_tree: Path.T -> unit
-  val make_directory: Path.T -> unit
+  val make_directory: Path.T -> Path.T
   val mkdir: Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
   val copy_file: Path.T -> Path.T -> unit
@@ -64,10 +64,13 @@
 fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
 
 fun make_directory path =
-  if File.is_dir path then ()
-  else
-   (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\"");
-    if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path));
+  let
+    val _ =
+      if File.is_dir path then ()
+      else
+       (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\"");
+        if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path));
+  in path end;
 
 fun mkdir path =
   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
@@ -94,8 +97,7 @@
     val _ =
       if Path.starts_basic src then ()
       else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
-    val _ = make_directory (Path.append target_dir src_dir);
-  in copy_file (Path.append base_dir src) (Path.append target_dir src) end;
+  in copy_file (Path.append base_dir src) (make_directory (Path.append target_dir src_dir)) end;
 
 
 (* tmp files *)
@@ -115,9 +117,7 @@
 (* tmp dirs *)
 
 fun with_tmp_dir name f =
-  let
-    val path = create_tmp_path name "";
-    val _ = make_directory path;
-  in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
+  let val path = create_tmp_path name ""
+  in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
 
 end;
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -189,11 +189,14 @@
 
   /* directories */
 
-  def make_directory(path: Path): Unit =
+  def make_directory(path: Path): Path =
+  {
     if (!path.is_dir) {
       bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"")
       if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
     }
+    path
+  }
 
   def copy_dir(dir1: Path, dir2: Path): Unit =
     bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Thy/html.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -383,11 +383,8 @@
       fonts_css(make_url) + "\n\n" + File.read(isabelle_css))
   }
 
-  def init_dir(dir: Path)
-  {
-    Isabelle_System.make_directory(dir)
-    write_isabelle_css(dir)
-  }
+  def init_dir(dir: Path): Unit =
+    write_isabelle_css(Isabelle_System.make_directory(dir))
 
   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
     css: String = isabelle_css.file_name,
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Thy/present.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -36,8 +36,7 @@
 
   def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
   {
-    val dir = browser_info + Path.basic(chapter)
-    Isabelle_System.make_directory(dir)
+    val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter))
 
     val sessions0 =
       try { read_sessions(dir) }
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Tools/build.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -413,9 +413,8 @@
 
       if (result1.ok) {
         for (document_output <- proper_string(options.string("document_output"))) {
-          val document_output_dir = info.dir + Path.explode(document_output)
-          Isabelle_System.make_directory(document_output_dir)
-
+          val document_output_dir =
+            Isabelle_System.make_directory(info.dir + Path.explode(document_output))
           val base = deps(session_name)
           File.write(document_output_dir + Path.explode("session.tex"),
             base.session_theories.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString)
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Tools/phabricator.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -482,8 +482,7 @@
 
     progress.echo("\nPHP daemon setup ...")
 
-    val phd_log_path = Path.explode("/var/tmp/phd")
-    Isabelle_System.make_directory(phd_log_path)
+    val phd_log_path = Isabelle_System.make_directory(Path.explode("/var/tmp/phd"))
     Isabelle_System.chown(
       "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path)
     Isabelle_System.chmod("755", phd_log_path)
diff -r e48d93811ed7 -r 04bce3478688 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/Pure/Tools/scala_project.scala	Mon Oct 05 22:07:25 2020 +0200
@@ -73,8 +73,7 @@
 
     val src_dir = project_dir + Path.explode("src/main/scala")
     val java_src_dir = project_dir + Path.explode("src/main/java")
-    val scala_src_dir = project_dir + Path.explode("src/main/scala")
-    Isabelle_System.make_directory(scala_src_dir)
+    val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala"))
 
     Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir)