src/Pure/System/isabelle_process.scala
author wenzelm
Fri, 27 Mar 2020 22:01:27 +0100
changeset 71601 97ccf48c2f0c
parent 71598 269dc4bf1f40
child 71604 c6fa217c9d5e
permissions -rw-r--r--
misc tuning based on hints by IntelliJ IDEA;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43283
446e6621762d updated headers;
wenzelm
parents: 40848
diff changeset
     1
/*  Title:      Pure/System/isabelle_process.scala
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     3
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
     4
Isabelle process wrapper.
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     5
*/
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     6
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     7
package isabelle
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     8
55618
995162143ef4 tuned imports;
wenzelm
parents: 54443
diff changeset
     9
65310
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    10
import java.io.{File => JFile}
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    11
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    12
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    13
object Isabelle_Process
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    14
{
71597
d025735a4090 clarified signature;
wenzelm
parents: 71594
diff changeset
    15
  def apply(
71594
8a298184f3f9 clarified signature;
wenzelm
parents: 69572
diff changeset
    16
    session: Session,
65216
060a8a1f2dec tuned signature;
wenzelm
parents: 62754
diff changeset
    17
    options: Options,
71594
8a298184f3f9 clarified signature;
wenzelm
parents: 69572
diff changeset
    18
    sessions_structure: Sessions.Structure,
71598
269dc4bf1f40 clarified signature;
wenzelm
parents: 71597
diff changeset
    19
    store: Sessions.Store,
65216
060a8a1f2dec tuned signature;
wenzelm
parents: 62754
diff changeset
    20
    logic: String = "",
060a8a1f2dec tuned signature;
wenzelm
parents: 62754
diff changeset
    21
    args: List[String] = Nil,
060a8a1f2dec tuned signature;
wenzelm
parents: 62754
diff changeset
    22
    modes: List[String] = Nil,
65310
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    23
    cwd: JFile = null,
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    24
    env: Map[String, String] = Isabelle_System.settings(),
65225
ec9ec04546fc support for permanent phase_changed watcher;
wenzelm
parents: 65218
diff changeset
    25
    phase_changed: Session.Phase => Unit = null)
65216
060a8a1f2dec tuned signature;
wenzelm
parents: 62754
diff changeset
    26
  {
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    27
    val channel = System_Channel()
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    28
    val process =
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    29
      try {
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 68209
diff changeset
    30
        val channel_options =
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 68209
diff changeset
    31
          options.string.update("system_channel_address", channel.address).
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 68209
diff changeset
    32
            string.update("system_channel_password", channel.password)
71598
269dc4bf1f40 clarified signature;
wenzelm
parents: 71597
diff changeset
    33
        ML_Process(channel_options, sessions_structure, store,
269dc4bf1f40 clarified signature;
wenzelm
parents: 71597
diff changeset
    34
          logic = logic, args = args, modes = modes, cwd = cwd, env = env)
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    35
      }
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 68209
diff changeset
    36
      catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    37
    process.stdin.close
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    38
71597
d025735a4090 clarified signature;
wenzelm
parents: 71594
diff changeset
    39
    if (phase_changed != null)
d025735a4090 clarified signature;
wenzelm
parents: 71594
diff changeset
    40
      session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
d025735a4090 clarified signature;
wenzelm
parents: 71594
diff changeset
    41
d025735a4090 clarified signature;
wenzelm
parents: 71594
diff changeset
    42
    session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    43
  }
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    44
}