--- a/etc/options Wed Jun 21 22:48:55 2017 +0200
+++ b/etc/options Wed Jun 21 22:57:40 2017 +0200
@@ -76,7 +76,7 @@
option parallel_subproofs_threshold : real = 0.01
-- "lower bound of timing estimate for forked nested proofs (seconds)"
-option command_timing_threshold : real = 0.01
+option command_timing_threshold : real = 0.1
-- "default threshold for persistent command timing (seconds)"
@@ -200,6 +200,9 @@
public option completion_limit : int = 40
-- "limit for completion within the formal context"
+public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
+ -- "glob patterns to ignore in file-system path completion (separated by colons)"
+
section "Spell Checker"
--- a/src/Doc/JEdit/JEdit.thy Wed Jun 21 22:48:55 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy Wed Jun 21 22:57:40 2017 +0200
@@ -1633,7 +1633,7 @@
but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>= true\<close> means that
abbreviations of Isabelle symbols are handled nonetheless.
- \<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob''
+ \<^item> @{system_option_def completion_path_ignore} specifies ``glob''
patterns to ignore in file-system path completion (separated by colons),
e.g.\ backup files ending with tilde.
--- a/src/Pure/General/completion.scala Wed Jun 21 22:48:55 2017 +0200
+++ b/src/Pure/General/completion.scala Wed Jun 21 22:57:40 2017 +0200
@@ -31,19 +31,17 @@
object Result
{
def empty(range: Text.Range): Result = Result(range, "", false, Nil)
- def merge(history: History, result1: Option[Result], result2: Option[Result]): Option[Result] =
- (result1, result2) match {
- case (_, None) => result1
- case (None, _) => result2
- case (Some(res1), Some(res2)) =>
+ def merge(history: History, results: Option[Result]*): Option[Result] =
+ ((None: Option[Result]) /: results)({
+ case (result1, None) => result1
+ case (None, result2) => result2
+ case (result1 @ Some(res1), Some(res2)) =>
if (res1.range != res2.range || res1.original != res2.original) result1
else {
val items = (res1.items ::: res2.items).sorted(history.ordering)
Some(Result(res1.range, res1.original, false, items))
}
- }
- def merges(history: History, results: Option[Result]*): Option[Result] =
- ((None: Option[Result]) /: results)(merge(history, _, _))
+ })
}
sealed case class Result(
--- a/src/Pure/PIDE/rendering.scala Wed Jun 21 22:48:55 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Wed Jun 21 22:57:40 2017 +0200
@@ -8,6 +8,10 @@
package isabelle
+import java.io.{File => JFile}
+import java.nio.file.FileSystems
+
+
object Rendering
{
/* color */
@@ -268,6 +272,17 @@
Some(Completion.Language_Context.inner)
}).headOption.map(_.info)
+ def citation(range: Text.Range): Option[Text.Info[String]] =
+ snapshot.select(range, Rendering.citation_elements, _ =>
+ {
+ case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
+ Some(Text.Info(snapshot.convert(info_range), name))
+ case _ => None
+ }).headOption.map(_.info)
+
+
+ /* file-system path completion */
+
def language_path(range: Text.Range): Option[Text.Range] =
snapshot.select(range, Rendering.language_elements, _ =>
{
@@ -276,13 +291,59 @@
case _ => None
}).headOption.map(_.info)
- def citation(range: Text.Range): Option[Text.Info[String]] =
- snapshot.select(range, Rendering.citation_elements, _ =>
- {
- case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
- Some(Text.Info(snapshot.convert(info_range), name))
- case _ => None
- }).headOption.map(_.info)
+ def path_completion(caret: Text.Offset): Option[Completion.Result] =
+ {
+ def complete(text: String): List[(String, List[String])] =
+ {
+ try {
+ val path = Path.explode(text)
+ val (dir, base_name) =
+ if (text == "" || text.endsWith("/")) (path, "")
+ else (path.dir, path.base_name)
+
+ val directory = new JFile(session.resources.append(snapshot.node_name, dir))
+ val files = directory.listFiles
+ if (files == null) Nil
+ else {
+ val ignore =
+ Library.space_explode(':', options.string("completion_path_ignore")).
+ map(s => FileSystems.getDefault.getPathMatcher("glob:" + s))
+ (for {
+ file <- files.iterator
+
+ name = file.getName
+ if name.startsWith(base_name)
+ path_name = new JFile(name).toPath
+ if !ignore.exists(matcher => matcher.matches(path_name))
+
+ text1 = (dir + Path.basic(name)).implode_short
+ if text != text1
+
+ is_dir = new JFile(directory, name).isDirectory
+ replacement = text1 + (if (is_dir) "/" else "")
+ descr = List(text1, if (is_dir) "(directory)" else "(file)")
+ } yield (replacement, descr)).take(options.int("completion_limit")).toList
+ }
+ }
+ catch { case ERROR(_) => Nil }
+ }
+
+ def is_wrapped(s: String): Boolean =
+ s.startsWith("\"") && s.endsWith("\"") ||
+ s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
+
+ for {
+ r1 <- language_path(before_caret_range(caret))
+ s1 <- model.try_get_text(r1)
+ if is_wrapped(s1)
+ r2 = Text.Range(r1.start + 1, r1.stop - 1)
+ s2 = s1.substring(1, s1.length - 1)
+ if Path.is_valid(s2)
+ paths = complete(s2)
+ if paths.nonEmpty
+ items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
+ } yield Completion.Result(r2, s2, false, items)
+ }
/* spell checker */
--- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Jun 21 22:48:55 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Jun 21 22:57:40 2017 +0200
@@ -108,10 +108,11 @@
if (no_completion) Nil
else {
val results =
- Completion.Result.merges(history,
+ Completion.Result.merge(history,
semantic_completion,
syntax_completion,
VSCode_Spell_Checker.completion(rendering, caret),
+ path_completion(caret),
bibtex_completion(history, caret))
val items =
results match {
--- a/src/Tools/jEdit/etc/options Wed Jun 21 22:48:55 2017 +0200
+++ b/src/Tools/jEdit/etc/options Wed Jun 21 22:57:40 2017 +0200
@@ -69,9 +69,6 @@
public option jedit_completion_immediate : bool = true
-- "insert uniquely completed abbreviation immediately into buffer"
-public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
- -- "glob patterns to ignore in file-system path completion (separated by colons)"
-
section "Rendering of Document Content"
--- a/src/Tools/jEdit/src/completion_popup.scala Wed Jun 21 22:48:55 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Wed Jun 21 22:57:40 2017 +0200
@@ -12,7 +12,6 @@
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
@@ -130,9 +129,9 @@
rendering.before_caret_range(caret).try_restrict(line_range) match {
case Some(range) if !range.is_singularity =>
val range0 =
- Completion.Result.merges(Completion.History.empty,
+ Completion.Result.merge(Completion.History.empty,
syntax_completion(Completion.History.empty, true, Some(rendering)),
- path_completion(rendering),
+ rendering.path_completion(caret),
Document_Model.bibtex_completion(Completion.History.empty, rendering, caret))
.map(_.range)
rendering.semantic_completion(range0, range) match {
@@ -183,62 +182,6 @@
}
- /* path completion */
-
- def path_completion(rendering: JEdit_Rendering): Option[Completion.Result] =
- {
- def complete(text: String): List[(String, List[String])] =
- {
- try {
- val path = Path.explode(text)
- val (dir, base_name) =
- if (text == "" || text.endsWith("/")) (path, "")
- else (path.dir, path.base_name)
-
- val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, 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)
- if !ignore.exists(pat => pat.matcher(name).matches)
-
- text1 = (dir + Path.basic(name)).implode_short
- if text != text1
-
- is_dir = new JFile(directory, name).isDirectory
- replacement = text1 + (if (is_dir) "/" else "")
- descr = List(text1, if (is_dir) "(directory)" else "(file)")
- } yield (replacement, descr)).take(PIDE.options.int("completion_limit")).toList
- }
- }
- catch { case ERROR(_) => Nil }
- }
-
- def is_wrapped(s: String): Boolean =
- s.startsWith("\"") && s.endsWith("\"") ||
- s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
-
- for {
- r1 <- rendering.language_path(rendering.before_caret_range(text_area.getCaretPosition))
- s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
- if is_wrapped(s1)
- r2 = Text.Range(r1.start + 1, r1.stop - 1)
- s2 = s1.substring(1, s1.length - 1)
- if Path.is_valid(s2)
- paths = complete(s2)
- if paths.nonEmpty
- items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
- } yield Completion.Result(r2, s2, false, items)
- }
-
-
/* completion action: text area */
private def insert(item: Completion.Item)
@@ -371,10 +314,10 @@
opt_rendering match {
case None => result1
case Some(rendering) =>
- Completion.Result.merges(history,
+ Completion.Result.merge(history,
result1,
JEdit_Spell_Checker.completion(rendering, explicit, caret),
- path_completion(rendering),
+ rendering.path_completion(caret),
Document_Model.bibtex_completion(history, rendering, caret))
}
}