src/Tools/jEdit/src/plugin.scala
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 */