clarified modules;
authorwenzelm
Sun Oct 05 18:21:39 2014 +0200 (2014-10-05 ago)
changeset 585476080615b8b96
parent 58546 72e2b2a609c4
child 58548 d0ee64efd624
clarified modules;
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 18:14:26 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 18:21:39 2014 +0200
     1.3 @@ -10,6 +10,8 @@
     1.4  import isabelle._
     1.5  
     1.6  
     1.7 +import scala.collection.mutable
     1.8 +
     1.9  import javax.swing.text.Segment
    1.10  import javax.swing.tree.DefaultMutableTreeNode
    1.11  
    1.12 @@ -26,6 +28,21 @@
    1.13    def check(buffer: Buffer): Boolean =
    1.14      JEdit_Lib.buffer_name(buffer).endsWith(".bib")
    1.15  
    1.16 +  def parse_buffer_entries(buffer: Buffer): List[(String, Text.Offset)] =
    1.17 +  {
    1.18 +    val chunks =
    1.19 +      try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) }
    1.20 +      catch { case ERROR(msg) => Output.warning(msg); Nil }
    1.21 +
    1.22 +    val result = new mutable.ListBuffer[(String, Text.Offset)]
    1.23 +    var offset = 0
    1.24 +    for (chunk <- chunks) {
    1.25 +      if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
    1.26 +      offset += chunk.source.length
    1.27 +    }
    1.28 +    result.toList
    1.29 +  }
    1.30 +
    1.31    def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
    1.32      for {
    1.33        buffer <- JEdit_Lib.jedit_buffers()
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Oct 05 18:14:26 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Oct 05 18:21:39 2014 +0200
     2.3 @@ -167,19 +167,7 @@
     2.4          _bibtex match {
     2.5            case Some(entries) => entries
     2.6            case None =>
     2.7 -            val chunks =
     2.8 -              try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) }
     2.9 -              catch { case ERROR(msg) => Output.warning(msg); Nil }
    2.10 -            val entries =
    2.11 -            {
    2.12 -              val result = new mutable.ListBuffer[(String, Text.Offset)]
    2.13 -              var offset = 0
    2.14 -              for (chunk <- chunks) {
    2.15 -                if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
    2.16 -                offset += chunk.source.length
    2.17 -              }
    2.18 -              result.toList
    2.19 -            }
    2.20 +            val entries = Bibtex_JEdit.parse_buffer_entries(buffer)
    2.21              _bibtex = Some(entries)
    2.22              entries
    2.23          }