actual auto loading of required files;
authorwenzelm
Mon Aug 29 21:55:49 2011 +0200 (2011-08-29)
changeset 4457424444588fddd
parent 44573 51f8895b9ad9
child 44576 f23ac1a679d1
actual auto loading of required files;
eliminated File_Store in favour of Thy_Load;
tuned;
src/Pure/System/session.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/System/session.scala	Mon Aug 29 16:38:56 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Mon Aug 29 21:55:49 2011 +0200
     1.3 @@ -16,15 +16,6 @@
     1.4  
     1.5  object Session
     1.6  {
     1.7 -  /* file store */
     1.8 -
     1.9 -  abstract class File_Store
    1.10 -  {
    1.11 -    def append(master_dir: String, path: Path): String
    1.12 -    def require(file: String): Unit
    1.13 -  }
    1.14 -
    1.15 -
    1.16    /* events */
    1.17  
    1.18    //{{{
    1.19 @@ -43,7 +34,7 @@
    1.20  }
    1.21  
    1.22  
    1.23 -class Session(val file_store: Session.File_Store)
    1.24 +class Session(thy_load: Thy_Load)
    1.25  {
    1.26    /* real time parameters */  // FIXME properties or settings (!?)
    1.27  
    1.28 @@ -117,8 +108,6 @@
    1.29  
    1.30    @volatile var verbose: Boolean = false
    1.31  
    1.32 -  @volatile private var loaded_theories: Set[String] = Set()
    1.33 -
    1.34    @volatile private var syntax = new Outer_Syntax
    1.35    def current_syntax(): Outer_Syntax = syntax
    1.36  
    1.37 @@ -143,23 +132,6 @@
    1.38  
    1.39    /* theory files */
    1.40  
    1.41 -  val thy_load = new Thy_Load
    1.42 -  {
    1.43 -    override def is_loaded(name: String): Boolean =
    1.44 -      loaded_theories.contains(name)
    1.45 -
    1.46 -    override def check_thy(dir: Path, name: String): (String, Thy_Header) =
    1.47 -    {
    1.48 -      val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
    1.49 -      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    1.50 -      val text = Standard_System.read_file(file)
    1.51 -      val header = Thy_Header.read(text)
    1.52 -      (text, header)
    1.53 -    }
    1.54 -  }
    1.55 -
    1.56 -  val thy_info = new Thy_Info(thy_load)
    1.57 -
    1.58    def header_edit(name: String, master_dir: String,
    1.59      header: Document.Node_Header): Document.Edit_Text =
    1.60    {
    1.61 @@ -167,10 +139,10 @@
    1.62      {
    1.63        val thy_name = Thy_Header.base_name(s)
    1.64        if (thy_load.is_loaded(thy_name)) thy_name
    1.65 -      else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
    1.66 +      else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
    1.67      }
    1.68      def norm_use(s: String): String =
    1.69 -      file_store.append(master_dir, Path.explode(s))
    1.70 +      thy_load.append(master_dir, Path.explode(s))
    1.71  
    1.72      val header1: Document.Node_Header =
    1.73        header match {
    1.74 @@ -187,7 +159,6 @@
    1.75  
    1.76    private case class Start(timeout: Time, args: List[String])
    1.77    private case object Interrupt
    1.78 -  private case class Check_Loaded_Files(ask: List[String] => Boolean)
    1.79    private case class Init_Node(name: String, master_dir: String,
    1.80      header: Document.Node_Header, perspective: Text.Perspective, text: String)
    1.81    private case class Edit_Node(name: String, master_dir: String,
    1.82 @@ -337,7 +308,7 @@
    1.83                  catch { case _: Document.State.Fail => bad_result(result) }
    1.84                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    1.85                case List(Keyword.Keyword_Decl(name)) => syntax += name
    1.86 -              case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
    1.87 +              case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
    1.88                case _ => bad_result(result)
    1.89              }
    1.90            }
    1.91 @@ -373,8 +344,6 @@
    1.92          case Interrupt if prover.isDefined =>
    1.93            prover.get.interrupt
    1.94  
    1.95 -        case Check_Loaded_Files(ask) => // FIXME
    1.96 -
    1.97          case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
    1.98            // FIXME compare with existing node
    1.99            handle_edits(name, master_dir, header,
   1.100 @@ -417,11 +386,6 @@
   1.101  
   1.102    def interrupt() { session_actor ! Interrupt }
   1.103  
   1.104 -  def check_loaded_files(ask: List[String] => Boolean)
   1.105 -  {
   1.106 -    session_actor ! Check_Loaded_Files(ask)
   1.107 -  }
   1.108 -
   1.109    // FIXME simplify signature
   1.110    def init_node(name: String, master_dir: String,
   1.111      header: Document.Node_Header, perspective: Text.Perspective, text: String)
     2.1 --- a/src/Pure/Thy/thy_info.scala	Mon Aug 29 16:38:56 2011 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Aug 29 21:55:49 2011 +0200
     2.3 @@ -38,37 +38,38 @@
     2.4  
     2.5    /* dependencies */
     2.6  
     2.7 -  type Deps = Map[String, Exn.Result[(String, Thy_Header)]]  // name -> (text, header)
     2.8 +  type Deps = Map[String, Document.Node_Header]
     2.9  
    2.10 -  private def require_thys(ignored: String => Boolean,
    2.11 -      initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
    2.12 -    (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
    2.13 +  private def require_thys(initiators: List[String],
    2.14 +      deps: Deps, thys: List[(String, String)]): Deps =
    2.15 +    (deps /: thys)(require_thy(initiators, _, _))
    2.16  
    2.17 -  private def require_thy(ignored: String => Boolean,
    2.18 -      initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
    2.19 +  private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
    2.20    {
    2.21 +    val (dir, str) = thy
    2.22      val path = Path.explode(str)
    2.23 -    val name = path.base.implode
    2.24 +    val thy_name = path.base.implode
    2.25 +    val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
    2.26  
    2.27 -    if (deps.isDefinedAt(name) || ignored(name)) deps
    2.28 +    if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
    2.29      else {
    2.30 -      val dir1 = dir + path.dir
    2.31 +      val dir1 = thy_load.append(dir, path.dir)
    2.32        try {
    2.33 -        if (initiators.contains(name)) error(cycle_msg(initiators))
    2.34 -        val (text, header) =
    2.35 -          try { thy_load.check_thy(dir1, name) }
    2.36 +        if (initiators.contains(node_name)) error(cycle_msg(initiators))
    2.37 +        val header =
    2.38 +          try { thy_load.check_thy(node_name) }
    2.39            catch {
    2.40              case ERROR(msg) =>
    2.41 -              cat_error(msg, "The error(s) above occurred while examining theory " +
    2.42 -                quote(name) + required_by("\n", initiators))
    2.43 +              cat_error(msg, "The error(s) above occurred while examining theory file " +
    2.44 +                quote(node_name) + required_by("\n", initiators))
    2.45            }
    2.46 -        require_thys(ignored, name :: initiators, dir1,
    2.47 -          deps + (name -> Exn.Res(text, header)), header.imports)
    2.48 +        val thys = header.imports.map(str => (dir1, str))
    2.49 +        require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys)
    2.50        }
    2.51 -      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    2.52 +      catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) }
    2.53      }
    2.54    }
    2.55  
    2.56 -  def dependencies(dir: Path, str: String): Deps =
    2.57 -    require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
    2.58 +  def dependencies(thys: List[(String, String)]): Deps =
    2.59 +    require_thys(Nil, Map.empty, thys)
    2.60  }
     3.1 --- a/src/Pure/Thy/thy_load.scala	Mon Aug 29 16:38:56 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_load.scala	Mon Aug 29 21:55:49 2011 +0200
     3.3 @@ -8,8 +8,9 @@
     3.4  
     3.5  abstract class Thy_Load
     3.6  {
     3.7 -  def is_loaded(name: String): Boolean
     3.8 -
     3.9 -  def check_thy(dir: Path, name: String): (String, Thy_Header)
    3.10 +  def register_thy(thy_name: String)
    3.11 +  def is_loaded(thy_name: String): Boolean
    3.12 +  def append(master_dir: String, path: Path): String
    3.13 +  def check_thy(node_name: String): Thy_Header
    3.14  }
    3.15  
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 16:38:56 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 21:55:49 2011 +0200
     4.3 @@ -13,9 +13,11 @@
     4.4  import java.io.{File, FileInputStream, IOException}
     4.5  import java.awt.Font
     4.6  import javax.swing.JOptionPane
     4.7 +import javax.swing.text.Segment
     4.8  
     4.9  import scala.collection.mutable
    4.10  import scala.swing.ComboBox
    4.11 +import scala.util.Sorting
    4.12  
    4.13  import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
    4.14    Buffer, EditPane, MiscUtilities, ServiceManager, View}
    4.15 @@ -187,12 +189,10 @@
    4.16    def buffer_text(buffer: JEditBuffer): String =
    4.17      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    4.18  
    4.19 +  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    4.20 +
    4.21    def buffer_path(buffer: Buffer): (String, String) =
    4.22 -  {
    4.23 -    val master_dir = buffer.getDirectory
    4.24 -    val path = buffer.getSymlinkPath
    4.25 -    (master_dir, path)
    4.26 -  }
    4.27 +    (buffer.getDirectory, buffer_name(buffer))
    4.28  
    4.29  
    4.30    /* document model and view */
    4.31 @@ -347,10 +347,19 @@
    4.32  
    4.33  class Plugin extends EBPlugin
    4.34  {
    4.35 -  /* editor file store */
    4.36 +  /* theory files via editor document model */
    4.37 +
    4.38 +  val thy_load = new Thy_Load
    4.39 +  {
    4.40 +    private var loaded_theories: Set[String] = Set()
    4.41  
    4.42 -  private val file_store = new Session.File_Store
    4.43 -  {
    4.44 +    def register_thy(thy_name: String)
    4.45 +    {
    4.46 +      synchronized { loaded_theories += thy_name }
    4.47 +    }
    4.48 +    def is_loaded(thy_name: String): Boolean =
    4.49 +      synchronized { loaded_theories.contains(thy_name) }
    4.50 +
    4.51      def append(master_dir: String, source_path: Path): String =
    4.52      {
    4.53        val path = source_path.expand
    4.54 @@ -364,36 +373,58 @@
    4.55        }
    4.56      }
    4.57  
    4.58 -    def require(canonical_name: String)
    4.59 +    def check_thy(node_name: String): Thy_Header =
    4.60      {
    4.61 -      Swing_Thread.later {
    4.62 -        if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
    4.63 -          jEdit.openFile(null: View, canonical_name)
    4.64 +      Swing_Thread.now {
    4.65 +        Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
    4.66 +          case Some(buffer) =>
    4.67 +            Isabelle.buffer_lock(buffer) {
    4.68 +              val text = new Segment
    4.69 +              buffer.getText(0, buffer.getLength, text)
    4.70 +              Some(Thy_Header.read(text))
    4.71 +            }
    4.72 +          case None => None
    4.73 +        }
    4.74 +      } getOrElse {
    4.75 +        val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
    4.76 +        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    4.77 +        Thy_Header.read(file)
    4.78        }
    4.79      }
    4.80    }
    4.81  
    4.82 -
    4.83 -  /* session manager */
    4.84 +  val thy_info = new Thy_Info(thy_load)
    4.85  
    4.86    private lazy val delay_load =
    4.87 -    Swing_Thread.delay_last(Isabelle.session.load_delay) {
    4.88 -      def ask(files: List[String]): Boolean = Swing_Thread.now
    4.89 +    Swing_Thread.delay_last(Isabelle.session.load_delay)
    4.90 +    {
    4.91 +      val buffers = Isabelle.jedit_buffers().toList
    4.92 +      def loaded_buffer(name: String): Boolean =
    4.93 +        buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
    4.94 +
    4.95 +      val thys =
    4.96 +        for (buffer <- buffers; model <- Isabelle.document_model(buffer))
    4.97 +          yield (model.master_dir, model.thy_name)
    4.98 +      val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
    4.99 +
   4.100 +      val do_load = !files.isEmpty &&
   4.101          {
   4.102 -          val file_list = new scala.swing.TextArea(files.mkString("\n"))
   4.103 -          file_list.editable = false
   4.104 -          val answer =
   4.105 -            Library.confirm_dialog(jEdit.getActiveView(),
   4.106 +          val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
   4.107 +          val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
   4.108 +          files_text.editable = false
   4.109 +          Library.confirm_dialog(jEdit.getActiveView(),
   4.110              "Auto loading of required files",
   4.111              JOptionPane.YES_NO_OPTION,
   4.112 -            "The following files are required to resolve theory imports.",
   4.113 -            "Reload now?",
   4.114 -            file_list)
   4.115 -          answer == 0
   4.116 +            "The following files are required to resolve theory imports.  Reload now?",
   4.117 +            files_text) == 0
   4.118          }
   4.119 +      if (do_load)
   4.120 +        for (file <- files if !loaded_buffer(file))
   4.121 +          jEdit.openFile(null: View, file)
   4.122 +    }
   4.123  
   4.124 -      Isabelle.session.check_loaded_files(ask _)
   4.125 -    }
   4.126 +
   4.127 +  /* session manager */
   4.128  
   4.129    private val session_manager = actor {
   4.130      loop {
   4.131 @@ -471,7 +502,7 @@
   4.132      Isabelle.setup_tooltips()
   4.133      Isabelle_System.init()
   4.134      Isabelle_System.install_fonts()
   4.135 -    Isabelle.session = new Session(file_store)
   4.136 +    Isabelle.session = new Session(thy_load)
   4.137      SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   4.138      if (ModeProvider.instance.isInstanceOf[ModeProvider])
   4.139        ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)