--- a/src/Doc/Codegen/Evaluation.thy Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Doc/Codegen/Evaluation.thy Mon Oct 05 21:15:58 2020 +0200
@@ -3,7 +3,7 @@
begin (*<*)
ML \<open>
- Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
+ Isabelle_System.make_directory (File.tmp_path (Path.basic "examples"))
\<close> (*>*)
section \<open>Evaluation \label{sec:evaluation}\<close>
--- a/src/Doc/Codegen/Introduction.thy Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Doc/Codegen/Introduction.thy Mon Oct 05 21:15:58 2020 +0200
@@ -3,7 +3,7 @@
begin (*<*)
ML \<open>
- Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
+ Isabelle_System.make_directory (File.tmp_path (Path.basic "examples"))
\<close> (*>*)
section \<open>Introduction\<close>
--- a/src/HOL/Library/code_test.ML Sat Oct 03 23:01:40 2020 +0100
+++ b/src/HOL/Library/code_test.ML Mon Oct 05 21:15:58 2020 +0200
@@ -143,7 +143,7 @@
let
val dir =
Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
- val _ = Isabelle_System.mkdirs dir
+ val _ = Isabelle_System.make_directory dir
in Exn.release (Exn.capture f dir) end
fun dynamic_value_strict ctxt t compiler =
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Oct 03 23:01:40 2020 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Oct 05 21:15:58 2020 +0200
@@ -212,7 +212,7 @@
let
val path =
Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
- val _ = Isabelle_System.mkdirs path
+ val _ = Isabelle_System.make_directory path
in Exn.release (Exn.capture f path) end
fun elapsed_time description e =
--- a/src/Pure/Admin/build_cygwin.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_cygwin.scala Mon Oct 05 21:15:58 2020 +0200
@@ -25,7 +25,7 @@
val cygwin = tmp_dir + Path.explode("cygwin")
val cygwin_etc = cygwin + Path.explode("etc")
val cygwin_isabelle = cygwin + Path.explode("isabelle")
- Isabelle_System.mkdirs(cygwin_isabelle)
+ Isabelle_System.make_directory(cygwin_isabelle)
val cygwin_exe_name = mirror + "/setup-x86_64.exe"
val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe")
--- a/src/Pure/Admin/build_e.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_e.scala Mon Oct 05 21:15:58 2020 +0200
@@ -36,7 +36,7 @@
if (component_dir.is_dir) error("Component directory already exists: " + component_dir)
else {
progress.echo("Component " + component_dir)
- Isabelle_System.mkdirs(component_dir)
+ Isabelle_System.make_directory(component_dir)
}
val platform_name =
@@ -44,7 +44,7 @@
.getOrElse(error("No 64bit platform"))
val platform_dir = component_dir + Path.basic(platform_name)
- Isabelle_System.mkdirs(platform_dir)
+ Isabelle_System.make_directory(platform_dir)
/* runepar.pl */
@@ -112,7 +112,7 @@
/* settings */
val etc_dir = component_dir + Path.basic("etc")
- Isabelle_System.mkdirs(etc_dir)
+ Isabelle_System.make_directory(etc_dir)
File.write(etc_dir + Path.basic("settings"),
"""# -*- shell-script -*- :mode=shellscript:
--- a/src/Pure/Admin/build_fonts.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_fonts.scala Mon Oct 05 21:15:58 2020 +0200
@@ -219,7 +219,7 @@
progress: Progress = new Progress)
{
progress.echo("Directory " + target_dir)
- hinting.foreach(hinted => Isabelle_System.mkdirs(target_dir + hinted_path(hinted)))
+ hinting.foreach(hinted => Isabelle_System.make_directory(target_dir + hinted_path(hinted)))
val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))
for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
@@ -308,7 +308,7 @@
// etc/settings
val settings_path = Components.settings(target_dir)
- Isabelle_System.mkdirs(settings_path.dir)
+ Isabelle_System.make_directory(settings_path.dir)
def fonts_settings(hinted: Boolean): String =
"\n isabelle_fonts \\\n" +
--- a/src/Pure/Admin/build_history.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_history.scala Mon Oct 05 21:15:58 2020 +0200
@@ -221,7 +221,7 @@
}
Isabelle_System.rm_tree(isabelle_output)
- Isabelle_System.mkdirs(isabelle_output)
+ Isabelle_System.make_directory(isabelle_output)
val log_path =
other_isabelle.isabelle_home_user +
@@ -229,7 +229,7 @@
Build_Log.log_filename(Build_History.engine, build_history_date,
List(build_host, ml_platform, "M" + threads) ::: build_tags)
- Isabelle_System.mkdirs(log_path.dir)
+ Isabelle_System.make_directory(log_path.dir)
val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
val build_out_progress = new File_Progress(build_out)
--- a/src/Pure/Admin/build_jdk.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_jdk.scala Mon Oct 05 21:15:58 2020 +0200
@@ -95,7 +95,7 @@
{
try {
val tmp_dir = dir + Path.explode("tmp")
- Isabelle_System.mkdirs(tmp_dir)
+ Isabelle_System.make_directory(tmp_dir)
if (archive.get_ext == "zip") {
Isabelle_System.bash(
@@ -160,7 +160,7 @@
val jdk_path = Path.explode(jdk_name)
val component_dir = dir + jdk_path
- Isabelle_System.mkdirs(component_dir + Path.explode("etc"))
+ Isabelle_System.make_directory(component_dir + Path.explode("etc"))
File.write(Components.settings(component_dir), settings)
File.write(component_dir + Path.explode("README"), readme(version))
--- a/src/Pure/Admin/build_log.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_log.scala Mon Oct 05 21:15:58 2020 +0200
@@ -898,7 +898,7 @@
def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path,
days: Int = 100, ml_statistics: Boolean = false)
{
- Isabelle_System.mkdirs(sqlite_database.dir)
+ Isabelle_System.make_directory(sqlite_database.dir)
sqlite_database.file.delete
using(SQLite.open_database(sqlite_database))(db2 =>
--- a/src/Pure/Admin/build_polyml.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_polyml.scala Mon Oct 05 21:15:58 2020 +0200
@@ -143,7 +143,7 @@
val target = Path.explode(polyml_platform)
Isabelle_System.rm_tree(target)
- Isabelle_System.mkdirs(target)
+ Isabelle_System.make_directory(target)
for (file <- info.copy_files ::: ldd_files ::: sha1_files)
File.copy(Path.explode(file).expand_env(settings), target)
@@ -236,13 +236,13 @@
if (component_dir.is_file || component_dir.is_dir)
error("Component directory already exists: " + component_dir)
- Isabelle_System.mkdirs(component_dir)
+ Isabelle_System.make_directory(component_dir)
extract_sources(source_archive, component_dir)
File.copy(Path.explode("~~/Admin/polyml/README"), component_dir)
val etc_dir = component_dir + Path.explode("etc")
- Isabelle_System.mkdirs(etc_dir)
+ Isabelle_System.make_directory(etc_dir)
File.copy(Path.explode("~~/Admin/polyml/settings"), etc_dir)
sha1_root match {
--- a/src/Pure/Admin/build_release.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_release.scala Mon Oct 05 21:15:58 2020 +0200
@@ -118,7 +118,7 @@
{
val target = other_isabelle.isabelle_home + Path.explode("doc")
val target_fonts = target + Path.explode("fonts")
- Isabelle_System.mkdirs(target_fonts)
+ Isabelle_System.make_directory(target_fonts)
other_isabelle.copy_fonts(target_fonts)
HTML.write_document(target, "NEWS.html",
@@ -201,7 +201,7 @@
def make_contrib(dir: Path)
{
- Isabelle_System.mkdirs(Components.contrib(dir))
+ Isabelle_System.make_directory(Components.contrib(dir))
File.write(Components.contrib(dir, "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
@@ -324,7 +324,7 @@
else {
progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
- Isabelle_System.mkdirs(release.dist_dir)
+ Isabelle_System.make_directory(release.dist_dir)
if (release.isabelle_dir.is_dir)
error("Directory " + release.isabelle_dir + " already exists")
@@ -749,7 +749,7 @@
val other_isabelle = release.other_isabelle(tmp_dir)
- Isabelle_System.mkdirs(other_isabelle.etc)
+ Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
--- a/src/Pure/Admin/build_sqlite.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_sqlite.scala Mon Oct 05 21:15:58 2020 +0200
@@ -30,7 +30,7 @@
if (component_dir.is_dir) error("Component directory already exists: " + component_dir)
else {
progress.echo("Component " + component_dir)
- Isabelle_System.mkdirs(component_dir)
+ Isabelle_System.make_directory(component_dir)
}
@@ -44,7 +44,7 @@
/* settings */
val etc_dir = component_dir + Path.basic("etc")
- Isabelle_System.mkdirs(etc_dir)
+ Isabelle_System.make_directory(etc_dir)
File.write(etc_dir + Path.basic("settings"),
"""# -*- shell-script -*- :mode=shellscript:
@@ -77,7 +77,7 @@
for ((file, dir) <- jar_files) {
val target = component_dir + Path.explode(dir)
- Isabelle_System.mkdirs(target)
+ Isabelle_System.make_directory(target)
File.copy(jar_dir + Path.explode(file), target)
}
--- a/src/Pure/Admin/build_status.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/build_status.scala Mon Oct 05 21:15:58 2020 +0200
@@ -398,7 +398,7 @@
progress.echo("output " + quote(data_name))
val dir = target_dir + Path.basic(clean_name(data_name))
- Isabelle_System.mkdirs(dir)
+ Isabelle_System.make_directory(dir)
val data_files =
(for (session <- data_entry.sessions) yield {
--- a/src/Pure/Admin/components.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/components.scala Mon Oct 05 21:15:58 2020 +0200
@@ -58,7 +58,7 @@
copy_dir: Option[Path] = None,
progress: Progress = new Progress)
{
- Isabelle_System.mkdirs(base_dir)
+ Isabelle_System.make_directory(base_dir)
for (name <- names) {
val archive_name = Archive(name)
val archive = base_dir + Path.explode(archive_name)
@@ -68,7 +68,7 @@
Bytes.write(archive, Url.read_bytes(Url(remote)))
}
for (dir <- copy_dir) {
- Isabelle_System.mkdirs(dir)
+ Isabelle_System.make_directory(dir)
File.copy(archive, dir)
}
unpack(target_dir getOrElse base_dir, archive, progress = progress)
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Oct 05 21:15:58 2020 +0200
@@ -476,7 +476,7 @@
val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
- Isabelle_System.mkdirs(log_dir)
+ Isabelle_System.make_directory(log_dir)
log(start_date, "started")
}
--- a/src/Pure/Admin/jenkins.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/jenkins.scala Mon Oct 05 21:15:58 2020 +0200
@@ -103,7 +103,7 @@
if (!log_path.is_file) {
progress.echo(log_path.expand.implode)
- Isabelle_System.mkdirs(log_dir)
+ Isabelle_System.make_directory(log_dir)
val ml_statistics =
session_logs.map(_._1).distinct.sorted.flatMap(session_name =>
--- a/src/Pure/Admin/other_isabelle.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Mon Oct 05 21:15:58 2020 +0200
@@ -96,7 +96,7 @@
if (!clean_settings())
error("Cannot proceed with existing user settings file: " + etc_settings)
- Isabelle_System.mkdirs(etc_settings.dir)
+ Isabelle_System.make_directory(etc_settings.dir)
File.write(etc_settings,
"# generated by Isabelle " + Date.now() + "\n" +
"#-*- shell-script -*- :mode=shellscript:\n" +
--- a/src/Pure/General/completion.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/General/completion.scala Mon Oct 05 21:15:58 2020 +0200
@@ -105,7 +105,7 @@
def save()
{
- Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
+ Isabelle_System.make_directory(COMPLETION_HISTORY.dir)
File.write_backup(COMPLETION_HISTORY,
{
import XML.Encode._
--- a/src/Pure/General/mercurial.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/General/mercurial.scala Mon Oct 05 21:15:58 2020 +0200
@@ -56,7 +56,7 @@
: Repository =
{
val hg = new Repository(root, ssh)
- ssh.mkdirs(hg.root.dir)
+ ssh.make_directory(hg.root.dir)
hg.command(cmd, args, repository = false).check
hg
}
@@ -234,7 +234,7 @@
{
/* local repository */
- Isabelle_System.mkdirs(local_path)
+ Isabelle_System.make_directory(local_path)
val repos_name =
proper_string(remote_name) getOrElse local_path.absolute.base.implode
--- a/src/Pure/General/ssh.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/General/ssh.scala Mon Oct 05 21:15:58 2020 +0200
@@ -378,7 +378,7 @@
try { sftp.lstat(remote_path(path)).isLink }
catch { case _: SftpException => false }
- override def mkdirs(path: Path): Unit =
+ override def make_directory(path: Path): Unit =
if (!is_dir(path)) {
execute(
"perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
@@ -494,7 +494,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 mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
+ def make_directory(path: Path): Unit = Isabelle_System.make_directory(path)
def execute(command: String,
progress_stdout: String => Unit = (_: String) => (),
--- a/src/Pure/System/isabelle_system.ML Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/System/isabelle_system.ML Mon Oct 05 21:15:58 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 mkdirs: Path.T -> unit
+ val make_directory: Path.T -> unit
val mkdir: Path.T -> unit
val copy_dir: Path.T -> Path.T -> unit
val copy_file: Path.T -> Path.T -> unit
@@ -63,7 +63,7 @@
fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
-fun mkdirs 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 ^ "');\"");
@@ -94,7 +94,7 @@
val _ =
if Path.starts_basic src then ()
else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
- val _ = mkdirs (Path.append target_dir src_dir);
+ val _ = make_directory (Path.append target_dir src_dir);
in copy_file (Path.append base_dir src) (Path.append target_dir src) end;
@@ -117,7 +117,7 @@
fun with_tmp_dir name f =
let
val path = create_tmp_path name "";
- val _ = mkdirs path;
+ val _ = make_directory path;
in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
end;
--- a/src/Pure/System/isabelle_system.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala Mon Oct 05 21:15:58 2020 +0200
@@ -189,7 +189,7 @@
/* directories */
- def mkdirs(path: Path): Unit =
+ def make_directory(path: Path): Unit =
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)))
@@ -204,7 +204,7 @@
def isabelle_tmp_prefix(): JFile =
{
val path = Path.explode("$ISABELLE_TMP_PREFIX")
- path.file.mkdirs // low-level mkdirs
+ path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment
File.platform_file(path)
}
--- a/src/Pure/System/options.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/System/options.scala Mon Oct 05 21:15:58 2020 +0200
@@ -403,7 +403,7 @@
changed.sortBy(_._1)
.map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
- Isabelle_System.mkdirs(file.dir)
+ Isabelle_System.make_directory(file.dir)
File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs)
}
}
--- a/src/Pure/Thy/export.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Thy/export.scala Mon Oct 05 21:15:58 2020 +0200
@@ -336,7 +336,7 @@
else export_dir + Path.make(elems.drop(export_prune))
progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
- Isabelle_System.mkdirs(path.dir)
+ Isabelle_System.make_directory(path.dir)
Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
File.set_executable(path, entry.executable)
}
--- a/src/Pure/Thy/html.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Thy/html.scala Mon Oct 05 21:15:58 2020 +0200
@@ -385,7 +385,7 @@
def init_dir(dir: Path)
{
- Isabelle_System.mkdirs(dir)
+ Isabelle_System.make_directory(dir)
write_isabelle_css(dir)
}
--- a/src/Pure/Thy/present.ML Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Thy/present.ML Mon Oct 05 21:15:58 2020 +0200
@@ -239,7 +239,7 @@
val _ =
if info then
- (Isabelle_System.mkdirs session_prefix;
+ (Isabelle_System.make_directory session_prefix;
File.write_buffer (Path.append 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);
@@ -254,7 +254,7 @@
val doc_dir = Path.append doc_prefix (Path.basic doc_name);
fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else ();
val _ = purge ();
- val _ = Isabelle_System.mkdirs doc_dir;
+ 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")));
--- a/src/Pure/Thy/present.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Thy/present.scala Mon Oct 05 21:15:58 2020 +0200
@@ -37,7 +37,7 @@
def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
{
val dir = browser_info + Path.basic(chapter)
- Isabelle_System.mkdirs(dir)
+ Isabelle_System.make_directory(dir)
val sessions0 =
try { read_sessions(dir) }
@@ -64,7 +64,7 @@
def make_global_index(browser_info: Path)
{
if (!(browser_info + Path.explode("index.html")).is_file) {
- Isabelle_System.mkdirs(browser_info)
+ Isabelle_System.make_directory(browser_info)
File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
browser_info + Path.explode("isabelle.gif"))
File.write(browser_info + Path.explode("index.html"),
@@ -88,7 +88,7 @@
val session_fonts = session_prefix + Path.explode("fonts")
if (info.options.bool("browser_info")) {
- Isabelle_System.mkdirs(session_fonts)
+ Isabelle_System.make_directory(session_fonts)
val session_graph = session_prefix + Path.basic("session_graph.pdf")
File.copy(graph_file, session_graph.file)
--- a/src/Pure/Thy/sessions.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Oct 05 21:15:58 2020 +0200
@@ -1132,7 +1132,7 @@
def output_log(name: String): Path = output_dir + log(name)
def output_log_gz(name: String): Path = output_dir + log_gz(name)
- def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
+ def prepare_output_dir() { Isabelle_System.make_directory(output_dir + Path.basic("log")) }
/* heap */
--- a/src/Pure/Tools/build.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Tools/build.scala Mon Oct 05 21:15:58 2020 +0200
@@ -414,7 +414,7 @@
if (result1.ok) {
for (document_output <- proper_string(options.string("document_output"))) {
val document_output_dir = info.dir + Path.explode(document_output)
- Isabelle_System.mkdirs(document_output_dir)
+ Isabelle_System.make_directory(document_output_dir)
val base = deps(session_name)
File.write(document_output_dir + Path.explode("session.tex"),
--- a/src/Pure/Tools/dump.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Tools/dump.scala Mon Oct 05 21:15:58 2020 +0200
@@ -24,7 +24,7 @@
def write_path(file_name: Path): Path =
{
val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
- Isabelle_System.mkdirs(path.dir)
+ Isabelle_System.make_directory(path.dir)
path
}
--- a/src/Pure/Tools/generated_files.ML Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Tools/generated_files.ML Mon Oct 05 21:15:58 2020 +0200
@@ -147,7 +147,7 @@
fun write_file dir (file: file) =
let
val path = Path.expand (Path.append dir (#path file));
- val _ = Isabelle_System.mkdirs (Path.dir path);
+ val _ = Isabelle_System.make_directory (Path.dir path);
val _ = File.generate path (#content file);
in () end;
--- a/src/Pure/Tools/main.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Tools/main.scala Mon Oct 05 21:15:58 2020 +0200
@@ -53,7 +53,7 @@
if (props1 != props2) File.write(properties, cat_lines(props2))
}
- Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
+ Isabelle_System.make_directory(settings_dir + Path.explode("DockableWindowManager"))
if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
--- a/src/Pure/Tools/mkroot.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Tools/mkroot.scala Mon Oct 05 21:15:58 2020 +0200
@@ -27,7 +27,7 @@
author: String = "",
progress: Progress = new Progress)
{
- Isabelle_System.mkdirs(session_dir)
+ Isabelle_System.make_directory(session_dir)
val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC")
@@ -67,7 +67,7 @@
{
progress.echo(" creating " + root_tex)
- Isabelle_System.mkdirs(root_tex.dir)
+ Isabelle_System.make_directory(root_tex.dir)
File.write(root_tex,
"""\documentclass[11pt,a4paper]{article}
--- a/src/Pure/Tools/phabricator.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Tools/phabricator.scala Mon Oct 05 21:15:58 2020 +0200
@@ -483,7 +483,7 @@
progress.echo("\nPHP daemon setup ...")
val phd_log_path = Path.explode("/var/tmp/phd")
- Isabelle_System.mkdirs(phd_log_path)
+ Isabelle_System.make_directory(phd_log_path)
Isabelle_System.chown(
"-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path)
Isabelle_System.chmod("755", phd_log_path)
--- a/src/Pure/Tools/scala_project.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Tools/scala_project.scala Mon Oct 05 21:15:58 2020 +0200
@@ -74,7 +74,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.mkdirs(scala_src_dir)
+ Isabelle_System.make_directory(scala_src_dir)
Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir)
@@ -87,7 +87,7 @@
(Path.explode("~~") + Path.explode(file), scala_src_dir + p)
}).getOrElse(error("Unknown directory prefix for " + quote(file)))
- Isabelle_System.mkdirs(target)
+ Isabelle_System.make_directory(target)
if (symlinks) File.link(path, target) else File.copy(path, target)
}
--- a/src/Pure/Tools/spell_checker.scala Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Pure/Tools/spell_checker.scala Mon Oct 05 21:15:58 2020 +0200
@@ -175,7 +175,7 @@
#:mode=text:encoding=UTF-8:
"""
- Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
+ Isabelle_System.make_directory(dictionary.user_path.expand.dir)
File.write(dictionary.user_path, header + cat_lines(permanent_decls))
}
}
--- a/src/Tools/Code/code_target.ML Sat Oct 03 23:01:40 2020 +0100
+++ b/src/Tools/Code/code_target.ML Mon Oct 05 21:15:58 2020 +0200
@@ -312,7 +312,7 @@
(case pretty_modules of
Singleton (_, p) => File.write root (format p)
| Hierarchy code_modules =>
- (Isabelle_System.mkdirs root;
+ (Isabelle_System.make_directory root;
List.app (fn (names, p) =>
File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));