src/Pure/Tools/server.scala
author wenzelm
Thu, 14 Nov 2019 11:35:02 +0100
changeset 71114 6cfec8029831
parent 69818 60d0ee8f2ddb
child 71383 8313dca6dee9
permissions -rw-r--r--
clarified 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
    {
67903
6e85d866251f clarified message name: disallow single quote;
wenzelm
parents: 67902
diff changeset
    38
      val name = msg.takeWhile(is_name_char(_))
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    39
      val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
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
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    63
  object Command
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    64
  {
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
    65
    type T = PartialFunction[(Context, Any), Any]
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    66
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    67
    private val table: Map[String, T] =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    68
      Map(
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents: 67840
diff changeset
    69
        "help" -> { case (_, ()) => table.keySet.toList.sorted },
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    70
        "echo" -> { case (_, t) => t },
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
    71
        "shutdown" -> { case (context, ()) => context.server.shutdown() },
67920
c3c74310154e clarified signature;
wenzelm
parents: 67913
diff changeset
    72
        "cancel" ->
c3c74310154e clarified signature;
wenzelm
parents: 67913
diff changeset
    73
          { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) },
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents: 67840
diff changeset
    74
        "session_build" ->
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents: 67840
diff changeset
    75
          { case (context, Server_Commands.Session_Build(args)) =>
67861
cd1cac824ef8 asynchronous "session_build";
wenzelm
parents: 67860
diff changeset
    76
              context.make_task(task =>
67886
26510aad2ec6 tuned signature;
wenzelm
parents: 67885
diff changeset
    77
                Server_Commands.Session_Build.command(args, progress = task.progress)._1)
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67867
diff changeset
    78
          },
8cb4fef58379 support for "session_start";
wenzelm
parents: 67867
diff changeset
    79
        "session_start" ->
8cb4fef58379 support for "session_start";
wenzelm
parents: 67867
diff changeset
    80
          { case (context, Server_Commands.Session_Start(args)) =>
8cb4fef58379 support for "session_start";
wenzelm
parents: 67867
diff changeset
    81
              context.make_task(task =>
8cb4fef58379 support for "session_start";
wenzelm
parents: 67867
diff changeset
    82
                {
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
    83
                  val (res, entry) =
67878
15027fb50a0c clarified signature;
wenzelm
parents: 67876
diff changeset
    84
                    Server_Commands.Session_Start.command(
67886
26510aad2ec6 tuned signature;
wenzelm
parents: 67885
diff changeset
    85
                      args, progress = task.progress, log = context.server.log)
67878
15027fb50a0c clarified signature;
wenzelm
parents: 67876
diff changeset
    86
                  context.server.add_session(entry)
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67867
diff changeset
    87
                  res
8cb4fef58379 support for "session_start";
wenzelm
parents: 67867
diff changeset
    88
                })
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
    89
          },
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
    90
        "session_stop" ->
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
    91
          { case (context, Server_Commands.Session_Stop(id)) =>
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
    92
              context.make_task(_ =>
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
    93
                {
67878
15027fb50a0c clarified signature;
wenzelm
parents: 67876
diff changeset
    94
                  val session = context.server.remove_session(id)
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
    95
                  Server_Commands.Session_Stop.command(session)._1
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
    96
                })
67883
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
    97
          },
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
    98
        "use_theories" ->
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
    99
          { case (context, Server_Commands.Use_Theories(args)) =>
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
   100
              context.make_task(task =>
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
   101
                {
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
   102
                  val session = context.server.the_session(args.session_id)
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   103
                  Server_Commands.Use_Theories.command(
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   104
                    args, session, id = task.id, progress = task.progress)._1
68530
a110dcc9a4c7 remove trailing commas
Lars Hupel <lars.hupel@mytum.de>
parents: 68410
diff changeset
   105
                })
67941
49a34b2fa788 added command "purge_theories";
wenzelm
parents: 67931
diff changeset
   106
          },
49a34b2fa788 added command "purge_theories";
wenzelm
parents: 67931
diff changeset
   107
        "purge_theories" ->
49a34b2fa788 added command "purge_theories";
wenzelm
parents: 67931
diff changeset
   108
          { case (context, Server_Commands.Purge_Theories(args)) =>
49a34b2fa788 added command "purge_theories";
wenzelm
parents: 67931
diff changeset
   109
              val session = context.server.the_session(args.session_id)
49a34b2fa788 added command "purge_theories";
wenzelm
parents: 67931
diff changeset
   110
              Server_Commands.Purge_Theories.command(args, session)._1
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents: 67840
diff changeset
   111
          })
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   112
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   113
    def unapply(name: String): Option[T] = table.get(name)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   114
  }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   115
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   116
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   117
  /* output reply */
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   118
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   119
  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
   120
    extends RuntimeException(message)
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   121
67891
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   122
  def json_error(exn: Throwable): JSON.Object.T =
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   123
    exn match {
67913
d58fa3ed236f proper order of matches: Server.Error is an instance of Exn.ERROR;
wenzelm
parents: 67911
diff changeset
   124
      case e: Error => Reply.error_message(e.message) ++ e.json
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   125
      case ERROR(msg) => Reply.error_message(msg)
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   126
      case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
67891
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   127
      case _ => JSON.Object.empty
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   128
    }
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   129
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   130
  object Reply extends Enumeration
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   131
  {
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   132
    val OK, ERROR, FINISHED, FAILED, NOTE = Value
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   133
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   134
    def message(msg: String, kind: String = ""): JSON.Object.T =
67931
f7917c15b566 field "kind" is always present, with default "writeln";
wenzelm
parents: 67920
diff changeset
   135
      JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg)
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   136
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   137
    def error_message(msg: String): JSON.Object.T =
