equal
deleted
inserted
replaced
287 /* syntax */ |
287 /* syntax */ |
288 |
288 |
289 def syntax_changed() |
289 def syntax_changed() |
290 { |
290 { |
291 Untyped.get[LineManager](buffer, "lineMgr").setFirstInvalidLineContext(0) |
291 Untyped.get[LineManager](buffer, "lineMgr").setFirstInvalidLineContext(0) |
292 for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) { |
292 for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) |
293 val c = Class.forName("org.gjt.sp.jedit.textarea.TextArea") |
293 Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged"). |
294 val m = c.getDeclaredMethod("foldStructureChanged") |
294 invoke(text_area) |
295 m.setAccessible(true) |
|
296 m.invoke(text_area) |
|
297 } |
|
298 } |
295 } |
299 |
296 |
300 private def init_token_marker() |
297 private def init_token_marker() |
301 { |
298 { |
302 Isabelle.buffer_token_marker(buffer) match { |
299 Isabelle.buffer_token_marker(buffer) match { |