--- a/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 15:29:24 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 15:48:37 2013 +0200
@@ -27,7 +27,7 @@
"isabelle-raw", // SideKick content tree
"isabelle-root") // session ROOT
- private lazy val news_syntax = Outer_Syntax.init()
+ private lazy val news_syntax = Outer_Syntax.init().no_tokens
def mode_syntax(name: String): Option[Outer_Syntax] =
name match {
@@ -44,11 +44,8 @@
/* 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))): _*)
+ Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)