# HG changeset patch
# User wenzelm
# Date 1607354679 -3600
# Node ID 6aae62f55c2b5cb5cc03d4d416d04f3874f3c9ad
# Parent  fd8d82c4433b5a202b6d1d7bf7596ce64a032c82
clarified markup: support more completion, e.g. within ROOTS;

diff -r fd8d82c4433b -r 6aae62f55c2b src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Dec 07 16:09:06 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Dec 07 16:24:39 2020 +0100
@@ -194,6 +194,15 @@
           }
         case _ => None
       }
+
+    object Path
+    {
+      def unapply(markup: Markup): Option[Boolean] =
+        markup match {
+          case Language(PATH, _, _, delimited) => Some(delimited)
+          case _ => None
+        }
+    }
   }
 
 
diff -r fd8d82c4433b -r 6aae62f55c2b src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Dec 07 16:09:06 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Dec 07 16:24:39 2020 +0100
@@ -307,13 +307,13 @@
 
   /* file-system path completion */
 
-  def language_path(range: Text.Range): Option[Text.Range] =
+  def language_path(range: Text.Range): Option[Text.Info[Boolean]] =
     snapshot.select(range, Rendering.language_elements, _ =>
       {
-        case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) =>
-          Some(snapshot.convert(info_range))
+        case Text.Info(info_range, XML.Elem(Markup.Language.Path(delimited), _)) =>
+          Some((delimited, snapshot.convert(info_range)))
         case _ => None
-      }).headOption.map(_.info)
+      }).headOption.map({ case Text.Info(_, (delimited, range)) => Text.Info(range, delimited) })
 
   def path_completion(caret: Text.Offset): Option[Completion.Result] =
   {
@@ -357,11 +357,14 @@
       s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
 
     for {
-      r1 <- language_path(before_caret_range(caret))
+      Text.Info(r1, delimited) <- language_path(before_caret_range(caret))
       s1 <- model.get_text(r1)
-      if is_wrapped(s1)
-      r2 = Text.Range(r1.start + 1, r1.stop - 1)
-      s2 = s1.substring(1, s1.length - 1)
+      (r2, s2) <-
+        if (is_wrapped(s1)) {
+          Some((Text.Range(r1.start + 1, r1.stop - 1), s1.substring(1, s1.length - 1)))
+        }
+        else if (delimited) Some((r1, s1))
+        else None
       if Path.is_valid(s2)
       paths = complete(s2)
       if paths.nonEmpty
diff -r fd8d82c4433b -r 6aae62f55c2b src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Mon Dec 07 16:09:06 2020 +0100
+++ b/src/Pure/Tools/update.scala	Mon Dec 07 16:24:39 2020 +0100
@@ -28,7 +28,7 @@
       xml flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
           if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
-        case XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), body)
+        case XML.Elem(Markup.Language.Path(_), body)
         if path_cartouches =>
           Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
             case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))