# HG changeset patch # User wenzelm # Date 1498078660 -7200 # Node ID c6e9c7d140ffae7caadf582eceebbe0c74552c32 # Parent f54c32c413a9a6f31dd5e34db97b60f3e12abdaf# Parent 33f75974288788b90a3dfdf02ce15fbd717e57b4 merged diff -r f54c32c413a9 -r c6e9c7d140ff etc/options --- 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" diff -r f54c32c413a9 -r c6e9c7d140ff src/Doc/JEdit/JEdit.thy --- 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>\= true\ 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. diff -r f54c32c413a9 -r c6e9c7d140ff src/Pure/General/completion.scala --- 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( diff -r f54c32c413a9 -r c6e9c7d140ff src/Pure/PIDE/rendering.scala --- 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 */ diff -r f54c32c413a9 -r c6e9c7d140ff src/Tools/VSCode/src/vscode_rendering.scala --- 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 { diff -r f54c32c413a9 -r c6e9c7d140ff src/Tools/jEdit/etc/options --- 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" diff -r f54c32c413a9 -r c6e9c7d140ff src/Tools/jEdit/src/completion_popup.scala --- 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)) } }