src/Pure/Tools/server.scala
author wenzelm
Sat, 07 Aug 2021 21:25:47 +0200
changeset 74141 bba35ad317ab
parent 74140 8a5e02ef975c
child 74145 608f8ae89cac
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/server.scala
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     3
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     4
Resident Isabelle servers.
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     5
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     6
Message formats:
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     7
  - short message (single line):
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     8
      NAME ARGUMENT
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     9
  - long message (multiple lines):
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
    10
      BYTE_LENGTH
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
    11
      NAME ARGUMENT
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    12
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    13
Argument formats:
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    14
  - Unit as empty string
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    15
  - XML.Elem in YXML notation
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    16
  - JSON.T in standard notation
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    17
*/
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    18
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    19
package isabelle
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    20
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    21
67837
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
    22
import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter,
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
    23
  IOException}
67797
1cfc7541012e Entry.connection: proview password here;
wenzelm
parents: 67796
diff changeset
    24
import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    25
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    26
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    27
object Server
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    28
{
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    29
  /* message argument */
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    30
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    31
  object Argument
67794
wenzelm
parents: 67793
diff changeset
    32
  {
67903
6e85d866251f clarified message name: disallow single quote;
wenzelm
parents: 67902
diff changeset
    33
    def is_name_char(c: Char): Boolean =
6e85d866251f clarified message name: disallow single quote;
wenzelm
parents: 67902
diff changeset
    34
      Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.'
6e85d866251f clarified message name: disallow single quote;
wenzelm
parents: 67902
diff changeset
    35
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    36
    def split(msg: String): (String, String) =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    37
    {
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71383
diff changeset
    38
      val name = msg.takeWhile(is_name_char)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71383
diff changeset
    39
      val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank)
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    40
      (name, argument)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    41
    }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    42
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    43
    def print(arg: Any): String =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    44
      arg match {
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    45
        case () => ""
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    46
        case t: XML.Elem => YXML.string_of_tree(t)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    47
        case t: JSON.T => JSON.Format(t)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    48
      }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    49
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    50
    def parse(argument: String): Any =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    51
      if (argument == "") ()
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    52
      else if (YXML.detect_elem(argument)) YXML.parse_elem(argument)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    53
      else JSON.parse(argument, strict = false)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    54
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    55
    def unapply(argument: String): Option[Any] =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    56
      try { Some(parse(argument)) }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    57
      catch { case ERROR(_) => None }
67794
wenzelm
parents: 67793
diff changeset
    58
  }
wenzelm
parents: 67793
diff changeset
    59
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    60
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    61
  /* input command */
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    62
72163
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    63
  type Command_Body = PartialFunction[(Context, Any), Any]
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    64
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    65
  abstract class Command(val command_name: String)
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    66
  {
72163
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    67
    def command_body: Command_Body
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    68
    override def toString: String = command_name
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    69
  }
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    70
72163
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    71
  class Commands(commands: Command*) extends Isabelle_System.Service
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    72
  {
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    73
    def entries: List[Command] = commands.toList
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    74
  }
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    75
72163
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    76
  private lazy val command_table: Map[String, Command] =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
    77
    Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries).
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
    78
      foldLeft(Map.empty[String, Command]) {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
    79
        case (cmds, cmd) =>
72163
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    80
          val name = cmd.command_name
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    81
          if (cmds.isDefinedAt(name)) error("Duplicate Isabelle server command: " + quote(name))
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
    82
          else cmds + (name -> cmd)
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
    83
      }
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    84
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    85
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    86
  /* output reply */
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
    87
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
    88
  class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
    89
    extends RuntimeException(message)
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
    90
