# HG changeset patch
# User wenzelm
# Date 1467886080 -7200
# Node ID 3bf02e7fa8a390ca5de5a6d18c56b61251949c06
# Parent  b43a3f7d99355a78f37567aec7271bed20afb789
basic setup for indentation;

diff -r b43a3f7d9935 -r 3bf02e7fa8a3 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Jul 07 12:02:58 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Jul 07 12:08:00 2016 +0200
@@ -18,6 +18,7 @@
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher, Selection}
 import org.gjt.sp.jedit.syntax.TokenMarker
+import org.gjt.sp.jedit.indent.IndentRule
 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
 import org.jedit.options.CombinedOptions
 
@@ -83,6 +84,15 @@
   }
 
 
+  /* indentation */
+
+  def mode_indent_rule(mode: String): Option[IndentRule] =
+    mode match {
+      case "isabelle" => Some(Token_Markup.Indent_Rule)
+      case _ => None
+    }
+
+
   /* structure matchers */
 
   def structure_matchers(name: String): List[StructureMatcher] =
diff -r b43a3f7d9935 -r 3bf02e7fa8a3 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Thu Jul 07 12:02:58 2016 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jul 07 12:08:00 2016 +0200
@@ -12,16 +12,18 @@
 import java.awt.{Font, Color}
 import java.awt.font.TextAttribute
 import java.awt.geom.AffineTransform
+import javax.swing.text.Segment
+
+import scala.collection.convert.WrapAsJava
 
 import org.gjt.sp.util.SyntaxUtilities
 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.textarea.{TextArea, Selection}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
-import javax.swing.text.Segment
-
 
 object Token_Markup
 {
@@ -436,6 +438,15 @@
   }
 
 
+  /* 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
@@ -446,6 +457,9 @@
     {
       super.loadMode(mode, xmh)
       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
+      Isabelle.mode_indent_rule(mode.getName).foreach(indent_rule =>
+        Untyped.set[java.util.List[IndentRule]](
+          mode, "indentRules", WrapAsJava.seqAsJavaList(List(indent_rule))))
     }
   }
 }