--- a/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 08 13:08:17 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 08 14:46:04 2017 +0100
@@ -67,6 +67,28 @@
else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
}
+ def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
+ def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
+
+
+ /* file content */
+
+ def read_file_content(file: JFile): Option[String] =
+ try { Some(Line.normalize(File.read(file))) }
+ catch { case ERROR(_) => None }
+
+ def get_file_content(file: JFile): Option[String] =
+ get_model(file) match {
+ case Some(model) => Some(model.content.text)
+ case None => read_file_content(file)
+ }
+
+ def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
+ for {
+ (_, model) <- state.value.models.iterator
+ Text.Info(range, entry) <- model.content.bibtex_entries.iterator
+ } yield Text.Info(range, (entry, model))
+
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{
val file = node_file(name)
@@ -83,15 +105,6 @@
/* document models */
- def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
- def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
-
- def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
- for {
- (_, model) <- state.value.models.iterator
- Text.Info(range, entry) <- model.content.bibtex_entries.iterator
- } yield Text.Info(range, (entry, model))
-
def visible_node(name: Document.Node.Name): Boolean =
get_model(name) match {
case Some(model) => model.node_visible
@@ -136,19 +149,6 @@
})
- /* file content */
-
- def read_file_content(file: JFile): Option[String] =
- try { Some(Line.normalize(File.read(file))) }
- catch { case ERROR(_) => None }
-
- def get_file_content(file: JFile): Option[String] =
- get_model(file) match {
- case Some(model) => Some(model.content.text)
- case None => read_file_content(file)
- }
-
-
/* resolve dependencies */
val thy_info = new Thy_Info(this)