src/Tools/jEdit/src/token_markup.scala
changeset 53277 6aa348237973
parent 53274 1760c01f1c78
child 53278 c31532691e55
--- 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)
+    }
   }
 }