# HG changeset patch
# User wenzelm
# Date 1413622240 -7200
# Node ID 1be9855fb579791e85bab41b9b79ac27856f8d98
# Parent  5bc1d6c4a499d4d810bf9d735cdf55a285d0493f
tuned signature;

diff -r 5bc1d6c4a499 -r 1be9855fb579 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Sat Oct 18 10:32:19 2014 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Sat Oct 18 10:50:40 2014 +0200
@@ -79,7 +79,7 @@
 mode.isabelle-root.folding=sidekick
 mode.isabelle-root.sidekick.parser=isabelle-root
 mode.isabelle.customSettings=true
-mode.isabelle.folding=sidekick
+mode.isabelle.folding=isabelle
 mode.isabelle.sidekick.parser=isabelle
 mode.isabelle.sidekick.showStatusWindow.label=true
 mode.ml.sidekick.parser=isabelle
diff -r 5bc1d6c4a499 -r 1be9855fb579 src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sat Oct 18 10:32:19 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sat Oct 18 10:50:40 2014 +0200
@@ -154,8 +154,7 @@
   private val context_rules = new ParserRuleSet("bibtex", "MAIN")
 
   private class Line_Context(context: Option[Bibtex.Line_Context])
-    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](
-      context_rules, context, Outer_Syntax.Line_Structure.init)
+    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
 
 
   /* token marker */
diff -r 5bc1d6c4a499 -r 1be9855fb579 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Oct 18 10:32:19 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Oct 18 10:50:40 2014 +0200
@@ -175,17 +175,13 @@
 
   /* line context */
 
-  class Generic_Line_Context[C](
-      rules: ParserRuleSet,
-      val context: Option[C],
-      val structure: Outer_Syntax.Line_Structure)
+  class Generic_Line_Context[C](rules: ParserRuleSet, val context: Option[C])
     extends TokenMarker.LineContext(rules, null)
   {
-    override def hashCode: Int = (context, structure).hashCode
+    override def hashCode: Int = context.hashCode
     override def equals(that: Any): Boolean =
       that match {
-        case other: Generic_Line_Context[_] =>
-          context == other.context && structure == other.structure
+        case other: Generic_Line_Context[_] => context == other.context
         case _ => false
       }
   }
@@ -200,12 +196,6 @@
       case _ => None
     }
 
-  def buffer_line_structure(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Structure =
-    buffer_line_context(buffer, line) match {
-      case Some(c) => c.structure
-      case None => Outer_Syntax.Line_Structure.init
-    }
-
 
   /* token marker */
 
@@ -213,8 +203,14 @@
 
   private class Line_Context(
       context: Option[Scan.Line_Context],
-      structure: Outer_Syntax.Line_Structure)
-    extends Generic_Line_Context[Scan.Line_Context](context_rules, context, structure)
+      val structure: Outer_Syntax.Line_Structure)
+    extends Generic_Line_Context[Scan.Line_Context](context_rules, context)
+
+  def buffer_line_structure(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Structure =
+    buffer_line_context[Scan.Line_Context](buffer, line) match {
+      case Some(c: Line_Context) => c.structure
+      case _ => Outer_Syntax.Line_Structure.init
+    }
 
   class Marker(mode: String) extends TokenMarker
   {