# HG changeset patch
# User wenzelm
# Date 1498220688 -7200
# Node ID 09fe6ae943312c22b70e8f348e4ee8c9ed9304e3
# Parent  8903653fc22e0b80a96f864d2f31d9b9d607ac87
tuned;

diff -r 8903653fc22e -r 09fe6ae94331 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Fri Jun 23 14:21:16 2017 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Jun 23 14:24:48 2017 +0200
@@ -187,24 +187,21 @@
   }
 
   def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords,
-    range: Text.Range, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
+    range: Text.Range, ctxt: 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 (toks, ctxt1) = Token.explode_line(keywords, text, ctxt)
     val toks1 = toks.filterNot(_.is_space)
-    (toks1, context1)
+    (toks1, ctxt1)
   }
 
   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)
+    val ctxt0 = Token_Markup.Line_Context.prev(buffer, line).get_context
+    val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0)
+    val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1)
     (toks1, toks2)
   }