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