# HG changeset patch
# User wenzelm
# Date 1457371222 -3600
# Node ID 8ebffdaf2ce2580690fe24ab3301f43b8717afb0
# Parent  efa178abe023a38fc2a6d8fd871d7a4698a2a60b
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
more robust File.bash_escape;
more robust treatment of ML_OPTIONS;
clarified prover args (again);

diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -26,20 +26,21 @@
     }
   }
 
-  def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
-    new Process(cwd, env, redirect, args:_*)
+  def process(script: String,
+      cwd: JFile = null, env: Map[String, String] = null, redirect: Boolean = false): Process =
+    new Process(script, cwd, env, redirect)
 
   class Process private [Bash](
-      cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
+      script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
     extends Prover.System_Process
   {
+    val script_file = Isabelle_System.tmp_file("bash_script")
+    File.write(script_file, script)
+
     private val proc =
-    {
-      val params =
-        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", "bash")
-      Isabelle_System.process(
-        cwd, Isabelle_System.settings(env), redirect, (params ::: args.toList):_*)
-    }
+      Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
+        File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
+          "bash", File.standard_path(script_file))
 
 
     // channels
@@ -90,14 +91,20 @@
     try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
     catch { case _: IllegalStateException => }
 
-    private def cleanup() =
+
+    /* join */
+
+    def join: Int =
+    {
+      val rc = proc.waitFor
+
       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
       catch { case _: IllegalStateException => }
 
+      script_file.delete
 
-    /* join */
-
-    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
+      rc
+    }
 
 
     /* result */
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/General/file.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -101,11 +101,34 @@
   }
 
 
-  /* shell path (bash) */
+  /* bash path */
 
-  def shell_quote(s: String): String = "'" + s + "'"
-  def shell_path(path: Path): String = shell_quote(standard_path(path))
-  def shell_path(file: JFile): String = shell_quote(standard_path(file))
+  private def bash_escape(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) "$'\\x" + Integer.toHexString(c) + "'"
+        else  "\\" + ch
+    }
+  }
+
+  def bash_escape(s: String): String =
+    UTF8.bytes(s).iterator.map(bash_escape(_)).mkString
+
+  def bash_escape(args: List[String]): String =
+    args.iterator.map(bash_escape(_)).mkString(" ")
+
+  def bash_path(path: Path): String = bash_escape(standard_path(path))
+  def bash_path(file: JFile): String = bash_escape(standard_path(file))
 
 
   /* directory entries */
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/PIDE/batch_session.scala
--- a/src/Pure/PIDE/batch_session.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/PIDE/batch_session.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -58,7 +58,7 @@
         case _ =>
       }
 
-    prover_session.start("Isabelle", "-q " + quote(parent_session))
+    prover_session.start("Isabelle", List("-q", parent_session))
 
     batch_session
   }
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/PIDE/resources.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -136,7 +136,7 @@
 
   /* prover process */
 
-  def start_prover(receiver: Prover.Message => Unit, name: String, args: String): Prover =
+  def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
     Isabelle_Process(receiver, args)
 }
 
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/PIDE/session.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -212,7 +212,7 @@
 
   /* internal messages */
 
-  private case class Start(name: String, args: String)
+  private case class Start(name: String, args: List[String])
   private case object Stop
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
@@ -601,7 +601,7 @@
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
     global_state.value.snapshot(name, pending_edits)
 
-  def start(name: String, args: String)
+  def start(name: String, args: List[String])
   { manager.send(Start(name, args)) }
 
   def stop()
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -11,16 +11,14 @@
 {
   def apply(
     receiver: Prover.Message => Unit = Console.println(_),
-    prover_args: String = ""): Isabelle_Process =
+    prover_args: List[String] = Nil): Isabelle_Process =
   {
     val system_channel = System_Channel()
     val system_process =
       try {
-        val script =
-          File.shell_quote(Isabelle_System.getenv_strict("ISABELLE_PROCESS")) +
-            " -P " + system_channel.server_name +
-            (if (prover_args == "") "" else " " + prover_args)
-        val process = Bash.process(null, null, false, "-c", script)
+        val process =
+          Bash.process("\"$ISABELLE_PROCESS\" -P " + File.bash_escape(system_channel.server_name) +
+            " " + File.bash_escape(prover_args))
         process.stdin.close
         process
       }
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -167,7 +167,7 @@
 
   def mkdirs(path: Path): Unit =
     if (!path.is_dir) {
-      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
+      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)))
     }
 
@@ -308,11 +308,7 @@
     progress_limit: Option[Long] = None,
     strict: Boolean = true): Process_Result =
   {
-    with_tmp_file("isabelle_script") { script_file =>
-      File.write(script_file, script)
-      Bash.process(cwd, env, false, File.standard_path(script_file)).
-        result(progress_stdout, progress_stderr, progress_limit, strict)
-    }
+    Bash.process(script, cwd, env).result(progress_stdout, progress_stderr, progress_limit, strict)
   }
 
 
@@ -342,7 +338,7 @@
     bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
 
   def hg(cmd_line: String, cwd: Path = Path.current): Process_Result =
-    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
+    bash("cd " + File.bash_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
 
 
 
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -66,13 +66,18 @@
     // options
     val isabelle_process_options = Isabelle_System.tmp_file("options")
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
-    val bash_env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
+    val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = List("Options.load_default ()")
 
     val eval_process =
       if (process_socket == "") Nil
       else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket))
 
+    // bash
+    val bash_args =
+      Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
+      (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process).
+        map(eval => List("--eval", eval)).flatten ::: args
     val bash_script =
       """
         [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
@@ -83,7 +88,7 @@
         chmod $(umask -S) "$ISABELLE_TMP"
 
         librarypath "$ML_HOME"
-        "$ML_HOME/poly" -q -i $ML_OPTIONS "$@"
+        "$ML_HOME/poly" -q -i """ + File.bash_escape(bash_args) + """
         RC="$?"
 
         rm -f "$ISABELLE_PROCESS_OPTIONS"
@@ -92,11 +97,6 @@
         exit "$RC"
       """
 
-    val bash_args =
-      List("-c", bash_script, "ml_process") :::
-      (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process).
-        map(eval => List("--eval", eval)).flatten ::: args
-
-    Bash.process(null, bash_env, false, bash_args:_*)
+    Bash.process(bash_script, env = env)
   }
 }
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Pure/Tools/check_sources.scala
--- a/src/Pure/Tools/check_sources.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/Tools/check_sources.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -41,7 +41,7 @@
   def check_hg(root: Path)
   {
     Output.writeln("Checking " + root + " ...")
-    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
+    Isabelle_System.hg("--repository " + File.bash_path(root) + " root").check
     for {
       file <- Isabelle_System.hg("manifest", root).check.out_lines
       if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
diff -r efa178abe023 -r 8ebffdaf2ce2 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -69,12 +69,11 @@
       dirs = session_dirs(), sessions = List(session_name()))
   }
 
-  def session_args(): String =
+  def session_args(): List[String] =
   {
-    val print_modes =
-      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
-       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).map("-m " + _)
-    (print_modes ::: List("-q", File.shell_quote(session_name()))).mkString(" ")
+    (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
+     space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).
+      map(m => List("-m", m)).flatten ::: List("-q", session_name())
   }
 
   def session_start(): Unit = PIDE.session.start("Isabelle", session_args())