more token markers, based on actual outer syntax;
prefer official Outer_Syntax.init with its completions;

--- a/src/Pure/System/build.scala	Tue Aug 07 19:16:58 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Aug 07 20:28:35 2012 +0200
@@ -163,19 +163,19 @@
 
   /* parser */
 
+  private val SESSION = "session"
+  private val IN = "in"
+  private val DESCRIPTION = "description"
+  private val OPTIONS = "options"
+  private val THEORIES = "theories"
+  private val FILES = "files"
+
+  lazy val root_syntax =
+    Outer_Syntax.init() + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+      SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
+
   private object Parser extends Parse.Parser
   {
-    val SESSION = "session"
-    val IN = "in"
-    val DESCRIPTION = "description"
-    val OPTIONS = "options"
-    val THEORIES = "theories"
-    val FILES = "files"
-
-    val syntax =
-      Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-        SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
-
     def session_entry(pos: Position.T): Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
@@ -202,7 +202,7 @@
 
     def parse_entries(root: Path): List[Session_Entry] =
     {
-      val toks = syntax.scan(File.read(root))
+      val toks = root_syntax.scan(File.read(root))
       parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)

--- a/src/Pure/System/options.scala	Tue Aug 07 19:16:58 2012 +0200
+++ b/src/Pure/System/options.scala	Tue Aug 07 20:28:35 2012 +0200
@@ -30,13 +30,13 @@
 
   /* parsing */
 
+  private val DECLARE = "declare"
+  private val DEFINE = "define"
+
+  lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + DECLARE + DEFINE
+
   private object Parser extends Parse.Parser
   {
-    val DECLARE = "declare"
-    val DEFINE = "define"
-
-    val syntax = Outer_Syntax.empty + ":" + "=" + "--" + DECLARE + DEFINE
-
     val entry: Parser[Options => Options] =
     {
       val option_name = atom("option name", _.is_xname)
@@ -56,7 +56,8 @@
 
     def parse_entries(file: Path): List[Options => Options] =
     {
-      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.implode)) match {
+      val toks = options_syntax.scan(File.read(file))
+      parse_all(rep(entry), Token.reader(toks, file.implode)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }

--- a/src/Pure/System/session.scala	Tue Aug 07 19:16:58 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 07 20:28:35 2012 +0200
@@ -125,7 +125,7 @@
 
   /* global state */
 
-  @volatile private var base_syntax = Outer_Syntax.empty
+  @volatile private var base_syntax = Outer_Syntax.init()
 
   private val syslog = Volatile(Queue.empty[XML.Elem])
   def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
@@ -148,6 +148,9 @@
     if (version.is_init) base_syntax
     else version.syntax
   }
+  def get_recent_syntax(): Option[Outer_Syntax] =
+    if (is_ready) Some(recent_syntax)
+    else None
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =

--- a/src/Tools/jEdit/src/modes/isabelle-options.xml	Tue Aug 07 19:16:58 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml	Tue Aug 07 20:28:35 2012 +0200
@@ -4,34 +4,10 @@
 <!-- Isabelle options mode -->
 <MODE>
   <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
-  <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
-    <SPAN TYPE="COMMENT1">
-      <BEGIN>(*</BEGIN>
-      <END>*)</END>
-    </SPAN>
-    <SPAN TYPE="COMMENT3">
-      <BEGIN>{*</BEGIN>
-      <END>*}</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL2">
-      <BEGIN>`</BEGIN>
-      <END>`</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL1">
-      <BEGIN>"</BEGIN>
-      <END>"</END>
-    </SPAN>
-    <KEYWORDS>
-      <KEYWORD1>declare</KEYWORD1>
-      <KEYWORD2>define</KEYWORD2>
-    </KEYWORDS>
-  </RULES>
 </MODE>

--- a/src/Tools/jEdit/src/modes/isabelle-root.xml	Tue Aug 07 19:16:58 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml	Tue Aug 07 20:28:35 2012 +0200
@@ -4,38 +4,10 @@
 <!-- Isabelle session root mode -->
 <MODE>
   <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
-  <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
-    <SPAN TYPE="COMMENT1">
-      <BEGIN>(*</BEGIN>
-      <END>*)</END>
-    </SPAN>
-    <SPAN TYPE="COMMENT3">
-      <BEGIN>{*</BEGIN>
-      <END>*}</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL2">
-      <BEGIN>`</BEGIN>
-      <END>`</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL1">
-      <BEGIN>"</BEGIN>
-      <END>"</END>
-    </SPAN>
-    <KEYWORDS>
-      <KEYWORD1>session</KEYWORD1>
-      <KEYWORD2>in</KEYWORD2>
-      <KEYWORD2>description</KEYWORD2>
-      <KEYWORD2>files</KEYWORD2>
-      <KEYWORD2>options</KEYWORD2>
-      <KEYWORD2>theories</KEYWORD2>
-    </KEYWORDS>
-  </RULES>
 </MODE>

--- a/src/Tools/jEdit/src/token_markup.scala	Tue Aug 07 19:16:58 2012 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Aug 07 20:28:35 2012 +0200
@@ -162,7 +162,7 @@
       }
   }
 
-  class Marker extends TokenMarker
+  class Marker(ext_styles: Boolean, get_syntax: => Option[Outer_Syntax]) extends TokenMarker
   {
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
@@ -176,12 +176,12 @@
 
       val context1 =
       {
+        val syntax = get_syntax
         val (styled_tokens, context1) =
-          if (line_ctxt.isDefined && Isabelle.session.is_ready) {
-            val syntax = Isabelle.session.recent_syntax()
-            val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+          if (line_ctxt.isDefined && syntax.isDefined) {
+            val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
             val styled_tokens =
-              tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))
+              tokens.map(tok => (Isabelle_Rendering.token_markup(syntax.get, tok), tok))
             (styled_tokens, new Line_Context(Some(ctxt1)))
           }
           else {
@@ -189,7 +189,9 @@
             (List((JEditToken.NULL, token)), new Line_Context(None))
           }
 
-        val extended = extended_styles(line)
+        val extended =
+          if (ext_styles) extended_styles(line)
+          else Map.empty[Text.Offset, Byte => Byte]
 
         var offset = 0
         for ((style, token) <- styled_tokens) {
@@ -221,7 +223,10 @@
 
   /* mode provider */
 
-  private val isabelle_token_marker = new Token_Markup.Marker
+  private val markers = Map(
+    "isabelle" -> new Token_Markup.Marker(true, Isabelle.session.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
   {
@@ -230,15 +235,14 @@
     override def loadMode(mode: Mode, xmh: XModeHandler)
     {
       super.loadMode(mode, xmh)
-      if (mode.getName == "isabelle")
-        mode.setTokenMarker(isabelle_token_marker)
+      markers.get(mode.getName).map(mode.setTokenMarker(_))
     }
   }
 
   def refresh_buffer(buffer: JEditBuffer)
   {
     buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
-    buffer.setTokenMarker(isabelle_token_marker)
+    markers.get(buffer.getMode.getName).map(buffer.setTokenMarker(_))
   }
 }