generic markup for embedded languages;

--- a/src/Pure/ML/ml_lex.ML	Tue Feb 18 15:38:50 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Tue Feb 18 16:34:02 2014 +0100
@@ -300,7 +300,7 @@
 
 fun read pos txt =
   let
-    val _ = Position.report pos Markup.ML_source;
+    val _ = Position.report pos Markup.language_ML;
     val syms = Symbol_Pos.explode (txt, pos);
     val termination =
       if null syms then []

--- a/src/Pure/PIDE/markup.ML	Tue Feb 18 15:38:50 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 18 16:34:02 2014 +0100
@@ -20,6 +20,13 @@
   val name: string -> T -> T
   val kindN: string
   val instanceN: string
+  val languageN: string val language: string -> T
+  val language_sort: T
+  val language_type: T
+  val language_term: T
+  val language_prop: T
+  val language_ML: T
+  val language_document: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val get_entity_kind: T -> string option
@@ -62,10 +69,6 @@
   val inner_cartoucheN: string val inner_cartouche: T
   val inner_commentN: string val inner_comment: T
   val token_rangeN: string val token_range: T
-  val sortN: string val sort: T
-  val typN: string val typ: T
-  val termN: string val term: T
-  val propN: string val prop: T
   val sortingN: string val sorting: T
   val typingN: string val typing: T
   val ML_keyword1N: string val ML_keyword1: T
@@ -81,8 +84,6 @@
   val ML_openN: string
   val ML_structN: string
   val ML_typingN: string val ML_typing: T
-  val ML_sourceN: string val ML_source: T
-  val document_sourceN: string val document_source: T
   val antiquotedN: string val antiquoted: T
   val antiquoteN: string val antiquote: T
   val ML_antiquotationN: string
@@ -235,6 +236,19 @@
 val instanceN = "instance";
 
 
+(* embedded languages *)
+
+val (languageN, language) = markup_string "language" nameN;
+
+val language_sort = language "sort";
+val language_type = language "type";
+val language_term = language "term";
+val language_prop = language "prop";
+
+val language_ML = language "ML";
+val language_document = language "document";
+
+
 (* formal entities *)
 
 val (bindingN, binding) = markup_elem "binding";
@@ -317,11 +331,6 @@
 
 val (token_rangeN, token_range) = markup_elem "token_range";
 
-val (sortN, sort) = markup_elem "sort";
-val (typN, typ) = markup_elem "typ";
-val (termN, term) = markup_elem "term";
-val (propN, prop) = markup_elem "prop";
-
 val (sortingN, sorting) = markup_elem "sorting";
 val (typingN, typing) = markup_elem "typing";
 
@@ -344,10 +353,7 @@
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
 
-(* embedded source text *)
-
-val (ML_sourceN, ML_source) = markup_elem "ML_source";
-val (document_sourceN, document_source) = markup_elem "document_source";
+(* antiquotations *)
 
 val (antiquotedN, antiquoted) = markup_elem "antiquoted";
 val (antiquoteN, antiquote) = markup_elem "antiquote";

--- a/src/Pure/PIDE/markup.scala	Tue Feb 18 15:38:50 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 16:34:02 2014 +0100
@@ -67,6 +67,20 @@
   val POSITION = "position"
 
 
+  /* embedded languages */
+
+  val LANGUAGE = "language"
+
+  object Language
+  {
+    def unapply(markup: Markup): Option[String] =
+      markup match {
+        case Markup(LANGUAGE, Name(name)) => Some(name)
+        case _ => None
+      }
+  }
+
+
   /* external resources */
 
   val PATH = "path"
@@ -138,11 +152,6 @@
 
   val TOKEN_RANGE = "token_range"
 
-  val SORT = "sort"
-  val TYP = "typ"
-  val TERM = "term"
-  val PROP = "prop"
-
   val SORTING = "sorting"
   val TYPING = "typing"
 
