# HG changeset patch
# User wenzelm
# Date 1483883164 -3600
# Node ID 0a7179ad430de15bea8c23a34bba206d8a3f0e21
# Parent  0f410e3b1d200826cc287cb89b613d44bf10678a
tuned;

diff -r 0f410e3b1d20 -r 0a7179ad430d src/Tools/VSCode/src/vscode_resources.scala
--- 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)
diff -r 0f410e3b1d20 -r 0a7179ad430d src/Tools/jEdit/src/jedit_resources.scala
--- 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)
   {