clarified Position.Identified: do not require range from prover, default to command position;
authorwenzelm
Tue Aug 12 15:31:24 2014 +0200 (2014-08-12 ago)
changeset 57911dcb758188aa6
parent 57910 a50837b637dc
child 57912 dd9550f84106
clarified Position.Identified: do not require range from prover, default to command position;
src/Pure/General/position.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/General/position.scala	Tue Aug 12 14:15:58 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Tue Aug 12 15:31:24 2014 +0200
     1.3 @@ -81,17 +81,17 @@
     1.4        }
     1.5    }
     1.6  
     1.7 -  object Reported
     1.8 +  object Identified
     1.9    {
    1.10 -    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name, Symbol.Range)] =
    1.11 -      (pos, pos) match {
    1.12 -        case (Id(id), Range(range)) =>
    1.13 +    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
    1.14 +      pos match {
    1.15 +        case Id(id) =>
    1.16            val chunk_name =
    1.17              pos match {
    1.18                case File(name) => Symbol.Text_Chunk.File(name)
    1.19                case _ => Symbol.Text_Chunk.Default
    1.20              }
    1.21 -          Some((id, chunk_name, range))
    1.22 +          Some((id, chunk_name))
    1.23          case _ => None
    1.24        }
    1.25    }
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 14:15:58 2014 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 15:31:24 2014 +0200
     2.3 @@ -163,7 +163,7 @@
     2.4        val kind =
     2.5          if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
     2.6            val name = span.head.source
     2.7 -          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length))
     2.8 +          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
     2.9            Command_Span.Command_Span(name, pos)
    2.10          }
    2.11          else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
     3.1 --- a/src/Pure/PIDE/command.scala	Tue Aug 12 14:15:58 2014 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 12 15:31:24 2014 +0200
     3.3 @@ -189,8 +189,7 @@
     3.4                def bad(): Unit = Output.warning("Ignored report message: " + msg)
     3.5  
     3.6                msg match {
     3.7 -                case XML.Elem(
     3.8 -                    Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
     3.9 +                case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) =>
    3.10  
    3.11                    val target =
    3.12                      if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
    3.13 @@ -198,8 +197,8 @@
    3.14                      else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
    3.15                      else None
    3.16  
    3.17 -                  target match {
    3.18 -                    case Some((target_name, target_chunk)) =>
    3.19 +                  (target, atts) match {
    3.20 +                    case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
    3.21                        target_chunk.incorporate(symbol_range) match {
    3.22                          case Some(range) =>
    3.23                            val props = Position.purge(atts)
    3.24 @@ -207,7 +206,7 @@
    3.25                            state.add_markup(false, target_name, info)
    3.26                          case None => bad(); state
    3.27                        }
    3.28 -                    case None =>
    3.29 +                    case _ =>
    3.30                        // silently ignore excessive reports
    3.31                        state
    3.32                    }
    3.33 @@ -232,7 +231,8 @@
    3.34                if (Protocol.is_inlined(message)) {
    3.35                  for {
    3.36                    (chunk_name, chunk) <- command.chunks.iterator
    3.37 -                  range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
    3.38 +                  range <- Protocol.message_positions(
    3.39 +                    self_id, command.position, chunk_name, chunk, message)
    3.40                  } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
    3.41                }
    3.42                st
     4.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 12 14:15:58 2014 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 12 15:31:24 2014 +0200
     4.3 @@ -312,17 +312,21 @@
     4.4  
     4.5    def message_positions(
     4.6      self_id: Document_ID.Generic => Boolean,
     4.7 +    command_position: Position.T,
     4.8      chunk_name: Symbol.Text_Chunk.Name,
     4.9      chunk: Symbol.Text_Chunk,
    4.10      message: XML.Elem): Set[Text.Range] =
    4.11    {
    4.12      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    4.13        props match {
    4.14 -        case Position.Reported(id, name, symbol_range)
    4.15 -        if self_id(id) && name == chunk_name =>
    4.16 -          chunk.incorporate(symbol_range) match {
    4.17 -            case Some(range) => set + range
    4.18 -            case _ => set
    4.19 +        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
    4.20 +          Position.Range.unapply(props) orElse Position.Range.unapply(command_position) match {
    4.21 +            case Some(symbol_range) =>
    4.22 +              chunk.incorporate(symbol_range) match {
    4.23 +                case Some(range) => set + range
    4.24 +                case _ => set
    4.25 +              }
    4.26 +            case None => set
    4.27            }
    4.28          case _ => set
    4.29        }