# HG changeset patch
# User wenzelm
# Date 1497900809 -7200
# Node ID ea7c2a245b84803aebfa3e09c69d5a2bde140451
# Parent 571b698659c0b4ffd9817b18300d2118fd794aa4# Parent 070f2be51330a17cb4fa819a3aa2b7fd0ebfd37e
merged
diff -r 571b698659c0 -r ea7c2a245b84 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Pure/PIDE/document.scala Mon Jun 19 21:33:29 2017 +0200
@@ -498,6 +498,8 @@
def is_theory: Boolean = node_name.is_theory
override def toString: String = node_name.toString
+ def try_get_text(range: Text.Range): Option[String]
+
def node_required: Boolean
def get_blob: Option[Blob]
diff -r 571b698659c0 -r ea7c2a245b84 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala Mon Jun 19 21:33:29 2017 +0200
@@ -209,6 +209,17 @@
{
override def toString: String = "Rendering(" + snapshot.toString + ")"
+ def model: Document.Model
+
+
+ /* caret */
+
+ def before_caret_range(caret: Text.Offset): Text.Range =
+ {
+ val former_caret = snapshot.revert(caret)
+ snapshot.convert(Text.Range(former_caret - 1, former_caret))
+ }
+
/* completion */
@@ -231,13 +242,12 @@
history: Completion.History,
unicode: Boolean,
completed_range: Option[Text.Range],
- caret_range: Text.Range,
- try_get_text: Text.Range => Option[String]): (Boolean, Option[Completion.Result]) =
+ caret_range: Text.Range): (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 {
+ model.try_get_text(range) match {
case Some(original) => (false, names.complete(range, history, unicode, original))
case None => (false, None)
}
diff -r 571b698659c0 -r ea7c2a245b84 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Pure/PIDE/text.scala Mon Jun 19 21:33:29 2017 +0200
@@ -73,6 +73,10 @@
else Some(Range(this.start min that.start, this.stop max that.stop))
def substring(text: String): String = text.substring(start, stop)
+
+ def try_substring(text: String): Option[String] =
+ try { Some(substring(text)) }
+ catch { case _: IndexOutOfBoundsException => None }
}
diff -r 571b698659c0 -r ea7c2a245b84 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala Mon Jun 19 21:33:29 2017 +0200
@@ -422,4 +422,31 @@
}
(chunks.toList, ctxt)
}
+
+
+ /* completion */
+
+ def completion(history: Completion.History, rendering: Rendering, caret: Text.Offset,
+ complete: String => List[String]): Option[Completion.Result] =
+ {
+ for {
+ Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
+ name1 <- Completion.clean_name(name)
+
+ original <- rendering.model.try_get_text(r)
+ original1 <- Completion.clean_name(Library.perhaps_unquote(original))
+
+ entries = complete(name1).filter(_ != original1)
+ if entries.nonEmpty
+
+ items =
+ entries.sorted.map({
+ case entry =>
+ val full_name = Long_Name.qualify(Markup.CITATION, entry)
+ val description = List(entry, "(BibTeX entry)")
+ val replacement = quote(entry)
+ Completion.Item(r, original, full_name, description, replacement, 0, false)
+ }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
+ } yield Completion.Result(r, original, false, items)
+ }
}
diff -r 571b698659c0 -r ea7c2a245b84 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Pure/Tools/spell_checker.scala Mon Jun 19 21:33:29 2017 +0200
@@ -52,6 +52,15 @@
result.toList
}
+ def current_word(rendering: Rendering, range: Text.Range): Option[Text.Info[String]] =
+ {
+ for {
+ spell_range <- rendering.spell_checker_point(range)
+ text <- rendering.model.try_get_text(spell_range)
+ info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
+ } yield info
+ }
+
/* dictionaries */
@@ -210,7 +219,7 @@
Spell_Checker.marked_words(base, text, info => !check(info.info))
- /* suggestions for unknown words */
+ /* completion: suggestions for unknown words */
private def suggestions(word: String): Option[List[String]] =
{
@@ -240,6 +249,19 @@
}
def complete_enabled(word: String): Boolean = complete(word).nonEmpty
+
+ def completion(rendering: Rendering, caret: Text.Offset): Option[Completion.Result] =
+ {
+ val caret_range = rendering.before_caret_range(caret)
+ for {
+ word <- Spell_Checker.current_word(rendering, caret_range)
+ words = complete(word.info)
+ if words.nonEmpty
+ descr = "(from dictionary " + quote(dictionary.toString) + ")"
+ items =
+ words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
+ } yield Completion.Result(word.range, word.info, false, items)
+ }
}
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Mon Jun 19 21:33:29 2017 +0200
@@ -39,7 +39,6 @@
def text_length: Text.Offset = doc.text_length
def text_range: Text.Range = doc.text_range
def text: String = doc.text
- def try_get_text(range: Text.Range): Option[String] = doc.try_get_text(range)
lazy val bytes: Bytes = Bytes(text)
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
@@ -64,6 +63,14 @@
published_diagnostics: List[Text.Info[Command.Results]] = Nil,
published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model
{
+ model =>
+
+
+ /* text */
+
+ def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
+
+
/* external file */
def external(b: Boolean): Document_Model = copy(external_file = b)
@@ -84,7 +91,7 @@
: (Boolean, Document.Node.Perspective_Text) =
{
if (is_theory) {
- val snapshot = this.snapshot()
+ val snapshot = model.snapshot()
val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
val caret_range =
@@ -192,7 +199,7 @@
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
- new VSCode_Rendering(this, snapshot)
+ new VSCode_Rendering(snapshot, model)
def rendering(): VSCode_Rendering = rendering(snapshot())
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Jun 19 21:33:29 2017 +0200
@@ -65,20 +65,16 @@
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
}
-class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot)
- extends Rendering(snapshot, model.resources.options, model.session)
+class VSCode_Rendering(snapshot: Document.Snapshot, _model: Document_Model)
+ extends Rendering(snapshot, _model.resources.options, _model.session)
{
rendering =>
+ def model: Document_Model = _model
+
/* completion */
- 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 doc = model.content.doc
@@ -97,11 +93,15 @@
val (no_completion, semantic_completion) =
rendering.semantic_completion_result(
- history, false, syntax_completion.map(_.range), caret_range, doc.try_get_text(_))
+ history, false, syntax_completion.map(_.range), caret_range)
if (no_completion) Nil
else {
- Completion.Result.merge(history, semantic_completion, syntax_completion) match {
+ val results =
+ Completion.Result.merge(history,
+ Completion.Result.merge(history, semantic_completion, syntax_completion),
+ spell_checker_completion(caret))
+ results match {
case None => Nil
case Some(result) =>
result.items.map(item =>
@@ -199,12 +199,15 @@
(for {
spell_checker <- model.resources.spell_checker.get.iterator
spell_range <- spell_checker_ranges(model.content.text_range).iterator
- text <- model.content.try_get_text(spell_range).iterator
+ text <- model.try_get_text(spell_range).iterator
info <- spell_checker.marked_words(spell_range.start, text).iterator
} yield info.range).toList
Document_Model.Decoration.ranges("spell_checker", ranges)
}
+ def spell_checker_completion(caret: Text.Offset): Option[Completion.Result] =
+ model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
+
/* decorations */
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Jun 19 21:33:29 2017 +0200
@@ -21,7 +21,6 @@
declare -a SOURCES=(
"src/active.scala"
- "src/bibtex_jedit.scala"
"src/completion_popup.scala"
"src/context_menu.scala"
"src/debugger_dockable.scala"
@@ -37,6 +36,7 @@
"src/isabelle_encoding.scala"
"src/isabelle_options.scala"
"src/isabelle_sidekick.scala"
+ "src/jedit_bibtex.scala"
"src/jedit_editor.scala"
"src/jedit_lib.scala"
"src/jedit_options.scala"
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Mon Jun 19 16:42:28 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,234 +0,0 @@
-/* Title: Tools/jEdit/src/bibtex_jedit.scala
- Author: Makarius
-
-BibTeX support in Isabelle/jEdit.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-
-import scala.collection.mutable
-
-import java.awt.event.{ActionListener, ActionEvent}
-
-import javax.swing.text.Segment
-import javax.swing.tree.DefaultMutableTreeNode
-import javax.swing.{JMenu, JMenuItem}
-
-import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
-import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
-
-import sidekick.{SideKickParser, SideKickParsedData}
-
-
-object Bibtex_JEdit
-{
- /** completion **/
-
- def complete(name: String): List[String] =
- (for {
- Text.Info(_, (entry, _)) <- Document_Model.bibtex_entries_iterator()
- if entry.toLowerCase.containsSlice(name.toLowerCase)
- } yield entry).toList
-
- def completion(
- history: Completion.History,
- text_area: JEditTextArea,
- rendering: JEdit_Rendering): Option[Completion.Result] =
- {
- for {
- Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
- name1 <- Completion.clean_name(name)
-
- original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
- original1 <- Completion.clean_name(Library.perhaps_unquote(original))
-
- entries = complete(name1).filter(_ != original1)
- if entries.nonEmpty
-
- items =
- entries.sorted.map({
- case entry =>
- val full_name = Long_Name.qualify(Markup.CITATION, entry)
- val description = List(entry, "(BibTeX entry)")
- val replacement = quote(entry)
- Completion.Item(r, original, full_name, description, replacement, 0, false)
- }).sorted(history.ordering).take(PIDE.options.int("completion_limit"))
- } yield Completion.Result(r, original, false, items)
- }
-
-
-
- /** context menu **/
-
- def context_menu(text_area0: JEditTextArea): List[JMenuItem] =
- {
- text_area0 match {
- case text_area: TextArea =>
- text_area.getBuffer match {
- case buffer: Buffer
- if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
- val menu = new JMenu("BibTeX entries")
- for (entry <- Bibtex.entries) {
- val item = new JMenuItem(entry.kind)
- item.addActionListener(new ActionListener {
- def actionPerformed(evt: ActionEvent): Unit =
- Isabelle.insert_line_padding(text_area, entry.template)
- })
- menu.add(item)
- }
- List(menu)
- case _ => Nil
- }
- case _ => Nil
- }
- }
-
-
-
- /** token markup **/
-
- /* token style */
-
- private def token_style(context: String, token: Bibtex.Token): Byte =
- token.kind match {
- case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
- case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
- case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
- case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
- case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
- case Bibtex.Token.Kind.NAME => JEditToken.LABEL
- case Bibtex.Token.Kind.IDENT =>
- if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
- else
- Bibtex.get_entry(context) match {
- case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
- case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
- case _ => JEditToken.DIGIT
- }
- case Bibtex.Token.Kind.SPACE => JEditToken.NULL
- case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
- case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
- }
-
-
- /* line context */
-
- private val context_rules = new ParserRuleSet("bibtex", "MAIN")
-
- private class Line_Context(val context: Option[Bibtex.Line_Context])
- extends TokenMarker.LineContext(context_rules, null)
- {
- override def hashCode: Int = context.hashCode
- override def equals(that: Any): Boolean =
- that match {
- case other: Line_Context => context == other.context
- case _ => false
- }
- }
-
-
- /* token marker */
-
- class Token_Marker extends TokenMarker
- {
- override def markTokens(context: TokenMarker.LineContext,
- handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
- {
- val line_ctxt =
- context match {
- case c: Line_Context => c.context
- case _ => Some(Bibtex.Ignored)
- }
- val line = if (raw_line == null) new Segment else raw_line
-
- def no_markup =
- {
- val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
- (List(styled_token), new Line_Context(None))
- }
-
- val context1 =
- {
- val (styled_tokens, context1) =
- line_ctxt match {
- case Some(ctxt) =>
- try {
- val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
- val styled_tokens =
- for { chunk <- chunks; tok <- chunk.tokens }
- yield (token_style(chunk.kind, tok), tok.source)
- (styled_tokens, new Line_Context(Some(ctxt1)))
- }
- catch { case ERROR(msg) => Output.warning(msg); no_markup }
- case None => no_markup
- }
-
- var offset = 0
- for ((style, token) <- styled_tokens) {
- val length = token.length
- val end_offset = offset + length
-
- if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
- for (i <- offset until end_offset)
- handler.handleToken(line, style, i, 1, context1)
- }
- else handler.handleToken(line, style, offset, length, context1)
-
- offset += length
- }
- handler.handleToken(line, JEditToken.END, line.count, 0, context1)
- context1
- }
- val context2 = context1.intern
- handler.setLineContext(context2)
- context2
- }
- }
-
-
-
- /** Sidekick parser **/
-
- class Sidekick_Parser extends SideKickParser("bibtex")
- {
- override def supportsCompletion = false
-
- private class Asset(label: String, label_html: String, range: Text.Range, source: String)
- extends Isabelle_Sidekick.Asset(label, range) {
- override def getShortString: String = label_html
- override def getLongString: String = source
- }
-
- def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
- {
- val data = Isabelle_Sidekick.root_data(buffer)
-
- try {
- var offset = 0
- for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
- val kind = chunk.kind
- val name = chunk.name
- val source = chunk.source
- if (kind != "") {
- val label = kind + (if (name == "") "" else " " + name)
- val label_html =
- "" + HTML.output(kind) + "" +
- (if (name == "") "" else " " + HTML.output(name)) + ""
- val range = Text.Range(offset, offset + source.length)
- val asset = new Asset(label, label_html, range, source)
- data.root.add(new DefaultMutableTreeNode(asset))
- }
- offset += source.length
- }
- data
- }
- catch { case ERROR(msg) => Output.warning(msg); null }
- }
- }
-}
-
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Jun 19 21:33:29 2017 +0200
@@ -125,15 +125,16 @@
active_range match {
case Some(range) => range.try_restrict(line_range)
case None =>
- if (line_range.contains(text_area.getCaretPosition)) {
- JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
+ val caret = text_area.getCaretPosition
+ if (line_range.contains(caret)) {
+ 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,
syntax_completion(Completion.History.empty, true, Some(rendering)),
Completion.Result.merge(Completion.History.empty,
path_completion(rendering),
- Bibtex_JEdit.completion(Completion.History.empty, text_area, rendering)))
+ JEdit_Bibtex.completion(Completion.History.empty, rendering, caret)))
.map(_.range)
rendering.semantic_completion(range0, range) match {
case None => range0
@@ -164,7 +165,7 @@
(for {
rendering <- opt_rendering
if PIDE.options.bool("jedit_completion_context")
- caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
+ caret_range = rendering.before_caret_range(text_area.getCaretPosition)
context <- rendering.language_context(caret_range)
} yield context) getOrElse syntax.language_context
@@ -226,7 +227,7 @@
s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
for {
- r1 <- rendering.language_path(JEdit_Lib.before_caret_range(text_area, rendering))
+ r1 <- rendering.language_path(rendering.before_caret_range(text_area.getCaretPosition))
s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
if is_wrapped(s1)
r2 = Text.Range(r1.start + 1, r1.stop - 1)
@@ -349,6 +350,7 @@
}
if (buffer.isEditable) {
+ val caret = text_area.getCaretPosition
val opt_rendering = Document_View.get(text_area).map(_.get_rendering())
val result0 = syntax_completion(history, explicit, opt_rendering)
val (no_completion, semantic_completion) =
@@ -356,8 +358,7 @@
opt_rendering match {
case Some(rendering) =>
rendering.semantic_completion_result(history, unicode, result0.map(_.range),
- JEdit_Lib.before_caret_range(text_area, rendering),
- JEdit_Lib.try_get_text(buffer, _))
+ rendering.before_caret_range(caret))
case None => (false, None)
}
}
@@ -373,10 +374,10 @@
case Some(rendering) =>
Completion.Result.merge(history, result1,
Completion.Result.merge(history,
- JEdit_Spell_Checker.completion(text_area, explicit, rendering),
+ JEdit_Spell_Checker.completion(rendering, explicit, caret),
Completion.Result.merge(history,
path_completion(rendering),
- Bibtex_JEdit.completion(history, text_area, rendering))))
+ JEdit_Bibtex.completion(history, rendering, caret))))
}
}
result match {
@@ -509,7 +510,7 @@
val range = item.range
if (text_field.isEditable) {
val content = text_field.getText
- JEdit_Lib.try_get_text(content, range) match {
+ range.try_substring(content) match {
case Some(text) if text == item.original =>
text_field.setText(
content.substring(0, range.start) +
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/context_menu.scala Mon Jun 19 21:33:29 2017 +0200
@@ -35,7 +35,7 @@
}
else Nil
- val items2 = Bibtex_JEdit.context_menu(text_area)
+ val items2 = JEdit_Bibtex.context_menu(text_area)
val items = items1 ::: items2
if (items.isEmpty) null else items.toArray
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Jun 19 21:33:29 2017 +0200
@@ -372,6 +372,10 @@
object File_Model
{
+ def empty(session: Session): File_Model =
+ File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
+ false, Document.Node.no_perspective_text, Nil)
+
def init(session: Session,
node_name: Document.Node.Name,
text: String,
@@ -396,6 +400,12 @@
last_perspective: Document.Node.Perspective_Text,
pending_edits: List[Text.Edit]) extends Document_Model
{
+ /* text */
+
+ def try_get_text(range: Text.Range): Option[String] =
+ range.try_substring(content.text)
+
+
/* header */
def node_header: Document.Node.Header =
@@ -457,6 +467,12 @@
case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
extends Document_Model
{
+ /* text */
+
+ def try_get_text(range: Text.Range): Option[String] =
+ JEdit_Lib.try_get_text(buffer, range)
+
+
/* header */
def node_header(): Document.Node.Header =
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Mon Jun 19 21:33:29 2017 +0200
@@ -60,7 +60,8 @@
{
private val session = model.session
- def get_rendering(): JEdit_Rendering = JEdit_Rendering(model.snapshot(), PIDE.options.value)
+ def get_rendering(): JEdit_Rendering =
+ JEdit_Rendering(model.snapshot(), model, PIDE.options.value)
val rich_text_area =
new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Jun 19 21:33:29 2017 +0200
@@ -68,7 +68,8 @@
{
Pretty_Tooltip.invoke(() =>
{
- val rendering = JEdit_Rendering(snapshot, options)
+ val model = File_Model.empty(PIDE.session)
+ val rendering = JEdit_Rendering(snapshot, model, options)
val info = Text.Info(Text.Range.offside, body)
Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
})
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Jun 19 21:33:29 2017 +0200
@@ -74,7 +74,7 @@
private val mode_markers: Map[String, TokenMarker] =
Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) +
- ("bibtex" -> new Bibtex_JEdit.Token_Marker)
+ ("bibtex" -> new JEdit_Bibtex.Token_Marker)
def mode_token_marker(mode: String): Option[TokenMarker] = mode_markers.get(mode)
@@ -419,7 +419,7 @@
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
range = JEdit_Lib.caret_range(text_area)
- Text.Info(_, word) <- JEdit_Spell_Checker.current_word(text_area, rendering, range)
+ Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} {
spell_checker.update(word, include, permanent)
JEdit_Lib.jedit_views().foreach(_.repaint())
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/jedit_bibtex.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala Mon Jun 19 21:33:29 2017 +0200
@@ -0,0 +1,210 @@
+/* Title: Tools/jEdit/src/jedit_bibtex.scala
+ Author: Makarius
+
+BibTeX support in Isabelle/jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import scala.collection.mutable
+
+import java.awt.event.{ActionListener, ActionEvent}
+
+import javax.swing.text.Segment
+import javax.swing.tree.DefaultMutableTreeNode
+import javax.swing.{JMenu, JMenuItem}
+
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
+
+import sidekick.{SideKickParser, SideKickParsedData}
+
+
+object JEdit_Bibtex
+{
+ /** completion **/
+
+ def complete(name: String): List[String] =
+ (for {
+ Text.Info(_, (entry, _)) <- Document_Model.bibtex_entries_iterator()
+ if entry.toLowerCase.containsSlice(name.toLowerCase)
+ } yield entry).toList
+
+ def completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
+ : Option[Completion.Result] = Bibtex.completion(history, rendering, caret, complete _)
+
+
+
+ /** context menu **/
+
+ def context_menu(text_area0: JEditTextArea): List[JMenuItem] =
+ {
+ text_area0 match {
+ case text_area: TextArea =>
+ text_area.getBuffer match {
+ case buffer: Buffer
+ if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
+ val menu = new JMenu("BibTeX entries")
+ for (entry <- Bibtex.entries) {
+ val item = new JMenuItem(entry.kind)
+ item.addActionListener(new ActionListener {
+ def actionPerformed(evt: ActionEvent): Unit =
+ Isabelle.insert_line_padding(text_area, entry.template)
+ })
+ menu.add(item)
+ }
+ List(menu)
+ case _ => Nil
+ }
+ case _ => Nil
+ }
+ }
+
+
+
+ /** token markup **/
+
+ /* token style */
+
+ private def token_style(context: String, token: Bibtex.Token): Byte =
+ token.kind match {
+ case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
+ case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
+ case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
+ case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
+ case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
+ case Bibtex.Token.Kind.NAME => JEditToken.LABEL
+ case Bibtex.Token.Kind.IDENT =>
+ if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
+ else
+ Bibtex.get_entry(context) match {
+ case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
+ case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
+ case _ => JEditToken.DIGIT
+ }
+ case Bibtex.Token.Kind.SPACE => JEditToken.NULL
+ case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
+ case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
+ }
+
+
+ /* line context */
+
+ private val context_rules = new ParserRuleSet("bibtex", "MAIN")
+
+ private class Line_Context(val context: Option[Bibtex.Line_Context])
+ extends TokenMarker.LineContext(context_rules, null)
+ {
+ override def hashCode: Int = context.hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Line_Context => context == other.context
+ case _ => false
+ }
+ }
+
+
+ /* token marker */
+
+ class Token_Marker extends TokenMarker
+ {
+ override def markTokens(context: TokenMarker.LineContext,
+ handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
+ {
+ val line_ctxt =
+ context match {
+ case c: Line_Context => c.context
+ case _ => Some(Bibtex.Ignored)
+ }
+ val line = if (raw_line == null) new Segment else raw_line
+
+ def no_markup =
+ {
+ val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
+ (List(styled_token), new Line_Context(None))
+ }
+
+ val context1 =
+ {
+ val (styled_tokens, context1) =
+ line_ctxt match {
+ case Some(ctxt) =>
+ try {
+ val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
+ val styled_tokens =
+ for { chunk <- chunks; tok <- chunk.tokens }
+ yield (token_style(chunk.kind, tok), tok.source)
+ (styled_tokens, new Line_Context(Some(ctxt1)))
+ }
+ catch { case ERROR(msg) => Output.warning(msg); no_markup }
+ case None => no_markup
+ }
+
+ var offset = 0
+ for ((style, token) <- styled_tokens) {
+ val length = token.length
+ val end_offset = offset + length
+
+ if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
+ for (i <- offset until end_offset)
+ handler.handleToken(line, style, i, 1, context1)
+ }
+ else handler.handleToken(line, style, offset, length, context1)
+
+ offset += length
+ }
+ handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+ context1
+ }
+ val context2 = context1.intern
+ handler.setLineContext(context2)
+ context2
+ }
+ }
+
+
+
+ /** Sidekick parser **/
+
+ class Sidekick_Parser extends SideKickParser("bibtex")
+ {
+ override def supportsCompletion = false
+
+ private class Asset(label: String, label_html: String, range: Text.Range, source: String)
+ extends Isabelle_Sidekick.Asset(label, range) {
+ override def getShortString: String = label_html
+ override def getLongString: String = source
+ }
+
+ def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
+ {
+ val data = Isabelle_Sidekick.root_data(buffer)
+
+ try {
+ var offset = 0
+ for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
+ val kind = chunk.kind
+ val name = chunk.name
+ val source = chunk.source
+ if (kind != "") {
+ val label = kind + (if (name == "") "" else " " + name)
+ val label_html =
+ "" + HTML.output(kind) + "" +
+ (if (name == "") "" else " " + HTML.output(name)) + ""
+ val range = Text.Range(offset, offset + source.length)
+ val asset = new Asset(label, label_html, range, source)
+ data.root.add(new DefaultMutableTreeNode(asset))
+ }
+ offset += source.length
+ }
+ data
+ }
+ catch { case ERROR(msg) => Output.warning(msg); null }
+ }
+ }
+}
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Jun 19 21:33:29 2017 +0200
@@ -175,10 +175,6 @@
try { Some(buffer.getText(range.start, range.length)) }
catch { case _: ArrayIndexOutOfBoundsException => None }
- def try_get_text(text: String, range: Text.Range): Option[String] =
- try { Some(range.substring(text)) }
- catch { case _: IndexOutOfBoundsException => None }
-
/* point range */
@@ -211,13 +207,6 @@
def caret_range(text_area: TextArea): Text.Range =
point_range(text_area.getBuffer, text_area.getCaretPosition)
- def before_caret_range(text_area: TextArea, rendering: JEdit_Rendering): Text.Range =
- {
- val snapshot = rendering.snapshot
- val former_caret = snapshot.revert(text_area.getCaretPosition)
- snapshot.convert(Text.Range(former_caret - 1, former_caret))
- }
-
def visible_range(text_area: TextArea): Option[Text.Range] =
{
val buffer = text_area.getBuffer
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Jun 19 21:33:29 2017 +0200
@@ -21,8 +21,8 @@
object JEdit_Rendering
{
- def apply(snapshot: Document.Snapshot, options: Options): JEdit_Rendering =
- new JEdit_Rendering(snapshot, options)
+ def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
+ new JEdit_Rendering(snapshot, model, options)
/* popup window bounds */
@@ -148,9 +148,12 @@
}
-class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
+class JEdit_Rendering(snapshot: Document.Snapshot, _model: Document_Model, options: Options)
extends Rendering(snapshot, options, PIDE.session)
{
+ def model: Document_Model = _model
+
+
/* colors */
def color(s: String): Color =
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 21:33:29 2017 +0200
@@ -19,36 +19,16 @@
object JEdit_Spell_Checker
{
- /* words within text */
-
- def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range)
- : Option[Text.Info[String]] =
- {
- for {
- spell_range <- rendering.spell_checker_point(range)
- text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
- info <- Spell_Checker.marked_words(
- spell_range.start, text, info => info.range.overlaps(range)).headOption
- } yield info
- }
-
-
/* completion */
- def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering)
- : Option[Completion.Result] =
+ def completion(
+ rendering: JEdit_Rendering, explicit: Boolean, caret: Text.Offset): Option[Completion.Result] =
{
- for {
- spell_checker <- PIDE.plugin.spell_checker.get
- if explicit
- range = JEdit_Lib.before_caret_range(text_area, rendering)
- word <- current_word(text_area, rendering, range)
- words = spell_checker.complete(word.info)
- if words.nonEmpty
- descr = "(from dictionary " + quote(spell_checker.toString) + ")"
- items =
- words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
- } yield Completion.Result(word.range, word.info, false, items)
+ PIDE.plugin.spell_checker.get match {
+ case Some(spell_checker) if explicit =>
+ spell_checker.completion(rendering, caret)
+ case _ => None
+ }
}
@@ -62,7 +42,7 @@
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
range = JEdit_Lib.point_range(text_area.getBuffer, offset)
- Text.Info(_, word) <- current_word(text_area, rendering, range)
+ Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} yield (spell_checker, word)
result match {
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Jun 19 21:33:29 2017 +0200
@@ -57,7 +57,8 @@
formatted_body: XML.Body): (String, JEdit_Rendering) =
{
val (text, state) = document_state(base_snapshot, base_results, formatted_body)
- val rendering = JEdit_Rendering(state.snapshot(), PIDE.options.value)
+ val model = File_Model.empty(PIDE.session)
+ val rendering = JEdit_Rendering(state.snapshot(), model, PIDE.options.value)
(text, rendering)
}
}
diff -r 571b698659c0 -r ea7c2a245b84 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml Mon Jun 19 16:42:28 2017 +0100
+++ b/src/Tools/jEdit/src/services.xml Mon Jun 19 21:33:29 2017 +0200
@@ -39,7 +39,7 @@
new isabelle.jedit.Isabelle_Sidekick_Root();
- new isabelle.jedit.Bibtex_JEdit.Sidekick_Parser();
+ new isabelle.jedit.JEdit_Bibtex.Sidekick_Parser();
new isabelle.jedit.Scala_Console();