# HG changeset patch
# User wenzelm
# Date 1377777225 -7200
# Node ID 6aa348237973a35ea0243a41751e8c47776b2905
# Parent  cbed0aa0b0db6f7fd8ff278c7db8380d6f297b22
more uniform configuration of editor modes and token markers;

diff -r cbed0aa0b0db -r 6aa348237973 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 13:14:00 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 13:53:45 2013 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/isabelle.scala
     Author:     Makarius
 
-Convenience operations for Isabelle/jEdit.
+Global configuration and convenience operations for Isabelle/jEdit.
 */
 
 package isabelle.jedit
@@ -18,20 +18,41 @@
 {
   /* editor modes */
 
-  val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news")
+  val modes =
+    List(
+      "isabelle",         // theory source
+      "isabelle-news",    // NEWS
+      "isabelle-options", // etc/options
+      "isabelle-output",  // pretty text area output
+      "isabelle-raw",     // SideKick content tree
+      "isabelle-root")    // session ROOT
 
   private lazy val news_syntax = Outer_Syntax.init()
 
   def mode_syntax(name: String): Option[Outer_Syntax] =
     name match {
-      case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax
+      case "isabelle" | "isabelle-raw" =>
+        val syntax = PIDE.session.recent_syntax
+        if (syntax == Outer_Syntax.empty) None else Some(syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Build.root_syntax)
       case "isabelle-news" => Some(news_syntax)
+      case "isabelle-output" => None
       case _ => None
     }
 
 
+  /* token markers */
+
+  private val marker_modes =
+    List("isabelle", "isabelle-options", "isabelle-output", "isabelle-root")
+
+  private val markers =
+    Map(marker_modes.map(name => (name, new Token_Markup.Marker(name))): _*)
+
+  def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
+
+
   /* dockable windows */
 
   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
diff -r cbed0aa0b0db -r 6aa348237973 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 13:14:00 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 13:53:45 2013 +0200
@@ -43,13 +43,6 @@
   def thy_load(): JEdit_Thy_Load =
     session.thy_load.asInstanceOf[JEdit_Thy_Load]
 
-  def get_recent_syntax(): Option[Outer_Syntax] =
-  {
-    val current_session = session
-    if (current_session.recent_syntax == Outer_Syntax.empty) None
-    else Some(current_session.recent_syntax)
-  }
-
   lazy val editor = new JEdit_Editor
 
 
diff -r cbed0aa0b0db -r 6aa348237973 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Aug 29 13:14:00 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Aug 29 13:53:45 2013 +0200
@@ -196,7 +196,7 @@
   getPainter.setStructureHighlightEnabled(false)
   getPainter.setLineHighlightEnabled(false)
 
-  getBuffer.setTokenMarker(new Token_Markup.Marker(true, None))
+  getBuffer.setTokenMarker(Isabelle.token_marker("isabelle-output").get)
   getBuffer.setReadOnly(true)
   getBuffer.setStringProperty("noWordSep", "_'.?")
 
diff -r cbed0aa0b0db -r 6aa348237973 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 13:14:00 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 13:53:45 2013 +0200
@@ -206,8 +206,10 @@
       }
   }
 
-  class Marker(ext_styles: Boolean, get_syntax: => Option[Outer_Syntax]) extends TokenMarker
+  class Marker(mode: String) extends TokenMarker
   {
+    private val ext_styles = mode == "isabelle"
+
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
@@ -220,7 +222,7 @@
 
       val context1 =
       {
-        val syntax = get_syntax
+        val syntax = Isabelle.mode_syntax(mode)
         val (styled_tokens, context1) =
           if (line_ctxt.isDefined && syntax.isDefined) {
             val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
@@ -266,11 +268,6 @@
 
   /* mode provider */
 
-  private val markers = Map(
-    "isabelle" -> new Token_Markup.Marker(true, PIDE.get_recent_syntax()),
-    "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
-    "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
-
   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   {
     for (mode <- orig_provider.getModes) addMode(mode)
@@ -278,15 +275,18 @@
     override def loadMode(mode: Mode, xmh: XModeHandler)
     {
       super.loadMode(mode, xmh)
-      markers.get(mode.getName).map(mode.setTokenMarker(_))
+      Isabelle.token_marker(mode.getName).foreach(mode.setTokenMarker _)
     }
   }
 
   def refresh_buffer(buffer: JEditBuffer)
   {
-    buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
-    val marker = markers.get(JEdit_Lib.buffer_mode(buffer))
-    marker.map(buffer.setTokenMarker(_))
+    Isabelle.token_marker(JEdit_Lib.buffer_mode(buffer)) match {
+      case None =>
+      case Some(marker) =>
+        buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
+        buffer.setTokenMarker(marker)
+    }
   }
 }