src/Tools/jEdit/src/jedit_editor.scala
2013-08-12 wenzelm 2013-08-12 tuned signature;
2013-08-12 wenzelm 2013-08-12 tuned signature -- more abstract PIDE editor operations;