# HG changeset patch
# User wenzelm
# Date 1619984819 -7200
# Node ID 4b413b78cd948f063e597be95f3570f151c822e4
# Parent  20d0abffee997940afee6976bb980894d169229a
more robust indentation: proper line context after insert;

diff -r 20d0abffee99 -r 4b413b78cd94 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Sun May 02 20:51:21 2021 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Sun May 02 21:46:59 2021 +0200
@@ -362,7 +362,10 @@
                     val start_line = text_area.getCaretLine + 1
                     text_area.setSelectedText("\n" + text)
                     val end_line = text_area.getCaretLine
-                    buffer.indentLines(start_line, end_line)
+                    for (line <- start_line to end_line) {
+                      Token_Markup.Line_Context.refresh(buffer, line)
+                      buffer.indentLine(line, true)
+                    }
                   }
                   else {
                     buffer.remove(start, range.length)
diff -r 20d0abffee99 -r 4b413b78cd94 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sun May 02 20:51:21 2021 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun May 02 21:46:59 2021 +0200
@@ -30,6 +30,9 @@
     def init(mode: String): Line_Context =
       new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
 
+    def refresh(buffer: JEditBuffer, line: Int): Unit =
+      buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+
     def before(buffer: JEditBuffer, line: Int): Line_Context =
       if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
       else after(buffer, line - 1)
@@ -42,8 +45,9 @@
           case c: Line_Context => Some(c)
           case _ => None
         }
+
       context getOrElse {
-        buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+        refresh(buffer, line)
         context getOrElse init(JEdit_Lib.buffer_mode(buffer))
       }
     }