more language markup;
authorwenzelm
Wed Mar 30 22:35:41 2016 +0200 (2016-03-30)
changeset 6277277bbe5af41c3
parent 62771 dd2914250ca7
child 62773 e6443edaebff
more language markup;
src/Pure/PIDE/markup.ML
src/Pure/Syntax/syntax_ext.ML
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Wed Mar 30 22:00:55 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Wed Mar 30 22:35:41 2016 +0200
     1.3 @@ -43,6 +43,7 @@
     1.4    val language_verbatim: bool -> T
     1.5    val language_rail: T
     1.6    val language_path: T
     1.7 +  val language_mixfix: T
     1.8    val bindingN: string val binding: T
     1.9    val entityN: string val entity: string -> string -> T
    1.10    val get_entity_kind: T -> string option
    1.11 @@ -317,9 +318,11 @@
    1.12  val language_antiquotation =
    1.13    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
    1.14  val language_text = language' {name = "text", symbols = true, antiquotes = false};
    1.15 -val language_verbatim = language' {name = "verbatim", symbols = true, antiquotes = false};
    1.16 +val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
    1.17  val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
    1.18  val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
    1.19 +val language_mixfix =
    1.20 +  language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
    1.21  
    1.22  
    1.23  (* formal entities *)
     2.1 --- a/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 22:00:55 2016 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 22:35:41 2016 +0200
     2.3 @@ -190,6 +190,7 @@
     2.4  
     2.5  fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
     2.6    let
     2.7 +    val _ = Position.report pos Markup.language_mixfix;
     2.8      val symbs0 = read_mfix sy;
     2.9  
    2.10      fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 30 22:00:55 2016 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 30 22:35:41 2016 +0200
     3.3 @@ -568,7 +568,8 @@
     3.4                else "breakpoint (disabled)"
     3.5              Some(add(prev, r, (true, XML.Text(text))))
     3.6            case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
     3.7 -            Some(add(prev, r, (true, XML.Text("language: " + language))))
     3.8 +            val lang = Word.implode(Word.explode('_', language))
     3.9 +            Some(add(prev, r, (true, XML.Text("language: " + lang))))
    3.10  
    3.11            case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
    3.12              Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))