support for path completion based on file-system content;
authorwenzelm
Sat May 03 22:47:43 2014 +0200 (2014-05-03 ago)
changeset 56843b2bfcd8cda80
parent 56842 b6e266574b26
child 56844 52e5bf245b2a
support for path completion based on file-system content;
NEWS
src/Pure/PIDE/markup.scala
src/Pure/library.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/NEWS	Sat May 03 20:31:29 2014 +0200
     1.2 +++ b/NEWS	Sat May 03 22:47:43 2014 +0200
     1.3 @@ -89,6 +89,9 @@
     1.4      place-holder), e.g. "`" for text cartouche, or "@{" for
     1.5      antiquotation.
     1.6  
     1.7 +  - Support for path completion within the formal text, based on
     1.8 +    file-system content.
     1.9 +
    1.10    - Improved treatment of completion vs. various forms of jEdit text
    1.11      selection (multiple selections, rectangular selections,
    1.12      rectangular selection as "tall caret").
     2.1 --- a/src/Pure/PIDE/markup.scala	Sat May 03 20:31:29 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sat May 03 22:47:43 2014 +0200
     2.3 @@ -126,6 +126,7 @@
     2.4    {
     2.5      val ML = "ML"
     2.6      val SML = "SML"
     2.7 +    val PATH = "path"
     2.8      val UNKNOWN = "unknown"
     2.9  
    2.10      def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
     3.1 --- a/src/Pure/library.scala	Sat May 03 20:31:29 2014 +0200
     3.2 +++ b/src/Pure/library.scala	Sat May 03 22:47:43 2014 +0200
     3.3 @@ -112,6 +112,11 @@
     3.4    /* quote */
     3.5  
     3.6    def quote(s: String): String = "\"" + s + "\""
     3.7 +
     3.8 +  def try_unquote(s: String): Option[String] =
     3.9 +    if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
    3.10 +    else None
    3.11 +
    3.12    def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
    3.13    def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
    3.14  
     4.1 --- a/src/Tools/jEdit/etc/options	Sat May 03 20:31:29 2014 +0200
     4.2 +++ b/src/Tools/jEdit/etc/options	Sat May 03 22:47:43 2014 +0200
     4.3 @@ -51,6 +51,9 @@
     4.4  public option jedit_completion_immediate : bool = false
     4.5    -- "insert uniquely completed abbreviation immediately into buffer"
     4.6  
     4.7 +public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
     4.8 +  -- "glob patterns to ignore in path completion (separated by colons)"
     4.9 +
    4.10  
    4.11  section "Spell Checker"
    4.12  
     5.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 20:31:29 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 22:47:43 2014 +0200
     5.3 @@ -11,6 +11,8 @@
     5.4  
     5.5  import java.awt.{Color, Font, Point, BorderLayout, Dimension}
     5.6  import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     5.7 +import java.io.{File => JFile}
     5.8 +import java.util.regex.Pattern
     5.9  import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    5.10  import javax.swing.border.LineBorder
    5.11  import javax.swing.text.DefaultCaret
    5.12 @@ -21,6 +23,7 @@
    5.13  import org.gjt.sp.jedit.View
    5.14  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
    5.15  import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
    5.16 +import org.gjt.sp.util.StandardUtilities
    5.17  
    5.18  
    5.19  object Completion_Popup
    5.20 @@ -191,6 +194,52 @@
    5.21      }
    5.22  
    5.23  
    5.24 +    /* path completion */
    5.25 +
    5.26 +    def path_completion(rendering: Rendering): Option[Completion.Result] =
    5.27 +    {
    5.28 +      def complete(text: String): List[(String, String)] =
    5.29 +      {
    5.30 +        try {
    5.31 +          val path = Path.explode(text)
    5.32 +          val (dir, base_name) =
    5.33 +            if (text == "" || text.endsWith("/")) (path, "")
    5.34 +            else (path.dir, path.base.implode)
    5.35 +
    5.36 +          val directory =
    5.37 +            new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
    5.38 +          val files = directory.listFiles
    5.39 +          if (files == null) Nil
    5.40 +          else {
    5.41 +            val ignore =
    5.42 +              Library.space_explode(':', PIDE.options.string("jedit_completion_path_ignore")).
    5.43 +                map(s => Pattern.compile(StandardUtilities.globToRE(s)))
    5.44 +            (for {
    5.45 +              file <- files.iterator
    5.46 +              name = file.getName
    5.47 +              if name.startsWith(base_name) && name != base_name
    5.48 +              if !ignore.exists(pat => pat.matcher(name).matches)
    5.49 +              descr = if (new JFile(directory, name).isDirectory) "(directory)" else "(file)"
    5.50 +            } yield ((dir + Path.basic(name)).implode, descr)).
    5.51 +              take(PIDE.options.int("completion_limit")).toList
    5.52 +          }
    5.53 +        }
    5.54 +        catch { case ERROR(_) => Nil }
    5.55 +      }
    5.56 +
    5.57 +      for {
    5.58 +        r1 <- rendering.language_path(JEdit_Lib.before_caret_range(text_area, rendering))
    5.59 +        s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
    5.60 +        s2 <- Library.try_unquote(s1)
    5.61 +        r2 = Text.Range(r1.start + 1, r1.stop - 1)
    5.62 +        if Path.is_valid(s2)
    5.63 +        paths = complete(s2)
    5.64 +        if !paths.isEmpty
    5.65 +        items = paths.map(p => Completion.Item(r2, s2, "", List(p._1, p._2), p._1, 0, false))
    5.66 +      } yield Completion.Result(r2, s2, false, items)
    5.67 +    }
    5.68 +
    5.69 +
    5.70      /* completion action: text area */
    5.71  
    5.72      private def insert(item: Completion.Item)
    5.73 @@ -336,7 +385,9 @@
    5.74              opt_rendering match {
    5.75                case None => result0
    5.76                case Some(rendering) =>
    5.77 -                Completion.Result.merge(history, result0, spell_checker_completion(rendering))
    5.78 +                Completion.Result.merge(history, result0,
    5.79 +                  Completion.Result.merge(history,
    5.80 +                    spell_checker_completion(rendering), path_completion(rendering)))
    5.81              }
    5.82            }
    5.83            result match {
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat May 03 20:31:29 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat May 03 22:47:43 2014 +0200
     6.3 @@ -136,6 +136,8 @@
     6.4        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
     6.5        Markup.ML_STRING, Markup.ML_COMMENT)
     6.6  
     6.7 +  private val language_elements = Markup.Elements(Markup.LANGUAGE)
     6.8 +
     6.9    private val highlight_elements =
    6.10      Markup.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    6.11        Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    6.12 @@ -283,6 +285,14 @@
    6.13            Some(Completion.Language_Context.inner)
    6.14        }).headOption.map(_.info)
    6.15  
    6.16 +  def language_path(range: Text.Range): Option[Text.Range] =
    6.17 +    snapshot.select(range, Rendering.language_elements, _ =>
    6.18 +      {
    6.19 +        case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) =>
    6.20 +          Some(snapshot.convert(info_range))
    6.21 +        case _ => None
    6.22 +      }).headOption.map(_.info)
    6.23 +
    6.24  
    6.25    /* spell checker */
    6.26