67911
3cda747493d8 clarified markup according to common Command.Results;
wenzelm
parents: 67904
diff changeset
   138
      message(msg, kind = Markup.ERROR)
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   139
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   140
    def unapply(msg: String): Option[(Reply.Value, Any)] =
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   141
    {
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   142
      if (msg == "") None
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   143
      else {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   144
        val (name, argument) = Argument.split(msg)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   145
        for {
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   146
          reply <-
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   147
            try { Some(withName(name)) }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   148
            catch { case _: NoSuchElementException => None }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   149
          arg <- Argument.unapply(argument)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   150
        } yield (reply, arg)
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   151
      }
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
   152
    }
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   153
  }
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   154
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
   155
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   156
  /* socket connection */
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   157
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   158
  object Connection
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   159
  {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   160
    def apply(socket: Socket): Connection =
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   161
      new Connection(socket)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   162
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   163
69393
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69033
diff changeset
   164
  class Connection private(socket: Socket) extends AutoCloseable
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   165
  {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   166
    override def toString: String = socket.toString
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   167
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   168
    def close() { socket.close }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   169
67832
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   170
    def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) }
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   171
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   172
    private val in = new BufferedInputStream(socket.getInputStream)
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   173
    private val out = new BufferedOutputStream(socket.getOutputStream)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   174
    private val out_lock: AnyRef = new Object
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   175
67837
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
   176
    def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   177
      new TTY_Loop(
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   178
        new OutputStreamWriter(out),
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   179
        new InputStreamReader(in),
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   180
        writer_lock = out_lock,
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   181
        interrupt = interrupt)
67837
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
   182
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   183
    def read_password(password: String): Boolean =
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   184
      try { Byte_Message.read_line(in).map(_.text) == Some(password) }
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   185
      catch { case _: IOException => false }
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   186
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   187
    def read_message(): Option[String] =
69451
387894c2fb2c more uniform multi-language operations;
wenzelm
parents: 69448
diff changeset
   188
      try { Byte_Message.read_line_message(in).map(_.text) }
387894c2fb2c more uniform multi-language operations;
wenzelm
parents: 69448
diff changeset
   189
      catch { case _: IOException => None }
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   190
69448
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69393
diff changeset
   191
    def write_message(msg: String): Unit =
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69393
diff changeset
   192
      out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   193
67859
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   194
    def reply(r: Reply.Value, arg: Any)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   195
    {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   196
      val argument = Argument.print(arg)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   197
      write_message(if (argument == "") r.toString else r.toString + " " + argument)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   198
    }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   199
