# HG changeset patch
# User wenzelm
# Date 1672078062 -3600
# Node ID 8ebde8164bbaeca88f14f3145c2743e65c7ba951
# Parent  a62a609b5db2fb274af7a25aca262adc0f2c2d7b
tuned signature;

diff -r a62a609b5db2 -r 8ebde8164bba src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 19:00:00 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 19:07:42 2022 +0100
@@ -73,7 +73,8 @@
       if (models.isDefinedAt(node_name)) this
       else {
         val edit = Text.Edit.insert(0, text)
-        val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
+        val content = File_Content(node_name, text)
+        val model = File_Model.init(session, content = content, pending_edits = List(edit))
         copy(models = models + (node_name -> model))
       }
   }
@@ -391,21 +392,17 @@
 }
 
 object File_Model {
-  def empty(session: Session): File_Model =
-    File_Model(session, None, Document_Model.File_Content.empty,
-      false, Document.Node.Perspective_Text.empty, Nil)
-
   def init(session: Session,
-    node_name: Document.Node.Name,
-    text: String,
+    content: Document_Model.File_Content = Document_Model.File_Content.empty,
     node_required: Boolean = false,
     last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
     pending_edits: List[Text.Edit] = Nil
   ): File_Model = {
+    val node_name = content.node_name
+
     val file = JEdit_Lib.check_file(node_name.node)
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
-    val content = Document_Model.File_Content(node_name, text)
     val node_required1 = node_required || File_Format.registry.is_theory(node_name)
     File_Model(session, file, content, node_required1, last_perspective, pending_edits)
   }
@@ -700,7 +697,8 @@
     buffer.removeBufferListener(buffer_listener)
     init_token_marker()
 
-    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
+    File_Model.init(session,
+      content = Document_Model.File_Content(node_name, JEdit_Lib.buffer_text(buffer)),
       node_required = node_required,
       last_perspective = buffer_state.get_last_perspective,
       pending_edits = pending_edits)
diff -r a62a609b5db2 -r 8ebde8164bba src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Dec 26 19:00:00 2022 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Dec 26 19:07:42 2022 +0100
@@ -87,7 +87,7 @@
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = {
             Pretty_Tooltip.invoke(() =>
               {
-                val model = File_Model.empty(PIDE.session)
+                val model = File_Model.init(PIDE.session)
                 val rendering = JEdit_Rendering(snapshot, model, options)
                 val info = Text.Info(Text.Range.offside, body)
                 Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
diff -r a62a609b5db2 -r 8ebde8164bba src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Dec 26 19:00:00 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Dec 26 19:07:42 2022 +0100
@@ -32,7 +32,7 @@
   ): (String, JEdit_Rendering) = {
     val command = Command.rich_text(Document_ID.make(), results, formatted_body)
     val snippet = snapshot.snippet(command)
-    val model = File_Model.empty(PIDE.session)
+    val model = File_Model.init(PIDE.session)
     val rendering = apply(snippet, model, PIDE.options.value)
     (command.source, rendering)
   }