src/Tools/VSCode/src/server.scala
author wenzelm
Wed, 15 Mar 2017 21:52:04 +0100
changeset 65272 7611c55c39d0
parent 65264 7e6ecd04b5fe
child 65317 b9f5cd845616
permissions -rw-r--r--
always output proof state: there is only one output buffer in Isabelle/VSCode;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/VSCode/src/server.scala
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     3
65160
6e042537555d incremental document changes;
wenzelm
parents: 65134
diff changeset
     4
Server for VS Code Language Server Protocol 2.0/3.0, see also
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     5
https://github.com/Microsoft/language-server-protocol
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     6
https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
65160
6e042537555d incremental document changes;
wenzelm
parents: 65134
diff changeset
     7
6e042537555d incremental document changes;
wenzelm
parents: 65134
diff changeset
     8
PIDE protocol extensions depend on system option "vscode_pide_extensions".
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     9
*/
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    10
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    11
package isabelle.vscode
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    12
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    13
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    14
import isabelle._
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    15
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    16
import java.io.{PrintStream, OutputStream, File => JFile}
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    17
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    18
import scala.annotation.tailrec
65234
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
    19
import scala.collection.mutable
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    20
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    21
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    22
object Server
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    23
{
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    24
  /* Isabelle tool wrapper */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    25
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    26
  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    27
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    28
  val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    29
  {
64644
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    30
    try {
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    31
      var log_file: Option[Path] = None
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    32
      var dirs: List[Path] = Nil
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    33
      var logic = default_logic
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    34
      var modes: List[String] = Nil
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    35
      var options = Options.init()
64733
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
    36
      var system_mode = false
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    37
64644
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    38
      val getopts = Getopts("""
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    39
Usage: isabelle vscode_server [OPTIONS]
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    40
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    41
  Options are:
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    42
    -L FILE      enable logging on FILE
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    43
    -d DIR       include session directory
64737
9fc965612459 proper default;
wenzelm
parents: 64733
diff changeset
    44
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    45
    -m MODE      add print mode for output
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    46
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
64733
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
    47
    -s           system build mode for session image
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    48
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    49
  Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    50
""",
64755
ceb81f4928ea support for Windows;
wenzelm
parents: 64748
diff changeset
    51
        "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
ceb81f4928ea support for Windows;
wenzelm
parents: 64748
diff changeset
    52
        "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
64644
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    53
        "l:" -> (arg => logic = arg),
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    54
        "m:" -> (arg => modes = arg :: modes),
64733
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
    55
        "o:" -> (arg => options = options + arg),
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
    56
        "s" -> (_ => system_mode = true))
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    57
64644
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    58
      val more_args = getopts(args)
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    59
      if (more_args.nonEmpty) getopts.usage()
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    60
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
    61
      val log = Logger.make(log_file)
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
    62
      val channel = new Channel(System.in, System.out, log)
65196
e8760a98db78 discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents: 65191
diff changeset
    63
      val server = new Server(channel, options, logic, dirs, modes, system_mode, log)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    64
64644
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    65
      // prevent spurious garbage on the main protocol channel
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    66
      val orig_out = System.out
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    67
      try {
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    68
        System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    69
        server.start()
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    70
      }
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    71
      finally { System.setOut(orig_out) }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    72
    }
64644
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    73
    catch {
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    74
      case exn: Throwable =>
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
    75
        val channel = new Channel(System.in, System.out, No_Logger)
64644
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    76
        channel.error_message(Exn.message(exn))
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    77
        throw(exn)
7dbc9485ed70 more explicit error;
wenzelm
parents: 64643
diff changeset
    78
    }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    79
  })
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    80
}
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    81
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    82
class Server(
65191
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
    83
  val channel: Channel,
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    84
  options: Options,
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    85
  session_name: String = Server.default_logic,
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    86
  session_dirs: List[Path] = Nil,
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
    87
  modes: List[String] = Nil,
64733
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
    88
  system_mode: Boolean = false,
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
    89
  log: Logger = No_Logger)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    90
{
64725
wenzelm
parents: 64724
diff changeset
    91
  /* prover session */
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    92
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
    93
  private val session_ = Synchronized(None: Option[Session])
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
    94
  def session: Session = session_.value getOrElse error("Server inactive")
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64622
diff changeset
    95
  def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    96
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
    97
  def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
64649
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
    98
    for {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
    99
      model <- resources.get_model(new JFile(node_pos.name))
64704
08c2d80428ff re-use options from resources;
wenzelm
parents: 64703
diff changeset
   100
      rendering = model.rendering()
64830
9bc44bef99e6 more explocit Document_Model.Content;
wenzelm
parents: 64821
diff changeset
   101
      offset <- model.content.doc.offset(node_pos.pos)
64649
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
   102
    } yield (rendering, offset)
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
   103
65191
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
   104
  private val dynamic_output = Dynamic_Output(this)
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
   105
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   106
64725
wenzelm
parents: 64724
diff changeset
   107
  /* input from client or file-system */
wenzelm
parents: 64724
diff changeset
   108
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64783
diff changeset
   109
  private val delay_input: Standard_Thread.Delay =
64810
05b29c8f0add more informative error for spurious crash;
wenzelm
parents: 64801
diff changeset
   110
    Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
64725
wenzelm
parents: 64724
diff changeset
   111
    { resources.flush_input(session) }
wenzelm
parents: 64724
diff changeset
   112
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64783
diff changeset
   113
  private val delay_load: Standard_Thread.Delay =
64810
05b29c8f0add more informative error for spurious crash;
wenzelm
parents: 64801
diff changeset
   114
    Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
64857
wenzelm
parents: 64856
diff changeset
   115
      val (invoke_input, invoke_load) = resources.resolve_dependencies(session, file_watcher)
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64783
diff changeset
   116
      if (invoke_input) delay_input.invoke()
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64783
diff changeset
   117
      if (invoke_load) delay_load.invoke
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64783
diff changeset
   118
    }
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64725
diff changeset
   119
