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