# HG changeset patch # User wenzelm # Date 1476799410 -7200 # Node ID 96bc94c87a81b1607d512e4b94944d7f224c9616 # Parent 605351c7ef970a4bd8c0b05699cdb7092da7f934 clarified modules; diff -r 605351c7ef97 -r 96bc94c87a81 src/HOL/Library/Old_SMT/old_smt_solver.ML --- 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 = diff -r 605351c7ef97 -r 96bc94c87a81 src/HOL/Tools/Nitpick/kodkod.ML --- 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 "") ^ diff -r 605351c7ef97 -r 96bc94c87a81 src/HOL/Tools/SMT/smt_solver.ML --- 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 " " diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/Admin/build_history.scala --- 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)) diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/Admin/build_release.scala --- 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 } } diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/Admin/isabelle_cronjob.scala --- 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) diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/Admin/other_isabelle.scala --- 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 = diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/Admin/remote_dmg.scala --- 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) }) diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/General/file.ML --- 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 *) diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/General/file.scala --- 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 */ diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/General/mercurial.scala --- 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 } diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/General/ssh.scala --- 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 diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/ROOT.ML --- 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"; diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/System/bash.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; diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/System/bash.scala --- 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 diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/System/bash_syntax.ML --- /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; diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/System/isabelle_system.scala --- 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 &") diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/System/isabelle_tool.scala --- 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) } }) diff -r 605351c7ef97 -r 96bc94c87a81 src/Pure/Tools/ml_process.scala --- 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,