# HG changeset patch
# User wenzelm
# Date 1606398502 -3600
# Node ID 59a7f82a7180f57d4a3a8e6191118e4e4acb011b
# Parent  4fa1aa5dac4f80f3383d09efd23856c03e8555ea
clarified signature;

diff -r 4fa1aa5dac4f -r 59a7f82a7180 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Nov 26 13:15:57 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 26 14:48:22 2020 +0100
@@ -552,6 +552,26 @@
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
 
+    def command_snippet(command: Command): Snapshot =
+    {
+      val node_name = command.node_name
+
+      val nodes0 = version.nodes
+      val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
+      val version1 = Document.Version.make(nodes1)
+
+      val edits: List[Edit_Text] =
+        List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source))))
+
+      val state0 = state.define_command(command)
+      val state1 =
+        state0.continue_history(Future.value(version), edits, Future.value(version1))
+          .define_version(version1, state0.the_assignment(version))
+          .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
+
+      state1.snapshot()
+    }
+
     def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
     def messages: List[(XML.Tree, Position.T)]
     def exports: List[Export.Entry]
diff -r 4fa1aa5dac4f -r 59a7f82a7180 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Thu Nov 26 13:15:57 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Thu Nov 26 14:48:22 2020 +0100
@@ -21,9 +21,21 @@
 
 object JEdit_Rendering
 {
+  /* make rendering */
+
   def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
     new JEdit_Rendering(snapshot, model, options)
 
+  def text(snapshot: Document.Snapshot, formatted_body: XML.Body,
+    results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) =
+  {
+    val command = Command.rich_text(Document_ID.make(), results, formatted_body)
+    val snippet = snapshot.command_snippet(command)
+    val model = File_Model.empty(PIDE.session)
+    val rendering = apply(snippet, model, PIDE.options.value)
+    (command.source, rendering)
+  }
+
 
   /* popup window bounds */
 
diff -r 4fa1aa5dac4f -r 59a7f82a7180 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 26 13:15:57 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 26 14:48:22 2020 +0100
@@ -27,42 +27,6 @@
 import org.gjt.sp.util.{SyntaxUtilities, Log}
 
 
-object Pretty_Text_Area
-{
-  /* auxiliary */
-
-  private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
-    formatted_body: XML.Body): (String, Document.State) =
-  {
-    val command = Command.rich_text(Document_ID.make(), base_results, formatted_body)
-    val node_name = command.node_name
-    val edits: List[Document.Edit_Text] =
-      List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
-
-    val state0 = base_snapshot.state.define_command(command)
-    val version0 = base_snapshot.version
-    val nodes0 = version0.nodes
-
-    val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
-    val version1 = Document.Version.make(nodes1)
-    val state1 =
-      state0.continue_history(Future.value(version0), edits, Future.value(version1))
-        .define_version(version1, state0.the_assignment(version0))
-        .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
-
-    (command.source, state1)
-  }
-
-  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
-    formatted_body: XML.Body): (String, JEdit_Rendering) =
-  {
-    val (text, state) = document_state(base_snapshot, base_results, formatted_body)
-    val model = File_Model.empty(PIDE.session)
-    val rendering = JEdit_Rendering(state.snapshot(), model, PIDE.options.value)
-    (text, rendering)
-  }
-}
-
 class Pretty_Text_Area(
   view: View,
   close_action: () => Unit = () => (),
@@ -77,7 +41,7 @@
   private var current_base_snapshot = Document.Snapshot.init
   private var current_base_results = Command.Results.empty
   private var current_rendering: JEdit_Rendering =
-    Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
+    JEdit_Rendering.text(current_base_snapshot, Nil)._2
   private var future_refresh: Option[Future[Unit]] = None
 
   private val rich_text_area =
@@ -127,15 +91,15 @@
       val metric = JEdit_Lib.pretty_metric(getPainter)
       val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0
 
-      val base_snapshot = current_base_snapshot
-      val base_results = current_base_results
+      val snapshot = current_base_snapshot
+      val results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
 
       future_refresh.map(_.cancel)
       future_refresh =
         Some(Future.fork {
           val (text, rendering) =
-            try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
+            try { JEdit_Rendering.text(snapshot, formatted_body, results = results) }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
           Exn.Interrupt.expose()