more uniform configuration of editor modes and token markers;
authorwenzelm
Thu Aug 29 13:53:45 2013 +0200 (2013-08-29)
changeset 532776aa348237973
parent 53276 cbed0aa0b0db
child 53278 c31532691e55
more uniform configuration of editor modes and token markers;
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 13:14:00 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 13:53:45 2013 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Tools/jEdit/src/isabelle.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Convenience operations for Isabelle/jEdit.
     1.8 +Global configuration and convenience operations for Isabelle/jEdit.
     1.9  */
    1.10  
    1.11  package isabelle.jedit
    1.12 @@ -18,20 +18,41 @@
    1.13  {
    1.14    /* editor modes */
    1.15  
    1.16 -  val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news")
    1.17 +  val modes =
    1.18 +    List(
    1.19 +      "isabelle",         // theory source
    1.20 +      "isabelle-news",    // NEWS
    1.21 +      "isabelle-options", // etc/options
    1.22 +      "isabelle-output",  // pretty text area output
    1.23 +      "isabelle-raw",     // SideKick content tree
    1.24 +      "isabelle-root")    // session ROOT
    1.25  
    1.26    private lazy val news_syntax = Outer_Syntax.init()
    1.27  
    1.28    def mode_syntax(name: String): Option[Outer_Syntax] =
    1.29      name match {
    1.30 -      case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax
    1.31 +      case "isabelle" | "isabelle-raw" =>
    1.32 +        val syntax = PIDE.session.recent_syntax
    1.33 +        if (syntax == Outer_Syntax.empty) None else Some(syntax)
    1.34        case "isabelle-options" => Some(Options.options_syntax)
    1.35        case "isabelle-root" => Some(Build.root_syntax)
    1.36        case "isabelle-news" => Some(news_syntax)
    1.37 +      case "isabelle-output" => None
    1.38        case _ => None
    1.39      }
    1.40  
    1.41  
    1.42 +  /* token markers */
    1.43 +
    1.44 +  private val marker_modes =
    1.45 +    List("isabelle", "isabelle-options", "isabelle-output", "isabelle-root")
    1.46 +
    1.47 +  private val markers =
    1.48 +    Map(marker_modes.map(name => (name, new Token_Markup.Marker(name))): _*)
    1.49 +
    1.50 +  def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
    1.51 +
    1.52 +
    1.53    /* dockable windows */
    1.54  
    1.55    private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 13:14:00 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 13:53:45 2013 +0200
     2.3 @@ -43,13 +43,6 @@
     2.4    def thy_load(): JEdit_Thy_Load =
     2.5      session.thy_load.asInstanceOf[JEdit_Thy_Load]
     2.6  
     2.7 -  def get_recent_syntax(): Option[Outer_Syntax] =
     2.8 -  {
     2.9 -    val current_session = session
    2.10 -    if (current_session.recent_syntax == Outer_Syntax.empty) None
    2.11 -    else Some(current_session.recent_syntax)
    2.12 -  }
    2.13 -
    2.14    lazy val editor = new JEdit_Editor
    2.15  
    2.16  
     3.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Aug 29 13:14:00 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Aug 29 13:53:45 2013 +0200
     3.3 @@ -196,7 +196,7 @@
     3.4    getPainter.setStructureHighlightEnabled(false)
     3.5    getPainter.setLineHighlightEnabled(false)
     3.6  
     3.7 -  getBuffer.setTokenMarker(new Token_Markup.Marker(true, None))
     3.8 +  getBuffer.setTokenMarker(Isabelle.token_marker("isabelle-output").get)
     3.9    getBuffer.setReadOnly(true)
    3.10    getBuffer.setStringProperty("noWordSep", "_'.?")
    3.11  
     4.1 --- a/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 13:14:00 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 13:53:45 2013 +0200
     4.3 @@ -206,8 +206,10 @@
     4.4        }
     4.5    }
     4.6  
     4.7 -  class Marker(ext_styles: Boolean, get_syntax: => Option[Outer_Syntax]) extends TokenMarker
     4.8 +  class Marker(mode: String) extends TokenMarker
     4.9    {
    4.10 +    private val ext_styles = mode == "isabelle"
    4.11 +
    4.12      override def markTokens(context: TokenMarker.LineContext,
    4.13          handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
    4.14      {
    4.15 @@ -220,7 +222,7 @@
    4.16  
    4.17        val context1 =
    4.18        {
    4.19 -        val syntax = get_syntax
    4.20 +        val syntax = Isabelle.mode_syntax(mode)
    4.21          val (styled_tokens, context1) =
    4.22            if (line_ctxt.isDefined && syntax.isDefined) {
    4.23              val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
    4.24 @@ -266,11 +268,6 @@
    4.25  
    4.26    /* mode provider */
    4.27  
    4.28 -  private val markers = Map(
    4.29 -    "isabelle" -> new Token_Markup.Marker(true, PIDE.get_recent_syntax()),
    4.30 -    "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
    4.31 -    "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
    4.32 -
    4.33    class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
    4.34    {
    4.35      for (mode <- orig_provider.getModes) addMode(mode)
    4.36 @@ -278,15 +275,18 @@
    4.37      override def loadMode(mode: Mode, xmh: XModeHandler)
    4.38      {
    4.39        super.loadMode(mode, xmh)
    4.40 -      markers.get(mode.getName).map(mode.setTokenMarker(_))
    4.41 +      Isabelle.token_marker(mode.getName).foreach(mode.setTokenMarker _)
    4.42      }
    4.43    }
    4.44  
    4.45    def refresh_buffer(buffer: JEditBuffer)
    4.46    {
    4.47 -    buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
    4.48 -    val marker = markers.get(JEdit_Lib.buffer_mode(buffer))
    4.49 -    marker.map(buffer.setTokenMarker(_))
    4.50 +    Isabelle.token_marker(JEdit_Lib.buffer_mode(buffer)) match {
    4.51 +      case None =>
    4.52 +      case Some(marker) =>
    4.53 +        buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
    4.54 +        buffer.setTokenMarker(marker)
    4.55 +    }
    4.56    }
    4.57  }
    4.58