src/Tools/jEdit/src/rendering.scala
changeset 54702 3daeba5130f0
parent 54515 570ba266f5b5
child 55033 8e8243975860
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Dec 09 09:44:57 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Dec 09 12:16:52 2013 +0100
     1.3 @@ -202,8 +202,9 @@
     1.4  
     1.5    private val highlight_include =
     1.6      Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
     1.7 -      Markup.ENTITY, Markup.PATH, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM,
     1.8 -      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOCUMENT_SOURCE)
     1.9 +      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE,
    1.10 +      Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE,
    1.11 +      Markup.DOCUMENT_SOURCE)
    1.12  
    1.13    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    1.14    {
    1.15 @@ -217,7 +218,7 @@
    1.16    }
    1.17  
    1.18  
    1.19 -  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
    1.20 +  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.URL)
    1.21  
    1.22    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    1.23    {
    1.24 @@ -230,6 +231,10 @@
    1.25              val link = PIDE.editor.hyperlink_file(jedit_file)
    1.26              Some(Text.Info(snapshot.convert(info_range), link) :: links)
    1.27  
    1.28 +          case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
    1.29 +            val link = PIDE.editor.hyperlink_url(name)
    1.30 +            Some(Text.Info(snapshot.convert(info_range), link) :: links)
    1.31 +
    1.32            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    1.33            if !props.exists(
    1.34              { case (Markup.KIND, Markup.ML_OPEN) => true
    1.35 @@ -335,7 +340,7 @@
    1.36  
    1.37    private val tooltip_elements =
    1.38      Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
    1.39 -      Markup.ML_TYPING, Markup.PATH) ++ tooltips.keys
    1.40 +      Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys
    1.41  
    1.42    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    1.43      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
    1.44 @@ -371,6 +376,8 @@
    1.45            if Path.is_ok(name) =>
    1.46              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    1.47              Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
    1.48 +          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
    1.49 +            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
    1.50            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
    1.51            if name == Markup.SORTING || name == Markup.TYPING =>
    1.52              Some(add(prev, r, (true, pretty_typing("::", body))))