# HG changeset patch
# User wenzelm
# Date 1453729864 -3600
# Node ID d9410066dbd5c3b87e987dc434eddd52b40fd811
# Parent  d61174f5cc6d9d43d3168d8885a07ed9ec2bf6f7
more thorough syntax_changed: new commands need require new folds;

diff -r d61174f5cc6d -r d9410066dbd5 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Jan 24 20:39:01 2016 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jan 25 14:51:04 2016 +0100
@@ -309,6 +309,7 @@
     for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
       Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
         invoke(text_area)
+    buffer.invalidateCachedFoldLevels
   }
 
   private def init_token_marker()