avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
authorwenzelm
Wed Sep 12 13:21:33 2012 +0200 (2012-09-12 ago)
changeset 49321a48f9bbbe720
parent 49320 94bd2fb83d11
child 49322 fbb320d02420
avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/Thy/thy_output.ML
src/Tools/jEdit/src/isabelle_rendering.scala
     1.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Wed Sep 12 12:09:40 2012 +0200
     1.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Wed Sep 12 13:21:33 2012 +0200
     1.3 @@ -64,8 +64,8 @@
     1.4    val doc_sourceN: string val doc_source: Markup.T
     1.5    val antiqN: string val antiq: Markup.T
     1.6    val ML_antiquotationN: string
     1.7 -  val doc_antiquotationN: string
     1.8 -  val doc_antiquotation_optionN: string
     1.9 +  val document_antiquotationN: string
    1.10 +  val document_antiquotation_optionN: string
    1.11    val keywordN: string val keyword: Markup.T
    1.12    val operatorN: string val operator: Markup.T
    1.13    val commandN: string val command: Markup.T
    1.14 @@ -169,7 +169,7 @@
    1.15  
    1.16  val theoryN = "theory";
    1.17  val classN = "class";
    1.18 -val type_nameN = "type name";
    1.19 +val type_nameN = "type_name";
    1.20  val constantN = "constant";
    1.21  
    1.22  val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
    1.23 @@ -222,9 +222,9 @@
    1.24  val (doc_sourceN, doc_source) = markup_elem "doc_source";
    1.25  
    1.26  val (antiqN, antiq) = markup_elem "antiq";
    1.27 -val ML_antiquotationN = "ML antiquotation";
    1.28 -val doc_antiquotationN = "document antiquotation";
    1.29 -val doc_antiquotation_optionN = "document antiquotation option";
    1.30 +val ML_antiquotationN = "ML_antiquotation";
    1.31 +val document_antiquotationN = "document_antiquotation";
    1.32 +val document_antiquotation_optionN = "document_antiquotation_option";
    1.33  
    1.34  
    1.35  (* outer syntax *)
     2.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Wed Sep 12 12:09:40 2012 +0200
     2.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Wed Sep 12 13:21:33 2012 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4    /* logical entities */
     2.5  
     2.6    val CLASS = "class"
     2.7 -  val TYPE_NAME = "type name"
     2.8 +  val TYPE_NAME = "type_name"
     2.9    val FIXED = "fixed"
    2.10    val CONSTANT = "constant"
    2.11  
    2.12 @@ -115,12 +115,12 @@
    2.13    /* embedded source text */
    2.14  
    2.15    val ML_SOURCE = "ML_source"
    2.16 -  val DOC_SOURCE = "doc_source"
    2.17 +  val DOCUMENT_SOURCE = "document_source"
    2.18  
    2.19    val ANTIQ = "antiq"
    2.20 -  val ML_ANTIQUOTATION = "ML antiquotation"
    2.21 -  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
    2.22 -  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
    2.23 +  val ML_ANTIQUOTATION = "ML_antiquotation"
    2.24 +  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
    2.25 +  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
    2.26  
    2.27  
    2.28    /* ML syntax */
     3.1 --- a/src/Pure/Thy/thy_output.ML	Wed Sep 12 12:09:40 2012 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Sep 12 13:21:33 2012 +0200
     3.3 @@ -83,8 +83,8 @@
     3.4      (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
     3.5        (string -> Proof.context -> Proof.context) Name_Space.table;
     3.6    val empty : T =
     3.7 -    (Name_Space.empty_table Isabelle_Markup.doc_antiquotationN,
     3.8 -      Name_Space.empty_table Isabelle_Markup.doc_antiquotation_optionN);
     3.9 +    (Name_Space.empty_table Isabelle_Markup.document_antiquotationN,
    3.10 +      Name_Space.empty_table Isabelle_Markup.document_antiquotation_optionN);
    3.11    val extend = I;
    3.12    fun merge ((commands1, options1), (commands2, options2)) : T =
    3.13      (Name_Space.merge_tables (commands1, commands2),
     4.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 12 12:09:40 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 12 13:21:33 2012 +0200
     4.3 @@ -70,7 +70,7 @@
     4.4        Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
     4.5        Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
     4.6        Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
     4.7 -      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOC_SOURCE)
     4.8 +      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
     4.9  
    4.10    def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
    4.11    {
    4.12 @@ -163,7 +163,7 @@
    4.13        Isabelle_Markup.TFREE -> "free type variable",
    4.14        Isabelle_Markup.TVAR -> "schematic type variable",
    4.15        Isabelle_Markup.ML_SOURCE -> "ML source",
    4.16 -      Isabelle_Markup.DOC_SOURCE -> "document source")
    4.17 +      Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
    4.18  
    4.19    private val tooltip_elements =
    4.20      Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
    4.21 @@ -183,7 +183,8 @@
    4.22          range, Text.Info(range, Nil), Some(tooltip_elements),
    4.23          {
    4.24            case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
    4.25 -            add(prev, r, (true, kind + " " + quote(name)))
    4.26 +            val kind1 = space_explode('_', kind).mkString(" ")
    4.27 +            add(prev, r, (true, kind1 + " " + quote(name)))
    4.28            case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
    4.29            if Path.is_ok(name) =>
    4.30              val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))