67859
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   200
    def reply_ok(arg: Any) { reply(Reply.OK, arg) }
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   201
    def reply_error(arg: Any) { reply(Reply.ERROR, arg) }
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   202
    def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   203
      reply_error(Reply.error_message(message) ++ more)
67801
8f5f5fbe291b added Reply.NOTE for asynchronous notifications;
wenzelm
parents: 67800
diff changeset
   204
67859
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   205
    def notify(arg: Any) { reply(Reply.NOTE, arg) }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   206
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   207
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   208
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   209
  /* context with output channels */
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   210
67878
15027fb50a0c clarified signature;
wenzelm
parents: 67876
diff changeset
   211
  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
   212
    extends AutoCloseable
67839
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 =>
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   215
67859
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   216
    def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
67840
a9d450fc5a49 tuned signature;
wenzelm
parents: 67839
diff changeset
   217
    def notify(arg: Any) { connection.notify(arg) }
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   218
    def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   219
      notify(Reply.message(msg, kind = kind) ++ more)
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   220
    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
   221
    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
   222
    def error_message(msg: String, more: JSON.Object.Entry*): Unit =
67911
3cda747493d8 clarified markup according to common Command.Results;
wenzelm
parents: 67904
diff changeset
   223
      message(Markup.ERROR, msg, more:_*)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   224
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   225
    def progress(more: JSON.Object.Entry*): Connection_Progress =
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   226
      new Connection_Progress(context, more:_*)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   227
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   228
    override def toString: String = connection.toString
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   229
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   230
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   231
    /* asynchronous tasks */
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   232
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   233
    private val _tasks = Synchronized(Set.empty[Task])
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   234
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   235
    def make_task(body: Task => JSON.Object.T): Task =
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
      val task = new Task(context, body)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   238
      _tasks.change(_ + task)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   239
      task
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   240
    }
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 remove_task(task: Task): Unit =
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   243
      _tasks.change(_ - task)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   244
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   245
    def cancel_task(id: UUID.T): Unit =
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   246
      _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
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
    def close()
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   249
    {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   250
      while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) }))
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   251
      { _tasks.value.foreach(_.join) }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   252
    }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   253
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   254
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   255
  class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   256
    extends Progress
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   257
  {
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   258
    override def echo(msg: String): Unit = context.writeln(msg, more:_*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   259
    override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   260
    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
   261
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   262
    override def theory(theory: Progress.Theory)
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   263
    {
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   264
      val entries: List[JSON.Object.Entry] =
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   265
        List("theory" -> theory.theory, "session" -> theory.session) :::
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   266
          (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) })
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   267
      context.writeln(theory.message, entries ::: more.toList:_*)
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   268
    }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   269
69818
60d0ee8f2ddb more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents: 69817
diff changeset
   270
    override def nodes_status(nodes_status: Document_Status.Nodes_Status)
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   271
    {
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68888
diff changeset
   272
      val json =
69818
60d0ee8f2ddb more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents: 69817
diff changeset
   273
        for ((name, node_status) <- nodes_status.present)
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68888
diff changeset
   274
          yield name.json + ("status" -> nodes_status(name).json)
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   275
      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
   276
    }
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   277
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   278
    @volatile private var is_stopped = false
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   279
    override def stopped: Boolean = is_stopped
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   280
    def stop { is_stopped = true }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   281
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   282
    override def toString: String = context.toString
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   283
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   284
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   285
  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
   286
  {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   287
    task =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   288
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   289
    val id: UUID.T = UUID.random()
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   290
    val ident: JSON.Object.Entry = ("task" -> id.toString)
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   291
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   292
    val progress: Connection_Progress = context.progress(ident)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   293
    def cancel { progress.stop }
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
    private lazy val thread = Standard_Thread.fork("server_task")
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   296
    {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   297
      Exn.capture { body(task) } match {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   298
        case Exn.Res(res) =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   299
          context.reply(Reply.FINISHED, res + ident)
67891
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   300
        case Exn.Exn(exn) =>
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   301
          val err = json_error(exn)
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   302
          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
   303
      }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   304
      progress.stop
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   305
      context.remove_task(task)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   306
    }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   307
    def start { thread }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   308
    def join { thread.join }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   309
  }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   310
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   311
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   312
  /* server info */
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   313
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   314
  val localhost_name: String = "127.0.0.1"
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   315
  def localhost: InetAddress = InetAddress.getByName(localhost_name)
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   316
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   317
  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
   318
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   319
  def print(port: Int, password: String): String =