67891
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
    91
  def json_error(exn: Throwable): JSON.Object.T =
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
    92
    exn match {
67913
d58fa3ed236f proper order of matches: Server.Error is an instance of Exn.ERROR;
wenzelm
parents: 67911
diff changeset
    93
      case e: Error => Reply.error_message(e.message) ++ e.json
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
    94
      case ERROR(msg) => Reply.error_message(msg)
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
    95
      case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
67891
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
    96
      case _ => JSON.Object.empty
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
    97
    }
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
    98
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    99
  object Reply extends Enumeration
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   100
  {
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   101
    val OK, ERROR, FINISHED, FAILED, NOTE = Value
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   102
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   103
    def message(msg: String, kind: String = ""): JSON.Object.T =
67931
f7917c15b566 field "kind" is always present, with default "writeln";
wenzelm
parents: 67920
diff changeset
   104
      JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg)
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   105
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   106
    def error_message(msg: String): JSON.Object.T =
67911
3cda747493d8 clarified markup according to common Command.Results;
wenzelm
parents: 67904
diff changeset
   107
      message(msg, kind = Markup.ERROR)
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   108
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   109
    def unapply(msg: String): Option[(Reply.Value, Any)] =
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   110
    {
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   111
      if (msg == "") None
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   112
      else {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   113
        val (name, argument) = Argument.split(msg)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   114
        for {
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   115
          reply <-
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   116
            try { Some(withName(name)) }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   117
            catch { case _: NoSuchElementException => None }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   118
          arg <- Argument.unapply(argument)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   119
        } yield (reply, arg)
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   120
      }
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   121
    }
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   122
  }
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   123
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   124
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   125
  /* handler: port, password, thread */
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   126
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   127
  abstract class Handler(port0: Int)
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   128
  {
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   129
    val socket: ServerSocket = new ServerSocket(port0, 50, Server.localhost)
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   130
    def port: Int = socket.getLocalPort
74094
6113f1db4342 clarified signature;
wenzelm
parents: 73702
diff changeset
   131
    val password: String = UUID.random().toString
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   132
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   133
    override def toString: String = print(port, password)
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   134
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   135
    def handle(connection: Server.Connection): Unit
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   136
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   137
    private lazy val thread: Thread =
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   138
      Isabelle_Thread.fork(name = "server_handler") {
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   139
        var finished = false
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   140
        while (!finished) {
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   141
          Exn.capture(socket.accept) match {
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   142
            case Exn.Res(client) =>
73179
f9c71ce29150 tuned name, e.g. relevant for Naproche-SAD debugging in Isabelle/jEdit;
wenzelm
parents: 73135
diff changeset
   143
              Isabelle_Thread.fork(name = "client") {
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   144
                using(Connection(client))(connection =>
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   145
                  if (connection.read_password(password)) handle(connection))
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   146
              }
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   147
            case Exn.Exn(_) => finished = true
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   148
          }
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   149
        }
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   150
      }
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   151
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   152
    def start(): Unit = thread
74140
8a5e02ef975c clarified signature;
wenzelm
parents: 74139
diff changeset
   153
    def join(): Unit = thread.join()
8a5e02ef975c clarified signature;
wenzelm
parents: 74139
diff changeset
   154
    def stop(): Unit = { socket.close(); join() }
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   155
  }
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   156
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   157
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   158
  /* socket connection */
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   159
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   160
  object Connection
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   161
  {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   162
    def apply(socket: Socket): Connection =
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   163
      new Connection(socket)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   164
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   165
69393
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69033
diff changeset
   166
  class Connection private(socket: Socket) extends AutoCloseable
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   167
  {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   168
    override def toString: String = socket.toString
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   169
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   170
    def close(): Unit = socket.close()
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   171
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   172
    def set_timeout(t: Time): Unit = socket.setSoTimeout(t.ms.toInt)
67832
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   173
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   174
    private val in = new BufferedInputStream(socket.getInputStream)
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   175
    private val out = new BufferedOutputStream(socket.getOutputStream)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   176
    private val out_lock: AnyRef = new Object
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   177
71713
928fd852f3e2 more robust interrupt handling;
wenzelm
parents: 71692
diff changeset
   178
    def tty_loop(): TTY_Loop =
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   179
      new TTY_Loop(
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   180
        new OutputStreamWriter(out),
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   181
        new InputStreamReader(in),
71713
928fd852f3e2 more robust interrupt handling;
wenzelm
parents: 71692
diff changeset
   182
        writer_lock = out_lock)
67837
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
   183
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   184
    def read_password(password: String): Boolean =
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   185
      try { Byte_Message.read_line(in).map(_.text) == Some(password) }
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   186
      catch { case _: IOException => false }
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   187
74139
3314559ef095 clarified signature;
wenzelm
parents: 74094
diff changeset
   188
    def read_line_message(): Option[String] =
69451
387894c2fb2c more uniform multi-language operations;
wenzelm
parents: 69448
diff changeset
   189
      try { Byte_Message.read_line_message(in).map(_.text) }
387894c2fb2c more uniform multi-language operations;
wenzelm
parents: 69448
diff changeset
   190
      catch { case _: IOException => None }
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   191
73133
497e11537d48 clarified signature: more operations;
wenzelm
parents: 73132
diff changeset
   192
    def await_close(): Unit =
73135
76bdfde8a579 clarified;
wenzelm
parents: 73133
diff changeset
   193
      try { Byte_Message.read(in, 1); socket.close() }
73133
497e11537d48 clarified signature: more operations;
wenzelm
parents: 73132
diff changeset
   194
      catch { case _: IOException => }
497e11537d48 clarified signature: more operations;
wenzelm
parents: 73132
diff changeset
   195
74139
3314559ef095 clarified signature;
wenzelm
parents: 74094
diff changeset
   196
    def write_line_message(msg: String): Unit =
69448
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69393
diff changeset
   197
      out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   198
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   199
    def reply(r: Reply.Value, arg: Any): Unit =
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   200
    {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   201
      val argument = Argument.print(arg)
74139
3314559ef095 clarified signature;
wenzelm
parents: 74094
diff changeset
   202
      write_line_message(if (argument == "") r.toString else r.toString + " " + argument)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   203
    }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   204
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   205
    def reply_ok(arg: Any): Unit = reply(Reply.OK, arg)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   206
    def reply_error(arg: Any): Unit = reply(Reply.ERROR, arg)
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   207
    def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   208
      reply_error(Reply.error_message(message) ++ more)
67801
8f5f5fbe291b added Reply.NOTE for asynchronous notifications;
wenzelm
parents: 67800
diff changeset
   209
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   210
    def notify(arg: Any): Unit = reply(Reply.NOTE, arg)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   211
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   212
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   213
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   214
  /* context with output channels */
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   215
67878
15027fb50a0c clarified signature;
wenzelm
parents: 67876
diff changeset
   216
  class Context private[Server](val server: Server, connection: Connection)
69393
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69033
diff changeset
   217
    extends AutoCloseable
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   218
  {
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   219
    context =>
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   220
72163
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
   221
    def command_list: List[String] = command_table.keys.toList.sorted
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 71747
diff changeset
   222
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   223
    def reply(r: Reply.Value, arg: Any): Unit = connection.reply(r, arg)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   224
    def notify(arg: Any): Unit = connection.notify(arg)
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   225
    def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   226
      notify(Reply.message(msg, kind = kind) ++ more)
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   227
    def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   228
    def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   229
    def error_message(msg: String, more: JSON.Object.Entry*): Unit =
67911
3cda747493d8 clarified markup according to common Command.Results;
wenzelm
parents: 67904
diff changeset
   230
      message(Markup.ERROR, msg, more:_*)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   231
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   232
    def progress(more: JSON.Object.Entry*): Connection_Progress =
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   233
      new Connection_Progress(context, more:_*)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   234
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   235
    override def toString: String = connection.toString
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   236
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   237
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   238
    /* asynchronous tasks */
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   239
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   240
    private val _tasks = Synchronized(Set.empty[Task])
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   241
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   242
    def make_task(body: Task => JSON.Object.T): Task =
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   243
    {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   244
      val task = new Task(context, body)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   245
      _tasks.change(_ + task)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   246
      task
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   247
    }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   248
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   249
    def remove_task(task: Task): Unit =
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   250
      _tasks.change(_ - task)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   251
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   252
    def cancel_task(id: UUID.T): Unit =
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   253
      _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel()); tasks })
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   254
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   255
    def close(): Unit =
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   256
    {
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   257
      while(_tasks.change_result(tasks => { tasks.foreach(_.cancel()); (tasks.nonEmpty, tasks) }))
74140
8a5e02ef975c clarified signature;
wenzelm
parents: 74139
diff changeset
   258
      { _tasks.value.foreach(_.join()) }
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   259
    }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   260
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   261
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   262
  class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   263
    extends Progress
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   264
  {
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   265
    override def echo(msg: String): Unit = context.writeln(msg, more:_*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   266
    override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   267
    override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   268
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   269
    override def theory(theory: Progress.Theory): Unit =
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   270
    {
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   271
      val entries: List[JSON.Object.Entry] =
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   272
        List("theory" -> theory.theory, "session" -> theory.session) :::
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   273
          (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) })
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   274
      context.writeln(theory.message, entries ::: more.toList:_*)
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   275
    }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   276
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   277
    override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit =
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   278
    {
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68888
diff changeset
   279
      val json =
69818
60d0ee8f2ddb more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents: 69817
diff changeset
   280
        for ((name, node_status) <- nodes_status.present)
73132
wenzelm
parents: 73131
diff changeset
   281
          yield name.json + ("status" -> node_status.json)
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   282
      context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   283
    }
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   284
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   285
    override def toString: String = context.toString
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   286
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   287
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   288
  class Task private[Server](val context: Context, body: Task => JSON.Object.T)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   289
  {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   290
    task =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   291
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   292
    val id: UUID.T = UUID.random()
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   293
    val ident: JSON.Object.Entry = ("task" -> id.toString)
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   294
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   295
    val progress: Connection_Progress = context.progress(ident)
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   296
    def cancel(): Unit = progress.stop()
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   297
71692
f8e52c0152fe clarified names;
wenzelm
parents: 71685
diff changeset
   298
    private lazy val thread = Isabelle_Thread.fork(name = "server_task")
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   299
    {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   300
      Exn.capture { body(task) } match {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   301
        case Exn.Res(res) =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   302
          context.reply(Reply.FINISHED, res + ident)
67891
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   303
        case Exn.Exn(exn) =>
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   304
          val err = json_error(exn)
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   305
          if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   306
      }
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   307
      progress.stop()
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   308
      context.remove_task(task)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   309
    }
74140
8a5e02ef975c clarified signature;
wenzelm
parents: 74139
diff changeset
   310
    def start(): Unit = thread
8a5e02ef975c clarified signature;
wenzelm
parents: 74139
diff changeset
   311
    def join(): Unit = thread.join()
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   312
  }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   313
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   314
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   315
  /* server info */
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   316
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   317
  val localhost_name: String = "127.0.0.1"
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   318
  def localhost: InetAddress = InetAddress.getByName(localhost_name)
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   319
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   320
  def print_address(port: Int): String = localhost_name + ":" + port
