src/Tools/jEdit/src/isabelle_rendering.scala
changeset 49321 a48f9bbbe720
parent 49294 a600c017f814
child 49355 7d1af0a6e797
     1.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 12 12:09:40 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 12 13:21:33 2012 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4        Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
     1.5        Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
     1.6        Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
     1.7 -      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOC_SOURCE)
     1.8 +      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
     1.9  
    1.10    def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
    1.11    {
    1.12 @@ -163,7 +163,7 @@
    1.13        Isabelle_Markup.TFREE -> "free type variable",
    1.14        Isabelle_Markup.TVAR -> "schematic type variable",
    1.15        Isabelle_Markup.ML_SOURCE -> "ML source",
    1.16 -      Isabelle_Markup.DOC_SOURCE -> "document source")
    1.17 +      Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
    1.18  
    1.19    private val tooltip_elements =
    1.20      Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
    1.21 @@ -183,7 +183,8 @@
    1.22          range, Text.Info(range, Nil), Some(tooltip_elements),
    1.23          {
    1.24            case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
    1.25 -            add(prev, r, (true, kind + " " + quote(name)))
    1.26 +            val kind1 = space_explode('_', kind).mkString(" ")
    1.27 +            add(prev, r, (true, kind1 + " " + quote(name)))
    1.28            case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
    1.29            if Path.is_ok(name) =>
    1.30              val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))