# HG changeset patch
# User wenzelm
# Date 1431027052 -7200
# Node ID 4f72b00d9952aaf43641758a26d500887182e8e8
# Parent  a6c6a3fb78826e4e13cea01bb5a6095b0d5a4fb7
no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;

diff -r a6c6a3fb7882 -r 4f72b00d9952 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed May 06 23:39:30 2015 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu May 07 21:30:52 2015 +0200
@@ -27,7 +27,6 @@
 
   def apply(buffer: Buffer): Option[Document_Model] =
   {
-    GUI_Thread.require {}
     buffer.getProperty(key) match {
       case model: Document_Model => Some(model)
       case _ => None
@@ -223,17 +222,19 @@
 
   /* pending edits */
 
-  private object pending_edits  // owned by GUI thread
+  private object pending_edits
   {
     private var pending_clear = false
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var last_perspective = Document.Node.no_perspective_text
 
-    def is_pending(): Boolean = pending_clear || pending.nonEmpty
-    def snapshot(): List[Text.Edit] = pending.toList
+    def is_pending(): Boolean = synchronized { pending_clear || pending.nonEmpty }
+    def snapshot(): List[Text.Edit] = synchronized { pending.toList }
 
-    def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
+    def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] = synchronized
     {
+      GUI_Thread.require {}
+
       val clear = pending_clear
       val edits = snapshot()
       val (reparse, perspective) = node_perspective(doc_blobs)
@@ -246,8 +247,10 @@
       else Nil
     }
 
-    def edit(clear: Boolean, e: Text.Edit)
+    def edit(clear: Boolean, e: Text.Edit): Unit = synchronized
     {
+      GUI_Thread.require {}
+
       reset_blob()
       reset_bibtex()
 
@@ -261,10 +264,10 @@
   }
 
   def snapshot(): Document.Snapshot =
-    GUI_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
+    session.snapshot(node_name, pending_edits.snapshot())
 
   def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
-    GUI_Thread.require { pending_edits.flushed_edits(doc_blobs) }
+    pending_edits.flushed_edits(doc_blobs)
 
 
   /* buffer listener */
diff -r a6c6a3fb7882 -r 4f72b00d9952 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed May 06 23:39:30 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu May 07 21:30:52 2015 +0200
@@ -93,7 +93,7 @@
 
     // FIXME lock buffer (!??)
     val data = Isabelle_Sidekick.root_data(buffer)
-    val syntax = GUI_Thread.now { Isabelle.buffer_syntax(buffer) }
+    val syntax = Isabelle.buffer_syntax(buffer)
     val ok =
       if (syntax.isDefined) {
         val ok = parser(buffer, syntax.get, data)
@@ -162,11 +162,9 @@
   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
     val opt_snapshot =
-      GUI_Thread.now {
-        PIDE.document_model(buffer) match {
-          case Some(model) if model.is_theory => Some(model.snapshot)
-          case _ => None
-        }
+      PIDE.document_model(buffer) match {
+        case Some(model) if model.is_theory => Some(model.snapshot)
+        case _ => None
       }
     opt_snapshot match {
       case Some(snapshot) =>
diff -r a6c6a3fb7882 -r 4f72b00d9952 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed May 06 23:39:30 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu May 07 21:30:52 2015 +0200
@@ -148,7 +148,7 @@
 
   /* current document content */
 
-  def snapshot(view: View): Document.Snapshot = GUI_Thread.now
+  def snapshot(view: View): Document.Snapshot =
   {
     val buffer = view.getBuffer
     document_model(buffer) match {