# HG changeset patch
# User wenzelm
# Date 1536321523 -7200
# Node ID 1751765b636ddeb51a6629c1c5796e4fdec7bbdb
# Parent  e50312982ba05bc538829e874c4d3c9dae316bf0
tuned;

diff -r e50312982ba0 -r 1751765b636d src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Thu Sep 06 16:50:16 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Fri Sep 07 13:58:43 2018 +0200
@@ -84,6 +84,9 @@
   {
     session =>
 
+
+    /* temporary directory */
+
     val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
     val tmp_dir_name: String = File.path(tmp_dir).implode
 
@@ -309,6 +312,40 @@
 
   /* internal state */
 
+  final class Theory private[Thy_Resources](
+    val node_name: Document.Node.Name,
+    val node_header: Document.Node.Header,
+    val text: String,
+    val node_required: Boolean)
+  {
+    override def toString: String = node_name.toString
+
+    def node_perspective: Document.Node.Perspective_Text =
+      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
+
+    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
+      List(node_name -> Document.Node.Deps(node_header),
+        node_name -> Document.Node.Edits(text_edits),
+        node_name -> node_perspective)
+
+    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
+    {
+      val (text_edits, old_required) =
+        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
+        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
+
+      if (text_edits.isEmpty && node_required == old_required) Nil
+      else make_edits(text_edits)
+    }
+
+    def purge_edits: List[Document.Edit_Text] =
+      make_edits(Text.Edit.removes(0, text))
+
+    def required(required: Boolean): Theory =
+      if (required == node_required) this
+      else new Theory(node_name, node_header, text, required)
+  }
+
   sealed case class State(
     required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
     theories: Map[Document.Node.Name, Theory] = Map.empty)
@@ -344,40 +381,6 @@
       Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
     }
   }
-
-  final class Theory private[Thy_Resources](
-    val node_name: Document.Node.Name,
-    val node_header: Document.Node.Header,
-    val text: String,
-    val node_required: Boolean)
-  {
-    override def toString: String = node_name.toString
-
-    def node_perspective: Document.Node.Perspective_Text =
-      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
-
-    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
-      List(node_name -> Document.Node.Deps(node_header),
-        node_name -> Document.Node.Edits(text_edits),
-        node_name -> node_perspective)
-
-    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
-    {
-      val (text_edits, old_required) =
-        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
-        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
-
-      if (text_edits.isEmpty && node_required == old_required) Nil
-      else make_edits(text_edits)
-    }
-
-    def purge_edits: List[Document.Edit_Text] =
-      make_edits(Text.Edit.removes(0, text))
-
-    def required(required: Boolean): Theory =
-      if (required == node_required) this
-      else new Theory(node_name, node_header, text, required)
-  }
 }
 
 class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)