# HG changeset patch
# User wenzelm
# Date 1392908919 -3600
# Node ID 8d69c15b6fb992104dae66252831730fed15dac1
# Parent  19dffae33cdea48fed8913a5255f221b2d962a4a
added PIDE.snapshot, PIDE.rendering for convenience;

diff -r 19dffae33cde -r 8d69c15b6fb9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Feb 20 16:00:37 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Feb 20 16:08:39 2014 +0100
@@ -142,6 +142,27 @@
       Document_View.exit(text_area)
     }
   }
+
+
+  /* current document content */
+
+  def snapshot(view: View): Document.Snapshot =
+  {
+    val buffer = view.getBuffer
+    document_model(buffer) match {
+      case Some(model) => model.snapshot
+      case None => error("No document model for current buffer")
+    }
+  }
+
+  def rendering(view: View): Rendering =
+  {
+    val text_area = view.getTextArea
+    document_view(text_area) match {
+      case Some(doc_view) => doc_view.get_rendering()
+      case None => error("No document view for current text area")
+    }
+  }
 }
 
 
diff -r 19dffae33cde -r 8d69c15b6fb9 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Thu Feb 20 16:00:37 2014 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala	Thu Feb 20 16:08:39 2014 +0100
@@ -147,7 +147,7 @@
      "The following special toplevel bindings are provided:\n" +
      "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
      "  console -- jEdit Console plugin\n" +
-     "  PIDE    -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.document_model)\n")
+     "  PIDE    -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
   }
 
   override def printPrompt(console: Console, out: Output)