# HG changeset patch
# User wenzelm
# Date 1412583891 -7200
# Node ID d9350ec0937e1cb4c4dd8406c156a994ad1d8637
# Parent  d230e7075bcfe65ab039d35e053407d081e6eeac
tuned signature;

diff -r d230e7075bcf -r d9350ec0937e src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sun Oct 05 20:30:58 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Mon Oct 06 10:24:51 2014 +0200
@@ -186,8 +186,8 @@
 
   // context of partial line-oriented scans
   abstract class Line_Context
-  case object Ignored_Context extends Line_Context
-  case class Item_Context(kind: String, delim: Delimited, right: String) extends Line_Context
+  case object Ignored extends Line_Context
+  case class Item(kind: String, delim: Delimited, right: String) extends Line_Context
   case class Delimited(quoted: Boolean, depth: Int)
   val Closed = Delimited(false, 0)
 
@@ -215,7 +215,7 @@
         case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
 
     private def ignored_line: Parser[(Chunk, Line_Context)] =
-      ignored ^^ { case a => (a, Ignored_Context) }
+      ignored ^^ { case a => (a, Ignored) }
 
 
     /* delimited string: outermost "..." or {...} and body with balanced {...} */
@@ -265,12 +265,12 @@
     private def recover_delimited: Parser[Token] =
       """(?m)["{][^@]*""".r ^^ token(Token.Kind.ERROR)
 
-    def delimited_line(item_ctxt: Item_Context): Parser[(Chunk, Line_Context)] =
+    def delimited_line(item_ctxt: Item): Parser[(Chunk, Line_Context)] =
       item_ctxt match {
-        case Item_Context(kind, delim, _) =>
+        case Item(kind, delim, _) =>
           delimited_depth(delim) ^^ { case (s, delim1) =>
             (Chunk(kind, List(Token(Token.Kind.STRING, s))), item_ctxt.copy(delim = delim1)) } |
-          recover_delimited ^^ { case a => (Chunk(kind, List(a)), Ignored_Context) }
+          recover_delimited ^^ { case a => (Chunk(kind, List(a)), Ignored) }
         }
 
 
@@ -330,22 +330,22 @@
     def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] =
     {
       ctxt match {
-        case Ignored_Context =>
+        case Ignored =>
           ignored_line |
           item_start ~ (left_brace | left_paren) ~ opt(item_name) ^^
             { case (kind, a) ~ b ~ c =>
                 val right = if (b.source == "{") "}" else ")"
                 val chunk = Chunk(kind, a ::: List(b) ::: (c getOrElse Nil))
-                (chunk, Item_Context(kind, Closed, right)) } |
-          recover_item ^^ { case a => (a, Ignored_Context) }
-        case item_ctxt @ Item_Context(kind, delim, right) =>
+                (chunk, Item(kind, Closed, right)) } |
+          recover_item ^^ { case a => (a, Ignored) }
+        case item_ctxt @ Item(kind, delim, right) =>
           if (delim.depth > 0)
             delimited_line(item_ctxt) |
             ignored_line
           else {
             delimited_line(item_ctxt) |
             other_token ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
-            right ^^ { case a => (Chunk(kind, List(keyword(a))), Ignored_Context) } |
+            right ^^ { case a => (Chunk(kind, List(keyword(a))), Ignored) } |
             ignored_line
           }
         case _ => failure("")
diff -r d230e7075bcf -r d9350ec0937e src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 20:30:58 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Mon Oct 06 10:24:51 2014 +0200
@@ -127,7 +127,7 @@
       val line_ctxt =
         context match {
           case c: Line_Context => c.context
-          case _ => Some(Bibtex.Ignored_Context)
+          case _ => Some(Bibtex.Ignored)
         }
       val line = if (raw_line == null) new Segment else raw_line