364 /* theory files */ |
364 /* theory files */ |
365 |
365 |
366 private lazy val delay_load = |
366 private lazy val delay_load = |
367 Swing_Thread.delay_last(Isabelle.session.load_delay) |
367 Swing_Thread.delay_last(Isabelle.session.load_delay) |
368 { |
368 { |
|
369 val view = jEdit.getActiveView() |
|
370 |
369 val buffers = Isabelle.jedit_buffers().toList |
371 val buffers = Isabelle.jedit_buffers().toList |
370 def loaded_buffer(name: String): Boolean = |
372 def loaded_buffer(name: String): Boolean = |
371 buffers.exists(buffer => Isabelle.buffer_name(buffer) == name) |
373 buffers.exists(buffer => Isabelle.buffer_name(buffer) == name) |
372 |
374 |
373 val thys = |
375 val thys = |
374 for (buffer <- buffers; model <- Isabelle.document_model(buffer)) |
376 for (buffer <- buffers; model <- Isabelle.document_model(buffer)) |
375 yield model.name |
377 yield model.name |
376 val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).filterNot(loaded_buffer _) |
378 val files = Isabelle.thy_info.dependencies(thys).map(_._1.node). |
|
379 filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file)) |
377 |
380 |
378 if (!files.isEmpty) { |
381 if (!files.isEmpty) { |
379 val files_list = new ListView(Library.sort_strings(files)) |
382 val files_list = new ListView(Library.sort_strings(files)) |
380 for (i <- 0 until files.length) |
383 for (i <- 0 until files.length) |
381 files_list.selection.indices += i |
384 files_list.selection.indices += i |
382 |
385 |
383 val answer = |
386 val answer = |
384 Library.confirm_dialog(jEdit.getActiveView(), |
387 Library.confirm_dialog(view, |
385 "Auto loading of required files", |
388 "Auto loading of required files", |
386 JOptionPane.YES_NO_OPTION, |
389 JOptionPane.YES_NO_OPTION, |
387 "The following files are required to resolve theory imports.", |
390 "The following files are required to resolve theory imports.", |
388 "Reload selected files now?", |
391 "Reload selected files now?", |
389 new ScrollPane(files_list)) |
392 new ScrollPane(files_list)) |
390 if (answer == 0) |
393 if (answer == 0) |
391 for { |
394 for { |
392 file <- files |
395 file <- files |
393 if !loaded_buffer(file) && files_list.selection.items.contains(file) |
396 if files_list.selection.items.contains(file) |
394 } jEdit.openFile(null: View, file) |
397 } jEdit.openFile(null: View, file) |
395 } |
398 } |
396 } |
399 } |
397 |
400 |
398 |
401 |