Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Wed, 21 Jun 2017 14:30:20 +0200
changeset 66151 26eecd42cbc5
parent 66150 c2e19b9e1398
child 66152 18e1aba549f6
tuned signature;
src/Pure/General/completion.scala file | annotate | diff | comparison | revisions
src/Tools/VSCode/src/vscode_rendering.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/completion_popup.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/completion.scala	Wed Jun 21 14:06:16 2017 +0200
+++ b/src/Pure/General/completion.scala	Wed Jun 21 14:30:20 2017 +0200
@@ -42,6 +42,8 @@
             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/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 21 14:06:16 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 21 14:30:20 2017 +0200
@@ -99,8 +99,9 @@
         if (no_completion) Nil
         else {
           val results =
-            Completion.Result.merge(history,
-              Completion.Result.merge(history, semantic_completion, syntax_completion),
+            Completion.Result.merges(history,
+              semantic_completion,
+              syntax_completion,
               VSCode_Spell_Checker.completion(rendering, caret))
           val items =
             results match {
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 14:06:16 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 14:30:20 2017 +0200
@@ -130,11 +130,10 @@
             rendering.before_caret_range(caret).try_restrict(line_range) match {
               case Some(range) if !range.is_singularity =>
                 val range0 =
-                  Completion.Result.merge(Completion.History.empty,
+                  Completion.Result.merges(Completion.History.empty,
                     syntax_completion(Completion.History.empty, true, Some(rendering)),
-                    Completion.Result.merge(Completion.History.empty,
-                      path_completion(rendering),
-                      JEdit_Bibtex.completion(Completion.History.empty, rendering, caret)))
+                    path_completion(rendering),
+                    JEdit_Bibtex.completion(Completion.History.empty, rendering, caret))
                   .map(_.range)
                 rendering.semantic_completion(range0, range) match {
                   case None => range0
@@ -372,12 +371,11 @@
             opt_rendering match {
               case None => result1
               case Some(rendering) =>
-                Completion.Result.merge(history, result1,
-                  Completion.Result.merge(history,
-                    JEdit_Spell_Checker.completion(rendering, explicit, caret),
-                    Completion.Result.merge(history,
-                      path_completion(rendering),
-                      JEdit_Bibtex.completion(history, rendering, caret))))
+                Completion.Result.merges(history,
+                  result1,
+                  JEdit_Spell_Checker.completion(rendering, explicit, caret),
+                  path_completion(rendering),
+                  JEdit_Bibtex.completion(history, rendering, caret))
             }
           }
           result match {
isabelle