# HG changeset patch
# User wenzelm
# Date 1498211733 -7200
# Node ID 6c71a3af85a3875c8c642a1f3f2b3aa9a72cac3d
# Parent  cad55bc7e37ddcaec63d5a75ef6edbc4a055ac93
clarified modules;
tuned;

diff -r cad55bc7e37d -r 6c71a3af85a3 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Jun 22 21:48:57 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 11:55:33 2017 +0200
@@ -259,27 +259,14 @@
           case Some(syntax) if buffer.isInstanceOf[Buffer] =>
             val keywords = syntax.keywords
 
+            val line = text_area.getCaretLine
             val caret = text_area.getCaretPosition
-            val line = text_area.getCaretLine
-            val line_range = JEdit_Lib.line_range(buffer, line)
+            val (toks1, toks2) = Text_Structure.split_line_content(buffer, keywords, line, caret)
 
-            def line_content(start: Text.Offset, stop: Text.Offset, context: Scan.Line_Context)
-              : (List[Token], Scan.Line_Context) =
-            {
-              val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("")
-              val (toks, context1) = Token.explode_line(keywords, text, context)
-              val toks1 = toks.filterNot(_.is_space)
-              (toks1, context1)
-            }
-
-            val context0 = Token_Markup.Line_Context.prev(buffer, line).get_context
-            val (tokens1, context1) = line_content(line_range.start, caret, context0)
-            val (tokens2, _) = line_content(caret, line_range.stop, context1)
-
-            if (tokens1.nonEmpty && keywords.is_indent_command(tokens1.head))
+            if (toks1.nonEmpty && keywords.is_indent_command(toks1.head))
               buffer.indentLine(line, true)
 
-            if (tokens2.isEmpty || keywords.is_indent_command(tokens2.head))
+            if (toks2.isEmpty || keywords.is_indent_command(toks2.head))
               JEdit_Lib.buffer_edit(buffer) {
                 text_area.setSelectedText("\n")
                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
diff -r cad55bc7e37d -r 6c71a3af85a3 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Thu Jun 22 21:48:57 2017 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Jun 23 11:55:33 2017 +0200
@@ -186,6 +186,28 @@
     }
   }
 
+  def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords,
+    range: Text.Range, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
+  {
+    val text = JEdit_Lib.try_get_text(buffer, range).getOrElse("")
+    val (toks, context1) = Token.explode_line(keywords, text, context)
+    val toks1 = toks.filterNot(_.is_space)
+    (toks1, context1)
+  }
+
+  def split_line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, line: Int, caret: Int)
+    : (List[Token], List[Token]) =
+  {
+    val line_range = JEdit_Lib.line_range(buffer, line)
+    val context0 = Token_Markup.Line_Context.prev(buffer, line).get_context
+
+    val (toks1, context1) =
+      line_content(buffer, keywords, Text.Range(line_range.start, caret), context0)
+    val (toks2, _) =
+      line_content(buffer, keywords, Text.Range(caret, line_range.stop), context1)
+    (toks1, toks2)
+  }
+
 
   /* structure matching */