author | wenzelm |
Wed, 04 Jan 2017 22:57:39 +0100 | |
changeset 64783 | 0be08e4cd0ec |
parent 64779 | 6cdcc271dbd5 |
child 64796 | 22a1b061ae15 |
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 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
14 |
import scala.util.parsing.input.{Reader, CharSequenceReader} |
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( |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
22 |
models: Map[JFile, Document_Model] = Map.empty, |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
23 |
pending_input: Set[JFile] = Set.empty, |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
24 |
pending_output: Set[JFile] = Set.empty) |
64605 | 25 |
} |
26 |
||
64623 | 27 |
class VSCode_Resources( |
64703 | 28 |
val options: Options, |
64706 | 29 |
val text_length: Text.Length, |
64605 | 30 |
loaded_theories: Set[String], |
31 |
known_theories: Map[String, Document.Node.Name], |
|
64718 | 32 |
base_syntax: Outer_Syntax, |
33 |
log: Logger = No_Logger) |
|
34 |
extends Resources(loaded_theories, known_theories, base_syntax, log) |
|
64605 | 35 |
{ |
64703 | 36 |
private val state = Synchronized(VSCode_Resources.State()) |
37 |
||
38 |
||
39 |
/* document node name */ |
|
40 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
41 |
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
|
42 |
|
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
43 |
def node_name(file: JFile): Document.Node.Name = |
64605 | 44 |
{ |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
45 |
val node = file.getPath |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
46 |
val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("") |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
47 |
val master_dir = if (theory == "") "" else file.getParent |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
48 |
Document.Node.Name(node, master_dir, theory) |
64605 | 49 |
} |
64703 | 50 |
|
64759 | 51 |
override def append(dir: String, source_path: Path): String = |
64716 | 52 |
{ |
64759 | 53 |
val path = source_path.expand |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
54 |
if (dir == "" || path.is_absolute) File.platform_path(path) |
64759 | 55 |
else if (path.is_current) dir |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
56 |
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
|
57 |
dir + JFile.separator + File.platform_path(path) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
58 |
else if (path.is_basic) dir + File.platform_path(path) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
59 |
else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath |
64716 | 60 |
} |
61 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
62 |
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
|
63 |
{ |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
64 |
val file = node_file(name) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
65 |
get_model(file) match { |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
66 |
case Some(model) => |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
67 |
f(new CharSequenceReader(model.doc.make_text)) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
68 |
case None if file.isFile => |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
69 |
val reader = Scan.byte_reader(file) |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
70 |
try { f(reader) } finally { reader.close } |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
71 |
case None => |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
72 |
error("No such file: " + quote(file.toString)) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
73 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
74 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
75 |
|
64703 | 76 |
|
77 |
/* document models */ |
|
78 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
79 |
def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
80 |
def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name)) |
64703 | 81 |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
82 |
def update_model(session: Session, file: JFile, text: String) |
64703 | 83 |
{ |
84 |
state.change(st => |
|
64709 | 85 |
{ |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
86 |
val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file))) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
87 |
val model1 = (model.update_text(text) getOrElse model).external(false) |
64709 | 88 |
st.copy( |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
89 |
models = st.models + (file -> model1), |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
90 |
pending_input = st.pending_input + file) |
64709 | 91 |
}) |
64703 | 92 |
} |
93 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
94 |
def close_model(file: JFile): Option[Document_Model] = |
64710 | 95 |
state.change_result(st => |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
96 |
st.models.get(file) match { |
64710 | 97 |
case None => (None, st) |
98 |
case Some(model) => |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
99 |
(Some(model), st.copy(models = st.models + (file -> model.external(true)))) |
64710 | 100 |
}) |
101 |
||
64722 | 102 |
def sync_models(changed_files: Set[JFile]): Boolean = |
64710 | 103 |
state.change_result(st => |
104 |
{ |
|
64719 | 105 |
val changed_models = |
64710 | 106 |
(for { |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
107 |
(file, model) <- st.models.iterator |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
108 |
if changed_files(file) && model.external_file |
64779 | 109 |
text <- try_read(file) |
110 |
model1 <- model.update_text(text) |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
111 |
} yield (file, model1)).toList |
64719 | 112 |
if (changed_models.isEmpty) (false, st) |
64721 | 113 |
else (true, |
114 |
st.copy( |
|
115 |
models = (st.models /: changed_models)(_ + _), |
|
116 |
pending_input = (st.pending_input /: changed_models.iterator.map(_._1))(_ + _))) |
|
64710 | 117 |
}) |
118 |
||
64703 | 119 |
|
64779 | 120 |
/* file content */ |
121 |
||
122 |
def try_read(file: JFile): Option[String] = |
|
123 |
try { Some(File.read(file)) } |
|
124 |
catch { case ERROR(_) => None } |
|
125 |
||
126 |
def get_file_content(file: JFile): Option[String] = |
|
127 |
get_model(file) match { |
|
128 |
case Some(model) => Some(model.doc.make_text) |
|
129 |
case None => try_read(file) |
|
130 |
} |
|
131 |
||
132 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
133 |
/* resolve dependencies */ |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
134 |
|
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
135 |
val thy_info = new Thy_Info(this) |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
136 |
|
64783 | 137 |
def resolve_dependencies(session: Session, watcher: File_Watcher): Boolean = |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
138 |
{ |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
139 |
state.change_result(st => |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
140 |
{ |
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
141 |
val thys = |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
142 |
(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
|
143 |
yield (model.node_name, Position.none)).toList |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
144 |
|
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
145 |
val loaded_models = |
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
146 |
(for { |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
147 |
dep <- thy_info.dependencies("", thys).deps.iterator |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
148 |
file = node_file(dep.name) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
149 |
if !st.models.isDefinedAt(file) |
64783 | 150 |
_ = watcher.register_parent(file) |
64779 | 151 |
text <- try_read(file) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
152 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
153 |
yield { |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
154 |
val model = Document_Model.init(session, node_name(file)) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
155 |
val model1 = (model.update_text(text) getOrElse model).external(true) |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
156 |
(file, model1) |
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
157 |
}).toList |
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
158 |
|
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
159 |
if (loaded_models.isEmpty) (false, st) |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
160 |
else |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
161 |
(true, |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
162 |
st.copy( |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
163 |
models = st.models ++ loaded_models, |
64731
84192ecae582
just one synchronized access to global state: works recursively on JVM;
wenzelm
parents:
64729
diff
changeset
|
164 |
pending_input = st.pending_input ++ loaded_models.iterator.map(_._1))) |
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
165 |
}) |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
166 |
} |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
167 |
|
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
168 |
|
64703 | 169 |
/* pending input */ |
170 |
||
171 |
def flush_input(session: Session) |
|
172 |
{ |
|
173 |
state.change(st => |
|
174 |
{ |
|
64719 | 175 |
val changed_models = |
64703 | 176 |
(for { |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
177 |
file <- st.pending_input.iterator |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
178 |
model <- st.models.get(file) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
179 |
(edits, model1) <- model.flush_edits |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
180 |
} yield (edits, (file, model1))).toList |
64707 | 181 |
|
64719 | 182 |
session.update(Document.Blobs.empty, changed_models.flatMap(_._1)) |
64703 | 183 |
st.copy( |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
184 |
models = (st.models /: changed_models.iterator.map(_._2))(_ + _), |
64703 | 185 |
pending_input = Set.empty) |
186 |
}) |
|
187 |
} |
|
188 |
||
189 |
||
190 |
/* pending output */ |
|
191 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
192 |
def update_output(changed_nodes: List[JFile]): Unit = |
64703 | 193 |
state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) |
194 |
||
195 |
def flush_output(channel: Channel) |
|
196 |
{ |
|
197 |
state.change(st => |
|
198 |
{ |
|
199 |
val changed_iterator = |
|
200 |
for { |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
201 |
file <- st.pending_output.iterator |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
202 |
model <- st.models.get(file) |
64704 | 203 |
rendering = model.rendering() |
64703 | 204 |
(diagnostics, model1) <- model.publish_diagnostics(rendering) |
205 |
} yield { |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
206 |
channel.diagnostics(file, rendering.diagnostics_output(diagnostics)) |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
207 |
(file, model1) |
64703 | 208 |
} |
209 |
st.copy( |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
210 |
models = (st.models /: changed_iterator)(_ + _), |
64703 | 211 |
pending_output = Set.empty) |
212 |
} |
|
213 |
) |
|
214 |
} |
|
64605 | 215 |
} |