equal
deleted
inserted
replaced
264 |
264 |
265 /* session build */ |
265 /* session build */ |
266 |
266 |
267 def session_build(): Int = |
267 def session_build(): Int = |
268 { |
268 { |
269 val system_dialog = new System_Dialog |
269 val system_dialog = new System_Dialog(jEdit.getActiveView()) |
270 |
270 |
271 try { |
271 try { |
272 val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE") |
272 val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE") |
273 if (mode == "none") |
273 if (mode == "none") |
274 system_dialog.return_code(0) |
274 system_dialog.return_code(0) |