69461
be142f577da6 tuned signature;
wenzelm
parents: 69460
diff changeset
   320
    print_address(port) + " (password " + quote(password) + ")"
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
  object Info
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   323
  {
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   324
    private val Pattern =
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   325
      ("""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
   326
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   327
    def parse(s: String): Option[Info] =
69460
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   328
      s match {
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   329
        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
   330
        case _ => None
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   331
      }
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   332
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   333
    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
   334
      new Info(name, port, password)
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
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   337
  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
   338
  {
69461
be142f577da6 tuned signature;
wenzelm
parents: 69460
diff changeset
   339
    def address: String = print_address(port)
69460
5ffe7e17f770 clarified signature, e.g. for re-use by other servers;
wenzelm
parents: 69458
diff changeset
   340
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   341
    override def toString: String =
67821
82fb12061069 more uniform output: this may be parsed by another program;
wenzelm
parents: 67820
diff changeset
   342
      "server " + quote(name) + " = " + print(port, password)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   343
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   344
    def connection(): Connection =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   345
    {
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   346
      val connection = Connection(new Socket(localhost, port))
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   347
      connection.write_message(password)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   348
      connection
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   349
    }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   350
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   351
    def active(): Boolean =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   352
      try {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   353
        using(connection())(connection =>
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   354
          {
67832
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   355
            connection.set_timeout(Time.seconds(2.0))
67867
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   356
            connection.read_message() match {
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   357
              case Some(Reply(Reply.OK, _)) => true
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   358
              case _ => false
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   359
            }
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   360
          })
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   361
      }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   362
      catch {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   363
        case _: IOException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   364
        case _: SocketException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   365
        case _: SocketTimeoutException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   366
      }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   367
  }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   368
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   369
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   370
  /* per-user servers */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   371
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   372
  val default_name = "isabelle"
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   373
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   374
  object Data
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   375
  {
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   376
    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   377
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66353
diff changeset
   378
    val name = SQL.Column.string("name").make_primary_key
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   379
    val port = SQL.Column.int("port")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   380
    val password = SQL.Column.string("password")
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   381
    val table = SQL.Table("isabelle_servers", List(name, port, password))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   382
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   383
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   384
  def list(db: SQLite.Database): List[Info] =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   385
    if (db.tables.contains(Data.table.name)) {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   386
      db.using_statement(Data.table.select())(stmt =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   387
        stmt.execute_query().iterator(res =>
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   388
          Info(
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   389
            res.string(Data.name),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   390
            res.int(Data.port),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   391
            res.string(Data.password))).toList.sortBy(_.name))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   392
    }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   393
    else Nil
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   394
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   395
  def find(db: SQLite.Database, name: String): Option[Info] =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   396
    list(db).find(server_info => server_info.name == name && server_info.active)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   397
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   398
  def init(
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   399
    name: String = default_name,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   400
    port: Int = 0,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   401
    existing_server: Boolean = false,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   402
    log: Logger = No_Logger): (Info, Option[Server]) =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   403
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   404
    using(SQLite.open_database(Data.database))(db =>
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   405
      {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   406
        db.transaction {
71114
6cfec8029831 clarified signature;
wenzelm
parents: 69818
diff changeset
   407
          Isabelle_System.chmod("600", Data.database)
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   408
          db.create_table(Data.table)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   409
          list(db).filterNot(_.active).foreach(server_info =>
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   410
            db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   411
              _.execute))
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   412
        }
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   413
        db.transaction {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   414
          find(db, name) match {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   415
            case Some(server_info) => (server_info, None)
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   416
            case None =>
67821
82fb12061069 more uniform output: this may be parsed by another program;
wenzelm
parents: 67820
diff changeset
   417
              if (existing_server) error("Isabelle server " + quote(name) + " not running")
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   418
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   419
              val server = new Server(port, log)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   420
              val server_info = Info(name, server.port, server.password)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   421
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   422
              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   423
              db.using_statement(Data.table.insert())(stmt =>
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   424
              {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   425
                stmt.string(1) = server_info.name
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   426
                stmt.int(2) = server_info.port
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   427
                stmt.string(3) = server_info.password
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   428
                stmt.execute()
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   429
              })
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   430
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   431
              server.start
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   432
              (server_info, Some(server))
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   433
          }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   434
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   435
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   436
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   437
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   438
  def exit(name: String = default_name): Boolean =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   439
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   440
    using(SQLite.open_database(Data.database))(db =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   441
      db.transaction {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   442
        find(db, name) match {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   443
          case Some(server_info) =>
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   444
            using(server_info.connection())(_.write_message("shutdown"))
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   445
            while(server_info.active) { Thread.sleep(50) }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   446
            true
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   447
          case None => false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   448
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   449
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   450
  }
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
  /* Isabelle tool wrapper */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   454
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   455
  val isabelle_tool =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   456
    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   457
    {
67806
bd4c440c8be7 option for console interaction;
wenzelm
parents: 67805
diff changeset
   458
      var console = false
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   459
      var log_file: Option[Path] = None
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   460
      var operation_list = false
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   461
      var operation_exit = false
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   462
      var name = default_name
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   463
      var port = 0
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   464
      var existing_server = false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   465
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   466
      val getopts =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   467
        Getopts("""
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   468
Usage: isabelle server [OPTIONS]
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   469
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   470
  Options are:
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   471
    -L FILE      logging on FILE
67875
641315ebed02 tuned options;
wenzelm
parents: 67873
diff changeset
   472
    -c           console interaction with specified server
67904
465f43a9f780 documentation for the Isabelle server;
wenzelm
parents: 67903
diff changeset
   473
    -l           list servers (alternative operation)
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   474
    -n NAME      explicit server name (default: """ + default_name + """)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   475
    -p PORT      explicit server port
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   476
    -s           assume existing server, no implicit startup
67904
465f43a9f780 documentation for the Isabelle server;
wenzelm
parents: 67903
diff changeset
   477
    -x           exit specified server (alternative operation)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   478
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   479
  Manage resident Isabelle servers.
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   480
""",
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   481
          "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
67875
641315ebed02 tuned options;
wenzelm
parents: 67873
diff changeset
   482
          "c" -> (_ => console = true),
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   483
          "l" -> (_ => operation_list = true),
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   484
          "n:" -> (arg => name = arg),
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   485
          "p:" -> (arg => port = Value.Int.parse(arg)),
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   486
          "s" -> (_ => existing_server = true),
67876
cc4832285c38 proper options;
wenzelm
parents: 67875
diff changeset
   487
          "x" -> (_ => operation_exit = true))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   488
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   489
      val more_args = getopts(args)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   490
      if (more_args.nonEmpty) getopts.usage()
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   491
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   492
      if (operation_list) {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   493
        for {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   494
          server_info <- using(SQLite.open_database(Data.database))(list(_))
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   495
          if server_info.active
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   496
        } Output.writeln(server_info.toString, stdout = true)
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   497
      }
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   498
      else if (operation_exit) {
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   499
        val ok = Server.exit(name)
69033
c5db368833b1 proper return code for runtime failure;
wenzelm
parents: 69012
diff changeset
   500
        sys.exit(if (ok) 0 else 2)
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   501
      }
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   502
      else {
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   503
        val log = Logger.make(log_file)
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   504
        val (server_info, server) =
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   505
          init(name, port = port, existing_server = existing_server, log = log)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   506
        Output.writeln(server_info.toString, stdout = true)
67834
wenzelm
parents: 67833
diff changeset
   507
        if (console) {
wenzelm
parents: 67833
diff changeset
   508
          using(server_info.connection())(connection => connection.tty_loop().join)
wenzelm
parents: 67833
diff changeset
   509
        }
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   510
        server.foreach(_.join)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   511
      }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   512
    })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   513
}
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   514
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   515
class Server private(_port: Int, val log: Logger)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   516
{
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   517
  server =>
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   518
69463
6439c9024dcc clarified signature;
wenzelm
parents: 69461
diff changeset
   519
  private val server_socket = new ServerSocket(_port, 50, Server.localhost)
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   520
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   521
  private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   522
  def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   523
  def the_session(id: UUID.T): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   524
  def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) }
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   525
  def remove_session(id: UUID.T): Headless.Session =
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   526
  {
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   527
    _sessions.change_result(sessions =>
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   528
      sessions.get(id) match {
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   529
        case Some(session) => (session, sessions - id)
67883
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
   530
        case None => err_session(id)
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   531
      })
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
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   534
  def shutdown()
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   535
  {
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   536
    server_socket.close
67791
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   537
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   538
    val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   539
    for ((_, session) <- sessions) {
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   540
      try {
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   541
        val result = session.stop()
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   542
        if (!result.ok) log("Session shutdown failed: return code " + result.rc)
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   543
      }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   544
      catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   545
    }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   546
  }
67791
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   547
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   548
  def port: Int = server_socket.getLocalPort
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69451
diff changeset
   549
  val password: String = UUID.random_string()
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   550
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   551
  override def toString: String = Server.print(port, password)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   552
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   553
  private def handle(connection: Server.Connection)
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   554
  {
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   555
    using(new Server.Context(server, connection))(context =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   556
    {
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   557
      if (connection.read_password(password)) {
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   558
        connection.reply_ok(
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   559
          JSON.Object(
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   560
            "isabelle_id" -> Isabelle_System.isabelle_id(),
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   561
            "isabelle_version" -> Distribution.version))
67867
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   562
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   563
        var finished = false
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   564
        while (!finished) {
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   565
          connection.read_message() match {
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   566
            case None => finished = true
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   567
            case Some("") => context.notify("Command 'help' provides list of commands")
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   568
            case Some(msg) =>
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   569
              val (name, argument) = Server.Argument.split(msg)
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   570
              name match {
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   571
                case Server.Command(cmd) =>
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   572
                  argument match {
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   573
                    case Server.Argument(arg) =>
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   574
                      if (cmd.isDefinedAt((context, arg))) {
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   575
                        Exn.capture { cmd((context, arg)) } match {
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   576
                          case Exn.Res(task: Server.Task) =>
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   577
                            connection.reply_ok(JSON.Object(task.ident))
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   578
                            task.start
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   579
                          case Exn.Res(res) => connection.reply_ok(res)
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   580
                          case Exn.Exn(exn) =>
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   581
                            val err = Server.json_error(exn)
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   582
                            if (err.isEmpty) throw exn else connection.reply_error(err)
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   583
                        }
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   584
                      }
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   585
                      else {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   586
                        connection.reply_error_message(
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   587
                          "Bad argument for command " + Library.single_quote(name),
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   588
                          "argument" -> argument)
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   589
                      }
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   590
                    case _ =>
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   591
                      connection.reply_error_message(
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   592
                        "Malformed argument for command " + Library.single_quote(name),
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   593
                        "argument" -> argument)
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   594
                  }
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   595
                case _ => connection.reply_error("Bad command " + Library.single_quote(name))
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   596
              }
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   597
          }
69464
2323dce4a0db clarified protocol;
wenzelm
parents: 69463
diff changeset
   598
        }
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   599
      }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   600
    })
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   601
  }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   602
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   603
  private lazy val server_thread: Thread =
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   604
    Standard_Thread.fork("server") {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   605
      var finished = false
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   606
      while (!finished) {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   607
        Exn.capture(server_socket.accept) match {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   608
          case Exn.Res(socket) =>
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   609
            Standard_Thread.fork("server_connection")
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   610
              { using(Server.Connection(socket))(handle(_)) }
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   611
          case Exn.Exn(_) => finished = true
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   612
        }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   613
      }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   614
    }
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   615
67790
1babcc248be0 clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents: 67789
diff changeset
   616
  def start { server_thread }
1babcc248be0 clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents: 67789
diff changeset
   617
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   618
  def join { server_thread.join; shutdown() }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   619
}