# HG changeset patch
# User wenzelm
# Date 1377784117 -7200
# Node ID c63a016805b959c8418b4028f3cf9356c6d0b96c
# Parent  763d356973380219407a0a2b281dc9f2617ff0c4
explicit indication of outer syntax with no tokens;
uniform Isabelle.markers, based on syntax specification -- no tokens for NEWS;

diff -r 763d35697338 -r c63a016805b9 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Thu Aug 29 15:29:24 2013 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Aug 29 15:48:37 2013 +0200
@@ -42,7 +42,8 @@
 final class Outer_Syntax private(
   keywords: Map[String, (String, List[String])] = Map.empty,
   lexicon: Scan.Lexicon = Scan.Lexicon.empty,
-  val completion: Completion = Completion.empty)
+  val completion: Completion = Completion.empty,
+  val has_tokens: Boolean = true)
 {
   override def toString: String =
     (for ((name, (kind, files)) <- keywords) yield {
@@ -59,14 +60,19 @@
     (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
 
   def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
-    new Outer_Syntax(
-      keywords + (name -> kind),
-      lexicon + name,
+  {
+    val keywords1 = keywords + (name -> kind)
+    val lexicon1 = lexicon + name
+    val completion1 =
       if (Keyword.control(kind._1) || replace == Some("")) completion
-      else completion + (name, replace getOrElse name))
+      else completion + (name, replace getOrElse name)
+    new Outer_Syntax(keywords1, lexicon1, completion1, true)
+  }
 
-  def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, Some(name))
-  def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), Some(name))
+  def + (name: String, kind: (String, List[String])): Outer_Syntax =
+    this + (name, kind, Some(name))
+  def + (name: String, kind: String): Outer_Syntax =
+    this + (name, (kind, Nil), Some(name))
   def + (name: String, replace: Option[String]): Outer_Syntax =
     this + (name, (Keyword.MINOR, Nil), replace)
   def + (name: String): Outer_Syntax = this + (name, None)
@@ -106,7 +112,13 @@
     heading_level(command.name)
 
 
-  /* tokenize */
+  /* token language */
+
+  def no_tokens: Outer_Syntax =
+  {
+    require(keywords.isEmpty && lexicon.isEmpty)
+    new Outer_Syntax(completion = completion, has_tokens = false)
+  }
 
   def scan(input: Reader[Char]): List[Token] =
   {
diff -r 763d35697338 -r c63a016805b9 src/Tools/jEdit/src/isabelle.scala
--- 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)
 
diff -r 763d35697338 -r c63a016805b9 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 15:29:24 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 15:48:37 2013 +0200
@@ -220,16 +220,15 @@
 
       val context1 =
       {
-        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)
-            val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax.get, tok), tok))
-            (styled_tokens, new Line_Context(Some(ctxt1)))
-          }
-          else {
-            val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
-            (List((JEditToken.NULL, token)), new Line_Context(None))
+          Isabelle.mode_syntax(mode) match {
+            case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
+              val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+              val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax, tok), tok))
+              (styled_tokens, new Line_Context(Some(ctxt1)))
+            case _ =>
+              val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
+              (List((JEditToken.NULL, token)), new Line_Context(None))
           }
 
         val extended = extended_styles(line)