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