@@ -150,10 +159,7 @@
   val METHOD = "method"
 
 
-  /* embedded source text */
-
-  val ML_SOURCE = "ML_source"
-  val DOCUMENT_SOURCE = "document_source"
+  /* antiquotations */
 
   val ANTIQUOTED = "antiquoted"
   val ANTIQUOTE = "antiquote"

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Feb 18 15:38:50 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Feb 18 16:34:02 2014 +0100
@@ -342,7 +342,7 @@
     Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
 fun parse_sort ctxt =
-  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
+  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
     (fn (syms, pos) =>
       parse_tree ctxt "sort" (syms, pos)
       |> uncurry (report_result ctxt pos)
@@ -351,7 +351,7 @@
       handle ERROR msg => parse_failed ctxt pos msg "sort");
 
 fun parse_typ ctxt =
-  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
+  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type
     (fn (syms, pos) =>
       parse_tree ctxt "type" (syms, pos)
       |> uncurry (report_result ctxt pos)
@@ -362,8 +362,8 @@
   let
     val (markup, kind, root, constrain) =
       if is_prop
-      then (Markup.prop, "proposition", "prop", Type.constraint propT)
-      else (Markup.term, "term", Config.get ctxt Syntax.root, I);
+      then (Markup.language_prop, "prop", "prop", Type.constraint propT)
+      else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
     val decode = constrain o Term_XML.Decode.term;
   in
     Syntax.parse_token ctxt decode markup
@@ -749,8 +749,8 @@
 
 in
 
-val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
-val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
+val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort;
+val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type;
 
 fun unparse_term ctxt =
   let
@@ -760,7 +760,7 @@
   in
     unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
-      Markup.term ctxt
+      Markup.language_term ctxt
   end;
 
 end;

--- a/src/Pure/Thy/thy_output.ML	Tue Feb 18 15:38:50 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Feb 18 16:34:02 2014 +0100
@@ -188,7 +188,7 @@
 
 
 fun check_text (txt, pos) state =
- (Position.report pos Markup.document_source;
+ (Position.report pos Markup.language_document;
   if Toplevel.is_skipped_proof state then ()
   else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
 

--- a/src/Tools/jEdit/src/rendering.scala	Tue Feb 18 15:38:50 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Feb 18 16:34:02 2014 +0100
@@ -241,10 +241,10 @@
   /* markup selectors */
 
   private val highlight_include =
-    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
-      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE,
-      Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE,
-      Markup.DOCUMENT_SOURCE)
+    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
+      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
+      Markup.VAR, Markup.TFREE, Markup.TVAR)
 
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   {
@@ -375,23 +375,18 @@
 
   private val tooltips: Map[String, String] =
     Map(
-      Markup.SORT -> "sort",
-      Markup.TYP -> "type",
-      Markup.TERM -> "term",
-      Markup.PROP -> "proposition",
       Markup.TOKEN_RANGE -> "inner syntax token",
       Markup.FREE -> "free variable",
       Markup.SKOLEM -> "skolem variable",
       Markup.BOUND -> "bound variable",
       Markup.VAR -> "schematic variable",
       Markup.TFREE -> "free type variable",
-      Markup.TVAR -> "schematic type variable",
-      Markup.ML_SOURCE -> "ML source",
-      Markup.DOCUMENT_SOURCE -> "document source")
+      Markup.TVAR -> "schematic type variable")
 
   private val tooltip_elements =
-    Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
-      Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys
+    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
+      tooltips.keys
 
   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
     Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
@@ -434,6 +429,8 @@
             Some(add(prev, r, (true, pretty_typing("::", body))))
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
             Some(add(prev, r, (false, pretty_typing("ML:", body))))
+          case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) =>
+            Some(add(prev, r, (true, XML.Text("language: " + name))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
             if (tooltips.isDefinedAt(name))
               Some(add(prev, r, (true, XML.Text(tooltips(name)))))