equal
deleted
inserted
replaced
76 { |
76 { |
77 try { |
77 try { |
78 Swing_Thread.require() |
78 Swing_Thread.require() |
79 if (model.buffer == text_area.getBuffer) body |
79 if (model.buffer == text_area.getBuffer) body |
80 else { |
80 else { |
81 Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model")) |
81 Log.log(Log.ERROR, this, ERROR("Inconsistent document model")) |
82 default |
82 default |
83 } |
83 } |
84 } |
84 } |
85 catch { case t: Throwable => Log.log(Log.ERROR, this, t); default } |
85 catch { case t: Throwable => Log.log(Log.ERROR, this, t); default } |
86 } |
86 } |