equal
deleted
inserted
replaced
12 |
12 |
13 |
13 |
14 import isabelle._ |
14 import isabelle._ |
15 |
15 |
16 import java.io.{PrintStream, OutputStream, File => JFile} |
16 import java.io.{PrintStream, OutputStream, File => JFile} |
17 import isabelle.vscode.Sledgehammer_Panel |
|
18 import scala.annotation.tailrec |
17 import scala.annotation.tailrec |
19 |
18 |
20 |
19 |
21 object Language_Server { |
20 object Language_Server { |
22 type Editor = isabelle.Editor[Unit] |
21 type Editor = isabelle.Editor[Unit] |
115 /* prover session */ |
114 /* prover session */ |
116 |
115 |
117 private val session_ = Synchronized(None: Option[VSCode_Session]) |
116 private val session_ = Synchronized(None: Option[VSCode_Session]) |
118 def session: VSCode_Session = session_.value getOrElse error("Server inactive") |
117 def session: VSCode_Session = session_.value getOrElse error("Server inactive") |
119 def resources: VSCode_Resources = session.resources |
118 def resources: VSCode_Resources = session.resources |
120 private val sledgehammer_panel = Sledgehammer_Panel(this) |
119 private val sledgehammer_panel = VSCode_Sledgehammer(this) |
121 |
120 |
122 def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = |
121 def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = |
123 for { |
122 for { |
124 rendering <- resources.get_rendering(new JFile(node_pos.name)) |
123 rendering <- resources.get_rendering(new JFile(node_pos.name)) |
125 offset <- rendering.model.content.doc.offset(node_pos.pos) |
124 offset <- rendering.model.content.doc.offset(node_pos.pos) |