--- a/src/Pure/Concurrent/bash.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala Sat Feb 13 20:41:56 2016 +0100
@@ -40,8 +40,9 @@
extends Prover.System_Process
{
private val params =
- List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
- private val proc = Isabelle_System.execute_env(cwd, env, redirect, (params ::: args.toList):_*)
+ List(Isabelle_System.getenv_strict("ISABELLE_BASH_PROCESS"), "-", "bash")
+ private val proc =
+ Isabelle_System.execute_env(cwd, env, redirect, (params ::: args.toList):_*)
// channels
--- a/src/Pure/PIDE/batch_session.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Pure/PIDE/batch_session.scala Sat Feb 13 20:41:56 2016 +0100
@@ -58,7 +58,7 @@
case _ =>
}
- prover_session.start("Isabelle", List("-r", "-q", parent_session))
+ prover_session.start("Isabelle", "-r -q " + quote(parent_session))
batch_session
}
--- a/src/Pure/PIDE/resources.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Feb 13 20:41:56 2016 +0100
@@ -136,7 +136,7 @@
/* prover process */
- def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
+ def start_prover(receiver: Prover.Message => Unit, name: String, args: String): Prover =
Isabelle_Process(receiver, args)
}
--- a/src/Pure/PIDE/session.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Pure/PIDE/session.scala Sat Feb 13 20:41:56 2016 +0100
@@ -212,7 +212,7 @@
/* internal messages */
- private case class Start(name: String, args: List[String])
+ private case class Start(name: String, args: 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: List[String])
+ def start(name: String, args: String)
{ manager.send(Start(name, args)) }
def stop()
--- a/src/Pure/System/isabelle_process.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala Sat Feb 13 20:41:56 2016 +0100
@@ -11,15 +11,15 @@
{
def apply(
receiver: Prover.Message => Unit = Console.println(_),
- prover_args: List[String] = Nil): Isabelle_Process =
+ prover_args: String = ""): Isabelle_Process =
{
val system_channel = System_Channel()
val system_process =
try {
- val cmdline =
- Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
- (system_channel.prover_args ::: prover_args)
- val process = Bash.process(null, null, false, cmdline: _*)
+ val script =
+ "\"$ISABELLE_PROCESS\" " + system_channel.prover_options +
+ (if (prover_args == "") "" else " " + prover_args)
+ val process = Bash.process(null, null, false, "-c", script)
process.stdin.close
process
}
--- a/src/Pure/System/isabelle_system.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Feb 13 20:41:56 2016 +0100
@@ -324,7 +324,7 @@
{
with_tmp_file("isabelle_script") { script_file =>
File.write(script_file, script)
- val proc = Bash.process(cwd, env, false, "bash", File.standard_path(script_file))
+ val proc = Bash.process(cwd, env, false, File.standard_path(script_file))
proc.stdin.close
val limited = new Limited_Progress(proc, progress_limit)
--- a/src/Pure/System/system_channel.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Pure/System/system_channel.scala Sat Feb 13 20:41:56 2016 +0100
@@ -22,7 +22,7 @@
def params: List[String] = List("127.0.0.1", server.getLocalPort.toString)
- def prover_args: List[String] = List("-P", "127.0.0.1:" + server.getLocalPort)
+ def prover_options: String = "-P 127.0.0.1:" + server.getLocalPort
def rendezvous(): (OutputStream, InputStream) =
{
--- a/src/Tools/jEdit/src/isabelle_logic.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Sat Feb 13 20:41:56 2016 +0100
@@ -72,9 +72,10 @@
def session_start()
{
val print_modes =
- space_explode(',', PIDE.options.string("jedit_print_mode")) :::
- space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))
- PIDE.session.start("Isabelle", print_modes.map("-m" + _) ::: List("-r", "-q", session_name()))
+ (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
+ space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).map("-m " + _)
+ val args = (print_modes ::: List("-r", "-q", quote(session_name()))).mkString(" ")
+ PIDE.session.start("Isabelle", args)
}
def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))