src/Tools/jEdit/src/token_markup.scala

--- a/src/Tools/jEdit/src/token_markup.scala	Thu Jul 07 12:08:00 2016 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jul 07 20:54:41 2016 +0200
@@ -20,7 +20,7 @@
 import org.gjt.sp.jedit.{jEdit, Mode, Buffer}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
   ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
-import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
+import org.gjt.sp.jedit.indent.IndentRule
 import org.gjt.sp.jedit.textarea.{TextArea, Selection}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
@@ -438,15 +438,6 @@
   }
 
 
-  /* indentation */
-
-  object Indent_Rule extends IndentRule
-  {
-    def apply(buffer: JEditBuffer, this_line: Int, prev_line: Int, prev_prev_line: Int,
-      actions: java.util.List[IndentAction]): Unit = ()
-  }
-
-
   /* mode provider */
 
   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
@@ -457,7 +448,7 @@
     {
       super.loadMode(mode, xmh)
       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
-      Isabelle.mode_indent_rule(mode.getName).foreach(indent_rule =>
+      Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
         Untyped.set[java.util.List[IndentRule]](
           mode, "indentRules", WrapAsJava.seqAsJavaList(List(indent_rule))))
     }