64605
|
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 lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
|
|
24 |
|
|
25 |
val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
|
|
26 |
{
|
|
27 |
var log_file: Option[Path] = None
|
|
28 |
var dirs: List[Path] = Nil
|
|
29 |
var logic = default_logic
|
|
30 |
var modes: List[String] = Nil
|
|
31 |
var options = Options.init()
|
|
32 |
|
|
33 |
val getopts = Getopts("""
|
|
34 |
Usage: isabelle vscode_server [OPTIONS]
|
|
35 |
|
|
36 |
Options are:
|
|
37 |
-L FILE enable logging on FILE
|
|
38 |
-d DIR include session directory
|
|
39 |
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
|
|
40 |
-m MODE add print mode for output
|
|
41 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
|
|
42 |
|
|
43 |
Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
|
|
44 |
""",
|
|
45 |
"L:" -> (arg => log_file = Some(Path.explode(arg))),
|
|
46 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
|
|
47 |
"l:" -> (arg => logic = arg),
|
|
48 |
"m:" -> (arg => modes = arg :: modes),
|
|
49 |
"o:" -> (arg => options = options + arg))
|
|
50 |
|
|
51 |
val more_args = getopts(args)
|
|
52 |
if (more_args.nonEmpty) getopts.usage()
|
|
53 |
|
|
54 |
if (!Build.build(options = options, build_heap = true, no_build = true,
|
|
55 |
dirs = dirs, sessions = List(logic)).ok)
|
|
56 |
error("Missing logic image " + quote(logic))
|
|
57 |
|
|
58 |
val channel = new Channel(System.in, System.out, log_file)
|
|
59 |
val server = new Server(channel, options, logic, dirs, modes)
|
|
60 |
|
|
61 |
// prevent spurious garbage on the main protocol channel
|
|
62 |
val orig_out = System.out
|
|
63 |
try {
|
|
64 |
System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
|
|
65 |
server.start()
|
|
66 |
}
|
|
67 |
finally { System.setOut(orig_out) }
|
|
68 |
})
|
|
69 |
|
|
70 |
|
|
71 |
/* server state */
|
|
72 |
|
|
73 |
sealed case class State(
|
|
74 |
session: Option[Session] = None,
|
|
75 |
models: Map[String, Document_Model] = Map.empty)
|
|
76 |
}
|
|
77 |
|
|
78 |
class Server(
|
|
79 |
channel: Channel,
|
|
80 |
options: Options,
|
|
81 |
session_name: String = Server.default_logic,
|
|
82 |
session_dirs: List[Path] = Nil,
|
|
83 |
modes: List[String] = Nil)
|
|
84 |
{
|
|
85 |
/* server state */
|
|
86 |
|
|
87 |
private val state = Synchronized(Server.State())
|
|
88 |
|
|
89 |
def session: Session = state.value.session getOrElse error("Session inactive")
|
|
90 |
def resources: URI_Resources = session.resources.asInstanceOf[URI_Resources]
|
|
91 |
|
|
92 |
|
|
93 |
/* init and exit */
|
|
94 |
|
|
95 |
def initialize(reply: String => Unit)
|
|
96 |
{
|
|
97 |
val content = Build.session_content(options, false, session_dirs, session_name)
|
|
98 |
val resources =
|
|
99 |
new URI_Resources(content.loaded_theories, content.known_theories, content.syntax)
|
|
100 |
|
|
101 |
val session =
|
|
102 |
new Session(resources) {
|
|
103 |
override def output_delay = options.seconds("editor_output_delay")
|
|
104 |
override def prune_delay = options.seconds("editor_prune_delay")
|
|
105 |
override def syslog_limit = options.int("editor_syslog_limit")
|
|
106 |
override def reparse_limit = options.int("editor_reparse_limit")
|
|
107 |
}
|
|
108 |
|
|
109 |
var session_phase: Session.Consumer[Session.Phase] = null
|
|
110 |
session_phase =
|
|
111 |
Session.Consumer(getClass.getName) {
|
|
112 |
case Session.Ready =>
|
|
113 |
session.phase_changed -= session_phase
|
|
114 |
session.update_options(options)
|
|
115 |
reply("")
|
|
116 |
case Session.Failed =>
|
|
117 |
session.phase_changed -= session_phase
|
|
118 |
reply("Prover startup failed")
|
|
119 |
case _ =>
|
|
120 |
}
|
|
121 |
session.phase_changed += session_phase
|
|
122 |
|
|
123 |
session.start(receiver =>
|
|
124 |
Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
|
|
125 |
modes = modes, receiver = receiver))
|
|
126 |
|
|
127 |
state.change(_.copy(session = Some(session)))
|
|
128 |
}
|
|
129 |
|
|
130 |
def shutdown(reply: String => Unit)
|
|
131 |
{
|
|
132 |
state.change(st =>
|
|
133 |
st.session match {
|
|
134 |
case None => reply("Prover inactive"); st
|
|
135 |
case Some(session) =>
|
|
136 |
var session_phase: Session.Consumer[Session.Phase] = null
|
|
137 |
session_phase =
|
|
138 |
Session.Consumer(getClass.getName) {
|
|
139 |
case Session.Inactive =>
|
|
140 |
session.phase_changed -= session_phase
|
|
141 |
reply("")
|
|
142 |
case _ =>
|
|
143 |
}
|
|
144 |
session.phase_changed += session_phase
|
|
145 |
session.stop()
|
|
146 |
st.copy(session = None)
|
|
147 |
})
|
|
148 |
}
|
|
149 |
|
|
150 |
def exit() { sys.exit(if (state.value.session.isDefined) 1 else 0) }
|
|
151 |
|
|
152 |
|
|
153 |
/* document management */
|
|
154 |
|
|
155 |
private val delay_flush =
|
|
156 |
Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
|
|
157 |
state.change(st =>
|
|
158 |
{
|
|
159 |
val models = st.models
|
|
160 |
val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList
|
|
161 |
val edits = for { (_, model) <- changed; edit <- model.node_edits } yield edit
|
|
162 |
val models1 =
|
|
163 |
(models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) })
|
|
164 |
|
|
165 |
session.update(Document.Blobs.empty, edits)
|
|
166 |
st.copy(models = models1)
|
|
167 |
})
|
|
168 |
}
|
|
169 |
|
|
170 |
def update_document(uri: String, text: String)
|
|
171 |
{
|
|
172 |
state.change(st =>
|
|
173 |
{
|
|
174 |
val node_name = resources.node_name(uri)
|
|
175 |
val model = Document_Model(session, Line.Document(text), node_name)
|
|
176 |
st.copy(models = st.models + (uri -> model))
|
|
177 |
})
|
|
178 |
delay_flush.invoke()
|
|
179 |
}
|
|
180 |
|
|
181 |
|
|
182 |
/* tooltips -- see $ISABELLE_HOME/src/Tools/jEdit/rendering.scala */
|
|
183 |
|
|
184 |
def hover(uri: String, pos: Line.Position): Option[(Line.Range, List[String])] =
|
|
185 |
for {
|
|
186 |
model <- state.value.models.get(uri)
|
|
187 |
snapshot = model.snapshot()
|
|
188 |
offset <- model.doc.offset(pos)
|
|
189 |
info <- tooltip(snapshot, Text.Range(offset, offset + 1))
|
|
190 |
} yield {
|
|
191 |
val r = Line.Range(model.doc.position(info.range.start), model.doc.position(info.range.stop))
|
|
192 |
val s = Pretty.string_of(info.info, margin = tooltip_margin.toDouble)
|
|
193 |
(r, List("```\n" + s + "\n```"))
|
|
194 |
}
|
|
195 |
|
|
196 |
private val tooltip_descriptions =
|
|
197 |
Map(
|
|
198 |
Markup.CITATION -> "citation",
|
|
199 |
Markup.TOKEN_RANGE -> "inner syntax token",
|
|
200 |
Markup.FREE -> "free variable",
|
|
201 |
Markup.SKOLEM -> "skolem variable",
|
|
202 |
Markup.BOUND -> "bound variable",
|
|
203 |
Markup.VAR -> "schematic variable",
|
|
204 |
Markup.TFREE -> "free type variable",
|
|
205 |
Markup.TVAR -> "schematic type variable")
|
|
206 |
|
|
207 |
private val tooltip_elements =
|
|
208 |
Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
|
|
209 |
Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
|
|
210 |
Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
|
|
211 |
Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
|
|
212 |
|
|
213 |
private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
|
|
214 |
Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
|
|
215 |
|
|
216 |
private def timing_threshold: Double = options.real("jedit_timing_threshold")
|
|
217 |
|
|
218 |
def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[XML.Body]] =
|
|
219 |
{
|
|
220 |
def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
|
|
221 |
r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
|
|
222 |
{
|
|
223 |
val r = snapshot.convert(r0)
|
|
224 |
val (t, info) = prev.info
|
|
225 |
if (prev.range == r)
|
|
226 |
Text.Info(r, (t, info :+ p))
|
|
227 |
else Text.Info(r, (t, Vector(p)))
|
|
228 |
}
|
|
229 |
|
|
230 |
val results =
|
|
231 |
snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
|
|
232 |
range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
|
|
233 |
{
|
|
234 |
case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
|
|
235 |
Some(Text.Info(r, (t1 + t2, info)))
|
|
236 |
|
|
237 |
case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
|
|
238 |
if kind != "" &&
|
|
239 |
kind != Markup.ML_DEF &&
|
|
240 |
kind != Markup.ML_OPEN &&
|
|
241 |
kind != Markup.ML_STRUCTURE =>
|
|
242 |
val kind1 = Word.implode(Word.explode('_', kind))
|
|
243 |
val txt1 =
|
|
244 |
if (name == "") kind1
|
|
245 |
else if (kind1 == "") quote(name)
|
|
246 |
else kind1 + " " + quote(name)
|
|
247 |
val t = prev.info._1
|
|
248 |
val txt2 =
|
|
249 |
if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
|
|
250 |
"\n" + t.message
|
|
251 |
else ""
|
|
252 |
Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
|
|
253 |
|
|
254 |
case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
|
|
255 |
val text = "doc " + quote(name)
|
|
256 |
Some(add(prev, r, (true, XML.Text(text))))
|
|
257 |
|
|
258 |
case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
|
|
259 |
Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
|
|
260 |
|
|
261 |
case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
|
|
262 |
if name == Markup.SORTING || name == Markup.TYPING =>
|
|
263 |
Some(add(prev, r, (true, pretty_typing("::", body))))
|
|
264 |
|
|
265 |
case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
|
|
266 |
Some(add(prev, r, (true, Pretty.block(0, body))))
|
|
267 |
|
|
268 |
case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
|
|
269 |
Some(add(prev, r, (false, pretty_typing("ML:", body))))
|
|
270 |
|
|
271 |
case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
|
|
272 |
val lang = Word.implode(Word.explode('_', language))
|
|
273 |
Some(add(prev, r, (true, XML.Text("language: " + lang))))
|
|
274 |
|
|
275 |
case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
|
|
276 |
val descr = if (kind == "") "expression" else "expression: " + kind
|
|
277 |
Some(add(prev, r, (true, XML.Text(descr))))
|
|
278 |
|
|
279 |
case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
|
|
280 |
Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
|
|
281 |
case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
|
|
282 |
Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
|
|
283 |
|
|
284 |
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
|
|
285 |
tooltip_descriptions.get(name).
|
|
286 |
map(descr => add(prev, r, (true, XML.Text(descr))))
|
|
287 |
}).map(_.info)
|
|
288 |
|
|
289 |
results.map(_.info).flatMap(res => res._2.toList) match {
|
|
290 |
case Nil => None
|
|
291 |
case tips =>
|
|
292 |
val r = Text.Range(results.head.range.start, results.last.range.stop)
|
|
293 |
val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
|
|
294 |
Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
|
|
295 |
}
|
|
296 |
}
|
|
297 |
|
|
298 |
def tooltip_margin: Int = options.int("jedit_tooltip_margin")
|
|
299 |
|
|
300 |
|
|
301 |
/* main loop */
|
|
302 |
|
|
303 |
def start()
|
|
304 |
{
|
|
305 |
channel.log("\nServer started " + Date.now())
|
|
306 |
|
|
307 |
def handle(json: JSON.T)
|
|
308 |
{
|
|
309 |
try {
|
|
310 |
json match {
|
|
311 |
case Protocol.Initialize(id) =>
|
|
312 |
def initialize_reply(err: String)
|
|
313 |
{
|
|
314 |
channel.write(Protocol.Initialize.reply(id, err))
|
|
315 |
if (err == "") {
|
|
316 |
channel.write(Protocol.DisplayMessage(Protocol.MessageType.Info,
|
|
317 |
"Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")"))
|
|
318 |
}
|
|
319 |
else channel.write(Protocol.DisplayMessage(Protocol.MessageType.Error, err))
|
|
320 |
}
|
|
321 |
initialize(initialize_reply _)
|
|
322 |
case Protocol.Shutdown(id) =>
|
|
323 |
shutdown((error: String) => channel.write(Protocol.Shutdown.reply(id, error)))
|
|
324 |
case Protocol.Exit =>
|
|
325 |
exit()
|
|
326 |
case Protocol.DidOpenTextDocument(uri, lang, version, text) =>
|
|
327 |
update_document(uri, text)
|
|
328 |
case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
|
|
329 |
update_document(uri, text)
|
|
330 |
case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
|
|
331 |
case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
|
|
332 |
case Protocol.Hover(id, uri, pos) =>
|
|
333 |
channel.write(Protocol.Hover.reply(id, hover(uri, pos)))
|
|
334 |
case _ => channel.log("### IGNORED")
|
|
335 |
}
|
|
336 |
}
|
|
337 |
catch { case exn: Throwable => channel.log("*** ERROR: " + Exn.message(exn)) }
|
|
338 |
}
|
|
339 |
|
|
340 |
@tailrec def loop()
|
|
341 |
{
|
|
342 |
channel.read() match {
|
|
343 |
case Some(json) =>
|
|
344 |
json match {
|
|
345 |
case bulk: List[_] => bulk.foreach(handle(_))
|
|
346 |
case _ => handle(json)
|
|
347 |
}
|
|
348 |
loop()
|
|
349 |
case None => channel.log("### TERMINATE")
|
|
350 |
}
|
|
351 |
}
|
|
352 |
loop()
|
|
353 |
}
|
|
354 |
}
|