added buffer_text convenience, with explicit locking;
authorwenzelm
Wed Nov 10 20:21:55 2010 +0100 (2010-11-10)
changeset 40474576b88b1dce9
parent 40473 a6db1a68fe3c
child 40475 8a57ff2c2600
added buffer_text convenience, with explicit locking;
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Nov 10 17:53:41 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Wed Nov 10 20:21:55 2010 +0100
     1.3 @@ -219,7 +219,7 @@
     1.4      buffer.setTokenMarker(token_marker)
     1.5      buffer.addBufferListener(buffer_listener)
     1.6      buffer.propertiesChanged()
     1.7 -    pending_edits += Text.Edit.insert(0, buffer.getText(0, buffer.getLength))
     1.8 +    pending_edits += Text.Edit.insert(0, Isabelle.buffer_text(buffer))
     1.9    }
    1.10  
    1.11    def refresh()
     2.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 17:53:41 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 20:21:55 2010 +0100
     2.3 @@ -137,8 +137,7 @@
     2.4          case _ => Nil
     2.5        }
     2.6  
     2.7 -    val buffer = model.buffer
     2.8 -    val text = Isabelle.buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
     2.9 +    val text = Isabelle.buffer_text(model.buffer)
    2.10      val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text)
    2.11  
    2.12      make_tree(0, structure) foreach (node => data.root.add(node))
     3.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Nov 10 17:53:41 2010 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Nov 10 20:21:55 2010 +0100
     3.3 @@ -147,6 +147,9 @@
     3.4    def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
     3.5      Swing_Thread.now { buffer_lock(buffer) { body } }
     3.6  
     3.7 +  def buffer_text(buffer: JEditBuffer): String =
     3.8 +    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
     3.9 +
    3.10  
    3.11    /* dockable windows */
    3.12