64857
wenzelm
parents: 64856
diff changeset
   120
  private val file_watcher =
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64725
diff changeset
   121
    File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
64725
wenzelm
parents: 64724
diff changeset
   122
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   123
  private def close_document(file: JFile)
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   124
  {
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   125
    if (resources.close_model(file)) {
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   126
      file_watcher.register_parent(file)
65116
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   127
      sync_documents(Set(file))
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   128
      delay_input.invoke()
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   129
      delay_output.invoke()
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   130
    }
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   131
  }
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   132
65116
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   133
  private def sync_documents(changed: Set[JFile])
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   134
  {
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   135
    resources.sync_models(changed)
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   136
    delay_input.invoke()
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   137
    delay_output.invoke()
06d9bcb66ef3 simplified;
wenzelm
parents: 65111
diff changeset
   138
  }
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   139
65160
6e042537555d incremental document changes;
wenzelm
parents: 65134
diff changeset
   140
  private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
6e042537555d incremental document changes;
wenzelm
parents: 65134
diff changeset
   141
  {
65234
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   142
    val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange]
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   143
    @tailrec def norm(chs: List[Protocol.TextDocumentChange])
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   144
    {
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   145
      if (chs.nonEmpty) {
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   146
        val (full_texts, rest1) = chs.span(_.range.isEmpty)
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   147
        val (edits, rest2) = rest1.span(_.range.nonEmpty)
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   148
        norm_changes ++= full_texts
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   149
        norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   150
        norm(rest2)
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   151
      }
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   152
    }
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   153
    norm(changes)
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   154
    norm_changes.foreach(change =>
65184
0f555ce33970 apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);
wenzelm
parents: 65162
diff changeset
   155
      resources.change_model(session, file, change.text, change.range))
65234
1d6e9048cb62 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
wenzelm
parents: 65232
diff changeset
   156
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   157
    delay_input.invoke()
65111
3224a6f7bd6b more robust treatment of pending input/output: these are often correlated;
wenzelm
parents: 65107
diff changeset
   158
    delay_output.invoke()
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   159
  }
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   160
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   161
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   162
  /* caret handling */
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   163
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   164
  private val delay_caret_update: Standard_Thread.Delay =
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   165
    Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   166
    { session.caret_focus.post(Session.Caret_Focus) }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   167
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   168
  private def update_caret(caret: Option[(JFile, Line.Position)])
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   169
  {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   170
    resources.update_caret(caret)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   171
    delay_caret_update.invoke()
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   172
  }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   173
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   174
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   175
  /* output to client */
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   176
64691
db2b21a52f20 prefer stable state -- reduce repeated diagnostics;
wenzelm
parents: 64690
diff changeset
   177
  private val delay_output: Standard_Thread.Delay =
