# HG changeset patch
# User wenzelm
# Date 1497899706 -7200
# Node ID e03ff7e831cc66e5d1f0860d358f37e9160f7bc7
# Parent 0b257d7d81a5e96f0f55f4327ce5ffcb746a5485
clarified modules;
diff -r 0b257d7d81a5 -r e03ff7e831cc src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Jun 19 21:09:19 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Jun 19 21:15:06 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 0b257d7d81a5 -r e03ff7e831cc src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Mon Jun 19 21:09:19 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,210 +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, 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 0b257d7d81a5 -r e03ff7e831cc src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Jun 19 21:09:19 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Jun 19 21:15:06 2017 +0200
@@ -134,7 +134,7 @@
syntax_completion(Completion.History.empty, true, Some(rendering)),
Completion.Result.merge(Completion.History.empty,
path_completion(rendering),
- Bibtex_JEdit.completion(Completion.History.empty, rendering, caret)))
+ JEdit_Bibtex.completion(Completion.History.empty, rendering, caret)))
.map(_.range)
rendering.semantic_completion(range0, range) match {
case None => range0
@@ -377,7 +377,7 @@
JEdit_Spell_Checker.completion(rendering, explicit, caret),
Completion.Result.merge(history,
path_completion(rendering),
- Bibtex_JEdit.completion(history, rendering, caret))))
+ JEdit_Bibtex.completion(history, rendering, caret))))
}
}
result match {
diff -r 0b257d7d81a5 -r e03ff7e831cc src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala Mon Jun 19 21:09:19 2017 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala Mon Jun 19 21:15:06 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 0b257d7d81a5 -r e03ff7e831cc src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala Mon Jun 19 21:09:19 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Jun 19 21:15:06 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)
diff -r 0b257d7d81a5 -r e03ff7e831cc 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:15:06 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 0b257d7d81a5 -r e03ff7e831cc src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml Mon Jun 19 21:09:19 2017 +0200
+++ b/src/Tools/jEdit/src/services.xml Mon Jun 19 21:15:06 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();