--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Tue Oct 18 15:31:08 2016 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Tue Oct 18 16:03:30 2016 +0200
@@ -53,7 +53,7 @@
fun make_cmd command options problem_path proof_path =
space_implode " "
- ("(exec 2>&1;" :: map File.bash_string (command () @ options) @
+ ("(exec 2>&1;" :: map Bash.string (command () @ options) @
[File.bash_path problem_path, ")", ">", File.bash_path proof_path])
fun trace_and ctxt msg f x =
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 18 15:31:08 2016 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 18 16:03:30 2016 +0200
@@ -1028,7 +1028,7 @@
val outcome =
let
val code =
- Isabelle_System.bash ("cd " ^ File.bash_string temp_dir ^ ";\n\
+ Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
\\"$KODKODI/bin/kodkodi\"" ^
(if ms >= 0 then " -max-msecs " ^ string_of_int ms
else "") ^
--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 18 15:31:08 2016 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 18 16:03:30 2016 +0200
@@ -49,7 +49,7 @@
local
fun make_command command options problem_path proof_path =
- "(exec 2>&1;" :: map File.bash_string (command () @ options) @
+ "(exec 2>&1;" :: map Bash.string (command () @ options) @
[File.bash_path problem_path, ")", ">", File.bash_path proof_path]
|> space_implode " "
--- a/src/Pure/Admin/build_history.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/Admin/build_history.scala Tue Oct 18 16:03:30 2016 +0200
@@ -190,7 +190,7 @@
val build_start = Date.now()
val build_args1 = List("-v", "-j" + processes) ::: build_args
val build_result =
- other_isabelle("build " + File.bash_args(build_args1), redirect = true, echo = verbose)
+ other_isabelle("build " + Bash.strings(build_args1), redirect = true, echo = verbose)
val build_end = Date.now()
val log_path =
@@ -373,7 +373,7 @@
options: String = "",
args: String = ""): List[(String, Bytes)] =
{
- val isabelle_admin = ssh.remote_path(isabelle_repos_self + Path.explode("Admin"))
+ val isabelle_admin = ssh.bash_path(isabelle_repos_self + Path.explode("Admin"))
/* prepare repository clones */
@@ -384,19 +384,19 @@
if (self_update) {
isabelle_hg.pull()
isabelle_hg.update(clean = true)
- ssh.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check
+ ssh.execute(Bash.string(isabelle_admin + "/build") + " jars_fresh").check
}
Mercurial.setup_repository(
- ssh.remote_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
+ ssh.bash_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
/* Admin/build_history */
val result =
ssh.execute(
- File.bash_string(isabelle_admin + "/build_history") + " " + options + " " +
- File.bash_string(ssh.remote_path(isabelle_repos_other)) + " " + args,
+ Bash.string(isabelle_admin + "/build_history") + " " + options + " " +
+ ssh.bash_path(isabelle_repos_other) + " " + args,
progress_stderr = progress.echo(_)).check
for (line <- result.out_lines; log = Path.explode(line))
--- a/src/Pure/Admin/build_release.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/Admin/build_release.scala Tue Oct 18 16:03:30 2016 +0200
@@ -76,8 +76,8 @@
progress.bash(
"isabelle makedist -d " + File.bash_path(base_dir) + jobs_option +
(if (official_release) " -O" else "") +
- (if (release_name != "") " -r " + File.bash_string(release_name) else "") +
- (if (rev != "") " " + File.bash_string(rev) else ""),
+ (if (release_name != "") " -r " + Bash.string(release_name) else "") +
+ (if (rev != "") " " + Bash.string(rev) else ""),
echo = true).check
}
Library.trim_line(File.read(isabelle_ident_file))
@@ -98,8 +98,8 @@
progress.echo("\nApplication bundle for " + platform_family + ": " + bundle_archive.implode)
progress.bash(
"isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) +
- " " + File.bash_string(platform_family) +
- (if (remote_mac == "") "" else " " + File.bash_string(remote_mac)),
+ " " + Bash.string(platform_family) +
+ (if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
echo = true).check
}
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 18 16:03:30 2016 +0200
@@ -123,8 +123,7 @@
isabelle_repos_source = isabelle_dev_source,
self_update = !r.shared_home,
options =
- r.options + " -f -r " + File.bash_string(rev) +
- " -N " + File.bash_string(task_name),
+ r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
args = r.args)
for ((log, bytes) <- results)
Bytes.write(logger.log_dir + Path.explode(log), bytes)
--- a/src/Pure/Admin/other_isabelle.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/Admin/other_isabelle.scala Tue Oct 18 16:03:30 2016 +0200
@@ -16,7 +16,7 @@
def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
progress.bash(
- "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
+ "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" + script,
env = null, cwd = isabelle_home.file, redirect = redirect)
def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
--- a/src/Pure/Admin/remote_dmg.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/Admin/remote_dmg.scala Tue Oct 18 16:03:30 2016 +0200
@@ -13,13 +13,13 @@
{
ssh.with_tmp_dir(remote_dir =>
{
- val cd = "cd " + File.bash_string(ssh.remote_path(remote_dir)) + "; "
+ val cd = "cd " + ssh.bash_path(remote_dir) + "; "
ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
ssh.execute(
cd + "hdiutil create -srcfolder root" +
- (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
+ (if (volume_name == "") "" else " -volname " + Bash.string(volume_name)) +
" dmg.dmg").check
ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
})
--- a/src/Pure/General/file.ML Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/General/file.ML Tue Oct 18 16:03:30 2016 +0200
@@ -8,8 +8,6 @@
sig
val standard_path: Path.T -> string
val platform_path: Path.T -> string
- val bash_string: string -> string
- val bash_args: string list -> string
val bash_path: Path.T -> string
val full_path: Path.T -> Path.T -> Path.T
val tmp_path: Path.T -> Path.T
@@ -46,26 +44,7 @@
val standard_path = Path.implode o Path.expand;
val platform_path = ML_System.platform_path o standard_path;
-fun bash_string "" = "\"\""
- | bash_string str =
- str |> translate_string (fn ch =>
- let val c = ord ch in
- (case ch of
- "\t" => "$'\\t'"
- | "\n" => "$'\\n'"
- | "\f" => "$'\\f'"
- | "\r" => "$'\\r'"
- | _ =>
- if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
- exists_string (fn c => c = ch) "-./:_" then ch
- else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
- else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
- else "\\" ^ ch)
- end);
-
-val bash_args = space_implode " " o map bash_string;
-
-val bash_path = bash_string o standard_path;
+val bash_path = Bash_Syntax.string o standard_path;
(* full_path *)
--- a/src/Pure/General/file.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/General/file.scala Tue Oct 18 16:03:30 2016 +0200
@@ -108,33 +108,8 @@
/* bash path */
- private def bash_chr(c: Byte): String =
- {
- val ch = c.toChar
- ch match {
- case '\t' => "$'\\t'"
- case '\n' => "$'\\n'"
- case '\f' => "$'\\f'"
- case '\r' => "$'\\r'"
- case _ =>
- if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
- Symbol.ascii(ch)
- else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
- else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
- else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
- else "\\" + ch
- }
- }
-
- def bash_string(s: String): String =
- if (s == "") "\"\""
- else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
-
- def bash_args(args: List[String]): String =
- args.iterator.map(bash_string(_)).mkString(" ")
-
- def bash_path(path: Path): String = bash_string(standard_path(path))
- def bash_path(file: JFile): String = bash_string(standard_path(file))
+ def bash_path(path: Path): String = Bash.string(standard_path(path))
+ def bash_path(file: JFile): String = Bash.string(standard_path(file))
/* directory entries */
--- a/src/Pure/General/mercurial.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/General/mercurial.scala Tue Oct 18 16:03:30 2016 +0200
@@ -16,7 +16,7 @@
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
- if (s == "") "" else " " + prefix + " " + File.bash_string(s)
+ if (s == "") "" else " " + prefix + " " + Bash.string(s)
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
def opt_rev(s: String): String = optional(s, "--rev")
@@ -40,7 +40,7 @@
case None => Isabelle_System.mkdirs(hg.root.dir)
case Some(ssh) => ssh.mkdirs(hg.root.dir)
}
- hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
+ hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root), options).check
hg
}
--- a/src/Pure/General/ssh.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/General/ssh.scala Tue Oct 18 16:03:30 2016 +0200
@@ -243,6 +243,7 @@
}
def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
+ def bash_path(path: Path): String = Bash.string(remote_path(path))
def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2))
@@ -324,7 +325,7 @@
/* tmp dirs */
def rm_tree(remote_dir: String): Unit =
- execute("rm -r -f " + File.bash_string(remote_dir)).check
+ execute("rm -r -f " + Bash.string(remote_dir)).check
def tmp_dir(): String =
execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
--- a/src/Pure/ROOT.ML Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/ROOT.ML Tue Oct 18 16:03:30 2016 +0200
@@ -67,6 +67,7 @@
ML_file "PIDE/xml.ML";
ML_file "General/path.ML";
ML_file "General/url.ML";
+ML_file "System/bash_syntax.ML";
ML_file "General/file.ML";
ML_file "General/long_name.ML";
ML_file "General/binding.ML";
--- a/src/Pure/System/bash.ML Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/System/bash.ML Tue Oct 18 16:03:30 2016 +0200
@@ -6,6 +6,8 @@
signature BASH =
sig
+ val string: string -> string
+ val strings: string list -> string
val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
end;
@@ -14,6 +16,9 @@
structure Bash: BASH =
struct
+val string = Bash_Syntax.string;
+val strings = Bash_Syntax.strings;
+
val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
@@ -105,6 +110,9 @@
structure Bash: BASH =
struct
+val string = Bash_Syntax.string;
+val strings = Bash_Syntax.strings;
+
val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
--- a/src/Pure/System/bash.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/System/bash.scala Tue Oct 18 16:03:30 2016 +0200
@@ -13,6 +13,36 @@
object Bash
{
+ /* concrete syntax */
+
+ private def bash_chr(c: Byte): String =
+ {
+ val ch = c.toChar
+ ch match {
+ case '\t' => "$'\\t'"
+ case '\n' => "$'\\n'"
+ case '\f' => "$'\\f'"
+ case '\r' => "$'\\r'"
+ case _ =>
+ if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
+ Symbol.ascii(ch)
+ else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
+ else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
+ else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
+ else "\\" + ch
+ }
+ }
+
+ def string(s: String): String =
+ if (s == "") "\"\""
+ else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
+
+ def strings(ss: List[String]): String =
+ ss.iterator.map(Bash.string(_)).mkString(" ")
+
+
+ /* process and result */
+
private class Limited_Progress(proc: Process, progress_limit: Option[Long])
{
private var count = 0L
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash_syntax.ML Tue Oct 18 16:03:30 2016 +0200
@@ -0,0 +1,35 @@
+(* Title: Pure/System/bash_syntax.ML
+ Author: Makarius
+
+Syntax for GNU bash (see also Pure/System/bash.ML).
+*)
+
+signature BASH_SYNTAX =
+sig
+ val string: string -> string
+ val strings: string list -> string
+end;
+
+structure Bash_Syntax: BASH_SYNTAX =
+struct
+
+fun string "" = "\"\""
+ | string str =
+ str |> translate_string (fn ch =>
+ let val c = ord ch in
+ (case ch of
+ "\t" => "$'\\t'"
+ | "\n" => "$'\\n'"
+ | "\f" => "$'\\f'"
+ | "\r" => "$'\\r'"
+ | _ =>
+ if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
+ exists_string (fn c => c = ch) "-./:_" then ch
+ else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else "\\" ^ ch)
+ end);
+
+val strings = space_implode " " o map string;
+
+end;
--- a/src/Pure/System/isabelle_system.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Oct 18 16:03:30 2016 +0200
@@ -318,7 +318,7 @@
def hostname(): String = bash("hostname -s").check.out
def open(arg: String): Unit =
- bash("exec \"$ISABELLE_OPEN\" " + File.bash_string(arg) + " >/dev/null 2>/dev/null &")
+ bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
def pdf_viewer(arg: Path): Unit =
bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
--- a/src/Pure/System/isabelle_tool.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala Tue Oct 18 16:03:30 2016 +0200
@@ -89,7 +89,7 @@
(args: List[String]) =>
{
val tool = dir + Path.basic(name)
- val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
+ val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
sys.exit(result.print_stdout.rc)
}
})
--- a/src/Pure/Tools/ml_process.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala Tue Oct 18 16:03:30 2016 +0200
@@ -107,7 +107,7 @@
Bash.process(
"exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
- File.bash_args(bash_args),
+ Bash.strings(bash_args),
cwd = cwd,
env =
Isabelle_System.library_path(env ++ env_options ++ env_tmp,