src/Tools/jEdit/src/session_build.scala
changeset 65256 c3d6dd17d626
parent 62973 744266e32612
child 65828 02dd430d80c5
--- a/src/Tools/jEdit/src/session_build.scala	Wed Mar 15 11:07:07 2017 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Wed Mar 15 12:41:22 2017 +0100
@@ -21,13 +21,15 @@
 
 object Session_Build
 {
-  def session_build(view: View)
+  def check_dialog(view: View)
   {
     GUI_Thread.require {}
 
+    val options = PIDE.options.value
     try {
       if (JEdit_Sessions.session_build_mode() == "none" ||
-          JEdit_Sessions.session_build(no_build = true) == 0) JEdit_Sessions.session_start()
+          JEdit_Sessions.session_build(options, no_build = true) == 0)
+            JEdit_Sessions.session_start(options)
       else new Dialog(view)
     }
     catch {
@@ -38,6 +40,9 @@
 
   private class Dialog(view: View) extends JDialog(view)
   {
+    val options = PIDE.options.value
+
+
     /* text */
 
     private val text = new TextArea {
@@ -162,10 +167,10 @@
     setVisible(true)
 
     Standard_Thread.fork("session_build") {
-      progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name() + " ...")
+      progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name(options) + " ...")
 
       val (out, rc) =
-        try { ("", JEdit_Sessions.session_build(progress = progress)) }
+        try { ("", JEdit_Sessions.session_build(options, progress = progress)) }
         catch {
           case exn: Throwable =>
             (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
@@ -173,7 +178,7 @@
 
       progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
 
-      if (rc == 0) JEdit_Sessions.session_start()
+      if (rc == 0) JEdit_Sessions.session_start(options)
       else progress.echo("Session build failed -- prover process remains inactive!")
 
       return_code(rc)