src/Tools/jEdit/src/plugin.scala
changeset 65262 0fe4ebab9fdf
parent 65261 034c49653a8e
child 65263 c97abf0fa0c1
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 14:08:36 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 14:29:55 2017 +0100
     1.3 @@ -30,13 +30,12 @@
     1.4    def plugin: Plugin =
     1.5      if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
     1.6      else _plugin
     1.7 +
     1.8    def options: JEdit_Options = plugin.options
     1.9 +  def resources: JEdit_Resources = plugin.resources
    1.10  
    1.11    @volatile var session: Session = new Session(JEdit_Resources.empty)
    1.12  
    1.13 -  def resources(): JEdit_Resources =
    1.14 -    session.resources.asInstanceOf[JEdit_Resources]
    1.15 -
    1.16  
    1.17    /* semantic document content */
    1.18  
    1.19 @@ -61,11 +60,33 @@
    1.20  
    1.21  class Plugin extends EBPlugin
    1.22  {
    1.23 -  /* key parts */
    1.24 +  /* options */
    1.25  
    1.26    private var _options: JEdit_Options = null
    1.27 +  private def init_options(): Unit = _options = new JEdit_Options(Options.init())
    1.28    def options: JEdit_Options = _options
    1.29  
    1.30 +
    1.31 +  /* resources */
    1.32 +
    1.33 +  private var _resources: JEdit_Resources = null
    1.34 +  private def init_resources()
    1.35 +  {
    1.36 +    val options = this.options.value
    1.37 +    val session_name = JEdit_Sessions.session_name(options)
    1.38 +    val session_base =
    1.39 +      try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) }
    1.40 +      catch { case ERROR(_) => Sessions.pure_base(options) }
    1.41 +
    1.42 +    _resources =
    1.43 +      new JEdit_Resources(session_base.copy(known_theories =
    1.44 +        for ((a, b) <- session_base.known_theories) yield (a, b.map(File.platform_path(_)))))
    1.45 +  }
    1.46 +  def resources: JEdit_Resources = _resources
    1.47 +
    1.48 +
    1.49 +  /* misc support */
    1.50 +
    1.51    val completion_history = new Completion.History_Variable
    1.52    val spell_checker = new Spell_Checker_Variable
    1.53  
    1.54 @@ -109,7 +130,7 @@
    1.55            val thys =
    1.56              (for ((node_name, model) <- models.iterator if model.is_theory)
    1.57                yield (node_name, Position.none)).toList
    1.58 -          val thy_files = PIDE.resources.thy_info.dependencies("", thys).deps.map(_.name)
    1.59 +          val thy_files = resources.thy_info.dependencies("", thys).deps.map(_.name)
    1.60  
    1.61            val aux_files =
    1.62              if (options.bool("jedit_auto_resolve")) {
    1.63 @@ -118,7 +139,7 @@
    1.64                    PIDE.session.current_state().stable_tip_version
    1.65                  else None
    1.66                stable_tip_version match {
    1.67 -                case Some(version) => PIDE.resources.undefined_blobs(version.nodes)
    1.68 +                case Some(version) => resources.undefined_blobs(version.nodes)
    1.69                  case None => delay_load.invoke(); Nil
    1.70                }
    1.71              }
    1.72 @@ -132,7 +153,7 @@
    1.73                val loaded_files =
    1.74                  for {
    1.75                    name <- required_files
    1.76 -                  text <- PIDE.resources.read_file_content(name)
    1.77 +                  text <- resources.read_file_content(name)
    1.78                  } yield (name, text)
    1.79  
    1.80                GUI_Thread.later {
    1.81 @@ -226,7 +247,7 @@
    1.82        } {
    1.83          if (buffer.isLoaded) {
    1.84            JEdit_Lib.buffer_lock(buffer) {
    1.85 -            val node_name = PIDE.resources.node_name(buffer)
    1.86 +            val node_name = resources.node_name(buffer)
    1.87              val model = Document_Model.init(PIDE.session, node_name, buffer)
    1.88              for {
    1.89                text_area <- JEdit_Lib.jedit_text_areas(buffer)
    1.90 @@ -382,22 +403,21 @@
    1.91  
    1.92    override def start()
    1.93    {
    1.94 +    Debug.DISABLE_SEARCH_DIALOG_POOL = true
    1.95 +
    1.96 +
    1.97      /* strict initialization */
    1.98  
    1.99      // adhoc patch of confusing message
   1.100      val orig_plugin_error = jEdit.getProperty("plugin-error.start-error")
   1.101      jEdit.setProperty("plugin-error.start-error", "Cannot start plugin:\n{0}")
   1.102  
   1.103 -
   1.104 -    Debug.DISABLE_SEARCH_DIALOG_POOL = true
   1.105 -
   1.106 -    _options = new JEdit_Options(Options.init())
   1.107 -
   1.108 +    init_options()
   1.109 +    init_resources()
   1.110 +    PIDE._plugin = this
   1.111  
   1.112      jEdit.setProperty("plugin-error.start-error", orig_plugin_error)
   1.113  
   1.114 -    PIDE._plugin = this
   1.115 -
   1.116  
   1.117      /* non-strict initialization */
   1.118  
   1.119 @@ -409,8 +429,6 @@
   1.120        init_mode_provider()
   1.121        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   1.122  
   1.123 -      val resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
   1.124 -
   1.125        PIDE.session.stop()
   1.126        PIDE.session = new Session(resources) {
   1.127          override def output_delay = options.seconds("editor_output_delay")
   1.128 @@ -443,5 +461,7 @@
   1.129      exit_models(JEdit_Lib.jedit_buffers().toList)
   1.130      PIDE.session.stop()
   1.131      file_watcher.shutdown()
   1.132 +
   1.133 +    PIDE._plugin = null
   1.134    }
   1.135  }