# HG changeset patch
# User wenzelm
# Date 1399151700 -7200
# Node ID 52e5bf245b2a2bc7162eeac80228f0158e400fed
# Parent  b2bfcd8cda80f1ea8b3840803afd54bad7850bd0
standardize to implode_short form;
clarified treatment of directories;

diff -r b2bfcd8cda80 -r 52e5bf245b2a src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sat May 03 22:47:43 2014 +0200
+++ b/src/Pure/General/path.scala	Sat May 03 23:15:00 2014 +0200
@@ -50,11 +50,13 @@
   private def norm_elems(elems: List[Elem]): List[Elem] =
     (elems :\ (Nil: List[Elem]))(apply_elem)
 
-  private def implode_elem(elem: Elem): String =
+  private def implode_elem(elem: Elem, short: Boolean): String =
     elem match {
       case Root("") => ""
       case Root(s) => "//" + s
       case Basic(s) => s
+      case Variable("USER_HOME") if short => "~"
+      case Variable("ISABELLE_HOME") if short => "~~"
       case Variable(s) => "$" + s
       case Parent => ".."
     }
@@ -124,12 +126,14 @@
 
   /* implode */
 
-  def implode: String =
+  private def gen_implode(short: Boolean): String =
     elems match {
       case Nil => "."
       case List(Path.Root("")) => "/"
-      case _ => elems.map(Path.implode_elem).reverse.mkString("/")
+      case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/")
     }
+  def implode: String = gen_implode(false)
+  def implode_short: String = gen_implode(true)
 
   override def toString: String = quote(implode)
 
diff -r b2bfcd8cda80 -r 52e5bf245b2a src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 22:47:43 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 23:15:00 2014 +0200
@@ -198,7 +198,7 @@
 
     def path_completion(rendering: Rendering): Option[Completion.Result] =
     {
-      def complete(text: String): List[(String, String)] =
+      def complete(text: String): List[(String, List[String])] =
       {
         try {
           val path = Path.explode(text)
@@ -216,12 +216,18 @@
                 map(s => Pattern.compile(StandardUtilities.globToRE(s)))
             (for {
               file <- files.iterator
+
               name = file.getName
-              if name.startsWith(base_name) && name != base_name
+              if name.startsWith(base_name)
               if !ignore.exists(pat => pat.matcher(name).matches)
-              descr = if (new JFile(directory, name).isDirectory) "(directory)" else "(file)"
-            } yield ((dir + Path.basic(name)).implode, descr)).
-              take(PIDE.options.int("completion_limit")).toList
+
+              text1 = (dir + Path.basic(name)).implode_short
+              if text != text1
+
+              is_dir = new JFile(directory, name).isDirectory
+              replacement = text1 + (if (is_dir) "/" else "")
+              descr = List(text1, if (is_dir) "(directory)" else "(file)")
+            } yield (replacement, descr)).take(PIDE.options.int("completion_limit")).toList
           }
         }
         catch { case ERROR(_) => Nil }
@@ -235,7 +241,7 @@
         if Path.is_valid(s2)
         paths = complete(s2)
         if !paths.isEmpty
-        items = paths.map(p => Completion.Item(r2, s2, "", List(p._1, p._2), p._1, 0, false))
+        items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
       } yield Completion.Result(r2, s2, false, items)
     }