src/Pure/Tools/server.scala
author wenzelm
Tue, 11 Dec 2018 19:25:35 +0100
changeset 69448 51e696887b81
parent 69393 ed0824ef337e
child 69451 387894c2fb2c
permissions -rw-r--r--
more uniform multi-language operations;
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
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   183
    def read_message(): Option[String] =
69448
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69393
diff changeset
   184
      Byte_Message.read_line_message(in).map(_.text)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   185
69448
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69393
diff changeset
   186
    def write_message(msg: String): Unit =
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69393
diff changeset
   187
      out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   188
67859
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   189
    def reply(r: Reply.Value, arg: Any)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   190
    {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   191
      val argument = Argument.print(arg)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   192
      write_message(if (argument == "") r.toString else r.toString + " " + argument)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   193
    }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   194
67859
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   195
    def reply_ok(arg: Any) { reply(Reply.OK, arg) }
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   196
    def reply_error(arg: Any) { reply(Reply.ERROR, arg) }
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   197
    def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   198
      reply_error(Reply.error_message(message) ++ more)
67801
8f5f5fbe291b added Reply.NOTE for asynchronous notifications;
wenzelm
parents: 67800
diff changeset
   199
67859
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   200
    def notify(arg: Any) { reply(Reply.NOTE, arg) }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   201
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   202
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   203
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   204
  /* context with output channels */
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   205
67878
15027fb50a0c clarified signature;
wenzelm
parents: 67876
diff changeset
   206
  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
   207
    extends AutoCloseable
67839
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 =>
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   210
67859
612846bff1ea tuned signature;
wenzelm
parents: 67857
diff changeset
   211
    def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
67840
a9d450fc5a49 tuned signature;
wenzelm
parents: 67839
diff changeset
   212
    def notify(arg: Any) { connection.notify(arg) }
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   213
    def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
67901
3e6864cf387f more explicit error messages;
wenzelm
parents: 67891
diff changeset
   214
      notify(Reply.message(msg, kind = kind) ++ more)
67857
262d62a4c32b more informative error with JSON result;
wenzelm
parents: 67850
diff changeset
   215
    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
   216
    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
   217
    def error_message(msg: String, more: JSON.Object.Entry*): Unit =
