--- 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")
+ }
+ }
}
--- 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)