clarified modules;
authorwenzelm
Sun Oct 05 18:14:26 2014 +0200 (2014-10-05 ago)
changeset 5854672e2b2a609c4
parent 58545 30b75b7958d6
child 58547 6080615b8b96
clarified modules;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/bibtex_token_markup.scala
src/Tools/jEdit/src/context_menu.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/services.xml
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 05 17:58:36 2014 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 05 18:14:26 2014 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  declare -a SOURCES=(
     1.5    "src/active.scala"
     1.6    "src/bibtex_jedit.scala"
     1.7 -  "src/bibtex_token_markup.scala"
     1.8    "src/completion_popup.scala"
     1.9    "src/context_menu.scala"
    1.10    "src/dockable.scala"
     2.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 17:58:36 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 18:14:26 2014 +0200
     2.3 @@ -10,12 +10,21 @@
     2.4  import isabelle._
     2.5  
     2.6  
     2.7 +import javax.swing.text.Segment
     2.8 +import javax.swing.tree.DefaultMutableTreeNode
     2.9 +
    2.10  import org.gjt.sp.jedit.Buffer
    2.11 +import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
    2.12 +
    2.13 +import sidekick.{SideKickParser, SideKickParsedData}
    2.14  
    2.15  
    2.16  object Bibtex_JEdit
    2.17  {
    2.18 -  /* buffer model entries */
    2.19 +  /** buffer model **/
    2.20 +
    2.21 +  def check(buffer: Buffer): Boolean =
    2.22 +    JEdit_Lib.buffer_name(buffer).endsWith(".bib")
    2.23  
    2.24    def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
    2.25      for {
    2.26 @@ -23,5 +32,132 @@
    2.27        model <- PIDE.document_model(buffer).iterator
    2.28        (name, offset) <- model.bibtex_entries.iterator
    2.29      } yield (name, buffer, offset)
    2.30 +
    2.31 +
    2.32 +
    2.33 +  /** token markup **/
    2.34 +
    2.35 +  /* token style */
    2.36 +
    2.37 +  private def token_style(context: String, token: Bibtex.Token): Byte =
    2.38 +    token.kind match {
    2.39 +      case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
    2.40 +      case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
    2.41 +      case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
    2.42 +      case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
    2.43 +      case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
    2.44 +      case Bibtex.Token.Kind.NAME => JEditToken.LABEL
    2.45 +      case Bibtex.Token.Kind.IDENT =>
    2.46 +        if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
    2.47 +        else
    2.48 +          Bibtex.get_entry(context) match {
    2.49 +            case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
    2.50 +            case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
    2.51 +            case _ => JEditToken.DIGIT
    2.52 +          }
    2.53 +      case Bibtex.Token.Kind.SPACE => JEditToken.NULL
    2.54 +      case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
    2.55 +      case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
    2.56 +    }
    2.57 +
    2.58 +
    2.59 +  /* line context */
    2.60 +
    2.61 +  private val context_rules = new ParserRuleSet("bibtex", "MAIN")
    2.62 +
    2.63 +  private class Line_Context(context: Option[Bibtex.Line_Context])
    2.64 +    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
    2.65 +
    2.66 +
    2.67 +  /* token marker */
    2.68 +
    2.69 +  class Token_Marker extends TokenMarker
    2.70 +  {
    2.71 +    override def markTokens(context: TokenMarker.LineContext,
    2.72 +        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
    2.73 +    {
    2.74 +      val line_ctxt =
    2.75 +        context match {
    2.76 +          case c: Line_Context => c.context
    2.77 +          case _ => Some(Bibtex.Ignored_Context)
    2.78 +        }
    2.79 +      val line = if (raw_line == null) new Segment else raw_line
    2.80 +
    2.81 +      val context1 =
    2.82 +      {
    2.83 +        val (styled_tokens, context1) =
    2.84 +          line_ctxt match {
    2.85 +            case Some(ctxt) =>
    2.86 +              val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
    2.87 +              val styled_tokens =
    2.88 +                for { chunk <- chunks; tok <- chunk.tokens }
    2.89 +                yield (token_style(chunk.kind, tok), tok.source)
    2.90 +              (styled_tokens, new Line_Context(Some(ctxt1)))
    2.91 +            case None =>
    2.92 +              val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
    2.93 +              (List(styled_token), new Line_Context(None))
    2.94 +          }
    2.95 +
    2.96 +        var offset = 0
    2.97 +        for ((style, token) <- styled_tokens) {
    2.98 +          val length = token.length
    2.99 +          val end_offset = offset + length
   2.100 +
   2.101 +          if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
   2.102 +            for (i <- offset until end_offset)
   2.103 +              handler.handleToken(line, style, i, 1, context1)
   2.104 +          }
   2.105 +          else handler.handleToken(line, style, offset, length, context1)
   2.106 +
   2.107 +          offset += length
   2.108 +        }
   2.109 +        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   2.110 +        context1
   2.111 +      }
   2.112 +      val context2 = context1.intern
   2.113 +      handler.setLineContext(context2)
   2.114 +      context2
   2.115 +    }
   2.116 +  }
   2.117 +
   2.118 +
   2.119 +
   2.120 +  /** Sidekick parser **/
   2.121 +
   2.122 +  class Sidekick_Parser extends SideKickParser("bibtex")
   2.123 +  {
   2.124 +    override def supportsCompletion = false
   2.125 +
   2.126 +    private class Asset(
   2.127 +        label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String)
   2.128 +      extends Isabelle_Sidekick.Asset(label, start, stop) {
   2.129 +        override def getShortString: String = label_html
   2.130 +        override def getLongString: String = source
   2.131 +      }
   2.132 +
   2.133 +    def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
   2.134 +    {
   2.135 +      val data = Isabelle_Sidekick.root_data(buffer)
   2.136 +
   2.137 +      try {
   2.138 +        var offset = 0
   2.139 +        for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
   2.140 +          val kind = chunk.kind
   2.141 +          val name = chunk.name
   2.142 +          val source = chunk.source
   2.143 +          if (kind != "") {
   2.144 +            val label = kind + (if (name == "") "" else " " + name)
   2.145 +            val label_html =
   2.146 +              "<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>"
   2.147 +            val asset = new Asset(label, label_html, offset, offset + source.size, source)
   2.148 +            data.root.add(new DefaultMutableTreeNode(asset))
   2.149 +          }
   2.150 +          offset += source.size
   2.151 +        }
   2.152 +        data
   2.153 +      }
   2.154 +      catch { case ERROR(_) => null }
   2.155 +    }
   2.156 +  }
   2.157  }
   2.158  
     3.1 --- a/src/Tools/jEdit/src/bibtex_token_markup.scala	Sun Oct 05 17:58:36 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,102 +0,0 @@
     3.4 -/*  Title:      Tools/jEdit/src/bibtex_token_markup.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Bibtex token markup.
     3.8 -*/
     3.9 -
    3.10 -package isabelle.jedit
    3.11 -
    3.12 -
    3.13 -import isabelle._
    3.14 -
    3.15 -import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
    3.16 -
    3.17 -import javax.swing.text.Segment
    3.18 -
    3.19 -
    3.20 -object Bibtex_Token_Markup
    3.21 -{
    3.22 -  /* token style */
    3.23 -
    3.24 -  private def token_style(context: String, token: Bibtex.Token): Byte =
    3.25 -    token.kind match {
    3.26 -      case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
    3.27 -      case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
    3.28 -      case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
    3.29 -      case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
    3.30 -      case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
    3.31 -      case Bibtex.Token.Kind.NAME => JEditToken.LABEL
    3.32 -      case Bibtex.Token.Kind.IDENT =>
    3.33 -        if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
    3.34 -        else
    3.35 -          Bibtex.get_entry(context) match {
    3.36 -            case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
    3.37 -            case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
    3.38 -            case _ => JEditToken.DIGIT
    3.39 -          }
    3.40 -      case Bibtex.Token.Kind.SPACE => JEditToken.NULL
    3.41 -      case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
    3.42 -      case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
    3.43 -    }
    3.44 -
    3.45 -
    3.46 -  /* line context */
    3.47 -
    3.48 -  private val context_rules = new ParserRuleSet("bibtex", "MAIN")
    3.49 -
    3.50 -  private class Line_Context(context: Option[Bibtex.Line_Context])
    3.51 -    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
    3.52 -
    3.53 -
    3.54 -  /* token marker */
    3.55 -
    3.56 -  class Marker extends TokenMarker
    3.57 -  {
    3.58 -    override def markTokens(context: TokenMarker.LineContext,
    3.59 -        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
    3.60 -    {
    3.61 -      val line_ctxt =
    3.62 -        context match {
    3.63 -          case c: Line_Context => c.context
    3.64 -          case _ => Some(Bibtex.Ignored_Context)
    3.65 -        }
    3.66 -      val line = if (raw_line == null) new Segment else raw_line
    3.67 -
    3.68 -      val context1 =
    3.69 -      {
    3.70 -        val (styled_tokens, context1) =
    3.71 -          line_ctxt match {
    3.72 -            case Some(ctxt) =>
    3.73 -              val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
    3.74 -              val styled_tokens =
    3.75 -                for { chunk <- chunks; tok <- chunk.tokens }
    3.76 -                yield (token_style(chunk.kind, tok), tok.source)
    3.77 -              (styled_tokens, new Line_Context(Some(ctxt1)))
    3.78 -            case None =>
    3.79 -              val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
    3.80 -              (List(styled_token), new Line_Context(None))
    3.81 -          }
    3.82 -
    3.83 -        var offset = 0
    3.84 -        for ((style, token) <- styled_tokens) {
    3.85 -          val length = token.length
    3.86 -          val end_offset = offset + length
    3.87 -
    3.88 -          if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
    3.89 -            for (i <- offset until end_offset)
    3.90 -              handler.handleToken(line, style, i, 1, context1)
    3.91 -          }
    3.92 -          else handler.handleToken(line, style, offset, length, context1)
    3.93 -
    3.94 -          offset += length
    3.95 -        }
    3.96 -        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
    3.97 -        context1
    3.98 -      }
    3.99 -      val context2 = context1.intern
   3.100 -      handler.setLineContext(context2)
   3.101 -      context2
   3.102 -    }
   3.103 -  }
   3.104 -}
   3.105 -
     4.1 --- a/src/Tools/jEdit/src/context_menu.scala	Sun Oct 05 17:58:36 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/context_menu.scala	Sun Oct 05 18:14:26 2014 +0200
     4.3 @@ -75,7 +75,7 @@
     4.4        case text_area: TextArea =>
     4.5          text_area.getBuffer match {
     4.6            case buffer: Buffer
     4.7 -          if (Isabelle.is_bibtex(buffer) && buffer.isEditable) =>
     4.8 +          if (Bibtex_JEdit.check(buffer) && buffer.isEditable) =>
     4.9              val menu = new JMenu("BibTeX entries")
    4.10              for (entry <- Bibtex.entries) {
    4.11                val item = new JMenuItem(entry.kind)
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Oct 05 17:58:36 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Oct 05 18:14:26 2014 +0200
     5.3 @@ -163,7 +163,7 @@
     5.4  
     5.5    def bibtex_entries(): List[(String, Text.Offset)] =
     5.6      GUI_Thread.require {
     5.7 -      if (Isabelle.is_bibtex(buffer)) {
     5.8 +      if (Bibtex_JEdit.check(buffer)) {
     5.9          _bibtex match {
    5.10            case Some(entries) => entries
    5.11            case None =>
     6.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sun Oct 05 17:58:36 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sun Oct 05 18:14:26 2014 +0200
     6.3 @@ -64,17 +64,11 @@
     6.4      }
     6.5  
     6.6  
     6.7 -  /* buffer types */
     6.8 -
     6.9 -  def is_bibtex(buffer: Buffer): Boolean =
    6.10 -    JEdit_Lib.buffer_name(buffer).endsWith(".bib")
    6.11 -
    6.12 -
    6.13    /* token markers */
    6.14  
    6.15    private val markers: Map[String, TokenMarker] =
    6.16      Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*) +
    6.17 -      ("bibtex" -> new Bibtex_Token_Markup.Marker)
    6.18 +      ("bibtex" -> new Bibtex_JEdit.Token_Marker)
    6.19  
    6.20    def token_marker(name: String): Option[TokenMarker] = markers.get(name)
    6.21  
     7.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Oct 05 17:58:36 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Oct 05 18:14:26 2014 +0200
     7.3 @@ -242,40 +242,3 @@
     7.4    }
     7.5  }
     7.6  
     7.7 -
     7.8 -class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex")
     7.9 -{
    7.10 -  override def supportsCompletion = false
    7.11 -
    7.12 -  private class Asset(
    7.13 -      label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String)
    7.14 -    extends Isabelle_Sidekick.Asset(label, start, stop) {
    7.15 -      override def getShortString: String = label_html
    7.16 -      override def getLongString: String = source
    7.17 -    }
    7.18 -
    7.19 -  def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
    7.20 -  {
    7.21 -    val data = Isabelle_Sidekick.root_data(buffer)
    7.22 -
    7.23 -    try {
    7.24 -      var offset = 0
    7.25 -      for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
    7.26 -        val kind = chunk.kind
    7.27 -        val name = chunk.name
    7.28 -        val source = chunk.source
    7.29 -        if (kind != "") {
    7.30 -          val label = kind + (if (name == "") "" else " " + name)
    7.31 -          val label_html =
    7.32 -            "<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>"
    7.33 -          val asset = new Asset(label, label_html, offset, offset + source.size, source)
    7.34 -          data.root.add(new DefaultMutableTreeNode(asset))
    7.35 -        }
    7.36 -        offset += source.size
    7.37 -      }
    7.38 -      data
    7.39 -    }
    7.40 -    catch { case ERROR(_) => null }
    7.41 -  }
    7.42 -}
    7.43 -
     8.1 --- a/src/Tools/jEdit/src/services.xml	Sun Oct 05 17:58:36 2014 +0200
     8.2 +++ b/src/Tools/jEdit/src/services.xml	Sun Oct 05 18:14:26 2014 +0200
     8.3 @@ -27,7 +27,7 @@
     8.4      new isabelle.jedit.Isabelle_Sidekick_Root();
     8.5    </SERVICE>
     8.6    <SERVICE NAME="bibtex" CLASS="sidekick.SideKickParser">
     8.7 -    new isabelle.jedit.Isabelle_Sidekick_Bibtex();
     8.8 +    new isabelle.jedit.Bibtex_JEdit.Sidekick_Parser();
     8.9    </SERVICE>
    8.10    <SERVICE CLASS="console.Shell" NAME="Scala">
    8.11      new isabelle.jedit.Scala_Console();