tuned;
authorwenzelm
Fri Sep 07 13:58:43 2018 +0200 (9 months ago)
changeset 689221751765b636d
parent 68920 e50312982ba0
child 68923 59d2eab3f8b9
tuned;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Thu Sep 06 16:50:16 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Fri Sep 07 13:58:43 2018 +0200
     1.3 @@ -84,6 +84,9 @@
     1.4    {
     1.5      session =>
     1.6  
     1.7 +
     1.8 +    /* temporary directory */
     1.9 +
    1.10      val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
    1.11      val tmp_dir_name: String = File.path(tmp_dir).implode
    1.12  
    1.13 @@ -309,6 +312,40 @@
    1.14  
    1.15    /* internal state */
    1.16  
    1.17 +  final class Theory private[Thy_Resources](
    1.18 +    val node_name: Document.Node.Name,
    1.19 +    val node_header: Document.Node.Header,
    1.20 +    val text: String,
    1.21 +    val node_required: Boolean)
    1.22 +  {
    1.23 +    override def toString: String = node_name.toString
    1.24 +
    1.25 +    def node_perspective: Document.Node.Perspective_Text =
    1.26 +      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
    1.27 +
    1.28 +    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
    1.29 +      List(node_name -> Document.Node.Deps(node_header),
    1.30 +        node_name -> Document.Node.Edits(text_edits),
    1.31 +        node_name -> node_perspective)
    1.32 +
    1.33 +    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
    1.34 +    {
    1.35 +      val (text_edits, old_required) =
    1.36 +        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
    1.37 +        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
    1.38 +
    1.39 +      if (text_edits.isEmpty && node_required == old_required) Nil
    1.40 +      else make_edits(text_edits)
    1.41 +    }
    1.42 +
    1.43 +    def purge_edits: List[Document.Edit_Text] =
    1.44 +      make_edits(Text.Edit.removes(0, text))
    1.45 +
    1.46 +    def required(required: Boolean): Theory =
    1.47 +      if (required == node_required) this
    1.48 +      else new Theory(node_name, node_header, text, required)
    1.49 +  }
    1.50 +
    1.51    sealed case class State(
    1.52      required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
    1.53      theories: Map[Document.Node.Name, Theory] = Map.empty)
    1.54 @@ -344,40 +381,6 @@
    1.55        Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
    1.56      }
    1.57    }
    1.58 -
    1.59 -  final class Theory private[Thy_Resources](
    1.60 -    val node_name: Document.Node.Name,
    1.61 -    val node_header: Document.Node.Header,
    1.62 -    val text: String,
    1.63 -    val node_required: Boolean)
    1.64 -  {
    1.65 -    override def toString: String = node_name.toString
    1.66 -
    1.67 -    def node_perspective: Document.Node.Perspective_Text =
    1.68 -      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
    1.69 -
    1.70 -    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
    1.71 -      List(node_name -> Document.Node.Deps(node_header),
    1.72 -        node_name -> Document.Node.Edits(text_edits),
    1.73 -        node_name -> node_perspective)
    1.74 -
    1.75 -    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
    1.76 -    {
    1.77 -      val (text_edits, old_required) =
    1.78 -        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
    1.79 -        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
    1.80 -
    1.81 -      if (text_edits.isEmpty && node_required == old_required) Nil
    1.82 -      else make_edits(text_edits)
    1.83 -    }
    1.84 -
    1.85 -    def purge_edits: List[Document.Edit_Text] =
    1.86 -      make_edits(Text.Edit.removes(0, text))
    1.87 -
    1.88 -    def required(required: Boolean): Theory =
    1.89 -      if (required == node_required) this
    1.90 -      else new Theory(node_name, node_header, text, required)
    1.91 -  }
    1.92  }
    1.93  
    1.94  class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)