src/Tools/jEdit/src/plugin.scala
changeset 65256 c3d6dd17d626
parent 65249 c3ee88b9c3cb
child 65257 2307b91159bb
--- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 11:07:07 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 12:41:22 2017 +0100
@@ -302,12 +302,12 @@
 
           val view = jEdit.getActiveView()
 
-          Session_Build.session_build(view)
+          Session_Build.check_dialog(view)
 
           Keymap_Merge.check_dialog(view)
 
           JEdit_Editor.hyperlink_position(true, Document.Snapshot.init,
-            JEdit_Sessions.session_info().open_root).foreach(_.follow(view))
+            JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view))
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
@@ -382,7 +382,7 @@
 
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
-      val resources = new JEdit_Resources(JEdit_Sessions.session_base())
+      val resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
 
       PIDE.session.stop()
       PIDE.session = new Session(resources) {