--- 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 *)
--- 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);
--- 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"))))