clarified bash process -- similar to ML version;
authorwenzelm
Sat, 13 Feb 2016 20:41:56 +0100
changeset 62296 b04a5ddd6121
parent 62295 4f2fb9adfae5
child 62297 b886c0946308
clarified bash process -- similar to ML version;
src/Pure/Concurrent/bash.scala
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/system_channel.scala
src/Tools/jEdit/src/isabelle_logic.scala
--- 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"))