--- a/src/Tools/jEdit/src/text_structure.scala Thu Jul 07 20:54:41 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Thu Jul 07 21:10:12 2016 +0200
@@ -12,6 +12,7 @@
import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.Buffer
object Text_Structure
@@ -20,13 +21,23 @@
object Indent_Rule extends IndentRule
{
- def apply(buffer: JEditBuffer, this_line: Int, prev_line: Int, prev_prev_line: Int,
+ def apply(buffer0: JEditBuffer, line: Int, prev_line: Int, prev_prev_line: Int,
actions: java.util.List[IndentAction])
{
- val indent = 0 // FIXME
+ buffer0 match {
+ case buffer: Buffer =>
+ Isabelle.buffer_syntax(buffer) match {
+ case Some(syntax) =>
+ val limit = PIDE.options.value.int("jedit_structure_limit") max 0
- actions.clear()
- actions.add(new IndentAction.AlignOffset(indent))
+ val indent = 0 // FIXME
+
+ actions.clear()
+ actions.add(new IndentAction.AlignOffset(indent))
+ case _ =>
+ }
+ case _ =>
+ }
}
}