author | wenzelm |
Sat, 11 Mar 2017 23:12:55 +0100 | |
changeset 65191 | 4c9c83311cad |
parent 65161 | 6af056380d0b |
child 65196 | e8760a98db78 |
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._ |
|
11 |
||
64710 | 12 |
import java.io.{File => JFile} |
13 |
||
64605 | 14 |
|
64707 | 15 |
object Document_Model |
16 |
{ |
|
65095 | 17 |
/* decorations */ |
18 |
||
65140 | 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 |
} |
|
65105 | 26 |
sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) |
65095 | 27 |
|
28 |
||
29 |
/* content */ |
|
30 |
||
64830 | 31 |
sealed case class Content(doc: Line.Document) |
32 |
{ |
|
65161 | 33 |
override def toString: String = doc.toString |
64830 | 34 |
def text_range: Text.Range = doc.text_range |
35 |
def text: String = doc.text |
|
64877 | 36 |
def try_get_text(range: Text.Range): Option[String] = doc.try_get_text(range) |
64833 | 37 |
|
64830 | 38 |
lazy val bytes: Bytes = Bytes(text) |
39 |
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) |
|
64833 | 40 |
lazy val bibtex_entries: List[Text.Info[String]] = |
41 |
try { Bibtex.document_entries(text) } |
|
42 |
catch { case ERROR(_) => Nil } |
|
64830 | 43 |
} |
44 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
45 |
def init(session: Session, node_name: Document.Node.Name): Document_Model = |
64707 | 46 |
{ |
47 |
val resources = session.resources.asInstanceOf[VSCode_Resources] |
|
64830 | 48 |
val content = Content(Line.Document("", resources.text_length)) |
49 |
Document_Model(session, node_name, content) |
|
64707 | 50 |
} |
51 |
} |
|
52 |
||
64710 | 53 |
sealed case class Document_Model( |
64707 | 54 |
session: Session, |
55 |
node_name: Document.Node.Name, |
|
64830 | 56 |
content: Document_Model.Content, |
64726 | 57 |
external_file: Boolean = false, |
64707 | 58 |
node_required: Boolean = false, |
59 |
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
|
64816 | 60 |
pending_edits: List[Text.Edit] = Nil, |
65095 | 61 |
published_diagnostics: List[Text.Info[Command.Results]] = Nil, |
62 |
published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model |
|
64605 | 63 |
{ |
64710 | 64 |
/* external file */ |
65 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
66 |
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
|
67 |
|
64800 | 68 |
def node_visible: Boolean = !external_file |
69 |
||
64710 | 70 |
|
64690 | 71 |
/* header */ |
72 |
||
64702 | 73 |
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
|
74 |
resources.special_header(node_name) getOrElse |
64830 | 75 |
resources.check_thy_reader("", node_name, Scan.char_reader(content.text)) |
64605 | 76 |
|
77 |
||
64707 | 78 |
/* perspective */ |
79 |
||
64800 | 80 |
def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = |
81 |
{ |
|
82 |
if (is_theory) { |
|
83 |
val snapshot = this.snapshot() |
|
84 |
||
85 |
val text_perspective = |
|
86 |
if (node_visible || snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty) |
|
87 |
Text.Perspective.full |
|
88 |
else Text.Perspective.empty |
|
64723 | 89 |
|
64800 | 90 |
(snapshot.node.load_commands_changed(doc_blobs), |
91 |
Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)) |
|
92 |
} |
|
93 |
else (false, Document.Node.no_perspective_text) |
|
94 |
} |
|
95 |
||
64707 | 96 |
|
64800 | 97 |
/* blob */ |
98 |
||
99 |
def get_blob: Option[Document.Blob] = |
|
100 |
if (is_theory) None |
|
64830 | 101 |
else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))) |
64707 | 102 |
|
103 |
||
64605 | 104 |
/* edits */ |
105 |
||
65160 | 106 |
def change_text(text: String, range: Option[Line.Range] = None): Option[Document_Model] = |
64709 | 107 |
{ |
65160 | 108 |
val insert = Line.normalize(text) |
109 |
range match { |
|
110 |
case None => |
|
111 |
Text.Edit.replace(0, content.text, insert) match { |
|
112 |
case Nil => None |
|
113 |
case edits => |
|
114 |
val content1 = Document_Model.Content(Line.Document(insert, content.doc.text_length)) |
|
115 |
Some(copy(content = content1, pending_edits = pending_edits ::: edits)) |
|
116 |
} |
|
117 |
case Some(remove) => |
|
118 |
content.doc.change(remove, insert) match { |
|
119 |
case None => error("Failed to apply document change: " + remove) |
|
120 |
case Some((Nil, _)) => None |
|
121 |
case Some((edits, doc1)) => |
|
122 |
val content1 = Document_Model.Content(doc1) |
|
123 |
Some(copy(content = content1, pending_edits = pending_edits ::: edits)) |
|
124 |
} |
|
64709 | 125 |
} |
126 |
} |
|
127 |
||
64800 | 128 |
def flush_edits(doc_blobs: Document.Blobs): Option[(List[Document.Edit_Text], Document_Model)] = |
64707 | 129 |
{ |
64800 | 130 |
val (reparse, perspective) = node_perspective(doc_blobs) |
131 |
if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { |
|
64867 | 132 |
val edits = node_edits(node_header, pending_edits, perspective) |
64816 | 133 |
Some((edits, copy(pending_edits = Nil, last_perspective = perspective))) |
64605 | 134 |
} |
64707 | 135 |
else None |
136 |
} |
|
64605 | 137 |
|
138 |
||
65095 | 139 |
/* publish annotations */ |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
140 |
|
65115 | 141 |
def publish(rendering: VSCode_Rendering): |
142 |
(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
|
143 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
144 |
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
|
145 |
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
|
146 |
if (node_visible) rendering.decorations |
65140 | 147 |
else { for (deco <- published_decorations) yield Document_Model.Decoration.empty(deco.typ) } |
65095 | 148 |
|
65115 | 149 |
val changed_diagnostics = |
150 |
if (diagnostics == published_diagnostics) None else Some(diagnostics) |
|
151 |
val changed_decorations = |
|
152 |
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
|
153 |
else if (published_decorations.isEmpty) Some(decorations) |
65115 | 154 |
else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a) |
155 |
||
156 |
(changed_diagnostics, changed_decorations, |
|
157 |
copy(published_diagnostics = diagnostics, published_decorations = decorations)) |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
158 |
} |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
159 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
160 |
|
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
161 |
/* current command */ |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
162 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
163 |
def current_command(snapshot: Document.Snapshot, current_offset: Text.Offset): Option[Command] = |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
164 |
{ |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
165 |
if (is_theory) { |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
166 |
val node = snapshot.version.nodes(node_name) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
167 |
val caret = snapshot.revert(current_offset) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
168 |
val caret_command_iterator = node.command_iterator(caret) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
169 |
if (caret_command_iterator.hasNext) { |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
170 |
val (cmd0, _) = caret_command_iterator.next |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
171 |
node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
172 |
} |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
173 |
else None |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
174 |
} |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
175 |
else snapshot.version.nodes.commands_loading(node_name).headOption |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
176 |
} |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
177 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
178 |
|
64725 | 179 |
/* prover session */ |
64702 | 180 |
|
181 |
def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] |
|
64605 | 182 |
|
64816 | 183 |
def is_stable: Boolean = pending_edits.isEmpty |
184 |
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
|
185 |
|
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
186 |
def rendering(snapshot: Document.Snapshot): VSCode_Rendering = |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
187 |
new VSCode_Rendering(this, snapshot, resources) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65161
diff
changeset
|
188 |
def rendering(): VSCode_Rendering = rendering(snapshot()) |
64605 | 189 |
} |