more abstract Session.start, without prover command-line;
authorwenzelm
Tue Mar 08 14:44:11 2016 +0100 (2016-03-08)
changeset 62556c115e69f457f
parent 62555 fd6e64133684
child 62557 a4ea3a222e0e
more abstract Session.start, without prover command-line;
Isabelle_Process.apply is directly based on ML_Process;
clarified Isabelle_Process.main command-line;
tuned signature;
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/ml_process.scala
src/Tools/jEdit/src/isabelle_logic.scala
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Tue Mar 08 11:18:21 2016 +0100
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Tue Mar 08 14:44:11 2016 +0100
     1.3 @@ -58,7 +58,8 @@
     1.4          case _ =>
     1.5        }
     1.6  
     1.7 -    prover_session.start("Isabelle", List("-q", parent_session))
     1.8 +    prover_session.start(receiver =>
     1.9 +      Isabelle_Process(options, heap = parent_session, receiver = receiver))
    1.10  
    1.11      batch_session
    1.12    }
     2.1 --- a/src/Pure/PIDE/prover.scala	Tue Mar 08 11:18:21 2016 +0100
     2.2 +++ b/src/Pure/PIDE/prover.scala	Tue Mar 08 14:44:11 2016 +0100
     2.3 @@ -39,6 +39,7 @@
     2.4    /* messages */
     2.5  
     2.6    sealed abstract class Message
     2.7 +  type Receiver = Message => Unit
     2.8  
     2.9    class Input(val name: String, val args: List[String]) extends Message
    2.10    {
    2.11 @@ -85,7 +86,7 @@
    2.12  
    2.13  
    2.14  abstract class Prover(
    2.15 -  receiver: Prover.Message => Unit,
    2.16 +  receiver: Prover.Receiver,
    2.17    system_channel: System_Channel,
    2.18    system_process: Prover.System_Process) extends Protocol
    2.19  {
     3.1 --- a/src/Pure/PIDE/resources.scala	Tue Mar 08 11:18:21 2016 +0100
     3.2 +++ b/src/Pure/PIDE/resources.scala	Tue Mar 08 14:44:11 2016 +0100
     3.3 @@ -132,11 +132,5 @@
     3.4      Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
     3.5  
     3.6    def commit(change: Session.Change) { }
     3.7 -
     3.8 -
     3.9 -  /* prover process */
    3.10 -
    3.11 -  def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
    3.12 -    Isabelle_Process(receiver, args)
    3.13  }
    3.14  
     4.1 --- a/src/Pure/PIDE/session.scala	Tue Mar 08 11:18:21 2016 +0100
     4.2 +++ b/src/Pure/PIDE/session.scala	Tue Mar 08 14:44:11 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(start_prover: Prover.Receiver => Prover)
     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 @@ -532,10 +532,10 @@
    4.13            case input: Prover.Input =>
    4.14              all_messages.post(input)
    4.15  
    4.16 -          case Start(name, args) if !prover.defined =>
    4.17 +          case Start(start_prover) if !prover.defined =>
    4.18              if (phase == Session.Inactive || phase == Session.Failed) {
    4.19                phase = Session.Startup
    4.20 -              prover.set(resources.start_prover(manager.send(_), name, args))
    4.21 +              prover.set(start_prover(manager.send(_)))
    4.22              }
    4.23  
    4.24            case Stop =>
    4.25 @@ -601,8 +601,8 @@
    4.26        pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
    4.27      global_state.value.snapshot(name, pending_edits)
    4.28  
    4.29 -  def start(name: String, args: List[String])
    4.30 -  { manager.send(Start(name, args)) }
    4.31 +  def start(start_prover: Prover.Receiver => Prover)
    4.32 +  { manager.send(Start(start_prover)) }
    4.33  
    4.34    def stop()
    4.35    {
     5.1 --- a/src/Pure/System/isabelle_process.scala	Tue Mar 08 11:18:21 2016 +0100
     5.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Mar 08 14:44:11 2016 +0100
     5.3 @@ -10,21 +10,23 @@
     5.4  object Isabelle_Process
     5.5  {
     5.6    def apply(
     5.7 -    receiver: Prover.Message => Unit = Console.println(_),
     5.8 -    prover_args: List[String] = Nil): Isabelle_Process =
     5.9 +    options: Options,
    5.10 +    heap: String = "",
    5.11 +    args: List[String] = Nil,
    5.12 +    modes: List[String] = Nil,
    5.13 +    secure: Boolean = false,
    5.14 +    receiver: Prover.Receiver = Console.println(_)): Isabelle_Process =
    5.15    {
    5.16 -    val system_channel = System_Channel()
    5.17 -    val system_process =
    5.18 +    val channel = System_Channel()
    5.19 +    val process =
    5.20        try {
    5.21 -        val process =
    5.22 -          Bash.process("\"$ISABELLE_PROCESS\" -P " + File.bash_string(system_channel.server_name) +
    5.23 -            " " + File.bash_args(prover_args))
    5.24 -        process.stdin.close
    5.25 -        process
    5.26 +        ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
    5.27 +          process_socket = channel.server_name)
    5.28        }
    5.29 -      catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }
    5.30 +      catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    5.31 +    process.stdin.close
    5.32  
    5.33 -    new Isabelle_Process(receiver, system_channel, system_process)
    5.34 +    new Isabelle_Process(receiver, channel, process)
    5.35    }
    5.36  
    5.37  
    5.38 @@ -33,7 +35,7 @@
    5.39    def main(args: Array[String])
    5.40    {
    5.41      Command_Line.tool {
    5.42 -      var ml_args: List[String] = Nil
    5.43 +      var eval_args: List[String] = Nil
    5.44        var modes: List[String] = Nil
    5.45        var options = Options.init()
    5.46  
    5.47 @@ -50,8 +52,8 @@
    5.48    $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
    5.49    if it is RAW_ML_SYSTEM, the initial ML heap is used.
    5.50  """,
    5.51 -        "e:" -> (arg => ml_args = ml_args ::: List("--eval", arg)),
    5.52 -        "f:" -> (arg => ml_args = ml_args ::: List("--use", arg)),
    5.53 +        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    5.54 +        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
    5.55          "m:" -> (arg => modes = arg :: modes),
    5.56          "o:" -> (arg => options = options + arg))
    5.57  
    5.58 @@ -62,17 +64,15 @@
    5.59            case _ => getopts.usage()
    5.60          }
    5.61  
    5.62 -      ML_Process(options, heap = heap, args = ml_args, modes = modes).
    5.63 +      ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
    5.64          result().print_stdout.rc
    5.65      }
    5.66    }
    5.67  }
    5.68  
    5.69  class Isabelle_Process private(
    5.70 -    receiver: Prover.Message => Unit,
    5.71 -    system_channel: System_Channel,
    5.72 -    system_process: Prover.System_Process)
    5.73 -  extends Prover(receiver, system_channel, system_process)
    5.74 +    receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process)
    5.75 +  extends Prover(receiver, channel, process)
    5.76  {
    5.77    def encode(s: String): String = Symbol.encode(s)
    5.78    def decode(s: String): String = Symbol.decode(s)
     6.1 --- a/src/Pure/System/ml_process.scala	Tue Mar 08 11:18:21 2016 +0100
     6.2 +++ b/src/Pure/System/ml_process.scala	Tue Mar 08 14:44:11 2016 +0100
     6.3 @@ -12,9 +12,9 @@
     6.4    def apply(options: Options,
     6.5      heap: String = "",
     6.6      args: List[String] = Nil,
     6.7 -    process_socket: String = "",
     6.8 +    modes: List[String] = Nil,
     6.9      secure: Boolean = false,
    6.10 -    modes: List[String] = Nil): Bash.Process =
    6.11 +    process_socket: String = ""): Bash.Process =
    6.12    {
    6.13      val load_heaps =
    6.14      {
    6.15 @@ -55,19 +55,18 @@
    6.16        }
    6.17        else Nil
    6.18  
    6.19 -    val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
    6.20 -
    6.21      val eval_modes =
    6.22        if (modes.isEmpty) Nil
    6.23        else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
    6.24  
    6.25 -
    6.26      // options
    6.27      val isabelle_process_options = Isabelle_System.tmp_file("options")
    6.28      File.write(isabelle_process_options, YXML.string_of_body(options.encode))
    6.29      val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
    6.30      val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
    6.31  
    6.32 +    val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
    6.33 +
    6.34      val eval_process =
    6.35        if (process_socket == "") Nil
    6.36        else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket))
    6.37 @@ -75,7 +74,7 @@
    6.38      // bash
    6.39      val bash_args =
    6.40        Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
    6.41 -      (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process).
    6.42 +      (eval_heaps ::: eval_exit ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
    6.43          map(eval => List("--eval", eval)).flatten ::: args
    6.44  
    6.45      Bash.process(env = env, script =
     7.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Mar 08 11:18:21 2016 +0100
     7.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Mar 08 14:44:11 2016 +0100
     7.3 @@ -69,15 +69,16 @@
     7.4        dirs = session_dirs(), sessions = List(session_name()))
     7.5    }
     7.6  
     7.7 -  def session_args(): List[String] =
     7.8 +  def session_start()
     7.9    {
    7.10 -    (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
    7.11 -     space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).
    7.12 -      map(m => List("-m", m)).flatten ::: List("-q", session_name())
    7.13 +    val modes =
    7.14 +      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
    7.15 +       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
    7.16 +    PIDE.session.start(receiver =>
    7.17 +      Isabelle_Process(
    7.18 +        PIDE.options.value, heap = session_name(), modes = modes, receiver = receiver))
    7.19    }
    7.20  
    7.21 -  def session_start(): Unit = PIDE.session.start("Isabelle", session_args())
    7.22 -
    7.23    def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    7.24  
    7.25    def session_list(): List[String] =