# HG changeset patch # User wenzelm # Date 1399150063 -7200 # Node ID b2bfcd8cda80f1ea8b3840803afd54bad7850bd0 # Parent b6e266574b2626db184dc64937d482497474490c support for path completion based on file-system content; diff -r b6e266574b26 -r b2bfcd8cda80 NEWS --- 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"). diff -r b6e266574b26 -r b2bfcd8cda80 src/Pure/PIDE/markup.scala --- 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)] = diff -r b6e266574b26 -r b2bfcd8cda80 src/Pure/library.scala --- 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(", ") diff -r b6e266574b26 -r b2bfcd8cda80 src/Tools/jEdit/etc/options --- 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" diff -r b6e266574b26 -r b2bfcd8cda80 src/Tools/jEdit/src/completion_popup.scala --- 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 { diff -r b6e266574b26 -r b2bfcd8cda80 src/Tools/jEdit/src/rendering.scala --- 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 */