src/Tools/jEdit/src/plugin.scala
changeset 53277 6aa348237973
parent 53274 1760c01f1c78
child 53337 b3817a0e3211
--- a/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 13:14:00 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 13:53:45 2013 +0200
@@ -43,13 +43,6 @@
   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.recent_syntax == Outer_Syntax.empty) None
-    else Some(current_session.recent_syntax)
-  }
-
   lazy val editor = new JEdit_Editor