support more modes;

--- a/src/Tools/jEdit/src/isabelle.scala	Mon Jul 11 17:08:04 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Jul 11 17:45:51 2016 +0200
@@ -87,7 +87,11 @@
   /* text structure */
 
   def indent_rule(mode: String): Option[IndentRule] =
-    if (mode == "isabelle") Some(Text_Structure.Indent_Rule) else None
+    mode match {
+      case "isabelle" | "isabelle-options" | "isabelle-root" =>
+        Some(Text_Structure.Indent_Rule)
+      case _ => None
+    }
 
   def structure_matchers(mode: String): List[StructureMatcher] =
     if (mode == "isabelle") List(Text_Structure.Matcher) else Nil

--- a/src/Tools/jEdit/src/token_markup.scala	Mon Jul 11 17:08:04 2016 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Jul 11 17:45:51 2016 +0200
@@ -175,22 +175,23 @@
 
   /* line context */
 
-  private val context_rules = new ParserRuleSet("isabelle", "MAIN")
-
   object Line_Context
   {
-    val init = new Line_Context(Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
+    def init(mode: String): Line_Context =
+      new Line_Context(mode, Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
   }
 
   class Line_Context(
+      val mode: String,
       val context: Option[Scan.Line_Context],
       val structure: Outer_Syntax.Line_Structure)
-    extends TokenMarker.LineContext(context_rules, null)
+    extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
   {
-    override def hashCode: Int = (context, structure).hashCode
+    override def hashCode: Int = (mode, context, structure).hashCode
     override def equals(that: Any): Boolean =
       that match {
-        case other: Line_Context => context == other.context && structure == other.structure
+        case other: Line_Context =>
+          mode == other.mode && context == other.context && structure == other.structure
         case _ => false
       }
   }
@@ -205,7 +206,7 @@
       }
     context getOrElse {
       buffer.markTokens(line, DummyTokenHandler.INSTANCE)
-      context getOrElse Line_Context.init
+      context getOrElse Line_Context.init(JEdit_Lib.buffer_mode(buffer))
     }
   }
 
@@ -216,7 +217,7 @@
     : Option[List[Token]] =
   {
     val line_context =
-      if (line == 0) Line_Context.init
+      if (line == 0) Line_Context.init(JEdit_Lib.buffer_mode(buffer))
       else buffer_line_context(buffer, line - 1)
     for {
       ctxt <- line_context.context
@@ -381,7 +382,8 @@
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
       val line = if (raw_line == null) new Segment else raw_line
-      val line_context = context match { case c: Line_Context => c case _ => Line_Context.init }
+      val line_context =
+        context match { case c: Line_Context => c case _ => Line_Context.init(mode) }
       val structure = line_context.structure
 
       val context1 =
@@ -396,18 +398,18 @@
             case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
               val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
               val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
-              (styled_tokens, new Line_Context(Some(ctxt1), structure))
+              (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure))
 
             case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
               val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
               val structure1 = syntax.line_structure(tokens, structure)
               val styled_tokens =
                 tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
-              (styled_tokens, new Line_Context(Some(ctxt1), structure1))
+              (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))
 
             case _ =>
               val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
-              (List(styled_token), new Line_Context(None, structure))
+              (List(styled_token), new Line_Context(line_context.mode, None, structure))
           }
 
         val extended = extended_styles(line)