src/Tools/jEdit/src/plugin.scala
changeset 53277 6aa348237973
parent 53274 1760c01f1c78
child 53337 b3817a0e3211
equal deleted inserted replaced
53276:cbed0aa0b0db 53277:6aa348237973
    40     plugin.load_theories()
    40     plugin.load_theories()
    41   }
    41   }
    42 
    42 
    43   def thy_load(): JEdit_Thy_Load =
    43   def thy_load(): JEdit_Thy_Load =
    44     session.thy_load.asInstanceOf[JEdit_Thy_Load]
    44     session.thy_load.asInstanceOf[JEdit_Thy_Load]
    45 
       
    46   def get_recent_syntax(): Option[Outer_Syntax] =
       
    47   {
       
    48     val current_session = session
       
    49     if (current_session.recent_syntax == Outer_Syntax.empty) None
       
    50     else Some(current_session.recent_syntax)
       
    51   }
       
    52 
    45 
    53   lazy val editor = new JEdit_Editor
    46   lazy val editor = new JEdit_Editor
    54 
    47 
    55 
    48 
    56   /* popups */
    49   /* popups */