src/Tools/jEdit/src/completion_popup.scala
changeset 56843 b2bfcd8cda80
parent 56842 b6e266574b26
child 56844 52e5bf245b2a
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 20:31:29 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 22:47:43 2014 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4  
     1.5  import java.awt.{Color, Font, Point, BorderLayout, Dimension}
     1.6  import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     1.7 +import java.io.{File => JFile}
     1.8 +import java.util.regex.Pattern
     1.9  import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    1.10  import javax.swing.border.LineBorder
    1.11  import javax.swing.text.DefaultCaret
    1.12 @@ -21,6 +23,7 @@
    1.13  import org.gjt.sp.jedit.View
    1.14  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
    1.15  import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
    1.16 +import org.gjt.sp.util.StandardUtilities
    1.17  
    1.18  
    1.19  object Completion_Popup
    1.20 @@ -191,6 +194,52 @@
    1.21      }
    1.22  
    1.23  
    1.24 +    /* path completion */
    1.25 +
    1.26 +    def path_completion(rendering: Rendering): Option[Completion.Result] =
    1.27 +    {
    1.28 +      def complete(text: String): List[(String, String)] =
    1.29 +      {
    1.30 +        try {
    1.31 +          val path = Path.explode(text)
    1.32 +          val (dir, base_name) =
    1.33 +            if (text == "" || text.endsWith("/")) (path, "")
    1.34 +            else (path.dir, path.base.implode)
    1.35 +
    1.36 +          val directory =
    1.37 +            new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
    1.38 +          val files = directory.listFiles
    1.39 +          if (files == null) Nil
    1.40 +          else {
    1.41 +            val ignore =
    1.42 +              Library.space_explode(':', PIDE.options.string("jedit_completion_path_ignore")).
    1.43 +                map(s => Pattern.compile(StandardUtilities.globToRE(s)))
    1.44 +            (for {
    1.45 +              file <- files.iterator
    1.46 +              name = file.getName
    1.47 +              if name.startsWith(base_name) && name != base_name
    1.48 +              if !ignore.exists(pat => pat.matcher(name).matches)
    1.49 +              descr = if (new JFile(directory, name).isDirectory) "(directory)" else "(file)"
    1.50 +            } yield ((dir + Path.basic(name)).implode, descr)).
    1.51 +              take(PIDE.options.int("completion_limit")).toList
    1.52 +          }
    1.53 +        }
    1.54 +        catch { case ERROR(_) => Nil }
    1.55 +      }
    1.56 +
    1.57 +      for {
    1.58 +        r1 <- rendering.language_path(JEdit_Lib.before_caret_range(text_area, rendering))
    1.59 +        s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
    1.60 +        s2 <- Library.try_unquote(s1)
    1.61 +        r2 = Text.Range(r1.start + 1, r1.stop - 1)
    1.62 +        if Path.is_valid(s2)
    1.63 +        paths = complete(s2)
    1.64 +        if !paths.isEmpty
    1.65 +        items = paths.map(p => Completion.Item(r2, s2, "", List(p._1, p._2), p._1, 0, false))
    1.66 +      } yield Completion.Result(r2, s2, false, items)
    1.67 +    }
    1.68 +
    1.69 +
    1.70      /* completion action: text area */
    1.71  
    1.72      private def insert(item: Completion.Item)
    1.73 @@ -336,7 +385,9 @@
    1.74              opt_rendering match {
    1.75                case None => result0
    1.76                case Some(rendering) =>
    1.77 -                Completion.Result.merge(history, result0, spell_checker_completion(rendering))
    1.78 +                Completion.Result.merge(history, result0,
    1.79 +                  Completion.Result.merge(history,
    1.80 +                    spell_checker_completion(rendering), path_completion(rendering)))
    1.81              }
    1.82            }
    1.83            result match {