maintain multiple command chunks and markup trees: for main chunk and loaded files;
authorwenzelm
Tue Feb 11 21:58:31 2014 +0100 (2014-02-11)
changeset 554329c53198dbb1c
parent 55431 e0f20a44ff9d
child 55433 d2960d67f163
maintain multiple command chunks and markup trees: for main chunk and loaded files;
document view for all text areas, including auxiliary files;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Feb 11 17:44:29 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Feb 11 21:58:31 2014 +0100
     1.3 @@ -60,8 +60,13 @@
     1.4      command: Command,
     1.5      status: List[Markup] = Nil,
     1.6      results: Results = Results.empty,
     1.7 -    markup: Markup_Tree = Markup_Tree.empty)
     1.8 +    markups: Map[String, Markup_Tree] = Map.empty)
     1.9    {
    1.10 +    def get_markup(file_name: String): Markup_Tree =
    1.11 +      markups.getOrElse(file_name, Markup_Tree.empty)
    1.12 +
    1.13 +    def markup: Markup_Tree = get_markup("")
    1.14 +
    1.15      def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
    1.16        markup.to_XML(command.range, command.source, filter)
    1.17  
    1.18 @@ -75,7 +80,9 @@
    1.19        markup == other.markup
    1.20  
    1.21      private def add_status(st: Markup): State = copy(status = st :: status)
    1.22 -    private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
    1.23 +
    1.24 +    private def add_markup(file_name: String, m: Text.Markup): State =
    1.25 +      copy(markups = markups + (file_name -> (get_markup(file_name) + m)))
    1.26  
    1.27      def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
    1.28        message match {
    1.29 @@ -84,7 +91,7 @@
    1.30              msg match {
    1.31                case elem @ XML.Elem(markup, Nil) =>
    1.32                  state.add_status(markup)
    1.33 -                  .add_markup(Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
    1.34 +                  .add_markup("", Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
    1.35  
    1.36                case _ =>
    1.37                  java.lang.System.err.println("Ignored status message: " + msg)
    1.38 @@ -93,23 +100,40 @@
    1.39  
    1.40          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
    1.41            (this /: msgs)((state, msg) =>
    1.42 -            msg match {
    1.43 -              case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
    1.44 -              if (id == command.id || id == alt_id) && file_name == "" &&
    1.45 -                  command.range.contains(command.decode(raw_range)) =>
    1.46 -                val range = command.decode(raw_range)
    1.47 -                val props = Position.purge(atts)
    1.48 -                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.49 -                state.add_markup(info)
    1.50 -              case XML.Elem(Markup(name, atts), args)
    1.51 -              if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
    1.52 -                val range = command.proper_range
    1.53 -                val props = Position.purge(atts)
    1.54 -                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.55 -                state.add_markup(info)
    1.56 -              case _ =>
    1.57 -                // FIXME java.lang.System.err.println("Ignored report message: " + msg)
    1.58 -                state
    1.59 +            {
    1.60 +              def bad(): Unit = java.lang.System.err.println("Ignored report message: " + msg)
    1.61 +
    1.62 +              msg match {
    1.63 +                case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
    1.64 +                if id == command.id || id == alt_id =>
    1.65 +                  command.chunks.get(file_name) match {
    1.66 +                    case Some(chunk) =>
    1.67 +                      val range = chunk.decode(raw_range)
    1.68 +                      if (chunk.range.contains(range)) {
    1.69 +                        val props = Position.purge(atts)
    1.70 +                        val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.71 +                        state.add_markup(file_name, info)
    1.72 +                      }
    1.73 +                      else {
    1.74 +                        bad()
    1.75 +                        state
    1.76 +                      }
    1.77 +                    case None =>
    1.78 +                      bad()
    1.79 +                      state
    1.80 +                  }
    1.81 +
    1.82 +                case XML.Elem(Markup(name, atts), args)
    1.83 +                if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
    1.84 +                  val range = command.proper_range
    1.85 +                  val props = Position.purge(atts)
    1.86 +                  val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.87 +                  state.add_markup("", info)
    1.88 +
    1.89 +                case _ =>
    1.90 +                  // FIXME bad()
    1.91 +                  state
    1.92 +              }
    1.93              })
    1.94          case XML.Elem(Markup(name, props), body) =>
    1.95            props match {
    1.96 @@ -119,12 +143,18 @@
    1.97  
    1.98                val st0 = copy(results = results + (i -> message1))
    1.99                val st1 =
   1.100 -                if (Protocol.is_inlined(message))
   1.101 -                  (st0 /: Protocol.message_positions(command.id, command, message))(
   1.102 -                    (st, range) => st.add_markup(Text.Info(range, message2)))
   1.103 +                if (Protocol.is_inlined(message)) {
   1.104 +                  var st1 = st0
   1.105 +                  for {
   1.106 +                    (file_name, chunk) <- command.chunks
   1.107 +                    range <- Protocol.message_positions(command.id, chunk, message)
   1.108 +                  } st1 = st1.add_markup(file_name, Text.Info(range, message2))
   1.109 +                  st1
   1.110 +                }
   1.111                  else st0
   1.112  
   1.113                st1
   1.114 +
   1.115              case _ =>
   1.116                java.lang.System.err.println("Ignored message without serial number: " + message)
   1.117                this
   1.118 @@ -135,7 +165,10 @@
   1.119        copy(
   1.120          status = other.status ::: status,
   1.121          results = results ++ other.results,
   1.122 -        markup = markup ++ other.markup)
   1.123 +        markups =
   1.124 +          (markups.keySet ++ other.markups.keySet)
   1.125 +            .map(a => a -> (get_markup(a) ++ other.get_markup(a))).toMap
   1.126 +      )
   1.127    }
   1.128  
   1.129  
   1.130 @@ -268,6 +301,10 @@
   1.131    def blobs_digests: List[SHA1.Digest] =
   1.132      for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
   1.133  
   1.134 +  val chunks: Map[String, Command.Chunk] =
   1.135 +    (("" -> this) ::
   1.136 +      (for (Exn.Res((name, Some((_, file)))) <- blobs) yield (name.node -> file))).toMap
   1.137 +
   1.138  
   1.139    /* source */
   1.140  
   1.141 @@ -289,7 +326,7 @@
   1.142    /* accumulated results */
   1.143  
   1.144    val init_state: Command.State =
   1.145 -    Command.State(this, results = init_results, markup = init_markup)
   1.146 +    Command.State(this, results = init_results, markups = Map("" -> init_markup))
   1.147  
   1.148    val empty_state: Command.State = Command.State(this)
   1.149  }
     2.1 --- a/src/Pure/PIDE/document.scala	Tue Feb 11 17:44:29 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Tue Feb 11 21:58:31 2014 +0100
     2.3 @@ -361,6 +361,7 @@
     2.4  
     2.5      val node_name: Node.Name
     2.6      val node: Node
     2.7 +    val thy_load_commands: List[Command]
     2.8      def eq_content(other: Snapshot): Boolean
     2.9      def cumulate_markup[A](
    2.10        range: Text.Range,
    2.11 @@ -608,6 +609,10 @@
    2.12          val node_name = name
    2.13          val node = version.nodes(name)
    2.14  
    2.15 +        val thy_load_commands: List[Command] =
    2.16 +          if (node_name.is_theory) Nil
    2.17 +          else version.nodes.thy_load_commands(node_name)
    2.18 +
    2.19          def eq_content(other: Snapshot): Boolean =
    2.20            !is_outdated && !other.is_outdated &&
    2.21              node.commands.size == other.node.commands.size &&
    2.22 @@ -621,15 +626,30 @@
    2.23            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    2.24          {
    2.25            val former_range = revert(range)
    2.26 -          (for {
    2.27 -            (command, command_start) <- node.command_range(former_range)
    2.28 -            st = state.command_state(version, command)
    2.29 -            res = result(st)
    2.30 -            Text.Info(r0, a) <- st.markup.cumulate[A](
    2.31 -              (former_range - command_start).restrict(command.range), info, elements,
    2.32 -              { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
    2.33 -            ).iterator
    2.34 -          } yield Text.Info(convert(r0 + command_start), a)).toList
    2.35 +          thy_load_commands match {
    2.36 +            case thy_load_command :: _ =>
    2.37 +              val file_name = node_name.node
    2.38 +              (for {
    2.39 +                chunk <- thy_load_command.chunks.get(file_name).iterator
    2.40 +                st = state.command_state(version, thy_load_command)
    2.41 +                res = result(st)
    2.42 +                Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A](
    2.43 +                  former_range.restrict(chunk.range), info, elements,
    2.44 +                  { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    2.45 +                ).iterator
    2.46 +              } yield Text.Info(convert(r0), a)).toList
    2.47 +
    2.48 +            case _ =>
    2.49 +              (for {
    2.50 +                (command, command_start) <- node.command_range(former_range)
    2.51 +                st = state.command_state(version, command)
    2.52 +                res = result(st)
    2.53 +                Text.Info(r0, a) <- st.markup.cumulate[A](
    2.54 +                  (former_range - command_start).restrict(command.range), info, elements,
    2.55 +                  { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
    2.56 +                ).iterator
    2.57 +              } yield Text.Info(convert(r0 + command_start), a)).toList
    2.58 +          }
    2.59          }
    2.60  
    2.61          def select_markup[A](range: Text.Range, elements: Option[Set[String]],
     3.1 --- a/src/Pure/PIDE/protocol.scala	Tue Feb 11 17:44:29 2014 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Feb 11 21:58:31 2014 +0100
     3.3 @@ -302,8 +302,14 @@
     3.4        }
     3.5  
     3.6      val set = positions(Set.empty, message)
     3.7 -    if (set.isEmpty)
     3.8 -      set ++ Position.Range.unapply(message.markup.properties).map(chunk.decode(_))
     3.9 +    if (set.isEmpty) {
    3.10 +      message.markup.properties match {
    3.11 +        case Position.Reported(id, file_name, range)
    3.12 +        if id == command_id && file_name == chunk.file_name =>
    3.13 +          set + chunk.decode(range)
    3.14 +        case _ => set
    3.15 +      }
    3.16 +    }
    3.17      else set
    3.18    }
    3.19  }
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Feb 11 17:44:29 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Feb 11 21:58:31 2014 +0100
     4.3 @@ -106,10 +106,13 @@
     4.4        val snapshot = this.snapshot()
     4.5  
     4.6        val document_view_ranges =
     4.7 -        for {
     4.8 -          doc_view <- PIDE.document_views(buffer)
     4.9 -          range <- doc_view.perspective(snapshot).ranges
    4.10 -        } yield range
    4.11 +        if (is_theory) {
    4.12 +          for {
    4.13 +            doc_view <- PIDE.document_views(buffer)
    4.14 +            range <- doc_view.perspective(snapshot).ranges
    4.15 +          } yield range
    4.16 +        }
    4.17 +        else Nil
    4.18  
    4.19        val thy_load_ranges =
    4.20          for {
     5.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Feb 11 17:44:29 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Feb 11 21:58:31 2014 +0100
     5.3 @@ -210,14 +210,18 @@
     5.4                if (model.buffer == text_area.getBuffer) {
     5.5                  val snapshot = model.snapshot()
     5.6  
     5.7 -                if (changed.assignment ||
     5.8 +                val thy_load_changed =
     5.9 +                  snapshot.thy_load_commands.exists(changed.commands.contains)
    5.10 +
    5.11 +                if (changed.assignment || thy_load_changed ||
    5.12                      (changed.nodes.contains(model.node_name) &&
    5.13                       changed.commands.exists(snapshot.node.commands.contains)))
    5.14                    Swing_Thread.later { overview.delay_repaint.invoke() }
    5.15  
    5.16                  val visible_lines = text_area.getVisibleLines
    5.17                  if (visible_lines > 0) {
    5.18 -                  if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines)
    5.19 +                  if (changed.assignment || thy_load_changed)
    5.20 +                    text_area.invalidateScreenLineRange(0, visible_lines)
    5.21                    else {
    5.22                      val visible_range = JEdit_Lib.visible_range(text_area).get
    5.23                      val visible_cmds =
     6.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Feb 11 17:44:29 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Feb 11 21:58:31 2014 +0100
     6.3 @@ -148,8 +148,9 @@
     6.4  {
     6.5    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
     6.6    {
     6.7 -    Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
     6.8 -      case Some(snapshot) =>
     6.9 +    Swing_Thread.now { Document_Model(buffer) } match {
    6.10 +      case Some(model) if model.is_theory =>
    6.11 +        val snapshot = model.snapshot
    6.12          val root = data.root
    6.13          for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
    6.14            Isabelle_Sidekick.swing_markup_tree(
    6.15 @@ -171,7 +172,7 @@
    6.16                })
    6.17          }
    6.18          true
    6.19 -      case None => false
    6.20 +      case _ => false
    6.21      }
    6.22    }
    6.23  }
     7.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Feb 11 17:44:29 2014 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Feb 11 21:58:31 2014 +0100
     7.3 @@ -69,7 +69,7 @@
     7.4      val buffer = view.getBuffer
     7.5  
     7.6      PIDE.document_view(text_area) match {
     7.7 -      case Some(doc_view) =>
     7.8 +      case Some(doc_view) if doc_view.model.is_theory =>
     7.9          val node = snapshot.version.nodes(doc_view.model.node_name)
    7.10          val caret = snapshot.revert(text_area.getCaretPosition)
    7.11          if (caret < buffer.getLength) {
    7.12 @@ -81,7 +81,7 @@
    7.13            else None
    7.14          }
    7.15          else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    7.16 -      case None =>
    7.17 +      case _ =>
    7.18          PIDE.document_model(buffer) match {
    7.19            case Some(model) if !model.is_theory =>
    7.20              snapshot.version.nodes.thy_load_commands(model.node_name) match {
     8.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Feb 11 17:44:29 2014 +0100
     8.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Feb 11 21:58:31 2014 +0100
     8.3 @@ -114,12 +114,10 @@
     8.4                      val model = Document_Model.init(session, buffer, node_name)
     8.5                      (model.init_edits(), model)
     8.6                  }
     8.7 -              if (model.is_theory) {
     8.8 -                for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
     8.9 -                  if (document_view(text_area).map(_.model) != Some(model))
    8.10 -                    Document_View.init(model, text_area)
    8.11 -                }
    8.12 -              }
    8.13 +              for {
    8.14 +                text_area <- JEdit_Lib.jedit_text_areas(buffer)
    8.15 +                if document_view(text_area).map(_.model) != Some(model)
    8.16 +              } Document_View.init(model, text_area)
    8.17                model_edits ::: edits
    8.18              }
    8.19            }
    8.20 @@ -132,8 +130,8 @@
    8.21    {
    8.22      JEdit_Lib.swing_buffer_lock(buffer) {
    8.23        document_model(buffer) match {
    8.24 -        case Some(model) if model.is_theory => Document_View.init(model, text_area)
    8.25 -        case _ =>
    8.26 +        case Some(model) => Document_View.init(model, text_area)
    8.27 +        case None =>
    8.28        }
    8.29      }
    8.30    }