src/Tools/jEdit/src/bibtex_jedit.scala
author wenzelm
Sat Jan 07 14:34:53 2017 +0100 (2017-01-07)
changeset 64817 0bb6b582bb4f
parent 64813 7283f41d05ab
child 64828 e837f6bf653c
permissions -rw-r--r--
separate Buffer_Model vs. File_Model;
misc tuning and clarification;
     1 /*  Title:      Tools/jEdit/src/bibtex_jedit.scala
     2     Author:     Makarius
     3 
     4 BibTeX support in Isabelle/jEdit.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 
    13 import scala.collection.mutable
    14 
    15 import java.awt.event.{ActionListener, ActionEvent}
    16 
    17 import javax.swing.text.Segment
    18 import javax.swing.tree.DefaultMutableTreeNode
    19 import javax.swing.{JMenu, JMenuItem}
    20 
    21 import org.gjt.sp.jedit.Buffer
    22 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    23 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
    24 
    25 import sidekick.{SideKickParser, SideKickParsedData}
    26 
    27 
    28 object Bibtex_JEdit
    29 {
    30   /** buffer model **/
    31 
    32   /* file type */
    33 
    34   def check(buffer: Buffer): Boolean =
    35     JEdit_Lib.buffer_name(buffer).endsWith(".bib")
    36 
    37   def check(name: Document.Node.Name): Boolean =
    38     name.node.endsWith(".bib")
    39 
    40 
    41   /* parse entries */
    42 
    43   def parse_entries(text: String): List[(String, Text.Offset)] =
    44   {
    45     val chunks =
    46       try { Bibtex.parse(text) }
    47       catch { case ERROR(msg) => Output.warning(msg); Nil }
    48 
    49     val result = new mutable.ListBuffer[(String, Text.Offset)]
    50     var offset = 0
    51     for (chunk <- chunks) {
    52       if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
    53       offset += chunk.source.length
    54     }
    55     result.toList
    56   }
    57 
    58 
    59   /* retrieve entries */
    60 
    61   def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
    62     for {
    63       buffer <- JEdit_Lib.jedit_buffers()
    64       model <- Document_Model.get(buffer).iterator
    65       (name, offset) <- model.bibtex_entries.iterator
    66     } yield (name, buffer, offset)
    67 
    68 
    69   /* completion */
    70 
    71   def complete(name: String): List[String] =
    72   {
    73     val name1 = name.toLowerCase
    74     (for ((entry, _, _) <- entries_iterator() if entry.toLowerCase.containsSlice(name1))
    75       yield entry).toList
    76   }
    77 
    78   def completion(
    79     history: Completion.History,
    80     text_area: JEditTextArea,
    81     rendering: JEdit_Rendering): Option[Completion.Result] =
    82   {
    83     for {
    84       Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
    85       name1 <- Completion.clean_name(name)
    86 
    87       original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
    88       original1 <- Completion.clean_name(Library.perhaps_unquote(original))
    89 
    90       entries = complete(name1).filter(_ != original1)
    91       if entries.nonEmpty
    92 
    93       items =
    94         entries.sorted.map({
    95           case entry =>
    96             val full_name = Long_Name.qualify(Markup.CITATION, entry)
    97             val description = List(entry, "(BibTeX entry)")
    98             val replacement = quote(entry)
    99           Completion.Item(r, original, full_name, description, replacement, 0, false)
   100         }).sorted(history.ordering).take(PIDE.options.int("completion_limit"))
   101     } yield Completion.Result(r, original, false, items)
   102   }
   103 
   104 
   105 
   106   /** context menu **/
   107 
   108   def context_menu(text_area0: JEditTextArea): List[JMenuItem] =
   109   {
   110     text_area0 match {
   111       case text_area: TextArea =>
   112         text_area.getBuffer match {
   113           case buffer: Buffer
   114           if (check(buffer) && buffer.isEditable) =>
   115             val menu = new JMenu("BibTeX entries")
   116             for (entry <- Bibtex.entries) {
   117               val item = new JMenuItem(entry.kind)
   118               item.addActionListener(new ActionListener {
   119                 def actionPerformed(evt: ActionEvent): Unit =
   120                   Isabelle.insert_line_padding(text_area, entry.template)
   121               })
   122               menu.add(item)
   123             }
   124             List(menu)
   125           case _ => Nil
   126         }
   127       case _ => Nil
   128     }
   129   }
   130 
   131 
   132 
   133   /** token markup **/
   134 
   135   /* token style */
   136 
   137   private def token_style(context: String, token: Bibtex.Token): Byte =
   138     token.kind match {
   139       case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
   140       case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
   141       case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
   142       case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
   143       case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
   144       case Bibtex.Token.Kind.NAME => JEditToken.LABEL
   145       case Bibtex.Token.Kind.IDENT =>
   146         if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
   147         else
   148           Bibtex.get_entry(context) match {
   149             case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
   150             case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
   151             case _ => JEditToken.DIGIT
   152           }
   153       case Bibtex.Token.Kind.SPACE => JEditToken.NULL
   154       case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
   155       case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
   156     }
   157 
   158 
   159   /* line context */
   160 
   161   private val context_rules = new ParserRuleSet("bibtex", "MAIN")
   162 
   163   private class Line_Context(val context: Option[Bibtex.Line_Context])
   164     extends TokenMarker.LineContext(context_rules, null)
   165   {
   166     override def hashCode: Int = context.hashCode
   167     override def equals(that: Any): Boolean =
   168       that match {
   169         case other: Line_Context => context == other.context
   170         case _ => false
   171       }
   172   }
   173 
   174 
   175   /* token marker */
   176 
   177   class Token_Marker extends TokenMarker
   178   {
   179     override def markTokens(context: TokenMarker.LineContext,
   180         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
   181     {
   182       val line_ctxt =
   183         context match {
   184           case c: Line_Context => c.context
   185           case _ => Some(Bibtex.Ignored)
   186         }
   187       val line = if (raw_line == null) new Segment else raw_line
   188 
   189       def no_markup =
   190       {
   191         val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
   192         (List(styled_token), new Line_Context(None))
   193       }
   194 
   195       val context1 =
   196       {
   197         val (styled_tokens, context1) =
   198           line_ctxt match {
   199             case Some(ctxt) =>
   200               try {
   201                 val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
   202                 val styled_tokens =
   203                   for { chunk <- chunks; tok <- chunk.tokens }
   204                   yield (token_style(chunk.kind, tok), tok.source)
   205                 (styled_tokens, new Line_Context(Some(ctxt1)))
   206               }
   207               catch { case ERROR(msg) => Output.warning(msg); no_markup }
   208             case None => no_markup
   209           }
   210 
   211         var offset = 0
   212         for ((style, token) <- styled_tokens) {
   213           val length = token.length
   214           val end_offset = offset + length
   215 
   216           if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
   217             for (i <- offset until end_offset)
   218               handler.handleToken(line, style, i, 1, context1)
   219           }
   220           else handler.handleToken(line, style, offset, length, context1)
   221 
   222           offset += length
   223         }
   224         handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   225         context1
   226       }
   227       val context2 = context1.intern
   228       handler.setLineContext(context2)
   229       context2
   230     }
   231   }
   232 
   233 
   234 
   235   /** Sidekick parser **/
   236 
   237   class Sidekick_Parser extends SideKickParser("bibtex")
   238   {
   239     override def supportsCompletion = false
   240 
   241     private class Asset(label: String, label_html: String, range: Text.Range, source: String)
   242       extends Isabelle_Sidekick.Asset(label, range) {
   243         override def getShortString: String = label_html
   244         override def getLongString: String = source
   245       }
   246 
   247     def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
   248     {
   249       val data = Isabelle_Sidekick.root_data(buffer)
   250 
   251       try {
   252         var offset = 0
   253         for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
   254           val kind = chunk.kind
   255           val name = chunk.name
   256           val source = chunk.source
   257           if (kind != "") {
   258             val label = kind + (if (name == "") "" else " " + name)
   259             val label_html =
   260               "<html><b>" + HTML.output(kind) + "</b>" +
   261               (if (name == "") "" else " " + HTML.output(name)) + "</html>"
   262             val range = Text.Range(offset, offset + source.length)
   263             val asset = new Asset(label, label_html, range, source)
   264             data.root.add(new DefaultMutableTreeNode(asset))
   265           }
   266           offset += source.length
   267         }
   268         data
   269       }
   270       catch { case ERROR(msg) => Output.warning(msg); null }
   271     }
   272   }
   273 }
   274