src/Tools/jEdit/src/document_view.scala
changeset 43414 f0770743b7ec
parent 43404 c8369f3d88a1
child 43417 83be997a11d6
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 20:12:59 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 22:05:40 2011 +0200
     1.3 @@ -386,10 +386,6 @@
     1.4                  val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
     1.5                  if line_cmds.exists(changed)
     1.6                } text_area.invalidateScreenLineRange(line, line)
     1.7 -
     1.8 -              // FIXME danger of deadlock!?
     1.9 -              // FIXME potentially slow!?
    1.10 -              model.buffer.propertiesChanged()
    1.11              }
    1.12            }
    1.13