author | wenzelm |
Wed, 08 Apr 2020 13:14:05 +0200 | |
changeset 71733 | 6c470c918aad |
parent 70302 | 9ea7081c3f03 |
child 71774 | 491f185fd705 |
permissions | -rw-r--r-- |
64605 | 1 |
/* Title: Tools/VSCode/src/document_model.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Document model for line-oriented text. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
70302 | 11 |
import isabelle.vscode.{Protocol, Server} |
64605 | 12 |
|
64710 | 13 |
import java.io.{File => JFile} |
14 |
||
64605 | 15 |
|
64707 | 16 |
object Document_Model |
17 |
{ |
|
65095 | 18 |
/* decorations */ |
19 |
||
65140 | 20 |
object Decoration |
21 |
{ |
|
22 |
def empty(typ: String): Decoration = Decoration(typ, Nil) |
|
23 |
||
24 |
def ranges(typ: String, ranges: List[Text.Range]): Decoration = |
|
25 |
Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body]))) |
|
26 |
} |
|
65105 | 27 |
sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) |
65095 | 28 |
|
29 |
||
30 |
/* content */ |
|
31 |
||
65923 | 32 |
object Content |
33 |
{ |
|
34 |
val empty: Content = Content(Line.Document.empty) |
|
35 |
} |
|
36 |
||
64830 | 37 |
sealed case class Content(doc: Line.Document) |
38 |
{ |
|
65161 | 39 |
override def toString: String = doc.toString |
65197 | 40 |
def text_length: Text.Offset = doc.text_length |
64830 | 41 |
def text_range: Text.Range = doc.text_range |
42 |
def text: String = doc.text |
|
64833 | 43 |
|
64830 | 44 |
lazy val bytes: Bytes = Bytes(text) |
45 |
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) |
|
64833 | 46 |
lazy val bibtex_entries: List[Text.Info[String]] = |
66150 | 47 |
try { Bibtex.entries(text) } |
64833 | 48 |
catch { case ERROR(_) => Nil } |
66676
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
49 |
|
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
50 |
def recode_symbols: List[Protocol.TextEdit] = |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
51 |
(for { |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
52 |
(line, l) <- doc.lines.iterator.zipWithIndex |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
53 |
text1 = Symbol.encode(line.text) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
54 |
if (line.text != text1) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
55 |
} yield { |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
56 |
val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length)) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
57 |
Protocol.TextEdit(range, text1) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
58 |
}).toList |
64830 | 59 |
} |
60 |
||
66100 | 61 |
def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model = |
67292
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67265
diff
changeset
|
62 |
Document_Model(session, editor, node_name, Content.empty, |
71733 | 63 |
node_required = File_Format.registry.is_theory(node_name)) |
64707 | 64 |
} |
65 |
||
64710 | 66 |
sealed case class Document_Model( |
64707 | 67 |
session: Session, |
66100 | 68 |
editor: Server.Editor, |
64707 | 69 |
node_name: Document.Node.Name, |
64830 | 70 |
content: Document_Model.Content, |
66674 | 71 |
version: Option[Long] = None, |
64726 | 72 |
external_file: Boolean = false, |
64707 | 73 |
node_required: Boolean = false, |
74 |
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
|
64816 | 75 |
pending_edits: List[Text.Edit] = Nil, |
65095 | 76 |
published_diagnostics: List[Text.Info[Command.Results]] = Nil, |
77 |
published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model |
|
64605 | 78 |
{ |
66114 | 79 |
model => |
80 |
||
81 |
||
66674 | 82 |
/* content */ |
66114 | 83 |
|
67014 | 84 |
def get_text(range: Text.Range): Option[String] = content.doc.get_text(range) |
66114 | 85 |
|
66674 | 86 |
def set_version(new_version: Long): Document_Model = copy(version = Some(new_version)) |
87 |
||
66114 | 88 |
|
64710 | 89 |
/* external file */ |
90 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
91 |
def external(b: Boolean): Document_Model = copy(external_file = b) |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
92 |
|
64800 | 93 |
def node_visible: Boolean = !external_file |
94 |
||
64710 | 95 |
|
64690 | 96 |
/* header */ |
97 |
||
64702 | 98 |
def node_header: Document.Node.Header = |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
99 |
resources.special_header(node_name) getOrElse |
65359 | 100 |
resources.check_thy_reader(node_name, Scan.char_reader(content.text)) |
64605 | 101 |
|
102 |
||
64707 | 103 |
/* perspective */ |
104 |
||
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
105 |
def node_perspective(doc_blobs: Document.Blobs, caret: Option[Line.Position]) |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
106 |
: (Boolean, Document.Node.Perspective_Text) = |
64800 | 107 |
{ |
108 |
if (is_theory) { |
|
66114 | 109 |
val snapshot = model.snapshot() |
64800 | 110 |
|
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
111 |
val caret_perspective = resources.options.int("vscode_caret_perspective") max 0 |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
112 |
val caret_range = |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
113 |
if (caret_perspective != 0) { |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
114 |
caret match { |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
115 |
case Some(pos) => |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
116 |
val doc = content.doc |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
117 |
val pos1 = Line.Position((pos.line - caret_perspective) max 0) |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
118 |
val pos2 = Line.Position((pos.line + caret_perspective + 1) min doc.lines.length) |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
119 |
Text.Range(doc.offset(pos1).get, doc.offset(pos2).get) |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
120 |
case None => Text.Range.offside |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
121 |
} |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
122 |
} |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
123 |
else if (node_visible) content.text_range |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
124 |
else Text.Range.offside |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
125 |
|
64800 | 126 |
val text_perspective = |
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
127 |
if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty) |
64800 | 128 |
Text.Perspective.full |
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
129 |
else |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
130 |
content.text_range.try_restrict(caret_range) match { |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
131 |
case Some(range) => Text.Perspective(List(range)) |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
132 |
case None => Text.Perspective.empty |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
133 |
} |
64723 | 134 |
|
66100 | 135 |
val overlays = editor.node_overlays(node_name) |
136 |
||
64800 | 137 |
(snapshot.node.load_commands_changed(doc_blobs), |
66100 | 138 |
Document.Node.Perspective(node_required, text_perspective, overlays)) |
64800 | 139 |
} |
140 |
else (false, Document.Node.no_perspective_text) |
|
141 |
} |
|
142 |
||
64707 | 143 |
|
64800 | 144 |
/* blob */ |
145 |
||
146 |
def get_blob: Option[Document.Blob] = |
|
147 |
if (is_theory) None |
|
69558 | 148 |
else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) |
64707 | 149 |
|
150 |
||
66150 | 151 |
/* bibtex entries */ |
152 |
||
153 |
def bibtex_entries: List[Text.Info[String]] = |
|
154 |
model.content.bibtex_entries |
|
155 |
||
156 |
||
64605 | 157 |
/* edits */ |
158 |
||
65160 | 159 |
def change_text(text: String, range: Option[Line.Range] = None): Option[Document_Model] = |
64709 | 160 |
{ |
65160 | 161 |
val insert = Line.normalize(text) |
162 |
range match { |
|
163 |
case None => |
|
164 |
Text.Edit.replace(0, content.text, insert) match { |
|
165 |
case Nil => None |
|
166 |
case edits => |
|
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65191
diff
changeset
|
167 |
val content1 = Document_Model.Content(Line.Document(insert)) |
65160 | 168 |
Some(copy(content = content1, pending_edits = pending_edits ::: edits)) |
169 |
} |
|
170 |
case Some(remove) => |
|
171 |
content.doc.change(remove, insert) match { |
|
172 |
case None => error("Failed to apply document change: " + remove) |
|
173 |
case Some((Nil, _)) => None |
|
174 |
case Some((edits, doc1)) => |
|
175 |
val content1 = Document_Model.Content(doc1) |
|
176 |
Some(copy(content = content1, pending_edits = pending_edits ::: edits)) |
|
177 |
} |
|
64709 | 178 |
} |
179 |
} |
|
180 |
||
66676
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
181 |
def flush_edits( |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
182 |
unicode_symbols: Boolean, |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
183 |
doc_blobs: Document.Blobs, |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
184 |
file: JFile, |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
185 |
caret: Option[Line.Position]) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
186 |
: Option[((List[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] = |
64707 | 187 |
{ |
66676
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
188 |
val workspace_edits = |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
189 |
if (unicode_symbols && version.isDefined) { |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
190 |
val edits = content.recode_symbols |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
191 |
if (edits.nonEmpty) List(Protocol.TextDocumentEdit(file, version.get, edits)) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
192 |
else Nil |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
193 |
} |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
194 |
else Nil |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
195 |
|
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65923
diff
changeset
|
196 |
val (reparse, perspective) = node_perspective(doc_blobs, caret) |
66676
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
197 |
if (reparse || pending_edits.nonEmpty || last_perspective != perspective || |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
198 |
workspace_edits.nonEmpty) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
199 |
{ |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
200 |
val prover_edits = node_edits(node_header, pending_edits, perspective) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
201 |
val edits = (workspace_edits, prover_edits) |
64816 | 202 |
Some((edits, copy(pending_edits = Nil, last_perspective = perspective))) |
64605 | 203 |
} |
64707 | 204 |
else None |
205 |
} |
|
64605 | 206 |
|
207 |
||
65095 | 208 |
/* publish annotations */ |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
209 |
|
65115 | 210 |
def publish(rendering: VSCode_Rendering): |
211 |
(Option[List[Text.Info[Command.Results]]], Option[List[Document_Model.Decoration]], Document_Model) = |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
212 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
213 |
val diagnostics = rendering.diagnostics |
65120
db6cc23fcf33
proper reset of published decorations: initial value is Nil, afterwards it is a list of canonical length and order;
wenzelm
parents:
65115
diff
changeset
|
214 |
val decorations = |
db6cc23fcf33
proper reset of published decorations: initial value is Nil, afterwards it is a list of canonical length and order;
wenzelm
parents:
65115
diff
changeset
|
215 |
if (node_visible) rendering.decorations |
65140 | 216 |
else { for (deco <- published_decorations) yield Document_Model.Decoration.empty(deco.typ) } |
65095 | 217 |
|
65115 | 218 |
val changed_diagnostics = |
219 |
if (diagnostics == published_diagnostics) None else Some(diagnostics) |
|
220 |
val changed_decorations = |
|
221 |
if (decorations == published_decorations) None |
|
65120
db6cc23fcf33
proper reset of published decorations: initial value is Nil, afterwards it is a list of canonical length and order;
wenzelm
parents:
65115
diff
changeset
|
222 |
else if (published_decorations.isEmpty) Some(decorations) |
65115 | 223 |
else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a) |
224 |
||
225 |
(changed_diagnostics, changed_decorations, |
|
226 |
copy(published_diagnostics = diagnostics, published_decorations = decorations)) |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
227 |
} |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
228 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
229 |
|
64725 | 230 |
/* prover session */ |
64702 | 231 |
|
232 |
def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] |
|
64605 | 233 |
|
64816 | 234 |
def is_stable: Boolean = pending_edits.isEmpty |
235 |
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
236 |
|
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
237 |
def rendering(snapshot: Document.Snapshot): VSCode_Rendering = |
66114 | 238 |
new VSCode_Rendering(snapshot, model) |
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
239 |
def rendering(): VSCode_Rendering = rendering(snapshot()) |
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65926
diff
changeset
|
240 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65926
diff
changeset
|
241 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65926
diff
changeset
|
242 |
/* syntax */ |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65926
diff
changeset
|
243 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65926
diff
changeset
|
244 |
def syntax(): Outer_Syntax = |
67004
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
245 |
if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty |
64605 | 246 |
} |