67911
3cda747493d8 clarified markup according to common Command.Results;
wenzelm
parents: 67904
diff changeset
   218
      message(Markup.ERROR, msg, more:_*)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   219
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   220
    def progress(more: JSON.Object.Entry*): Connection_Progress =
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   221
      new Connection_Progress(context, more:_*)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   222
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   223
    override def toString: String = connection.toString
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   224
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   225
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   226
    /* asynchronous tasks */
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   227
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   228
    private val _tasks = Synchronized(Set.empty[Task])
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
    def make_task(body: Task => JSON.Object.T): Task =
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   231
    {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   232
      val task = new Task(context, body)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   233
      _tasks.change(_ + task)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   234
      task
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   235
    }
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
    def remove_task(task: Task): Unit =
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
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   240
    def cancel_task(id: UUID): Unit =
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   241
      _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
   242
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   243
    def close()
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   244
    {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   245
      while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) }))
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   246
      { _tasks.value.foreach(_.join) }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   247
    }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   248
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   249
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   250
  class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   251
    extends Progress
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   252
  {
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   253
    override def echo(msg: String): Unit = context.writeln(msg, more:_*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   254
    override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   255
    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
   256
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   257
    override def theory(theory: Progress.Theory)
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   258
    {
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   259
      val entries: List[JSON.Object.Entry] =
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   260
        List("theory" -> theory.theory, "session" -> theory.session) :::
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   261
          (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) })
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   262
      context.writeln(theory.message, entries ::: more.toList:_*)
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68904
diff changeset
   263
    }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   264
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68888
diff changeset
   265
    override def nodes_status(nodes_status: Document_Status.Nodes_Status)
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   266
    {
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68888
diff changeset
   267
      val json =
68904
09151c54aaac tuned signature;
wenzelm
parents: 68903
diff changeset
   268
        for ((name, node_status) <- nodes_status.present)
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68888
diff changeset
   269
          yield name.json + ("status" -> nodes_status(name).json)
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   270
      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
   271
    }
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68530
diff changeset
   272
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   273
    @volatile private var is_stopped = false
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   274
    override def stopped: Boolean = is_stopped
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   275
    def stop { is_stopped = true }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   276
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   277
    override def toString: String = context.toString
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   278
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   279
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   280
  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
   281
  {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   282
    task =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   283
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   284
    val id: UUID = UUID()
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   285
    val ident: JSON.Object.Entry = ("task" -> id.toString)
67860
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
    val progress: Connection_Progress = context.progress(ident)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   288
    def cancel { progress.stop }
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
    private lazy val thread = Standard_Thread.fork("server_task")
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
      Exn.capture { body(task) } match {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   293
        case Exn.Res(res) =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   294
          context.reply(Reply.FINISHED, res + ident)
67891
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   295
        case Exn.Exn(exn) =>
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   296
          val err = json_error(exn)
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   297
          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
   298
      }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   299
      progress.stop
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   300
      context.remove_task(task)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   301
    }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   302
    def start { thread }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   303
    def join { thread.join }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   304
  }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   305
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   306
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   307
  /* server info */
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   308
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   309
  sealed case class Info(name: String, port: Int, password: String)
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   310
  {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   311
    override def toString: String =
67821
82fb12061069 more uniform output: this may be parsed by another program;
wenzelm
parents: 67820
diff changeset
   312
      "server " + quote(name) + " = " + print(port, password)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   313
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   314
    def connection(): Connection =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   315
    {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   316
      val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   317
      connection.write_message(password)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   318
      connection
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   319
    }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   320
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   321
    def active(): Boolean =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   322
      try {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   323
        using(connection())(connection =>
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   324
          {
67832
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   325
            connection.set_timeout(Time.seconds(2.0))
67867
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   326
            connection.read_message() match {
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   327
              case Some(Reply(Reply.OK, _)) => true
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   328
              case _ => false
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   329
            }
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   330
          })
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   331
      }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   332
      catch {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   333
        case _: IOException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   334
        case _: SocketException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   335
        case _: SocketTimeoutException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   336
      }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   337
  }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   338
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   339
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   340
  /* per-user servers */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   341
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   342
  val default_name = "isabelle"
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   343
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   344
  def print(port: Int, password: String): String =
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   345
    "127.0.0.1:" + port + " (password " + quote(password) + ")"
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   346
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   347
  object Data
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   348
  {
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   349
    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   350
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66353
diff changeset
   351
    val name = SQL.Column.string("name").make_primary_key
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   352
    val port = SQL.Column.int("port")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   353
    val password = SQL.Column.string("password")
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   354
    val table = SQL.Table("isabelle_servers", List(name, port, password))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   355
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   356
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   357
  def list(db: SQLite.Database): List[Info] =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   358
    if (db.tables.contains(Data.table.name)) {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   359
      db.using_statement(Data.table.select())(stmt =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   360
        stmt.execute_query().iterator(res =>
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   361
          Info(
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   362
            res.string(Data.name),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   363
            res.int(Data.port),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   364
            res.string(Data.password))).toList.sortBy(_.name))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   365
    }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   366
    else Nil
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   367
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   368
  def find(db: SQLite.Database, name: String): Option[Info] =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   369
    list(db).find(server_info => server_info.name == name && server_info.active)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   370
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   371
  def init(
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   372
    name: String = default_name,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   373
    port: Int = 0,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   374
    existing_server: Boolean = false,
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   375
    log: Logger = No_Logger): (Info, Option[Server]) =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   376
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   377
    using(SQLite.open_database(Data.database))(db =>
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   378
      {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   379
        db.transaction {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   380
          Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   381
          db.create_table(Data.table)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   382
          list(db).filterNot(_.active).foreach(server_info =>
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   383
            db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   384
              _.execute))
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   385
        }
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   386
        db.transaction {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   387
          find(db, name) match {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   388
            case Some(server_info) => (server_info, None)
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   389
            case None =>
67821
82fb12061069 more uniform output: this may be parsed by another program;
wenzelm
parents: 67820
diff changeset
   390
              if (existing_server) error("Isabelle server " + quote(name) + " not running")
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   391
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   392
              val server = new Server(port, log)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   393
              val server_info = Info(name, server.port, server.password)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   394
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   395
              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   396
              db.using_statement(Data.table.insert())(stmt =>
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   397
              {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   398
                stmt.string(1) = server_info.name
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   399
                stmt.int(2) = server_info.port
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   400
                stmt.string(3) = server_info.password
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   401
                stmt.execute()
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   402
              })
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   403
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   404
              server.start
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   405
              (server_info, Some(server))
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   406
          }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   407
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   408
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   409
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   410
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   411
  def exit(name: String = default_name): Boolean =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   412
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   413
    using(SQLite.open_database(Data.database))(db =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   414
      db.transaction {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   415
        find(db, name) match {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   416
          case Some(server_info) =>
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   417
            using(server_info.connection())(_.write_message("shutdown"))
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   418
            while(server_info.active) { Thread.sleep(50) }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   419
            true
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   420
          case None => false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   421
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   422
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   423
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   424
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   425
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   426
  /* Isabelle tool wrapper */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   427
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   428
  val isabelle_tool =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   429
    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   430
    {
67806
bd4c440c8be7 option for console interaction;
wenzelm
parents: 67805
diff changeset
   431
      var console = false
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   432
      var log_file: Option[Path] = None
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   433
      var operation_list = false
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   434
      var operation_exit = false
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   435
      var name = default_name
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   436
      var port = 0
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   437
      var existing_server = false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   438
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   439
      val getopts =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   440
        Getopts("""
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   441
Usage: isabelle server [OPTIONS]
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   442
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   443
  Options are:
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   444
    -L FILE      logging on FILE
67875
641315ebed02 tuned options;
wenzelm
parents: 67873
diff changeset
   445
    -c           console interaction with specified server
67904
465f43a9f780 documentation for the Isabelle server;
wenzelm
parents: 67903
diff changeset
   446
    -l           list servers (alternative operation)
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   447
    -n NAME      explicit server name (default: """ + default_name + """)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   448
    -p PORT      explicit server port
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   449
    -s           assume existing server, no implicit startup
67904
465f43a9f780 documentation for the Isabelle server;
wenzelm
parents: 67903
diff changeset
   450
    -x           exit specified server (alternative operation)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   451
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   452
  Manage resident Isabelle servers.
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   453
""",
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   454
          "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
67875
641315ebed02 tuned options;
wenzelm
parents: 67873
diff changeset
   455
          "c" -> (_ => console = true),
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   456
          "l" -> (_ => operation_list = true),
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   457
          "n:" -> (arg => name = arg),
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   458
          "p:" -> (arg => port = Value.Int.parse(arg)),
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   459
          "s" -> (_ => existing_server = true),
67876
cc4832285c38 proper options;
wenzelm
parents: 67875
diff changeset
   460
          "x" -> (_ => operation_exit = true))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   461
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   462
      val more_args = getopts(args)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   463
      if (more_args.nonEmpty) getopts.usage()
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   464
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   465
      if (operation_list) {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   466
        for {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   467
          server_info <- using(SQLite.open_database(Data.database))(list(_))
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   468
          if server_info.active
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   469
        } Output.writeln(server_info.toString, stdout = true)
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   470
      }
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   471
      else if (operation_exit) {
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   472
        val ok = Server.exit(name)
69033
c5db368833b1 proper return code for runtime failure;
wenzelm
parents: 69012
diff changeset
   473
        sys.exit(if (ok) 0 else 2)
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   474
      }
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   475
      else {
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   476
        val log = Logger.make(log_file)
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   477
        val (server_info, server) =
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   478
          init(name, port = port, existing_server = existing_server, log = log)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   479
        Output.writeln(server_info.toString, stdout = true)
67834
wenzelm
parents: 67833
diff changeset
   480
        if (console) {
wenzelm
parents: 67833
diff changeset
   481
          using(server_info.connection())(connection => connection.tty_loop().join)
wenzelm
parents: 67833
diff changeset
   482
        }
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   483
        server.foreach(_.join)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   484
      }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   485
    })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   486
}
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   487
67870
586be47e00b3 clarified server log;
wenzelm
parents: 67869
diff changeset
   488
class Server private(_port: Int, val log: Logger)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   489
{
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   490
  server =>
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   491
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   492
  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   493
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68957
diff changeset
   494
  private val _sessions = Synchronized(Map.empty[UUID, Headless.Session])
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   495
  def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68957
diff changeset
   496
  def the_session(id: UUID): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
c91d14ab065f clarified modules;
wenzelm
parents: 68957
diff changeset
   497
  def add_session(entry: (UUID, Headless.Session)) { _sessions.change(_ + entry) }
c91d14ab065f clarified modules;
wenzelm
parents: 68957
diff changeset
   498
  def remove_session(id: UUID): Headless.Session =
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   499
  {
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   500
    _sessions.change_result(sessions =>
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   501
      sessions.get(id) match {
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   502
        case Some(session) => (session, sessions - id)
67883
171e7735ce25 support for "use_theories";
wenzelm
parents: 67878
diff changeset
   503
        case None => err_session(id)
67871
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   504
      })
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   505
  }
195ff117894c store session: per Server/Context, not Connection;
wenzelm
parents: 67870
diff changeset
   506
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   507
  def shutdown()
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   508
  {
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   509
    server_socket.close
67791
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   510
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   511
    val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   512
    for ((_, session) <- sessions) {
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   513
      try {
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   514
        val result = session.stop()
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   515
        if (!result.ok) log("Session shutdown failed: return code " + result.rc)
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   516
      }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   517
      catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   518
    }
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   519
  }
67791
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   520
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   521
  def port: Int = server_socket.getLocalPort
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   522
  val password: String = UUID().toString
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   523
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   524
  override def toString: String = Server.print(port, password)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   525
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   526
  private def handle(connection: Server.Connection)
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   527
  {
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   528
    using(new Server.Context(server, connection))(context =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   529
    {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   530
      connection.read_message() match {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   531
        case Some(msg) if msg == password =>
67867
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   532
          connection.reply_ok(
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   533
            JSON.Object(
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   534
              "isabelle_id" -> Isabelle_System.isabelle_id(),
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   535
              "isabelle_version" -> Distribution.version))
fb66d099adb2 clarified message;
wenzelm
parents: 67861
diff changeset
   536
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   537
          var finished = false
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   538
          while (!finished) {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   539
            connection.read_message() match {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   540
              case None => finished = true
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   541
              case Some("") => context.notify("Command 'help' provides list of commands")
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   542
              case Some(msg) =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   543
                val (name, argument) = Server.Argument.split(msg)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   544
                name match {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   545
                  case Server.Command(cmd) =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   546
                    argument match {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   547
                      case Server.Argument(arg) =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   548
                        if (cmd.isDefinedAt((context, arg))) {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   549
                          Exn.capture { cmd((context, arg)) } match {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   550
                            case Exn.Res(task: Server.Task) =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   551
                              connection.reply_ok(JSON.Object(task.ident))
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   552
                              task.start
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   553
                            case Exn.Res(res) => connection.reply_ok(res)
67891
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   554
                            case Exn.Exn(exn) =>
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   555
                              val err = Server.json_error(exn)
4f383cd54f69 clarified exception handling: include interrupts;
wenzelm
parents: 67886
diff changeset
   556
                              if (err.isEmpty) throw exn else connection.reply_error(err)
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   557
                          }
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   558
                        }
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   559
                        else {
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   560
                          connection.reply_error_message(
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   561
                            "Bad argument for command " + Library.single_quote(name),
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   562
                            "argument" -> argument)
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   563
                        }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   564
                      case _ =>
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   565
                        connection.reply_error_message(
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   566
                          "Malformed argument for command " + Library.single_quote(name),
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   567
                          "argument" -> argument)
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   568
                    }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   569
                  case _ => connection.reply_error("Bad command " + Library.single_quote(name))
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   570
                }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   571
            }
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   572
          }
67860
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   573
        case _ =>
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   574
      }
5a6c483269f3 support for asynchronous tasks, with "cancel" command;
wenzelm
parents: 67859
diff changeset
   575
    })
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   576
  }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   577
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   578
  private lazy val server_thread: Thread =
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   579
    Standard_Thread.fork("server") {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   580
      var finished = false
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   581
      while (!finished) {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   582
        Exn.capture(server_socket.accept) match {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   583
          case Exn.Res(socket) =>
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   584
            Standard_Thread.fork("server_connection")
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   585
              { using(Server.Connection(socket))(handle(_)) }
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   586
          case Exn.Exn(_) => finished = true
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   587
        }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   588
      }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   589
    }
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   590
67790
1babcc248be0 clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents: 67789
diff changeset
   591
  def start { server_thread }
1babcc248be0 clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents: 67789
diff changeset
   592
67902
c88044b10bbf clarified server shutdown: stop all sessions;
wenzelm
parents: 67901
diff changeset
   593
  def join { server_thread.join; shutdown() }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   594
}