src/Tools/VSCode/src/vscode_rendering.scala
changeset 66054 fb0eea226a4d
parent 65925 4a1b666b6362
child 66055 07175635f78c
equal deleted inserted replaced
66053:cd8d0ad5ac19 66054:fb0eea226a4d
    66 }
    66 }
    67 
    67 
    68 class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot)
    68 class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot)
    69   extends Rendering(snapshot, model.resources.options, model.session)
    69   extends Rendering(snapshot, model.resources.options, model.session)
    70 {
    70 {
       
    71   rendering =>
       
    72 
       
    73 
    71   /* completion */
    74   /* completion */
    72 
    75 
    73   def completion(range: Text.Range): List[Protocol.CompletionItem] =
    76   def before_caret_range(caret: Text.Offset): Text.Range =
    74     semantic_completion(None, range) match {
    77   {
    75       case Some(Text.Info(complete_range, names: Completion.Names)) =>
    78     val former_caret = snapshot.revert(caret)
    76         model.content.try_get_text(complete_range) match {
    79     snapshot.convert(Text.Range(former_caret - 1, former_caret))
    77           case Some(original) =>
    80   }
    78             names.complete(complete_range, Completion.History.empty,
    81 
    79                 model.resources.unicode_symbols, original) match {
    82   def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] =
    80               case Some(result) =>
    83   {
    81                 result.items.map(item =>
    84     val caret_range = before_caret_range(caret)
    82                   Protocol.CompletionItem(
    85 
    83                     label = item.replacement,
    86     val history = Completion.History.empty
    84                     detail = Some(item.description.mkString(" ")),
    87     val doc = model.content.doc
    85                     range = Some(model.content.doc.range(item.range))))
    88 
    86               case None => Nil
    89     val syntax_completion =
    87             }
    90     {
    88           case None => Nil
    91       val syntax = model.syntax()
    89         }
    92       val context = language_context(caret_range) getOrElse syntax.language_context
    90       case _ => Nil
    93 
    91     }
    94       val line = caret_pos.line
       
    95       doc.offset(Line.Position(line)) match {
       
    96         case Some(line_start) =>
       
    97           syntax.completion.complete(history, false, true,
       
    98             line_start, doc.lines(line).text, caret - line_start, context)
       
    99         case None => None
       
   100       }
       
   101     }
       
   102 
       
   103     val (no_completion, semantic_completion) =
       
   104       rendering.semantic_completion_result(
       
   105         history, false, syntax_completion.map(_.range), caret_range, doc.try_get_text(_))
       
   106 
       
   107     if (no_completion) Nil
       
   108     else {
       
   109       Completion.Result.merge(history, semantic_completion, syntax_completion) match {
       
   110         case None => Nil
       
   111         case Some(result) =>
       
   112           result.items.map(item =>
       
   113             Protocol.CompletionItem(
       
   114               label = item.replacement,
       
   115               detail = Some(item.description.mkString(" ")),
       
   116               range = Some(doc.range(item.range))))
       
   117       }
       
   118     }
       
   119   }
    92 
   120 
    93 
   121 
    94   /* diagnostics */
   122   /* diagnostics */
    95 
   123 
    96   def diagnostics: List[Text.Info[Command.Results]] =
   124   def diagnostics: List[Text.Info[Command.Results]] =