# HG changeset patch
# User wenzelm
# Date 1497037411 -7200
# Node ID fb0eea226a4d86f21c903cdab1bc72939d0c0e62
# Parent  cd8d0ad5ac1990938f161b86fd69791a3f845594
more uniform syntax_completion + semantic_completion;

diff -r cd8d0ad5ac19 -r fb0eea226a4d src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Fri Jun 09 21:43:31 2017 +0200
@@ -206,11 +206,11 @@
 
   /* completion */
 
-  def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
+  def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range)
       : Option[Text.Info[Completion.Semantic]] =
     if (snapshot.is_outdated) None
     else {
-      snapshot.select(range, Rendering.semantic_completion_elements, _ =>
+      snapshot.select(caret_range, Rendering.semantic_completion_elements, _ =>
         {
           case Completion.Semantic.Info(info) =>
             completed_range match {
@@ -221,6 +221,24 @@
         }).headOption.map(_.info)
     }
 
+  def semantic_completion_result(
+    history: Completion.History,
+    decode: Boolean,
+    completed_range: Option[Text.Range],
+    caret_range: Text.Range,
+    try_get_text: Text.Range => Option[String]): (Boolean, Option[Completion.Result]) =
+  {
+    semantic_completion(completed_range, caret_range) match {
+      case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
+      case Some(Text.Info(range, names: Completion.Names)) =>
+        try_get_text(range) match {
+          case Some(original) => (false, names.complete(range, history, decode, original))
+          case None => (false, None)
+        }
+      case None => (false, None)
+    }
+  }
+
   def language_context(range: Text.Range): Option[Completion.Language_Context] =
     snapshot.select(range, Rendering.language_context_elements, _ =>
       {
diff -r cd8d0ad5ac19 -r fb0eea226a4d src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Jun 09 21:43:31 2017 +0200
@@ -191,4 +191,12 @@
   def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
     new VSCode_Rendering(this, snapshot)
   def rendering(): VSCode_Rendering = rendering(snapshot())
+
+
+  /* syntax */
+
+  lazy private val syntax0 = Outer_Syntax.init()
+
+  def syntax(): Outer_Syntax =
+    if (is_theory) session.recent_syntax(node_name) else syntax0
 }
diff -r cd8d0ad5ac19 -r fb0eea226a4d src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Fri Jun 09 21:43:31 2017 +0200
@@ -325,7 +325,7 @@
   {
     val result =
       (for ((rendering, offset) <- rendering_offset(node_pos))
-        yield rendering.completion(Text.Range(offset - 1, offset))) getOrElse Nil
+        yield rendering.completion(node_pos.pos, offset)) getOrElse Nil
     channel.write(Protocol.Completion.reply(id, result))
   }
 
diff -r cd8d0ad5ac19 -r fb0eea226a4d src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Jun 09 21:43:31 2017 +0200
@@ -68,28 +68,56 @@
 class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot)
   extends Rendering(snapshot, model.resources.options, model.session)
 {
+  rendering =>
+
+
   /* completion */
 
-  def completion(range: Text.Range): List[Protocol.CompletionItem] =
-    semantic_completion(None, range) match {
-      case Some(Text.Info(complete_range, names: Completion.Names)) =>
-        model.content.try_get_text(complete_range) match {
-          case Some(original) =>
-            names.complete(complete_range, Completion.History.empty,
-                model.resources.unicode_symbols, original) match {
-              case Some(result) =>
-                result.items.map(item =>
-                  Protocol.CompletionItem(
-                    label = item.replacement,
-                    detail = Some(item.description.mkString(" ")),
-                    range = Some(model.content.doc.range(item.range))))
-              case None => Nil
-            }
-          case None => Nil
-        }
-      case _ => Nil
+  def before_caret_range(caret: Text.Offset): Text.Range =
+  {
+    val former_caret = snapshot.revert(caret)
+    snapshot.convert(Text.Range(former_caret - 1, former_caret))
+  }
+
+  def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] =
+  {
+    val caret_range = before_caret_range(caret)
+
+    val history = Completion.History.empty
+    val doc = model.content.doc
+
+    val syntax_completion =
+    {
+      val syntax = model.syntax()
+      val context = language_context(caret_range) getOrElse syntax.language_context
+
+      val line = caret_pos.line
+      doc.offset(Line.Position(line)) match {
+        case Some(line_start) =>
+          syntax.completion.complete(history, false, true,
+            line_start, doc.lines(line).text, caret - line_start, context)
+        case None => None
+      }
     }
 
+    val (no_completion, semantic_completion) =
+      rendering.semantic_completion_result(
+        history, false, syntax_completion.map(_.range), caret_range, doc.try_get_text(_))
+
+    if (no_completion) Nil
+    else {
+      Completion.Result.merge(history, semantic_completion, syntax_completion) match {
+        case None => Nil
+        case Some(result) =>
+          result.items.map(item =>
+            Protocol.CompletionItem(
+              label = item.replacement,
+              detail = Some(item.description.mkString(" ")),
+              range = Some(doc.range(item.range))))
+      }
+    }
+  }
+
 
   /* diagnostics */
 
diff -r cd8d0ad5ac19 -r fb0eea226a4d src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Jun 09 21:43:31 2017 +0200
@@ -164,8 +164,8 @@
             (for {
               rendering <- opt_rendering
               if PIDE.options.bool("jedit_completion_context")
-              range = JEdit_Lib.before_caret_range(text_area, rendering)
-              context <- rendering.language_context(range)
+              caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
+              context <- rendering.language_context(caret_range)
             } yield context) getOrElse syntax.language_context
 
           val caret = text_area.getCaretPosition
@@ -355,16 +355,9 @@
         {
           opt_rendering match {
             case Some(rendering) =>
-              val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
-              rendering.semantic_completion(result0.map(_.range), caret_range) match {
-                case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
-                case Some(Text.Info(range, names: Completion.Names)) =>
-                  JEdit_Lib.try_get_text(buffer, range) match {
-                    case Some(original) => (false, names.complete(range, history, decode, original))
-                    case None => (false, None)
-                  }
-                case None => (false, None)
-              }
+              rendering.semantic_completion_result(history, decode, result0.map(_.range),
+                JEdit_Lib.before_caret_range(text_area, rendering),
+                JEdit_Lib.try_get_text(buffer, _))
             case None => (false, None)
           }
         }