1/* Title: Tools/VSCode/src/document_model.scala 2 Author: Makarius 3 4Document model for line-oriented text. 5*/ 6 7package isabelle.vscode 8 9 10import isabelle._ 11 12import java.io.{File => JFile} 13 14 15object Document_Model 16{ 17 /* decorations */ 18 19 object Decoration 20 { 21 def empty(typ: String): Decoration = Decoration(typ, Nil) 22 23 def ranges(typ: String, ranges: List[Text.Range]): Decoration = 24 Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body]))) 25 } 26 sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) 27 28 29 /* content */ 30 31 object Content 32 { 33 val empty: Content = Content(Line.Document.empty) 34 } 35 36 sealed case class Content(doc: Line.Document) 37 { 38 override def toString: String = doc.toString 39 def text_length: Text.Offset = doc.text_length 40 def text_range: Text.Range = doc.text_range 41 def text: String = doc.text 42 43 lazy val bytes: Bytes = Bytes(text) 44 lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) 45 lazy val bibtex_entries: List[Text.Info[String]] = 46 try { Bibtex.entries(text) } 47 catch { case ERROR(_) => Nil } 48 49 def recode_symbols: List[Protocol.TextEdit] = 50 (for { 51 (line, l) <- doc.lines.iterator.zipWithIndex 52 text1 = Symbol.encode(line.text) 53 if (line.text != text1) 54 } yield { 55 val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length)) 56 Protocol.TextEdit(range, text1) 57 }).toList 58 } 59 60 def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model = 61 Document_Model(session, editor, node_name, Content.empty, 62 node_required = node_name.is_bibtex_theory) 63} 64 65sealed case class Document_Model( 66 session: Session, 67 editor: Server.Editor, 68 node_name: Document.Node.Name, 69 content: Document_Model.Content, 70 version: Option[Long] = None, 71 external_file: Boolean = false, 72 node_required: Boolean = false, 73 last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, 74 pending_edits: List[Text.Edit] = Nil, 75 published_diagnostics: List[Text.Info[Command.Results]] = Nil, 76 published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model 77{ 78 model => 79 80 81 /* content */ 82 83 def get_text(range: Text.Range): Option[String] = content.doc.get_text(range) 84 85 def set_version(new_version: Long): Document_Model = copy(version = Some(new_version)) 86 87 88 /* external file */ 89 90 def external(b: Boolean): Document_Model = copy(external_file = b) 91 92 def node_visible: Boolean = !external_file 93 94 95 /* header */ 96 97 def node_header: Document.Node.Header = 98 resources.special_header(node_name) getOrElse 99 resources.check_thy_reader(node_name, Scan.char_reader(content.text)) 100 101 102 /* perspective */ 103 104 def node_perspective(doc_blobs: Document.Blobs, caret: Option[Line.Position]) 105 : (Boolean, Document.Node.Perspective_Text) = 106 { 107 if (is_theory) { 108 val snapshot = model.snapshot() 109 110 val caret_perspective = resources.options.int("vscode_caret_perspective") max 0 111 val caret_range = 112 if (caret_perspective != 0) { 113 caret match { 114 case Some(pos) => 115 val doc = content.doc 116 val pos1 = Line.Position((pos.line - caret_perspective) max 0) 117 val pos2 = Line.Position((pos.line + caret_perspective + 1) min doc.lines.length) 118 Text.Range(doc.offset(pos1).get, doc.offset(pos2).get) 119 case None => Text.Range.offside 120 } 121 } 122 else if (node_visible) content.text_range 123 else Text.Range.offside 124 125 val text_perspective = 126 if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty) 127 Text.Perspective.full 128 else 129 content.text_range.try_restrict(caret_range) match { 130 case Some(range) => Text.Perspective(List(range)) 131 case None => Text.Perspective.empty 132 } 133 134 val overlays = editor.node_overlays(node_name) 135 136 (snapshot.node.load_commands_changed(doc_blobs), 137 Document.Node.Perspective(node_required, text_perspective, overlays)) 138 } 139 else (false, Document.Node.no_perspective_text) 140 } 141 142 143 /* blob */ 144 145 def get_blob: Option[Document.Blob] = 146 if (is_theory) None 147 else Some((Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))) 148 149 150 /* bibtex entries */ 151 152 def bibtex_entries: List[Text.Info[String]] = 153 model.content.bibtex_entries 154 155 156 /* edits */ 157 158 def change_text(text: String, range: Option[Line.Range] = None): Option[Document_Model] = 159 { 160 val insert = Line.normalize(text) 161 range match { 162 case None => 163 Text.Edit.replace(0, content.text, insert) match { 164 case Nil => None 165 case edits => 166 val content1 = Document_Model.Content(Line.Document(insert)) 167 Some(copy(content = content1, pending_edits = pending_edits ::: edits)) 168 } 169 case Some(remove) => 170 content.doc.change(remove, insert) match { 171 case None => error("Failed to apply document change: " + remove) 172 case Some((Nil, _)) => None 173 case Some((edits, doc1)) => 174 val content1 = Document_Model.Content(doc1) 175 Some(copy(content = content1, pending_edits = pending_edits ::: edits)) 176 } 177 } 178 } 179 180 def flush_edits( 181 unicode_symbols: Boolean, 182 doc_blobs: Document.Blobs, 183 file: JFile, 184 caret: Option[Line.Position]) 185 : Option[((List[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] = 186 { 187 val workspace_edits = 188 if (unicode_symbols && version.isDefined) { 189 val edits = content.recode_symbols 190 if (edits.nonEmpty) List(Protocol.TextDocumentEdit(file, version.get, edits)) 191 else Nil 192 } 193 else Nil 194 195 val (reparse, perspective) = node_perspective(doc_blobs, caret) 196 if (reparse || pending_edits.nonEmpty || last_perspective != perspective || 197 workspace_edits.nonEmpty) 198 { 199 val prover_edits = node_edits(node_header, pending_edits, perspective) 200 val edits = (workspace_edits, prover_edits) 201 Some((edits, copy(pending_edits = Nil, last_perspective = perspective))) 202 } 203 else None 204 } 205 206 207 /* publish annotations */ 208 209 def publish(rendering: VSCode_Rendering): 210 (Option[List[Text.Info[Command.Results]]], Option[List[Document_Model.Decoration]], Document_Model) = 211 { 212 val diagnostics = rendering.diagnostics 213 val decorations = 214 if (node_visible) rendering.decorations 215 else { for (deco <- published_decorations) yield Document_Model.Decoration.empty(deco.typ) } 216 217 val changed_diagnostics = 218 if (diagnostics == published_diagnostics) None else Some(diagnostics) 219 val changed_decorations = 220 if (decorations == published_decorations) None 221 else if (published_decorations.isEmpty) Some(decorations) 222 else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a) 223 224 (changed_diagnostics, changed_decorations, 225 copy(published_diagnostics = diagnostics, published_decorations = decorations)) 226 } 227 228 229 /* prover session */ 230 231 def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] 232 233 def is_stable: Boolean = pending_edits.isEmpty 234 def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) 235 236 def rendering(snapshot: Document.Snapshot): VSCode_Rendering = 237 new VSCode_Rendering(snapshot, model) 238 def rendering(): VSCode_Rendering = rendering(snapshot()) 239 240 241 /* syntax */ 242 243 def syntax(): Outer_Syntax = 244 if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty 245} 246