--- a/NEWS Sat May 03 20:31:29 2014 +0200
+++ b/NEWS Sat May 03 22:47:43 2014 +0200
@@ -89,6 +89,9 @@
place-holder), e.g. "`" for text cartouche, or "@{" for
antiquotation.
+ - Support for path completion within the formal text, based on
+ file-system content.
+
- Improved treatment of completion vs. various forms of jEdit text
selection (multiple selections, rectangular selections,
rectangular selection as "tall caret").
--- a/src/Pure/PIDE/markup.scala Sat May 03 20:31:29 2014 +0200
+++ b/src/Pure/PIDE/markup.scala Sat May 03 22:47:43 2014 +0200
@@ -126,6 +126,7 @@
{
val ML = "ML"
val SML = "SML"
+ val PATH = "path"
val UNKNOWN = "unknown"
def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
--- a/src/Pure/library.scala Sat May 03 20:31:29 2014 +0200
+++ b/src/Pure/library.scala Sat May 03 22:47:43 2014 +0200
@@ -112,6 +112,11 @@
/* quote */
def quote(s: String): String = "\"" + s + "\""
+
+ def try_unquote(s: String): Option[String] =
+ if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
+ else None
+
def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
--- a/src/Tools/jEdit/etc/options Sat May 03 20:31:29 2014 +0200
+++ b/src/Tools/jEdit/etc/options Sat May 03 22:47:43 2014 +0200
@@ -51,6 +51,9 @@
public option jedit_completion_immediate : bool = false
-- "insert uniquely completed abbreviation immediately into buffer"
+public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
+ -- "glob patterns to ignore in path completion (separated by colons)"
+
section "Spell Checker"
--- a/src/Tools/jEdit/src/completion_popup.scala Sat May 03 20:31:29 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat May 03 22:47:43 2014 +0200
@@ -11,6 +11,8 @@
import java.awt.{Color, Font, Point, BorderLayout, Dimension}
import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
+import java.io.{File => JFile}
+import java.util.regex.Pattern
import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
import javax.swing.border.LineBorder
import javax.swing.text.DefaultCaret
@@ -21,6 +23,7 @@
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
+import org.gjt.sp.util.StandardUtilities
object Completion_Popup
@@ -191,6 +194,52 @@
}
+ /* path completion */
+
+ def path_completion(rendering: Rendering): Option[Completion.Result] =
+ {
+ def complete(text: String): List[(String, String)] =
+ {
+ try {
+ val path = Path.explode(text)
+ val (dir, base_name) =
+ if (text == "" || text.endsWith("/")) (path, "")
+ else (path.dir, path.base.implode)
+
+ val directory =
+ new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
+ val files = directory.listFiles
+ if (files == null) Nil
+ else {
+ val ignore =
+ Library.space_explode(':', PIDE.options.string("jedit_completion_path_ignore")).
+ map(s => Pattern.compile(StandardUtilities.globToRE(s)))
+ (for {
+ file <- files.iterator
+ name = file.getName
+ if name.startsWith(base_name) && name != 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
+ }
+ }
+ catch { case ERROR(_) => Nil }
+ }
+
+ for {
+ r1 <- rendering.language_path(JEdit_Lib.before_caret_range(text_area, rendering))
+ s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
+ s2 <- Library.try_unquote(s1)
+ r2 = Text.Range(r1.start + 1, r1.stop - 1)
+ 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))
+ } yield Completion.Result(r2, s2, false, items)
+ }
+
+
/* completion action: text area */
private def insert(item: Completion.Item)
@@ -336,7 +385,9 @@
opt_rendering match {
case None => result0
case Some(rendering) =>
- Completion.Result.merge(history, result0, spell_checker_completion(rendering))
+ Completion.Result.merge(history, result0,
+ Completion.Result.merge(history,
+ spell_checker_completion(rendering), path_completion(rendering)))
}
}
result match {
--- a/src/Tools/jEdit/src/rendering.scala Sat May 03 20:31:29 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Sat May 03 22:47:43 2014 +0200
@@ -136,6 +136,8 @@
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
+ private val language_elements = Markup.Elements(Markup.LANGUAGE)
+
private val highlight_elements =
Markup.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
@@ -283,6 +285,14 @@
Some(Completion.Language_Context.inner)
}).headOption.map(_.info)
+ def language_path(range: Text.Range): Option[Text.Range] =
+ snapshot.select(range, Rendering.language_elements, _ =>
+ {
+ case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) =>
+ Some(snapshot.convert(info_range))
+ case _ => None
+ }).headOption.map(_.info)
+
/* spell checker */