# HG changeset patch
# User wenzelm
# Date 1514122667 -3600
# Node ID abac35ee356574968e893f22da9c43c5d6126f4b
# Parent  5e427586cb57f050f89304d4fefb2e4bfd973842
clarified positions;

diff -r 5e427586cb57 -r abac35ee3565 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Sun Dec 24 14:10:41 2017 +0100
+++ b/src/Pure/Thy/bibtex.scala	Sun Dec 24 14:37:47 2017 +0100
@@ -56,9 +56,8 @@
     var line = 1
     var offset = 1
 
-    def token_pos(tok: Token): Position.T =
-      Position.Offset(offset) ::: Position.End_Offset(offset + tok.source.length) :::
-      Position.Line(line)
+    def make_pos(length: Int): Position.T =
+      Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
 
     def advance_pos(tok: Token)
     {
@@ -74,10 +73,10 @@
     for (chunk <- chunks) {
       val name = chunk.name
       if (name != "" && !chunk_pos.isDefinedAt(name)) {
-        chunk_pos += (name -> token_pos(chunk.tokens.head))
+        chunk_pos += (name -> make_pos(chunk.heading_length))
       }
       for (tok <- chunk.tokens) {
-        tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> token_pos(tok))
+        tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
         advance_pos(tok)
       }
     }
@@ -320,8 +319,10 @@
     def is_ignored: Boolean =
       kind == Token.Kind.SPACE ||
       kind == Token.Kind.COMMENT
-    def is_malformed: Boolean = kind ==
-      Token.Kind.ERROR
+    def is_malformed: Boolean =
+      kind == Token.Kind.ERROR
+    def is_open: Boolean =
+      kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
   }
 
   case class Chunk(kind: String, tokens: List[Token])
@@ -349,6 +350,10 @@
         case _ => ""
       }
 
+    def heading_length: Int =
+      if (name == "") 1
+      else (0 /: tokens.takeWhile(tok => !tok.is_open)){ case (n, tok) => n + tok.source.length }
+
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
     def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
     def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined