generic markup for embedded languages;
authorwenzelm
Tue Feb 18 16:34:02 2014 +0100 (2014-02-18 ago)
changeset 55552bcc643ac071a
parent 55551 5c40782f68b3
child 55553 4a5f65df29fa
generic markup for embedded languages;
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/thy_output.ML
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/ML/ml_lex.ML	Tue Feb 18 15:38:50 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Tue Feb 18 16:34:02 2014 +0100
     1.3 @@ -300,7 +300,7 @@
     1.4  
     1.5  fun read pos txt =
     1.6    let
     1.7 -    val _ = Position.report pos Markup.ML_source;
     1.8 +    val _ = Position.report pos Markup.language_ML;
     1.9      val syms = Symbol_Pos.explode (txt, pos);
    1.10      val termination =
    1.11        if null syms then []
     2.1 --- a/src/Pure/PIDE/markup.ML	Tue Feb 18 15:38:50 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Tue Feb 18 16:34:02 2014 +0100
     2.3 @@ -20,6 +20,13 @@
     2.4    val name: string -> T -> T
     2.5    val kindN: string
     2.6    val instanceN: string
     2.7 +  val languageN: string val language: string -> T
     2.8 +  val language_sort: T
     2.9 +  val language_type: T
    2.10 +  val language_term: T
    2.11 +  val language_prop: T
    2.12 +  val language_ML: T
    2.13 +  val language_document: T
    2.14    val bindingN: string val binding: T
    2.15    val entityN: string val entity: string -> string -> T
    2.16    val get_entity_kind: T -> string option
    2.17 @@ -62,10 +69,6 @@
    2.18    val inner_cartoucheN: string val inner_cartouche: T
    2.19    val inner_commentN: string val inner_comment: T
    2.20    val token_rangeN: string val token_range: T
    2.21 -  val sortN: string val sort: T
    2.22 -  val typN: string val typ: T
    2.23 -  val termN: string val term: T
    2.24 -  val propN: string val prop: T
    2.25    val sortingN: string val sorting: T
    2.26    val typingN: string val typing: T
    2.27    val ML_keyword1N: string val ML_keyword1: T
    2.28 @@ -81,8 +84,6 @@
    2.29    val ML_openN: string
    2.30    val ML_structN: string
    2.31    val ML_typingN: string val ML_typing: T
    2.32 -  val ML_sourceN: string val ML_source: T
    2.33 -  val document_sourceN: string val document_source: T
    2.34    val antiquotedN: string val antiquoted: T
    2.35    val antiquoteN: string val antiquote: T
    2.36    val ML_antiquotationN: string
    2.37 @@ -235,6 +236,19 @@
    2.38  val instanceN = "instance";
    2.39  
    2.40  
    2.41 +(* embedded languages *)
    2.42 +
    2.43 +val (languageN, language) = markup_string "language" nameN;
    2.44 +
    2.45 +val language_sort = language "sort";
    2.46 +val language_type = language "type";
    2.47 +val language_term = language "term";
    2.48 +val language_prop = language "prop";
    2.49 +
    2.50 +val language_ML = language "ML";
    2.51 +val language_document = language "document";
    2.52 +
    2.53 +
    2.54  (* formal entities *)
    2.55  
    2.56  val (bindingN, binding) = markup_elem "binding";
    2.57 @@ -317,11 +331,6 @@
    2.58  
    2.59  val (token_rangeN, token_range) = markup_elem "token_range";
    2.60  
    2.61 -val (sortN, sort) = markup_elem "sort";
    2.62 -val (typN, typ) = markup_elem "typ";
    2.63 -val (termN, term) = markup_elem "term";
    2.64 -val (propN, prop) = markup_elem "prop";
    2.65 -
    2.66  val (sortingN, sorting) = markup_elem "sorting";
    2.67  val (typingN, typing) = markup_elem "typing";
    2.68  
    2.69 @@ -344,10 +353,7 @@
    2.70  val (ML_typingN, ML_typing) = markup_elem "ML_typing";
    2.71  
    2.72  
    2.73 -(* embedded source text *)
    2.74 -
    2.75 -val (ML_sourceN, ML_source) = markup_elem "ML_source";
    2.76 -val (document_sourceN, document_source) = markup_elem "document_source";
    2.77 +(* antiquotations *)
    2.78  
    2.79  val (antiquotedN, antiquoted) = markup_elem "antiquoted";
    2.80  val (antiquoteN, antiquote) = markup_elem "antiquote";
     3.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 18 15:38:50 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 16:34:02 2014 +0100
     3.3 @@ -67,6 +67,20 @@
     3.4    val POSITION = "position"
     3.5  
     3.6  
     3.7 +  /* embedded languages */
     3.8 +
     3.9 +  val LANGUAGE = "language"
    3.10 +
    3.11 +  object Language
    3.12 +  {
    3.13 +    def unapply(markup: Markup): Option[String] =
    3.14 +      markup match {
    3.15 +        case Markup(LANGUAGE, Name(name)) => Some(name)
    3.16 +        case _ => None
    3.17 +      }
    3.18 +  }
    3.19 +
    3.20 +
    3.21    /* external resources */
    3.22  
    3.23    val PATH = "path"
    3.24 @@ -138,11 +152,6 @@
    3.25  
    3.26    val TOKEN_RANGE = "token_range"
    3.27  
    3.28 -  val SORT = "sort"
    3.29 -  val TYP = "typ"
    3.30 -  val TERM = "term"
    3.31 -  val PROP = "prop"
    3.32 -
    3.33    val SORTING = "sorting"
    3.34    val TYPING = "typing"
    3.35  
    3.36 @@ -150,10 +159,7 @@
    3.37    val METHOD = "method"
    3.38  
    3.39  
    3.40 -  /* embedded source text */
    3.41 -
    3.42 -  val ML_SOURCE = "ML_source"
    3.43 -  val DOCUMENT_SOURCE = "document_source"
    3.44 +  /* antiquotations */
    3.45  
    3.46    val ANTIQUOTED = "antiquoted"
    3.47    val ANTIQUOTE = "antiquote"
     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Feb 18 15:38:50 2014 +0100
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue Feb 18 16:34:02 2014 +0100
     4.3 @@ -342,7 +342,7 @@
     4.4      Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
     4.5  
     4.6  fun parse_sort ctxt =
     4.7 -  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
     4.8 +  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
     4.9      (fn (syms, pos) =>
    4.10        parse_tree ctxt "sort" (syms, pos)
    4.11        |> uncurry (report_result ctxt pos)
    4.12 @@ -351,7 +351,7 @@
    4.13        handle ERROR msg => parse_failed ctxt pos msg "sort");
    4.14  
    4.15  fun parse_typ ctxt =
    4.16 -  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
    4.17 +  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type
    4.18      (fn (syms, pos) =>
    4.19        parse_tree ctxt "type" (syms, pos)
    4.20        |> uncurry (report_result ctxt pos)
    4.21 @@ -362,8 +362,8 @@
    4.22    let
    4.23      val (markup, kind, root, constrain) =
    4.24        if is_prop
    4.25 -      then (Markup.prop, "proposition", "prop", Type.constraint propT)
    4.26 -      else (Markup.term, "term", Config.get ctxt Syntax.root, I);
    4.27 +      then (Markup.language_prop, "prop", "prop", Type.constraint propT)
    4.28 +      else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
    4.29      val decode = constrain o Term_XML.Decode.term;
    4.30    in
    4.31      Syntax.parse_token ctxt decode markup
    4.32 @@ -749,8 +749,8 @@
    4.33  
    4.34  in
    4.35  
    4.36 -val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
    4.37 -val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
    4.38 +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort;
    4.39 +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type;
    4.40  
    4.41  fun unparse_term ctxt =
    4.42    let
    4.43 @@ -760,7 +760,7 @@
    4.44    in
    4.45      unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
    4.46        (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
    4.47 -      Markup.term ctxt
    4.48 +      Markup.language_term ctxt
    4.49    end;
    4.50  
    4.51  end;
     5.1 --- a/src/Pure/Thy/thy_output.ML	Tue Feb 18 15:38:50 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Feb 18 16:34:02 2014 +0100
     5.3 @@ -188,7 +188,7 @@
     5.4  
     5.5  
     5.6  fun check_text (txt, pos) state =
     5.7 - (Position.report pos Markup.document_source;
     5.8 + (Position.report pos Markup.language_document;
     5.9    if Toplevel.is_skipped_proof state then ()
    5.10    else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
    5.11  
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Feb 18 15:38:50 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Feb 18 16:34:02 2014 +0100
     6.3 @@ -241,10 +241,10 @@
     6.4    /* markup selectors */
     6.5  
     6.6    private val highlight_include =
     6.7 -    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
     6.8 -      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE,
     6.9 -      Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE,
    6.10 -      Markup.DOCUMENT_SOURCE)
    6.11 +    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    6.12 +      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    6.13 +      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    6.14 +      Markup.VAR, Markup.TFREE, Markup.TVAR)
    6.15  
    6.16    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    6.17    {
    6.18 @@ -375,23 +375,18 @@
    6.19  
    6.20    private val tooltips: Map[String, String] =
    6.21      Map(
    6.22 -      Markup.SORT -> "sort",
    6.23 -      Markup.TYP -> "type",
    6.24 -      Markup.TERM -> "term",
    6.25 -      Markup.PROP -> "proposition",
    6.26        Markup.TOKEN_RANGE -> "inner syntax token",
    6.27        Markup.FREE -> "free variable",
    6.28        Markup.SKOLEM -> "skolem variable",
    6.29        Markup.BOUND -> "bound variable",
    6.30        Markup.VAR -> "schematic variable",
    6.31        Markup.TFREE -> "free type variable",
    6.32 -      Markup.TVAR -> "schematic type variable",
    6.33 -      Markup.ML_SOURCE -> "ML source",
    6.34 -      Markup.DOCUMENT_SOURCE -> "document source")
    6.35 +      Markup.TVAR -> "schematic type variable")
    6.36  
    6.37    private val tooltip_elements =
    6.38 -    Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
    6.39 -      Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys
    6.40 +    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    6.41 +      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
    6.42 +      tooltips.keys
    6.43  
    6.44    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    6.45      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
    6.46 @@ -434,6 +429,8 @@
    6.47              Some(add(prev, r, (true, pretty_typing("::", body))))
    6.48            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    6.49              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    6.50 +          case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) =>
    6.51 +            Some(add(prev, r, (true, XML.Text("language: " + name))))
    6.52            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
    6.53              if (tooltips.isDefinedAt(name))
    6.54                Some(add(prev, r, (true, XML.Text(tooltips(name)))))