# HG changeset patch
# User wenzelm
# Date 1347448893 -7200
# Node ID a48f9bbbe720944accf631c1e7ab8a8e6bf39617
# Parent  94bd2fb83d110fd575eab544bcbdb2583e908f49
avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);

diff -r 94bd2fb83d11 -r a48f9bbbe720 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Wed Sep 12 12:09:40 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Wed Sep 12 13:21:33 2012 +0200
@@ -64,8 +64,8 @@
   val doc_sourceN: string val doc_source: Markup.T
   val antiqN: string val antiq: Markup.T
   val ML_antiquotationN: string
-  val doc_antiquotationN: string
-  val doc_antiquotation_optionN: string
+  val document_antiquotationN: string
+  val document_antiquotation_optionN: string
   val keywordN: string val keyword: Markup.T
   val operatorN: string val operator: Markup.T
   val commandN: string val command: Markup.T
@@ -169,7 +169,7 @@
 
 val theoryN = "theory";
 val classN = "class";
-val type_nameN = "type name";
+val type_nameN = "type_name";
 val constantN = "constant";
 
 val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
@@ -222,9 +222,9 @@
 val (doc_sourceN, doc_source) = markup_elem "doc_source";
 
 val (antiqN, antiq) = markup_elem "antiq";
-val ML_antiquotationN = "ML antiquotation";
-val doc_antiquotationN = "document antiquotation";
-val doc_antiquotation_optionN = "document antiquotation option";
+val ML_antiquotationN = "ML_antiquotation";
+val document_antiquotationN = "document_antiquotation";
+val document_antiquotation_optionN = "document_antiquotation_option";
 
 
 (* outer syntax *)
diff -r 94bd2fb83d11 -r a48f9bbbe720 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Wed Sep 12 12:09:40 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Wed Sep 12 13:21:33 2012 +0200
@@ -78,7 +78,7 @@
   /* logical entities */
 
   val CLASS = "class"
-  val TYPE_NAME = "type name"
+  val TYPE_NAME = "type_name"
   val FIXED = "fixed"
   val CONSTANT = "constant"
 
@@ -115,12 +115,12 @@
   /* embedded source text */
 
   val ML_SOURCE = "ML_source"
-  val DOC_SOURCE = "doc_source"
+  val DOCUMENT_SOURCE = "document_source"
 
   val ANTIQ = "antiq"
-  val ML_ANTIQUOTATION = "ML antiquotation"
-  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
-  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
+  val ML_ANTIQUOTATION = "ML_antiquotation"
+  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
+  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
   /* ML syntax */
diff -r 94bd2fb83d11 -r a48f9bbbe720 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Sep 12 12:09:40 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed Sep 12 13:21:33 2012 +0200
@@ -83,8 +83,8 @@
     (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
       (string -> Proof.context -> Proof.context) Name_Space.table;
   val empty : T =
-    (Name_Space.empty_table Isabelle_Markup.doc_antiquotationN,
-      Name_Space.empty_table Isabelle_Markup.doc_antiquotation_optionN);
+    (Name_Space.empty_table Isabelle_Markup.document_antiquotationN,
+      Name_Space.empty_table Isabelle_Markup.document_antiquotation_optionN);
   val extend = I;
   fun merge ((commands1, options1), (commands2, options2)) : T =
     (Name_Space.merge_tables (commands1, commands2),
diff -r 94bd2fb83d11 -r a48f9bbbe720 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 12 12:09:40 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 12 13:21:33 2012 +0200
@@ -70,7 +70,7 @@
       Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
       Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
       Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
-      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOC_SOURCE)
+      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
 
   def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
   {
@@ -163,7 +163,7 @@
       Isabelle_Markup.TFREE -> "free type variable",
       Isabelle_Markup.TVAR -> "schematic type variable",
       Isabelle_Markup.ML_SOURCE -> "ML source",
-      Isabelle_Markup.DOC_SOURCE -> "document source")
+      Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
 
   private val tooltip_elements =
     Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
@@ -183,7 +183,8 @@
         range, Text.Info(range, Nil), Some(tooltip_elements),
         {
           case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
-            add(prev, r, (true, kind + " " + quote(name)))
+            val kind1 = space_explode('_', kind).mkString(" ")
+            add(prev, r, (true, kind1 + " " + quote(name)))
           case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
           if Path.is_ok(name) =>
             val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))