# HG changeset patch
# User wenzelm
# Date 1459370141 -7200
# Node ID 77bbe5af41c362e75db0bd82157283ec70763a90
# Parent  dd2914250ca721fb6b6e18ee8a4b4223da87f443
more language markup;

diff -r dd2914250ca7 -r 77bbe5af41c3 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Mar 30 22:00:55 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Mar 30 22:35:41 2016 +0200
@@ -43,6 +43,7 @@
   val language_verbatim: bool -> T
   val language_rail: T
   val language_path: T
+  val language_mixfix: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val get_entity_kind: T -> string option
@@ -317,9 +318,11 @@
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
-val language_verbatim = language' {name = "verbatim", symbols = true, antiquotes = false};
+val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
 val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
+val language_mixfix =
+  language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
 
 
 (* formal entities *)
diff -r dd2914250ca7 -r 77bbe5af41c3 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 22:00:55 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 22:35:41 2016 +0200
@@ -190,6 +190,7 @@
 
 fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
   let
+    val _ = Position.report pos Markup.language_mixfix;
     val symbs0 = read_mfix sy;
 
     fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
diff -r dd2914250ca7 -r 77bbe5af41c3 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 30 22:00:55 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 30 22:35:41 2016 +0200
@@ -568,7 +568,8 @@
               else "breakpoint (disabled)"
             Some(add(prev, r, (true, XML.Text(text))))
           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
-            Some(add(prev, r, (true, XML.Text("language: " + language))))
+            val lang = Word.implode(Word.explode('_', language))
+            Some(add(prev, r, (true, XML.Text("language: " + lang))))
 
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
             Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))