resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
authorwenzelm
Sun Jan 08 16:47:53 2017 +0100 (2017-01-08 ago)
changeset 64835fd1efd6dd385
parent 64834 0a7179ad430d
child 64836 3611f759f896
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
src/Pure/PIDE/resources.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Jan 08 14:46:04 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Jan 08 16:47:53 2017 +0100
     1.3 @@ -145,13 +145,6 @@
     1.4        start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
     1.5      with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
     1.6  
     1.7 -  def check_file(file: String): Boolean =
     1.8 -    try {
     1.9 -      if (Url.is_wellformed(file)) Url.is_readable(file)
    1.10 -      else (new JFile(file)).isFile
    1.11 -    }
    1.12 -    catch { case ERROR(_) => false }
    1.13 -
    1.14  
    1.15    /* special header */
    1.16  
     2.1 --- a/src/Tools/jEdit/etc/options	Sun Jan 08 14:46:04 2017 +0100
     2.2 +++ b/src/Tools/jEdit/etc/options	Sun Jan 08 16:47:53 2017 +0100
     2.3 @@ -6,11 +6,8 @@
     2.4  public option jedit_print_mode : string = ""
     2.5    -- "default print modes for output, separated by commas (change requires restart)"
     2.6  
     2.7 -public option jedit_auto_load : bool = false
     2.8 -  -- "load all required files automatically to resolve theory imports"
     2.9 -
    2.10  public option jedit_auto_resolve : bool = false
    2.11 -  -- "automatically resolve auxiliary files within the editor"
    2.12 +  -- "automatically resolve auxiliary files within the document model"
    2.13  
    2.14  public option jedit_reset_font_size : int = 18
    2.15    -- "reset main text font size"
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 14:46:04 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 16:47:53 2017 +0100
     3.3 @@ -64,18 +64,21 @@
     3.4              buffer_models = buffer_models - buffer)
     3.5        }
     3.6      }
     3.7 +
     3.8 +    def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
     3.9 +      if (models.isDefinedAt(node_name)) this
    3.10 +      else {
    3.11 +        val edit = Text.Edit.insert(0, text)
    3.12 +        val model = File_Model(session, node_name, File_Content(text), pending_edits = List(edit))
    3.13 +        copy(models = models + (node_name -> model))
    3.14 +      }
    3.15    }
    3.16  
    3.17    private val state = Synchronized(State())  // owned by GUI thread
    3.18  
    3.19 -  def get(name: Document.Node.Name): Option[Document_Model] =
    3.20 -    state.value.models.get(name)
    3.21 -
    3.22 -  def get(buffer: JEditBuffer): Option[Buffer_Model] =
    3.23 -    state.value.buffer_models.get(buffer)
    3.24 -
    3.25 -  def is_stable(): Boolean =
    3.26 -    state.value.models_iterator.forall(_.is_stable)
    3.27 +  def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
    3.28 +  def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
    3.29 +  def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
    3.30  
    3.31    def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    3.32      for {
    3.33 @@ -113,6 +116,13 @@
    3.34        else st)
    3.35    }
    3.36  
    3.37 +  def provide_files(session: Session, files: List[(Document.Node.Name, String)])
    3.38 +  {
    3.39 +    GUI_Thread.require {}
    3.40 +    state.change(st =>
    3.41 +      (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
    3.42 +  }
    3.43 +
    3.44  
    3.45    /* required nodes */
    3.46  
    3.47 @@ -191,7 +201,7 @@
    3.48  
    3.49    sealed case class File_Content(text: String)
    3.50    {
    3.51 -    lazy val bytes: Bytes = Bytes(text)
    3.52 +    lazy val bytes: Bytes = Bytes(Symbol.encode(text))
    3.53      lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
    3.54      lazy val bibtex_entries: List[Text.Info[String]] =
    3.55        try { Bibtex.document_entries(text) }
    3.56 @@ -341,7 +351,7 @@
    3.57            _blob match {
    3.58              case Some(x) => x
    3.59              case None =>
    3.60 -              val bytes = PIDE.resources.file_content(buffer)
    3.61 +              val bytes = PIDE.resources.make_file_content(buffer)
    3.62                val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
    3.63                _blob = Some((bytes, chunk))
    3.64                (bytes, chunk)
    3.65 @@ -418,7 +428,7 @@
    3.66      }
    3.67    }
    3.68  
    3.69 -  def is_stable(): Boolean = !pending_edits.nonEmpty
    3.70 +  def is_stable: Boolean = !pending_edits.nonEmpty
    3.71    def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
    3.72  
    3.73    def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
     4.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 14:46:04 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 16:47:53 2017 +0100
     4.3 @@ -37,13 +37,6 @@
     4.4    def invoke(): Unit = delay1_flush.invoke()
     4.5    def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
     4.6  
     4.7 -  def stable_tip_version(): Option[Document.Version] =
     4.8 -    GUI_Thread.require {
     4.9 -      if (Document_Model.is_stable())
    4.10 -        session.current_state().stable_tip_version
    4.11 -      else None
    4.12 -    }
    4.13 -
    4.14    def visible_node(name: Document.Node.Name): Boolean =
    4.15      JEdit_Lib.jedit_buffer(name) match {
    4.16        case Some(buffer) => JEdit_Lib.jedit_text_areas(buffer).nonEmpty
     5.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 14:46:04 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 16:47:53 2017 +0100
     5.3 @@ -67,6 +67,18 @@
     5.4  
     5.5    /* file content */
     5.6  
     5.7 +  def read_file_content(node_name: Document.Node.Name): Option[String] =
     5.8 +  {
     5.9 +    val name = node_name.node
    5.10 +    try {
    5.11 +      val text =
    5.12 +        if (Url.is_wellformed(name)) Url.read(Url(name))
    5.13 +        else File.read(new JFile(name))
    5.14 +      Some(Symbol.decode(Line.normalize(text)))
    5.15 +    }
    5.16 +    catch { case ERROR(_) => None }
    5.17 +  }
    5.18 +
    5.19    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    5.20    {
    5.21      GUI_Thread.now {
    5.22 @@ -104,7 +116,7 @@
    5.23      }
    5.24    }
    5.25  
    5.26 -  def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
    5.27 +  def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
    5.28  
    5.29  
    5.30    /* theory text edits */
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Jan 08 14:46:04 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Jan 08 16:47:53 2017 +0100
     6.3 @@ -180,65 +180,56 @@
     6.4      if (Isabelle.continuous_checking && delay_load_activated() &&
     6.5          PerspectiveManager.isPerspectiveEnabled)
     6.6      {
     6.7 -      try {
     6.8 -        val view = jEdit.getActiveView()
     6.9 -
    6.10 -        val buffers = JEdit_Lib.jedit_buffers().toList
    6.11 -        if (buffers.forall(_.isLoaded)) {
    6.12 -          def loaded_buffer(name: String): Boolean =
    6.13 -            buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
    6.14 +      if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
    6.15 +      else {
    6.16 +        val required_files =
    6.17 +        {
    6.18 +          val models = Document_Model.get_models()
    6.19  
    6.20            val thys =
    6.21 -            for {
    6.22 -              buffer <- buffers
    6.23 -              model <- Document_Model.get(buffer)
    6.24 -              if model.is_theory
    6.25 -            } yield (model.node_name, Position.none)
    6.26 +            (for ((node_name, model) <- models.iterator if model.is_theory)
    6.27 +              yield (node_name, Position.none)).toList
    6.28  
    6.29            val thy_info = new Thy_Info(PIDE.resources)
    6.30 -          val thy_files = thy_info.dependencies("", thys).deps.map(_.name.node)
    6.31 +          val thy_files: List[Document.Node.Name] = thy_info.dependencies("", thys).deps.map(_.name)
    6.32  
    6.33 -          val aux_files =
    6.34 +          val aux_files: List[Document.Node.Name] =
    6.35              if (PIDE.options.bool("jedit_auto_resolve")) {
    6.36 -              PIDE.editor.stable_tip_version() match {
    6.37 -                case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node)
    6.38 +              val stable_tip_version =
    6.39 +                if (models.forall(p => p._2.is_stable))
    6.40 +                  PIDE.session.current_state().stable_tip_version
    6.41 +                else None
    6.42 +              stable_tip_version match {
    6.43 +                case Some(version) => PIDE.resources.undefined_blobs(version.nodes)
    6.44                  case None => delay_load.invoke(); Nil
    6.45                }
    6.46              }
    6.47              else Nil
    6.48  
    6.49 -          val files =
    6.50 -            (thy_files ::: aux_files).filter(file =>
    6.51 -              !loaded_buffer(file) && PIDE.resources.check_file(file))
    6.52 -
    6.53 -          if (files.nonEmpty) {
    6.54 -            if (PIDE.options.bool("jedit_auto_load")) {
    6.55 -              files.foreach(file => jEdit.openFile(null: View, file))
    6.56 -            }
    6.57 -            else {
    6.58 -              val files_list = new ListView(files.sorted)
    6.59 -              for (i <- 0 until files.length)
    6.60 -                files_list.selection.indices += i
    6.61 +          (thy_files ::: aux_files).filterNot(models.isDefinedAt(_))
    6.62 +        }
    6.63 +        if (required_files.nonEmpty) {
    6.64 +          try {
    6.65 +            Standard_Thread.fork("resolve_dependencies") {
    6.66 +              val loaded_files =
    6.67 +                for {
    6.68 +                  name <- required_files
    6.69 +                  text <- PIDE.resources.read_file_content(name)
    6.70 +                } yield (name, text)
    6.71  
    6.72 -              val answer =
    6.73 -                GUI.confirm_dialog(view,
    6.74 -                  "Auto loading of required files",
    6.75 -                  JOptionPane.YES_NO_OPTION,
    6.76 -                  "The following files are required to resolve theory imports.",
    6.77 -                  "Reload selected files now?",
    6.78 -                  new ScrollPane(files_list),
    6.79 -                  new Isabelle.Continuous_Checking)
    6.80 -              if (answer == 0) {
    6.81 -                files.foreach(file =>
    6.82 -                  if (files_list.selection.items.contains(file))
    6.83 -                    jEdit.openFile(null: View, file))
    6.84 +              GUI_Thread.later {
    6.85 +                try {
    6.86 +                  Document_Model.provide_files(PIDE.session, loaded_files)
    6.87 +                  delay_init.invoke()
    6.88 +                }
    6.89 +                finally { delay_load_active.change(_ => false) }
    6.90                }
    6.91              }
    6.92            }
    6.93 +          catch { case _: Throwable => delay_load_active.change(_ => false) }
    6.94          }
    6.95 -        else delay_load.invoke()
    6.96 +        else delay_load_active.change(_ => false)
    6.97        }
    6.98 -      finally { delay_load_active.change(_ => false) }
    6.99      }
   6.100    }
   6.101