clarified modules;
authorwenzelm
Wed Jun 21 21:55:07 2017 +0200 (2017-06-21)
changeset 66158ad83d4971dfe
parent 66157 cb57fcdbaf70
child 66159 907720561c82
clarified modules;
etc/options
src/Doc/JEdit/JEdit.thy
src/Pure/PIDE/rendering.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/etc/options	Wed Jun 21 21:10:51 2017 +0200
     1.2 +++ b/etc/options	Wed Jun 21 21:55:07 2017 +0200
     1.3 @@ -200,6 +200,9 @@
     1.4  public option completion_limit : int = 40
     1.5    -- "limit for completion within the formal context"
     1.6  
     1.7 +public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
     1.8 +  -- "glob patterns to ignore in file-system path completion (separated by colons)"
     1.9 +
    1.10  
    1.11  section "Spell Checker"
    1.12  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Wed Jun 21 21:10:51 2017 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Wed Jun 21 21:55:07 2017 +0200
     2.3 @@ -1633,7 +1633,7 @@
     2.4    but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>= true\<close> means that
     2.5    abbreviations of Isabelle symbols are handled nonetheless.
     2.6  
     2.7 -  \<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob''
     2.8 +  \<^item> @{system_option_def completion_path_ignore} specifies ``glob''
     2.9    patterns to ignore in file-system path completion (separated by colons),
    2.10    e.g.\ backup files ending with tilde.
    2.11  
     3.1 --- a/src/Pure/PIDE/rendering.scala	Wed Jun 21 21:10:51 2017 +0200
     3.2 +++ b/src/Pure/PIDE/rendering.scala	Wed Jun 21 21:55:07 2017 +0200
     3.3 @@ -8,6 +8,10 @@
     3.4  package isabelle
     3.5  
     3.6  
     3.7 +import java.io.{File => JFile}
     3.8 +import java.nio.file.FileSystems
     3.9 +
    3.10 +
    3.11  object Rendering
    3.12  {
    3.13    /* color */
    3.14 @@ -268,6 +272,17 @@
    3.15            Some(Completion.Language_Context.inner)
    3.16        }).headOption.map(_.info)
    3.17  
    3.18 +  def citation(range: Text.Range): Option[Text.Info[String]] =
    3.19 +    snapshot.select(range, Rendering.citation_elements, _ =>
    3.20 +      {
    3.21 +        case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
    3.22 +          Some(Text.Info(snapshot.convert(info_range), name))
    3.23 +        case _ => None
    3.24 +      }).headOption.map(_.info)
    3.25 +
    3.26 +
    3.27 +  /* file-system path completion */
    3.28 +
    3.29    def language_path(range: Text.Range): Option[Text.Range] =
    3.30      snapshot.select(range, Rendering.language_elements, _ =>
    3.31        {
    3.32 @@ -276,13 +291,59 @@
    3.33          case _ => None
    3.34        }).headOption.map(_.info)
    3.35  
    3.36 -  def citation(range: Text.Range): Option[Text.Info[String]] =
    3.37 -    snapshot.select(range, Rendering.citation_elements, _ =>
    3.38 -      {
    3.39 -        case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
    3.40 -          Some(Text.Info(snapshot.convert(info_range), name))
    3.41 -        case _ => None
    3.42 -      }).headOption.map(_.info)
    3.43 +  def path_completion(caret: Text.Offset): Option[Completion.Result] =
    3.44 +  {
    3.45 +    def complete(text: String): List[(String, List[String])] =
    3.46 +    {
    3.47 +      try {
    3.48 +        val path = Path.explode(text)
    3.49 +        val (dir, base_name) =
    3.50 +          if (text == "" || text.endsWith("/")) (path, "")
    3.51 +          else (path.dir, path.base_name)
    3.52 +
    3.53 +        val directory = new JFile(session.resources.append(snapshot.node_name, dir))
    3.54 +        val files = directory.listFiles
    3.55 +        if (files == null) Nil
    3.56 +        else {
    3.57 +          val ignore =
    3.58 +            Library.space_explode(':', options.string("completion_path_ignore")).
    3.59 +              map(s => FileSystems.getDefault.getPathMatcher("glob:" + s))
    3.60 +          (for {
    3.61 +            file <- files.iterator
    3.62 +
    3.63 +            name = file.getName
    3.64 +            if name.startsWith(base_name)
    3.65 +            path_name = new JFile(name).toPath
    3.66 +            if !ignore.exists(matcher => matcher.matches(path_name))
    3.67 +
    3.68 +            text1 = (dir + Path.basic(name)).implode_short
    3.69 +            if text != text1
    3.70 +
    3.71 +            is_dir = new JFile(directory, name).isDirectory
    3.72 +            replacement = text1 + (if (is_dir) "/" else "")
    3.73 +            descr = List(text1, if (is_dir) "(directory)" else "(file)")
    3.74 +          } yield (replacement, descr)).take(options.int("completion_limit")).toList
    3.75 +        }
    3.76 +      }
    3.77 +      catch { case ERROR(_) => Nil }
    3.78 +    }
    3.79 +
    3.80 +    def is_wrapped(s: String): Boolean =
    3.81 +      s.startsWith("\"") && s.endsWith("\"") ||
    3.82 +      s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
    3.83 +
    3.84 +    for {
    3.85 +      r1 <- language_path(before_caret_range(caret))
    3.86 +      s1 <- model.try_get_text(r1)
    3.87 +      if is_wrapped(s1)
    3.88 +      r2 = Text.Range(r1.start + 1, r1.stop - 1)
    3.89 +      s2 = s1.substring(1, s1.length - 1)
    3.90 +      if Path.is_valid(s2)
    3.91 +      paths = complete(s2)
    3.92 +      if paths.nonEmpty
    3.93 +      items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
    3.94 +    } yield Completion.Result(r2, s2, false, items)
    3.95 +  }
    3.96  
    3.97  
    3.98    /* spell checker */
     4.1 --- a/src/Tools/jEdit/etc/options	Wed Jun 21 21:10:51 2017 +0200
     4.2 +++ b/src/Tools/jEdit/etc/options	Wed Jun 21 21:55:07 2017 +0200
     4.3 @@ -69,9 +69,6 @@
     4.4  public option jedit_completion_immediate : bool = true
     4.5    -- "insert uniquely completed abbreviation immediately into buffer"
     4.6  
     4.7 -public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
     4.8 -  -- "glob patterns to ignore in file-system path completion (separated by colons)"
     4.9 -
    4.10  
    4.11  section "Rendering of Document Content"
    4.12  
     5.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 21:10:51 2017 +0200
     5.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 21:55:07 2017 +0200
     5.3 @@ -12,7 +12,6 @@
     5.4  import java.awt.{Color, Font, Point, BorderLayout, Dimension}
     5.5  import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     5.6  import java.io.{File => JFile}
     5.7 -import java.util.regex.Pattern
     5.8  import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
     5.9  import javax.swing.border.LineBorder
    5.10  import javax.swing.text.DefaultCaret
    5.11 @@ -132,7 +131,7 @@
    5.12                  val range0 =
    5.13                    Completion.Result.merge(Completion.History.empty,
    5.14                      syntax_completion(Completion.History.empty, true, Some(rendering)),
    5.15 -                    path_completion(rendering),
    5.16 +                    rendering.path_completion(caret),
    5.17                      Document_Model.bibtex_completion(Completion.History.empty, rendering, caret))
    5.18                    .map(_.range)
    5.19                  rendering.semantic_completion(range0, range) match {
    5.20 @@ -183,62 +182,6 @@
    5.21      }
    5.22  
    5.23  
    5.24 -    /* path completion */
    5.25 -
    5.26 -    def path_completion(rendering: JEdit_Rendering): Option[Completion.Result] =
    5.27 -    {
    5.28 -      def complete(text: String): List[(String, List[String])] =
    5.29 -      {
    5.30 -        try {
    5.31 -          val path = Path.explode(text)
    5.32 -          val (dir, base_name) =
    5.33 -            if (text == "" || text.endsWith("/")) (path, "")
    5.34 -            else (path.dir, path.base_name)
    5.35 -
    5.36 -          val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
    5.37 -          val files = directory.listFiles
    5.38 -          if (files == null) Nil
    5.39 -          else {
    5.40 -            val ignore =
    5.41 -              Library.space_explode(':', PIDE.options.string("jedit_completion_path_ignore")).
    5.42 -                map(s => Pattern.compile(StandardUtilities.globToRE(s)))
    5.43 -            (for {
    5.44 -              file <- files.iterator
    5.45 -
    5.46 -              name = file.getName
    5.47 -              if name.startsWith(base_name)
    5.48 -              if !ignore.exists(pat => pat.matcher(name).matches)
    5.49 -
    5.50 -              text1 = (dir + Path.basic(name)).implode_short
    5.51 -              if text != text1
    5.52 -
    5.53 -              is_dir = new JFile(directory, name).isDirectory
    5.54 -              replacement = text1 + (if (is_dir) "/" else "")
    5.55 -              descr = List(text1, if (is_dir) "(directory)" else "(file)")
    5.56 -            } yield (replacement, descr)).take(PIDE.options.int("completion_limit")).toList
    5.57 -          }
    5.58 -        }
    5.59 -        catch { case ERROR(_) => Nil }
    5.60 -      }
    5.61 -
    5.62 -      def is_wrapped(s: String): Boolean =
    5.63 -        s.startsWith("\"") && s.endsWith("\"") ||
    5.64 -        s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
    5.65 -
    5.66 -      for {
    5.67 -        r1 <- rendering.language_path(rendering.before_caret_range(text_area.getCaretPosition))
    5.68 -        s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
    5.69 -        if is_wrapped(s1)
    5.70 -        r2 = Text.Range(r1.start + 1, r1.stop - 1)
    5.71 -        s2 = s1.substring(1, s1.length - 1)
    5.72 -        if Path.is_valid(s2)
    5.73 -        paths = complete(s2)
    5.74 -        if paths.nonEmpty
    5.75 -        items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
    5.76 -      } yield Completion.Result(r2, s2, false, items)
    5.77 -    }
    5.78 -
    5.79 -
    5.80      /* completion action: text area */
    5.81  
    5.82      private def insert(item: Completion.Item)
    5.83 @@ -374,7 +317,7 @@
    5.84                  Completion.Result.merge(history,
    5.85                    result1,
    5.86                    JEdit_Spell_Checker.completion(rendering, explicit, caret),
    5.87 -                  path_completion(rendering),
    5.88 +                  rendering.path_completion(caret),
    5.89                    Document_Model.bibtex_completion(history, rendering, caret))
    5.90              }
    5.91            }