64810
05b29c8f0add more informative error for spurious crash;
wenzelm
parents: 64801
diff changeset
   178
    Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   179
    {
65232
ca571c8c0788 avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents: 65231
diff changeset
   180
      if (resources.flush_output(channel)) delay_output.invoke()
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   181
    }
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
   182
64725
wenzelm
parents: 64724
diff changeset
   183
  private val prover_output =
wenzelm
parents: 64724
diff changeset
   184
    Session.Consumer[Session.Commands_Changed](getClass.getName) {
65119
a7bedf94e71c always invoke output: pending_output may be present due to other reasons;
wenzelm
parents: 65116
diff changeset
   185
      case changed =>
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   186
        resources.update_output(changed.nodes.toList.map(resources.node_file(_)))
64725
wenzelm
parents: 64724
diff changeset
   187
        delay_output.invoke()
wenzelm
parents: 64724
diff changeset
   188
    }
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   189
64725
wenzelm
parents: 64724
diff changeset
   190
  private val syslog =
64692
ccf017e2f2b4 support for syslog messages;
wenzelm
parents: 64691
diff changeset
   191
    Session.Consumer[Prover.Message](getClass.getName) {
ccf017e2f2b4 support for syslog messages;
wenzelm
parents: 64691
diff changeset
   192
      case output: Prover.Output if output.is_syslog =>
64870
41e2797af496 clarified text output wrt. symbols;
wenzelm
parents: 64857
diff changeset
   193
        channel.log_writeln(resources.output_xml(output.message))
64692
ccf017e2f2b4 support for syslog messages;
wenzelm
parents: 64691
diff changeset
   194
      case _ =>
ccf017e2f2b4 support for syslog messages;
wenzelm
parents: 64691
diff changeset
   195
    }
ccf017e2f2b4 support for syslog messages;
wenzelm
parents: 64691
diff changeset
   196
ccf017e2f2b4 support for syslog messages;
wenzelm
parents: 64691
diff changeset
   197
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   198
  /* init and exit */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   199
