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