src/Tools/VSCode/src/server.scala
author wenzelm
Wed Dec 21 16:28:02 2016 +0100 (2016-12-21)
changeset 64645 0b513620d949
parent 64644 7dbc9485ed70
child 64646 805c5e6fa430
permissions -rw-r--r--
proper pattern match;
     1 /*  Title:      Tools/VSCode/src/server.scala
     2     Author:     Makarius
     3 
     4 Server for VS Code Language Server Protocol 2.0, see also
     5 https://github.com/Microsoft/language-server-protocol
     6 https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
     7 */
     8 
     9 package isabelle.vscode
    10 
    11 
    12 import isabelle._
    13 
    14 import java.io.{PrintStream, OutputStream}
    15 
    16 import scala.annotation.tailrec
    17 
    18 
    19 object Server
    20 {
    21   /* Isabelle tool wrapper */
    22 
    23   private val default_text_length = "UTF-16"
    24   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    25 
    26   val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
    27   {
    28     try {
    29       var log_file: Option[Path] = None
    30       var text_length = Length.encoding(default_text_length)
    31       var dirs: List[Path] = Nil
    32       var logic = default_logic
    33       var modes: List[String] = Nil
    34       var options = Options.init()
    35 
    36       def text_length_choice: String =
    37         commas(Length.encodings.map(
    38           { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
    39 
    40       val getopts = Getopts("""
    41 Usage: isabelle vscode_server [OPTIONS]
    42 
    43   Options are:
    44     -L FILE      enable logging on FILE
    45     -T LENGTH    text length encoding: """ + text_length_choice + """
    46     -d DIR       include session directory
    47     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
    48     -m MODE      add print mode for output
    49     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    50 
    51   Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
    52 """,
    53         "L:" -> (arg => log_file = Some(Path.explode(arg))),
    54         "T:" -> (arg => Length.encoding(arg)),
    55         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    56         "l:" -> (arg => logic = arg),
    57         "m:" -> (arg => modes = arg :: modes),
    58         "o:" -> (arg => options = options + arg))
    59 
    60       val more_args = getopts(args)
    61       if (more_args.nonEmpty) getopts.usage()
    62 
    63       if (!Build.build(options = options, build_heap = true, no_build = true,
    64             dirs = dirs, sessions = List(logic)).ok)
    65         error("Missing logic image " + quote(logic))
    66 
    67       val channel = new Channel(System.in, System.out, log_file)
    68       val server = new Server(channel, options, text_length, logic, dirs, modes)
    69 
    70       // prevent spurious garbage on the main protocol channel
    71       val orig_out = System.out
    72       try {
    73         System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
    74         server.start()
    75       }
    76       finally { System.setOut(orig_out) }
    77     }
    78     catch {
    79       case exn: Throwable =>
    80         val channel = new Channel(System.in, System.out, None)
    81         channel.error_message(Exn.message(exn))
    82         throw(exn)
    83     }
    84   })
    85 
    86 
    87   /* server state */
    88 
    89   sealed case class State(
    90     session: Option[Session] = None,
    91     models: Map[String, Document_Model] = Map.empty)
    92 }
    93 
    94 class Server(
    95   channel: Channel,
    96   options: Options,
    97   text_length: Length = Length.encoding(Server.default_text_length),
    98   session_name: String = Server.default_logic,
    99   session_dirs: List[Path] = Nil,
   100   modes: List[String] = Nil)
   101 {
   102   /* server state */
   103 
   104   private val state = Synchronized(Server.State())
   105 
   106   def session: Session = state.value.session getOrElse error("Session inactive")
   107   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
   108 
   109 
   110   /* init and exit */
   111 
   112   def init(id: Protocol.Id)
   113   {
   114     def reply(err: String)
   115     {
   116       channel.write(Protocol.Initialize.reply(id, err))
   117       if (err == "")
   118         channel.writeln("Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")")
   119       else channel.error_message(err)
   120     }
   121 
   122     val try_session =
   123       try {
   124         val content = Build.session_content(options, false, session_dirs, session_name)
   125         val resources =
   126           new VSCode_Resources(content.loaded_theories, content.known_theories, content.syntax)
   127 
   128         Some(new Session(resources) {
   129           override def output_delay = options.seconds("editor_output_delay")
   130           override def prune_delay = options.seconds("editor_prune_delay")
   131           override def syslog_limit = options.int("editor_syslog_limit")
   132           override def reparse_limit = options.int("editor_reparse_limit")
   133         })
   134       }
   135       catch { case ERROR(msg) => reply(msg); None }
   136 
   137     for (session <- try_session) {
   138       var session_phase: Session.Consumer[Session.Phase] = null
   139       session_phase =
   140         Session.Consumer(getClass.getName) {
   141           case Session.Ready =>
   142             session.phase_changed -= session_phase
   143             session.update_options(options)
   144             reply("")
   145           case Session.Failed =>
   146             session.phase_changed -= session_phase
   147             reply("Prover startup failed")
   148           case _ =>
   149         }
   150       session.phase_changed += session_phase
   151 
   152       session.start(receiver =>
   153         Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
   154           modes = modes, receiver = receiver))
   155 
   156       state.change(_.copy(session = Some(session)))
   157     }
   158   }
   159 
   160   def shutdown(id: Protocol.Id)
   161   {
   162     def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err))
   163 
   164     state.change(st =>
   165       st.session match {
   166         case None => reply("Prover inactive"); st
   167         case Some(session) =>
   168           var session_phase: Session.Consumer[Session.Phase] = null
   169           session_phase =
   170             Session.Consumer(getClass.getName) {
   171               case Session.Inactive =>
   172                 session.phase_changed -= session_phase
   173                 reply("")
   174               case _ =>
   175             }
   176           session.phase_changed += session_phase
   177           session.stop()
   178           st.copy(session = None)
   179       })
   180   }
   181 
   182   def exit() { sys.exit(if (state.value.session.isDefined) 1 else 0) }
   183 
   184 
   185   /* document management */
   186 
   187   private val delay_flush =
   188     Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
   189       state.change(st =>
   190         {
   191           val models = st.models
   192           val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList
   193           val edits = for { (_, model) <- changed; edit <- model.node_edits } yield edit
   194           val models1 =
   195             (models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) })
   196 
   197           session.update(Document.Blobs.empty, edits)
   198           st.copy(models = models1)
   199         })
   200     }
   201 
   202   def update_document(uri: String, text: String)
   203   {
   204     state.change(st =>
   205       {
   206         val node_name = resources.node_name(uri)
   207         val model = Document_Model(session, Line.Document(text), node_name)
   208         st.copy(models = st.models + (uri -> model))
   209       })
   210     delay_flush.invoke()
   211   }
   212 
   213 
   214   /* hover */
   215 
   216   def hover(id: Protocol.Id, uri: String, pos: Line.Position)
   217   {
   218     val result =
   219       for {
   220         model <- state.value.models.get(uri)
   221         rendering = model.rendering(options)
   222         offset <- model.doc.offset(pos, text_length)
   223         info <- rendering.tooltip(Text.Range(offset, offset + 1))
   224       } yield {
   225         val start = model.doc.position(info.range.start, text_length)
   226         val stop = model.doc.position(info.range.stop, text_length)
   227         val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
   228         (Line.Range(start, stop), List("```\n" + s + "\n```"))  // FIXME proper content format
   229       }
   230     channel.write(Protocol.Hover.reply(id, result))
   231   }
   232 
   233 
   234   /* main loop */
   235 
   236   def start()
   237   {
   238     channel.log("\nServer started " + Date.now())
   239 
   240     def handle(json: JSON.T)
   241     {
   242       try {
   243         json match {
   244           case Protocol.Initialize(id) => init(id)
   245           case Protocol.Shutdown(id) => shutdown(id)
   246           case Protocol.Exit(()) => exit()
   247           case Protocol.DidOpenTextDocument(uri, lang, version, text) =>
   248             update_document(uri, text)
   249           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
   250             update_document(uri, text)
   251           case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
   252           case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
   253           case Protocol.Hover(id, uri, pos) => hover(id, uri, pos)
   254           case _ => channel.log("### IGNORED")
   255         }
   256       }
   257       catch { case exn: Throwable => channel.log("*** ERROR: " + Exn.message(exn)) }
   258     }
   259 
   260     @tailrec def loop()
   261     {
   262       channel.read() match {
   263         case Some(json) =>
   264           json match {
   265             case bulk: List[_] => bulk.foreach(handle(_))
   266             case _ => handle(json)
   267           }
   268           loop()
   269         case None => channel.log("### TERMINATE")
   270       }
   271     }
   272     loop()
   273   }
   274 }