64641
wenzelm
parents: 64623
diff changeset
   200
  def init(id: Protocol.Id)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   201
  {
64641
wenzelm
parents: 64623
diff changeset
   202
    def reply(err: String)
wenzelm
parents: 64623
diff changeset
   203
    {
wenzelm
parents: 64623
diff changeset
   204
      channel.write(Protocol.Initialize.reply(id, err))
64642
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64641
diff changeset
   205
      if (err == "")
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64641
diff changeset
   206
        channel.writeln("Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")")
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64641
diff changeset
   207
      else channel.error_message(err)
64641
wenzelm
parents: 64623
diff changeset
   208
    }
wenzelm
parents: 64623
diff changeset
   209
64643
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   210
    val try_session =
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   211
      try {
64733
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   212
        if (!Build.build(options = options, build_heap = true, no_build = true,
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   213
              system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   214
        {
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   215
          val start_msg = "Build started for Isabelle/" + session_name + " ..."
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   216
          val fail_msg = "Session build failed -- prover process remains inactive!"
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   217
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   218
          val progress = channel.make_progress(verbose = true)
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   219
          progress.echo(start_msg); channel.writeln(start_msg)
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   220
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   221
          if (!Build.build(options = options, progress = progress, build_heap = true,
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   222
              system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   223
          {
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   224
            progress.echo(fail_msg); error(fail_msg)
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   225
          }
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   226
        }
20174e871623 automatically build session image;
wenzelm
parents: 64727
diff changeset
   227
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 65234
diff changeset
   228
        val base = Sessions.session_base(options, session_name, session_dirs)
65196
e8760a98db78 discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents: 65191
diff changeset
   229
        val resources = new VSCode_Resources(options, base, log)
64854
f5aa712e6250 tuned signature;
wenzelm
parents: 64830
diff changeset
   230
          {
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64725
diff changeset
   231
            override def commit(change: Session.Change): Unit =
64800
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64783
diff changeset
   232
              if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
415dafeb9669 manage document blobs as well;
wenzelm
parents: 64783
diff changeset
   233
                delay_load.invoke()
64727
13e37567a0d6 automatically resolve dependencies from document models and file-system;
wenzelm
parents: 64725
diff changeset
   234
          }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   235
65272
7611c55c39d0 always output proof state: there is only one output buffer in Isabelle/VSCode;
wenzelm
parents: 65264
diff changeset
   236
        val session_options = options.bool("editor_output_state") = true
7611c55c39d0 always output proof state: there is only one output buffer in Isabelle/VSCode;
wenzelm
parents: 65264
diff changeset
   237
        Some(new Session(session_options, resources))
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   238
      }
64643
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   239
      catch { case ERROR(msg) => reply(msg); None }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   240
64643
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   241
    for (session <- try_session) {
65191
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
   242
      session_.change(_ => Some(session))
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
   243
65227
wenzelm
parents: 65216
diff changeset
   244
      session.commands_changed += prover_output
wenzelm
parents: 65216
diff changeset
   245
      session.all_messages += syslog
wenzelm
parents: 65216
diff changeset
   246
wenzelm
parents: 65216
diff changeset
   247
      dynamic_output.init()
wenzelm
parents: 65216
diff changeset
   248
64643
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   249
      var session_phase: Session.Consumer[Session.Phase] = null
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   250
      session_phase =
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   251
        Session.Consumer(getClass.getName) {
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   252
          case Session.Ready =>
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   253
            session.phase_changed -= session_phase
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   254
            reply("")
65206
ff8c3c29a924 clarified Session.Phase;
wenzelm
parents: 65197
diff changeset
   255
          case Session.Terminated(rc) if rc != 0 =>
64643
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   256
            session.phase_changed -= session_phase
65228
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   257
            reply("Prover startup failed: return code " + rc)
64643
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   258
          case _ =>
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   259
        }
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   260
      session.phase_changed += session_phase
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   261
65216
060a8a1f2dec tuned signature;
wenzelm
parents: 65210
diff changeset
   262
      Isabelle_Process.start(session, options,
060a8a1f2dec tuned signature;
wenzelm
parents: 65210
diff changeset
   263
        logic = session_name, dirs = session_dirs, modes = modes)
64643
b755f6069ba2 more explicit error;
wenzelm
parents: 64642
diff changeset
   264
    }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   265
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   266
64641
wenzelm
parents: 64623
diff changeset
   267
  def shutdown(id: Protocol.Id)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   268
  {
64641
wenzelm
parents: 64623
diff changeset
   269
    def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err))
wenzelm
parents: 64623
diff changeset
   270
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   271
    session_.change({
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   272
      case Some(session) =>
65228
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   273
        session.commands_changed -= prover_output
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   274
        session.all_messages -= syslog
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   275
65191
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
   276
        dynamic_output.exit()
65228
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   277
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   278
        delay_load.revoke()
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   279
        file_watcher.shutdown()
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   280
        delay_input.revoke()
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   281
        delay_output.revoke()
65228
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   282
        delay_caret_update.revoke()
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   283
b11099b7d868 clarified shutdown;
wenzelm
parents: 65227
diff changeset
   284
        val rc = session.stop()
65231
wenzelm
parents: 65229
diff changeset
   285
        if (rc == 0) reply("") else reply("Prover shutdown failed: return code " + rc)
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   286
        None
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   287
      case None =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   288
        reply("Prover inactive")
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   289
        None
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   290
    })
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   291
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   292
64646
805c5e6fa430 tuned messages;
wenzelm
parents: 64645
diff changeset
   293
  def exit() {
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
   294
    log("\n")
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
   295
    sys.exit(if (session_.value.isDefined) 1 else 0)
64646
805c5e6fa430 tuned messages;
wenzelm
parents: 64645
diff changeset
   296
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   297
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   298
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   299
  /* completion */
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   300
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   301
  def completion(id: Protocol.Id, node_pos: Line.Node_Position)
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   302
  {
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   303
    val result =
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   304
      (for ((rendering, offset) <- rendering_offset(node_pos))
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   305
        yield rendering.completion(Text.Range(offset - 1, offset))) getOrElse Nil
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   306
    channel.write(Protocol.Completion.reply(id, result))
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   307
  }
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   308
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   309
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 64618
diff changeset
   310
  /* hover */
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   311
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   312
  def hover(id: Protocol.Id, node_pos: Line.Node_Position)
64641
wenzelm
parents: 64623
diff changeset
   313
  {
wenzelm
parents: 64623
diff changeset
   314
    val result =
wenzelm
parents: 64623
diff changeset
   315
      for {
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   316
        (rendering, offset) <- rendering_offset(node_pos)
65134
511bf19348d3 clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents: 65129
diff changeset
   317
        info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1))
64641
wenzelm
parents: 64623
diff changeset
   318
      } yield {
65197
8fada74d82be tuned signature;
wenzelm
parents: 65196
diff changeset
   319
        val range = rendering.model.content.doc.range(info.range)
64748
155bf8632104 clarified multiple tooltips;
wenzelm
parents: 64747
diff changeset
   320
        val contents =
65107
70b0113fa4ef clarified pretty margin;
wenzelm
parents: 65093
diff changeset
   321
          info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t))))
64748
155bf8632104 clarified multiple tooltips;
wenzelm
parents: 64747
diff changeset
   322
        (range, contents)
64641
wenzelm
parents: 64623
diff changeset
   323
      }
