ranges of thy_load commands count as visible within perspective;
authorwenzelm
Wed Nov 20 15:53:59 2013 +0100 (2013-11-20)
changeset 545302c1440f70028
parent 54529 2ea4d717d152
child 54531 8330faaeebd5
ranges of thy_load commands count as visible within perspective;
convert ranges wrt. snapshot -- relevant for outdated situation;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Nov 20 15:00:25 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Nov 20 15:53:59 2013 +0100
     1.3 @@ -239,6 +239,9 @@
     1.4  
     1.5    /* blobs */
     1.6  
     1.7 +  def blobs_names: List[Document.Node.Name] =
     1.8 +    for (Exn.Res((name, _)) <- blobs) yield name
     1.9 +
    1.10    def blobs_digests: List[SHA1.Digest] =
    1.11      for (Exn.Res((_, Some(digest))) <- blobs) yield digest
    1.12  
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Nov 20 15:00:25 2013 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Nov 20 15:53:59 2013 +0100
     2.3 @@ -257,7 +257,7 @@
     2.4        (for {
     2.5          (_, node) <- entries
     2.6          cmd <- node.thy_load_commands.iterator
     2.7 -        Exn.Res((name, _)) <- cmd.blobs.iterator
     2.8 +        name <- cmd.blobs_names.iterator
     2.9          if name == file_name
    2.10        } yield cmd).toList
    2.11  
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Nov 20 15:00:25 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Nov 20 15:53:59 2013 +0100
     3.3 @@ -104,11 +104,26 @@
     3.4  
     3.5      if (Isabelle.continuous_checking && is_theory) {
     3.6        val snapshot = this.snapshot()
     3.7 -      Document.Node.Perspective(node_required, Text.Perspective(
     3.8 +
     3.9 +      val document_view_ranges =
    3.10          for {
    3.11            doc_view <- PIDE.document_views(buffer)
    3.12            range <- doc_view.perspective(snapshot).ranges
    3.13 -        } yield range), PIDE.editor.node_overlays(node_name))
    3.14 +        } yield range
    3.15 +
    3.16 +      val thy_load_ranges =
    3.17 +        for {
    3.18 +          cmd <- snapshot.node.thy_load_commands
    3.19 +          blob_name <- cmd.blobs_names
    3.20 +          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
    3.21 +          if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
    3.22 +          start <- snapshot.node.command_start(cmd)
    3.23 +          range = snapshot.convert(cmd.proper_range + start)
    3.24 +        } yield range
    3.25 +
    3.26 +      Document.Node.Perspective(node_required,
    3.27 +        Text.Perspective(document_view_ranges ::: thy_load_ranges),
    3.28 +        PIDE.editor.node_overlays(node_name))
    3.29      }
    3.30      else empty_perspective
    3.31    }
     4.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Nov 20 15:00:25 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Nov 20 15:53:59 2013 +0100
     4.3 @@ -82,7 +82,7 @@
     4.4          PIDE.editor.current_command(view, snapshot) match {
     4.5            case Some(command) =>
     4.6              snapshot.node.command_start(command) match {
     4.7 -              case Some(start) => List(command.proper_range + start)
     4.8 +              case Some(start) => List(snapshot.convert(command.proper_range + start))
     4.9                case None => Nil
    4.10              }
    4.11            case None => Nil