misc tuning and clarification;
authorwenzelm
Thu Jan 05 12:23:25 2017 +0100 (2017-01-05)
changeset 64799c0c648911f1a
parent 64798 0e5ec80c352a
child 64800 415dafeb9669
misc tuning and clarification;
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Jan 05 10:49:47 2017 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Jan 05 12:23:25 2017 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5    final class Overlays private(rep: Map[Node.Name, Node.Overlays])
     1.6    {
     1.7 -    def apply(name: Document.Node.Name): Node.Overlays =
     1.8 +    def apply(name: Node.Name): Node.Overlays =
     1.9        rep.getOrElse(name, Node.Overlays.empty)
    1.10  
    1.11      private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays =
    1.12 @@ -261,10 +261,12 @@
    1.13  
    1.14      def commands: Linear_Set[Command] = _commands.commands
    1.15      def load_commands: List[Command] = _commands.load_commands
    1.16 +    def load_commands_changed(doc_blobs: Blobs): Boolean =
    1.17 +      load_commands.exists(_.blobs_changed(doc_blobs))
    1.18  
    1.19      def clear: Node = new Node(header = header, syntax = syntax)
    1.20  
    1.21 -    def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
    1.22 +    def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged))
    1.23  
    1.24      def update_header(new_header: Node.Header): Node =
    1.25        new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
    1.26 @@ -340,7 +342,7 @@
    1.27      def iterator: Iterator[(Node.Name, Node)] =
    1.28        graph.iterator.map({ case (name, (node, _)) => (name, node) })
    1.29  
    1.30 -    def load_commands(file_name: Node.Name): List[Command] =
    1.31 +    def commands_loading(file_name: Node.Name): List[Command] =
    1.32        (for {
    1.33          (_, node) <- iterator
    1.34          cmd <- node.load_commands.iterator
    1.35 @@ -443,8 +445,8 @@
    1.36  
    1.37      def node_name: Node.Name
    1.38      def node: Node
    1.39 -    def load_commands: List[Command]
    1.40 -    def is_loaded: Boolean
    1.41 +    def commands_loading: List[Command]
    1.42 +    def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
    1.43  
    1.44      def find_command(id: Document_ID.Generic): Option[(Node, Command)]
    1.45      def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
    1.46 @@ -771,13 +773,19 @@
    1.47          def revert(range: Text.Range) = range.map(revert(_))
    1.48  
    1.49          val node_name: Node.Name = name
    1.50 -        def node: Node = version.nodes(name)
    1.51 +        val node: Node = version.nodes(name)
    1.52  
    1.53 -        val load_commands: List[Command] =
    1.54 +        val commands_loading: List[Command] =
    1.55            if (node_name.is_theory) Nil
    1.56 -          else version.nodes.load_commands(node_name)
    1.57 +          else version.nodes.commands_loading(node_name)
    1.58  
    1.59 -        def is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
    1.60 +        def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] =
    1.61 +          (for {
    1.62 +            cmd <- node.load_commands.iterator
    1.63 +            blob_name <- cmd.blobs_names.iterator
    1.64 +            if pred(blob_name)
    1.65 +            start <- node.command_start(cmd)
    1.66 +          } yield convert(cmd.proper_range + start)).toList
    1.67  
    1.68  
    1.69          /* find command */
    1.70 @@ -816,7 +824,7 @@
    1.71          {
    1.72            val former_range = revert(range).inflate_singularity
    1.73            val (chunk_name, command_iterator) =
    1.74 -            load_commands match {
    1.75 +            commands_loading match {
    1.76                case command :: _ => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
    1.77                case _ => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
    1.78              }
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Jan 05 10:49:47 2017 +0100
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Jan 05 12:23:25 2017 +0100
     2.3 @@ -307,7 +307,7 @@
     2.4          val reparse =
     2.5            (syntax_changed /: nodes0.iterator)({
     2.6              case (reparse, (name, node)) =>
     2.7 -              if (node.load_commands.exists(_.blobs_changed(doc_blobs)) && !reparse.contains(name))
     2.8 +              if (node.load_commands_changed(doc_blobs) && !reparse.contains(name))
     2.9                  name :: reparse
    2.10                else reparse
    2.11              })
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Thu Jan 05 10:49:47 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Thu Jan 05 12:23:25 2017 +0100
     3.3 @@ -119,7 +119,8 @@
     3.4      }
     3.5    }
     3.6  
     3.7 -  def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
     3.8 +  def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs)
     3.9 +    : (Boolean, Document.Node.Perspective_Text) =
    3.10    {
    3.11      GUI_Thread.require {}
    3.12  
    3.13 @@ -132,17 +133,8 @@
    3.14            range <- doc_view.perspective(snapshot).ranges
    3.15          } yield range
    3.16  
    3.17 -      val load_ranges =
    3.18 -        for {
    3.19 -          cmd <- snapshot.node.load_commands
    3.20 -          blob_name <- cmd.blobs_names
    3.21 -          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
    3.22 -          if JEdit_Lib.jedit_text_areas(blob_buffer).nonEmpty
    3.23 -          start <- snapshot.node.command_start(cmd)
    3.24 -          range = snapshot.convert(cmd.proper_range + start)
    3.25 -        } yield range
    3.26 -
    3.27 -      val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs))
    3.28 +      val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
    3.29 +      val reparse = snapshot.node.load_commands_changed(doc_blobs)
    3.30  
    3.31        (reparse,
    3.32          Document.Node.Perspective(node_required,
     4.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Jan 05 10:49:47 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Jan 05 12:23:25 2017 +0100
     4.3 @@ -212,10 +212,8 @@
     4.4              if (model.buffer == text_area.getBuffer) {
     4.5                val snapshot = model.snapshot()
     4.6  
     4.7 -              val load_changed =
     4.8 -                snapshot.load_commands.exists(changed.commands.contains)
     4.9 -
    4.10 -              if (changed.assignment || load_changed ||
    4.11 +              if (changed.assignment ||
    4.12 +                  snapshot.commands_loading.exists(changed.commands.contains) ||
    4.13                    (changed.nodes.contains(model.node_name) &&
    4.14                     changed.commands.exists(snapshot.node.commands.contains)))
    4.15                  text_overview.invoke()
     5.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Jan 05 10:49:47 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Jan 05 12:23:25 2017 +0100
     5.3 @@ -60,6 +60,12 @@
     5.4        else None
     5.5      }
     5.6  
     5.7 +  def visible_node(name: Document.Node.Name): Boolean =
     5.8 +    JEdit_Lib.jedit_buffer(name) match {
     5.9 +      case Some(buffer) => JEdit_Lib.jedit_text_areas(buffer).nonEmpty
    5.10 +      case None => false
    5.11 +    }
    5.12 +
    5.13  
    5.14    /* current situation */
    5.15  
    5.16 @@ -109,7 +115,7 @@
    5.17        case _ =>
    5.18          PIDE.document_model(buffer) match {
    5.19            case Some(model) if !model.is_theory =>
    5.20 -            snapshot.version.nodes.load_commands(model.node_name) match {
    5.21 +            snapshot.version.nodes.commands_loading(model.node_name) match {
    5.22                case cmd :: _ => Some(cmd)
    5.23                case Nil => None
    5.24              }