--- 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)
--- a/src/Tools/jEdit/src/jedit_resources.scala Sun Jan 08 13:08:17 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sun Jan 08 14:46:04 2017 +0100
@@ -33,7 +33,7 @@
base_syntax: Outer_Syntax)
extends Resources(loaded_theories, known_theories, base_syntax)
{
- /* document node names */
+ /* document node name */
def node_name(buffer: Buffer): Document.Node.Name =
{
@@ -49,9 +49,6 @@
if (name.is_theory) Some(name) else None
}
-
- /* file-system operations */
-
override def append(dir: String, source_path: Path): String =
{
val path = source_path.expand
@@ -67,6 +64,9 @@
}
}
+
+ /* file content */
+
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{
GUI_Thread.now {
@@ -86,8 +86,6 @@
}
- /* file content */
-
private class File_Content_Output(buffer: Buffer) extends
ByteArrayOutputStream(buffer.getLength + 1)
{