tuned signature -- prefer static type Document.Node.Name;
authorwenzelm
Mon Apr 07 21:23:02 2014 +0200 (2014-04-07)
changeset 56457eea4bbe15745
parent 56450 16d4213d4cbc
child 56458 a8d960baa5c2
tuned signature -- prefer static type Document.Node.Name;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Apr 07 16:37:57 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Apr 07 21:23:02 2014 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4          for {
     1.5            cmd <- snapshot.node.load_commands
     1.6            blob_name <- cmd.blobs_names
     1.7 -          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
     1.8 +          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
     1.9            if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
    1.10            start <- snapshot.node.command_start(cmd)
    1.11            range = snapshot.convert(cmd.proper_range + start)
     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 16:37:57 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 21:23:02 2014 +0200
     2.3 @@ -52,7 +52,7 @@
     2.4    {
     2.5      Swing_Thread.require()
     2.6  
     2.7 -    JEdit_Lib.jedit_buffer(name.node) match {
     2.8 +    JEdit_Lib.jedit_buffer(name) match {
     2.9        case Some(buffer) =>
    2.10          PIDE.document_model(buffer) match {
    2.11            case Some(model) => model.snapshot
     3.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 07 16:37:57 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 07 21:23:02 2014 +0200
     3.3 @@ -120,6 +120,9 @@
     3.4    def jedit_buffer(name: String): Option[Buffer] =
     3.5      jedit_buffers().find(buffer => buffer_name(buffer) == name)
     3.6  
     3.7 +  def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
     3.8 +    jedit_buffer(name.node)
     3.9 +
    3.10    def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    3.11  
    3.12    def jedit_text_areas(view: View): Iterator[JEditTextArea] =
     4.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 07 16:37:57 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 07 21:23:02 2014 +0200
     4.3 @@ -57,7 +57,7 @@
     4.4    override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
     4.5    {
     4.6      Swing_Thread.now {
     4.7 -      JEdit_Lib.jedit_buffer(name.node) match {
     4.8 +      JEdit_Lib.jedit_buffer(name) match {
     4.9          case Some(buffer) =>
    4.10            JEdit_Lib.buffer_lock(buffer) {
    4.11              Some(f(buffer.getSegment(0, buffer.getLength)))
     5.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 07 16:37:57 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 07 21:23:02 2014 +0200
     5.3 @@ -41,7 +41,7 @@
     5.4            if (in_checkbox(peer.indexToLocation(index), point)) {
     5.5              if (clicks == 1) {
     5.6                for {
     5.7 -                buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
     5.8 +                buffer <- JEdit_Lib.jedit_buffer(listData(index))
     5.9                  model <- PIDE.document_model(buffer)
    5.10                } model.node_required = !model.node_required
    5.11              }