changeset 48884 | 963b50ec6d73 |
parent 48872 | 6124e0d1120a |
child 49098 | 673e0ed547af |
--- a/src/Tools/jEdit/src/plugin.scala Wed Aug 22 16:10:23 2012 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 22 16:24:52 2012 +0200 @@ -40,6 +40,13 @@ def thy_load(): JEdit_Thy_Load = session.thy_load.asInstanceOf[JEdit_Thy_Load] + def get_recent_syntax(): Option[Outer_Syntax] = + { + val current_session = session + if (current_session != null) Some(current_session.recent_syntax) + else None + } + /* properties */