# HG changeset patch
# User wenzelm
# Date 1392728708 -3600
# Node ID a645277885cf0dd59f5a9b46a2b1ea5c2875d527
# Parent  384bfd19ee615e99181aaa2153d2f0ec8a38f1e7
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;

diff -r 384bfd19ee61 -r a645277885cf src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Feb 17 22:39:20 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Feb 18 14:05:08 2014 +0100
@@ -108,19 +108,17 @@
                 if id == command.id || id == alt_id =>
                   command.chunks.get(file_name) match {
                     case Some(chunk) =>
-                      val range = chunk.decode(raw_range)
-                      if (chunk.range.contains(range)) {
-                        val props = Position.purge(atts)
-                        val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
-                        state.add_markup(file_name, info)
+                      chunk.decode(raw_range).try_restrict(chunk.range) match {
+                        case Some(range) =>
+                          if (!range.is_singularity) {
+                            val props = Position.purge(atts)
+                            state.add_markup(file_name,
+                              Text.Info(range, XML.Elem(Markup(name, props), args)))
+                          }
+                          else state
+                        case None => bad(); state
                       }
-                      else {
-                        bad()
-                        state
-                      }
-                    case None =>
-                      bad()
-                      state
+                    case None => bad(); state
                   }
 
                 case XML.Elem(Markup(name, atts), args)
@@ -130,9 +128,7 @@
                   val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
                   state.add_markup("", info)
 
-                case _ =>
-                  // FIXME bad()
-                  state
+                case _ => /* FIXME bad(); */ state
               }
             })
         case XML.Elem(Markup(name, props), body) =>
diff -r 384bfd19ee61 -r a645277885cf src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Feb 17 22:39:20 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Feb 18 14:05:08 2014 +0100
@@ -282,10 +282,12 @@
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
-        case Position.Reported(id, file_name, range)
+        case Position.Reported(id, file_name, raw_range)
         if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
-          val range1 = chunk.decode(range).restrict(chunk.range)
-          if (range1.is_singularity) set else set + range1
+          chunk.decode(raw_range).try_restrict(chunk.range) match {
+            case Some(range) if !range.is_singularity => set + range
+            case _ => set
+          }
         case _ => set
       }