equal
deleted
inserted
replaced
25 { |
25 { |
26 GUI_Thread.require {} |
26 GUI_Thread.require {} |
27 |
27 |
28 val options = PIDE.options.value |
28 val options = PIDE.options.value |
29 try { |
29 try { |
30 if (JEdit_Sessions.session_build_mode() == "none" || |
30 if (JEdit_Sessions.session_no_build || |
31 JEdit_Sessions.session_build(options, no_build = true) == 0) |
31 JEdit_Sessions.session_build(options, no_build = true) == 0) |
32 JEdit_Sessions.session_start(options) |
32 JEdit_Sessions.session_start(options) |
33 else new Dialog(view) |
33 else new Dialog(view) |
34 } |
34 } |
35 catch { |
35 catch { |