# HG changeset patch
# User wenzelm
# Date 1498074907 -7200
# Node ID ad83d4971dfe8523133b8af1d123f698f482ceb4
# Parent  cb57fcdbaf7013ddc582914552b0eb8e4ff158b0
clarified modules;

diff -r cb57fcdbaf70 -r ad83d4971dfe etc/options
--- a/etc/options	Wed Jun 21 21:10:51 2017 +0200
+++ b/etc/options	Wed Jun 21 21:55:07 2017 +0200
@@ -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 cb57fcdbaf70 -r ad83d4971dfe src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Jun 21 21:10:51 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Jun 21 21:55:07 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.
 
diff -r cb57fcdbaf70 -r ad83d4971dfe src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Jun 21 21:10:51 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Wed Jun 21 21:55:07 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 cb57fcdbaf70 -r ad83d4971dfe src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Jun 21 21:10:51 2017 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Jun 21 21:55:07 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 cb57fcdbaf70 -r ad83d4971dfe src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 21:10:51 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 21:55:07 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
@@ -132,7 +131,7 @@
                 val range0 =
                   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)
@@ -374,7 +317,7 @@
                 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))
             }
           }