clarified server log;
authorwenzelm
Thu Mar 15 21:44:34 2018 +0100 (21 months ago ago)
changeset 67870586be47e00b3
parent 67869 8cb4fef58379
child 67871 195ff117894c
clarified server log;
tuned options;
src/Pure/PIDE/markup.scala
src/Pure/Tools/server.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Mar 15 21:26:39 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Mar 15 21:44:34 2018 +0100
     1.3 @@ -457,7 +457,6 @@
     1.4    val STDOUT = "stdout"
     1.5    val STDERR = "stderr"
     1.6    val EXIT = "exit"
     1.7 -  val LOGGER = "logger"
     1.8  
     1.9    val WRITELN_MESSAGE = "writeln_message"
    1.10    val STATE_MESSAGE = "state_message"
     2.1 --- a/src/Pure/Tools/server.scala	Thu Mar 15 21:26:39 2018 +0100
     2.2 +++ b/src/Pure/Tools/server.scala	Thu Mar 15 21:44:34 2018 +0100
     2.3 @@ -78,7 +78,7 @@
     2.4                context.make_task(task =>
     2.5                  {
     2.6                    val (res, session_id, session) =
     2.7 -                    Server_Commands.Session_Start.command(task.progress, args, log = context.logger())
     2.8 +                    Server_Commands.Session_Start.command(task.progress, args, log = context.log)
     2.9                    // FIXME store session in context
    2.10                    res
    2.11                  })
    2.12 @@ -196,12 +196,11 @@
    2.13      def error_message(msg: String, more: JSON.Object.Entry*): Unit =
    2.14        message(Markup.ERROR_MESSAGE, msg, more:_*)
    2.15  
    2.16 -    def logger(more: JSON.Object.Entry*): Connection_Logger =
    2.17 -      new Connection_Logger(context, more:_*)
    2.18 -
    2.19      def progress(more: JSON.Object.Entry*): Connection_Progress =
    2.20        new Connection_Progress(context, more:_*)
    2.21  
    2.22 +    def log: Logger = server.log
    2.23 +
    2.24      override def toString: String = connection.toString
    2.25  
    2.26  
    2.27 @@ -229,14 +228,6 @@
    2.28      }
    2.29    }
    2.30  
    2.31 -  class Connection_Logger private[Server](context: Context, more: JSON.Object.Entry*)
    2.32 -    extends Logger
    2.33 -  {
    2.34 -    def apply(msg: => String): Unit = context.message(Markup.LOGGER, msg, more:_*)
    2.35 -
    2.36 -    override def toString: String = context.toString
    2.37 -  }
    2.38 -
    2.39    class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
    2.40      extends Progress
    2.41    {
    2.42 @@ -261,8 +252,6 @@
    2.43      val id: String = Library.UUID()
    2.44      val ident: JSON.Object.Entry = ("task" -> id)
    2.45  
    2.46 -    val logger: Logger = context.logger(ident)
    2.47 -
    2.48      val progress: Connection_Progress = context.progress(ident)
    2.49      def cancel { progress.stop }
    2.50  
    2.51 @@ -349,8 +338,11 @@
    2.52    def find(db: SQLite.Database, name: String): Option[Info] =
    2.53      list(db).find(server_info => server_info.name == name && server_info.active)
    2.54  
    2.55 -  def init(name: String = default_name, port: Int = 0, existing_server: Boolean = false)
    2.56 -    : (Info, Option[Server]) =
    2.57 +  def init(
    2.58 +    name: String = default_name,
    2.59 +    port: Int = 0,
    2.60 +    existing_server: Boolean = false,
    2.61 +    log: Logger = No_Logger): (Info, Option[Server]) =
    2.62    {
    2.63      using(SQLite.open_database(Data.database))(db =>
    2.64        {
    2.65 @@ -367,7 +359,7 @@
    2.66              case None =>
    2.67                if (existing_server) error("Isabelle server " + quote(name) + " not running")
    2.68  
    2.69 -              val server = new Server(port)
    2.70 +              val server = new Server(port, log)
    2.71                val server_info = Info(name, server.port, server.password)
    2.72  
    2.73                db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
    2.74 @@ -407,6 +399,7 @@
    2.75      Isabelle_Tool("server", "manage resident Isabelle servers", args =>
    2.76      {
    2.77        var console = false
    2.78 +      var log_file: Option[Path] = None
    2.79        var operation_list = false
    2.80        var operation_exit = false
    2.81        var name = default_name
    2.82 @@ -419,20 +412,22 @@
    2.83  
    2.84    Options are:
    2.85      -C           console interaction with specified server
    2.86 -    -L           list servers (exclusive operation)
    2.87 -    -X           exit specified server (exclusive operation)
    2.88 +    -L FILE      logging on FILE
    2.89 +    -l           list servers (exclusive operation)
    2.90      -n NAME      explicit server name (default: """ + default_name + """)
    2.91      -p PORT      explicit server port
    2.92      -s           assume existing server, no implicit startup
    2.93 +    -x           exit specified server (exclusive operation)
    2.94  
    2.95    Manage resident Isabelle servers.
    2.96  """,
    2.97            "C" -> (_ => console = true),
    2.98 -          "L" -> (_ => operation_list = true),
    2.99 -          "X" -> (_ => operation_exit = true),
   2.100 +          "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
   2.101 +          "l" -> (_ => operation_list = true),
   2.102            "n:" -> (arg => name = arg),
   2.103            "p:" -> (arg => port = Value.Int.parse(arg)),
   2.104 -          "s" -> (_ => existing_server = true))
   2.105 +          "s" -> (_ => existing_server = true),
   2.106 +          "X" -> (_ => operation_exit = true))
   2.107  
   2.108        val more_args = getopts(args)
   2.109        if (more_args.nonEmpty) getopts.usage()
   2.110 @@ -448,7 +443,9 @@
   2.111          sys.exit(if (ok) 0 else 1)
   2.112        }
   2.113        else {
   2.114 -        val (server_info, server) = init(name, port = port, existing_server = existing_server)
   2.115 +        val log = Logger.make(log_file)
   2.116 +        val (server_info, server) =
   2.117 +          init(name, port = port, existing_server = existing_server, log = log)
   2.118          Output.writeln(server_info.toString, stdout = true)
   2.119          if (console) {
   2.120            using(server_info.connection())(connection => connection.tty_loop().join)
   2.121 @@ -458,7 +455,7 @@
   2.122      })
   2.123  }
   2.124  
   2.125 -class Server private(_port: Int)
   2.126 +class Server private(_port: Int, val log: Logger)
   2.127  {
   2.128    server =>
   2.129  
     3.1 --- a/src/Tools/VSCode/src/server.scala	Thu Mar 15 21:26:39 2018 +0100
     3.2 +++ b/src/Tools/VSCode/src/server.scala	Thu Mar 15 21:44:34 2018 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4  
     3.5    Options are:
     3.6      -A           explore theory name space of all known sessions (potentially slow)
     3.7 -    -L FILE      enable logging on FILE
     3.8 +    -L FILE      logging on FILE
     3.9      -d DIR       include session directory
    3.10      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
    3.11      -m MODE      add print mode for output