wenzelm
parents: 64623
diff changeset
   324
    channel.write(Protocol.Hover.reply(id, result))
wenzelm
parents: 64623
diff changeset
   325
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   326
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   327
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64646
diff changeset
   328
  /* goto definition */
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64646
diff changeset
   329
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   330
  def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position)
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64646
diff changeset
   331
  {
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64646
diff changeset
   332
    val result =
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   333
      (for ((rendering, offset) <- rendering_offset(node_pos))
64649
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
   334
        yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64646
diff changeset
   335
    channel.write(Protocol.GotoDefinition.reply(id, result))
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64646
diff changeset
   336
  }
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64646
diff changeset
   337
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64646
diff changeset
   338
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   339
  /* document highlights */
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   340
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   341
  def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   342
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   343
    val result =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   344
      (for ((rendering, offset) <- rendering_offset(node_pos))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   345
        yield {
65197
8fada74d82be tuned signature;
wenzelm
parents: 65196
diff changeset
   346
          val model = rendering.model
8fada74d82be tuned signature;
wenzelm
parents: 65196
diff changeset
   347
          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range)
8fada74d82be tuned signature;
wenzelm
parents: 65196
diff changeset
   348
            .map(r => Protocol.DocumentHighlight.text(model.content.doc.range(r)))
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   349
        }) getOrElse Nil
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   350
    channel.write(Protocol.DocumentHighlights.reply(id, result))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   351
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   352
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   353
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   354
  /* main loop */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   355
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   356
  def start()
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   357
  {
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
   358
    log("Server started " + Date.now())
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   359
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   360
    def handle(json: JSON.T)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   361
    {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   362
      try {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   363
        json match {
64641
wenzelm
parents: 64623
diff changeset
   364
          case Protocol.Initialize(id) => init(id)
65229
cc96b8c3b8cb explicitly ignore "initialized" message;
wenzelm
parents: 65228
diff changeset
   365
          case Protocol.Initialized(()) =>
64641
wenzelm
parents: 64623
diff changeset
   366
          case Protocol.Shutdown(id) => shutdown(id)
64645
0b513620d949 proper pattern match;
wenzelm
parents: 64644
diff changeset
   367
          case Protocol.Exit(()) => exit()
65162
wenzelm
parents: 65160
diff changeset
   368
          case Protocol.DidOpenTextDocument(file, _, _, text) =>
wenzelm
parents: 65160
diff changeset
   369
            change_document(file, List(Protocol.TextDocumentChange(None, text)))
65160
6e042537555d incremental document changes;
wenzelm
parents: 65134
diff changeset
   370
          case Protocol.DidChangeTextDocument(file, _, changes) => change_document(file, changes)
6e042537555d incremental document changes;
wenzelm
parents: 65134
diff changeset
   371
          case Protocol.DidCloseTextDocument(file) => close_document(file)
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64870
diff changeset
   372
          case Protocol.Completion(id, node_pos) => completion(id, node_pos)
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   373
          case Protocol.Hover(id, node_pos) => hover(id, node_pos)
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   374
          case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64755
diff changeset
   375
          case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65184
diff changeset
   376
          case Protocol.Caret_Update(caret) => update_caret(caret)
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
   377
          case _ => log("### IGNORED")
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   378
        }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   379
      }
64687
04806ad1e43a clarified protocol errors;
wenzelm
parents: 64684
diff changeset
   380
      catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   381
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   382
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   383
    @tailrec def loop()
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   384
    {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   385
      channel.read() match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   386
        case Some(json) =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   387
          json match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   388
            case bulk: List[_] => bulk.foreach(handle(_))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   389
            case _ => handle(json)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   390
          }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   391
          loop()
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64710
diff changeset
   392
        case None => log("### TERMINATE")
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   393
      }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   394
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   395
    loop()
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   396
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   397
}