author | wenzelm |
Sun, 05 Oct 2014 17:58:36 +0200 | |
changeset 58545 | 30b75b7958d6 |
child 58546 | 72e2b2a609c4 |
permissions | -rw-r--r-- |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/bibtex_jedit.scala |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
3 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
4 |
BibTeX support in Isabelle/jEdit. |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
6 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
8 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
9 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
11 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
12 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
13 |
import org.gjt.sp.jedit.Buffer |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
14 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
15 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
16 |
object Bibtex_JEdit |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
17 |
{ |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
18 |
/* buffer model entries */ |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
19 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
20 |
def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] = |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
21 |
for { |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
22 |
buffer <- JEdit_Lib.jedit_buffers() |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
23 |
model <- PIDE.document_model(buffer).iterator |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
24 |
(name, offset) <- model.bibtex_entries.iterator |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
25 |
} yield (name, buffer, offset) |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
26 |
} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
27 |