author | wenzelm |
Thu, 10 Dec 2020 15:08:31 +0100 | |
changeset 72866 | 1d21b4c8023d |
parent 72761 | 4519eeefe3b5 |
child 73340 | 0ffcad1f6130 |
permissions | -rw-r--r-- |
64623 | 1 |
/* Title: Tools/VSCode/src/vscode_resources.scala |
64605 | 2 |
Author: Makarius |
3 |
||
64729 | 4 |
Resources for VSCode Language Server: file-system access and global state. |
64605 | 5 |
*/ |
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import java.io.{File => JFile} |
|
13 |
||
64824 | 14 |
import scala.util.parsing.input.Reader |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
15 |
|
64605 | 16 |
|
64623 | 17 |
object VSCode_Resources |
64605 | 18 |
{ |
64703 | 19 |
/* internal state */ |
20 |
||
21 |
sealed case class State( |
|
72761 | 22 |
models: Map[JFile, VSCode_Model] = Map.empty, |
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
23 |
caret: Option[(JFile, Line.Position)] = None, |
66101
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
24 |
overlays: Document.Overlays = Document.Overlays.empty, |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
25 |
pending_input: Set[JFile] = Set.empty, |
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
26 |
pending_output: Set[JFile] = Set.empty) |
64800 | 27 |
{ |
72761 | 28 |
def update_models(changed: Traversable[(JFile, VSCode_Model)]): State = |
65111
3224a6f7bd6b
more robust treatment of pending input/output: these are often correlated;
wenzelm
parents:
65107
diff
changeset
|
29 |
copy( |
65113 | 30 |
models = models ++ changed, |
31 |
pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file }, |
|
32 |
pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file }) |
|
65111
3224a6f7bd6b
more robust treatment of pending input/output: these are often correlated;
wenzelm
parents:
65107
diff
changeset
|
33 |
|
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
34 |
def update_caret(new_caret: Option[(JFile, Line.Position)]): State = |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
35 |
if (caret == new_caret) this |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
36 |
else |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
37 |
copy( |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
38 |
caret = new_caret, |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
39 |
pending_input = pending_input ++ caret.map(_._1) ++ new_caret.map(_._1)) |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
40 |
|
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
41 |
def get_caret(file: JFile): Option[Line.Position] = |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
42 |
caret match { |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
43 |
case Some((caret_file, caret_pos)) if caret_file == file => Some(caret_pos) |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
44 |
case _ => None |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
45 |
} |
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
46 |
|
64800 | 47 |
lazy val document_blobs: Document.Blobs = |
48 |
Document.Blobs( |
|
49 |
(for { |
|
50 |
(_, model) <- models.iterator |
|
51 |
blob <- model.get_blob |
|
52 |
} yield (model.node_name -> blob)).toMap) |
|
66101
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
53 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
54 |
def change_overlay(insert: Boolean, file: JFile, |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
55 |
command: Command, fn: String, args: List[String]): State = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
56 |
copy( |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
57 |
overlays = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
58 |
if (insert) overlays.insert(command, fn, args) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
59 |
else overlays.remove(command, fn, args), |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
60 |
pending_input = pending_input + file) |
64800 | 61 |
} |
66086 | 62 |
|
63 |
||
64 |
/* caret */ |
|
65 |
||
72761 | 66 |
sealed case class Caret(file: JFile, model: VSCode_Model, offset: Text.Offset) |
66086 | 67 |
{ |
68 |
def node_name: Document.Node.Name = model.node_name |
|
69 |
} |
|
64605 | 70 |
} |
71 |
||
64623 | 72 |
class VSCode_Resources( |
65361 | 73 |
val options: Options, |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
74 |
session_base_info: Sessions.Base_Info, |
65361 | 75 |
log: Logger = No_Logger) |
72627 | 76 |
extends Resources(session_base_info.sessions_structure, session_base_info.check.base, log = log) |
64605 | 77 |
{ |
67292
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
78 |
resources => |
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
79 |
|
64703 | 80 |
private val state = Synchronized(VSCode_Resources.State()) |
81 |
||
82 |
||
65137 | 83 |
/* options */ |
84 |
||
85 |
def pide_extensions: Boolean = options.bool("vscode_pide_extensions") |
|
86 |
def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols") |
|
87 |
def tooltip_margin: Int = options.int("vscode_tooltip_margin") |
|
88 |
def message_margin: Int = options.int("vscode_message_margin") |
|
89 |
||
90 |
||
64703 | 91 |
/* document node name */ |
92 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
93 |
def node_file(name: Document.Node.Name): JFile = new JFile(name.node) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
94 |
|
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
95 |
def node_name(file: JFile): Document.Node.Name = |
70718
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70716
diff
changeset
|
96 |
find_theory(file) getOrElse { |
67060 | 97 |
val node = file.getPath |
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
98 |
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) |
70716 | 99 |
if (session_base.loaded_theory(theory)) loaded_theory_node(theory) |
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
100 |
else { |
67292
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
101 |
val master_dir = file.getParent |
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
102 |
Document.Node.Name(node, master_dir, theory) |
67060 | 103 |
} |
104 |
} |
|
64703 | 105 |
|
64759 | 106 |
override def append(dir: String, source_path: Path): String = |
64716 | 107 |
{ |
64759 | 108 |
val path = source_path.expand |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
109 |
if (dir == "" || path.is_absolute) File.platform_path(path) |
64759 | 110 |
else if (path.is_current) dir |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
111 |
else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator)) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
112 |
dir + JFile.separator + File.platform_path(path) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
113 |
else if (path.is_basic) dir + File.platform_path(path) |
66235
d4fa51e7c4ff
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
wenzelm
parents:
66234
diff
changeset
|
114 |
else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path))) |
64716 | 115 |
} |
116 |
||
72761 | 117 |
def get_models: Map[JFile, VSCode_Model] = state.value.models |
118 |
def get_model(file: JFile): Option[VSCode_Model] = get_models.get(file) |
|
119 |
def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name)) |
|
64834 | 120 |
|
121 |
||
122 |
/* file content */ |
|
123 |
||
69256
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
124 |
def read_file_content(name: Document.Node.Name): Option[String] = |
67292
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
125 |
{ |
69256
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
126 |
make_theory_content(name) orElse { |
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
127 |
try { Some(Line.normalize(File.read(node_file(name)))) } |
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
128 |
catch { case ERROR(_) => None } |
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
129 |
} |
67292
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
130 |
} |
64834 | 131 |
|
69256
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
132 |
def get_file_content(name: Document.Node.Name): Option[String] = |
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
133 |
get_model(name) match { |
64834 | 134 |
case Some(model) => Some(model.content.text) |
69256
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
135 |
case None => read_file_content(name) |
64834 | 136 |
} |
137 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
138 |
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
139 |
{ |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
140 |
val file = node_file(name) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
141 |
get_model(file) match { |
64830 | 142 |
case Some(model) => f(Scan.char_reader(model.content.text)) |
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69256
diff
changeset
|
143 |
case None if file.isFile => using(Scan.byte_reader(file))(f) |
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69256
diff
changeset
|
144 |
case None => error("No such file: " + quote(file.toString)) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
145 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
146 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
147 |
|
64703 | 148 |
|
149 |
/* document models */ |
|
150 |
||
64800 | 151 |
def visible_node(name: Document.Node.Name): Boolean = |
152 |
get_model(name) match { |
|
153 |
case Some(model) => model.node_visible |
|
154 |
case None => false |
|
155 |
} |
|
156 |
||
66100 | 157 |
def change_model( |
158 |
session: Session, |
|
72761 | 159 |
editor: Language_Server.Editor, |
66100 | 160 |
file: JFile, |
66674 | 161 |
version: Long, |
66100 | 162 |
text: String, |
163 |
range: Option[Line.Range] = None) |
|
64703 | 164 |
{ |
165 |
state.change(st => |
|
64709 | 166 |
{ |
72761 | 167 |
val model = st.models.getOrElse(file, VSCode_Model.init(session, editor, node_name(file))) |
66674 | 168 |
val model1 = |
169 |
(model.change_text(text, range) getOrElse model).set_version(version).external(false) |
|
65114
200b787ceb51
potentially redundant pending_output, for the sake of uniformity and reactivity;
wenzelm
parents:
65113
diff
changeset
|
170 |
st.update_models(Some(file -> model1)) |
64709 | 171 |
}) |
64703 | 172 |
} |
173 |
||
65111
3224a6f7bd6b
more robust treatment of pending input/output: these are often correlated;
wenzelm
parents:
65107
diff
changeset
|
174 |
def close_model(file: JFile): Boolean = |
64710 | 175 |
state.change_result(st => |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
176 |
st.models.get(file) match { |
65111
3224a6f7bd6b
more robust treatment of pending input/output: these are often correlated;
wenzelm
parents:
65107
diff
changeset
|
177 |
case None => (false, st) |
65113 | 178 |
case Some(model) => (true, st.update_models(Some(file -> model.external(true)))) |
64710 | 179 |
}) |
180 |
||
65116 | 181 |
def sync_models(changed_files: Set[JFile]): Unit = |
182 |
state.change(st => |
|
64710 | 183 |
{ |
64719 | 184 |
val changed_models = |
64710 | 185 |
(for { |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
186 |
(file, model) <- st.models.iterator |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
187 |
if changed_files(file) && model.external_file |
69256
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
188 |
text <- read_file_content(model.node_name) |
65160 | 189 |
model1 <- model.change_text(text) |
65116 | 190 |
} yield (file, model1)).toList |
191 |
st.update_models(changed_models) |
|
64710 | 192 |
}) |
193 |
||
64703 | 194 |
|
66101
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
195 |
/* overlays */ |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
196 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
197 |
def node_overlays(name: Document.Node.Name): Document.Node.Overlays = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
198 |
state.value.overlays(name) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
199 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
200 |
def insert_overlay(command: Command, fn: String, args: List[String]): Unit = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
201 |
state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args)) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
202 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
203 |
def remove_overlay(command: Command, fn: String, args: List[String]): Unit = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
204 |
state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args)) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
205 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66100
diff
changeset
|
206 |
|
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
207 |
/* resolve dependencies */ |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
208 |
|
66100 | 209 |
def resolve_dependencies( |
210 |
session: Session, |
|
72761 | 211 |
editor: Language_Server.Editor, |
66100 | 212 |
file_watcher: File_Watcher): (Boolean, Boolean) = |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
213 |
{ |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
214 |
state.change_result(st => |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
215 |
{ |
64800 | 216 |
/* theory files */ |
217 |
||
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
218 |
val thys = |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
219 |
(for ((_, model) <- st.models.iterator if model.is_theory) |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
220 |
yield (model.node_name, Position.none)).toList |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
221 |
|
67292
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
222 |
val thy_files1 = resources.dependencies(thys).theories |
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
223 |
|
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
224 |
val thy_files2 = |
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
225 |
(for { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
67547
diff
changeset
|
226 |
(_, model) <- st.models.iterator |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
67547
diff
changeset
|
227 |
thy_name <- resources.make_theory_name(model.node_name) |
67292
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
228 |
} yield thy_name).toList |
64800 | 229 |
|
230 |
||
231 |
/* auxiliary files */ |
|
232 |
||
233 |
val stable_tip_version = |
|
64815 | 234 |
if (st.models.forall(entry => entry._2.is_stable)) |
70775
97d3485028b6
more sequential access to Session.manager.global_state: avoid minor divergence of tip version;
wenzelm
parents:
70718
diff
changeset
|
235 |
session.get_state().stable_tip_version |
64800 | 236 |
else None |
237 |
||
238 |
val aux_files = |
|
239 |
stable_tip_version match { |
|
240 |
case Some(version) => undefined_blobs(version.nodes) |
|
241 |
case None => Nil |
|
242 |
} |
|
243 |
||
244 |
||
245 |
/* loaded models */ |
|
246 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
247 |
val loaded_models = |
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
248 |
(for { |
67292
386ddccfccbf
implicit thy_load context for bibtex files (VSCode);
wenzelm
parents:
67104
diff
changeset
|
249 |
node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator |
64800 | 250 |
file = node_file(node_name) |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
251 |
if !st.models.isDefinedAt(file) |
69256
c78c95d2a3d1
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
wenzelm
parents:
69255
diff
changeset
|
252 |
text <- { file_watcher.register_parent(file); read_file_content(node_name) } |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
253 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
254 |
yield { |
72761 | 255 |
val model = VSCode_Model.init(session, editor, node_name) |
65160 | 256 |
val model1 = (model.change_text(text) getOrElse model).external(true) |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
257 |
(file, model1) |
65117 | 258 |
}).toList |
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
259 |
|
64800 | 260 |
val invoke_input = loaded_models.nonEmpty |
261 |
val invoke_load = stable_tip_version.isEmpty |
|
262 |
||
65113 | 263 |
((invoke_input, invoke_load), st.update_models(loaded_models)) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
264 |
}) |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
265 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
266 |
|
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
267 |
|
64703 | 268 |
/* pending input */ |
269 |
||
66676
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
270 |
def flush_input(session: Session, channel: Channel) |
64703 | 271 |
{ |
272 |
state.change(st => |
|
273 |
{ |
|
64719 | 274 |
val changed_models = |
64703 | 275 |
(for { |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
276 |
file <- st.pending_input.iterator |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
277 |
model <- st.models.get(file) |
66676
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
278 |
(edits, model1) <- |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
279 |
model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file)) |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
280 |
} yield (edits, (file, model1))).toList |
64707 | 281 |
|
66676
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
282 |
for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty } |
72761 | 283 |
channel.write(LSP.WorkspaceEdit(workspace_edits)) |
66676
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
284 |
|
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
285 |
session.update(st.document_blobs, changed_models.flatMap(res => res._1._2)) |
39db5bb7eb0a
recode Unicode text on the spot, e.g. from copy-paste of output;
wenzelm
parents:
66674
diff
changeset
|
286 |
|
64703 | 287 |
st.copy( |
65112 | 288 |
models = st.models ++ changed_models.iterator.map(_._2), |
64703 | 289 |
pending_input = Set.empty) |
290 |
}) |
|
291 |
} |
|
292 |
||
293 |
||
294 |
/* pending output */ |
|
295 |
||
65118 | 296 |
def update_output(changed_nodes: Traversable[JFile]): Unit = |
64703 | 297 |
state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) |
298 |
||
66138 | 299 |
def update_output_visible(): Unit = |
300 |
state.change(st => st.copy(pending_output = st.pending_output ++ |
|
301 |
(for ((file, model) <- st.models.iterator if model.node_visible) yield file))) |
|
302 |
||
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
303 |
def flush_output(channel: Channel): Boolean = |
64703 | 304 |
{ |
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
305 |
state.change_result(st => |
64703 | 306 |
{ |
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
307 |
val (postponed, flushed) = |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
308 |
(for { |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
309 |
file <- st.pending_output.iterator |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
310 |
model <- st.models.get(file) |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
311 |
} yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated) |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
312 |
|
64703 | 313 |
val changed_iterator = |
314 |
for { |
|
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
315 |
(file, model, rendering) <- flushed.iterator |
65115 | 316 |
(changed_diags, changed_decos, model1) = model.publish(rendering) |
317 |
if changed_diags.isDefined || changed_decos.isDefined |
|
65095 | 318 |
} |
319 |
yield { |
|
65115 | 320 |
for (diags <- changed_diags) |
72761 | 321 |
channel.write(LSP.PublishDiagnostics(file, rendering.diagnostics_output(diags))) |
65137 | 322 |
if (pide_extensions) { |
323 |
for (decos <- changed_decos; deco <- decos) |
|
324 |
channel.write(rendering.decoration_output(deco).json(file)) |
|
325 |
} |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
326 |
(file, model1) |
64703 | 327 |
} |
65232
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
328 |
|
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
329 |
(postponed.nonEmpty, |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
330 |
st.copy( |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
331 |
models = st.models ++ changed_iterator, |
ca571c8c0788
avoid race condition between current_state().stable_tip_version and model.rendering();
wenzelm
parents:
65198
diff
changeset
|
332 |
pending_output = postponed.map(_._1).toSet)) |
64703 | 333 |
} |
334 |
) |
|
335 |
} |
|
64870 | 336 |
|
337 |
||
338 |
/* output text */ |
|
339 |
||
72866 | 340 |
def output_text(text: String): String = |
341 |
Symbol.output(unicode_symbols, text) |
|
64870 | 342 |
|
65107 | 343 |
def output_xml(xml: XML.Tree): String = |
344 |
output_text(XML.content(xml)) |
|
345 |
||
64870 | 346 |
def output_pretty(body: XML.Body, margin: Int): String = |
71649 | 347 |
output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric)) |
65107 | 348 |
def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) |
349 |
def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) |
|
65142 | 350 |
|
351 |
||
65189 | 352 |
/* caret handling */ |
353 |
||
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
354 |
def update_caret(caret: Option[(JFile, Line.Position)]) |
65926
0f7821a07aa9
restricted perspective depending on the caret -- important for reactivity when editing big files;
wenzelm
parents:
65532
diff
changeset
|
355 |
{ state.change(_.update_caret(caret)) } |
65189 | 356 |
|
66086 | 357 |
def get_caret(): Option[VSCode_Resources.Caret] = |
65189 | 358 |
{ |
359 |
val st = state.value |
|
360 |
for { |
|
361 |
(file, pos) <- st.caret |
|
362 |
model <- st.models.get(file) |
|
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
363 |
offset <- model.content.doc.offset(pos) |
65189 | 364 |
} |
66086 | 365 |
yield VSCode_Resources.Caret(file, model, offset) |
65189 | 366 |
} |
367 |
||
368 |
||
65142 | 369 |
/* spell checker */ |
370 |
||
371 |
val spell_checker = new Spell_Checker_Variable |
|
372 |
spell_checker.update(options) |
|
64605 | 373 |
} |