# HG changeset patch
# User wenzelm
# Date 1483877297 -3600
# Node ID 0f410e3b1d200826cc287cb89b613d44bf10678a
# Parent  f6a09ac4e640e7dadbd4347e73e45f780a170969
support for bibtex entries;

diff -r f6a09ac4e640 -r 0f410e3b1d20 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Jan 08 13:03:14 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Jan 08 13:08:17 2017 +0100
@@ -31,7 +31,7 @@
 
     let server_options: ServerOptions = { run: run, debug: run };
     let client_options: LanguageClientOptions = {
-      documentSelector: ["isabelle", "isabelle-ml"]
+      documentSelector: ["isabelle", "isabelle-ml", "bibtex"]
     };
 
     let disposable = new LanguageClient("Isabelle", server_options, client_options, false).start();
diff -r f6a09ac4e640 -r 0f410e3b1d20 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sun Jan 08 13:03:14 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Jan 08 13:08:17 2017 +0100
@@ -18,8 +18,12 @@
   {
     def text_range: Text.Range = doc.text_range
     def text: String = doc.text
+
     lazy val bytes: Bytes = Bytes(text)
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
+    lazy val bibtex_entries: List[Text.Info[String]] =
+      try { Bibtex.document_entries(text) }
+      catch { case ERROR(_) => Nil }
   }
 
   def init(session: Session, node_name: Document.Node.Name): Document_Model =
diff -r f6a09ac4e640 -r 0f410e3b1d20 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 08 13:03:14 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 08 13:08:17 2017 +0100
@@ -34,7 +34,7 @@
       Markup.BAD)
 
   private val hyperlink_elements =
-    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
+    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
 }
 
 class VSCode_Rendering(
@@ -140,6 +140,14 @@
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
             hyperlink_position(props).map(_ :: links)
 
+          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
+            val iterator =
+              for {
+                Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
+                if entry == name
+              } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
+            if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
+
           case _ => None
         }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
   }
diff -r f6a09ac4e640 -r 0f410e3b1d20 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 13:03:14 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 13:08:17 2017 +0100
@@ -86,6 +86,12 @@
   def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
   def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
 
+  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
+    for {
+      (_, model) <- state.value.models.iterator
+      Text.Info(range, entry) <- model.content.bibtex_entries.iterator
+    } yield Text.Info(range, (entry, model))
+
   def visible_node(name: Document.Node.Name): Boolean =
     get_model(name) match {
       case Some(model) => model.node_visible