report (but ignore) markup within auxiliary files;
authorwenzelm
Tue Feb 11 15:05:13 2014 +0100 (2014-02-11)
changeset 554294a50f9e70dc1
parent 55391 eae296b5ef33
child 55430 8eb6c740ec1a
report (but ignore) markup within auxiliary files;
src/Pure/General/position.scala
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/General/position.scala	Tue Feb 11 12:08:44 2014 +0100
     1.2 +++ b/src/Pure/General/position.scala	Tue Feb 11 15:05:13 2014 +0100
     1.3 @@ -75,11 +75,12 @@
     1.4        }
     1.5    }
     1.6  
     1.7 -  object Id_Range
     1.8 +  object Reported
     1.9    {
    1.10 -    def unapply(pos: T): Option[(Long, Text.Range)] =
    1.11 +    def unapply(pos: T): Option[(Long, String, Text.Range)] =
    1.12        (pos, pos) match {
    1.13 -        case (Id(id), Range(range)) => Some((id, range))
    1.14 +        case (Id(id), Range(range)) =>
    1.15 +          Some((id, File.unapply(pos).getOrElse(""), range))
    1.16          case _ => None
    1.17        }
    1.18    }
     2.1 --- a/src/Pure/PIDE/command.ML	Tue Feb 11 12:08:44 2014 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Tue Feb 11 15:05:13 2014 +0100
     2.3 @@ -102,8 +102,14 @@
     2.4            fun make_file src_path (Exn.Res (_, NONE)) =
     2.5                  Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
     2.6              | make_file src_path (Exn.Res (file, SOME text)) =
     2.7 -                let val _ = Position.report pos (Markup.path file)
     2.8 -                in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
     2.9 +                let
    2.10 +                  val _ = Position.report pos (Markup.path file);
    2.11 +                  val file_pos =
    2.12 +                    Position.file file (*sic!*) |>
    2.13 +                    (case Position.get_id (Position.thread_data ()) of
    2.14 +                      NONE => I
    2.15 +                    | SOME exec_id => Position.put_id exec_id);
    2.16 +                in Exn.Res {src_path = src_path, text = text, pos = file_pos} end
    2.17              | make_file _ (Exn.Exn e) = Exn.Exn e;
    2.18  
    2.19            val src_paths = Keyword.command_files cmd path;
     3.1 --- a/src/Pure/PIDE/command.scala	Tue Feb 11 12:08:44 2014 +0100
     3.2 +++ b/src/Pure/PIDE/command.scala	Tue Feb 11 15:05:13 2014 +0100
     3.3 @@ -94,8 +94,8 @@
     3.4          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
     3.5            (this /: msgs)((state, msg) =>
     3.6              msg match {
     3.7 -              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
     3.8 -              if (id == command.id || id == alt_id) &&
     3.9 +              case XML.Elem(Markup(name, atts @ Position.Reported(id, file, raw_range)), args)
    3.10 +              if (id == command.id || id == alt_id) && file == "" &&
    3.11                    command.range.contains(command.decode(raw_range)) =>
    3.12                  val range = command.decode(raw_range)
    3.13                  val props = Position.purge(atts)
     4.1 --- a/src/Pure/PIDE/protocol.scala	Tue Feb 11 12:08:44 2014 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Feb 11 15:05:13 2014 +0100
     4.3 @@ -285,11 +285,11 @@
     4.4  
     4.5      def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
     4.6        tree match {
     4.7 -        case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body)
     4.8 -        if include_pos(name) && id == command.id => elem_positions(range, set, body)
     4.9 +        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file, range)), _, body)
    4.10 +        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
    4.11  
    4.12 -        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    4.13 -        if include_pos(name) && id == command.id => elem_positions(range, set, body)
    4.14 +        case XML.Elem(Markup(name, Position.Reported(id, file, range)), body)
    4.15 +        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
    4.16  
    4.17          case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)
    4.18