default completion context via outer syntax;
no symbol completion for ML files;
tuned;

--- a/src/Pure/Isar/outer_syntax.scala	Thu Feb 20 12:53:12 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Feb 20 13:23:49 2014 +0100
@@ -43,6 +43,7 @@
   keywords: Map[String, (String, List[String])] = Map.empty,
   lexicon: Scan.Lexicon = Scan.Lexicon.empty,
   val completion: Completion = Completion.empty,
+  val completion_context: Completion.Context = Completion.Context.default,
   val has_tokens: Boolean = true)
 {
   override def toString: String =
@@ -72,7 +73,7 @@
     val completion1 =
       if (Keyword.control(kind._1) || replace == Some("")) completion
       else completion + (name, replace getOrElse name)
-    new Outer_Syntax(keywords1, lexicon1, completion1, true)
+    new Outer_Syntax(keywords1, lexicon1, completion1, completion_context, true)
   }
 
   def + (name: String, kind: (String, List[String])): Outer_Syntax =
@@ -120,15 +121,10 @@
 
   /* 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] =
   {
-    Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
+    Token.Parsers.parseAll(
+        Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
       case Token.Parsers.Success(tokens, _) => tokens
       case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
     }
@@ -151,4 +147,19 @@
     }
     (toks.toList, ctxt)
   }
+
+
+  /* language context */
+
+  def set_completion_context(context: Completion.Context): Outer_Syntax =
+    new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
+
+  def no_tokens: Outer_Syntax =
+  {
+    require(keywords.isEmpty && lexicon.isEmpty)
+    new Outer_Syntax(
+      completion = completion,
+      completion_context = completion_context,
+      has_tokens = false)
+  }
 }

--- a/src/Pure/PIDE/markup.scala	Thu Feb 20 12:53:12 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Feb 20 13:23:49 2014 +0100
@@ -93,6 +93,9 @@
   val LANGUAGE = "language"
   object Language
   {
+    val ML = "ML"
+    val UNKNOWN = "unknown"
+
     def unapply(markup: Markup): Option[(String, Boolean)] =
       markup match {
         case Markup(LANGUAGE, props) =>

--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Feb 20 12:53:12 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Feb 20 13:23:49 2014 +0100
@@ -111,10 +111,11 @@
             val history = PIDE.completion_history.value
             val decode = Isabelle_Encoding.is_active(buffer)
             val context =
-              PIDE.document_view(text_area) match {
-                case None => Completion.Context.default
+              (PIDE.document_view(text_area) match {
+                case None => None
                 case Some(doc_view) => doc_view.get_rendering().completion_context(caret)
-              }
+              }) getOrElse syntax.completion_context
+
             syntax.completion.complete(history, decode, explicit, text, context) match {
               case Some(result) =>
                 if (result.unique && result.items.head.immediate && immediate)
@@ -283,7 +284,7 @@
           val text = text_field.getText.substring(0, caret)
 
           syntax.completion.complete(
-              history, decode = true, explicit = false, text, Completion.Context.default) match {
+              history, decode = true, explicit = false, text, syntax.completion_context) match {
             case Some(result) =>
               val fm = text_field.getFontMetrics(text_field.getFont)
               val loc =

--- a/src/Tools/jEdit/src/isabelle.scala	Thu Feb 20 12:53:12 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Feb 20 13:23:49 2014 +0100
@@ -31,7 +31,12 @@
       "isabelle-output",  // pretty text area output
       "isabelle-root")    // session ROOT
 
-  private lazy val symbols_syntax = Outer_Syntax.init().no_tokens
+  private lazy val ml_syntax: Outer_Syntax =
+    Outer_Syntax.init().no_tokens.
+      set_completion_context(Completion.Context(Markup.Language.ML, false))
+
+  private lazy val news_syntax: Outer_Syntax =
+    Outer_Syntax.init().no_tokens
 
   def mode_syntax(name: String): Option[Outer_Syntax] =
     name match {
@@ -40,7 +45,8 @@
         if (syntax == Outer_Syntax.empty) None else Some(syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Build.root_syntax)
-      case "isabelle-ml" | "isabelle-news" => Some(symbols_syntax)
+      case "isabelle-ml" => Some(ml_syntax)
+      case "isabelle-news" => Some(news_syntax)
       case "isabelle-output" => None
       case _ => None
     }

--- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 12:53:12 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 13:23:49 2014 +0100
@@ -206,7 +206,7 @@
     Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
       Markup.COMMENT, Markup.LANGUAGE)
 
-  def completion_context(caret: Text.Offset): Completion.Context =
+  def completion_context(caret: Text.Offset): Option[Completion.Context] =
     if (caret > 0) {
       val result =
         snapshot.select_markup(Text.Range(caret - 1, caret + 1), Some(completion_elements), _ =>
@@ -214,15 +214,16 @@
             case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
               Some(Completion.Context(language, symbols))
             case Text.Info(_, XML.Elem(markup, _)) =>
-              if (completion_elements(markup.name)) Some(Completion.Context("unknown", true))
+              if (completion_elements(markup.name))
+                Some(Completion.Context(Markup.Language.UNKNOWN, true))
               else None
           })
       result match {
-        case Text.Info(_, context) :: _ => context
-        case Nil => Completion.Context.default
+        case Text.Info(_, context) :: _ => Some(context)
+        case Nil => None
       }
     }
-    else Completion.Context.default
+    else None
 
 
   /* command overview */