1/* Title: Tools/VSCode/src/vscode_resources.scala 2 Author: Makarius 3 4Resources for VSCode Language Server: file-system access and global state. 5*/ 6 7package isabelle.vscode 8 9 10import isabelle._ 11 12import java.io.{File => JFile} 13 14import scala.util.parsing.input.Reader 15 16 17object VSCode_Resources 18{ 19 /* internal state */ 20 21 sealed case class State( 22 models: Map[JFile, Document_Model] = Map.empty, 23 caret: Option[(JFile, Line.Position)] = None, 24 overlays: Document.Overlays = Document.Overlays.empty, 25 pending_input: Set[JFile] = Set.empty, 26 pending_output: Set[JFile] = Set.empty) 27 { 28 def update_models(changed: Traversable[(JFile, Document_Model)]): State = 29 copy( 30 models = models ++ changed, 31 pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file }, 32 pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file }) 33 34 def update_caret(new_caret: Option[(JFile, Line.Position)]): State = 35 if (caret == new_caret) this 36 else 37 copy( 38 caret = new_caret, 39 pending_input = pending_input ++ caret.map(_._1) ++ new_caret.map(_._1)) 40 41 def get_caret(file: JFile): Option[Line.Position] = 42 caret match { 43 case Some((caret_file, caret_pos)) if caret_file == file => Some(caret_pos) 44 case _ => None 45 } 46 47 lazy val document_blobs: Document.Blobs = 48 Document.Blobs( 49 (for { 50 (_, model) <- models.iterator 51 blob <- model.get_blob 52 } yield (model.node_name -> blob)).toMap) 53 54 def change_overlay(insert: Boolean, file: JFile, 55 command: Command, fn: String, args: List[String]): State = 56 copy( 57 overlays = 58 if (insert) overlays.insert(command, fn, args) 59 else overlays.remove(command, fn, args), 60 pending_input = pending_input + file) 61 } 62 63 64 /* caret */ 65 66 sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset) 67 { 68 def node_name: Document.Node.Name = model.node_name 69 } 70} 71 72class VSCode_Resources( 73 val options: Options, 74 session_base: Sessions.Base, 75 log: Logger = No_Logger) 76 extends Resources(session_base, log = log) 77{ 78 resources => 79 80 private val state = Synchronized(VSCode_Resources.State()) 81 82 83 /* options */ 84 85 def pide_extensions: Boolean = options.bool("vscode_pide_extensions") 86 def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols") 87 def tooltip_margin: Int = options.int("vscode_tooltip_margin") 88 def message_margin: Int = options.int("vscode_message_margin") 89 90 91 /* document node name */ 92 93 def node_file(name: Document.Node.Name): JFile = new JFile(name.node) 94 95 def node_name(file: JFile): Document.Node.Name = 96 session_base.known.get_file(file, bootstrap = true) getOrElse { 97 val node = file.getPath 98 val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) 99 if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory) 100 else { 101 val master_dir = file.getParent 102 Document.Node.Name(node, master_dir, theory) 103 } 104 } 105 106 override def append(dir: String, source_path: Path): String = 107 { 108 val path = source_path.expand 109 if (dir == "" || path.is_absolute) File.platform_path(path) 110 else if (path.is_current) dir 111 else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator)) 112 dir + JFile.separator + File.platform_path(path) 113 else if (path.is_basic) dir + File.platform_path(path) 114 else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path))) 115 } 116 117 def get_models: Map[JFile, Document_Model] = state.value.models 118 def get_model(file: JFile): Option[Document_Model] = get_models.get(file) 119 def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name)) 120 121 122 /* file content */ 123 124 def read_file_content(file: JFile): Option[String] = 125 { 126 Bibtex.make_theory_content(file) orElse { 127 try { Some(Line.normalize(File.read(file))) } 128 catch { case ERROR(_) => None } 129 } 130 } 131 132 def get_file_content(file: JFile): Option[String] = 133 get_model(file) match { 134 case Some(model) => Some(model.content.text) 135 case None => read_file_content(file) 136 } 137 138 override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = 139 { 140 val file = node_file(name) 141 get_model(file) match { 142 case Some(model) => f(Scan.char_reader(model.content.text)) 143 case None if file.isFile => 144 val reader = Scan.byte_reader(file) 145 try { f(reader) } finally { reader.close } 146 case None => 147 error("No such file: " + quote(file.toString)) 148 } 149 } 150 151 152 /* document models */ 153 154 def visible_node(name: Document.Node.Name): Boolean = 155 get_model(name) match { 156 case Some(model) => model.node_visible 157 case None => false 158 } 159 160 def change_model( 161 session: Session, 162 editor: Server.Editor, 163 file: JFile, 164 version: Long, 165 text: String, 166 range: Option[Line.Range] = None) 167 { 168 state.change(st => 169 { 170 val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file))) 171 val model1 = 172 (model.change_text(text, range) getOrElse model).set_version(version).external(false) 173 st.update_models(Some(file -> model1)) 174 }) 175 } 176 177 def close_model(file: JFile): Boolean = 178 state.change_result(st => 179 st.models.get(file) match { 180 case None => (false, st) 181 case Some(model) => (true, st.update_models(Some(file -> model.external(true)))) 182 }) 183 184 def sync_models(changed_files: Set[JFile]): Unit = 185 state.change(st => 186 { 187 val changed_models = 188 (for { 189 (file, model) <- st.models.iterator 190 if changed_files(file) && model.external_file 191 text <- read_file_content(file) 192 model1 <- model.change_text(text) 193 } yield (file, model1)).toList 194 st.update_models(changed_models) 195 }) 196 197 198 /* overlays */ 199 200 def node_overlays(name: Document.Node.Name): Document.Node.Overlays = 201 state.value.overlays(name) 202 203 def insert_overlay(command: Command, fn: String, args: List[String]): Unit = 204 state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args)) 205 206 def remove_overlay(command: Command, fn: String, args: List[String]): Unit = 207 state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args)) 208 209 210 /* resolve dependencies */ 211 212 def resolve_dependencies( 213 session: Session, 214 editor: Server.Editor, 215 file_watcher: File_Watcher): (Boolean, Boolean) = 216 { 217 state.change_result(st => 218 { 219 /* theory files */ 220 221 val thys = 222 (for ((_, model) <- st.models.iterator if model.is_theory) 223 yield (model.node_name, Position.none)).toList 224 225 val thy_files1 = resources.dependencies(thys).theories 226 227 val thy_files2 = 228 (for { 229 (_, model) <- st.models.iterator if model.node_name.is_bibtex 230 thy_name <- Bibtex.make_theory_name(resources, model.node_name) 231 } yield thy_name).toList 232 233 234 /* auxiliary files */ 235 236 val stable_tip_version = 237 if (st.models.forall(entry => entry._2.is_stable)) 238 session.current_state().stable_tip_version 239 else None 240 241 val aux_files = 242 stable_tip_version match { 243 case Some(version) => undefined_blobs(version.nodes) 244 case None => Nil 245 } 246 247 248 /* loaded models */ 249 250 val loaded_models = 251 (for { 252 node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator 253 file = node_file(node_name) 254 if !st.models.isDefinedAt(file) 255 text <- { file_watcher.register_parent(file); read_file_content(file) } 256 } 257 yield { 258 val model = Document_Model.init(session, editor, node_name) 259 val model1 = (model.change_text(text) getOrElse model).external(true) 260 (file, model1) 261 }).toList 262 263 val invoke_input = loaded_models.nonEmpty 264 val invoke_load = stable_tip_version.isEmpty 265 266 ((invoke_input, invoke_load), st.update_models(loaded_models)) 267 }) 268 } 269 270 271 /* pending input */ 272 273 def flush_input(session: Session, channel: Channel) 274 { 275 state.change(st => 276 { 277 val changed_models = 278 (for { 279 file <- st.pending_input.iterator 280 model <- st.models.get(file) 281 (edits, model1) <- 282 model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file)) 283 } yield (edits, (file, model1))).toList 284 285 for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty } 286 channel.write(Protocol.WorkspaceEdit(workspace_edits)) 287 288 session.update(st.document_blobs, changed_models.flatMap(res => res._1._2)) 289 290 st.copy( 291 models = st.models ++ changed_models.iterator.map(_._2), 292 pending_input = Set.empty) 293 }) 294 } 295 296 297 /* pending output */ 298 299 def update_output(changed_nodes: Traversable[JFile]): Unit = 300 state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) 301 302 def update_output_visible(): Unit = 303 state.change(st => st.copy(pending_output = st.pending_output ++ 304 (for ((file, model) <- st.models.iterator if model.node_visible) yield file))) 305 306 def flush_output(channel: Channel): Boolean = 307 { 308 state.change_result(st => 309 { 310 val (postponed, flushed) = 311 (for { 312 file <- st.pending_output.iterator 313 model <- st.models.get(file) 314 } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated) 315 316 val changed_iterator = 317 for { 318 (file, model, rendering) <- flushed.iterator 319 (changed_diags, changed_decos, model1) = model.publish(rendering) 320 if changed_diags.isDefined || changed_decos.isDefined 321 } 322 yield { 323 for (diags <- changed_diags) 324 channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags))) 325 if (pide_extensions) { 326 for (decos <- changed_decos; deco <- decos) 327 channel.write(rendering.decoration_output(deco).json(file)) 328 } 329 (file, model1) 330 } 331 332 (postponed.nonEmpty, 333 st.copy( 334 models = st.models ++ changed_iterator, 335 pending_output = postponed.map(_._1).toSet)) 336 } 337 ) 338 } 339 340 341 /* output text */ 342 343 def output_text(s: String): String = 344 if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s) 345 346 def output_xml(xml: XML.Tree): String = 347 output_text(XML.content(xml)) 348 349 def output_pretty(body: XML.Body, margin: Int): String = 350 output_text(Pretty.string_of(body, margin = margin)) 351 def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) 352 def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) 353 354 355 /* caret handling */ 356 357 def update_caret(caret: Option[(JFile, Line.Position)]) 358 { state.change(_.update_caret(caret)) } 359 360 def get_caret(): Option[VSCode_Resources.Caret] = 361 { 362 val st = state.value 363 for { 364 (file, pos) <- st.caret 365 model <- st.models.get(file) 366 offset <- model.content.doc.offset(pos) 367 } 368 yield VSCode_Resources.Caret(file, model, offset) 369 } 370 371 372 /* spell checker */ 373 374 val spell_checker = new Spell_Checker_Variable 375 spell_checker.update(options) 376} 377