# HG changeset patch
# User wenzelm
# Date 1521146674 -3600
# Node ID 586be47e00b30b019cfb693c36382fea65e43796
# Parent  8cb4fef5837900585c88a09b5a06acf15986a53f
clarified server log;
tuned options;

diff -r 8cb4fef58379 -r 586be47e00b3 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Mar 15 21:26:39 2018 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Mar 15 21:44:34 2018 +0100
@@ -457,7 +457,6 @@
   val STDOUT = "stdout"
   val STDERR = "stderr"
   val EXIT = "exit"
-  val LOGGER = "logger"
 
   val WRITELN_MESSAGE = "writeln_message"
   val STATE_MESSAGE = "state_message"
diff -r 8cb4fef58379 -r 586be47e00b3 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Mar 15 21:26:39 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 15 21:44:34 2018 +0100
@@ -78,7 +78,7 @@
               context.make_task(task =>
                 {
                   val (res, session_id, session) =
-                    Server_Commands.Session_Start.command(task.progress, args, log = context.logger())
+                    Server_Commands.Session_Start.command(task.progress, args, log = context.log)
                   // FIXME store session in context
                   res
                 })
@@ -196,12 +196,11 @@
     def error_message(msg: String, more: JSON.Object.Entry*): Unit =
       message(Markup.ERROR_MESSAGE, msg, more:_*)
 
-    def logger(more: JSON.Object.Entry*): Connection_Logger =
-      new Connection_Logger(context, more:_*)
-
     def progress(more: JSON.Object.Entry*): Connection_Progress =
       new Connection_Progress(context, more:_*)
 
+    def log: Logger = server.log
+
     override def toString: String = connection.toString
 
 
@@ -229,14 +228,6 @@
     }
   }
 
-  class Connection_Logger private[Server](context: Context, more: JSON.Object.Entry*)
-    extends Logger
-  {
-    def apply(msg: => String): Unit = context.message(Markup.LOGGER, msg, more:_*)
-
-    override def toString: String = context.toString
-  }
-
   class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
     extends Progress
   {
@@ -261,8 +252,6 @@
     val id: String = Library.UUID()
     val ident: JSON.Object.Entry = ("task" -> id)
 
-    val logger: Logger = context.logger(ident)
-
     val progress: Connection_Progress = context.progress(ident)
     def cancel { progress.stop }
 
@@ -349,8 +338,11 @@
   def find(db: SQLite.Database, name: String): Option[Info] =
     list(db).find(server_info => server_info.name == name && server_info.active)
 
-  def init(name: String = default_name, port: Int = 0, existing_server: Boolean = false)
-    : (Info, Option[Server]) =
+  def init(
+    name: String = default_name,
+    port: Int = 0,
+    existing_server: Boolean = false,
+    log: Logger = No_Logger): (Info, Option[Server]) =
   {
     using(SQLite.open_database(Data.database))(db =>
       {
@@ -367,7 +359,7 @@
             case None =>
               if (existing_server) error("Isabelle server " + quote(name) + " not running")
 
-              val server = new Server(port)
+              val server = new Server(port, log)
               val server_info = Info(name, server.port, server.password)
 
               db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
@@ -407,6 +399,7 @@
     Isabelle_Tool("server", "manage resident Isabelle servers", args =>
     {
       var console = false
+      var log_file: Option[Path] = None
       var operation_list = false
       var operation_exit = false
       var name = default_name
@@ -419,20 +412,22 @@
 
   Options are:
     -C           console interaction with specified server
-    -L           list servers (exclusive operation)
-    -X           exit specified server (exclusive operation)
+    -L FILE      logging on FILE
+    -l           list servers (exclusive operation)
     -n NAME      explicit server name (default: """ + default_name + """)
     -p PORT      explicit server port
     -s           assume existing server, no implicit startup
+    -x           exit specified server (exclusive operation)
 
   Manage resident Isabelle servers.
 """,
           "C" -> (_ => console = true),
-          "L" -> (_ => operation_list = true),
-          "X" -> (_ => operation_exit = true),
+          "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
+          "l" -> (_ => operation_list = true),
           "n:" -> (arg => name = arg),
           "p:" -> (arg => port = Value.Int.parse(arg)),
-          "s" -> (_ => existing_server = true))
+          "s" -> (_ => existing_server = true),
+          "X" -> (_ => operation_exit = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
@@ -448,7 +443,9 @@
         sys.exit(if (ok) 0 else 1)
       }
       else {
-        val (server_info, server) = init(name, port = port, existing_server = existing_server)
+        val log = Logger.make(log_file)
+        val (server_info, server) =
+          init(name, port = port, existing_server = existing_server, log = log)
         Output.writeln(server_info.toString, stdout = true)
         if (console) {
           using(server_info.connection())(connection => connection.tty_loop().join)
@@ -458,7 +455,7 @@
     })
 }
 
-class Server private(_port: Int)
+class Server private(_port: Int, val log: Logger)
 {
   server =>
 
diff -r 8cb4fef58379 -r 586be47e00b3 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Mar 15 21:26:39 2018 +0100
+++ b/src/Tools/VSCode/src/server.scala	Thu Mar 15 21:44:34 2018 +0100
@@ -45,7 +45,7 @@
 
   Options are:
     -A           explore theory name space of all known sessions (potentially slow)
-    -L FILE      enable logging on FILE
+    -L FILE      logging on FILE
     -d DIR       include session directory
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
     -m MODE      add print mode for output