69460
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   321
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   322
  def print(port: Int, password: String): String =
69461
be142f577da6 tuned signature;
wenzelm
parents: 69460
diff changeset
   323
    print_address(port) + " (password " + quote(password) + ")"
69460
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   324
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   325
  object Info
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   326
  {
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   327
    private val Pattern =
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   328
      ("""server "([^"]*)" = \Q""" + localhost_name + """\E:(\d+) \(password "([^"]*)"\)""").r
69460
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   329
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   330
    def parse(s: String): Option[Info] =
69460
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   331
      s match {
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   332
        case Pattern(name, Value.Int(port), password) => Some(Info(name, port, password))
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   333
        case _ => None
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   334
      }
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   335
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   336
    def apply(name: String, port: Int, password: String): Info =
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   337
      new Info(name, port, password)
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   338
  }
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   339
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   340
  class Info private(val name: String, val port: Int, val password: String)
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   341
  {
69461
be142f577da6 tuned signature;
wenzelm
parents: 69460
diff changeset
   342
    def address: String = print_address(port)
69460
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   343
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   344
    override def toString: String =
67821
82fb12061069 more uniform output: this may be parsed by another program;
wenzelm
parents: 67820
diff changeset
   345
      "server " + quote(name) + " = " + print(port, password)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   346
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   347
    def connection(): Connection =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   348
    {
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   349
      val connection = Connection(new Socket(localhost, port))
74139
3314559ef095 clarified signature;
wenzelm
parents: 74094
diff changeset
   350
      connection.write_line_message(password)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   351
      connection
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   352
    }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   353
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   354
    def active: Boolean =
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   355
      try {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   356
        using(connection())(connection =>
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   357
          {
67832
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   358
            connection.set_timeout(Time.seconds(2.0))
74139
3314559ef095 clarified signature;
wenzelm
parents: 74094
diff changeset
   359
            connection.read_line_message() match {
67867
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   360
              case Some(Reply(Reply.OK, _)) => true
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   361
              case _ => false
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   362
            }
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   363
          })
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   364
      }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   365
      catch {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   366
        case _: IOException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   367
        case _: SocketException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   368
        case _: SocketTimeoutException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   369
      }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   370
  }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   371
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   372
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   373
  /* per-user servers */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   374
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   375
  val default_name = "isabelle"
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   376
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   377
  object Data
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   378
  {
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   379
    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   380
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66353
diff changeset
   381
    val name = SQL.Column.string("name").make_primary_key
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   382
    val port = SQL.Column.int("port")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   383
    val password = SQL.Column.string("password")
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   384
    val table = SQL.Table("isabelle_servers", List(name, port, password))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   385
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   386
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   387
  def list(db: SQLite.Database): List[Info] =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   388
    if (db.tables.contains(Data.table.name)) {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   389
      db.using_statement(Data.table.select())(stmt =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   390
        stmt.execute_query().iterator(res =>
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   391
          Info(
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   392
            res.string(Data.name),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   393
            res.int(Data.port),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   394
            res.string(Data.password))).toList.sortBy(_.name))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   395
    }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   396
    else Nil
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   397
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   398
  def find(db: SQLite.Database, name: String): Option[Info] =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   399
    list(db).find(server_info => server_info.name == name && server_info.active)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   400
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   401
  def init(
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   402
    name: String = default_name,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   403
    port: Int = 0,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   404
    existing_server: Boolean = false,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   405
    log: Logger = No_Logger): (Info, Option[Server]) =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   406
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   407
    using(SQLite.open_database(Data.database))(db =>
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   408
      {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   409
        db.transaction {
71114
6cfec8029831 clarified signature;
wenzelm
parents: 69818
diff changeset
   410
          Isabelle_System.chmod("600", Data.database)
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   411
          db.create_table(Data.table)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   412
          list(db).filterNot(_.active).foreach(server_info =>
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   413
            db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   414
              _.execute()))
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   415
        }
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   416
        db.transaction {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   417
          find(db, name) match {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   418
            case Some(server_info) => (server_info, None)
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   419
            case None =>
67821
82fb12061069 more uniform output: this may be parsed by another program;
wenzelm
parents: 67820
diff changeset
   420
              if (existing_server) error("Isabelle server " + quote(name) + " not running")
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   421
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   422
              val server = new Server(port, log)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   423
              val server_info = Info(name, server.port, server.password)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   424
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   425
              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute())
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   426
              db.using_statement(Data.table.insert())(stmt =>
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   427
              {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   428
                stmt.string(1) = server_info.name
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   429
                stmt.int(2) = server_info.port
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   430
                stmt.string(3) = server_info.password
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   431
                stmt.execute()
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   432
              })
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   433
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   434
              server.start()
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   435
              (server_info, Some(server))
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   436
          }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   437
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   438
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   439
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   440
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   441
  def exit(name: String = default_name): Boolean =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   442
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   443
    using(SQLite.open_database(Data.database))(db =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   444
      db.transaction {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   445
        find(db, name) match {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   446
          case Some(server_info) =>
74139
3314559ef095 clarified signature;
wenzelm
parents: 74094
diff changeset
   447
            using(server_info.connection())(_.write_line_message("shutdown"))
73702
7202e12cb324 tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents: 73523
diff changeset
   448
            while(server_info.active) { Time.seconds(0.05).sleep() }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   449
            true
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   450
          case None => false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   451
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   452
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   453
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   454
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   455
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   456
  /* Isabelle tool wrapper */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   457
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   458
  val isabelle_tool =
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72163
diff changeset
   459
    Isabelle_Tool("server", "manage resident Isabelle servers", Scala_Project.here, args =>
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   460
    {
67806
bd4c440c8be7 option for console interaction;
wenzelm
parents: 67805
diff changeset
   461
      var console = false
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   462
      var log_file: Option[Path] = None
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   463
      var operation_list = false
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   464
      var operation_exit = false
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   465
      var name = default_name
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   466
      var port = 0
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   467
      var existing_server = false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   468
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   469
      val getopts =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   470
        Getopts("""
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   471
Usage: isabelle server [OPTIONS]
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   472
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   473
  Options are:
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   474
    -L FILE      logging on FILE
67875
641315ebed02 tuned options;
wenzelm
parents: 67873
diff changeset
   475
    -c           console interaction with specified server
67904
465f43a9f780 documentation for the Isabelle server;
wenzelm
parents: 67903
diff changeset
   476
    -l           list servers (alternative operation)
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   477
    -n NAME      explicit server name (default: """ + default_name + """)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   478
    -p PORT      explicit server port
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   479
    -s           assume existing server, no implicit startup
67904
465f43a9f780 documentation for the Isabelle server;
wenzelm
parents: 67903
diff changeset
   480
    -x           exit specified server (alternative operation)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   481
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   482
  Manage resident Isabelle servers.
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   483
""",
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   484
          "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
67875
641315ebed02 tuned options;
wenzelm
parents: 67873
diff changeset
   485
          "c" -> (_ => console = true),
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   486
          "l" -> (_ => operation_list = true),
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   487
          "n:" -> (arg => name = arg),
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   488
          "p:" -> (arg => port = Value.Int.parse(arg)),
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   489
          "s" -> (_ => existing_server = true),
67876
cc4832285c38 proper options;
wenzelm
parents: 67875
diff changeset
   490
          "x" -> (_ => operation_exit = true))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   491
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   492
      val more_args = getopts(args)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   493
      if (more_args.nonEmpty) getopts.usage()
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   494
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   495
      if (operation_list) {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   496
        for {
71714
wenzelm
parents: 71713
diff changeset
   497
          server_info <- using(SQLite.open_database(Data.database))(list)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   498
          if server_info.active
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   499
        } Output.writeln(server_info.toString, stdout = true)
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   500
      }
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   501
      else if (operation_exit) {
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   502
        val ok = Server.exit(name)
69033
c5db368833b1 proper return code for runtime failure;
wenzelm
parents: 69012
diff changeset
   503
        sys.exit(if (ok) 0 else 2)
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   504
      }
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   505
      else {
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   506
        val log = Logger.make(log_file)
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   507
        val (server_info, server) =
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   508
          init(name, port = port, existing_server = existing_server, log = log)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   509
        Output.writeln(server_info.toString, stdout = true)
67834
wenzelm
parents: 67833
diff changeset
   510
        if (console) {
74141
bba35ad317ab tuned signature;
wenzelm
parents: 74140
diff changeset
   511
          using(server_info.connection())(connection => connection.tty_loop().join())
67834
wenzelm
parents: 67833
diff changeset
   512
        }
74140
8a5e02ef975c clarified signature;
wenzelm
parents: 74139
diff changeset
   513
        server.foreach(_.join())
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   514
      }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   515
    })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   516
}
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   517
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   518
class Server private(port0: Int, val log: Logger) extends Server.Handler(port0)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   519
{
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   520
  server =>
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   521
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   522
  private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   523
  def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
71383
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 71114
diff changeset
   524
  def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id))
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   525
  def add_session(entry: (UUID.T, Headless.Session)): Unit = _sessions.change(_ + entry)
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   526
  def remove_session(id: UUID.T): Headless.Session =
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   527
  {
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   528
    _sessions.change_result(sessions =>
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   529
      sessions.get(id) match {
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   530
        case Some(session) => (session, sessions - id)
67883
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
   531
        case None => err_session(id)
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   532
      })
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   533
  }
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   534
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   535
  def shutdown(): Unit =
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   536
  {
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73359
diff changeset
   537
    server.socket.close()
67791
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   538
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   539
    val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   540
    for ((_, session) <- sessions) {
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   541
      try {
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   542
        val result = session.stop()
71747
1dd514c8c1df clarified signature;
wenzelm
parents: 71726
diff changeset
   543
        if (!result.ok) log("Session shutdown failed: " + result.print_rc)
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   544
      }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   545
      catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   546
    }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   547
  }
67791
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   548
74140
8a5e02ef975c clarified signature;
wenzelm
parents: 74139
diff changeset
   549
  override def join(): Unit = { super.join(); shutdown() }
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   550
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73179
diff changeset
   551
  override def handle(connection: Server.Connection): Unit =
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   552
  {
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   553
    using(new Server.Context(server, connection))(context =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   554
    {
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   555
      connection.reply_ok(
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   556
        JSON.Object(
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   557
          "isabelle_id" -> Isabelle_System.isabelle_id(),
73523
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73367
diff changeset
   558
          "isabelle_name" -> Isabelle_System.isabelle_name()))
67867
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   559
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   560
      var finished = false
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   561
      while (!finished) {
74139
3314559ef095 clarified signature;
wenzelm
parents: 74094
diff changeset
   562
        connection.read_line_message() match {
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   563
          case None => finished = true
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   564
          case Some("") => context.notify("Command 'help' provides list of commands")
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   565
          case Some(msg) =>
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   566
            val (name, argument) = Server.Argument.split(msg)
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   567
            Server.command_table.get(name) match {
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   568
              case Some(cmd) =>
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   569
                argument match {
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   570
                  case Server.Argument(arg) =>
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   571
                    if (cmd.command_body.isDefinedAt((context, arg))) {
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   572
                      Exn.capture { cmd.command_body((context, arg)) } match {
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   573
                        case Exn.Res(task: Server.Task) =>
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   574
                          connection.reply_ok(JSON.Object(task.ident))
74140
8a5e02ef975c clarified signature;
wenzelm
parents: 74139
diff changeset
   575
                          task.start()
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   576
                        case Exn.Res(res) => connection.reply_ok(res)
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   577
                        case Exn.Exn(exn) =>
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   578
                          val err = Server.json_error(exn)
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   579
                          if (err.isEmpty) throw exn else connection.reply_error(err)
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   580
                      }
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   581
                    }
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   582
                    else {
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   583
                      connection.reply_error_message(
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   584
                        "Bad argument for command " + Library.single_quote(name),
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   585
                        "argument" -> argument)
73131
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   586
                    }
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   587
                  case _ =>
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   588
                    connection.reply_error_message(
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   589
                      "Malformed argument for command " + Library.single_quote(name),
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   590
                      "argument" -> argument)
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   591
                }
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   592
              case None => connection.reply_error("Bad command " + Library.single_quote(name))
ff6b5e468d5f clarified signature: support more generic server implementations;
wenzelm
parents: 72763
diff changeset
   593
            }
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   594
        }
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   595
      }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   596
    })
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   597
  }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   598
}