--- 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
--- 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 */
--- 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
{