clarified bash process -- similar to ML version;
authorwenzelm
Sat Feb 13 20:41:56 2016 +0100 (2016-02-13)
changeset 62296b04a5ddd6121
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
     1.1 --- a/src/Pure/Concurrent/bash.scala	Sat Feb 13 20:01:48 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.scala	Sat Feb 13 20:41:56 2016 +0100
     1.3 @@ -40,8 +40,9 @@
     1.4      extends Prover.System_Process
     1.5    {
     1.6      private val params =
     1.7 -      List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
     1.8 -    private val proc = Isabelle_System.execute_env(cwd, env, redirect, (params ::: args.toList):_*)
     1.9 +      List(Isabelle_System.getenv_strict("ISABELLE_BASH_PROCESS"), "-", "bash")
    1.10 +    private val proc =
    1.11 +      Isabelle_System.execute_env(cwd, env, redirect, (params ::: args.toList):_*)
    1.12  
    1.13  
    1.14      // channels
     2.1 --- a/src/Pure/PIDE/batch_session.scala	Sat Feb 13 20:01:48 2016 +0100
     2.2 +++ b/src/Pure/PIDE/batch_session.scala	Sat Feb 13 20:41:56 2016 +0100
     2.3 @@ -58,7 +58,7 @@
     2.4          case _ =>
     2.5        }
     2.6  
     2.7 -    prover_session.start("Isabelle", List("-r", "-q", parent_session))
     2.8 +    prover_session.start("Isabelle", "-r -q " + quote(parent_session))
     2.9  
    2.10      batch_session
    2.11    }
     3.1 --- a/src/Pure/PIDE/resources.scala	Sat Feb 13 20:01:48 2016 +0100
     3.2 +++ b/src/Pure/PIDE/resources.scala	Sat Feb 13 20:41:56 2016 +0100
     3.3 @@ -136,7 +136,7 @@
     3.4  
     3.5    /* prover process */
     3.6  
     3.7 -  def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
     3.8 +  def start_prover(receiver: Prover.Message => Unit, name: String, args: String): Prover =
     3.9      Isabelle_Process(receiver, args)
    3.10  }
    3.11  
     4.1 --- a/src/Pure/PIDE/session.scala	Sat Feb 13 20:01:48 2016 +0100
     4.2 +++ b/src/Pure/PIDE/session.scala	Sat Feb 13 20:41:56 2016 +0100
     4.3 @@ -212,7 +212,7 @@
     4.4  
     4.5    /* internal messages */
     4.6  
     4.7 -  private case class Start(name: String, args: List[String])
     4.8 +  private case class Start(name: String, args: String)
     4.9    private case object Stop
    4.10    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    4.11    private case class Protocol_Command(name: String, args: List[String])
    4.12 @@ -601,7 +601,7 @@
    4.13        pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
    4.14      global_state.value.snapshot(name, pending_edits)
    4.15  
    4.16 -  def start(name: String, args: List[String])
    4.17 +  def start(name: String, args: String)
    4.18    { manager.send(Start(name, args)) }
    4.19  
    4.20    def stop()
     5.1 --- a/src/Pure/System/isabelle_process.scala	Sat Feb 13 20:01:48 2016 +0100
     5.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Feb 13 20:41:56 2016 +0100
     5.3 @@ -11,15 +11,15 @@
     5.4  {
     5.5    def apply(
     5.6      receiver: Prover.Message => Unit = Console.println(_),
     5.7 -    prover_args: List[String] = Nil): Isabelle_Process =
     5.8 +    prover_args: String = ""): Isabelle_Process =
     5.9    {
    5.10      val system_channel = System_Channel()
    5.11      val system_process =
    5.12        try {
    5.13 -        val cmdline =
    5.14 -          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
    5.15 -            (system_channel.prover_args ::: prover_args)
    5.16 -        val process = Bash.process(null, null, false, cmdline: _*)
    5.17 +        val script =
    5.18 +          "\"$ISABELLE_PROCESS\" " + system_channel.prover_options +
    5.19 +            (if (prover_args == "") "" else " " + prover_args)
    5.20 +        val process = Bash.process(null, null, false, "-c", script)
    5.21          process.stdin.close
    5.22          process
    5.23        }
     6.1 --- a/src/Pure/System/isabelle_system.scala	Sat Feb 13 20:01:48 2016 +0100
     6.2 +++ b/src/Pure/System/isabelle_system.scala	Sat Feb 13 20:41:56 2016 +0100
     6.3 @@ -324,7 +324,7 @@
     6.4    {
     6.5      with_tmp_file("isabelle_script") { script_file =>
     6.6        File.write(script_file, script)
     6.7 -      val proc = Bash.process(cwd, env, false, "bash", File.standard_path(script_file))
     6.8 +      val proc = Bash.process(cwd, env, false, File.standard_path(script_file))
     6.9        proc.stdin.close
    6.10  
    6.11        val limited = new Limited_Progress(proc, progress_limit)
     7.1 --- a/src/Pure/System/system_channel.scala	Sat Feb 13 20:01:48 2016 +0100
     7.2 +++ b/src/Pure/System/system_channel.scala	Sat Feb 13 20:41:56 2016 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4  
     7.5    def params: List[String] = List("127.0.0.1", server.getLocalPort.toString)
     7.6  
     7.7 -  def prover_args: List[String] = List("-P", "127.0.0.1:" + server.getLocalPort)
     7.8 +  def prover_options: String = "-P 127.0.0.1:" + server.getLocalPort
     7.9  
    7.10    def rendezvous(): (OutputStream, InputStream) =
    7.11    {
     8.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Sat Feb 13 20:01:48 2016 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Sat Feb 13 20:41:56 2016 +0100
     8.3 @@ -72,9 +72,10 @@
     8.4    def session_start()
     8.5    {
     8.6      val print_modes =
     8.7 -      space_explode(',', PIDE.options.string("jedit_print_mode")) :::
     8.8 -      space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))
     8.9 -    PIDE.session.start("Isabelle", print_modes.map("-m" + _) ::: List("-r", "-q", session_name()))
    8.10 +      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
    8.11 +       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).map("-m " + _)
    8.12 +    val args = (print_modes ::: List("-r", "-q", quote(session_name()))).mkString(" ")
    8.13 +    PIDE.session.start("Isabelle", args)
    8.14    }
    8.15  
    8.16    def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))